Birch and Swinnerton-Dyer ConjectureOpen Problem
## Motivation An **elliptic curve** over $\mathbb{Q}$ is a smooth cubic curve with a rational point. Its rational points form a finitely generated abelian group $E(\mathbb{Q})$ (Mordell, 1922), so $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$ for an integer $r \ge 0$, the **rank**. No algorithm is known that decides, for a given curve, whether $r > 0$, i.e. whether there are infinitely many rational points. The **Birch and Swinnerton-Dyer conjecture** predicts $r$ from an analytic object, the Hasse–Weil $L$-function $L(E,s)$: it asserts that $r$ equals the order of vanishing of $L(E,s)$ at $s = 1$. It is one of the seven Millennium Prize Problems of the Clay Mathematics Institute; the official formulation is Andrew Wiles' problem description, [*The Birch and Swinnerton-Dyer Conjecture*](https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf) (2000). This mission formalizes that statement, its weak form, and the results Wiles lists as known. **Timeline.** - 1922: L. Mordell (Proc. Cambridge Phil. Soc. 21) proves that $E(\mathbb{Q})$ is finitely generated, answering a question of Poincaré (1901). - 1936: H. Hasse proves $|p + 1 - \#E(\mathbb{F}_p)| \le 2\sqrt p$ at primes of good reduction, so the Euler product for $L(E,s)$ converges for $\operatorname{Re} s > 3/2$; he conjectures that $L(E,s)$ continues to an entire function. - 1965: B. Birch and H. P. F. Swinnerton-Dyer, [*Notes on elliptic curves II*](https://doi.org/10.1515/crll.1965.218.79), state the conjecture, found experimentally on the EDSAC computer. - 1977: J. Coates and A. Wiles, [*On the conjecture of Birch and Swinnerton-Dyer*](https://doi.org/10.1007/BF01402975): for curves with complex multiplication, $L(E,1) \ne 0$ implies $E(\mathbb{Q})$ finite. - 1986: B. Gross and D. Zagier, [*Heegner points and derivatives of L-series*](https://doi.org/10.1007/BF01388809): for modular $E$ with $L(E,1) = 0 \ne L'(E,1)$, a Heegner point has infinite order. - 1989–1990: V. Kolyvagin, [*Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*](https://doi.org/10.1070/IM1989v032n03ABEH000779): for modular $E$ with $L(E,s)$ vanishing to order at most $1$ at $s=1$, the rank equals that order (with a non-vanishing theorem of Bump–Friedberg–Hoffstein and Murty–Murty). - 1995–2001: A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118559)), R. Taylor and A. Wiles ([Ann. Math. 141](https://doi.org/10.2307/2118560)), and C. Breuil, B. Conrad, F. Diamond and R. Taylor ([J. Amer. Math. Soc. 14](https://doi.org/10.1090/S0894-0347-01-00370-8)): every elliptic curve over $\mathbb{Q}$ is modular, so $L(E,s)$ is entire and Kolyvagin's theorem applies to all $E/\mathbb{Q}$. - 2000: the Clay Mathematics Institute adopts Wiles' formulation as a Millennium Prize Problem. - 2014: M. Bhargava, C. Skinner and W. Zhang, [*A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*](https://arxiv.org/abs/1407.1826): the rank conjecture holds for more than $66\%$ of curves ordered by height. The general case is open. ## Setting A **Weierstrass equation** over $\mathbb{Q}$ is $$E :\ y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in \mathbb{Q},$$ with discriminant $\Delta$; in Lean, `WeierstrassCurve ℚ`. It is an **elliptic curve** when $\Delta \ne 0$ (Mathlib's typeclass `IsElliptic`). Its **rational points** $E(\mathbb{Q})$ are the rational solutions $(x,y)$ together with the point at infinity $O$, an abelian group under the chord-and-tangent law (`W.toAffine.Point`). The **rank** is the rank of this group as a $\mathbb{Z}$-module, $$r = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}) \qquad \text{(`BSD.rank W`)},$$ the $r$ in $E(\mathbb{Q}) \simeq \mathbb{Z}^r \oplus E(\mathbb{Q})_{\mathrm{tors}}$. The **Hasse–Weil $L$-series** is built prime by prime. For each prime $p$ take a Weierstrass equation for $E$ that is *minimal at $p$* (integral coefficients, with the $p$-adic valuation of $\Delta$ as small as possible) and reduce it modulo $p$; put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ when the reduction is smooth (**good reduction**). The local factor is $$L_p(E,s) = \begin{cases} (1 - a_p p^{-s} + p^{1-2s})^{-1} & \text{good reduction,}\\ (1 - p^{-s})^{-1} & \text{split multiplicative reduction,}\\ (1 + p^{-s})^{-1} & \text{non-split multiplicative reduction,}\\ 1 & \text{additive reduction,}\end{cases}$$ and $L(E,s) = \prod_p L_p(E,s) = \sum_{n \ge 1} a_n n^{-s}$, convergent for $\operatorname{Re} s > 3/2$ by Hasse's bound. In Lean this is Mathlib's `WeierstrassCurve.LSeries W s`, defined by exactly this recipe (`WeierstrassCurve.LFunction` is the arithmetic function $n \mapsto a_n$, an Euler product of local factors computed on a model minimal at each prime); where the Dirichlet series does not converge, Mathlib's `LSeries` takes the junk value $0$. This is the complete $L$-series $L^*(C,s)$ of Wiles' Remark 1; it differs from the incomplete product over $p \nmid 2\Delta$ in Wiles' display by finitely many factors holomorphic and non-zero at $s = 1$, so both have the same order of vanishing there. An **$L$-function of $E$** is an entire function $\Lambda : \mathbb{C} \to \mathbb{C}$ with $\Lambda(s) = L(E,s)$ for $\operatorname{Re} s > 3/2$ (`BSD.IsLFunction W Λ`). By the identity theorem there is at most one; by modularity there is exactly one. The **order of vanishing** of $\Lambda$ at $s = 1$ is the $m$ with $\Lambda(s) = c(s-1)^m + \dots$, $c \ne 0$; in Lean, `analyticOrderAt Λ 1`, valued in $\mathbb{N} \cup \{\infty\}$, with value $\infty$ exactly when $\Lambda$ vanishes identically near $1$. ## Formalization targets ### Goal: the Birch and Swinnerton-Dyer conjecture (`BSD.birch_swinnerton_dyer`) For every elliptic curve $E$ over $\mathbb{Q}$ there is an entire $\Lambda$ agreeing with $L(E,s)$ on $\operatorname{Re} s > 3/2$ such that $$\operatorname{ord}_{s=1} \Lambda = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{Q}).$$ This is Wiles' *Conjecture (Birch and Swinnerton-Dyer)*: $L(C,s) = c(s-1)^r + \text{higher order terms}$ with $c \ne 0$ and $r = \operatorname{rank} C(\mathbb{Q})$. Open. ### Weaker target: the weak conjecture (`BSD.weak_birch_swinnerton_dyer`) There is an $L$-function $\Lambda$ of $E$ with $\Lambda(1) = 0$ if and only if $E(\mathbb{Q})$ is infinite. Wiles: "In particular this conjecture asserts that $L(C,1) = 0 \Leftrightarrow C(\mathbb{Q})$ is infinite." Open. ### Milestones: what Wiles lists as known 1. **Mordell's theorem** (`BSD.mordell`): $E(\mathbb{Q})$ is a finitely generated abelian group. 2. **Convergence of the $L$-series** (`BSD.lSeriesSummable`): $\sum a_n n^{-s}$ converges for $\operatorname{Re} s > 3/2$. Wiles: "this Euler product is then known to converge for $\operatorname{Re}(s) > 3/2$." 3. **Analytic continuation** (`BSD.exists_isLFunction`): $E$ has an $L$-function. Wiles: Hasse's conjecture, "now been proved" by Wiles, Taylor–Wiles and Breuil–Conrad–Diamond–Taylor. 4. **Gross–Zagier–Kolyvagin** (`BSD.birch_swinnerton_dyer_of_analyticOrderAt_le_one`): if an $L$-function of $E$ vanishes to order at most $1$ at $s = 1$, its order equals the rank. Wiles: "If $L(C,s) \sim c(s-1)^m$ with $c \ne 0$ and $m = 0$ or $1$, then the conjecture holds." A bridging lemma, `BSD.isLFunction_unique`, records that an $L$-function of $E$ is unique when it exists. ## Significance *The result itself.* The conjecture makes the finiteness of $E(\mathbb{Q})$ decidable from $L(E,1)$ and, in its refined form, gives an effective procedure for finding generators (Manin, 1971). Conditionally on it, Tunnell (1983) characterises the congruent numbers, the areas of right triangles with rational sides, a problem open since the tenth century. It is the prototype of the conjectures of Tate, Deligne, Beilinson and Bloch–Kato relating ranks of arithmetic groups to orders of vanishing of $L$-functions. *Formalizing it.* None of the statements in this mission has a machine-checked proof. Mathlib provides the objects: the group law on $E(\mathbb{Q})$, minimal models and reduction types over discrete valuation rings, and the Hasse–Weil $L$-series as a Dirichlet series (2025–2026). It does not contain Mordell's theorem (no theory of heights), Hasse's bound, modularity, or the continuation of $L(E,s)$. On this platform, earlier library entries named `birch_swinnerton_dyer` are retired placeholders whose formal statements reduce to trivialities such as $0 = 0$; they carry a notice saying so and are not formalizations of the conjecture. This mission gives the first faithful statement against Mathlib's own $L$-series. Two published platform results bear directly on the milestones: the descent step `WeierstrassCurve.Affine.Point.addGroup_fg_of_finiteIndex` (finite index of $2E(\mathbb{Q})$ implies finite generation) reduces milestone 1 to the weak Mordell–Weil theorem, and `WeierstrassCurve.modularity_of_semistableModel` from the platform's Fermat's Last Theorem development proves modularity of semistable curves for a notion of modularity defined through eigenform coefficients; relating that notion to `WeierstrassCurve.LSeries` would give milestone 3 for semistable curves. ## Difficulty Neither side of the equation is computable in general. On the algebraic side, descent bounds the rank from above by the rank of a Selmer group, but the gap is the Tate–Shafarevich group Ш$(E)$, which is not known to be finite; the obvious plan, compute the Selmer group and show it has the rank of $E(\mathbb{Q})$, founders on Ш. On the analytic side one can certify $\Lambda(1) \ne 0$ or $\Lambda'(1) \ne 0$ numerically but cannot certify an exact zero, and the only known bridge from $L$-values to rational points, the Heegner point construction, produces at most one independent point. This is why milestone 4 stops at order $\le 1$ and the conjecture is not known for a single curve of rank $\ge 2$. Iwasawa theory (Kato, Skinner–Urban) relates $p$-adic $L$-functions to Selmer groups but yields $p$-adic, not Archimedean, orders of vanishing. The formalization adds its own obstacles: milestone 1 needs heights and the weak Mordell–Weil theorem (Kummer theory over number fields, finiteness of class groups and units); milestone 2 needs Hasse's bound, i.e. the degree of the Frobenius endomorphism; milestones 3 and 4 rest on modularity, Galois representations, modular curves and Euler systems. ## Formalization scope - $E$ is any `WeierstrassCurve ℚ` with `IsElliptic` ($\Delta \ne 0$); no minimality or integrality of the model is assumed. Mathlib's $L$-series passes to a minimal model at each prime internally, and the point group depends only on the curve, so every statement is invariant under change of Weierstrass equation. - The rank is `Module.finrank ℤ W.toAffine.Point`: for a finitely generated abelian group, the $r$ in $\mathbb{Z}^r \oplus T$; for a group of infinite rank Mathlib's `finrank` is $0$, a case milestone 1 excludes. - The $L$-series is Mathlib's `WeierstrassCurve.LSeries`, with all Euler factors including the bad primes, and junk value $0$ where the Dirichlet series diverges. `BSD.IsLFunction` constrains $\Lambda$ only on $\operatorname{Re} s > 3/2$; milestone 2 shows the series is genuine there, and the bridging lemma shows $\Lambda$ is then unique. - The order of vanishing is `analyticOrderAt Λ 1 : ℕ∞`; equating it with a natural number asserts in particular that $\Lambda \not\equiv 0$ near $1$. *No trivializing formalization.* The existential $\Lambda$ cannot be chosen freely: it must agree with the honest, non-zero Dirichlet series on a half-plane, so it is unique, and $\Lambda \equiv 0$ is excluded by the finite value of the rank. Without `IsElliptic` the statements would concern singular cubics, whose point group is $\mathbb{Q}$ or $\mathbb{Q}^\times$; the hypothesis is required, not decorative. *Out of scope.* The refined conjecture (the leading coefficient in terms of Ш$(E)$, the regulator, the real period and the Tamagawa numbers), the finiteness of Ш$(E)$, number fields and abelian varieties, and the functional equation of $L(E,s)$. *Infrastructure needed and welcome contributions.* Heights on $E(\mathbb{Q})$ and the weak Mordell–Weil theorem; Hasse's bound and the multiplicativity of $a_n$; a bridge from Mathlib's `WeierstrassCurve.LSeries` to the $L$-series of a weight-two newform, so that existing modularity results yield milestone 3; Heegner points and Kolyvagin's Euler system for milestone 4; and the bridging lemma, provable now from the identity theorem. Decompositions of every milestone and lemmas about `WeierstrassCurve.LFunction` (its values at primes, multiplicativity, independence of the model) are welcome. ## Selected references - A. Wiles, *The Birch and Swinnerton-Dyer Conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/05/birchswin.pdf - B. J. Birch, H. P. F. Swinnerton-Dyer, *Notes on elliptic curves II*, Journal für die reine und angewandte Mathematik 218 (1965), 79–108. https://doi.org/10.1515/crll.1965.218.79 - L. J. Mordell, *On the rational solutions of the indeterminate equations of the third and fourth degrees*, Proceedings of the Cambridge Philosophical Society 21 (1922), 179–192. - J. Coates, A. Wiles, *On the conjecture of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 39 (1977), 223–251. https://doi.org/10.1007/BF01402975 - B. H. Gross, D. B. Zagier, *Heegner points and derivatives of L-series*, Inventiones Mathematicae 84 (1986), 225–320. https://doi.org/10.1007/BF01388809 - V. A. Kolyvagin, *Finiteness of $E(\mathbb{Q})$ and Ш$(E,\mathbb{Q})$ for a subclass of Weil curves*, Mathematics of the USSR-Izvestiya 32 (1989), 523–541. https://doi.org/10.1070/IM1989v032n03ABEH000779 - A. Wiles, *Modular elliptic curves and Fermat's Last Theorem*, Annals of Mathematics 141 (1995), 443–551. https://doi.org/10.2307/2118559 - R. Taylor, A. Wiles, *Ring-theoretic properties of certain Hecke algebras*, Annals of Mathematics 141 (1995), 553–572. https://doi.org/10.2307/2118560 - C. Breuil, B. Conrad, F. Diamond, R. Taylor, *On the modularity of elliptic curves over $\mathbb{Q}$: wild 3-adic exercises*, Journal of the American Mathematical Society 14 (2001), 843–939. https://doi.org/10.1090/S0894-0347-01-00370-8 - J. B. Tunnell, *A classical Diophantine problem and modular forms of weight 3/2*, Inventiones Mathematicae 72 (1983), 323–334. https://doi.org/10.1007/BF01389327 - M. Bhargava, C. Skinner, W. Zhang, *A majority of elliptic curves over $\mathbb{Q}$ satisfy the Birch and Swinnerton-Dyer conjecture*, 2014. https://arxiv.org/abs/1407.1826 - J. H. Silverman, *The Arithmetic of Elliptic Curves*, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. https://doi.org/10.1007/978-0-387-09494-6