Claude Completes First Fully Machine-Verified Proof of Fermat's Last Theorem in 11 Days

One of mathematics' most storied proofs is now machine-checked from end to end — and a language model did the encoding. Anthropic announced that Claude completed the first formalized proof of Fermat's Last Theorem, converting the mathematical reasoning behind Andrew Wiles' celebrated 1995 result into Lean code that a computer proof assistant verified in full.

The numbers

The scale is unlike anything previously attempted in formalization. Working over 11 days with only limited high-level human input, Claude produced roughly 13 million lines of Lean — the largest Lean codebase ever written — and proved about 29,500 intermediate theorems along the way. The system spun up several dozen agents that generated some 6 billion tokens of output, orchestrated through Prove2Me, an open-source platform for large-scale automated proving.

Why this was considered a years-long problem

Formalization is brutal, unglamorous work: every lemma, every implicit "it is easy to see," must be made explicit enough for a proof checker. Imperial College's long-running FLT formalization project — which had been methodically encoding the proof with a team of human contributors and, more recently, AI autoformalization tools — estimated completion was still years away. In a candid blog post titled "Anthropic has beaten me to it," project lead Kevin Buzzard acknowledged the result, noting both its magnitude and the questions it raises about how the mathematical community should audit and maintain machine-generated formal corpora.

The payoff is more than symbolic. A fully formal proof rules out human error in verification and turns the proof's entire dependency graph — hundreds of results across algebraic geometry and number theory — into reusable, machine-checkable building blocks for future work.

The new frontier: math at industrial scale

The result reframes what "AI for mathematics" means in practice. Rather than conjuring novel theorems, the near-term revolution is throughput: converting humanity's existing mathematical edifice into verified code, at a pace no human team can match. With Mistral's Leanstral models pushing formal verification in Europe and Chinese labs benchmarking on formal reasoning suites, formalization is quietly becoming a competitive axis among frontier labs — one where the output, unusually for AI, can be checked with absolute certainty.