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

48 declarations, 23 contain sorry, 0 declared as axioms

Some conjectures about ranks of elliptic curves over ℚ

References:

[PPVW2016] Jennifer Park, Bjorn Poonen, John Voight, and Melanie Matchett Wood. A heuristic for boundedness of ranks of elliptic curves, https://ems.press/journals/jems/articles/16228
[BS2013] Manjul Bhargava and Arul Shankar. The average size of the 5-Selmer group of elliptic curves is 6, and the average rank is less than 1, https://arxiv.org/pdf/1312.7859
[Goldfeld1979] Dorian Goldfeld. Conjectures on elliptic curves over quadratic fields, Number Theory Carbondale 1979, Lecture Notes in Math. 751, 108-118, https://doi.org/10.1007/BFb0062705
[Smith2025] Alexander Smith. The Birch and Swinnerton-Dyer conjecture implies Goldfeld's conjecture, https://arxiv.org/abs/2503.17619
Wikipedia
ICARM
[Stoll] Michael Stoll. EllipticCurves, a Lean 4 formalization of the Mordell–Weil theorem and explicit 2-descent, https://github.com/MichaelStollBayreuth/EllipticCurves

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

structure EllipticCurveRank.RatEllipticCurve A data structure representing isomoprhism classes of elliptic curves over ℚ line 50 source
Source documentation
A data structure representing isomoprhism classes of elliptic curves over ℚ. Every elliptic curve over ℚ is isomorphic to one with Weierstrass equation y² = x³ + Ax + B, and the pair (A,B) is unique if it satisfy the reduced condition below. See Section 5.1 in [PPVW2016].

standard axioms: propext what this means
```
structure RatEllipticCurve : Type where
…
```
theorem EllipticCurveRank.mordell_weil sorry line 67 source
depends on sorry what this means
Statement uses: Field, NumberField, DecidableEq, WeierstrassCurve.Affine, WeierstrassCurve.IsElliptic, Module.Finite, Int, WeierstrassCurve.Affine.Point
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def EllipticCurveRank.RatEllipticCurve.toWeierstrass Convert the structure RatEllipticCurve to a Weierstrass curve line 74 source
Source documentation
Convert the structure RatEllipticCurve to a Weierstrass curve.

standard axioms: Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, EllipticCurveRank.RatEllipticCurve.A, EllipticCurveRank.RatEllipticCurve.B
3 instances, coercions and auxiliary constants left out.
```
def toWeierstrass (E : RatEllipticCurve) : Affine ℚ :=
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
abbrev EllipticCurveRank.RatEllipticCurve.rank The rank of an elliptic curve over ℚ line 78 source
Source documentation
The rank of an elliptic curve over ℚ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Nat
Proof uses: Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.RatEllipticCurve.toWeierstrass
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable abbrev rank (E : RatEllipticCurve) : ℕ := finrank ℤ E.toWeierstrass.Point
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
instance EllipticCurveRank.RatEllipticCurve.(instance at line 81) line 81 source
def EllipticCurveRank.RatEllipticCurve.naiveHeight The naïve height of an elliptic curve over ℚ line 88 source
Source documentation
The naïve height of an elliptic curve over ℚ.

standard axioms: propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Nat
Proof uses: Max.max, HMul.hMul, OfNat.ofNat, HPow.hPow, Int.natAbs, EllipticCurveRank.RatEllipticCurve.A, EllipticCurveRank.RatEllipticCurve.B
8 instances, coercions and auxiliary constants left out.
```
def naiveHeight (E : RatEllipticCurve) : ℕ := max (4 * E.A.natAbs ^ 3) (27 * E.B.natAbs ^ 2)
```
Mentions: EllipticCurveRank.RatEllipticCurve
def EllipticCurveRank.RatEllipticCurve.heightLE The set of elliptic curves over ℚ with naïve height less than or equal to a given height line 91 source
Source documentation
The set of elliptic curves over ℚ with naïve height less than or equal to a given height.

standard axioms: propext what this means
Statement uses: Nat, Set, EllipticCurveRank.RatEllipticCurve
Proof uses: Set.ofPred, LE.le, EllipticCurveRank.RatEllipticCurve.naiveHeight
1 instances, coercions and auxiliary constants left out.
```
def heightLE (H : ℕ) : Set RatEllipticCurve := {E : RatEllipticCurve | E.naiveHeight ≤ H}
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.card_heightLE_div_pow_five_div_six_tensto Formula (5.1.1) of [PPVW2016]: The number of elliptic curves over ℚ with naïve height at most H is asymptotically 2^(4/3)*3^(-3/2)/ζ(10) * H^(5/6) sorry line 99 source
Source documentation
Formula (5.1.1) of [PPVW2016]: The number of elliptic curves over ℚ with naïve height at most H is asymptotically 2^(4/3)*3^(-3/2)/ζ(10) * H^(5/6).

