The route of the proof
The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles, largely as in Darmon, Diamond and Taylor,
run as a proof by contradiction. A theorem X.y is stated in Theorems/Thm_X_y.lean and proved in
P2M/Sol/S_X_y.lean, whose import Theorems.Thm_… lines are exactly the theorems it cites. Where this prose and the
Lean differ, the Lean is right. Named classical theorems are proved in the strength the argument needs; the last
section says exactly what that is.
1. Reduction to a prime p ≥ 5. fermat_last_theorem follows in one line from FLT.fermatLastTheorem : FermatLastTheorem
(Mathlib's formulation), whose proof applies Mathlib's FermatLastTheorem.of_odd_primes (using exponent 4)
and fermatLastTheoremThree and hands a prime p ≥ 5 to FreyPackage.fermatLastTheoremFor_of_five_le, proved from
exactly FreyPackage.of_counterexample and FreyPackage.no_frey_package.
2. Frey package. A Frey package (Definitions/Def_FLTPrelim_FreyPackage.lean, adapted from the Imperial College
London FLT project) is a solution a^p + b^p = c^p in nonzero integers, p ≥ 5 prime, normalised to gcd(a,b) = 1,
a ≡ 3 (mod 4), 2 | b, with the Frey curve E_P : y² + xy = x³ + ((b^p − 1 − a^p)/4)x² − (a^p b^p/16)x, an integral
model of y² = x(x − a^p)(x + b^p). FreyPackage.of_counterexample builds one from any counterexample in nonzero integers with prime exponent
p ≥ 5 (citing only Mathlib); FreyPackage.no_frey_package (P : FreyPackage) : False is assembled from exactly the four theorems of steps
3 to 6: irreducible and modular gives, after level lowering, a nonzero weight-2 cusp form on Γ₀(2), and there is
none.
3. Irreducibility. FreyPackage.Mazur_Frey proves GaloisRepIsIrreducible ℚ P.freyCurve P.p
(Definitions/Def_FLTPrelim_GaloisRep.lean: E_P[p] is nontrivial with no Galois-stable F_p-submodule besides 0 and
itself). The case a ≡ 3 (mod 8) has its own argument at the prime 2 (FreyPackage.Mazur_Frey_of_a_mod_eight).
Otherwise reducibility would give a Galois-stable line with trivial action on the quotient
(FreyPackage.frey_reducible_hasCofixedLine, Serre's observation, using that E_P has no rational point of order p),
excluded in three ranges:
- p ≥ 17: FreyPackage.frey_no_cofixed_large, Mazur's Eisenstein-ideal argument carried out for this situation
(X₀(N), its Jacobian and Néron model, the cuspidal subgroup, the Eisenstein quotient; ModularCurve and
AlgebraicGeometry namespaces; the global input is WeierstrassCurve.mazurStepThree_not_inZeroComponentAt). This is
by far the largest part of the step.
- p = 11 (FreyPackage.frey_no_cofixed_eleven) and p ∈ {5, 7, 13} (FreyPackage.frey_no_cofixed_small) hold
vacuously because those exponents are settled outright: fermatLastTheoremFive by a self-contained descent in
Z[(1+√5)/2]; fermatLastTheoremSeven, …Eleven, …Thirteen by Kummer's theorem for regular primes flt_regular
(a port of the flt-regular project: cases I and II, Kummer's lemma via Hilbert's theorems 90-94) plus proofs
that the rings of integers of the 7th, 11th and 13th cyclotomic fields are principal
(IsCyclotomicExtension.Rat.seven_pid, ….eleven_pid, ….thirteen_pid).
4. Modularity. FreyPackage.frey_isModular follows from WeierstrassCurve.modularity_of_semistableModel: every
integral Weierstrass model with Δ ≠ 0 and no prime dividing both Δ and c₄ (IsSemistableModel) is modular
(IsModular: a_ℓ matches a normalised weight-2 eigenform on some Γ₀(N) at good primes; both in
Definitions/Def_FLTPrelim_Modularity.lean; cusp forms, Γ₀(N) and q-expansions are Mathlib's). The proof is Wiles's:
- one of ρ̄{W,3}, ρ̄{W,5} is irreducible (WeierstrassCurve.modThreeOrFiveIrreducible: if both were reducible W would
have a rational 15-isogeny, and WeierstrassCurve.fifteenIsogenyClassification pins c₄³/Δ of such a curve to one of
four values, none of which a semistable model can have);
- Langlands-Tunnell in the weight-2, level-conditioned form Wiles uses,
WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel: a
weight-one form for the odd octahedral representation lifting ρ̄{W,3}
(LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift, for surjective ρ̄₃ with cyclotomic determinant,
by Tunnell's argument: monomial automorphy over the subfields cut out by subgroups of GL₂(F₃), cyclic base change,
a converse theorem with Rankin-Selberg integrals), then multiplication by the Eisenstein series E₁(1, χ₋₃) and a
Deligne-Serre lifting lemma to reach a congruent weight-2 eigenform;
- two modularity lifting theorems, R = T by Taylor-Wiles patching in Diamond's formulation
(GaloisRep.DeformationRingData, CuspForm.HeckeGaloisRepDatum, Algebra.PatchingDatum,
GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum):
WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd
(p = 3; a condition on inertia-fixed 3-torsion when 9 divides the residual level) and
WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd (p ∈ {3, 5}; p² not
dividing the residual level);
- the 3-5 switch WeierstrassCurve.threeFiveSwitchCurve (a second semistable model W′ with ρ̄{W′,3} irreducible and
a_ℓ(W′) ≡ a_ℓ(W) (mod 5) at common good primes ℓ ≠ 5, built beneath from a curve with W′[5] ≅ W[5] taken from an
explicit family in the RubinSilverberg namespace) and WeierstrassCurve.isResiduallyModularOfLevel_of_switch.
If ρ̄_{W,3} is irreducible, Langlands-Tunnell and lifting at 3; otherwise the switch gives W′, the first case makes
W′ modular, W is residually modular mod 5, and lifting at 5 finishes.
5. Level lowering. FreyPackage.level_lowering_to_two: E_P modular and ρ̄_{E_P,p} irreducible give a nonzero
f : CuspForm (CongruenceSubgroup.Gamma0 2) 2. First FreyPackage.modularRepOfConductorLevel: the representation arises
from a squarefree level supported on the primes dividing abc, "arises from" (ModularRepOfLevel,
Definitions/Def_FLTPrelim_ModularRep.lean) being a congruence of traces modulo a prime above p, not an isomorphism
of representations (this proof re-derives modularity itself, so the IsModular hypothesis above is formally
unused). Then primes are removed one at a time (FreyPackage.level_lowering_to_two_of_conductorLevel): an odd
q ≠ p, at which E_P[p] is unramified, by FreyPackage.level_lowering_odd_prime_of_conductorLevel, Ribet's theorem
in the form needed (Čerednik-Drinfeld uniformisation, CerednikDrinfeld namespace); p itself by
FreyPackage.level_lowering_at_p_of_conductorLevel, the Mazur-Ribet step, using that E_P[p] is finite at p
(FreyCurve.isPeuRamifieeAt_odd_of_integralForm). Levels 1 and 2 are closed by ModularForm.S2_Gamma0_one_eq_zero
and step 6.
6. S₂(Γ₀(2)) = 0. ModularForm.S2_Gamma0_2_eq_zero: every f : CuspForm (CongruenceSubgroup.Gamma0 2) 2 is 0,
proved from Mathlib alone.
Exact strength of the named steps
- Mazur. Proved: irreducibility of E_P[p] for Frey curves (p ≥ 17 by the Eisenstein quotient; p ≤ 13 by
Kummer or descent, not modular curves). Not proved: Mazur's theorems on rational isogenies or torsion of
general curves.
- Langlands-Tunnell. Proved: the octahedral case with explicit lift, for surjective ρ̄₃ with cyclotomic
determinant, delivered as a weight-one form and then as weight-2 residual modularity with level conditions.
Not proved: automorphy of general odd two-dimensional representations with soluble image.
- Modularity lifting. Proved: the two level-conditioned statements above for semistable W at p = 3 and
p ∈ {3, 5}. Not proved: versions without the level conditions, for non-semistable curves or other p.
- Wiles. Proved: every semistable integral Weierstrass model with Δ ≠ 0 is modular in the a_ℓ-matching
sense. The hypothesis is on a chosen integral equation; nothing is said about non-semistable curves, modular
parametrisations or L-functions.
- Ribet. Proved: level lowering for the Frey representation at squarefree conductor-supported levels, as a
congruence of traces. Not proved: Ribet's theorem for a general modular mod-p representation.
- "Irreducible" is F_p-irreducibility of E[p]; absolute irreducibility, where lifting needs it, is derived in
the tree (
ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd).