AI for Science

Claude Formalizes Fermat's Last Theorem; the Novelty Is Verification

By Kaleido Field Staff · September 5, 2026

Citation-ready: Anthropic published a complete Lean formalization of Fermat's Last Theorem on September 4, 2026, and said Claude produced it largely autonomously over 11 days.

What happened and why it matters

The achievement is a complete formalization and machine-checking result, not a newly discovered theorem proof; confidence depends on the exact statement, axioms, code, checker, dependencies, and independent replay.

Anthropic's published formalization account and proof artifact

Primary reference: Anthropic: Formalizing Fermat's Last Theorem. Kaleido Field checked the event date and the article's attributed facts against this source.

Formalization and discovery answer different questions

Andrew Wiles and Richard Taylor established Fermat's Last Theorem decades ago. The new artifact asks whether the theorem and the modern mathematical route to it can be expressed end to end in Lean so a checker can verify every formal step.

That distinction matters for citations. The event supports a claim about complete machine-checked formalization, not a claim that Claude independently discovered the theorem or replaced mathematical exposition.

The orchestration layer is part of the result

Anthropic says early attempts lost project state and coordination. The successful run used Prove2Me to maintain a dependency graph, separate theorem statements from proofs, speed compilation, and make intermediate results searchable across agents.

A reproducibility package therefore needs more than the final root theorem: repository commit, Lean and Mathlib versions, dependency graph, build commands, agent and model identifiers, prompts, human interventions, token use, failed branches, and checker output.

Machine checking narrows one risk, not every risk

Lean can determine whether the submitted formal terms satisfy the declared rules and assumptions. Reviewers still need to inspect whether the encoded statement matches the intended theorem, whether dependencies are acceptable, and whether the artifact can be rebuilt from a clean environment.

A separate human-readable explanation remains valuable because a formally accepted term can be difficult to study, teach, or compare with the mathematical ideas in the source proof.

Evidence boundary

Published first-party evidence: the formalization account, linked proof artifact, named Lean checker, three standard axioms, comparator against Mathlib's FLT statement, 13 million lines of Lean, and 30,300 proved intermediate theorems, 29,500 of them used in the final proof. Anthropic-reported process: 11 days, roughly six billion output tokens, dozens of agents, limited high-level human direction, and failed attempts contributing about 7% of non-boilerplate lines. Attributed expert review: Kevin Buzzard's assessment of the artifact. Not established: an independent full-process audit, minimality or readability of the code, reproducible cost and timing on public models, absence of every dependency or tooling defect, or a new human-understandable proof of FLT.