Some conjectures about ranks of elliptic curves over ℚ

The question

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. See p. 28 of https://people.maths.bris.ac.uk/~matyd/BSD2011/bsd2011-Bhargava.pdf.

goldfeld_conjecture. 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\le 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$.

unbounded_rank_conjecture. From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness."

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

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

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

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

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

rank_ranksunbounded30. The rank of the ranksunbounded curve is exactly 30.

rank_elkiesKlagsbrun29. The rank of the Elkies-Klagsbrun curve is exactly 29.

rank_elkies28. The rank of the Elkies curve is exactly 28.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.EllipticCurveRank (11 statements).

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))

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))

theorem unbounded_rank_conjecture (n : ℕ) : ∃ E : RatEllipticCurve, n ≤ E.rank

theorem finite_twentyone_lt_finrank : {E : RatEllipticCurve | 21 < E.rank}.Finite

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)

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

theorem exists_rank_ge_thirtytwo : ∃ E : RatEllipticCurve, 32 ≤ E.rank

theorem rank_claudeAlpogeHowell31 : finrank ℤ claudeAlpogeHowell31.Point = 31

theorem rank_ranksunbounded30 : finrank ℤ ranksunbounded30.Point = 30

theorem rank_elkiesKlagsbrun29 : finrank ℤ elkiesKlagsbrun29.Point = 29

theorem rank_elkies28 : finrank ℤ elkies28.Point = 28

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

• goldfeld_conjecture.variants.squarefree — 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…

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

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.