Formalizing Fermat's Last Theorem
Claude agents wrote the first complete computer-checked Lean proof of Fermat's Last Theorem in about 11 days, with 13 million lines of Lean.
Dozens of agents, coordinated through Columbia's Prove2Me platform and an internal model roughly comparable to Fable 5.1, proved 30,300 theorems (29,500 used), over 5x the size of Mathlib. It follows a simplified version of Wiles's proof; Kevin Buzzard, who leads the community formalization, endorsed the result.
- Date
- Friday, 4 September 2026
- Lab
- Anthropic
- Kind
- paper
- Access
- paper only
Figures
| Measure | Value | Measured by |
|---|---|---|
| Time to full Lean proof | about 11 days post's method section says a little under two weeks | company |
| Lean code and theorems in the final proof | 13 million lines, 29,500 theorems over 5x Mathlib; about six billion output tokens | company |
The new part is the verification of Wiles's argument as simplified by Darmon, Diamond and Taylor, built on top of Mathlib and the Buzzard-led community project, and it adds no new mathematics. Early agent attempts failed and contributed about 7% of final lines. Buzzard's endorsement is quoted in Anthropic's post and was not independently reproduced here.
Sources
This record was checked against its sources on 6 October 2026. How we check