Fermat's Last Theorem formalized end to end in Lean 4
A complete machine-checked proof of Fermat's Last Theorem in Lean 4, written by AI agents in eleven days, resting on Lean's three standard axioms and accepted by two independent kernels.
- Lab
- Anthropic
- Model
- Internal Anthropic research model, described in the announcement as roughly comparable to Claude Fable 5.1
- Field
- Mathematics
- Date
- 2026-09-04
- Human collaborators
- Tianyi Peng
- Problem posed
- 1637 · open 389 yrs
Sources
Original work
Announcement
Independent commentary
What was found
The repository states the theorem over Lean's built-in naturals as fermat_last_theorem, and its default build target FinalCheck.lean derives Mathlib's own FermatLastTheorem from it, so the statement is not a bespoke restatement. The build fails unless the proof depends on exactly propext, Classical.choice and Quot.sound: no sorry, no added axiom, no native_decide. Three checks are recorded. A from-scratch build compiled all 60,475 modules; leanprover/comparator v4.33.0 checked the result against a Mathlib-only Challenge.lean and returned 'Your solution is okay!'; and nanoda 0.4.13, an independent Lean kernel written in Rust, accepted an export of the same environment with 1,052,234 declarations and no errors. The argument formalized is the classical one of Frey, Serre, Ribet, Wiles and Taylor-Wiles, and the development builds on the Imperial College London FLT project, flt-regular and Mathlib, with 106 files containing material from the first two.
Novelty check
This is a formalization, not a new theorem, and the entry is graded as such. Wiles and Taylor-Wiles proved Fermat's Last Theorem in 1995; nothing mathematically new is claimed here, and Kevin Buzzard states directly that 'mathematically this work of anthropic tells us essentially nothing' and that 'the formalization just faithfully follows the early literature on the proof and adds nothing'. What is new is the scale of autoformalization: prior partial formalizations existed, notably the ongoing Imperial College FLT project this work builds on, and no complete machine-checked proof of the theorem existed before. It completes the last open item of Wiedijk's list of 100 theorems.
Caveats and known objections
The result is a formalization of an existing proof and should not be read as new mathematics. Verification is graded formal on the machine checks rather than on the announcement: the comparator check ties the proved statement to Mathlib's own, and a second independent kernel replayed it. What no tool establishes, and the repository says so itself, is that each intermediate theorem means what its name suggests, since names are machine-generated and 'where a name and a statement disagree the statement is what was proved'. Buzzard reports the codebase is over 13.4 million lines and that the proof as formalized only works for exponents p at least 17, with smaller cases covered by earlier work. Reproducing the checks is expensive: the build takes hours at 96 jobs with a peak of 153 GB of memory, and the comparator run about 15 hours. Autonomy is graded ai-led rather than autonomous: the announcement describes Claude working 'largely autonomously' but also records high-level human steering from Tianyi Peng, and the strictest defensible reading applies.
Independent checks
Kevin Buzzard, Imperial College London, who leads the FLT formalization project this work builds on: Ran the comparator and reports the proof checks out. States he 'manually inspected every line of the code base which (according to Claude) was not a mathematical definition or proof of a theorem', looking for soundness exploits, and that random reads of the mathematics were clearly developing FLT the classical way. Judges the mathematical contribution to be nil. · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Fermat's Last Theorem formalized end to end in Lean 4. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-04-fermat-last-theorem-leanBibTeX
@misc{whataifound-anthropic-2026-lean,
title = {Fermat's Last Theorem formalized end to end in Lean 4},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Anthropic. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-04-fermat-last-theorem-lean}
}