# Claude Produced a Machine-Checked Proof of Fermat's Last Theorem in 13 Million Lines of Lean

Anthropic says a team of Claude agents worked largely autonomously for 11 days and proved 29,500 intermediate theorems, a formalization more than five times the size of Lean's main mathematics library.

- Published: 2026-09-08T06:18:45.692Z
- Canonical: https://polylog.news/ai/2026-09-08/claude-produced-a-machine-checked-proof-of-fermat-s-last-the
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [Anthropic Research](https://www.anthropic.com/research/formalizing-fermats-last-theorem), [Anthropic Research (paper)](https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf)

Anthropic [published what it describes as the first complete, computer-checked proof of Fermat's Last Theorem](https://www.anthropic.com/research/formalizing-fermats-last-theorem), written in the Lean proof assistant by Claude agents over 11 days with limited human intervention. The result is large: roughly 13 million lines of Lean code and 29,500 intermediate theorems, more than five times the size of Mathlib, the community-maintained Lean mathematics library.

The important property is not the size but the checking. Anthropic says the proof uses only Lean's three standard axioms and contains no omitted steps, meaning no placeholder arguments and no additional axioms introduced to close a gap. That claim can be verified mechanically by anyone who runs the Lean kernel against the [published repository](https://www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf), which puts it in a different category from a self-reported benchmark score. Kevin Buzzard of Imperial College London, who leads the long-running human effort to formalize the same theorem in Lean, [called it an extraordinary autoformalization achievement](https://thenextweb.com/news/anthropic-claude-fermat-last-theorem-lean-buzzard).

Two limits deserve stating plainly. The underlying mathematics was already proved by Andrew Wiles and Richard Taylor in the 1990s, so this is a translation of an existing argument into machine-checkable form rather than a new theorem. And the human blueprint work that broke the proof into formalizable pieces predates the model. What changed is the speed of a task where correctness can be checked by a machine, which is exactly the setting where long-horizon agents are least likely to produce an undetected error.

## What this means

Formal verification is the clearest case where an agent's output can be validated without having to trust the agent, and that is the channel through which this result matters commercially. The same process, generating a candidate proof and then having a checker reject or accept it, applies to hardware design rules, cryptographic protocol proofs, compiler correctness and safety-critical software. Vendors selling verification tools gain a large new source of demand for proof capacity, while the scarce resource shifts from proof engineers to computing power and to the blueprints that break a problem into checkable pieces.

## What to watch

- Whether independent mathematicians run the Lean kernel over the repository and confirm that it compiles without errors. That is the only verification that matters here, and it is inexpensive to do.
- Whether Mathlib's maintainers accept machine-generated contributions at scale, or set review rules that slow them down. Their decision will set the norm for how autoformalization enters shared mathematical infrastructure.
- Whether the same agent process is applied to industrial verification targets such as chip design rules or cryptographic protocols, which is where the technique would generate revenue.