On September 4, 2026, Anthropic reported a landmark: Claude produced the first end-to-end, computer-checked formalization of Fermat’s Last Theorem (FLT) in about 11 days, working largely autonomously. The artifact is roughly 13 million lines of Lean, proving about 29,500 intermediate theorems along the way. Lean accepted the proof using only its three standard axioms, and a comparator confirmed the statement matches Mathlib’s FLT.
This is not another “model aced a contest problem” anecdote. Wiles’s 1995 human proof took months of expert checking; the community Lean effort launched in recent years was expected to take years. AI compressed “rewrite a human proof into machine-checkable language” from a multi-year research program into a roughly two-week agent campaign.
What happened
FLT says: for any integer $n>2$, no positive integers $a,b,c$ satisfy $a^n+b^n=c^n$. Andrew Wiles’s proof (with a later gap fix alongside Richard Taylor) runs about 129 pages and relies on modern number theory far beyond Fermat’s era.
Formalization means rewriting the argument so a proof assistant—here, Lean—can verify every step. Human proofs skip “obvious” lemmas; machines do not. Anthropic researcher Tianyi Peng (whose Columbia collaborators also build AI formalization tools) set out to see whether Claude could advance FLT formalization. The run overshot: with the Prove2Me platform and a Claude Code multi-agent harness, a team of agents finished end-to-end in under two weeks, emitting about six billion output tokens from an internal research model Anthropic places roughly on par with Claude Fable 5.1.
Early runs failed—agents lost global project state and stopped coordinating; failed work still contributed about 7% of non-boilerplate lines in the final proof. Switching to Prove2Me stabilized the campaign: a DAG of theorem statements steered what to attempt next, statement/proof file splits sped compilation, and natural-language descriptions aided search and reuse.
Why it matters
Anthropic draws a deliberate contrast: earlier Claude work on the Riemann zeta function produced new mathematical content; here the novelty is verification—checking a long proof the way a calculator checks a long computation. Kevin Buzzard, a central figure in the Imperial College London FLT Lean blueprint, reviewed the result and called it an extraordinary autoformalization achievement whose artefacts are now “robust enough to be built upon,” spanning algebra, harmonic analysis, geometry, and number theory.
For the mathematical community, two pressures ease at once:
- Corpus hygiene and refereeing load: autoformalizing large swaths of modern literature could surface errors and lighten the human cost of reviewing ultra-long proofs.
- A trust channel for AI-produced claims: as models and AI-assisted mathematicians emit more purported proofs, shipping a formalization alongside a human-readable write-up may be how the field keeps up—Anthropic stresses formalization should not replace human exposition, but it can become trust infrastructure.
A small control experiment is telling: three personal Claude Max plans, collaborating only through Prove2Me, formalized Vinogradov’s Three Primes Theorem in three days—suggesting that, with the right scaffold, consumer subscriptions can already carry serious formalization campaigns.
Limits and how to read it
Keep the hype in check:
- This formalizes the Wiles–Taylor route; it does not rediscover Fermat’s mythical elementary proof. The argument follows Darmon–Diamond–Taylor’s exposition of Wiles and adapts pieces from the Imperial College FLT project and flt-regular.
- Scale is not elegance. ~13M lines of Lean—several times Mathlib’s size—partly reflects Mathlib’s concision and an AI artifact not yet shaped for community merge. Buzzard frames it as a buildable workpiece, not a polished textbook.
- Humans stayed in the loop. Peng’s high-level nudges and the platform scaffold separated failed runs from the successful campaign; “autonomous” is relative to multi-agent orchestration, not magic unattended discovery.
- The token bill is heavy. Billions of output tokens mean today’s path is still sensitive to compute, scaffolding, and engineering discipline—not a single chat window.
Take
Reading FLT formalization as “AGI has arrived” misses the real story. The news is that proof assistants + agent graph scheduling + large-scale inference are compressing multi-year blueprint projects into week-scale campaigns—and partially rewriting mathematical trust from “who has months to read 129 pages” into “does the kernel accept this derivation.”
The next race is productization: open collaborative graphs (Prove2Me-class tools), reusable intermediate theorem libraries, and toolchains that compress bloated AI Lean into Mathlib-grade form. Whoever makes “paper ships with a machine-checked proof” the default delivery changes the cost structure of peer review. OpenAI has been pushing Erdős problems and open questions in theoretical CS with frontier models; Anthropic is alternating between new zeta-function results and FLT-scale formalization—math is becoming both a discovery arena and a verification arena at once.
Bottom line
Eleven days, 13 million lines of Lean, end-to-end FLT: Anthropic turned autoformalization from a prospectus into a citable engineering fact. What to watch next is not a louder headline, but whether the community can reproduce the scaffold, compress the artifact, and make “formalization parallel to human exposition” ordinary research hygiene.