Arithmetic Geometry

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 (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, state the conjecture, found experimentally on the EDSAC computer.
• 1977: J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer: 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: 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: 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), R. Taylor and A. Wiles (Ann. Math. 141), and C. Breuil, B. Conrad, F. Diamond and R. Taylor (J. Amer. Math. Soc. 14): 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: 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

Motivation

The Selmer group is the main computable invariant attached to the rational points of an elliptic curve (more generally, of an abelian variety) over a number field. J. W. S. Cassels named it in honour of E. S. Selmer, whose numerical work on the curves $ax^3+by^3+cz^3=0$ exposed the limits of descent methods (Selmer 1951). For an elliptic curve $E$ over a number field $K$ and an integer $n\ge 1$, the $n$-Selmer group $\mathrm{Sel}^{(n)}(E/K)$ is a finite group, computable in principle, which contains $E(K)/nE(K)$ and whose remaining part is the $n$-torsion of the Tate–Shafarevich group $\text{Ш}(E/K)$. Finiteness of the Selmer group is the cohomological core of the weak Mordell–Weil theorem, and hence of the Mordell–Weil theorem that $E(K)$ is finitely generated.

Timeline.

• 1951–1954: Selmer studies rational points on cubic curves by two descents and states a conjecture on the number of generators detected by a second descent (Selmer 1951; Selmer 1954).
• 1959–1962: Cassels, in the series Arithmetic on curves of genus 1, introduces the name "Selmer group" and studies its relation with the Tate–Šafarevič group (Cassels 1962).
• 1994: Greenberg extends the notion to $p$-adic Galois representations and motives in Iwasawa theory.

Setting

Let $K$ be a number field with algebraic closure $\bar K$ and absolute Galois group $G_K=\mathrm{Gal}(\bar K/K)$, a profinite group with its Krull topology. Let $E$ be an elliptic curve over $K$, given by a Weierstrass equation, and let $n\ge1$. For a field $L\supseteq K$ write $E(L)$ for the group of $L$-points and $E(\bar L)[n]$ for the $n$-torsion of $E(\bar L)$; the group $G_L$ acts on both.

For a topological group $G$ acting on an abelian group $M$ (regarded as discrete), the continuous first cohomology $H^1(G,M)$ is the group of locally constant maps $c:G\to M$ with $c(gh)=c(g)+g\,c(h)$, modulo the maps $g\mapsto gm-m$.

For each place $v$ of $K$ (finite or infinite), let $K_v$ be the completion, $G_{K_v}=\mathrm{Gal}(\bar K_v/K_v)$, and fix a $K$-embedding $\bar K\hookrightarrow\bar K_v$; it induces the restriction $G_{K_v}\to G_K$ and $H^1(G_K,E[n])\to H^1(G_{K_v},E[n])$. The local Kummer map is

$$\kappa_v: E(K_v)/nE(K_v)\to H^1(G_{K_v},E(\bar K_v)[n]),\qquad P\mapsto[\sigma\mapsto \sigma Q-Q],\quad nQ=P.$$

The $n$-Selmer group is

$$\mathrm{Sel}^{(n)}(E/K)=\bigcap_v \ker\Big(H^1(G_K,E(\bar K)[n])\to H^1(G_{K_v},E(\bar K_v)[n])/\mathrm{im}\,\kappa_v\Big),$$

and the Tate–Shafarevich group $\text{Ш}(E/K)$ is the set of classes in $H^1(G_K,E(\bar K))$ whose restriction to every $G_{K_v}$ is trivial.

Formalization targets

Goal

$$\mathrm{Sel}^{(n)}(E/K)\ \text{is finite}\qquad(n\ge1).$$

Milestones

