Formalizing Fermat's Last Theorem
An AI system has produced a complete Lean formalization of Fermat’s Last Theorem in 11 days, generating 13 million lines of machine-checked proof code for one of modern mathematics’ most famous results. Commenters see this as a milestone for automated theorem proving and formal methods, but raise concerns about verification trust (possible bugs in proof assistants), proof readability, and whether such gigantic AI-generated formalizations are reusable or meaningful to humans. The thread also explores broader implications: the cost and efficiency of large-scale AI reasoning, its impact on mathematical careers and research funding, and whether future systems might move from formalizing known proofs to discovering fundamentally new ones.
Nature of the result
- Thread emphasizes this is not a new mathematical proof of Fermat’s Last Theorem (FLT), but a Lean formalization of an existing Wiles/Taylor-style proof.
- Several commenters note the math community already considered FLT essentially settled; the novelty is the autoformalization scale and speed.
- The formalization follows a 1990s exposition, not the most modern streamlined approaches, and handles primes ≥17; other prior formalizations cover the remaining cases.
Scale, cost, and tooling
- Claude produced ~13M lines of Lean and ~29.5k lemmas in ~11 days, using ~6B output tokens and large compute (hundreds of GB RAM, many cores).
- Rough cost estimates at public API prices are around hundreds of thousands of dollars, but there is debate about whether internal inference is much cheaper and how to amortize training cost.
- A collaborative Lean platform (prove2.me) and custom orchestration (“swarm of agents”) were key; some see this as evidence that structured tooling is crucial for serious work.
Trust, correctness, and Lean’s kernel
- Many ask: how can 13M lines be trusted? Response: Lean’s type checker verifies each step; humans mainly need to trust:
- the formal statement of FLT,
- the small kernel and axioms,
- and a secondary checker (“comparator”) that re‑verifies the final theorem.
- Others caution that Lean has had recent soundness bugs, including an AI‑found Collatz “disproof” exploiting a kernel bug; multiple independent checkers reduce but don’t eliminate risk.
- Some want translation to other systems (e.g., HOL/Metamath) for additional assurance.
Value to mathematics and reuse
- Supporters: huge proof efforts typically generate many reusable abstractions; autoformalization can catch literature errors and reduce referee burden.
- Skeptics: 13M lines may be “AI slop” with poor abstractions, hard to integrate into standard libraries; may not advance human understanding.
- An ongoing human FLT formalization project had different goals: contributing clean, general mathlib components and a human-explorable “dynamic document.”
Impact on mathematicians and careers
- Mixed emotions: awe at capability, concern for early‑career researchers being “scooped” by LLMs.
- Some argue formalizing is distinct from discovering proofs, so there’s still a large role for human creativity and exposition.
Broader AI implications and ethics
- Optimists see this as evidence AI can tackle large swaths of math and, by analogy, scientific problems (e.g., medicine, physics).
- Pessimists worry about concentration of power, opaque compute budgets, hype for IPOs, and limited public access to the strongest models.
- Philosophical debate appears about human meaning, “playing God” (e.g., curing aging), and whether AI progress improves or undermines human welfare.
Future directions
- Suggested next targets: classification of finite simple groups, Riemann Hypothesis, P vs NP.
- Several want subsequent AI passes to radically simplify and refactor the FLT formalization, or show it’s near‑minimal in some formal sense.