birch_swinnerton_dyer_conjecture

⚠️ Retired — this formal statement is not a formalization of the Birch–Swinnerton-Dyer conjecture.

Despite appearances, the statement reduces to 0 = 0. Its Proved status is an artifact of the preamble and must not be read as progress on BSD. Do not import it or use it as a dependency.

Birch and Swinnerton-Dyer conjecture: for an elliptic curve $E$ over $\mathbb{Q}$, the algebraic rank of $E(\mathbb{Q})$ equals the order of vanishing of the $L$-function $L(E,s)$ at $s = 1$.

One of the seven Millennium Prize Problems. Partial results: Kolyvagin proved BSD for curves of analytic rank $0$ or $1$. The full conjecture is open.

Source: Birch & Swinnerton-Dyer (1965). J. Reine Angew. Math. 218, 79–108.

Why this node was retired

The theorem statement

theorem birch_swinnerton_dyer_conjecture (W : WeierstrassCurve ℚ) [W.IsElliptic] :
    bsdAnalyticRank W = bsdAlgebraicRank W

reads like a faithful formalization, but the two ranks it compares are introduced in the preamble as constant placeholders:

noncomputable def bsdAnalyticRank (W : WeierstrassCurve ℚ) : ℕ := 0
noncomputable def bsdAlgebraicRank (W : WeierstrassCurve ℚ) : ℕ := 0

Both are defined to be the literal natural number $0$, independently of $W$. The goal is therefore definitionally $0 = 0$, closed by rfl, and the hypotheses W and [W.IsElliptic] are never used. Nothing about elliptic curves, Mordell–Weil ranks, or $L$-functions is asserted.

This defect is invisible in the statement itself — only the preamble reveals it — which makes the node more misleading than an overtly vacuous one, and makes its Proved status particularly dangerous to anyone browsing by status.

What a faithful statement would require

bsdAlgebraicRank must be defined as the rank of the finitely generated abelian group $E(\mathbb{Q})$, and bsdAnalyticRank as the order of vanishing at $s = 1$ of the analytic continuation of the Hasse–Weil $L$-function $L(E,s)$. Both are substantial formalization projects, and neither may be introduced as an unconstrained constant in a preamble.

No corrected replacement node exists yet. The Millennium Prize problem remains open.