Claude formalizes Fermat's Last Theorem in Lean
An internal research model produced 13 million lines of proof code in 11 days, and Imperial College mathematician Kevin Buzzard signed off on it.
Symbolic image: at a workstation at night, monitors fill with abstract verification blocks while a person seen from behind works through an open manuscript.
Anthropic says an internal research model rewrote Andrew Wiles' 1995 proof of Fermat's Last Theorem as 13 million lines of machine-checkable Lean code in 11 days.
At a glance
- 13 million lines of Lean code in 11 days — more than five times the size of the Mathlib library, per Anthropic.
- 30,300 theorems proved in total; 29,500 of them feed the final proof.
- Roughly six billion output tokens, generated by several dozen agents running in parallel.
- The starting point is Andrew Wiles' 129-page proof from 1995; Kevin Buzzard (Imperial College London) reviewed the result.
- Side result: three personal Claude Max plans formalized Vinogradov's Three Primes Theorem in three days.
On September 4, 2026, Anthropic published what it describes as the first complete computer-checked proof of Fermat's Last Theorem. An internal research model translated Andrew Wiles' 129-page 1995 proof into Lean, a language in which every inference has to be spelled out for a compiler to accept it. The output runs to 13 million lines. Mathematicians had estimated the job would take years; it took 11 days.
The numbers behind the run
Anthropic puts the model roughly on par with Claude Fable 5.1 and says it is an internal research build rather than a shipped product. Several dozen agents worked in parallel and burned through about six billion output tokens. They proved 30,300 theorems along the way, 29,500 of which the final proof actually uses.
Scale is what separates this from earlier formalization work. Anthropic reckons the artifact at over five times the size of Mathlib, the community library the proof itself depends on — one run outweighing a corpus built collectively over years.
Why the reviewer matters
Kevin Buzzard of Imperial College London checked the result, and he is an unusually well-placed skeptic: since 2024 he has led the community effort formalizing the same theorem by hand.
His verdict points at two things. The proof rests on nothing beyond the standard axioms of mathematics, and it spans algebra, harmonic analysis, geometry and number theory at once. Buzzard also notes that the intermediate artifacts are now solid enough for other people to build on — a claim about durability, not just about one headline result.
The tool that unstuck it
The first attempt failed outright. What changed the outcome was Prove2Me, an open-source collaborative formalization platform built by Tianyi Peng and colleagues at Columbia University; Peng led the effort at Anthropic. It coordinates how agents split the work and cuts inference cost in the process.
How much it cuts shows up in a smaller experiment: three personal Claude Max plans, running on Prove2Me, formalized Vinogradov's Three Primes Theorem in three days.
What neither source states
No dollar figure for compute appears in either publication, and neither names the hardware. The six billion tokens are the only cost signal on offer.
Nor does either say whether anyone besides Buzzard has reviewed the output. The Lean compiler guarantees each step follows from the last; whether the formal statement at the top is really Fermat's Last Theorem is still a human judgment.
FAQ
What is Fermat's Last Theorem?
It states that no three positive integers satisfy a to the power n plus b to the power n equals c to the power n for any n greater than 2. Andrew Wiles proved it in 1995 across 129 pages.
How long did the formalization take?
Eleven days. Several dozen agents ran in parallel and produced 13 million lines of Lean code, spending roughly six billion output tokens in the process.
Who checked that the proof is correct?
Kevin Buzzard of Imperial College London reviewed it, and the Lean compiler verifies every formal step. Neither source mentions any additional independent review.