depends on sorry what this means
Statement uses: Filter.Tendsto, Nat, Real, HDiv.hDiv, Set.ncard, EllipticCurveRank.RatEllipticCurve, EllipticCurveRank.RatEllipticCurve.heightLE, HPow.hPow, OfNat.ofNat, Filter.atTop, nhds, HMul.hMul, Neg.neg, Complex.re, riemannZeta, Complex
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem card_heightLE_div_pow_five_div_six_tensto :
    atTop.Tendsto (fun H ↦ (heightLE H).ncard / (H : ℝ) ^ (5 / 6 : ℝ))
      (𝓝 (2 ^ (4 / 3 : ℝ) * 3 ^ (-3 / 2 : ℝ) / (riemannZeta 10).re)) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve.half_rank_zero_and_half_rank_one Conjecture by Goldfeld and Katz–Sarnak: if elliptic curves over ℚ are ordered by their heights, then 50% of the curves have rank 0 and 50% have rank 1 sorry line 108 source
Source documentation
Conjecture by Goldfeld and Katz–Sarnak: if elliptic curves over ℚ are ordered by their heights, then 50% of the curves have rank 0 and 50% have rank 1. See p. 28 of https://people.maths.bris.ac.uk/~matyd/BSD2011/bsd2011-Bhargava.pdf.

depends on sorry what this means
Statement uses: Nat, Or, Eq, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Set.ncard, EllipticCurveRank.RatEllipticCurve, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.heightLE, EllipticCurveRank.RatEllipticCurve.rank, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem half_rank_zero_and_half_rank_one (r : ℕ) (hr : r = 0 ∨ r = 1) :
    atTop.Tendsto
      (fun H ↦ ({E ∈ heightLE H | E.rank = r}.ncard / (heightLE H).ncard : ℝ)) (𝓝 (1 / 2)) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve.avg_rank_lt_0885 Theorem 3 of [BS2013]: when elliptic curves over ℚ are ordered by height, their average rank is < .885 sorry line 116 source
Source documentation
Theorem 3 of [BS2013]: when elliptic curves over ℚ are ordered by height, their average rank is < .885.

depends on sorry what this means
Statement uses: LT.lt, Real, Filter.limsup, Nat, HDiv.hDiv, finsum, EllipticCurveRank.RatEllipticCurve, EllipticCurveRank.RatEllipticCurve.heightLE, EllipticCurveRank.RatEllipticCurve.rank, Membership.mem, Set, Set.ncard, Filter.atTop, OfScientific.ofScientific, Bool.true
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
31 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem avg_rank_lt_0885 :
    atTop.limsup (fun H ↦ ((∑ᶠ E : heightLE H, E.1.rank) / (heightLE H).ncard : ℝ)) < 0.885 := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve._08375_le_density_rank_zero_one Theorem 4 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 83.75% have rank 0 or 1 sorry line 124 source
Source documentation
Theorem 4 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 83.75% have rank 0 or 1.

depends on sorry what this means
Statement uses: LE.le, Real, OfScientific.ofScientific, Bool.true, Filter.liminf, Nat, HDiv.hDiv, Set.ncard, EllipticCurveRank.RatEllipticCurve, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.heightLE, Or, Eq, EllipticCurveRank.RatEllipticCurve.rank, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem _08375_le_density_rank_zero_one : 0.8375 ≤ atTop.liminf
    fun H ↦ ({E ∈ heightLE H | E.rank = 0 ∨ E.rank = 1}.ncard / (heightLE H).ncard : ℝ) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve._02062_le_density_rank_zero Theorem 5 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 20.62% have rank 0 sorry line 131 source
Source documentation
Theorem 5 of [BS2013]: when elliptic curves over ℚ are ordered by height, a density of at least 20.62% have rank 0.

depends on sorry what this means
Statement uses: LE.le, Real, OfScientific.ofScientific, Bool.true, Filter.liminf, Nat, HDiv.hDiv, Set.ncard, EllipticCurveRank.RatEllipticCurve, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.heightLE, Eq, EllipticCurveRank.RatEllipticCurve.rank, OfNat.ofNat, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem _02062_le_density_rank_zero : 0.2062 ≤ atTop.liminf
    fun H ↦ ({E ∈ heightLE H | E.rank = 0}.ncard / (heightLE H).ncard : ℝ) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
