A 13-Million-Line Check of Fermat’s Last Theorem Tests AI at Proof Scale

An old theorem becomes a new test for AI

Fermat’s Last Theorem has not changed. What has changed is the form in which its proof can now be inspected.

On September 4, 2026, Anthropic announced that Claude agents had produced what the company describes as the first complete, computer-checked formalization of the theorem in Lean 4. Anthropic says the work emerged from a largely autonomous run lasting about 11 days. The resulting repository is public, so the central artifact is not merely a claim that an AI system solved a difficult task: it is code that other people can examine and attempt to check with the specified proof software.

That distinction matters. This is not a new proof of a previously open problem, nor a discovery that changes what mathematicians know about Fermat’s Last Theorem. The theorem was proved in the 1990s through the work of Andrew Wiles and Richard Taylor, building on a chain of ideas associated with Gerhard Frey, Jean-Pierre Serre and Ken Ribet. Anthropic’s repository says its formal argument follows that established route, in the classical exposition by Henri Darmon, Fred Diamond and Richard Taylor. The mathematical destination and the broad route were already known. The achievement is to express the journey in enough precise detail for a small trusted checker to verify it.

The formal statement covers natural-number exponents n of at least 3 and positive natural numbers a, b and c: a raised to n plus b raised to n does not equal c raised to n. To a reader, that statement is compact. Its accepted proof, however, depends on sophisticated modern number theory far removed from the elementary appearance of the equation. Moving that proof into a formal system means defining the objects, exposing assumptions and supplying the intermediate reasoning that a conventional paper may leave to expert readers.

This is why the scale of the release is as important as the famous theorem attached to it. Anthropic reports roughly 13 million lines of Lean code, around six billion output tokens and 30,300 proved intermediate results, of which about 29,500 are used in the final proof. The repository provides related but differently defined inventory figures: 29,511 theorem pages, 1,450 definition modules and 60,475 built modules. Those counts should not be collapsed into one measure. They describe different layers of a very large generated proof project.

The numbers also explain why this is a more informative test of AI-assisted reasoning than a polished answer in a chat window. A long mathematical response can contain a subtle gap that is difficult to spot. Lean does not accept a step because it sounds plausible or resembles the literature. Each term must type-check against explicit definitions and prior results. At this scale, producing prose that looks mathematical would be easy; producing an artifact that survives formal checking is a categorically stronger requirement.

What “computer-checked” does—and does not—mean

Lean is both a programming language and an interactive theorem prover. In a Lean development, mathematical claims are represented as types, while proofs are represented as terms that inhabit those types. Elaborators, tactics and automation may help construct those terms, but acceptance ultimately rests on the proof checker and the assumptions available to it.

The released project pins Lean 4.33.1 and Mathlib v4.33.0 rather than leaving the software environment vague. Its default check requires the final theorem to depend on exactly three foundational items: propext, Classical.choice and Quot.sound. Naming those dependencies is valuable because formal verification is never simply “the computer says yes.” A meaningful check identifies the statement, the software version, the imported library and the trusted foundations under which the proof is accepted.

The proper conclusion is therefore precise: within that specified Lean environment and those foundations, the checker accepts a term of the stated theorem. This dramatically narrows the space for hidden logical gaps in the encoded argument. It does not independently prove that the compiler, hardware, operating system or every component of the software supply chain is flawless. Nor does it establish that the formal statement captures every informal nuance a reader might associate with a theorem. Those are ordinary boundaries of machine verification, not defects peculiar to this project.

The result is strongest when viewed as a reproducible technical object rather than as an appeal to authority. Readers can inspect the declared theorem, trace its dependencies and compare the implementation with the mathematical route it is meant to represent. Specialists can ask whether definitions match their intended meanings; engineers can test whether the pinned project builds as documented. Formal checking makes those questions sharper, but it does not make human scrutiny obsolete.

That layered review is especially important for generated mathematics. A model can choose an awkward representation, duplicate work, prove a needlessly weak helper theorem or encode the right-sounding target in an unintended way. A kernel check addresses logical validity under the encoded definitions. Mathematical review addresses whether the encoding and architecture faithfully serve the intended mathematics. Software review addresses whether the artifact can be reconstructed and maintained. None of these substitutes for the others.

Why the scale changes the conversation

The most consequential aspect of the project may not be Fermat’s Last Theorem itself. It is evidence that an AI workflow can sustain a very large formalization across thousands of connected results, at least when working from a known proof route and an existing formal ecosystem.

Formalization has traditionally demanded substantial expert labor. Published mathematics is written for trained humans who can bridge routine gaps, infer conventions and recognize when an author invokes a standard result. A proof assistant requires those bridges to be made explicit in a language it can check. The work includes locating suitable library lemmas, reconciling definitions, managing coercions, constructing missing infrastructure and repeatedly reorganizing an argument when a local choice becomes an obstacle much later.

An agent that can carry out more of that engineering could make formal verification practical for projects that currently sit beyond the available human time budget. The immediate benefit would not be a machine replacing the creative mathematician. It would be a machine absorbing portions of the exacting conversion work between human mathematical knowledge and a checkable artifact.

That could improve research in several concrete ways. Authors might be able to test complicated chains of dependencies before publication. Collaborations could maintain machine-readable foundations that reveal exactly which lemmas a result uses. Educators could provide students with environments that distinguish a valid proof from an argument that merely gestures in the right direction. Library maintainers could gain large new bodies of formal material, provided the contributions are reviewed, organized and made maintainable rather than deposited as opaque generated code.

The qualifier is essential. Thirteen million lines are impressive as evidence of successful construction, but volume is not the same as quality. A proof can check while remaining difficult for people to navigate. Generated projects can impose costs on reviewers through repetitive structure, unstable abstractions or poor documentation. If nobody can sensibly modify an artifact after a library update, its long-term value will be lower than its successful first build suggests.

