Anthropic says Claude formalised Fermat's Last Theorem

Anthropic reported that Claude had produced a complete, machine-checked formalisation of Fermat’s Last Theorem in the proof assistant Lean, a task the company said took roughly 11 days. The resulting proof runs to about 13 million lines of Lean code and around 29,500 intermediate theorems — more than five times the size of Mathlib, the community-maintained library that most Lean formalisation work builds on.

The work used a framework Anthropic calls Prove2Me, in which many model instances work in parallel on a shared, searchable graph of theorem statements, allowing later proofs to reuse results established earlier rather than duplicating work. Formalising a proof of this size is a different exercise from finding the original mathematics — Fermat’s Last Theorem was proved by Andrew Wiles in 1994 — the task here was translating an accepted human proof, and the vast machinery it depends on, into a form a computer can verify step by step against the axioms of mathematics with no gaps or hidden assumptions.

Kevin Buzzard, who leads a formalisation effort at Imperial College London, called it “this extraordinary autoformalization achievement,” noting it “proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics,” and said the techniques demonstrated point toward automatic formalisation of the wider mathematical literature — useful, he suggested, for rooting out errors in existing proofs and easing the burden on human referees.

The result sits alongside other recent claims about AI systems doing large-scale formal mathematics, including OpenAI’s ten Lean-verified results credited to an internal model and its reported resolution of a Navier–Stokes problem. As with those claims, the achievement is bounded: formalising an already-proved theorem, however large the resulting proof object, is a different and more constrained task than discovering new mathematics, and the scale of the output — millions of lines of code — makes independent line-by-line human review impractical, leaving verification to Lean’s own type-checker.