How an AI Just Converted Fermat's Last Theorem Proof Into Millions of Lines of Code

On September 4, 2026, researchers at Anthropic released the first complete, machine-checked formalization of Fermat’s Last Theorem, converting the landmark 129-page proof published by Sir Andrew Wiles and Richard Taylor in 1995 into 13 million lines of Lean 4 computer code. Running an internal experimental model across dozens of parallel automated agents, the system completed the autoformalization in 11 days. Along the way, the system generated proofs for 30,300 intermediate theorems, utilizing 29,500 of them to close the final verification loop.

The project, spearheaded by Anthropic researcher Tianyi Peng in collaboration with his research group at Columbia University, achieved a milestone that academic mathematicians had anticipated would take the better part of a decade. In doing so, it resolved the 100th and final entry on Dutch logician Freek Wiedijk’s famous list of formalization benchmarks, a 20-year-old challenge cataloging the most celebrated mathematical results remaining to be translated into formal logic.

The verification was authenticated using the native Lean kernel, operating solely on the language’s three foundational axioms: propositional extensionality, quotient soundness, and the axiom of choice. Kevin Buzzard, a professor of pure mathematics at Imperial College London who has led an EPSRC-funded five-year academic initiative to formalize the theorem manually, audited the output with Lean’s comparator utilities. Buzzard confirmed that the machine-generated corpus contains no circular definitions, logical shortcuts, or soundness exploits.

"This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," Buzzard stated following his review. "Along the way we see autoformalization of algebra, harmonic analysis, geometry, and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon."

The event marks an inflection point in computational mathematics. It does not establish new mathematical truths—Wiles’s proof has been accepted by the global mathematical community for more than three decades—but it demonstrates that modern software agents can translate dense, highly abstract human reasoning into mathematically indisputable syntax at industrial scale. The deployment of this AI Fermat's Last Theorem pipeline exposes both the immense capacity of automated proof assistants and the operational shockwaves now facing academia, peer review, and software verification.

Deconstructing the 13-Million-Line Artifact

Fermat’s Last Theorem posits that no three positive integers $a$, $b$, and $c$ satisfy the equation $a^n + b^n = c^n$ for any integer value of $n$ greater than 2. Pierre de Fermat jotted down the proposition in 1637 in the margins of his copy of Diophantus’s Arithmetica, claiming he possessed an argument too extensive for the parchment. For 358 years, the conjecture resisted resolution until Wiles, building on fundamental contributions by Ken Ribet, Gerhard Frey, Jean-Pierre Serre, and Barry Mazur, established the modularity theorem for semistable elliptic curves.

Wiles’s strategy established that if a non-trivial solution to Fermat's equation existed, it could be used to construct a hypothetical elliptic curve—the Frey curve—whose Galois representations possessed mathematical properties incompatible with the modular forms dictated by the Langlands program. The mathematical mechanics required establishing an isomorphism between a universal deformation ring $R$ and a Hecke ring $T$, commonly referred to as the $R = T$ theorem, using the Taylor-Wiles patching method.

While Wiles’s published papers span 129 pages, human mathematical writing relies heavily on what mathematicians term "abuse of notation," background conventions, and omissions of deductions considered trivial to an expert reader. Human referees spend months manually interpolating these conceptual leaps. Proof assistants like Lean, developed initially by Leonardo de Moura at Microsoft Research, accept no omissions. Lean’s kernel requires every type, morphism, functor, group action, and algebraic structure to be explicitly declared and derived from fundamental axioms.

                     ┌──────────────────────────────┐
                     │  Wiles-Taylor-Wiles (1995)   │
                     │  Darmon-Diamond-Taylor Text  │
                     └──────────────┬───────────────┘
                                    │
                         Informal Mathematical
                             Paper (129 pp)
                                    │
                                    ▼
                     ┌──────────────────────────────┐
                     │       Prove2Me Engine        │
                     │   (DAG Dependency Planner)   │
                     └──────────────┬───────────────┘
                                    │
                   Top-down decomposition of conjectures
                                    │
         ┌──────────────────────────┼──────────────────────────┐
         ▼                          ▼                          ▼
