Wiles already proved Fermat's Last Theorem. That part of the story is old.
What Anthropic published on September 4 is not a new mathematical breakthrough. It is industrial-scale translation and verification: Claude agents, working largely autonomously for 11 days, produced the first complete computer-checked proof of FLT in Lean. Anthropic's research post says the swarm wrote about 13 million lines of Lean, proved 29,500 intermediate theorems used in the final proof out of 30,300 attempted, and burned roughly 6 billion output tokens from an internal research model roughly comparable to Claude Fable 5.1. Lean checked the result against only Lean's three standard axioms. A comparator confirmed the top statement matches Mathlib's FLT statement.
Claude agents formalized Fermat's Last Theorem in 11 days not by inventing math, but by surviving a multi-day swarm only after a shared dependency graph replaced lost project state. So operators who keep buying bigger models for long-horizon work will miss that generation is now the expensive half, and that the product that lasts is the checker, the pinned statement, and the coordination layer your agents consult when memory dies.
What actually changed
Keep the meme and the mechanism apart.
The meme is "AI cracked Fermat." The mechanism is colder. Anthropic researcher Tianyi Peng, who also works on formalization tools at Columbia, started the test. Human input stayed limited to occasional high-level nudges such as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon." The proof follows a simplified Wiles route via the Darmon, Diamond, and Taylor exposition. It adapts pieces from the Imperial College London FLT project led by Kevin Buzzard and from flt-regular. It is not new mathematics. Buzzard's September 4 Xena post is blunt: the artefact mathematically tells us essentially nothing new. It faithfully follows early literature. What it does tell us is what autoformalization can do at scale.
Scale is not a metaphor. Anthropic reports the codebase is over five times the size of Mathlib at about 13 million lines. Buzzard compiled it and ran the comparator: it checks out, at over 13.4 million lines, and took nearly twenty times as long to compile as Mathlib on a 96-core machine. Stanford Tech Review adds the time split: writing took about 264 hours of wall-clock; re-verification took about 22 hours, roughly one twelfth. The check needs no language model. Peak memory for the comparator hit about 230 GB, and Anthropic advises allowing around 300 GB. Two kernels, Lean and nanoda (Rust), agreed. Attribution is not pure generation either: about 106 Lean files came from the Buzzard project or flt-regular, and 23 reproduce Mathlib text. Roughly 440 Lean lines per theorem and about 460 output tokens per surviving Lean line sit behind the headline.
AI Weekly notes the obvious operational detail people bury: several dozen parallel agents, and 11 days of wall-clock, not one immortal agent with infinite context. Early runs collapsed. Agents drowned in local context, lost track of proved results, and duplicated work. Anthropic's own post is clear that first attempts failed when agents lost project state and stopped collaborating effectively. Failed efforts still left about 7 percent of the non-boilerplate lines in the final proof.
The turnaround was not a bigger context window. It was Prove2Me, an open collaborative platform by Peng and Columbia collaborators: a DAG of theorem statements, separate statement and proof files, and natural-language descriptions for search and reuse. Same agents. Same weights. Different shared memory. That is the product news, not the Fermat branding.
The mechanism
Long-horizon agent fleets die the same way every time. Each worker optimizes for its local transcript. The global task graph lives nowhere durable. Proved results become folklore. Duplicated work looks like progress. Collaboration collapses into parallel hallucination with better syntax.
Prove2Me externalizes the thing chat memory pretends to be. Statements live as nodes. Dependencies are edges. Proofs are separate from claims. Search works across natural-language descriptions, so agents can find and reuse work instead of regenerating it. Anthropic's harness was Claude Code-based multi-agent orchestration plus that platform. The checker (Lean) made green meaningful. The DAG made green composable across days.
Statement pinning is the trust boundary at the top. The comparator to Mathlib's FLT statement is how outsiders know the swarm proved the intended theorem rather than a lookalike. Stanford Tech Review quotes the README's harder confession: no tool can check that each intermediate theorem means what its name suggests. You can typecheck a mountain of lemmas and still need humans for semantic honesty in the middle of the pile.
Economics invert once you stare at the numbers. Generation burned billions of output tokens. The Next Web's illustrative cost, not an invoice, puts 6 billion output tokens at Fable 5.1 list pricing of $50 per million at about $300,000, with the caveat that the run used an internal model. Verification is a batch job: hours, not days, if you have the RAM. Check time is cheap relative to writing. Hardware for the check is not free. Reviewer time after the green check is not free either. Mathlib will not currently accept AI reviews. The Next Web notes roughly 3,000 open PRs and more than 600 active ones. The bottleneck has already started shifting from writing to reading.
Buzzard called the result extraordinary autoformalization: artefacts robust enough to be built upon, a big step toward autoformalizing modern literature, and a lightener of referee load. He also checked for Lean soundness exploits. He still has his own work: Mathlib PRs for modern number theory, and a dynamic human-explorable document of the modern proof route, not the 1995 exposition the swarm followed. His EPSRC grant is £1 million over five years. He wonders aloud whether Anthropic spent more. For operators, that comparison is the tell. Frontier labs are buying coordination plus tokens. Grant-funded formalization is buying careful human structure. Both are racing the same bottleneck: trusted shared state and trusted reading.
What operators get wrong
The first miss is treating this as a model IQ story. Wiles already did the math. Lean already existed. Mathlib already stated FLT. The swarm translated a known route into a machine-checked artefact at industrial scale. If your takeaway is "buy the next larger model," you read the press release and skipped the failure mode.
The second miss is shipping multi-day agents without an external task graph. Anthropic's first attempts failed for the same reason your overnight research fleets fail: lost shared state. Bigger context windows do not replace a DAG when dozens of agents work for days. Chat history is a local cache. It is not a project database. If your long-horizon product still stores "what is done" only inside transcripts, you are re-running the failed Fermat swarm with a different brand name.
The third miss is trusting unlabeled intermediate artifacts because the top statement typechecks. The comparator pins the final claim. Intermediate lemma names still need humans. A green final check is necessary. It is not a license to treat every named subproof as semantically faithful. Operators who ship agent-generated policies, migrations, or analyses with only an end-to-end test are making the same category error: trusting the summit because the trail markers look confident.
The fourth miss is assuming verification is free. It is not free in RAM (hundreds of gigabytes here). It is not free in compile time (nearly 20x Mathlib on Buzzard's machine). It is not free in reviewer time (Mathlib's PR queue is the canary). If your budget line is only generation tokens, you are funding the expensive half and ignoring the half that makes the expensive half usable.
Second-order effects
Scaffolding democratizes faster than raw frontier weights. Anthropic's companion result matters here: three personal Claude Max plans formalized Vinogradov's Three Primes Theorem in three days via Prove2Me. That is not "only labs can do this." That is "coordination platforms turn consumer seats into serious formalization capacity." The moat moves from who can rent the biggest model to who can pin statements, share dependency graphs, and budget the check.
Autoformalization of modern literature becomes a product category, not a research stunt. Buzzard's read is that modern research formalization on the fly is coming. FLT was on Freek Wiedijk's list of 100 formalization challenges. Clearing a famous list item with a non-modern proof route still changes the expected cost of "make this paper machine-checkable." Expect journals, labs, and enterprise risk teams to start asking for pinned statements the way they once asked for unit tests.
Human reading becomes the scarce resource. When agents can emit millions of lines that a kernel can check, the queue of humans who can decide whether intermediate claims mean what they claim becomes the choke. Mathlib's refusal of AI reviews is not Luddism. It is an early admission that review capacity does not scale with generation. Your org will hit the same wall with agent-written runbooks, compliance memos, and architecture diffs.
Hardware for verification shows up as a first-class line item. A 22-hour re-check that needs ~300 GB is not a laptop chore. Teams that treat "we have CI" as equivalent to "we can verify agent mountains" will discover the difference on the first serious run. Generation is a token bill. Verification is a memory and compile bill plus a people bill.
Finally, the failed 7 percent is a product feature, not embarrassment. Failed efforts left residue in the final proof. Multi-day swarms will always leave scar tissue. The operators who win will design for salvage: searchable failed attempts, separated statement interfaces, and reuse paths so the next agent does not rediscover the dead end.
What to do this week
Inventory every long-horizon agent job you already run or plan to run. For each one, write down whether "done," "blocked," and "reusable" live in an external store or only in chat memory. If the answer is chat, you are on the failing Fermat path.
Add statement or spec pinning for any agent-generated artifact that will be reused. Final green checks are not enough. Pin the contract the artifact is supposed to satisfy, the way the Mathlib comparator pinned FLT. Separate the claim from the proof of the claim.
Budget verification hardware and time separately from generation tokens. Put RAM, compile windows, and reviewer hours on the same planning page as the token estimate. If you cannot price the check, you cannot price the work.
Design human review gates for intermediate claims, not only for final green checks. Decide which lemma-like objects in your domain need a person to confirm that the name matches the meaning. Do that before the swarm multiplies the pile.
Prefer coordination scaffolds before model upgrades. A DAG, a search index over natural-language descriptions, and separated interfaces for statements versus proofs will buy more long-horizon reliability than another context-window bump. Prove2Me was the variable that turned failure into success with the same agents and weights. Copy the lesson, not the theorem.
The durable stack is not the cleverest generator. It is the checker that refuses to lie, the pinned statement that refuses to drift, and the coordination layer your agents still consult after every local memory dies. Fermat was the demo. Shared state is the product.
