Lean formalization: Liquid Tensor Experiment
Formalización en Lean: Liquid Tensor Experiment y mathlib
- Date
- 2022 · confidence high
- Place
- Bonn (Germany) and London (Imperial College)
- Credited to
- Peter Scholze (challenge), Johan Commelin and the mathlib community (Kevin Buzzard and others)
- People
- 👤 Peter Scholze1987–
- Field
- Knowledge & symbols
What was discovered
A complete verification, in 18 months, in the Lean proof assistant of a cutting-edge theorem by Clausen and Scholze on condensed mathematics. It showed that current research mathematics can be formalised and gave a major boost to the mathlib library.
The Flyspeck project and Gonthier's proof of the Feit-Thompson theorem in Coq (2012) were the large-scale precedents.
What it led to
- the systematic formalisation of mathematics
- formalisation projects for Fermat's theorem (2024-) and the prime number theorem
- AI for automated theorem proving (AlphaProof)
Built on
- Russell paradox and Principia Mathematica1901
- Coq (four-colour theorem, 2005)
- Flyspeck (2014)
- Martin-Lof type theory
Made possible
- AI mathematical proving at Olympiad level2024-2025
- proof assistants embedded in research