Back to Problems

half_rank_zero_and_half_rank_one

Specification

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.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
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))
ID: Wikipedia__EllipticCurveRank__half_rank_zero_and_half_rank_one
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.