def EllipticCurveRank.RatEllipticCurve.quadraticTwist The quadratic twist $E^d$ of $E : y^2 = x^3 + Ax + B$ by an integer $d$, given by the Weierstrass equation $y^2 = x^3 + d^2Ax + d^3B$ line 138 source
Source documentation
The quadratic twist $E^d$ of $E : y^2 = x^3 + Ax + B$ by an integer $d$, given by the Weierstrass equation $y^2 = x^3 + d^2Ax + d^3B$. For $d \neq 0$ this is the twist of $E$ corresponding to the quadratic field $\mathbb{Q}(\sqrt{d})$. See Section 1 of [Smith2025].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Int, WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat, EllipticCurveRank.RatEllipticCurve.A, EllipticCurveRank.RatEllipticCurve.B
10 instances, coercions and auxiliary constants left out.
```
def quadraticTwist (E : RatEllipticCurve) (d : ℤ) : Affine ℚ :=
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.quadraticTwist_one The twist of $E$ by $d = 1$ is $E$ itself line 143 source
Source documentation
The twist of $E$ by $d = 1$ is $E$ itself.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Eq, WeierstrassCurve.Affine, Rat, EllipticCurveRank.RatEllipticCurve.quadraticTwist, OfNat.ofNat, Int, EllipticCurveRank.RatEllipticCurve.toWeierstrass
Proof uses: of_eq_true, WeierstrassCurve.mk, EllipticCurveRank.RatEllipticCurve.A, EllipticCurveRank.RatEllipticCurve.B, Eq.trans, True, congrFun', congrArg, congr, WeierstrassCurve, HMul.hMul, HPow.hPow, Nat, Int.cast_one, one_pow, one_mul, eq_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwist_one (E : RatEllipticCurve) : E.quadraticTwist 1 = E.toWeierstrass := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.isElliptic_quadraticTwist The quadratic twist of an elliptic curve over $\mathbb{Q}$ by a nonzero $d$ is again an elliptic curve line 149 source
Source documentation
The quadratic twist of an elliptic curve over $\mathbb{Q}$ by a nonzero $d$ is again an elliptic curve.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Int, Ne, OfNat.ofNat, WeierstrassCurve.IsElliptic, Rat, EllipticCurveRank.RatEllipticCurve.quadraticTwist
Proof uses: WeierstrassCurve.IsElliptic.mk, Iff.mpr, IsUnit, WeierstrassCurve.Δ, isUnit_iff_ne_zero, Eq.mpr, HMul.hMul, HPow.hPow, Nat, EllipticCurveRank.RatEllipticCurve.toWeierstrass, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HSub.hSub and 64 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem isElliptic_quadraticTwist (E : RatEllipticCurve) {d : ℤ} (hd : d ≠ 0) :
    (E.quadraticTwist d).IsElliptic where
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.naiveHeight_quadraticTwist The naïve height of the Weierstrass model $E^d$ is $|d|^6$ times the naïve height of $E$ line 159 source
Source documentation
The naïve height of the Weierstrass model $E^d$ is $|d|^6$ times the naïve height of $E$. Ordering the twists of $E$ by $|d|$ is therefore the same as ordering them by naïve height.

standard axioms: propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Int, Eq, Nat, Max.max, HMul.hMul, OfNat.ofNat, HPow.hPow, Int.natAbs, EllipticCurveRank.RatEllipticCurve.A, EllipticCurveRank.RatEllipticCurve.B, EllipticCurveRank.RatEllipticCurve.naiveHeight
Proof uses: Eq.mpr, id, congr, congrArg, Eq.trans, congrFun', Int.natAbs_mul, Int.natAbs_pow, mul_pow, of_eq_true, True, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 20 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem naiveHeight_quadraticTwist (E : RatEllipticCurve) (d : ℤ) :
    max (4 * (d ^ 2 * E.A).natAbs ^ 3) (27 * (d ^ 3 * E.B).natAbs ^ 2)
      = d.natAbs ^ 6 * E.naiveHeight := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
abbrev EllipticCurveRank.RatEllipticCurve.twistRank The rank of the quadratic twist $E^d$ of an elliptic curve $E$ over $\mathbb{Q}$ line 166 source
Source documentation
The rank of the quadratic twist $E^d$ of an elliptic curve $E$ over $\mathbb{Q}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Int, Nat
Proof uses: Module.finrank, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.RatEllipticCurve.quadraticTwist
7 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev twistRank (E : RatEllipticCurve) (d : ℤ) : ℕ :=
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
def EllipticCurveRank.RatEllipticCurve.twistIndexLE The set of nonzero integers $d$ with $|d| \leq H$, which index the quadratic twists $E^d$ ordered by $|d|$ line 171 source
Source documentation
The set of nonzero integers $d$ with $|d| \leq H$, which index the quadratic twists $E^d$ ordered by $|d|$. By naiveHeight_quadraticTwist this is the same as ordering them by height.

standard axioms: propext what this means
Statement uses: Nat, Set, Int
Proof uses: Set.ofPred, And, Ne, OfNat.ofNat, LE.le, abs
6 instances, coercions and auxiliary constants left out.
```
def twistIndexLE (H : ℕ) : Set ℤ := {d : ℤ | d ≠ 0 ∧ |d| ≤ (H : ℤ)}
…
```
theorem EllipticCurveRank.RatEllipticCurve.ncard_twistIndexLE There are $2H$ nonzero integers $d$ with $|d| \leq H$ line 176 source
Source documentation
There are $2H$ nonzero integers $d$ with $|d| \leq H$. This is the normalisation used in [Smith2025].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Set.ncard, Int, EllipticCurveRank.RatEllipticCurve.twistIndexLE, HMul.hMul, OfNat.ofNat
Proof uses: Set, Finset, Finset.erase, Finset.Icc, Neg.neg, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, And, LE.le, Not, True, congr, congrArg, congrFun', Set.ofPred, Ne, abs and 17 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem ncard_twistIndexLE (H : ℕ) : (twistIndexLE H).ncard = 2 * H := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.twistIndexLE
theorem EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025]: when the quadratic twists sorry line 192 source
Source documentation
Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025]: when the quadratic twists $E^d$ of an elliptic curve $E$ over $\mathbb{Q}$ are ordered by $|d|$, 50% of them have rank $0$ and 50% have rank $1$. See goldfeld_conjecture.variants.two_le for the remaining case $2 \leq r$.
Goldfeld states the conjecture for the analytic rank of $E^d$, which the Birch and Swinnerton-Dyer conjecture predicts is equal to the Mordell–Weil rank used here. Corollary 1.2 of [Smith2025] proves that the Birch and Swinnerton-Dyer conjecture for the quadratic twist family of $E$ implies Goldfeld's conjecture for $E$.

depends on sorry what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Nat, Or, Eq, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Set.ncard, Int, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.twistIndexLE, EllipticCurveRank.RatEllipticCurve.twistRank, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem goldfeld_conjecture (E : RatEllipticCurve) (r : ℕ) (hr : r = 0 ∨ r = 1) :
    atTop.Tendsto
      (fun H ↦ ({d ∈ twistIndexLE H | E.twistRank d = r}.ncard / (twistIndexLE H).ncard : ℝ))
      (𝓝 (1 / 2)) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve, EllipticCurveRank.RatEllipticCurve.twistIndexLE
theorem EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture.variants.two_le Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025], in the case sorry line 208 source
Source documentation
Goldfeld's conjecture ([Goldfeld1979], Conjecture B), in the form stated in the introduction of [Smith2025], in the case $2 \leq r$: a density $0$ of the quadratic twists $E^d$ of an elliptic curve $E$ over $\mathbb{Q}$ have rank $r$.
For the Mordell–Weil rank used here this is an unconditional theorem: by Theorem 1.1 of [Smith2025], $100\%$ of the twists $E^d$ have $2^\infty$-Selmer corank $0$ or $1$, and the Mordell–Weil rank is at most the $2^\infty$-Selmer corank (equation (1.1) there), so the twists of rank at least $2$ have density $0$. The corresponding statement for the analytic rank is open.

depends on sorry what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Nat, LE.le, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Set.ncard, Int, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.twistIndexLE, Eq, EllipticCurveRank.RatEllipticCurve.twistRank, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem goldfeld_conjecture.variants.two_le (E : RatEllipticCurve) (r : ℕ) (hr : 2 ≤ r) :
    atTop.Tendsto
      (fun H ↦ ({d ∈ twistIndexLE H | E.twistRank d = r}.ncard / (twistIndexLE H).ncard : ℝ))
      (𝓝 0) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve, EllipticCurveRank.RatEllipticCurve.twistIndexLE
theorem EllipticCurveRank.RatEllipticCurve.goldfeld_conjecture.variants.squarefree Documented declaration: squarefree sorry line 220 source
Source documentation
Goldfeld's conjecture with $d$ restricted to squarefree integers, which is how it is usually stated informally: 50% of the quadratic twists of $E$ have rank $0$ and 50% have rank $1$. The twist $E^d$ only depends on the class of $d$ modulo nonzero rational squares, and the squarefree integers are a system of representatives of these classes. (They need not give pairwise non-isomorphic curves: if $B = 0$ then $E^{-d} = E^d$.)

depends on sorry what this means
Statement uses: EllipticCurveRank.RatEllipticCurve, Nat, Or, Eq, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Set.ncard, Int, Set.ofPred, And, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.twistIndexLE, Squarefree, EllipticCurveRank.RatEllipticCurve.twistRank, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem goldfeld_conjecture.variants.squarefree (E : RatEllipticCurve) (r : ℕ)
    (hr : r = 0 ∨ r = 1) :
    atTop.Tendsto
      (fun H ↦ ({d ∈ twistIndexLE H | Squarefree d ∧ E.twistRank d = r}.ncard /
        {d ∈ twistIndexLE H | Squarefree d}.ncard : ℝ))
      (𝓝 (1 / 2)) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve, EllipticCurveRank.RatEllipticCurve.twistIndexLE
theorem EllipticCurveRank.RatEllipticCurve.unbounded_rank_conjecture From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness." sorry line 231 source
Source documentation
From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness."

depends on sorry what this means
Statement uses: Nat, Exists, EllipticCurveRank.RatEllipticCurve, LE.le, EllipticCurveRank.RatEllipticCurve.rank
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem unbounded_rank_conjecture (n : ℕ) : ∃ E : RatEllipticCurve, n ≤ E.rank := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.finite_twentyone_lt_finrank From [PPVW2016], Section 8.2: "Our heuristic predicts (a) All but finitely many E ∈ ℰ satisfy rk E(ℚ) ≤ 21" sorry line 240 source
Source documentation
From [PPVW2016], Section 8.2: "Our heuristic predicts (a) All but finitely many E ∈ ℰ satisfy rk E(ℚ) ≤ 21". In other words, there are only finitely many elliptic curves over ℚ (up to isomorphism) with rank greater than 21. Notice that this contradicts the previous conjecture.

depends on sorry what this means
Statement uses: Set.Finite, EllipticCurveRank.RatEllipticCurve, Set.ofPred, LT.lt, Nat, OfNat.ofNat, EllipticCurveRank.RatEllipticCurve.rank
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem finite_twentyone_lt_finrank : {E : RatEllipticCurve | 21 < E.rank}.Finite := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.rank_height_count_asymptotic [PPVW2016] 8.2(b): for 1 ≤ r ≤ 20, the number of elliptic curves over ℚ with rank at least r and naïve height at most H is asymptotically H ^ ((21 - r) / 24 + o(1)) sorry line 255 source
Source documentation
[PPVW2016] 8.2(b): for 1 ≤ r ≤ 20, the number of elliptic curves over ℚ with rank at least r and naïve height at most H is asymptotically H ^ ((21 - r) / 24 + o(1)). Note: ℰ_H in 8.2(b) should be ℰ_{≤H}, see the statement of Theorem 7.3.3. When r = 1, the exponent is 20 / 24 = 5 / 6, which agrees with the exponent in card_heightLE_div_pow_five_div_six_tensto and is consistent with half_rank_zero_and_half_rank_one. The equality is asserted only for large H, matching the o(1) above: it cannot hold at small H, because heightLE H is empty for H ≤ 3 (naiveHeight E ≤ 3 forces A = B = 0, which both Δ_ne_zero and reduced exclude) and consists only of the two rank-zero curves y² = x³ ± x for 4 ≤ H ≤ 26, while the right hand side is Real.rpow and hence strictly positive.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Real, And, Filter.Tendsto, Filter.atTop, nhds, Filter.Eventually, Eq, Set.ncard, EllipticCurveRank.RatEllipticCurve, Set.ofPred, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.heightLE, EllipticCurveRank.RatEllipticCurve.rank, HPow.hPow, HAdd.hAdd and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rank_height_count_asymptotic (r : ℕ) (h₁ : 1 ≤ r) (h₂ : r ≤ 20) :
    ∃ f : ℕ → ℝ, atTop.Tendsto f (𝓝 0) ∧
      ∀ᶠ H : ℕ in atTop,
        {E ∈ heightLE H | r ≤ E.rank}.ncard = (H : ℝ) ^ ((21 - r) / 24 + f H) := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve.twentyone_le_rank_height_count_asymptotic [PPVW2016] 8.2(c): the number of elliptic curves over ℚ with rank ≥ 21 and naïve height at most H is asymptotically at most H ^ o(1) sorry line 264 source
Source documentation
[PPVW2016] 8.2(c): the number of elliptic curves over ℚ with rank ≥ 21 and naïve height at most H is asymptotically at most H ^ o(1).

depends on sorry what this means
Statement uses: Exists, Nat, Real, And, Filter.Tendsto, Filter.atTop, nhds, OfNat.ofNat, LT.lt, LE.le, Set.ncard, EllipticCurveRank.RatEllipticCurve, Set.ofPred, Membership.mem, Set, EllipticCurveRank.RatEllipticCurve.heightLE, EllipticCurveRank.RatEllipticCurve.rank, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem twentyone_le_rank_height_count_asymptotic :
    ∃ f : ℕ → ℝ, atTop.Tendsto f (𝓝 0) ∧
      ∀ H : ℕ, 1 < H → {E ∈ heightLE H | 21 ≤ E.rank}.ncard ≤ (H : ℝ) ^ f H := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve.heightLE
theorem EllipticCurveRank.RatEllipticCurve.exists_rank_ge_thirtyone Is there an elliptic curve over ℚ of rank at least 31? sorry line 275 source
Source documentation
Is there an elliptic curve over ℚ of rank at least 31?
The answer is yes: such a curve was found by Claude, Levent Alpöge and Ava Howell in 2026. See https://elliptic-rank.icarm.cloud/curve/302 and WeierstrassCurve.claudeAlpogeHowell31 below.

depends on sorry what this means
Statement uses: Exists, EllipticCurveRank.RatEllipticCurve, LE.le, Nat, OfNat.ofNat, EllipticCurveRank.RatEllipticCurve.rank
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_rank_ge_thirtyone : ∃ E : RatEllipticCurve, 31 ≤ E.rank := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
theorem EllipticCurveRank.RatEllipticCurve.exists_rank_ge_thirtytwo Is there an elliptic curve over ℚ of rank at least 32? sorry line 283 source
Source documentation
Is there an elliptic curve over ℚ of rank at least 32? The largest known rank of an elliptic curve over ℚ as of 2026 is at least 31 (and exactly 31 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer conjecture). See https://elliptic-rank.icarm.cloud/curve/302.

depends on sorry what this means
Statement uses: Exists, EllipticCurveRank.RatEllipticCurve, LE.le, Nat, OfNat.ofNat, EllipticCurveRank.RatEllipticCurve.rank
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_rank_ge_thirtytwo : ∃ E : RatEllipticCurve, 32 ≤ E.rank := by
…
```
Mentions: EllipticCurveRank.RatEllipticCurve
def EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31 The elliptic curve over ℚ of rank at least 31 found by Claude, Levent Alpöge and Ava Howell in 2026 line 295 source
Source documentation
The elliptic curve over ℚ of rank at least 31 found by Claude, Levent Alpöge and Ava Howell in 2026. It has rank exactly 31 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer conjecture.

