Anthropic put its Fermat proof's correctness check inside the default build target
The build fails unless the theorem rests on exactly Lean's three standard axioms, and an independent kernel written in Rust re-checked more than a million declarations. The eleven-day timeline rests on Anthropic's own account.
The Board Room · Leadership desk
What happened
- Anthropic published what it calls the first complete computer-checked proof of Fermat's Last Theorem, written in Lean by Claude working largely autonomously over eleven days.
- The repository's default build target prints the theorem's axiom dependencies and fails unless they are exactly propext, Classical.choice and Quot.sound, with no sorry, added axiom or native_decide.
- A from-scratch build on Lean 4.33.1 compiled all 60,475 modules of the repository with Mathlib built from source, and every declaration was checked by the Lean kernel.
- An independent Lean kernel written in Rust, nanoda 0.4.13, accepted an export of the same environment and reported 1,052,234 declarations checked with no errors.
- Kevin Buzzard called the work an extraordinary autoformalization achievement that proves the theorem with no assumptions beyond the axioms of mathematics, attributing the eleven-day figure to Anthropic researchers.
Why it matters
- What's now possible capability Correctness here is something an outside party re-runs rather than reads, because the no-hidden-assumptions claim is a condition the toolchain enforces every time the repository is built.
- What it limits constraint The audit is open to anyone and cheap for nobody: re-running it needs Linux or macOS, elan and a network connection, and a Mathlib compiled from source because no prebuilt one matches the toolchain.
- Who's exposed exposure Trust concentrates in three places: the Lean kernel and the checking tools, the four local patches to the Rust kernel, and a reader's judgement of whether the intermediate theorems are what their names imply.
- What it sets up precedent Anthropic frames the novelty as the verification rather than new mathematics, which sets the expectation that the next model-produced result of this kind arrives with its checker attached.
Next story · Science · 2d ago
Thomas Bloom stops marking Erdős problems open or solved as AI-written proofs multiplyConfirmed2 publishers
The check that does the most work is the comparison. leanprover's comparator v4.33.0 checked the build against a challenge file that states Fermat's Last Theorem using only Mathlib, and confirmed that the proved statement and every constant in it are identical to the challenge, and that the whole proof, Mathlib included, replays through the Lean kernel; the verdict recorded is "Your solution is okay!" [11]. That prerequisite is the part most work cannot borrow: someone had to write down the goal independently of the proof, in a form the artifact could be diffed against.
Independence also has a cost, which the repository discloses. The Rust kernel was built with four of the authors' own patches, one adding progress output and three speeding up its definitional-equality search, without which a few declarations occupy unmodified nanoda for many hours each; the repository states that none of them adds, removes or weakens a typing rule [13]. That disclosure does not undercut the purpose of running a second kernel. Lean 4.33.1, the toolchain used, itself carries the 2026 kernel soundness fixes [21], and a checker sharing no code with Lean's is how a kernel bug stops being invisible.
Volume explains why the audit had to be mechanical. Anthropic says Claude wrote 13 million lines of Lean and proved 29,500 intermediate theorems [4], which over eleven days is roughly 1.2 million lines a day [22]. Wiles's proof, published in May 1995, ran to 129 pages and needed months of painstaking work to verify [5]; the Lean artifact is about 100,000 lines for every one of those pages [23]. The repository does not pretend a reader closes that gap: its 390 MB html folder gives a page for each of 29,511 theorems and 1,450 definition modules, with English summaries generated automatically and the Lean statement authoritative [3].
The axiom guard shows only that a theorem carrying a particular name depends on three axioms; it says nothing on its own about whether those 29,511 intermediate results mean what they are called. The repository says the same: the checks establish that the statement follows from the three axioms given trust in the kernel and the checking tools, no tool can check that each intermediate theorem means what its name suggests, and that judgement is left to the reader, with PROOF-PATH.md naming the Lean theorem behind each step [15]. The narrowness is what makes the top claim carry weight. The statement uses Lean's built-in natural numbers, its one Mathlib ingredient is exponentiation on the naturals, which Mathlib defines as Lean's own, and nothing else in Mathlib has to be trusted because the kernel checks everything beneath [16].
The board-deck version is that a model proved Fermat's Last Theorem in eleven days. What an outside party can re-run is the proof; the eleven days and the working largely autonomously are Anthropic's account of its own process [1], and the two sit on different footing in the same release. The repository is a research artifact, not maintained and not accepting contributions [17], so it is a completed audit rather than a standing pipeline. For a buyer this quarter, the discrimination worth carrying into vendor conversations is between claims a build can fail on and claims that appear only in a document, and this release contains one of each.
What to watch
- Whether the community formalization project Kevin Buzzard started in 2024 adopts this artifact as a base or keeps to its own route.
- Whether a group with no Anthropic connection publishes a from-scratch reproduction of the build and both kernel checks.
- Whether the pinned Mathlib commit and the Lean 4.33.1 toolchain keep replaying as Mathlib moves on, given the repository is not maintained.
Clarity's read
What the record supports and how the coverage leans. The claims behind it follow.
Reality
- Evidence76
- Adoption22
- Hype gap+14
- Incentives72
- Confidence70
Perspective Coverage
3 publishers- Builder
- Builder 47%
- Operator
- Operator 17%
- Investor
- Investor 36%
Claim ledger
Ranked by verification strength, evidence, and original report placement.
- [1]
Anthropic says it is sharing the first complete computer-checked proof of Fermat's Last Theorem, and that Claude worked largely autonomously over 11 days to write the proof in the Lean programming language.
- [2]
The anthropics/fermats-last-theorem repository contains a complete, machine-checked proof of Fermat's Last Theorem in Lean 4 built on Mathlib (Lean 4.33.1; Mathlib v4.33.0, pinned by commit in lakefile.lean), following the argument of Frey, Serre, Ribet, Wiles and Taylor-Wiles.
- [3]
The html/ folder is about 390 MB and presents the repository as static offline web pages, with a page for each of 29,511 theorems and each of 1,450 definition modules; the English summaries and suggested references are generated automatically and the Lean statement is authoritative.
- [4]
Anthropic says that along the way Claude wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
- [5]
Andrew Wiles published the first correct proof of Fermat's Last Theorem in May 1995; it ran to 129 pages and required months of painstaking work to verify.
- [6]
Kevin Buzzard, shown the proof, called it an "extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days", said it proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics, and said AI autoformalization artefacts are now robust enough to be built upon.
- [7]
Kevin Buzzard at Imperial College London kicked off a multi-year community effort in 2024 to complete the formalization of Fermat's Last Theorem using the Lean proof assistant.
- [8]
The default build target FinalCheck.lean runs #print axioms fermat_last_theorem inside #guard_msgs expecting the list [propext, Classical.choice, Quot.sound], so the build fails unless the proof rests on exactly Lean's three standard axioms (no sorry, no added axiom, no native_decide).
- [9]
FinalCheck.lean also derives Mathlib's own statement, FermatLastTheorem, from the repository's fermat_last_theorem.
- [10]
A from-scratch lake build on Lean 4.33.1 with Mathlib compiled from source built all 60,475 modules of the repository, and every declaration was checked by the Lean kernel.
- [11]
leanprover/comparator v4.33.0 checked the build against verification/comparator/Challenge.lean, which states the theorem using only Mathlib, and confirmed that the proved statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the whole proof, Mathlib included, replays through the Lean kernel; verdict: "Your solution is okay!"
- [12]
nanoda 0.4.13, an independent Lean kernel written in Rust, accepted an export of the same environment written with lean4export and reported "Checked 1052234 declarations with no errors".
- [13]
The authors built nanoda with four of their own patches: one adds progress output and three speed up its definitional-equality search, without which a few declarations of the proof occupy unmodified nanoda for many hours each; the repository states that none of the patches adds, removes or weakens a typing rule.
- [14]
No module in the package contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def or #eval; Challenge.lean uses sorry by design and is not part of the package.
- [15]
The repository states that the checks establish the statement follows from the three axioms given trust in the Lean kernel (or nanoda) and the checking tools, and that what no tool can check is whether each intermediate theorem means what its name suggests, which is for the reader to judge; PROOF-PATH.md names the Lean theorem behind each step.
- [16]
The theorem statement is written with Lean's built-in natural numbers, +, less-or-equal, less-than and not-equal; its one Mathlib ingredient is exponentiation on the naturals, which Mathlib defines as Lean's built-in exponentiation, and nothing else in Mathlib has to be trusted because the kernel checks everything beneath the statement.
- [17]
The repository is labelled a research artifact, not maintained and not accepting contributions.
- [18]
Reproducing the build requires Linux or macOS (some paths are too long for Windows), elan, which installs Lean 4.33.1 from lean-toolchain, and a network connection, because Lake fetches Mathlib from GitHub and compiles it from source since no prebuilt Mathlib matches this toolchain.
- [19]
Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, set out to test whether Claude could make progress on formalizing Fermat's Last Theorem.
- [20]
Anthropic says that unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what is novel in this work is the verification.
- [21]
Lean 4.33.1, the toolchain used for the from-scratch build, includes the 2026 kernel soundness fixes.
- [22]
13 million lines of Lean over 11 days is about 1.18 million lines a day.
- [23]
The 13 million lines of Lean amount to roughly 100,000 lines for each of the 129 pages of Wiles's 1995 proof.
Sources
3 independent publishers whose own reporting we read for this story.
- anthropic.comAnthropic says Claude worked “largely autonomously” over 11 days to formalize the proof of Fermat's Last Theorem in the Lean programming language
1 article · September 4, 2026
- github.comGitHub - anthropics/fermats-last-theorem · GitHub
1 article · September 4, 2026
- newscientist.comFermat's last theorem formalised by AI agents in just 11 days | New Scientist
1 article · September 6, 2026
Topics and entities
Topics
- Fermat's Last Theorem
- Formal Verification
- AI for Mathematics
- Autoformalization