All Mathematics Machine-Checked
Having every important theorem checked gap-free by machine is still far off; in September 2026 AI agents formalized the whole proof of Fermat's Last Theorem, but most research mathematics is not formalized.
Open in the interactive tree →Mathematics lives in papers that a human reads and judges correct; errors and gaps do occur. Lean and Mathlib provide a shared, mechanically checkable framework, but it covers only part of research mathematics. The goal: every new theorem arrives with a machine-checked proof.
As of October 2026
September 2026: the Fermat's Last Theorem formalization shows that AI agents can formalize thousands of pages of literature in days (13 million lines of Lean, more than five times the size of Mathlib itself, compiling nearly 20 times slower than Mathlib on a 96-core machine). AI systems also verify new results in Lean (Erdős 728, the Navier-Stokes blow-up in 17 hours). Breadth remains the gap: many fields, definitions and older proofs are not yet formalized, and the machine proofs are unreadable to humans.
What is missing
- Definitions and libraries for large areas (for example modern algebraic geometry) are missing
- Understandable, maintainable proofs instead of machine bulk: nobody reads 13 million lines
- Compute and money: roughly 300,000 US dollars of output tokens at list prices for the Fermat proof (a press estimate)
- Community standards across Lean, Rocq and Isabelle, and trust in the checkers themselves
Becomes possible once solved
- Mathematics in which errors are technically excluded
- Verified software, chips and protocols at large scale
- AI-generated proofs that can be trusted without human re-checking
Open steps
- Library coverage for whole fields High AI leverageWrite the definitions and foundational results missing from Lean's Mathlib for large areas such as modern algebraic geometry, so current research papers can be stated in Lean.
- Readable, maintainable machine proofs Medium AI leverageCompress and refactor machine-written Lean developments (13 million lines for Fermat) into shorter, modular libraries that people can maintain.
- Faithful formal statements Medium AI leverageBuild reliable ways to confirm a Lean statement says what the paper meant; today formal statements compile far more often than they are faithful.
- Cutting formalization cost and time Medium AI leverageReduce the token cost and compile time of large formalizations; the Fermat project compiled about 20 times slower than Mathlib on 96 cores.
- Shared standards across proof assistants Low AI leverageMake results portable between Lean, Rocq and Isabelle, and establish trust in the checkers themselves through independent kernels.
Where AI could help
High AI leverage. Autoformalization is AI work: agents formalized Fermat's Last Theorem in 11 days; the limits left are libraries, readability and cost.
- Autoformalize published proofs, turning thousands of pages into checked Lean code in days
- Fill missing definitions and library gaps, for example in algebraic geometry
- Check AI-generated new results mechanically before humans spend time on them
- Compress machine proofs into shorter, readable, maintainable form
Shown so far
- In September 2026 coordinated Claude agents produced a machine-checked Lean 4 formalization of Fermat's Last Theorem in 11 days (about 13 million lines), a known proof, reviewed by Kevin Buzzard. source
- In September 2025 Math Inc reported that its agent Gauss finished a Lean formalization of the strong Prime Number Theorem in about three weeks (about 25,000 lines), according to the company. source
- In November 2025 DeepMind published AlphaProof in Nature, a reinforcement-learning system that proves problems in Lean and reached silver-medal level at the 2024 Math Olympiad. source
Prerequisites
- Four Colour Theorem Proved1976The debate over the computer proof pushed the goal of fully machine-checked mathematics
- Formal Proofs (Lean, Rocq)2005-2026
- Busy Beaver BB(5) Proved2024BB(5) shows a crowd-built proof can be fully machine-checked in Rocq
- AI Wins Math Olympiad Gold2025