Late Friday, Anthropic published the first complete, computer-checked proof of Fermat’s Last Theorem: Claude, working largely autonomously over 11 days, wrote it in Lean. To be clear about what this is not — it is not new mathematics, the theorem has been proven since Wiles and Taylor in 1995, and no one is claiming otherwise. It is new verification. A proof that human referees took months to check, and that the formalization community expected to take years of expert effort, is now a file Lean can verify in minutes. Kevin Buzzard, who leads the multi-year community project that was chasing exactly this, put the headline on it himself: Anthropic has beaten me to it.
The last theorem on the list fell in eleven days
What happened. Per Anthropic’s research post, a team of Claude Code agents working on Prove2Me — an open coordination platform built by Anthropic researcher Tianyi Peng with collaborators at Columbia — formalized the Wiles argument (in the Darmon–Diamond–Taylor presentation) end-to-end in Lean. The run took 11 days, wrote 13 million lines of Lean — more than five times the size of Mathlib, the community’s principal proof library — proved 30,300 intermediate theorems (about 29,500 used in the final proof), and consumed roughly six billion output tokens from an internal research model “roughly comparable to Claude Fable 5.1.” Lean checks the result with only its three standard axioms, and the theorem’s statement was cross-verified against Mathlib’s own via the comparator tool. Kevin Buzzard, who led the Imperial College effort whose 86-page blueprint was the community’s roadmap, reviewed the proof and confirmed the consequence the numbers imply: it closes the final open entry of Freek Wiedijk’s list of 100 formalization challenges, a benchmark untouched for two decades. Anthropic published the proof on GitHub. Techstrong and Buzzard’s own timeline independently corroborate the figures (Sept 4).
Why it matters. The operator-sized number is not eleven days, it is the run’s failure mode. Anthropic reports the first attempt failed — not on capability, but on coordination: the agents “quickly lost track of the project’s state and stopped collaborating effectively,” and the effort only succeeded once Prove2Me gave them a shared, dependency-tracked work graph. That is the same lesson the agent-deployment thread keeps surfacing all summer: long-horizon agent fleets at this scale do not fail on the math, they fail on state management, and the fix is scaffolding, not a bigger model. The second consequence is for trust. Formalization converts “the lab says its model proved X” into “Lean checked X,” and Anthropic has now done it twice in a row — this follows last month’s Riemann-zeta formalization. For anyone reading AI math claims, the burden just inverted: the verifying is now the cheap part, which is exactly how a referee ought to want it.
What I’m watching
Whether the price of entry collapses to consumer tier. Anthropic notes a side experiment where three personal Claude Max subscriptions, collaborating entirely through Prove2Me, formalized Vinogradov’s Three Primes Theorem in three days — if that holds, the moat for this kind of work is the coordination layer, not the model, and the six-billion-token bill for FLT (a low-six-figure API tab at list output rates) is a high-water mark, not a steadystate. Also whether formalization-by-default spreads to the other labs’ claims, not just Anthropic’s own.
Source: anthropic.com, xenaproject.wordpress.com, techstrong.ai