What mathematicians should know about the Lean Theorem Prover: reliability & AI
What Mathematicians Should Know About the Lean Theorem Prover: Reliability & AI
Guest post by Thomas Hales, published on Terence Tao's blog (October 9, 2026).
Introduction: The Value of Mathematical Certainty
In discussions regarding the intrinsic value of mathematics, I find that the most critical aspects are its consistency and its unrivaled reliability. These qualities provide the essential bedrock upon which science and modern civilization are constructed.
Defining Formalization
A formal proof is not merely a standard mathematical argument; it is a proof that has been rigorously verified down to the most basic foundations of mathematics and the core rules of logic. While theoretically possible to perform by hand, the sheer volume of steps makes this impractical. Instead, we utilize specialized software.
Below are several landmark theorems that have undergone this process:
| Theorem | Status | Note |
|---|---|---|
| Four-Color Theorem | Formalized | Classic example of computer-aided proof |
| Feit-Thompson Theorem | Formalized | Odd-order theorem |
| Kepler Conjecture | Formalized | Required massive effort |
| Sphere Eversion | Formalized | Topological verification |
| Sphere Packing (8D & 24D) | Formalized | Recent breakthroughs |
| Navier-Stokes Forced Blowup | Formalized | Completed in 2026 |
| Fermat's Last Theorem | Formalized | Completed in 2026 |
The completion of the final three projects this year has significantly increased the mathematical community's awareness of formalization's potential.
The Ecosystem of Proof Assistants
Software designed for this purpose is referred to by several names, which are generally used interchangeably:
- Proof Assistants
- Theorem Provers
- Interactive Theorem Provers (ITPs)
Historically, various systems have emerged. Freek Wiedijk’s work, "The Seventeen Provers of the World," provides a comparative look at these tools by implementing the proof that is irrational across different systems. Some notable examples include:
AutomathHOL LightIsabelleCoq(recently rebranded as Rocq)MetamathMizarLeanThe current favorite among mathematicians.
The Evolution of Lean
Lean was launched in 2013 by Leo de Moura while he was at Microsoft. Crucially, de Moura ensured the software remained open-source. According to Kevin Hartnett's The Proof in the Code, Jeremy Avigad (Director of ICARM at Carnegie Mellon) was the tool's first adopter.
mathlib has grown into a colossal resource. Its current scale is staggering:
- Theorems:
- Definitions:
- Codebase: million lines
- Contributors:
This library allows mathematicians to cite established results (like the Cauchy-Schwarz inequality) without needing to re-prove them from scratch.
The Era of Autoformalization
Historically, moving from a "paper proof" to a "formal proof" was a grueling manual process. For instance, the Kepler conjecture took roughly 20 human work-years and resulted in 500,000 lines of script.
The dream has always been autoformalization: using AI to read a or PDF file and automatically generate the corresponding Lean code.
Recent Milestones (2025–2026)
The momentum shifted dramatically in 2025. We have seen a transition from "quasi-autoformalization" (where humans guide the AI) to fully autonomous generation.
- Prime Number Theorem: Achieved via quasi-autoformalization.
- Formal Topology: Urban produced 130k lines of formal topology based on Munkres' textbook in just two weeks.
- 24D Sphere Packing: Math Inc. autoformalized Viazovska's proof. The initial output was
500K SLOC, which was later "golfed" (pruned) down to 200K lines. - ATLAS Project: Meta/Facebook Research autoformalized large portions of 26 textbooks in May 2026.
- Fermat's Last Theorem: Announced by Anthropic on September 4, 2026.
- Navier-Stokes Blowup: Announced by OpenAI on September 8, 2026, including a Lean formalization.
"We believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used." — Urban, January 2026
This shift is viewed by some, like Jesse Han, as a "revolutionary transformation" where massive-scale formalization becomes the norm. Furthermore, Jared Lichtman launched the MAP (Mathematics Autoformalization Project) on September 8, 2026, with the ambitious goal of translating all known mathematics into formal code.
Technical Foundations
Lean is built upon Type Theory, specifically a version known as the Calculus of Inductive Constructions (CIC).
To understand why this is necessary, one must recall the crisis in set theory triggered by Russell's Paradox in 1901, which concerned the set of all sets that do not contain themselves:
(The article continues into the specifics of type theory...)
Visual Gallery
Community Contributors:
