Mathlib·mathlib:FermatLastTheorem
Fermat's Last Theorem
No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.
Fidelity F2: The correspondence is declared through a Comparator challenge and written divergences.
number theory, Diophantine equations·Source
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
Fidelity
How fidelity is gradedF2 declared. The correspondence is declared through a Comparator challenge and written divergences.
Declared by the projects
1As each project's formalization.yaml states it.
Fermat's Last Theorem in Lean 4
- authors
- Anthropic
- method
- agent
- review
- self-assessed
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 2 main results named, checked with Comparator
- sources
- Modular elliptic curves and Fermat's Last Theorem — adapts, authors not-contacted; Ring-theoretic properties of certain Hecke algebras — adapts, authors not-contacted; Fermat's Last Theorem — adapts, authors not-contacted
- related
- ImperialCollegeLondon/FLT — builds-on; leanprover-community/flt-regular — builds-on
- divergences
- The development follows the strategy of the sources, not their text. Named classical theorems are proved in the strength the argument needs, as set out under "Exact strength of the named steps" in PROOF-PATH.md: irreducibility of E[p] is proved for Frey curves rather than via Mazur's general theorems; Langlands-Tunnell in the octahedral case only; modularity lifting under level conditions at p = 3 and p in {3, 5}; modularity for semistable integral Weierstrass models in the sense of matching a_l; level lowering for the Frey representation as a congruence of traces. The top-level statement is the standard one and is checked identical to a Mathlib-only challenge file.
- checked by
- nobody independent of its authors yet
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themFormal material
Formal statements · 0
No formal statement located.
Cited proofs · 0
No proof artifact cited by the formal record.
Cite this record
qed.bot, “Fermat's Last Theorem”, https://qed.bot/s/mathlib-fermatlasttheorem, as of 30 Sep 2026.