standard axioms: Quot.sound, propext what this means
Statement uses: WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, Neg.neg
2 instances, coercions and auxiliary constants left out.
```
def claudeAlpogeHowell31 : Affine ℚ where
…
```
theorem EllipticCurveRank.WeierstrassCurve.Δ_claudeAlpogeHowell31 See https://elliptic-rank.icarm.cloud/curve/302 line 307 source
Source documentation
See https://elliptic-rank.icarm.cloud/curve/302. User profile: https://elliptic-rank.icarm.cloud/user/18 and https://elliptic-rank.icarm.cloud/user/53

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, WeierstrassCurve.Δ, EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Eq.mpr, WeierstrassCurve.mk, Neg.neg, id, congrArg, WeierstrassCurve.Affine, EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31.eq_1, HAdd.hAdd, HSub.hSub, WeierstrassCurve.b₂, WeierstrassCurve.b₈, WeierstrassCurve.b₄, WeierstrassCurve.b₆, WeierstrassCurve.Δ.eq_1, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.b₂.eq_1, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.b₄.eq_1 and 29 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Δ_claudeAlpogeHowell31 : claudeAlpogeHowell31.Δ =
    2 ^ 15 * 3 ^ 4 * 5 ^ 4 * 7 ^ 6 * 11 ^ 4 * 13 ^ 5 * 19 ^ 2 * 23 ^ 2 * 29 ^ 3 * 37 ^ 2 * 41 ^ 2 *
    73 ^ 2 * 131 ^ 2 * 167 ^ 2 * 7547 * 632881 * 966509 * 18145679437533309132469 *
    767028866604834801397681553 *
    30580600452196904409276223329355584892025407195996968868775951126238056443210297 := by
