A proof a computer can check
Anthropic said on 4 September that an internal research model has produced the first end-to-end, computer-checked proof of Fermat’s Last Theorem. The formalisation runs to roughly 13 million lines of Lean, the proof assistant mathematicians use to force every step of an argument into a form a machine can verify. Anthropic said the work took 11 days.
Fermat’s Last Theorem states that no three positive integers satisfy a^n + b^n = c^n for any integer n greater than two. Andrew Wiles proved it in 1995 in a paper of about 129 pages, drawing on machinery built across the twentieth century. Checking such a proof by hand takes specialists years. Formalising it — rewriting every inference so a computer can confirm it follows — had been expected to take a comparable span of time.
What the model actually did
The model was, in Anthropic’s description, a general-purpose internal research system roughly comparable to Claude Fable 5.1 rather than a bespoke mathematics engine. Anthropic said several dozen agents worked in parallel, generating about six billion output tokens and proving 30,300 theorems along the way, of which 29,500 appear in the final artefact. Human input was limited to high-level direction.
Anthropic said early attempts failed outright. The run that succeeded depended on an internal platform it calls Prove2Me, which tracks which theorems depend on which and lets many agents work on different branches of the same proof without losing the thread. Roughly seven per cent of the non-boilerplate lines in the final file came out of the failed attempts.
The human groundwork underneath it
The result is not a proof produced from nothing. It follows a simplified version of Wiles’s argument set out by Henri Darmon, Fred Diamond and Richard Taylor, and it sits on top of Mathlib, the community mathematics library that thousands of contributors have built in Lean over more than a decade, and on the formalisation project Kevin Buzzard has run at Imperial College London. Buzzard, who reviewed the output, framed the significance as one of reliability: the artefacts, he said, are now robust enough to be built upon.
Anthropic itself flagged limits. The proof relies only on Lean’s three standard axioms, and a comparator confirmed the statement being proved matches Mathlib’s formulation of the theorem — the check that stops a system from proving something subtly weaker than what it claims. But the company also said the proof is likely far longer than it needs to be, which matters for anyone hoping to reuse the pieces.
Why formalisation is the interesting part
Mathematics has had a verification bottleneck for decades: proofs at the frontier are long enough that only a handful of people can referee them, and errors have survived publication. Formalisation removes the referee problem, at the cost of an enormous amount of tedious work. That trade has kept it rare.
If the tedious half can be automated at this scale, the calculation changes. It also sits alongside a run of similar claims: Anthropic published work in August on Claude generating new results about the Riemann zeta function, and OpenAI has said its Astra model solved several open Erdős problems.
The thing to watch is independent reuse. A 13-million-line Lean file is verifiable by construction — that is the point of Lean — but its value to working mathematicians depends on whether the intermediate theorems can be lifted into Mathlib and used elsewhere. Anthropic has not said when or whether the full artefact will be released for that.
