Anthropic announced a mathematics milestone on 5 September: its Claude model produced the first fully machine-checked proof of Fermat’s Last Theorem in the Lean proof language – in just eleven days and working largely autonomously.
What Claude accomplished
Over eleven days of compute, Claude wrote roughly 13 million lines of Lean code and proved about 29,500 intermediate theorems that fed into the final result, according to Anthropic. The formalization is more than five times the size of Mathlib, the established community mathematics library. The effort consumed around six billion output tokens from an internal research model, spread across several agents working in parallel.
- Duration: 11 days, largely autonomous
- Scale: roughly 13 million lines of Lean code
- Intermediate theorems: about 29,500 in the final proof
How the agents collaborated
Multiple Claude instances split the work through Prove2Me, a platform built by researcher Tianyi Peng and colleagues at Columbia University. Early attempts failed because the agents lost track of the project’s state and stopped collaborating effectively. Only Prove2Me – which manages theorem statements in a directed graph and speeds up Lean compilation – enabled the coordinated formalization to succeed.
What it means
Mathematician Kevin Buzzard of Imperial College London reviewed the proof and called it an extraordinary autoformalization achievement that establishes Fermat’s Last Theorem with no assumptions beyond the axioms of mathematics. Anthropic concedes the generated version is probably far longer than it needs to be. Even so, the result signals how AI agents could increasingly automate formal mathematics.
Sources: Anthropic Research · The Next Web