…
```
instance EllipticCurveRank.WeierstrassCurve.(instance at line 315) line 315 source
theorem EllipticCurveRank.WeierstrassCurve.thirtyone_le_rank_claudeAlpogeHowell31 The rank of the Claude–Alpöge–Howell curve is at least 31 sorry line 320 source
Source documentation
The rank of the Claude–Alpöge–Howell curve is at least 31.

depends on sorry what this means
Statement uses: LE.le, Nat, OfNat.ofNat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem thirtyone_le_rank_claudeAlpogeHowell31 : 31 ≤ finrank ℤ claudeAlpogeHowell31.Point := by
…
```
theorem EllipticCurveRank.WeierstrassCurve.rank_claudeAlpogeHowell31 The rank of the Claude–Alpöge–Howell curve is exactly 31 sorry line 328 source
Source documentation
The rank of the Claude–Alpöge–Howell curve is exactly 31. It has rank exactly 31 assuming the generalized Riemann hypothesis and the Birch and Swinnerton-Dyer conjecture.

depends on sorry what this means
Statement uses: Eq, Nat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.claudeAlpogeHowell31, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rank_claudeAlpogeHowell31 : finrank ℤ claudeAlpogeHowell31.Point = 31 := by
…
```
def EllipticCurveRank.WeierstrassCurve.ranksunbounded30 The elliptic curve over ℚ of rank at least 30 found by user ranksunbounded in 2026 line 335 source
Source documentation
The elliptic curve over ℚ of rank at least 30 found by user ranksunbounded in 2026. User profile: https://elliptic-rank.icarm.cloud/user/18 It has rank exactly 30 assuming the generalized Riemann hypothesis and Birch and Swinnerton-Dyer conjecture.

standard axioms: Quot.sound, propext what this means
Statement uses: WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, Neg.neg
2 instances, coercions and auxiliary constants left out.
```
def ranksunbounded30 : Affine ℚ where
…
```
theorem EllipticCurveRank.WeierstrassCurve.Δ_ranksunbounded30 See https://elliptic-rank.icarm.cloud/curve/273 line 344 source
Source documentation
See https://elliptic-rank.icarm.cloud/curve/273.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, WeierstrassCurve.Δ, EllipticCurveRank.WeierstrassCurve.ranksunbounded30, HMul.hMul, Neg.neg, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Eq.mpr, WeierstrassCurve.mk, id, congrArg, WeierstrassCurve.Affine, EllipticCurveRank.WeierstrassCurve.ranksunbounded30.eq_1, HAdd.hAdd, HSub.hSub, WeierstrassCurve.b₂, WeierstrassCurve.b₈, WeierstrassCurve.b₄, WeierstrassCurve.b₆, WeierstrassCurve.Δ.eq_1, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.b₂.eq_1, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.b₄.eq_1, WeierstrassCurve.a₆ and 28 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Δ_ranksunbounded30 : ranksunbounded30.Δ =
    -2 ^ 16 * 3 ^ 12 * 5 ^ 8 * 7 ^ 5 * 13 ^ 5 * 31 ^ 2 * 41 ^ 2 * 47 ^ 4 * 53 ^ 3 * 67 ^ 3 * 379 ^ 2 *
    4349 * 25721454817 *
    97018222656318846556561979214040553412450110580812087282349817173780902099339117104673990259247421230916714670243202937 := by
…
```
instance EllipticCurveRank.WeierstrassCurve.(instance at line 351) line 351 source
theorem EllipticCurveRank.WeierstrassCurve.thirty_le_rank_ranksunbounded30 The rank of the ranksunbounded curve is at least 30 sorry line 356 source
Source documentation
The rank of the ranksunbounded curve is at least 30.

