Claude Formalized Fermat's Last Theorem in 11 Days: What Changed Is Verification, Not New Mathematics

Anthropic reported on September 4, 2026 that Claude produced the first end-to-end, computer-checked proof of Fermat's Last Theorem in 11 days. Claude proved 30,300 machine-verifiable theorems along the way and used 29,500 of them in the final proof, producing 13 million lines of Lean code, over 5x the size of Mathlib, the community's principal standard library. The run consumed roughly six billion output tokens from a general-purpose internal research model described as roughly comparable to Claude Fable 5.1. The single most important cue for reading this announcement is that Anthropic itself states the novelty here is the verification rather than the mathematics. ASAP works only from the figures and wording in Anthropic's official research post to separate what was actually proved from what was not.

Four numbers define the 11 days: 30,300 theorems and six billion tokens

The scale of Claude's Fermat's Last Theorem run is defined by four figures: 11 days, 30,300 theorems, 13 million lines of Lean, and roughly six billion output tokens. Anthropic states that in 11 days, working largely autonomously, Claude produced the first end-to-end, computer-checked proof of Fermat's Last Theorem. Along that path it produced computer-verifiable proofs of 30,300 theorems, of which 29,500 appear in the final proof. The resulting Lean code runs to 13 million lines, over 5x the size of Mathlib. On the compute side, a general-purpose internal research model consumed about six billion output tokens.

The human comparison numbers are supplied alongside. The first proof, from Sir Andrew Wiles in 1995, ran to 129 pages and required months of painstaking work to verify. What this formalization followed was not that original but a simplified version of Wiles's proof from Darmon, Diamond and Taylor. The formalization project itself is a multi-year community effort initiated in 2024 and led by Kevin Buzzard at Imperial College London, and the blueprint the mathematical community has been using to describe the initial phase runs to 86 pages on its own.

The verification conditions are stated explicitly. The finished proof was checked by Lean and uses just Lean's three standard axioms, and a comparator confirmed that the theorem's statement matches Mathlib's own statement of FLT. That last step is not a formality. Proving an adjacent but subtly different proposition perfectly, then claiming the original theorem, is the classic failure mode of autoformalization.

The level of human involvement was recorded too. Mathematical input from humans was limited to occasional high-level instructions from Tianyi Peng, an Anthropic researcher affiliated with Columbia University, in the form of directions such as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon." Those are interventions about what to prove next, not about how to prove it.

The first attempts failed, and that failure survives as 7% of the final proof

The most useful passage in this announcement is not a success figure but a failure record. Anthropic writes that a number of Claude's initial attempts failed: agents had some early success, then quickly lost track of the project's state and stopped collaborating effectively. That discarded work was not thrown away. Their failed efforts contributed roughly 7% of the non-boilerplate lines in the final proof.

The turning point was not a change of model. Anthropic identifies the turning point as the switch to Prove2Me, a collaborative platform designed by Tianyi Peng and collaborators that maintains a directed acyclic graph of theorem statements. Agents consult that graph to decide what proofs to attempt next and which intermediate theorems must land before a larger goal becomes reachable. Anthropic credits the structure with mitigating memory degradation and allowing multiple agents to work in parallel.

Read from the perspective of anyone building multi-agent systems, the conclusion is unusually clean. The bottleneck was the structure of shared state, not the reasoning ability of the model. The same model failed and then succeeded on the same problem, and what changed in between was where and how the agents' work was recorded. Using conversation transcripts or heaps of logs as shared memory makes the cost of reconstructing what everyone else is doing grow with the number of agents, and the agents end up repeating each other's attempts. A dependency graph converts "what should I do next" into a query with a determinate answer: which node is still unproved and has all of its prerequisites satisfied.

The 7% figure deserves its own weight. It says the output produced without structure was not worthless, which supports reading the problem as one of retrieval and coordination rather than production capacity. Once the coordination structure existed, work that already existed became recoverable.

13 million lines is closer to a liability than a trophy

Proof size reads like a boast, but Anthropic's own framing runs the other way. The post states that Mathlib is concise and well-reviewed while this proof is likely much longer than it needs to be. A single theorem generating code five times the size of a standard library the mathematical community built over years is offered as a measure of bloat, not efficiency.

This distinction matters because it goes to where the value of a formal proof actually sits. A formal proof is machine-checked, so its truth does not depend on anyone reading it. Nobody needs to read 13 million lines for the conclusion to stand. But the other purpose of a formal library is reuse. Mathlib is valuable because its theorems become components in the next person's proof, which requires that they be findable, readable, and named. How well 13 million machine-written lines produced in 11 days satisfy that requirement is not something this announcement answers.

