ICTS:31590

Video URL

Redoing definitions in the Lean Mathematical Library

Redoing definitions in the Lean Mathematical Library

(2025). Redoing definitions in the Lean Mathematical Library. SciVideos. https://youtube.com/live/pQf-GLnQLt8

Redoing definitions in the Lean Mathematical Library. SciVideos, Apr. 24, 2025, https://youtube.com/live/pQf-GLnQLt8 

          @misc{ scivideos_ICTS:31590,
            doi = {},
            url = {https://youtube.com/live/pQf-GLnQLt8},
            author = {},
            keywords = {},
            language = {en},
            title = {Redoing definitions in the Lean Mathematical Library},
            publisher = {},
            year = {2025},
            month = {apr},
            note = {ICTS:31590 see, \url{https://scivideos.org/icts-tifr/31590}}
          }
Anne Baanen
Talk numberICTS:31590
Source RepositoryICTS-TIFR
Collection

Abstract

Mathematicians have trained themselves to see objects from many points of view. When considering the real numbers, we can as easily see them as equivalence classes of Cauchy sequences, or Dedekind cuts, or the unique uniformly complete Archimedean field. The computer is not as forgiving and forces us to pick a particular definition that we must stick with. Using examples from the Lean mathematical library, Mathlib, I investigate why it is so important to choose the right definition when formalizing, what makes formal definitions look different from pen and paper definitions, and how we can design our definitions to make proofs flow smoothly.