┌─────────────────┐        ┌─────────────────┐        ┌─────────────────┐
│  Claude Agent 1 │        │  Claude Agent 2 │        │ Claude Agent N  │
│ (Galois Reps)   │        │ (Hecke Rings)   │        │ (Deformations)  │
└────────┬────────┘        └────────┬────────┘        └────────┬────────┘
         │                          │                          │
         └──────────────────────────┼──────────────────────────┘
                                    │
                     13 Million Lines of Lean 4 Code
                     30,300 Intermediate Theorems
                                    │
                                    ▼
                     ┌──────────────────────────────┐
                     │      Lean 4 Micro-Kernel     │
                     │   (Deterministic Checking)   │
                     └──────────────┬───────────────┘
                                    │
                        0 Assumptions / Axioms:
                        • Propositional Extensionality
                        • Quotient Soundness
                        • Axiom of Choice
                                    │
                                    ▼
                     ┌──────────────────────────────┐
                     │  Fully Certified FLT Proof   │
                     └──────────────────────────────┘

The scale of the generated artifact reflects this disparity. Anthropic’s run relied on the 1995 exposition of the Wiles-Taylor-Wiles argument authored by Henri Darmon, Fred Diamond, and Richard Taylor. Translating this treatise required building enormous swathes of modern number theory that had never before been coded into formal logic.

The resulting artifact contains 13 million lines of Lean 4 code. By comparison, Mathlib—the centralized, community-maintained repository of formalized mathematics cultivated by hundreds of mathematicians over nearly a decade—contains roughly 2.5 million lines. The machine output dwarfs the entire preexisting library by a factor of five, making it the largest formal proof artifact ever compiled.

Compiling the proof demands substantial computational power. On a dedicated 96-core server, executing Lean’s deterministic type-checker across the full directory tree compiles nearly 20 times slower than the standard Mathlib build. Yet, once compilation terminates without an error flag, the proof is mathematically absolute. The system does not output a probabilistic confidence score; it supplies a machine certificate of correctness guaranteed down to the foundations of constructive logic.

The Architecture Behind the Run: Prove2Me and Multi-Agent Orchestration

Early attempts to autoformalize high-level mathematics using single large language models failed consistently. While models can generate localized Lean lemmas, they suffer from context window degradation, compounding hallucinated variables, and circular dependency loops when tasked with multi-step formalizations spanning thousands of lines.

Anthropic bypassed these limitations by shifting from monolithic prompt-and-response generation to a coordinated, distributed agent topology managed through Prove2Me, an open coordination infrastructure developed by Tianyi Peng and researchers at Columbia University.

Prove2Me maintains a dynamic directed acyclic graph (DAG) representing the complete architecture of the proof. At the apex sits the ultimate theorem statement:

$$\forall a, b, c, n \in \mathbb{Z}^+, \quad n > 2 \implies a^n + b^n \neq c^n$$

From this target, the system executed an automated top-down decomposition. The engine ingested the Darmon-Diamond-Taylor text and divided the logical progression into tens of thousands of unproven intermediate nodes, or "sorries"—Lean syntax for assertions accepted without present proof.

Dozens of autonomous Claude agents, running on an internal research model comparable to the Claude Fable 5.1 generation, were dispatched across the dependency graph. Rather than working sequentially, the agents operated concurrently:

