Back to Problems

finite_twentyone_lt_finrank

Specification

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.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem finite_twentyone_lt_finrank : {E : RatEllipticCurve | 21 < E.rank}.Finite
ID: Wikipedia__EllipticCurveRank__finite_twentyone_lt_finrank
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.