FreyPackage.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

9 declarations, 0 contain sorry, 0 declared as axioms

Frey packages

A "Frey package" is a bundle of data consisting of nonzero pairwise coprime integers a, b, and c, and a prime p ≥ 5, such that a is 3 mod 4, b is even, and a^p+b^p=c^p.

The main result of this file is that if Fermat's Last Theorem is false, then there exists a Frey package.

The motivation behind this definition is that then all the results in Section 4.1 of Serre's paper [Serre] apply to the elliptic curve $Y^2=X(X-a^p)(X+b^p)$; this is the Frey curve associated to the Frey package.

Main definition

FreyPackage : A Frey package is a triple (a,b,c) of nonzero, pairwise coprime integers and a prime p ≥ 5 such that a is 3 mod 4, b is even, and a^p+b^p=c^p.
FreyPackage.freyCurve : The Frey curve associated to a Frey package.

Main theorem

FreyPackage.of_not_FermatLastTheorem : A counterexample to FermatLastTheorem gives rise to a Frey Package.

The proof is an elementary arithmetic argument, assuming Fermat's result that FLT is true for n=4 and Euler's result that it's true for n=3.

Imports (11)

Imported by 2 files

structure FreyPackage Frey package line 75 source
Source documentation
A Frey Package is a 4-tuple (a,b,c,p) of integers satisfying $a^p+b^p=c^p$ and some other inequalities and congruences. These facts guarantee that all of the all the results in section 4.1 of Serre's paper [serre] apply to the corresponding Frey curve, the elliptic curve $Y^2=X(X-a^p)(X+b^p).$ In particular the $p$-torsion of this curve is a highly suspicious object. Serre could already prove in 1987 (using Mazur's theorem) that the $p$-torsion had to be an irreducible Galois representation; in 1990 Ribet proved that the $p$-torsion could not be irreducible, assuming modularity of the Frey curve. In 1993 Wiles showed that the Frey curve was modular, completing the proof.
L4DEL explanation
A Frey package bundles a hypothetical counterexample a^p + b^p = c^p, with a prime p at least 5, into normalised data (a coprime to b, a congruent to 3 mod 4, b even) so that the associated elliptic curve is well behaved.
1. The structure carries integers a, b, c, all nonzero, and a natural number p that is prime with 5 at most p.
2. It carries the equation hFLT, coprimality of a and b, the congruence a = 3 mod 4, and evenness of b.
3. Its docstring explains the historical role: Serre (using Mazur) showed the p-torsion of the resulting curve is irreducible, Ribet showed it cannot be (assuming modularity), and Wiles proved modularity.
See also: FreyPackage.freyCurve, FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
standard axioms: Classical.choice, Quot.sound, propext what this means

Frey package: a normalised hypothetical counterexample (a, b, c, p) to Fermat's Last Theorem with p a prime at least 5
```
structure FreyPackage where
…
```
lemma FreyPackage.hppos line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, LT.lt, Nat, OfNat.ofNat, FreyPackage.p
Proof uses: lt_of_lt_of_le, Decidable.byContradiction, Not, FreyPackage.hp5
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FreyPackage.hp0 line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Ne, Nat, FreyPackage.p, OfNat.ofNat
Proof uses: LT.lt.ne', FreyPackage.hppos
3 instances, coercions and auxiliary constants left out.
lemma FreyPackage.hp_odd line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Odd, Nat, FreyPackage.p
Proof uses: Nat.Prime.odd_of_ne_two, FreyPackage.pp, LE.le, OfNat.ofNat, FreyPackage.hp5, Not.intro, Eq, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, LT.lt, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne and 52 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FreyPackage.gcdab_eq_gcdac line 113 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, GCDMonoid.gcd
Proof uses: Dvd.dvd, GCDMonoid.dvd_gcd, GCDMonoid.gcd_dvd_left, Eq.mpr, id, congrArg, Eq.symm, propext, Int.pow_dvd_pow_iff, LT.lt.ne', dvd_add, GCDMonoid.gcd_dvd_right, HSub.hSub, eq_sub_of_add_eq', Neg.neg, dvd_neg, Int.gcd, congr_arg, Nat.dvd_antisymm, Iff.mp and 1 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma FreyPackage.hgcdac line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Int, GCDMonoid.gcd, FreyPackage.a, FreyPackage.c, OfNat.ofNat
Proof uses: Eq.mpr, FreyPackage.b, id, congrArg, Eq.symm, FreyPackage.gcdab_eq_gcdac, FreyPackage.p, FreyPackage.hppos, FreyPackage.hFLT, FreyPackage.hgcdab, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FreyPackage.hgcdbc line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Int, GCDMonoid.gcd, FreyPackage.b, FreyPackage.c, OfNat.ofNat
Proof uses: Eq.mpr, FreyPackage.a, id, congrArg, Eq.symm, FreyPackage.gcdab_eq_gcdac, FreyPackage.p, FreyPackage.hppos, HAdd.hAdd, HPow.hPow, Nat, add_comm, FreyPackage.hFLT, gcd_comm, FreyPackage.hgcdab, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma FreyPackage.of_not_FermatLastTheoremFor_p_ge_5 Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package line 145 source
Source documentation
Given a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5 and prime, there exists a Frey package.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, LE.le, OfNat.ofNat, Not, FermatLastTheoremFor, Nonempty, FreyPackage
Proof uses: Odd, Nat.Prime.odd_of_ne_two, Eq, Exists, And, Ne, HAdd.hAdd, HPow.hPow, Eq.mp, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Int, Iff.mpr, Int.ofNat_ne_zero, Nat.ToInt.of_eq, rfl, NatCast.natCast, Int.gcd and 80 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma of_not_FermatLastTheoremFor_p_ge_5
    {p : ℕ} (pp : p.Prime) (hp5 : 5 ≤ p) (H : ¬ FermatLastTheoremFor p) :
    Nonempty FreyPackage := by
…
```
Mentions: FreyPackage
lemma FreyPackage.fermatLastTheoremFor_p_ge_5 Empty type of Frey packages gives FLT for p at least 5 line 217 source
Source documentation
If there is no Frey package, then Fermat's Last Theorem is true for all primes p≥5.
L4DEL explanation
By contraposition: a counterexample for some prime p at least 5 would produce a Frey package.
1. Assume the type of Frey packages is empty, take a prime p at least 5, and suppose FLT fails for p.
2. The earlier lemma of_not_FermatLastTheoremFor_p_ge_5 builds a Frey package from the counterexample.
3. That contradicts emptiness.
Prerequisites: FreyPackage, FreyPackage.of_not_FermatLastTheoremFor_p_ge_5
Sources and attribution: Pinned Lean source (f6c6a2fe9796)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsEmpty, FreyPackage, Nat, GE.ge, OfNat.ofNat, Nat.Prime, FermatLastTheoremFor
Proof uses: Classical.byContradiction, Not, Nonempty, False, FreyPackage.of_not_FermatLastTheoremFor_p_ge_5, IsEmpty.false
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma fermatLastTheoremFor_p_ge_5 (h : IsEmpty FreyPackage) :
    ∀ p ≥ 5, p.Prime → FermatLastTheoremFor p := by
…
```
Mentions: FreyPackage