Two things are worth keeping apart here. One is the proof as a result, and the other is the library as an asset. The first is finished. Whether these 13 million lines become material for proving the next theorem is a separate consolidation problem, and Anthropic leaves that open. It signals that as autoformalization becomes routine, the real work may shift from generating proofs to compressing and organizing the proofs that get generated.

Why Anthropic did not call this new mathematics

The most carefully written sentence in the announcement is the one that limits the claim. Anthropic states that unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what is novel here is the verification: checking a mathematical proof as one would check a mathematical computation with a calculator. Fermat's Last Theorem was proved in 1995, and what Claude did was render that proof machine-checkable.

Losing that qualifier turns the announcement into a different story entirely. "AI solved a 350-year-old problem" and "AI transcribed a 30-year-old proof into machine-verifiable form in 11 days" are not the same claim. The second is still large, because formalization has been so labor-intensive for humans that most of the modern mathematical literature remains unformalized.

What stands out is that Anthropic imposed the limit itself. In a field where launch posts tend to make results look as large as possible, a publishing party drawing the line at "ours is verification, not discovery" before anyone else does is not the norm. That restraint doubles as evidence, given the subject: a post about verifiability begins by making the scope of its own claim verifiable.

It is also worth seeing why the distinction serves Anthropic. The company frames formalization as a major factor in how humans gain confidence in AI-generated mathematical results, arguing that as AI produces ever more proofs, easy formalization lightens the burden of evaluating them. The result is positioned not as an endpoint for AI mathematics but as groundwork for absorbing the mathematics AI will mass-produce. Kevin Buzzard made the same point, saying such autoformalization techniques will lead to new tools that root out errors in the current mathematical corpus and lighten the load on referees.

A second experiment finished in three days on consumer subscriptions

Anthropic's evidence for generalization is a much smaller second experiment. Agents running on consumer subscriptions, collaborating entirely through Prove2Me, jointly completed a formalization of Vinogradov's Three Primes Theorem in just three days. That theorem is far smaller and easier than Fermat's Last Theorem, but the question this experiment asks is a different one.

The intent shows in what was removed. No internal research model, no six-billion-token budget, no Anthropic-specific infrastructure. What remained was the collaboration structure. It functions as a near-controlled recheck of the diagnosis from the previous section, that the bottleneck was the structure of shared state rather than the model.

From there Anthropic concludes that if automatic formalization of FLT is possible now, a big step has been taken toward automatic formalization of the modern mathematical literature. That inference contains one untested jump. Fermat's Last Theorem was a problem humans had already decomposed, in the form of an 86-page blueprint. Whether the same approach holds for theorems with no map of what to prove in what order is not something these results address, and most of the mathematical literature has no such blueprint.

This method reproduces only where a checker exists

What an AI adoption team should take from this announcement is task design rather than mathematics. Three conditions made the result possible, and all three are identifiable outside mathematics. First, an automatic checker decided correctness: the Lean compiler either accepts a proof or does not, with no human judgment in the loop. Second, the problem was decomposed into small units that verify independently. Third, the dependencies among those units were recorded explicitly.

The set of practical domains meeting all three is narrower than it first appears. Codebases with dense type checking and test coverage, data transformations with explicit schemas and constraints, and hardware design under formal verification are the plausible candidates. Work whose correctness rests on taste or business judgment, such as writing, planning, or customer response, does not inherit this method. Without a checker, running agents for six billion tokens tells you nothing about which outputs were right, and recovering 7% of the failed attempts becomes impossible.

The order of operations to try, then, is not swapping models but securing a checker. Map how far into your own workload a machine can adjudicate true and false, and attach parallel agents only inside that boundary. The next decision is where dependencies get written down. Anthropic's record says that second decision separated failure from success, and the tool for it must be a structure you can query for state, not a conversation log.

One open question is worth leaving in place. This proof is true because Lean checked it, but only a small fraction of the 13 million lines has been read by anyone. Since the conclusion rests on machine checking, that is not a logical problem. It becomes a practical one when a formalized corpus grows at this rate and humans can no longer tell what inside it is reusable. Verification speed opened first; the consolidation and indexing that must follow it have not.

Source: ASAP analysis based on the figures and wording in Anthropic's official research post "Formalizing Fermat's Last Theorem" (September 4, 2026)