Some specialized in algebraic geometry, constructing schemes and modular curves.
Others handled harmonic analysis, representation theory, and class field theory.
Specialized auditing sub-agents parsed the Lean compiler’s error logs, adjusting proofs when tactics stalled or typestates failed to unify.

                    ┌─────────────────────────┐
                    │ Fermat's Last Theorem   │
                    └────────────┬────────────┘
                                 │
                 ┌───────────────┴───────────────┐
                 ▼                               ▼
       ┌──────────────────┐            ┌──────────────────┐
       │ Modularity of    │            │ Ribet's Theorem  │
       │ Semistable Curves│            │ (Level Lowering) │
       └─────────┬────────┘            └─────────┬────────┘
                 │                               │
         ┌───────┴───────┐                       │
         ▼               ▼                       │
  ┌─────────────┐ ┌─────────────┐                │
  │   R = T     │ │ Deformation │                │
  │ Isomorphism │ │   Rings     │                │
  └──────┬──────┘ └──────┬──────┘                │
         │               │                       │
         └───────┬───────┘                       │
                 ▼                               ▼
       ┌──────────────────┐            ┌──────────────────┐
       │ Hecke Algebras   │            │ Galois Reps &    │
       │ & Commutative    │            │ Selmer Groups    │
       │ Rings            │            │                  │
       └─────────┬────────┘            └─────────┬────────┘
                 │                               │
                 └───────────────┬───────────────┘
                                 ▼
                     ┌───────────────────────┐
                     │ Core Lean Foundations │
                     │ (ZFC/Type Theory)     │
                     └───────────────────────┘

The system proved 30,300 lemmas over the 11-day window. In instances where parallel agents produced redundant pathways to the same lemma, Prove2Me pruned the graph, isolating the most computationally direct sequence. The final build linked 29,500 of these theorems into a continuous chain.

The computation devoured an estimated six billion output tokens. Conservative pricing estimates place the direct compute cost at roughly $300,000. To test whether consumer-tier infrastructure could replicate such workflows on smaller targets, the researchers conducted a parallel run using three commercial subscription plans. Orchestrated across Prove2Me, those agents formalized Vinogradov’s Three Primes Theorem in three days, demonstrating that the coordination architecture, rather than raw single-prompt capacity, was the operative variable.

Who Is Affected: Academic and Industrial Fallout

The completion of the AI Fermat's Last Theorem formalization has sent tremors across mathematics departments, open-source verification communities, peer-review bodies, and mission-critical software sectors. The consequences vary dramatically across these constituencies.

1. Pure Mathematicians and Grant Holders

In 2024, Kevin Buzzard secured a £1 million, five-year research grant from the UK’s Engineering and Physical Sciences Research Council (EPSRC) to systematically formalize Fermat’s Last Theorem. Buzzard’s initiative was intended to serve as a pedagogical bridge, training an entire cohort of graduate students and postdocs to formalize contemporary number theory.

When Anthropic compressed this multi-year timeline into 11 days, it altered the rationale of academic formalization grants. Buzzard responded constructively, affirming the technical validity of the run while clarifying the distinction in methods.

The academic effort is working on a 21st-century reinterpretation of the theorem, integrating later advancements by Chandrashekhar Khare, Jean-Pierre Wintenberger, and Mark Kisin to produce modular, elegant abstractions for human learning. Anthropic's agents, by contrast, pursued brute-force syntactic satisfaction of the 1995 Darmon-Diamond-Taylor formulation.

Nevertheless, the funding calculus has changed. Grant agencies face pressure to explain why seven-figure public investments should underwrite multi-year manual formalizations when cloud-hosted models can output complete formal proofs over a single fortnight for a fraction of the cost.

2. The Lean and Mathlib Maintainers

The stewards of Mathlib operate one of the strictest gatekeeping environments in software engineering. Every line in Mathlib is written to maximize reusability, readability, performance, and conceptual clarity.

Anthropic’s 13-million-line codebase cannot be integrated into Mathlib in its current state. The repository’s maintainers currently maintain explicit policies excluding raw, uncurated AI-generated proofs.

The dilemma is structural:

Merging 13 million lines of machine-generated code would multiply Mathlib’s footprint sixfold overnight.
The code is structurally rigid and idiosyncratic, written to close a specific verification loop rather than serve as pedagogical infrastructure for future mathematicians.
Reviewing 29,500 machine-generated intermediate theorems to conform them to human stylistic idioms would consume more community labor than writing the proofs by hand.

