Anthropic's Claude Produces First Complete Computer-Checked Proof of Fermat's Last Theorem

Anthropic published a research post on September 4, 2026, announcing that Claude had produced the first end-to-end, machine-verified proof of Fermat's Last Theorem — a 350-year-old problem whose human solution alone required 129 pages and nearly a decade of effort. The proof, written in the Lean 4 programming language, was checked by Lean's logical kernel from first principles, using only three standard mathematical axioms. Working largely autonomously over 11 days, a swarm of Claude agents wrote approximately 13 million lines of Lean code and proved around 29,500 intermediate theorems to complete the formalization.

What Claude achieved was not a new mathematical proof. Andrew Wiles established the first correct proof in 1995, after six years of secret work and a near-breakdown when a gap was discovered. What Claude produced was something mathematicians had projected would take years of community effort: a formal translation of that proof into a language a computer can verify step by step, with no logical links skipped or assumed.

Read more: AI verification as the key bottleneck for agentic performance

The Distinction Between Proving and Formalizing

Mathematicians write proofs for other mathematicians. A published proof relies on shared intuition, skips obvious steps, and invokes results from previous work without restating them. A formal proof, by contrast, cannot assume anything: every inference must be spelled out explicitly, referenced to prior definitions, and connected to foundational axioms.

Lean is a proof assistant — a programming language designed for formal mathematics — built on a branch of logic called the Calculus of Inductive Constructions. When Lean accepts a proof, it means the kernel has mechanically verified that every step follows from the stated axioms. The three axioms used throughout Claude's proof — propext, Classical.choice, and Quot.sound — are the standard foundations for classical mathematics in Lean's type theory. The final check file confirms that no sorry statements (placeholders for unproved steps), no added axioms, and no native evaluation shortcuts appear anywhere in the final proof.

The scale of the formalization reflects how much work the abstraction normally hides. Wiles's 129-page prose argument, already one of the most demanding papers in modern mathematics, expands dramatically when every tacit step is made explicit. Claude's resulting codebase spans 60,475 Lean modules and is roughly five times the size of Mathlib, the principal community library of formalized mathematics that Lean users have been building for nearly a decade. The full proof is available in the anthropics/fermats-last-theorem repository.

How Dozens of AI Agents Sustained an 11-Day Mathematical Campaign

The formalization succeeded on its second attempt, using infrastructure that did not exist when the first attempt failed. Early experiments with multiple Claude agents quickly broke down: agents lost track of which theorems had already been proved, couldn't effectively reuse each other's work, and eventually stopped collaborating. That failure contributed roughly seven percent of the non-boilerplate lines in the final proof — preserved in the repository as a record.

The turning point came when Anthropic researcher Tianyi Peng, whose group at Columbia University develops tools for AI formalization, integrated the project with Prove2Me — an open collaborative platform he and his collaborators built specifically for this class of work. Prove2Me addressed the coordination problem through three technical choices.

First, it organized all theorems into a directed acyclic graph — a dependency map in which each node represents a theorem and each edge records what that theorem needs to be proved first. Agents could consult the graph to decide which theorems were ready to attempt, and could resume after long runs without losing their place in the proof campaign. Second, Prove2Me separated theorem statements and their proofs into different files, maintaining the links between them independently. This substantially reduced Lean's compilation time and memory requirements by avoiding full re-verification whenever a proof changed but its statement did not. Third, each theorem was paired with a natural-language description, enabling agents to search the library of already-proved results and avoid redundant effort.

Built on top of this platform using a Claude Code-based multi-agent harness, the campaign ran for just under two weeks. The internal research model used — described by Anthropic as comparable in capability to Claude Fable 5.1 — consumed approximately six billion output tokens over the course of the campaign. Human input consisted of occasional high-level direction from Peng, such as flagging a specific sub-theorem as high priority or indicating that a particular result should be completed sooner.

Two Independent Verification Layers Confirmed the Result

When the agents signaled completion — the FLT root node in the Prove2Me dependency graph showed "Proved" at 10:00:57 PM Eastern Time on August 17 — the verification process still had to run. Anthropic subjected the proof to two independent checks.

The first was Lean's own kernel, running on Lean 4.33.1, which includes soundness fixes released in August 2026. The build ran at 96 parallel jobs, took approximately five and a half hours, and peaked at roughly 153 gigabytes of memory. The build log confirmed that fermat_last_theorem depended on exactly the three standard axioms and nothing else.