depends on sorry what this means
Statement uses: LE.le, Nat, OfNat.ofNat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.ranksunbounded30
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem thirty_le_rank_ranksunbounded30 : 30 ≤ finrank ℤ ranksunbounded30.Point := by
…
```
theorem EllipticCurveRank.WeierstrassCurve.rank_ranksunbounded30 The rank of the ranksunbounded curve is exactly 30 sorry line 361 source
Source documentation
The rank of the ranksunbounded curve is exactly 30.

depends on sorry what this means
Statement uses: Eq, Nat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.ranksunbounded30, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rank_ranksunbounded30 : finrank ℤ ranksunbounded30.Point = 30 := by
…
```
def EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29 The elliptic curve over ℚ of rank at least 29 found by Elkies and Klagsbrun in 2024 line 366 source
Source documentation
The elliptic curve over ℚ of rank at least 29 found by Elkies and Klagsbrun in 2024. It has rank exactly 29 assuming the generalized Riemann hypothesis.

standard axioms: Quot.sound, propext what this means
Statement uses: WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, Neg.neg
2 instances, coercions and auxiliary constants left out.
```
def elkiesKlagsbrun29 : Affine ℚ where
…
```
theorem EllipticCurveRank.WeierstrassCurve.Δ_elkiesKlagsbrun29 See https://mathoverflow.net/a/478050 line 375 source
Source documentation
See https://mathoverflow.net/a/478050.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, WeierstrassCurve.Δ, EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29, HMul.hMul, Neg.neg, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Eq.mpr, WeierstrassCurve.mk, id, congrArg, WeierstrassCurve.Affine, EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29.eq_1, HAdd.hAdd, HSub.hSub, WeierstrassCurve.b₂, WeierstrassCurve.b₈, WeierstrassCurve.b₄, WeierstrassCurve.b₆, WeierstrassCurve.Δ.eq_1, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.b₂.eq_1, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.b₄.eq_1, WeierstrassCurve.a₆ and 28 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem Δ_elkiesKlagsbrun29 : elkiesKlagsbrun29.Δ =
    -2 ^ 19 * 3 ^ 7 * 5 ^ 7 * 7 ^ 4 * 11 ^ 5 * 13 ^ 3 * 17 ^ 4 * 31 ^ 3 * 41 ^ 2 * 43 ^ 2 * 61 ^ 2 *
    233 * 241 ^ 2 * 4139 * 678146849364709860535420504397393 *
    159788990966780131363155786084695062643236502969 *
    4402149008473369392540402625019227412319473055901 := by
