ModularityConjecture.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 10 curated AI-written annotations and 7190 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, Formal Conjectures paper, arXiv v1

8 declarations, 1 contain sorry, 0 declared as axioms

Modularity conjecture

The Modularity conjecture (also known as the Shimura-Taniyama-Weil conjecture) states that every rational elliptic curve is modular, meaning that it can be associated with a modular form. We state the a_p version of the conjecture, which relates the coefficients of the modular form to the number of points on the elliptic curve over finite fields.

Since we don't have the conductor of the elliptic curve, our definition of a_p(E) differs from that in the literature at primes of bad reduction. For this reason, we state the conjecture with the assumption that p ∤ N, in order to give an equivalent statement.

References:

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Wikipedia/SatoTateConjecture.lean

def ModularityConjecture.modularFormAn The n-th Fourier coefficient of a modular form (around the cusp at infinity) line 46 source
Source documentation
The n-th Fourier coefficient of a modular form (around the cusp at infinity).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, CuspForm, Subgroup.map, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Matrix.GeneralLinearGroup, Real, Matrix, Matrix.SpecialLinearGroup.mapGL, CongruenceSubgroup.Gamma0, Complex
Proof uses: LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, UpperHalfPlane.qExpansion, UpperHalfPlane
35 instances, coercions and auxiliary constants left out.
```
noncomputable def modularFormAn (n : ℕ) {N : ℕ} {k : ℤ} (f : CuspForm (Gamma0 N) k) : ℂ :=
…
```
def ModularityConjecture.ratRed We need to reduce a rational modulo p, in practice we won't be dividing by zero since the conductor of the elliptic curve saves us line 53 source
Source documentation
We need to reduce a rational modulo p, in practice we won't be dividing by zero since the conductor of the elliptic curve saves us.

standard axioms: Quot.sound, propext what this means
Statement uses: Rat, Nat, ZMod
Proof uses: HMul.hMul, Rat.num, Inv.inv, Rat.den
14 instances, coercions and auxiliary constants left out.
```
def ratRed (q : ℚ) (p : ℕ) : ZMod p :=
…
```
def ModularityConjecture.setOfPointsModN The set of points on an elliptic curve over ZMod n line 57 source
Source documentation
The set of points on an elliptic curve over ZMod n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, Nat, Set, Prod, ZMod
Proof uses: Set.ofPred, ModularityConjecture.setOfPointsModN.match_1, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, HMul.hMul, ModularityConjecture.ratRed, WeierstrassCurve.a₁, WeierstrassCurve.a₃, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.a₆
15 instances, coercions and auxiliary constants left out.
```
def setOfPointsModN (E : WeierstrassCurve ℚ) [E.IsElliptic] (n : ℕ) :=
…
```
instance ModularityConjecture.apFintype The set of point mod n is finite line 64 source
Source documentation
The set of point mod n is finite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, PNat, Fintype, Prod, ZMod, ModularityConjecture.setOfPointsModN
Proof uses: Eq.mpr, Set.ofPred, ModularityConjecture.setOfPointsModN.match_1, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, ModularityConjecture.ratRed, WeierstrassCurve.a₁, WeierstrassCurve.a₃, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.a₆, Membership.mem, Set, Prod.snd, Prod.fst
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
instance apFintype (E : WeierstrassCurve ℚ) [E.IsElliptic] (p : ℕ+) :
    Fintype (setOfPointsModN E p) := by
…
```
Mentions: ModularityConjecture.setOfPointsModN
def ModularityConjecture.WeierstrassCurve.ap Note that normally this is written as p + 1 - #E(𝔽ₚ), but since we don't have a point at infinity on this affine curve we only have p line 71 source
Source documentation
Note that normally this is written as p + 1 - #E(𝔽ₚ), but since we don't have a point at infinity on this affine curve we only have p. The trace is integer-valued and can be negative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, Nat, Int
Proof uses: HSub.hSub, MonoidWithZeroHom, Cardinal, Cardinal.toNat, Cardinal.mk, Prod, ZMod, ModularityConjecture.setOfPointsModN
13 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.ap (E : WeierstrassCurve ℚ) [E.IsElliptic] (p : ℕ) : ℤ :=
…
```
def ModularityConjecture.IsNormalisedEigenform Since we don't have Hecke operators yet, we define this via the q-expansion coefficients line 76 source
Source documentation
Since we don't have Hecke operators yet, we define this via the q-expansion coefficients. See Proposition 5.8.5 of [diamondshurman2005].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, CuspForm, Subgroup.map, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Matrix.GeneralLinearGroup, Real, Matrix, Matrix.SpecialLinearGroup.mapGL, CongruenceSubgroup.Gamma0
Proof uses: And, Eq, Complex, ModularityConjecture.modularFormAn, Nat.Coprime, HMul.hMul, Nat.Prime, LE.le, Ne, ZMod, HPow.hPow, HSub.hSub
55 instances, coercions and auxiliary constants left out.
```
def IsNormalisedEigenform {N : ℕ} {k : ℤ} (f : CuspForm (Gamma0 N) k) : Prop :=
…
```
def ModularityConjecture.modularityConjecture See theorem 8.8.1 of [diamondshurman2005] line 84 source
Source documentation
See theorem 8.8.1 of [diamondshurman2005].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic
Proof uses: Exists, PNat, CuspForm, Subgroup.map, Matrix.SpecialLinearGroup, Fin, OfNat.ofNat, Nat, Int, Matrix.GeneralLinearGroup, Real, Matrix, Matrix.SpecialLinearGroup.mapGL, CongruenceSubgroup.Gamma0, And, ModularityConjecture.IsNormalisedEigenform, Nat.Prime, Ne, ZMod, Eq and 3 more
29 instances, coercions and auxiliary constants left out.
```
def modularityConjecture (E : WeierstrassCurve ℚ) [E.IsElliptic] : Prop :=
…
```
theorem ModularityConjecture.modularity_conjecture The Modularity Theorem (formerly Shimura-Taniyama-Weil conjecture): every elliptic curve over $\mathbb{Q}$ is modular sorry line 93 source
Source documentation
The Modularity Theorem (formerly Shimura-Taniyama-Weil conjecture): every elliptic curve over $\mathbb{Q}$ is modular.

depends on sorry what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, ModularityConjecture.modularityConjecture
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem modularity_conjecture (E : WeierstrassCurve ℚ) [E.IsElliptic] : modularityConjecture E := by
…
```
Mentions: ModularityConjecture.modularityConjecture