1. The local identification $H^1(G_{K_v},E[n])/\mathrm{im}\,\kappa_v\cong H^1(G_{K_v},E)[n]$, stated as: $\mathrm{im}\,\kappa_v$ is the kernel of $H^1(G_{K_v},E[n])\to H^1(G_{K_v},E)$, and the image of that map is the $n$-torsion $H^1(G_{K_v},E)[n]$.
2. The exact sequence $0\to E(K)/nE(K)\to\mathrm{Sel}^{(n)}(E/K)\to\text{Ш}(E/K)[n]\to0$.
3. $\text{Ш}(E/K)[n]$ is finite.
4. The weak Mordell–Weil theorem: $E(K)/nE(K)$ is finite.

Significance

The result. Finiteness of $\mathrm{Sel}^{(n)}(E/K)$ gives, through the exact sequence, finiteness of $E(K)/nE(K)$ (weak Mordell–Weil) and of $\text{Ш}(E/K)[n]$. Combined with the theory of heights it yields the Mordell–Weil theorem. The Selmer group is also the object that descent algorithms compute, and the starting point of Iwasawa-theoretic and Bloch–Kato generalisations.

Formalizing it. The finiteness theorem is classical (see e.g. Silverman, Ch. X). A complete development produces continuous Galois cohomology of elliptic curves over number fields, the Kummer sequence, local conditions at all places, and a formal weak Mordell–Weil theorem for arbitrary number fields and arbitrary $n$.

Difficulty

The group $H^1(G_K,E[n])$ itself is infinite, so finiteness can only come from the local conditions, and conditions at all places must be used. The essential input is global arithmetic: the finiteness of the class group and the finite generation of the unit group of a ring of $S$-integers of a finite extension of $K$. The local analysis (behaviour of the Kummer image at places of good reduction not dividing $n$) and the profinite cohomology must both be built for elliptic curves before that input can be applied.

Formalization scope

• $E$ is a WeierstrassCurve K with [E.IsElliptic]; $K$ is a NumberField. The source treats an isogeny $f:A\to B$ of abelian varieties; this mission specialises to elliptic curves and to the isogeny $f=[n]$, $n\ge1$.
• $G_L$ is Field.absoluteGaloisGroup L with its Krull topology. $H^1$ is defined from scratch as locally constant 1-cocycles modulo coboundaries (discrete coefficients).
• Places: finite places are the height-one primes $v$ of $\mathcal O_K$ with completion v.adicCompletion K; infinite places are InfinitePlace K with completion w.Completion. Restriction uses a fixed embedding $\bar K\to\bar K_v$ chosen by IsAlgClosed.lift.
• $\mathrm{Sel}^{(n)}(E/K)$ and $\text{Ш}(E/K)$ are subsets of the cohomology groups. The local condition at $v$ asks that some representative cocycle restrict exactly to $\sigma\mapsto\sigma Q-Q$ with $nQ\in E(K_v)$; this is equivalent to the source's condition because $Q$ may be shifted by an $n$-torsion point.
• The source's exact sequence prints $\mathrm{Sel}^{(2)}$ and $\text{Ш}(A/K)$; the formal statement uses the standard form with $\mathrm{Sel}^{(n)}$ and $\text{Ш}(E/K)[n]$.
• The finiteness of all of $\text{Ш}(E/K)$ (conjectural) and effective computability are not part of the mission.
• Contributions welcome: Galois descent for points, the Kummer sequence, unramified cohomology classes, finiteness of $S$-unit and class-group quotients.

Selected references

• E. S. Selmer, The Diophantine equation $ax^3+by^3+cz^3=0$, Acta Math. 85 (1951), 203–362. https://doi.org/10.1007/BF02395746
• E. S. Selmer, A conjecture concerning rational points on cubic curves, Math. Scand. 2 (1954), 49–54. https://doi.org/10.7146/math.scand.a-10394
• J. W. S. Cassels, Arithmetic on curves of genus 1. III. The Tate–Šafarevič and Selmer groups, Proc. London Math. Soc. (3) 12 (1962), 259–296. https://doi.org/10.1112/plms/s3-12.1.259
• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer, 2009, Chapter X. https://doi.org/10.1007/978-0-387-09494-6
• Wikipedia, Selmer group (revision 1370673670). https://en.wikipedia.org/w/index.php?title=Selmer_group&oldid=1370673670