"The fact that a machine has been able to take the work of human mathematicians and turn it into a 13-million-line, fully reliable proof really blew my mind," remarked Rutgers University number theorist Alex Kontorovich. Yet Kontorovich and his peers acknowledge the ingestion challenge: an unreadable proof, even if machine-valid, is an alien library that few human maintainers know how to refactor.

3. Scientific Journal Referees and Publishers

The mathematical publishing ecosystem is straining under an unprecedented volume of submissions. As research fields become increasingly specialized, the pool of qualified referees shrinks. Complex proofs frequently sit in peer review limbo for two to four years.

In extreme cases, errors pass undetected for decades. A famous historical example occurred in Wiles's initial 1993 Cambridge lecture announcement; during the refereeing process for the Annals of Mathematics, Nick Katz and other reviewers identified a critical gap in the Euler system argument that required Wiles and Taylor an additional 14 months to repair.

The autoformalization of Fermat’s Last Theorem demonstrates that an AI engine can audit sprawling, cross-disciplinary arguments against core axioms. Scholarly publishers are evaluating systems like Prove2Me as automated pre-checks. A journal could soon mandate that submitted papers pass an automated formalization pipeline before human reviewers assess their novelty, fundamentally altering the peer-review timeline.

4. Safety-Critical Software and Hardware Engineers

The implications extend beyond academic mathematics into enterprise verification. Formal methods have historically been limited to elite defense, aerospace, and semiconductor projects, such as verifying the seL4 microkernel, certifying flight-control logic for commercial airliners, or verifying cryptographic protocols. The impediment has always been human labor: writing formal specifications and interactive proofs in Coq, Isabelle, or Lean requires rare dual expertise in domain engineering and type theory.

By demonstrating that autonomous agent swarms can produce millions of lines of syntactically tight, fully checked code, the Anthropic run signals a drastic reduction in verification overhead. Hardware vendors designing next-generation silicon can deploy autoformalization pipelines to verify complex floating-point units or cryptographic instruction sets against formal specifications in hours rather than quarters.

What Changes: The Epistemology and Economics of Mathematical Proof

The success of the AI Fermat's Last Theorem conversion challenges deep-seated conventions regarding how mathematics is verified, valued, and capitalized.

Dimension	Traditional Mathematical Practice	The Autoformalization Paradigm
Verification Method	Social consensus, peer review, seminar vetting	Deterministic computational kernel verification
Proof Artifact	50–150 pages of natural language and LaTeX	Millions of lines of functional, machine-checked code
Production Timeline	Years to decades of specialized human labor	Days to weeks of distributed machine inference
Economic Bottleneck	The intellectual discovery of proofs	The compute cost of exhaustive checking
Reusability	Readily accessible to humans; hard for computers	Absolute for computers; nearly unreadable for humans

From Social Consensus to Syntactic Verification

For centuries, mathematical truth has been a sociological phenomenon. A mathematician writes a paper; an informal network of peers reads it, discusses it at conferences, probes for hidden fallacies, and gradually incorporates the conclusions into their own work. If an error remains hidden, as did the flaw in Alfred Kempe’s 1879 proof of the Four Color Theorem for eleven years, the community operates on false assumptions.

Autoformalization eliminates sociological ambiguity. Once Lean’s micro-kernel verifies that the proof’s typing terms reduce to inductive axioms, the question of correctness is closed. The proof no longer depends on the reputation of the author, the prestige of the institution, or the patience of an overworked reviewer. Mathematical certainty shifts from an interpersonal agreement into a deterministic calculation.

The Economic Inversion: Discovery vs. Verification

This milestone reveals a dramatic economic realignment. In natural-language AI generation, generating answers is inexpensive, but verifying whether those answers are true is expensive and labor-intensive. In formal mathematics, the inverse holds true.

OpenAI and other research labs have demonstrated that AI systems can solve novel competitive programming problems and discover theoretical shortcuts for isolated challenges at low marginal inference costs. However, rigorous end-to-end verification remains compute-heavy. Anthropic spent hundreds of thousands of dollars in compute, burning six billion tokens, not to discover new mathematics, but entirely to certify existing knowledge down to its axiomatic bedrock.

