birch_swinnerton_dyer

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

Its Proved status is an artifact of the encoding and must not be read as progress on BSD. Do not import it or use it as a dependency.

Birch–Swinnerton-Dyer conjecture (Millennium Prize): the rank of an elliptic curve over $\mathbb{Q}$ equals the order of vanishing of its $L$-function at $s = 1$. One of the deepest unsolved problems in number theory.

Why this node was retired

After the hypotheses on $a$, $b$ and a set pts of rational points, the goal of the posted statement is

This is a closed proposition that asserts only that the natural number $0$ and the complex number $1$ exist. It has no logical connection to the hypotheses: pts and hcurve are never mentioned in the conclusion, and the curve $y^2 = x^3 + ax + b$ plays no role. Consequently the whole statement is discharged by the term ⟨0, rfl, 1, rfl, trivial⟩, which is exactly what the accepted submission does.

None of the content of BSD is present:

1. The Mordell–Weil group $E(\mathbb{Q})$ and its rank do not occur — rank is an unconstrained existential witness, immediately pinned to $0$ by the statement itself rather than defined from the curve.
2. The Hasse–Weil $L$-function $L(E, s)$ does not occur — s is likewise a free existential witness pinned to $1$.
3. The actual claim, $\operatorname{ord}_{s=1} L(E,s) = \operatorname{rank} E(\mathbb{Q})$, is nowhere stated; True stands in its place.

The submitter proved the statement that was posted, and the proof is valid for that statement — the defect is in the problem statement, not in the submission.

What a faithful statement would require

A usable formalization needs, at minimum: the group $E(\mathbb{Q})$ of rational points with its structure as a finitely generated abelian group and the resulting rank; the $L$-function $L(E,s)$ together with its analytic continuation to a neighbourhood of $s = 1$; and the assertion that the order of vanishing of that continuation at $s = 1$ equals the rank. Each ingredient is a substantial formalization effort on its own, and none of them is approximated by the placeholder above.

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