The second check used nanoda, an independent Lean kernel implemented in Rust by a separate team. Nanoda verified 1,052,234 declarations with no errors — independently reconstructing the chain of logic from the same axioms.

A third tool, leanprover/comparator, confirmed that the theorem statement proved by Claude matched Mathlib's own statement of Fermat's Last Theorem exactly — ruling out any possibility that Claude had proved a technically different but superficially similar claim.

Kevin Buzzard, the mathematician at Imperial College London who has led the main community effort to formalize FLT since 2024, reviewed the proof and described it as proving that AI autoformalization artifacts are now structurally sound enough to be built upon — not just demonstrated as isolated experiments. He noted that such techniques could both surface errors in existing mathematical literature and reduce the burden on referees who currently spend months verifying new results by hand.

What This Changes for Mathematical Peer Review

Mathematics has been accumulating a verification debt for decades. Human referees are limited: a complex proof can take years to fully check, as it did when Wiles submitted his work in 1993. Thomas Hales's 1998 proof of the Kepler conjecture spent four years in review before a 12-referee panel settled for "99 percent certain" — Hales subsequently led a 20-person formalization project called Flyspeck that took until 2015 to complete. Grigori Perelman's Poincaré conjecture proof required roughly four years and three 300-page expositions before the community accepted it.

AI is now producing mathematical results faster than traditional review can absorb them. OpenAI's Astra model solved ten open research problems in August 2026, publishing Lean proofs for each. A separate OpenAI effort in June 2026 formalized an Erdős counterexample proof in 1.2 million lines of Lean — roughly half the size of Mathlib at that time. The pace of AI-generated mathematical output is accelerating, while the capacity of human expert reviewers is not.

Formal verification offers a structural solution to this mismatch. A Lean proof, once checked by the kernel, is verified in a categorical sense that no human referee can match for speed or coverage. Buzzard has argued — and Anthropic's post reinforces — that producing a Lean formalization alongside a prose paper will likely become standard practice for AI-generated mathematical results. The FLT project demonstrates that the cost and time required to produce such a formalization are now within reach, not just for national laboratories but potentially for small research teams.

Anthropic demonstrated this directly with a smaller experiment. Three researchers using personal Claude Max subscriptions collaborated entirely through Prove2Me to formalize Vinogradov's Three Primes Theorem — a major number-theory result — in three days.

Read more: Anthropic's automated AI researchers closing safety gaps faster than experts

What the 13-Million-Line Proof Leaves Unresolved

The result carries a significant caveat that Lean's kernel itself cannot address. The kernel verifies that a logical chain follows from axioms — not that the theorems being proved are the ones the proof author intended. The code in Claude's repository was written to be machine-checkable, not human-readable: theorem names are machine-generated, labels include hexadecimal pipeline identifiers, and where a name and a statement disagree, the statement is what was proved. Anthropic explicitly notes that what no tool can check is whether each intermediate theorem means what its name suggests.

This is not a flaw in the result — it is an honest description of what formal verification does and does not provide. Lean's job is to confirm logical consistency within a stated axiom system. Whether the mathematical community eventually chooses to interpret Claude's Lean formalization as a definitive checkpoint for Fermat's Last Theorem, or whether an independently human-readable Lean formalization of similar scope is considered necessary, is an open question.

The 13-million-line size is also substantially larger than necessary. Mathlib's community library grew to its current size over nearly a decade of expert refinement and is highly compact. Claude generated code at speed, not elegance. Anthropic acknowledges the proof is likely much longer than it needs to be. Future iterations of AI-assisted formalization will face pressure to close that gap — producing proofs that are both machine-verifiable and comprehensible enough for mathematicians to audit, extend, and teach from.

The milestone worth noting is that the question has shifted. For over two decades since Bergstra first proposed formalizing Wiles's proof, the constraint was human labor: translating a proof of that complexity into machine-checkable form was simply too slow for any single research team to attempt. As of September 2026, that constraint is lifting. The outstanding challenge is no longer whether AI can formalize mathematics at this scale — it clearly can — but whether the resulting artifacts will become trusted infrastructure for the field, or remain impressive demonstrations waiting for a second generation of tools to make them legible.