The clarification belongs in the first paragraph, not the fifteenth. Fermat’s Last Theorem has not been open since 1995, when Andrew Wiles, with the Taylor–Wiles patch to the gap in his earlier manuscript, proved it. What the agents produced is a translation of that existing argument into a formal language a computer can mechanically check. It is not a new proof. It is not a new theorem. It is not a discovery.
Anthropic’s own writeup draws that contrast explicitly, separating this kind of formalization work from novel mathematics. Kevin Buzzard of Imperial College London, who has been leading the human-led formalization of FLT since 2024, put the mathematical content plainly in his own assessment: the formalization faithfully follows the early literature and, in his phrasing, “adds nothing” to the mathematics.
What the agents actually produced
Formalization is a specific and unglamorous activity. A human proof written for other humans leaves enormous amounts implicit — standard constructions, routine lemmas, the reader’s ability to fill a gap because they have seen the pattern before. A proof assistant like Lean refuses all of that. Every step has to reduce to something the kernel can verify against a small axiomatic base. That is why the line count is in the millions: the underlying mathematics is compressed, and formalization decompresses it.
The Claude agents followed the Darmon–Diamond–Taylor 1995 exposition of the Wiles / Taylor–Wiles argument. That choice matters for interpretation. It is the historical route, not the modernized approach that Buzzard’s EPSRC-funded community project has been building toward — a multi-year effort whose blueprint for the initial phase alone runs to roughly 86 pages. So the two projects are not straightforwardly comparable artifacts, even though they nominally target the same statement.
According to Anthropic, the proof compiles in Lean, relies only on Lean’s three standard axioms, and a comparator was used to confirm that the formal statement matches Mathlib’s own statement of Fermat’s Last Theorem. That last check is not a formality. A formalization that proves a subtly different statement is worthless, and “the statement is right” is exactly the kind of thing a kernel cannot tell you on its own. The code has been posted publicly at github.com/anthropics/fermats-last-theorem. Anthropic’s technical note also credits 106 files adapted from the Imperial FLT project and from flt-regular — the machine output is not built on nothing.
Buzzard, per The Next Web’s coverage, did the obvious first thing a formalizer does: he compiled it. He measured approximately 13.4 million lines and reported that compilation took nearly twenty times as long as Mathlib on a 96-core machine. He ran standard checks and blogged, with evident good humor, that “Anthropic has beaten me to it.”
What Buzzard did and did not concede
The distinction Buzzard drew is the one most coverage flattens. He has separately estimated the odds that Wiles’s proof is correct at around 99.9 percent — meaning the mathematical community’s confidence in FLT was not meaningfully in play. A formal check of a theorem nobody doubted moves the needle on certainty by a rounding error.
What he did treat as significant is the process claim. If dozens of agents can autoformalize a proof of this size, largely without step-by-step human direction, over eleven days, then autoformalization of modern research literature becomes newly plausible as an engineering problem rather than an aspiration. That is a statement about tooling, throughput, and the economics of formal verification. It is not a statement about mathematical insight, and Buzzard did not make it one.
There is a corollary he flagged that deserves more attention than it usually gets: the bottleneck moves. If machines can write Lean faster than humans can write it, the constraint becomes reading it. Mathlib, the community library, does not currently accept AI-generated reviews, and per TNW’s account it already carries something on the order of 3,000 open pull requests. A 13-million-line artifact that compiles is one thing. A 13-million-line artifact that a human community has audited, understood, refactored, and absorbed into shared infrastructure is a different thing entirely, and the second is much slower than the first.
Coordination, not just a bigger model
The most instructive detail in Anthropic’s account is that the early attempts failed. Agents lost project state and stopped collaborating with each other. Those failed runs were not entirely wasted — Anthropic reports they still contributed roughly seven percent of the non-boilerplate lines — but they did not produce a proof.
What changed was scaffolding. The successful run used Prove2Me, developed with Tianyi Peng and collaborators at Columbia, together with a Claude Code multi-agent harness. The structure Anthropic describes is a directed acyclic graph of theorem statements, with statement-writing separated from proof-writing, and natural-language descriptions attached so that agents could find and reuse each other’s results instead of re-deriving them. That is a project-management architecture as much as an AI one. Human involvement is described as occasional high-level fragments from Peng — Anthropic cites examples like “Jacobian as a scheme sounds high priority” and “Push Mazur to be done soon” — steering priorities rather than supplying mathematics.
The run consumed roughly six billion output tokens from an internal research model that Anthropic characterizes as roughly comparable to Claude Fable 5.1. Cost estimates circulating in coverage are illustrative arithmetic, not disclosed figures, and should be treated that way.
Anthropic also notes a smaller data point that may generalize better than the headline one: the Vinogradov Three Primes Theorem was formalized in three days by three researchers using personal Claude subscriptions through Prove2Me. The FLT run is the spectacle. The three-day one is closer to what routine practice might look like.
The honest summary is narrow and still consequential. A known theorem now has a machine-checked formal proof, produced mostly by machines, in under two weeks. Verification capacity grew. Mathematics did not.