Formal Proofs (Lean, Rocq)
Proof assistants check mathematics without gaps; in September 2026 Anthropic reported that Claude agents formalized Fermat's Last Theorem in Lean in 11 days (checked by Kevin Buzzard).
Open in the interactive tree →A proof assistant such as Lean or Rocq (formerly Coq) accepts only proofs in which every step is mechanically correct. Early milestones were the four-color theorem (Coq, 2005) and the Kepler sphere-packing theorem (Flyspeck, 2014). The Mathlib library, started in 2017, grew into a shared framework for modern mathematics in Lean.
As of October 2026
Kevin Buzzard began a multi-year project in 2024 (EPSRC grant of about GBP 1 million, five years) to formalize Fermat's Last Theorem in Lean along a modern route. On 4 September 2026 Anthropic reported that Claude agents produced a complete Lean proof in 11 days: about 13 million lines, 29,500 theorems and roughly 6 billion output tokens, using only Lean's three standard axioms; Buzzard compiled and checked it himself. It follows the 1995 Darmon-Diamond-Taylor account of Wiles's argument, so the mathematics is not new; what is new is that thousands of pages of literature were formalized automatically.
Open steps
- Checking that statements are faithful High AI leverageBuild tools and benchmarks that catch Lean statements which compile but do not say what the paper means; a large share of compiling statements are wrong today.
- Compress and refactor huge proofs High AI leverageCut the 13-million-line Fermat development into a modular, readable library that people can maintain; machine output is not structured the way human libraries are.
- Fill library gaps for whole fields Medium AI leverageWrite the missing definitions and basic theorems (for example modern algebraic geometry or PDE) so more papers can be formalized without building the groundwork first.
- Cut tokens and compile time Medium AI leverageReduce the roughly 6 billion output tokens and long compile times of large formalization runs through better proof search, caching and faster elaboration.
Where AI could help
High AI leverage. Formalization is code writing and checking, and agents did Fermat in 11 days; what remains is library breadth, readability and cost.
- Autoformalize landmark theorems and whole textbooks along known proof routes
- Fill Mathlib gaps in large fields such as algebraic geometry
- Refactor machine output into shorter modular libraries that people can maintain
- Audit that formal statements say what the paper meant
Shown so far
- In September 2026 coordinated Claude agents produced a Lean 4 formalization of Fermat's Last Theorem along a known route in 11 days (about 13 million lines), reviewed by Kevin Buzzard. source
- In September 2025 Math Inc reported that its agent Gauss formalized the strong Prime Number Theorem in Lean in about three weeks (about 25,000 lines), according to the company. source
- A preprint (submitted June 2026, revised October 2026) reports that a tool-augmented GPT-5.2 agent compiled 87.2% of graduate-level statements into Lean but only 57.7% were judged faithful. source
Prerequisites
- Gödel's Incompleteness1931
- Programmable Computer1941
- Four Colour Theorem Proved1976Gonthier's formal proof of the four colour theorem (2005) was a landmark of machine-checked proof
- Kepler Conjecture & Flyspeck1998-2014Flyspeck (2014) is an early full formalisation of a long computer-assisted proof
- Sphere Packing in 8 & 24 Dims2016Both sphere-packing proofs were formalised in Lean with AI help in March 2026