Cost Distribution: Traditional vs. AI Proof Production
──────────────────────────────────────────────────────────────────
Traditional Human Math:
  [=========================================] Discovery & Invention
  [======] Social Checking & Peer Review

Machine Autoformalization:
  [==] Structural Mapping (Human Source Material)
  [=============================================================] Syntactic Verification & Token Compute
──────────────────────────────────────────────────────────────────

Discovery is becoming cheap; definitive verification remains the dominant cost center. This dynamic reframes data center expansion and enterprise AI budgets. Enterprises deploying AI cannot safely ship unverified output to production environments. In mathematics, Lean provides a "free oracle"—a compiler that checks correctness at zero licensing cost. In real-world enterprise operations, such verification engines do not exist natively; building them requires immense computational and structural investment.

Short-Term Consequences: Shocks, Infrastructure Friction, and "Write-Only" Code

Over the next twelve to twenty-four months, the mathematical and computer science landscapes must absorb several operational bottlenecks highlighted by this experiment.

The Proliferation of "Write-Only" Formal Code

The 13 million lines of Lean generated by Claude suffer from the classic computer science pathology of "write-only code": it can be parsed and executed by a machine, but human engineers cannot realistically read, comprehend, or maintain it.

When Sir Andrew Wiles published his proof, he offered profound conceptual clarity. He illuminated deep geometric bridges between elliptic curves and modular forms, giving the community intellectual tools that fueled generations of subsequent breakthroughs.

Claude’s Lean output offers no such pedagogical illumination. It is a labyrinth of tens of thousands of auto-generated tactic proofs, filled with brute-force simplifications and repetitive algebraic expansions. If a mathematician asks why a particular lemma holds, the file returns a series of tactical instructions that satisfy the compiler without conveying conceptual intuition.

This creates a sharp divide:

Human Mathematics: Prioritizes understanding, structural elegance, and compression of concepts.
Machine Formalization: Prioritizes logical completeness, explicit step enumeration, and syntactic satisfaction.

Unless researchers develop automated "distillation" pipelines that can back-translate 13-million-line formal artifacts into concise, human-legible narratives, machine formalizations risk becoming functional dead-ends—artifacts that prove everything but teach nothing.

Compute Disparities and the Widening Academic Divide

Anthropic’s rapid formalization exposed a staggering capability gap between well-capitalized commercial AI laboratories and academic departments.

A university-led mathematical initiative cannot routinely allocate $300,000 in raw GPU compute for an 11-day exploratory run. If the primary tools for mathematical formalization become tightly coupled to frontier commercial models requiring billions of inference tokens, the frontier of formal verification will drift from public university departments into private technology conglomerates.

Academic institutions risk being relegated to supplying the informal papers and training datasets that commercial labs subsequently formalize, ingest, and monetize.

Infrastructure Strain on the Lean Ecosystem

The Lean language and its underlying toolchain were never designed to compile codebases of this magnitude. The sudden introduction of multi-million-line autoformalized artifacts introduces substantial software engineering challenges:

Memory consumption during dependency resolution spikes into hundreds of gigabytes.
Continuous integration (CI) pipelines that test package interoperability risk ground halts when forced to evaluate tens of thousands of auto-generated proofs.
The open-source tooling must now undergo immediate infrastructural optimization to separate lightweight human repositories from monolithic machine artifacts.

Long-Term Consequences: The Industrialization of Reason

Projecting forward over the next five to ten years, the autoformalization of Fermat’s Last Theorem points toward an industrial transformation of intellectual discovery.

                     ┌──────────────────────────────┐
                     │ Human Insight / Intuition    │
                     │ High-level Conjectures       │
                     └──────────────┬───────────────┘
                                    │
                                    ▼
                     ┌──────────────────────────────┐
                     │ Heuristic Discovery AI       │
                     │ Generates Candidate Proofs   │
                     └──────────────┬───────────────┘
                                    │
                                    ▼
                     ┌──────────────────────────────┐
                     │ Autoformalization Engine     │
                     │ (Prove2Me + Lean Kernel)     │
                     └──────────────┬───────────────┘
                                    │
                   ┌────────────────┴────────────────┐
                   │                                 │
                   ▼                                 ▼
         [ Compilation Fails ]              [ Verification Passes ]
                   │                                 │
                   ▼                                 ▼
         Feedback loop repairs               Certified Truth Added
         tactics & premises                  to Living Library

