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
Does the formal statement say what was claimed?
F2 declared The correspondence is declared through a Comparator challenge and written divergences.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Declared by the projects
1Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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 discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal material
Formal statements · 0
No formal statement located.
Cited proofs · 0
No proof artifact cited by the formal record.