…
```
instance EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29IsElliptic line 383 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve.IsElliptic, Rat, EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29
Proof uses: WeierstrassCurve.IsElliptic.mk, Eq.mpr, IsUnit, WeierstrassCurve.Δ, HMul.hMul, Neg.neg, HPow.hPow, Nat, OfNat.ofNat, id, Eq, congrArg, EllipticCurveRank.WeierstrassCurve.Δ_elkiesKlagsbrun29, of_eq_true, Eq.trans, Ne, True, Mathlib.Meta.NormNum.IsInt.neg_to_eq, Mathlib.Meta.NormNum.isInt_mul, Int.negOfNat and 16 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EllipticCurveRank.WeierstrassCurve.twentynine_le_rank_elkiesKlagsbrun29 The rank of the Elkies-Klagsbrun curve is at least 29 sorry line 388 source
Source documentation
The rank of the Elkies-Klagsbrun curve is at least 29.

depends on sorry what this means
Statement uses: LE.le, Nat, OfNat.ofNat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem twentynine_le_rank_elkiesKlagsbrun29 : 29 ≤ finrank ℤ elkiesKlagsbrun29.Point := by
…
```
theorem EllipticCurveRank.WeierstrassCurve.rank_elkiesKlagsbrun29 The rank of the Elkies-Klagsbrun curve is exactly 29 sorry line 393 source
Source documentation
The rank of the Elkies-Klagsbrun curve is exactly 29.

