Claude got a machine to check the proof of Fermat’s Last Theorem

Fermat’s Last Theorem fits in one sentence: if n is a whole number greater than two, no three positive whole numbers satisfy the equation x^n + y^n = z^n.

At n equals two, solutions are everywhere. For cubes, fourth powers and anything above, there is not a single one, and that holds for infinitely many equations at once.

Fermat wrote this in the margin of Diophantus’s Arithmetica in 1637 and added that he had found a truly marvelous proof, but the margin was too narrow to hold it. That proof never surfaced.

The theorem stayed open for 358 years. Andrew Wiles closed it in 1995, filling the last gap with Richard Taylor. So the proof is Wiles’s, not Claude’s.

Something else stayed open: there was no version of that proof a machine could check from start to finish. Refereeing a proof at this scale takes humans years.

Kevin Buzzard took that job on with a five-year, £1 million grant in 2024. His 2029 target was not even the whole proof. It was to reduce the theorem to a set of claims already known by the end of the 1980s.

Anthropic announced on September 4 that Claude had translated Wiles’s proof into Lean and had a machine verify it end to end. The result is the first computer-checked proof of the theorem.

The run began in early August and took 11 days, with Claude working largely on its own throughout. The proof compiled on August 18.

No new mathematics was produced. The one thing that changed is that the argument now sits in a language a machine can check line by line.

The numbers sit outside the usual scale.

Claude wrote 13 million lines of Lean. It proved 30,300 intermediate theorems and used 29,500 of them in the final proof. Getting there cost roughly 6 billion output tokens.

For scale: that is more than five times the size of Mathlib, the library the Lean community has spent years building.

This was not one model in one long session. Anthropic built a multi-agent harness on top of Claude Code and ran dozens of agents at once.

What held them together is Prove2Me, an open formalization platform built by Tianyi Peng and collaborators at Columbia University. It keeps theorem statements in a directed acyclic graph, speeds up Lean compilation, and lets agents search and reuse proved theorems through plain-language descriptions.

The model itself was an internal research model that Anthropic describes as roughly comparable to Claude Fable 5.1.

None of this appeared from nowhere. Three community projects sit underneath it: Mathlib, Kevin Buzzard’s FLT project at Imperial College London, and flt-regular.

Claude adapted pieces from that work. Lean verified the finished proof, and a separate comparator confirmed the statement it proved matches Mathlib’s.

On that side of it, Buzzard’s verdict: “This extraordinary autoformalization achievement proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics.”

On the mathematics, the same Buzzard is far harsher: the work “just faithfully follows the early literature on the proof and adds nothing.” Nothing new enters the mathematical record.

The code runs to 13.4 million lines and takes nearly twenty times longer to compile on a 96-core machine. As it stands it cannot enter Mathlib either, because the library does not accept AI-generated reviews.

One gap remains, and it is semantic: humans still have to check that the intermediate statements say the mathematics their names claim.