Breaking·First-hour kit
Formalizing Fermat's Last Theorem
The repository publishes the development, a Comparator challenge and a formalization.yaml. Read the announcement.
The first hour
What is claimed, and how much can be inspected?
A complete formalisation of Fermat's Last Theorem. Of 1 result announced, 1 is named, 1 written up and 1 published with an artifact anyone can check.
Has anyone independent checked it?
Nobody independent of the authors has checked the result held here.
- Fermat's Last Theorem: A formal artifact or object is published; no independent check of it is recorded.
Does the formal statement say what is claimed?
The authors declare how their formal statement matches the claim; no independent statement anchors it.
- Fermat's Last Theorem: No formal statement is held. F2 declared: The correspondence is declared through a Comparator challenge and written divergences. Flags: declares divergences from its source, reviewed by its authors only, source authors not contacted.
Who did the work?
Graded A1 collaborative for who did the mathematics.
- Claude: A1 collaborative. The mathematics is Wiles and Taylor's. The machine's contribution is the formalisation, which Anthropic describes as largely autonomous and the project's formalization.yaml records as agent work.
Who got there first?
No precursor, concurrent work or dispute is recorded against these results.
What would move the grades
- Evidence rises from V2 with an independent rebuild, by qed.bot or Palomar.
- Fidelity rises from F2 with a Comparator check against a statement from a separate corpus.
AI activity
How grades workA complete Lean 4 proof of Fermat's Last Theorem on the standard axioms, deriving Mathlib's own statement, with the classical inputs proved in the strength the argument needs rather than assumed.
Reasoning and sources
Autonomy
The mathematics is Wiles and Taylor's. The machine's contribution is the formalisation, which Anthropic describes as largely autonomous and the project's formalization.yaml records as agent work.
Details
scale: About 13 million lines of Lean and some 30,000 intermediate theorems, in 11 days
builds on: The Imperial College London FLT project led by Kevin Buzzard, and flt-regular
Sources
Citing this kit
qed.bot, “Formalizing Fermat's Last Theorem: first-hour kit”, https://qed.bot/a/anthropic-2026-09-04, as of 30 Sep 2026.