Questions, not proof records
Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.
sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.From [PPVW2016], Section 3.1: "from the mid-1960s to the present, it seems that most experts conjectured unboundedness."
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.
[PPVW2016] 8.2(b): for 1 ≤ r ≤ 20, the number of elliptic curves over ℚ with rank 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.
[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).
The rank of the Elkies-Klagsbrun curve is exactly 29.
The rank of the Elkies curve is exactly 28.