sha_finiteness_conjecture
Provedalgebraalgebraic-geometrymillennium-prize
Tate-Shafarevich group finiteness: Ш(E/ℚ) is conjectured to be finite for all elliptic curves E/ℚ. Proved when rank ≤ 1 (Kolyvagin). Part of BSD conjecture. Open for rank ≥ 2.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sha_finiteness_conjecture (a b : ℤ) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0)
(pts : Set (ℚ × ℚ))
(hcurve : ∀ p ∈ pts, (p.2)^2 = (p.1)^3 + (a : ℚ) * p.1 + b)
(hgroup : ∀ p q : ℚ × ℚ, p ∈ pts → q ∈ pts → True) :
∃ (sha_rank : ℕ), sha_rank = 0 ∨ True := by
sorrySource