`FLT/Proof.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

12 declarations, 1 contain sorry, 0 declared as axioms

The proof of Fermat's Last Theorem

This file contains the "main spine" of the proof of Fermat's Last Theorem.

The strategy of the proof is to prove the theorem via a series of reductions. In other words, we will define mathematical statements B_1=FLT, B_2, B_3, B_4, ..., up to around B_{12}, and then prove that B_2 implies B_1, B_3 implies B_2, B_4 implies B_3 etc etc, and then ultimately that B_{12} is true.

Imports (4)

Imported by 1 file

FLT.lean

def FLT.Bosses.B1 B1 is the statement of FLT line 40 source
Source documentation
B1 is the statement of FLT.

standard axioms: propext what this means
Proof uses: FermatLastTheorem
```
def B1 : Prop := FermatLastTheorem
```
def FLT.Bosses.B2 B2 is the statement that FLT is true for primes p ≥ 5 line 43 source
Source documentation
B2 is the statement that FLT is true for primes p ≥ 5.

standard axioms: propext what this means
Proof uses: Nat, GE.ge, OfNat.ofNat, Nat.Prime, FermatLastTheoremFor
2 instances, coercions and auxiliary constants left out.
```
def B2 : Prop := ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p
```
def FLT.Bosses.B3 B3 is the statement that there is no Frey Package line 50 source
Source documentation
B3 is the statement that there is no Frey Package. A Frey package is 4 integers a,b,c,p satisfying a^p+b^p=c^p and some other conditions (for example p is prime and at least 5, a,b,c are pairwise coprime etc). These conditions guarantee that the associated Frey curve Y^2=X(X-a^p)(X+b^p) is semistable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: IsEmpty, FreyPackage
```
def B3 : Prop := IsEmpty FreyPackage
```
Mentions: FreyPackage
def FLT.Bosses.B4 B4 is the statement that if E is the Frey curve attached to a Frey package (a,b,c,p), then E[p] is a reducible Galois representation line 54 source
Source documentation
B4 is the statement that if E is the Frey curve attached to a Frey package (a,b,c,p), then E[p] is a reducible Galois representation.

depends on sorry what this means
Proof uses: FreyPackage, WeierstrassCurve, Rat, FreyPackage.freyCurve, Nat, FreyPackage.p, Fact, Nat.Prime, GaloisRep, ZMod, WeierstrassCurve.nTorsion, AlgebraicClosure, WeierstrassCurve.map, Algebra.algebraMap, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy, WeierstrassCurve.galoisRep, FreyPackage.hppos and 2 more
26 instances, coercions and auxiliary constants left out.
```
def B4 : Prop :=
…
```
theorem FLT.Bosses.B2_implies_B1 line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FLT.Bosses.B2, FLT.Bosses.B1
Proof uses: FermatLastTheorem.of_p_ge_5
theorem FLT.Bosses.B3_implies_B2 No Frey package implies FLT for primes at least 5 line 80 source
L4DEL explanation
A counterexample to FLT at a prime p at least 5 can be normalised into a Frey package, so if none exist there is no counterexample.
1. The proof is a direct appeal to FreyPackage.fermatLastTheoremFor_p_ge_5, which does the normalisation (see that lemma).
Prerequisites: FLT.Bosses.B2, FLT.Bosses.B3, FreyPackage.fermatLastTheoremFor_p_ge_5
See also: FreyPackage
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FLT.Bosses.B3, FLT.Bosses.B2
Proof uses: FreyPackage.fermatLastTheoremFor_p_ge_5
```
theorem B3_implies_B2 : B3 → B2 :=
…
```
Mentions: FLT.Bosses.B3, FLT.Bosses.B2
theorem FLT.Bosses.B4_implies_B3 Reducible p-torsion rules out a Frey package line 83 source
L4DEL explanation
If the p-torsion of every Frey curve must be reducible, but Mazur's theorem says it is irreducible, then no Frey package can exist.
1. Assume B4 and suppose a Frey package P is given.
2. B4 applied to P says the Galois representation on the p-torsion of P's Frey curve is not irreducible.
3. FreyPackage.mazur says that same representation is irreducible, giving a contradiction, so the type of Frey packages is empty (B3).
Prerequisites: FLT.Bosses.B3, FLT.Bosses.B4, FreyPackage.mazur
See also: FLT.Bosses.B4_proof
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
depends on sorry what this means
Statement uses: FLT.Bosses.B4, FLT.Bosses.B3
Proof uses: id, IsEmpty, FreyPackage, WeierstrassCurve, Rat, FreyPackage.freyCurve, Nat, FreyPackage.p, Fact, Nat.Prime, GaloisRep, ZMod, WeierstrassCurve.nTorsion, AlgebraicClosure, WeierstrassCurve.map, Algebra.algebraMap, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy and 13 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem B4_implies_B3 : B4 → B3 := by
…
```
Mentions: FLT.Bosses.B4, FLT.Bosses.B3
theorem FLT.Bosses.B4_proof The remaining spine gap: the p-torsion is reducible (unproved) sorry line 98 source
L4DEL explanation
This is the deep core of the modularity-lifting argument, stated as B4 (the p-torsion of the Frey curve is a reducible Galois representation), and in this version of the repository its proof is just sorry.
1. There is no proof to describe: the body is sorry, so B4 is an unproved assumption of the whole development.
2. In the file's own outline, B5 and B6 (lifting hardly ramified representations and compatible families) are sketched in a comment only.
Prerequisites: FLT.Bosses.B4
See also: FLT.Bosses.B4_implies_B3
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
depends on sorry what this means
Statement uses: FLT.Bosses.B4
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
```
theorem B4_proof : B4 :=
…
```
Mentions: FLT.Bosses.B4
theorem FLT.Bosses.B3_proof line 101 source
depends on sorry what this means
Statement uses: FLT.Bosses.B3
Proof uses: FLT.Bosses.B4_implies_B3, FLT.Bosses.B4_proof
theorem FLT.Bosses.B2_proof line 103 source
depends on sorry what this means
Statement uses: FLT.Bosses.B2
Proof uses: FLT.Bosses.B3_implies_B2, FLT.Bosses.B3_proof
theorem FLT.Bosses.B1_proof line 105 source
depends on sorry what this means
Statement uses: FLT.Bosses.B1
Proof uses: FLT.Bosses.B2_implies_B1, FLT.Bosses.B2_proof
theorem flt Fermat's Last Theorem, conditional on unfinished work line 111 source
L4DEL explanation
This is Mathlib's FermatLastTheorem, obtained by chaining the reductions B4 to B3 to B2 to B1; it is not yet a complete proof, because it rests on the unproved theorem B4_proof.
1. The proof term is B1_proof, and B1 is defined to be exactly FermatLastTheorem.
2. B1_proof comes from B2_proof by the lemma that FLT follows from the case of primes at least 5.
3. B2_proof comes from B3_proof, which comes from B4_proof by the Mazur step.
4. B4_proof is currently sorry, so the theorem depends on sorryAx. The file FermatsLastTheorem.lean records that the axioms of the final statement include sorryAx and the project axiom knownin1980s.
Prerequisites: FLT.Bosses.B1, FLT.Bosses.B3_implies_B2, FLT.Bosses.B4_implies_B3, FLT.Bosses.B4_proof
See also: PNat.pow_add_pow_ne_pow_of_FermatLastTheorem
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
depends on sorry what this means
Statement uses: FermatLastTheorem
Proof uses: FLT.Bosses.B1_proof

sorryAx: the axiom behind Lean's sorry; a theorem whose axioms include it has an unfinished proof somewhere below it
```
theorem flt : FermatLastTheorem :=
…
```