News · 2026-09-04

Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem

Anthropic says Claude worked largely autonomously for 11 days to produce the first complete computer-checked Lean 4 proof of Fermat's Last Theorem. The repository and proof path describe a real machine-checkable artifact, but the result should be understood as formalizing a known mathematical route with substantial prior human infrastructure—not as a model independently discovering Wiles's proof from scratch. That distinction makes the news more useful, not less.

Key facts

• Anthropic says Claude worked largely autonomously for 11 days and generated 29,500 intermediate theorems in the final artifact.
• The repository calls the result a complete machine-checked Lean 4 proof and documents its verification path.
• The project attributes 106 files containing Lean text taken or adapted from Imperial College London's FLT project or flt-regular.
• Primary source: Anthropic's formalization announcement.

Fermat's Last Theorem says that no positive integers satisfy a^n + b^n = c^n for integers n greater than two. Andrew Wiles's proof is one of modern mathematics' landmark achievements, but writing a human proof and writing a proof assistant artifact are different jobs. A paper can safely omit steps experts know how to reconstruct. A proof assistant must be told every definition, transformation, and dependency in a language whose kernel can check each move.

That is why the announcement is a formal-methods story. The Mathlib statement already expresses Fermat's Last Theorem in Lean and points to the Imperial formalization project. Anthropic's proof path says the new work follows the Frey, Serre, Ribet, Wiles, and Taylor-Wiles route by contradiction, using a simplified version described by Darmon, Diamond, and Taylor. The advance is filling in and connecting the enormous number of formally valid steps so the checker can accept the entire result.

An analogy: a conventional proof is an architectural blueprint that a qualified builder can interpret. A Lean proof is the complete set of machine-verifiable assembly instructions, down to every fastener. The second form is laborious, but once it is accepted it can be rerun by anyone with the same checker. Anthropic's repository says the proof is accepted only with Lean's three standard axioms and after passing its comparator and a second-kernel check. That is what Kevin Buzzard means in Anthropic's post when he calls the result a major step and says the proof has “no assumptions other than the axioms of mathematics.”

The human contribution is central, not an inconvenient qualification. Buzzard's Imperial College London project has been active since 2024, with a 2024–2029 blueprint and an explicit goal of a complete proof. In a December 2024 update, he wrote that the team was already two months into teaching FLT to a computer. Anthropic's attribution file is unusually valuable because it makes the dependence inspectable: 106 files contain text taken or adapted from the Imperial project or another existing source.

This does not make Claude a glorified copy machine. Formalization is a difficult combinatorial and engineering task. The model had to work through a codebase, select lemmas, construct formal terms, repair errors, and leave an artifact that Lean can check. Anthropic's reported 29,500 intermediate theorems give a sense of scale. It is a promising demonstration of what language models can do when success has a hard, automatic verifier. The problem is well aligned with a machine because there is no ambiguity about whether the final proof builds.

The strongest counter-argument is that this alignment makes the headline misleading if phrased as “AI solved Fermat.” The theorem was solved by Wiles decades ago; the mathematical route, theorem statement, library, and project vocabulary already existed. Buzzard has also cautioned in Lean-community discussion that filling in small lemmas is not necessarily the bottleneck for formalizing the whole theorem. A model can accelerate a well-specified formal project without resolving the hardest questions of mathematical invention.

Why it matters anyway is that many consequential technical claims are closer to formalization than to original theorem discovery. Cryptographic protocols, compilers, hardware controllers, financial contracts, and safety-critical algorithms often have a specification and a verifier. In those domains, a system that can turn a human goal into checkable proof obligations could make rigorous assurance cheaper and more widespread. Our explainer on proof assistants explains why a small trusted kernel changes the confidence model.

The honest caveat is maintenance. Formal proofs depend on versions of Lean, Mathlib, definitions, automation, and libraries; a proof that checks today can require work to keep checking as its environment evolves. The important next milestones are reproducible independent builds, expert review, reusable lemmas flowing upstream, and evidence that models can contribute in domains where the roadmap is less completely pre-specified. Anthropic's artifact is an impressive answer to a constrained, rigorously checkable problem. It is not a reason to abandon human mathematical judgment.

Primary source, verified: read the paper →

Ground Truth. (2026, September 4). Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem. Ground Truth. https://groundtruth.day/news/claude-produced-a-complete-lean-proof-of-fermats-last-theorem.html

@misc{groundtruth:claude-produced-a-complete-lean-proof-of-fermats-last-theorem,
  title  = {Anthropic says Claude produced a complete Lean proof of Fermat's Last Theorem},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/claude-produced-a-complete-lean-proof-of-fermats-last-theorem.html}
}

Topics: anthropic · claude · formal-verification · mathematics · lean · reasoning · research