depends on sorry what this means
Statement uses: Eq, Nat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.elkiesKlagsbrun29, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rank_elkiesKlagsbrun29 : finrank ℤ elkiesKlagsbrun29.Point = 29 := by
…
```
def EllipticCurveRank.WeierstrassCurve.elkies28 The elliptic curve over ℚ of rank at least 28 found by Elkies in 2006 line 398 source
Source documentation
The elliptic curve over ℚ of rank at least 28 found by Elkies in 2006. It has rank exactly 28 assuming the generalized Riemann hypothesis.

standard axioms: Quot.sound, propext what this means
Statement uses: WeierstrassCurve.Affine, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, Neg.neg
2 instances, coercions and auxiliary constants left out.
```
def elkies28 : Affine ℚ where
…
```
theorem EllipticCurveRank.WeierstrassCurve.Δ_elkies28 See https://mathoverflow.net/a/478050 line 407 source
Source documentation
See https://mathoverflow.net/a/478050.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Rat, WeierstrassCurve.Δ, EllipticCurveRank.WeierstrassCurve.elkies28, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Eq.mpr, WeierstrassCurve.mk, Neg.neg, id, congrArg, WeierstrassCurve.Affine, EllipticCurveRank.WeierstrassCurve.elkies28.eq_1, HAdd.hAdd, HSub.hSub, WeierstrassCurve.b₂, WeierstrassCurve.b₈, WeierstrassCurve.b₄, WeierstrassCurve.b₆, WeierstrassCurve.Δ.eq_1, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.b₂.eq_1, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.b₄.eq_1 and 28 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem Δ_elkies28 : elkies28.Δ =
    2 ^ 15 * 3 ^ 6 * 5 ^ 6 * 7 ^ 4 * 11 ^ 2 * 13 ^ 4 * 17 ^ 5 * 19 ^ 3 *
    48463 * 20650099 * 315574902691581877528345013999136728634663121 *
    376018840263193489397987439236873583997122096511452343225772113000611087671413 := by
…
```
instance EllipticCurveRank.WeierstrassCurve.elkies28IsElliptic line 414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve.IsElliptic, Rat, EllipticCurveRank.WeierstrassCurve.elkies28
Proof uses: WeierstrassCurve.IsElliptic.mk, Eq.mpr, IsUnit, WeierstrassCurve.Δ, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, id, Eq, congrArg, EllipticCurveRank.WeierstrassCurve.Δ_elkies28, of_eq_true, Eq.trans, Ne, True, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_mul, Eq.refl, Mathlib.Meta.NormNum.isNat_pow and 10 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem EllipticCurveRank.WeierstrassCurve.twentyeight_le_rank_elkies28 The rank of the Elkies curve is at least 28 sorry line 419 source
Source documentation
The rank of the Elkies curve is at least 28.

depends on sorry what this means
Statement uses: LE.le, Nat, OfNat.ofNat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.elkies28
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem twentyeight_le_rank_elkies28 : 28 ≤ finrank ℤ elkies28.Point := by
…
```
theorem EllipticCurveRank.WeierstrassCurve.rank_elkies28 The rank of the Elkies curve is exactly 28 sorry line 424 source
Source documentation
The rank of the Elkies curve is exactly 28.

depends on sorry what this means
Statement uses: Eq, Nat, Module.finrank, Int, WeierstrassCurve.Affine.Point, Rat, EllipticCurveRank.WeierstrassCurve.elkies28, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rank_elkies28 : finrank ℤ elkies28.Point = 28 := by
…
```