Auditing the Mathematical Literature

Thousands of papers across arithmetic geometry, algebraic topology, and combinatorics contain minor oversights, misapplied lemmas, or imprecise boundary conditions. In most cases, these gaps can be repaired; in others, they invalidate the core claims.

With the feasibility of autoformalization established, automated systems will soon begin ingesting vast repositories of published literature, starting with preprints on the arXiv. Agents will convert natural-language math into Lean statements, flagging logical gaps, circular citations, and unproven claims at scale.

This process will create a dynamic, living library of certified mathematics. The historical corpus of human intellectual thought will transition from inert, printed text into an interactive, fully validated computational database.

The Emergence of Closed-Loop Discovery Systems

The formalization of known theorems is an intermediate stepping stone. The ultimate deployment of this architecture will unify heuristic exploration with deterministic verification into an automated closed loop.

Currently, generative models hallucinate plausible-looking mathematical falsehoods. But when an exploration model is coupled with an autoformalizer and an underlying kernel, hallucinations are arrested at the compilation stage. If an agent proposes a false step, the Lean kernel rejects it. The agent receives an explicit syntactic diagnostic, updates its context, and attempts an alternative route.

This continuous feedback loop allows machine agents to explore complex mathematical search spaces without human intervention, checking their own work every step of the way. Once models can autoformalize modern proofs effortlessly, they can begin autoformalizing their own novel conjectures, providing both the claim and the infallible certificate of proof simultaneously.

Hardware and Cybersecurity Synthesis

The real-world financial stakes of autoformalization sit in the technology sector. Modern computing infrastructure relies on brittle systems: microprocessors with billions of transistors, cryptographic protocols safeguarding global capital flows, and operating system kernels containing tens of millions of lines of C code. These codebases are systematically vulnerable to side-channel exploits, buffer overflows, and architectural errors.

Scaling formal verification from an elite, hand-crafted artisan pursuit into an industrial automated pipeline alters these economics. Within a decade, critical infrastructure—from the smart contracts managing decentralized financial assets to the flight controllers of unmanned aircraft and the hypervisors of cloud providers—will be automatically translated into formal logic and proven secure down to hardware-level mathematical specifications.

The techniques pioneered to verify that $a^n + b^n \neq c^n$ will underpin the systems that protect critical infrastructure against state-sponsored intrusion and runtime failure.

The Unresolved Horizons of Machine Mathematics

The completion of the AI Fermat's Last Theorem formalization leaves several fundamental questions open for the scientific community.

The immediate benchmark to watch is how the Lean community manages the artifact. Over the next six to twelve months, researchers will observe whether Mathlib maintainers can develop automated modularization pipelines that factor out the most crucial lemmas from the 13 million lines of code, or if the proof will sit isolated in its own external repository.

Attention is also turning to other major milestones. With Freek Wiedijk’s 100-theorem formalization list now officially complete, the mathematical and AI research communities need new, more challenging targets.

Focus is shifting toward unsolved problems: the Riemann Hypothesis, the Birch and Swinnerton-Dyer Conjecture, and the existence of smooth solutions to the Navier-Stokes equations. While formalizing a known proof verifies that the logical pipeline functions, deploying an AI system to solve an open Millennium Prize Problem requires conceptual leaps that autoformalization alone does not guarantee.

What Anthropic’s 11-day run proved is that machines are no longer limited to superficial textual mimicry. They are capable of executing the deepest, most complex logical deductions ever devised by human minds, mapping them into pristine formal code, and compiling them into indisputable mathematical reality. The margin that Fermat claimed was too narrow to contain his thoughts has finally been expanded across 13 million lines of code, and it was written by a machine.