For that reason, the next useful measurements should go beyond line counts and token totals. How much of the development can independent teams rebuild? How much expert intervention was required during and after the nominally autonomous run? Which portions reuse Mathlib directly, and which create new infrastructure? Can mathematicians locate the conceptual milestones they recognize from the published proof? How expensive is it to adapt the code when Lean or Mathlib changes? How many of the new components are reusable in unrelated formalizations?

Anthropic’s figure of roughly six billion output tokens conveys the size of the generation process, but it does not by itself reveal financial or energy cost. No complete public cost account accompanies the figures in the factual record for this article. Converting tokens into a confident cost estimate would require information about models, serving infrastructure, retries, caching, hardware utilization and post-processing. The responsible reading is simply that this was a computation-heavy run whose full resource profile remains unspecified.

The description “largely autonomous” needs similar care. It is Anthropic’s characterization, not a synonym for “no humans involved.” People selected the objective, supplied the surrounding systems and libraries, established checks, and prepared the release. The proof route itself represents decades of human mathematics, while Mathlib embodies years of community formalization. The AI contribution can be substantial without erasing that inherited work.

Verification as an engineering discipline

The project illustrates a useful property of formal methods: progress can be tested continuously. Instead of waiting for a reviewer to read millions of generated tokens, the system can reject malformed or unjustified constructions as they are assembled. That creates a feedback signal far less ambiguous than approval based on fluent language.

It also exposes failure cleanly. A missing proof obligation does not become true because the surrounding explanation is persuasive. An incompatible definition cannot be smoothed over by rhetoric. This makes theorem proving an unusually demanding environment for evaluating AI agents: the final product is subject to a deterministic check, even though choosing productive definitions and intermediate lemmas remains an open-ended intellectual task.

That combination is promising beyond pure mathematics. Software verification, protocol design and hardware correctness all contain claims that can, in suitable settings, be reduced to formal obligations. Success on one famous theorem does not demonstrate readiness across those domains. Their specifications, libraries and operational risks differ. But the same pattern—AI proposes detailed formal work, a checker rejects invalid steps, and humans review the specification and architecture—offers a credible route to tools that are more dependable than unconstrained text generation.

The chief safeguard is to keep the boundary between proof and specification visible. A machine can rigorously prove the wrong theorem if the target is encoded incorrectly. It can verify properties of a simplified model that omits the behavior people actually care about. In applied work, deciding what should be proved may be harder than proving it. Better automation increases the need for careful specifications, independent review and transparent dependency tracking; it does not reduce it.

The Fermat repository is therefore useful not only as a finished monument but as material for investigation. Researchers can examine where the agents needed extensive scaffolding, which formal patterns recurred, and how the development divided a vast goal into tractable intermediate results. Proof-assistant developers can study whether current interfaces and libraries encourage understandable output. Mathematicians can evaluate how closely the formal structure reflects the conceptual proof they know.

A public artifact also permits criticism to become constructive. If a definition is awkward, a dependency excessive or a module difficult to reuse, reviewers can point to the exact code. If the project can be rebuilt under its pinned versions, that result can be reported; if it cannot, the failure can be localized. This is a healthier basis for assessing an AI milestone than a private demonstration whose crucial evidence cannot be inspected.

A milestone with deliberately limited claims

The positive news here is not that AI has superseded Wiles, rediscovered his ideas or independently conquered an open frontier. It is that a machine-generated workflow appears to have converted an exceptionally large body of established mathematics into a form that a proof assistant accepts, and that the artifact has been released for scrutiny.

Keeping those claims narrow makes the achievement more credible, not less. The project depends on human-discovered mathematics, an existing proof exposition, Lean, Mathlib and decisions made by the people operating the system. Its headline figures describe output scale, not elegance or economy. Its token count does not reveal total cost. Its checked status applies to a specified formal statement and environment, not to every layer of computing beneath it. Anthropic’s priority and autonomy claims still require the attribution the company itself warrants.

Within those limits, the work marks meaningful progress. The labor of formalization has been a bottleneck between the mathematical literature and machine-verifiable knowledge. If agents can reliably reduce that bottleneck, more results could receive checks that are currently reserved for a small fraction of mathematics. Researchers could spend more time on definitions, strategy and interpretation while automated systems handle larger portions of proof construction and library plumbing.

The next phase should be empirical. Independent users need to build the repository, inspect key definitions and map the generated development against the established proof. Maintainers need to assess readability, modularity and resilience to software changes. Other teams need to test comparable workflows on different bodies of mathematics, including projects where the required library support is less mature. Repeatability across subjects will tell us far more than a single spectacular target.

There is also a broader lesson for AI evaluation. Tasks with externally checkable outputs allow progress to be measured without trusting a model’s confidence or a vendor’s presentation. Formal theorem proving is not perfectly self-validating—the statement and foundations still demand judgment—but it supplies a hard gate that ordinary generated prose lacks. The artifact either checks under the declared environment or it does not.

Fermat’s Last Theorem became famous because a simple question concealed extraordinary mathematical depth. Its new role is equally instructive: it is a demanding test of whether AI can turn inherited knowledge into exact, inspectable structure at enormous scale. The theorem was already settled. What this project may advance is the machinery for checking how mathematical knowledge fits together.

That is a practical achievement rather than a magical one. It offers no reason for naive optimism about automated discovery, and it leaves important questions about cost, maintainability, human involvement and reproducibility. Yet it gives the research community something unusually valuable: not just an announcement, but a large formal object that can be challenged by both machines and people. The quality of that scrutiny—and the project’s ability to survive it—will determine the lasting importance of the result.