Fermat’s Last Theorem, checked line by line
A 350-year story meets an 11-day formalization campaign.
Anthropic · Tianyi Peng · Kevin Buzzard · Lean community
Start with the question
The problem
Can three positive whole numbers satisfy aⁿ + bⁿ = cⁿ when n is greater than two? Fermat said no. Wiles, with Taylor’s contribution, established the theorem in the 1990s. The new challenge was to make the proof checkable by a small logical kernel.
01
The theorem was already proved
Kevin Buzzard’s community project pursues a modern route to FLT. Anthropic instead followed the Darmon–Diamond–Taylor exposition of the Wiles–Taylor–Wiles argument. Buzzard welcomed the achievement while explaining why useful, maintainable mathematical libraries remain a separate goal. [3]
02
Coordination unlocked the formalization
Anthropic reports that Claude agents completed the campaign in 11 days using Prove2Me. A shared graph tracked which theorems depended on which others, helping agents reuse work and choose the next missing step. The released artifact contains roughly 13 million lines of Lean. This is an automation milestone built on human proofs, Mathlib, and earlier formalization projects. [1]
03
Follow the proof all the way down
The repository documents a clean build, an axiom audit, a comparison with Mathlib’s statement, and a second-kernel check using a patched version of nanoda. Its proof-path guide connects the mathematical landmarks to the corresponding Lean declarations. These are the authors’ verification reports; we have not rebuilt this large artifact here. [2]
Inspect the evidence
The Lean formalization
Released Lean 4 formalization
The final declaration uses positive natural numbers and exponents at least three. FinalCheck.lean audits its axioms and derives Mathlib’s FLT statement. The excerpt below is the published theorem signature, with its proof body intentionally omitted.
1theorem fermat_last_theorem2 (n : ℕ) (hn : 3 ≤ n)3 (a b c : ℕ)4 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :5 a ^ n + b ^ n ≠ c ^ n6-- Signature excerpt; open the repository for the proof body.Sources & further reading
Reviewed 9 Sept 2026. X permalinks were recovered from indexed posts and linked discussions; direct X pages were not consistently accessible. They document the conversation, not proof correctness.
- 1.
- 2.
- 3.
- 4.Anthropic’s FLT announcement on X ↗
Announcement, 4 September 2026. Direct post access was unavailable during review; the permalink is also recorded by Claude Pulse and Daily Intel.
- 5.Kevin Buzzard’s original community-project announcement ↗
Historical context from October 2023, not a response to the 2026 release.