Claude's Fermat's Last Theorem Proof: What Lean Checked

On September 4, Anthropic published what it describes as the first complete, computer-checked proof of Fermat's Last Theorem. Dozens of Claude agents worked for eleven days, largely without human direction, and emitted roughly 13 million lines of Lean code. The headline wrote itself, and by the next morning most of the coverage had settled on the same three numbers: eleven days, six billion tokens, 13 million lines.

Those numbers describe the writing. The more interesting part of the release is the checking, and it is the part almost nobody quoted.

What was actually produced

Fermat's Last Theorem states that no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for any n greater than 2. Andrew Wiles published the first correct proof in 1995, running to 129 pages and resting on machinery that took the mathematical community months to verify — and that briefly turned out to contain a fatal gap, which Wiles spent a year repairing with his former student Richard Taylor.

Formalizing that proof means rewriting it so a machine can check every step, including the thousands of steps a human author is allowed to skip. Kevin Buzzard at Imperial College London launched a community project in 2024 to do exactly that, and the blueprint for its initial phase alone runs to 86 pages. Years was the working estimate.

Anthropic researcher Tianyi Peng, whose group at Columbia University builds formalization tooling, set the agents on it to see how far they would get. The run finished in eleven days. Human input was limited to occasional one-line nudges of the "push the Mazur theorem to be done soon" variety.

Measure	Value
Elapsed time	11 days
Output tokens consumed	~6 billion
Lines of Lean written	~13 million
Lean modules in the repository	60,475
Theorems proved	30,300 (29,511 kept in the final proof)
Files containing third-party Lean text	106
Share of final non-boilerplate lines from failed early runs	~7%
Peak memory to re-verify	230 GB

Two ratios fall out of those figures and are worth stating plainly, because neither appears in the release: the proof averages about 440 lines of Lean per theorem, and Anthropic spent roughly 460 output tokens for every line of Lean that survived into the final artifact. That second number is the honest price of machine-written mathematics right now. Most of what the agents wrote was thrown away.

The check is now the cheap half

Here is the finding that reframes the story. Anthropic's repository README documents its own verification runs in unusual detail, and those timings can be laid directly against the eleven-day generation run.

Generation is the stated 11-day run converted to hours. Verification figures are the runs Anthropic reports on its own hardware (96 threads). Sources: Anthropic's research post and the anthropics/fermats-last-theorem README, both September 4, 2026.

Writing the proof took 264 hours of agent wall-clock. Re-verifying it from nothing — compiling Mathlib from source, replaying the whole thing through the Lean kernel with comparator, then replaying it again through an entirely separate kernel — took Anthropic about 22 hours. The check costs roughly a twelfth of the write, in wall-clock terms, and none of it needs a language model.

That inversion is the substance of the announcement. For 350 years, producing a proof of Fermat's Last Theorem was the hard part and checking one was merely tedious; by 1993 the balance had shifted enough that verifying Wiles took a team of specialists two months to find the flaw and another year to see it closed. Formalization flips it back, and further: the proof is now the expensive artifact and the audit is a batch job.

With one caveat that matters more than the hours. Anthropic's build needs about 5 GB of memory per parallel job, a few modules want up to 36 GB each, and the comparator replay peaked at 230 GB. The company advises allowing 300 GB. So the check is cheap in time and expensive in hardware, which means "anyone can verify this" is true of institutions and false of the individual mathematician with a laptop. The bottleneck moved; it did not disappear.

What the proof does and does not establish

The repository is precise about its own limits, and the precision is worth reading before deciding what the result means.

The build fails unless the theorem rests on exactly Lean's three standard axioms. There is no sorry, no injected axiom, no native_decide escape hatch anywhere in the tree. Comparator confirmed that the statement proved is character-identical to Mathlib's own statement of Fermat's Last Theorem, so the proof cannot have quietly proved something weaker under a familiar name. And the whole environment was re-checked by nanoda, an independent Lean kernel written in Rust, which accepted 1,052,234 declarations without error. Two kernels, written by different people, agree.

Then the README states the thing no tool can do:

What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge.

That is the honest boundary. The machine guarantees the logic is sound from the axioms to the final statement. It cannot guarantee that a lemma called frey_curve_is_semistable is about what a mathematician would mean by those words. For the top-level statement that gap is closed, because comparator pinned it to Mathlib's wording. For the 29,510 theorems underneath it, the gap is closed only by a human reading them.

It is also worth being exact about what Claude did not do. This is not new mathematics. The argument is Frey, Serre, Ribet, Wiles and Taylor-Wiles, followed via the expository account by Darmon, Diamond and Taylor. The repository's own attribution file lists 106 Lean files carrying material from Buzzard's project or from flt-regular, plus 23 reproducing Mathlib text. The scaffolding underneath — Mathlib itself — represents the accumulated work of hundreds of mathematicians. Claude's contribution is translation at a scale and speed no human team could match, which is a large claim and a different one.

Why the tooling mattered more than the model

The first attempts failed. Agents made early progress, then lost track of the project state and stopped collaborating usefully; their dead ends still account for about 7% of the non-boilerplate lines in the finished proof.

What rescued the run was Prove2Me, an open collaborative formalization platform built by Peng and colleagues at Columbia. It maintains a directed acyclic graph of theorem statements that agents consult to choose their next target, keeps statements and proofs in separate files so Lean recompiles less, and holds a natural-language description of every statement so agents can find and reuse each other's work instead of re-proving it. Anthropic credits the DAG specifically with mitigating memory degradation and enabling parallelism.

The lesson generalizes past mathematics. The model that produced this was a general-purpose internal research model, not a specialized prover. What changed the outcome was shared external state that let dozens of agents build on each other rather than drift apart — the same problem every multi-agent system has, solved here with a dependency graph and a search index rather than a bigger context window.

Anthropic's smaller follow-on experiment makes the point sharply: three researchers on ordinary consumer Claude Max subscriptions, collaborating only through Prove2Me, formalized Vinogradov's Three Primes Theorem in three days.

The judgment

Buzzard, who reviewed the proof, told Anthropic that "AI autoformalization artefacts are now robust enough to be built upon." That is the load-bearing sentence in the whole release, and it is about durability rather than speed.

Formalization has inverted the economics of mathematical trust: writing a proof of this size is now the expensive step and checking it is a 22-hour batch job — which makes the real constraint on verifying AI-generated mathematics not intelligence but memory. Anthropic spent six billion tokens to write a proof that two independently written proof-checkers can audit on server hardware without a model in the loop, and the audit is the durable part. If that pattern holds across the mathematical literature, referees stop being the bottleneck and machines with 300 GB of RAM become one.

Cover image: generated illustration.