AIREITERIf the headline says “Claude solved Fermat’s Last Theorem,” read one word carefully: formalized. Anthropic has released a public Lean artifact that it says checks the theorem end to end, but the mathematical route is the established Frey–Serre–Ribet–Wiles–Taylor-Wiles argument, not a newly discovered proof.
First, separate the two claims
The narrow answer is yes: Anthropic released a public repository containing a Lean 4 formalization of Fermat’s Last Theorem (FLT), and the repository includes build and verification instructions. The broader claim that Claude independently solved the famous problem is not accurate; Andrew Wiles and Richard Taylor supplied the mathematical breakthrough decades earlier.
FLT states that there are no positive-integer solutions to a^n + b^n = c^n when n > 2. Wiles’s proof was published in 1995; Anthropic’s result turns that established route into a machine-checkable artifact. For historical context, see the Lean Community’s FLT project announcement.
A Lean proof answers a different question from an informal paper. It can show that a precisely encoded proposition follows from checked definitions, dependencies, and axioms in a specified environment. It cannot show that an AI invented the underlying mathematics or that theorem names match their descriptions.
What Anthropic actually released
Anthropic’s September 4, 2026 research post says Claude produced the first complete, end-to-end computer-checked Lean formalization of FLT in 11 days. The post reports approximately 13 million lines of Lean, 30,300 proved theorem statements, and 29,500 used in the final proof. It also reports roughly 6 billion output tokens.
The work used Prove2Me, a platform Anthropic describes as maintaining a directed acyclic graph of theorem statements and coordinating multiple agents. Anthropic says the formalization follows a simplified exposition of the established proof route associated with Frey, Serre, Ribet, Wiles, and Taylor-Wiles.
The public GitHub repository is more useful than the announcement for checking the claim. Its default target is FinalCheck.lean, and its theorem declaration is:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nThe repository identifies itself as a research artifact that is not maintained and does not accept contributions. It pins Lean 4.33.1 and Mathlib v4.33.0, includes PROOF-PATH.md, and provides an offline-browsable HTML rendering of the theorem and definition graph.
The repository’s final check is intended to fail if the proof depends on an added axiom, sorry, native_decide, unsafe, or similar escape hatch. That makes the artifact inspectable, rather than asking readers to trust a screenshot or a prose summary.
A reproducible verification path
A serious check starts with the repository’s pinned environment, not with copying an isolated .lean file into a different project. The Lean Community’s verification guide explains why: Lean releases monthly, Mathlib changes frequently, and backward compatibility is not guaranteed.
Pin the environment before building
The repository says the build is intended for Linux or macOS and requires elan, Git, Python, GNU coreutils, and a network connection so that Lake can fetch and build the pinned dependencies. It reports about 67 GB under .lake, plus roughly 220 GB of generated C files that can later be deleted.
The repository also reports about 5 GB of memory per parallel job, with some modules requiring up to 36 GB. At 96 jobs, its own build took 5 hours 32 minutes and reached a peak of 153 GB of memory. These are the repository’s reported figures, not a result measured in this article; use them as a planning warning rather than a guaranteed runtime.
Choose a verification path
- Inspect only: read
FinalCheck.lean,PROOF-PATH.md, andATTRIBUTION.mdwithout building. - Full Lean build: use the pinned toolchain and run
lake build. - Independent replay: after a successful build and export, run the comparator and nanoda scripts.
From a fresh clone, the repository gives this general sequence:
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.shThe stages serve different purposes:
| Stage | Repository-reported detail | What it is for |
|---|---|---|
lake build | 60,475 modules; 5 h 32 min at 96 jobs in the reported run | Builds the project from source and lets the Lean kernel check the declarations included in the build |
| Comparator | 14 h 46 min in the reported run; peak memory 230 GB | Checks that the exposed theorem and referenced constants match the intended Mathlib challenge statement |
nanoda | About 30 minutes at 16 threads after export | Replays an exported environment through an independently written Rust kernel |
The comparator is not a replacement for reading the theorem statement. It helps address the risk that a project proves a weakened or subtly different proposition. The repository’s PROOF-PATH.md maps named mathematical steps to Lean declarations, while the generated HTML pages let you inspect dependencies without serving a web application.
The repository reports additional costs for the second checks: writing a 37.8 GB export may require about 90 GB of memory, and the nanoda workflow may require about 40 GB during checking.
What the evidence proves, and what it cannot prove
| Evidence layer | Establishes | Does not establish |
|---|---|---|
| Lean kernel build | The submitted proof terms type-check in the pinned Lean environment | That Claude discovered the mathematics, or that the informal explanation matches every theorem name |
FinalCheck.lean and axiom guard | The repository’s final theorem is checked against the reported axiom list and rejects several listed shortcuts | That the theorem is the historical FLT statement unless the statement itself is inspected |
#print axioms output | The dependencies include Lean’s standard propext, Classical.choice, and Quot.sound rather than a hidden user axiom, when the expected check passes | That the entire software supply chain has been independently validated |
| Comparator | The proved result and referenced constants match the Mathlib-only challenge used by the repository | That every natural-language description in the project is clear or pedagogically adequate |
| nanoda replay | An exported environment was accepted by a second Lean-kernel implementation written in Rust | That the export, scripts, or operating system are beyond all possible error |
PROOF-PATH.md and attribution | A route for humans to inspect the mathematical correspondence and prior sources | That machine-generated theorem names accurately describe their statements without human review |
The Lean Community’s “Did you prove it?” checklist gives the key rule: compilation validates the encoded proposition, not whether a theorem name matches its intended informal claim. For this artifact, the comparator and its use of Mathlib reduce that risk, but they do not remove the need to read the theorem declaration and proof path.
What the artifact does—and does not—show
The system produced a formally checked Lean artifact at unusual scale. It does not demonstrate a new route to FLT, a new elementary proof, or independent mathematical discovery by Claude.
Anthropic says the proof follows a simplified version of the Wiles route. The repository also credits existing work: its ATTRIBUTION.md identifies 106 files containing material from the Imperial College London FLT project or flt-regular, alongside Mathlib. That provenance is part of accurately describing what the released artifact is built on.
The project reports 30,300 theorem statements proved during the run and about 29,500 used in the final proof, while the repository describes 29,511 theorem pages. Those are formal declarations and dependencies, not 29,511 newly discovered mathematical results. A formal proof expands implicit steps, types, coercions, definitions, and library dependencies that a human proof can leave to expert understanding.
The repository says its sources were written to be checked rather than read: names are machine-generated, labels such as P2M are pipeline labels, and the statement, not the name, is authoritative. That is why the proof path and comparator matter as much as the headline theorem.
Earlier Lean work should not be collapsed into the 2026 claim. A 2023 paper on Fermat’s Last Theorem for regular primes reported a complete, sorry-free formalization of Case I of Kummer’s theorem for regular primes, while noting that Case II and Kummer’s lemma remained substantial work. A 2025 revision described the regular-prime formalization as a complete proof of that narrower case.
| Work | Scope | Practical role |
|---|---|---|
flt-regular research | Regular-prime results and supporting algebraic-number-theory infrastructure | Earlier formal building block and source material |
| Imperial FLT project | A long-term, reusable formalization of modern number theory around FLT | Library and collaboration infrastructure |
| Anthropic repository | A claimed end-to-end FLT theorem in Lean 4, with build and replay checks | A large research artifact optimized for a checked result rather than long-term maintenance |
The Imperial/Lean FLT project describes formalizing modern number theory as a broader infrastructure effort, not merely translating one theorem. Anthropic’s release is best understood as complementary evidence about what coordinated AI agents can do inside an existing formal ecosystem, not as proof that the earlier project’s goals no longer matter.
Who should trust what
| If you want to know… | The responsible answer is… | Next action |
|---|---|---|
| Whether Anthropic released a real artifact | Yes; there is an official announcement and a public, pinned repository | Read the research post and repository together |
| Whether the encoded theorem is FLT | The repository provides a specific theorem declaration, comparator, and proof path | Inspect FinalCheck.lean, the comparator, and PROOF-PATH.md |
| Whether the code builds cleanly | The repository documents a from-scratch build and reports its own result | Rebuild with Lean 4.33.1 and Mathlib v4.33.0 if you have the required hardware |
| Whether Claude invented a new proof | No evidence supports that description; the route is established Wiles/Taylor-Wiles mathematics | Describe it as AI-assisted formalization or proof engineering |
| Whether the artifact is easy to maintain | No; the repository explicitly calls itself unmaintained, and its code is machine-generated | Treat it as a research artifact, not a drop-in Mathlib library |
| Whether this proves general mathematical autonomy | No; it shows performance on a highly specified formalization target with substantial scaffolding | Separate formal verification capability from open-ended theorem discovery |
If you only need the news, the official release and repository establish that the project exists. If you need an audit, reproduce the pinned build and inspect the statement. If you are evaluating AI research, include the orchestration, existing libraries, prior formalization, and compute as part of the system.
FAQ
Did Claude discover a new proof of Fermat’s Last Theorem?
No. Anthropic’s artifact formalizes an established proof route associated with Frey, Serre, Ribet, Wiles, and Taylor-Wiles. The achievement is the scale and speed of producing a machine-checkable Lean artifact, not a new mathematical solution.
Does a successful Lean build prove the informal theorem?
It proves that the encoded proposition follows from the checked dependencies in that Lean environment. You must still verify that the proposition and its definitions correspond to the informal theorem you intend to claim.
Does the repository use sorry or extra axioms?
The repository says its final check rejects sorry, added axioms, native_decide, unsafe, and several related shortcuts. Its expected axiom list is Lean’s three standard axioms: propext, Classical.choice, and Quot.sound; reproduce the check rather than relying only on the announcement.
Can I reproduce the result on a normal laptop?
You may be able to inspect and partially build the repository, but the full verification is not a normal lightweight workload. The repository reports 153 GB peak memory for its build, up to 230 GB for the comparator, and large disk requirements, so hardware is a central constraint.
To check the claim accurately, start with the pinned GitHub artifact, read the theorem declaration before the headline, and report the result as a large AI-assisted formalization of known mathematics.