ICTS:31586

Video URL

Finding theorems in Lean and Mathlib

Finding theorems in Lean and Mathlib

(2025). Finding theorems in Lean and Mathlib. SciVideos. https://youtube.com/live/9EFNKCHQE0M

Finding theorems in Lean and Mathlib. SciVideos, Apr. 25, 2025, https://youtube.com/live/9EFNKCHQE0M 

          @misc{ scivideos_ICTS:31586,
            doi = {},
            url = {https://youtube.com/live/9EFNKCHQE0M},
            author = {},
            keywords = {},
            language = {en},
            title = {Finding theorems in Lean and Mathlib},
            publisher = {},
            year = {2025},
            month = {apr},
            note = {ICTS:31586 see, \url{https://scivideos.org/icts-tifr/31586}}
          }
Ricardo Brasca
Talk numberICTS:31586
Source RepositoryICTS-TIFR
Collection

Abstract

Mathlib is a vast and constantly growing library of formalized mathematics. As its size increases, it becomes increasingly easy to spend a significant amount of time formalizing a theorem, only to later discover that it was already present in the library. This can be both frustrating and discouraging. In this talk, we will introduce and demonstrate a variety of tools and techniques that can help users efficiently navigate Mathlib, search for existing results, and better understand the structure of the library.