Anthropic Says Claude Formalised a Complete Proof of Fermat's Last Theorem

Anthropic says dozens of Claude Code agents have produced the first complete, machine checked formalisation of Andrew Wiles' proof of Fermat's Last Theorem, using the Lean 4 proof assistant. The project, run on a platform called Prove2Me, generated 13 million lines of Lean code and 29,500 new theorems in 11 days, a task mathematicians had expected to take years.

It is worth being precise about what formalisation means here, because it is easy to read this as an AI simply proving a famous theorem from scratch. Wiles proved Fermat's Last Theorem in 1994, using deep results in number theory that mathematicians have accepted for three decades. What Claude's agents did was take that existing proof and translate every step of its reasoning into Lean 4, a language and checker that verifies each logical inference is actually valid, with no gaps or hand waving.

That distinction matters. An informal mathematical proof, however well reviewed, still relies on human readers agreeing that each step follows from the last. A machine checked formalisation removes that reliance: Lean checks every single step mechanically, so if the code compiles and the theorem statement matches what was intended, the proof is verified with the same certainty as a piece of software passing its tests. Formalising a proof this large and this dependent on decades of prior number theory has historically been a multi year undertaking done by small teams of specialists.

Anthropic says the work used around 6 billion output tokens from an internal research model, running many Claude Code agents in parallel against the Prove2Me platform, and that the resulting proof has been published on GitHub for anyone to check or build on. The scale, 13 million lines of Lean and nearly 30,000 new theorems, reflects how much supporting mathematical infrastructure had to be built or reused along the way, not just the core argument itself.

The significance for mathematicians is less about Fermat's Last Theorem specifically, which was already settled, and more about what it says for the pace of formal verification generally. A field that has relied on patient, manual translation of proofs into systems like Lean, Coq or Isabelle now has a demonstrated case of that translation happening in 11 days rather than years. If that holds for other major proofs, it changes how quickly the mathematical community can build a fully checked, machine verifiable base of established results.