Arithmetic geometry and elliptic curves

Lens

MotivationH

Rational points on cubic curves

Which whole numbers $n$ are the area of a right-angled triangle whose three sides are rational? The $(3, 4, 5)$ triangle shows that $6$ is such a congruent number; the triangle with sides $\tfrac32, \tfrac{20}{3}, \tfrac{41}{6}$ shows that $5$ is. The question appears in Arabic manuscripts of the tenth century, Fibonacci showed in 1225 that $5$ is congruent, and Fermat proved by infinite descent that $1$ is not congruent. A little algebra turns the question into geometry: $n$ is congruent exactly when the cubic curve

y^2 = x^3 - n^2 x

has a rational point with $y \neq 0$ . (For $n = 6$ the $(3,4,5)$ triangle gives the point $(12, 36)$ : indeed $36^2 = 1296 = 12^3 - 36 \cdot 12$ .) A complete answer is still not known: Tunnell's theorem (1983) gives a simple criterion that decides the question — provided the Birch and Swinnerton-Dyer conjecture holds.

This is the pattern of the whole subject. Arithmetic geometry studies polynomial equations with integer or rational coefficients by looking at the geometry of their solution sets. For plane curves the geometry dictates the arithmetic with remarkable force:

Conics (genus $0$ ) have either no rational points or a rational parametrisation by a line — infinitely many, all known (whether a point exists is decided by the Hasse–Minkowski local–global principle).
Cubic curves with a rational point (genus $1$ , the elliptic curves) have rational points forming a finitely generated abelian group: finitely many points generate all the others by a chord-and-tangent construction (Mordell, 1922).
Curves of genus at least $2$ have only finitely many rational points (Faltings, 1983).

Elliptic curves sit on the boundary between "parametrisable" and "finite", which is why they are so rich. They also connect three worlds that this lesson visits in turn: rational points (Mordell–Weil, the rank, Birch and Swinnerton-Dyer), points over finite fields (Hasse, Weil, Sato–Tate) and modular forms (the modularity theorem, and through it Fermat's Last Theorem). This lesson builds on algebraic number theory and algebraic geometry.

IntuitionH

Chords, tangents and a group

Take a cubic curve $E$ and two rational points $P$ and $Q$ on it. The line through them is defined over $\Q$ , and substituting it into the cubic gives a cubic equation in $x$ with rational coefficients. Two of its roots, $x(P)$ and $x(Q)$ , are rational — so the third root is rational too, because the three roots add up to a rational coefficient. The third intersection point $R$ is a new rational point. (If $P = Q$ , use the tangent line.)

Diophantus already used such tricks, and Bachet (1621) found that doubling a point of $y^2 = x^3 - 2$ by the tangent turns $(3, 5)$ into $\left(\tfrac{129}{100}, -\tfrac{383}{1000}\right)$ . Newton described the chord and tangent constructions geometrically. The decisive step came with Poincaré (1901): reflect the third point in the $x$ -axis and declare the result to be $P + Q$ . With the "point at infinity" $O$ as zero, this is an abelian group law, and the arithmetic of the curve becomes the algebra of a group.

Three features of the picture organise everything that follows.

Size. The coordinates of $P, 2P, 3P, \dots$ on Bachet's curve have denominators with $1, 3, 5, 8, 15, 21, \dots$ digits — roughly proportional to $n^2$ . Heights grow quadratically, and this is what makes the group finitely generated.
Reduction. Reducing the equation modulo a prime $p$ gives a curve over $\mathbb{F}_p$ with about $p$ points. The errors $a_p = p + 1 - \#E(\mathbb{F}_p)$ carry deep information.
Analysis. Packaging all the $a_p$ into one function $L(E, s)$ links the finite fields back to the rational points: the conjecture of Birch and Swinnerton-Dyer.

DefinitionsH

Definitions

Throughout, $K$ is a field. When we write short equations we assume $\operatorname{char} K \neq 2, 3$ .

Definition— Weierstrass equation and elliptic curve

A Weierstrass equation over $K$ is

y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6, \qquad a_i \in K,

with associated quantities $b_2 = a_1^2 + 4a_2$ , $b_4 = 2a_4 + a_1a_3$ , $b_6 = a_3^2 + 4a_6$ , $b_8 = a_1^2a_6 + 4a_2a_6 - a_1a_3a_4 + a_2a_3^2 - a_4^2$ and discriminant $\Delta = -b_2^2b_8 - 8b_4^3 - 27b_6^2 + 9b_2b_4b_6$ . An elliptic curve over $K$ is the projective curve defined by a Weierstrass equation with $\Delta \neq 0$ ; it consists of the affine solutions together with one point at infinity $O = [0 : 1 : 0]$ . When $\operatorname{char} K \neq 2, 3$ , a change of variables brings it to the short form $y^2 = x^3 + ax + b$ , for which $\Delta = -16(4a^3 + 27b^2)$ . Intrinsically, an elliptic curve is a smooth projective curve of genus $1$ with a chosen $K$ -rational point.

The condition $\Delta \neq 0$ says that the cubic $x^3 + ax + b$ has no repeated root, which is exactly the condition that the curve is smooth.

Definition— the group law

For $P, Q \in E(K)$ , let $R$ be the third intersection point of the line $PQ$ (the tangent if $P = Q$ ) with $E$ , counted with multiplicity, and define $P + Q$ to be the third intersection of the line $RO$ with $E$ . In short form, $-(x, y) = (x, -y)$ and $P + Q = -R$ . Explicitly, if $P = (x_1, y_1)$ , $Q = (x_2, y_2)$ and $Q \neq -P$ , set

\lambda = \frac{y_2 - y_1}{x_2 - x_1} \ (x_1 \neq x_2), \qquad \lambda = \frac{3x_1^2 + a}{2y_1} \ (P = Q);

then $x_3 = \lambda^2 - x_1 - x_2$ and $P + Q = \big(x_3,\ -\lambda(x_3 - x_1) - y_1\big)$ . The point $O$ is the zero, and $P + (-P) = O$ .

Definition— Mordell–Weil group, rank and torsion

For a number field $K$ , $E(K)$ is the Mordell–Weil group. By the Mordell–Weil theorem it is finitely generated, so $E(K) \cong E(K)_{\mathrm{tors}} \times \Z^r$ with $E(K)_{\mathrm{tors}}$ finite; $r$ is the rank of $E$ over $K$ .

Definition— reduction, the trace of Frobenius and the L-function

Let $E/\Q$ be given by a Weierstrass equation with integer coefficients and minimal discriminant $\Delta$ . For a prime $p \nmid \Delta$ the reduced equation defines an elliptic curve $\tilde E$ over $\mathbb{F}_p$ (good reduction), and we put $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$ . For $p \mid \Delta$ the reduction is singular, and $a_p \in \{1, -1, 0\}$ according as it has a node with rational tangents (split multiplicative), a node with conjugate tangents (non-split multiplicative), or a cusp (additive). The conductor $N$ is a product of the bad primes, to the first power exactly at multiplicative primes. The L-function is

L(E, s) = \prod_{p \nmid \Delta} \big(1 - a_p p^{-s} + p^{1 - 2s}\big)^{-1} \prod_{p \mid \Delta} \big(1 - a_p p^{-s}\big)^{-1} = \sum_{n \ge 1} \frac{a_n}{n^s},

which converges for $\operatorname{Re} s > \tfrac32$ by the Hasse bound below.

Definition— modular elliptic curve

$E/\Q$ of conductor $N$ is modular if there is a weight- $2$ cuspidal newform $f = \sum a_n(f) q^n$ for $\Gamma_0(N)$ with $L(E, s) = L(f, s)$ , that is, $a_p(f) = a_p(E)$ for every prime $p$ . (Equivalently, there is a non-constant map $X_0(N) \to E$ defined over $\Q$ .)

Worked examplesH

Examples and non-examples

Example— A point of order six

On $y^2 = x^3 + 1$ (discriminant $-432$ ) take $P = (2, 3)$ . The tangent at $P$ has slope $\lambda = \tfrac{3 \cdot 4}{2 \cdot 3} = 2$ , so $x(2P) = 4 - 4 = 0$ and $2P = (0, 1)$ . Chords then give

$n$	$1$	$2$	$3$	$4$	$5$	$6$
$nP$	$(2, 3)$	$(0, 1)$	$(-1, 0)$	$(0, -1)$	$(2, -3)$	$O$

so $P$ has order $6$ . Every multiple is integral, as the Nagell–Lutz theorem below requires of torsion points, and $3P = (-1, 0)$ has $y = 0$ : it is a point of order $2$ . In fact $E(\Q) \cong \Z/6\Z$ .

Example— A point of infinite order

On Bachet's curve $y^2 = x^3 - 2$ , $P = (3, 5)$ and $2P = \left(\tfrac{129}{100}, -\tfrac{383}{1000}\right)$ . Since $2P$ is not integral, it is not a torsion point (Nagell–Lutz), so neither is $P$ . The rank of this curve is $1$ and $P$ generates $E(\Q) \cong \Z$ .

Example— The congruent number curves

$E_n: y^2 = x^3 - n^2 x$ . Its points of order $2$ are $(0, 0)$ and $(\pm n, 0)$ , and one can show that these, with $O$ , are all the torsion. So $n$ is congruent if and only if $E_n(\Q)$ has positive rank. For $n = 1$ the rank is $0$ (Fermat's descent), for $n = 5$ the point $(-4, 6)$ has infinite order (check: $(-4)^3 + 25 \cdot 4 = 36$ ), and for $n = 6$ the point $(12, 36)$ comes from the $(3, 4, 5)$ triangle.

Example— Counting points over a small field

Take $E: y^2 = x^3 + x + 1$ over $\mathbb{F}_5$ (here $4 + 27 = 31 \not\equiv 0$ ). The squares mod $5$ are $0, 1, 4$ . For $x = 0, 1, 2, 3, 4$ the right-hand side is $1, 3, 1, 1, 4$ , which has $2, 0, 2, 2, 2$ square roots. So there are $8$ affine points and $\#E(\mathbb{F}_5) = 9$ , inside the Hasse interval $6 \pm 2\sqrt 5 \approx [1.5,\ 10.5]$ , with $a_5 = 6 - 9 = -3$ . A group of order $9$ is $\Z/9$ or $(\Z/3)^2$ ; the second would need all of $E[3]$ to be rational, and the Weil pairing would then force $\mathbb{F}_5$ to contain the cube roots of unity, which it does not ( $3 \nmid 5 - 1$ ). So $E(\mathbb{F}_5) \cong \Z/9\Z$ .

Example— Curves of rank 0, 1, 2 and 3

From Cremona's tables, labelled by conductor: $11a1: y^2 + y = x^3 - x^2 - 10x - 20$ has rank $0$ (and $E(\Q) \cong \Z/5$ ); $37a1: y^2 + y = x^3 - x$ has rank $1$ , generated by $(0, 0)$ , and discriminant $37$ ; $389a1: y^2 + y = x^3 + x^2 - 2x$ has rank $2$ ; $5077a1: y^2 + y = x^3 - 7x + 6$ has rank $3$ . Each is the curve of smallest conductor with its rank. The computation section repeats Birch and Swinnerton-Dyer's experiment on these four.

Example— Non-examples: singular cubics

$y^2 = x^3$ has $\Delta = 0$ : it has a cusp at the origin. Its non-singular points still form a group under the chord rule, but $(x, y) \mapsto x/y$ identifies that group with $(K, +)$ . Similarly $y^2 = x^3 + x^2$ has a node, and its non-singular points form a group isomorphic to $K^\times$ (when the tangents at the node are rational). These degenerate "elliptic curves" are exactly what appears at primes of multiplicative and additive reduction.

ProofH

Central results

Theorem— Theorem 1 (the group law)

Let $E: y^2 = x^3 + ax + b$ be an elliptic curve over $K$ ( $\operatorname{char} K \neq 2, 3$ ). The chord-and-tangent rule makes $E(K)$ an abelian group with identity $O$ and $-(x, y) = (x, -y)$ .

Proof

Closure. Let $P = (x_1, y_1)$ , $Q = (x_2, y_2)$ with $x_1 \neq x_2$ and slope $\lambda$ as in the definition, so $y_2 - y_1 = \lambda(x_2 - x_1)$ . Substituting the line $y = \lambda(x - x_1) + y_1$ into the equation gives

f(x) := x^3 + ax + b - \big(\lambda(x - x_1) + y_1\big)^2 = x^3 - \lambda^2 x^2 + \cdots,

a monic cubic with coefficients in $K$ that vanishes at $x_1$ and $x_2$ . Hence $f(x) = (x - x_1)(x - x_2)(x - x_3)$ with $x_1 + x_2 + x_3 = \lambda^2$ (Vieta), so $x_3 = \lambda^2 - x_1 - x_2 \in K$ , and $y_3 = \lambda(x_3 - x_1) + y_1 \in K$ satisfies the equation because $f(x_3) = 0$ . If $P = Q$ with $y_1 \neq 0$ , the tangent line $y = \lambda(x - x_1) + y_1$ with $2y_1\lambda = 3x_1^2 + a$ makes $x_1$ a double root of $f$ (as $f'(x_1) = 3x_1^2 + a - 2\lambda y_1 = 0$ ), and the same argument gives $x_3 = \lambda^2 - 2x_1$ . In the remaining cases ( $x_1 = x_2$ , $y_1 = -y_2$ ) the line is vertical, meets $E$ again at $O$ , and $P + Q = O$ . Reflection preserves the equation, so $P + Q \in E(K)$ .

Identity, inverses, commutativity. The line through $P$ and $O$ is the vertical line through $P$ ; its third point is $-P$ , and reflecting gives $P + O = P$ . The line through $P$ and $-P$ is vertical, so $P + (-P) = O$ . The line through $P$ and $Q$ does not depend on their order, so $P + Q = Q + P$ .

Associativity is the one non-trivial axiom. It can be verified by a long computation with the formulas (computer algebra does it in seconds), but the conceptual proof identifies $E(K)$ with the degree-zero Picard group: $P \mapsto [P] - [O]$ is a bijection $E(K) \to \operatorname{Pic}^0_K(E)$ by the Riemann–Roch theorem, and the chord rule is the statement that $P + Q + R = O$ exactly when $[P] + [Q] + [R] - 3[O]$ is the divisor of a line, a principal divisor. So the group law is transported from a group (Silverman, The Arithmetic of Elliptic Curves, III.3.4). Mathlib uses an algebraic version of this idea; see the formal section.

∎

Theorem— Proposition 2 (points of order two)

A point $P \neq O$ satisfies $2P = O$ if and only if $y(P) = 0$ . Over an algebraic closure there are exactly three such points, $(e_i, 0)$ for the three roots $e_i$ of $x^3 + ax + b$ , and $E[2] \cong (\Z/2)^2$ .

Proof

$2P = O$ means $P = -P$ , i.e. $(x, y) = (x, -y)$ , i.e. $y = 0$ (as $\operatorname{char} K \neq 2$ ). The points with $y = 0$ are the $(e, 0)$ with $e^3 + ae + b = 0$ , and the three roots are distinct because $\Delta \neq 0$ . With $O$ these form a group of order $4$ in which every element has order at most $2$ , so it is $(\Z/2)^2$ .

∎

Theorem— Theorem 3 (Nagell 1935, Lutz 1937; Mazur 1977)

Let $E: y^2 = x^3 + ax + b$ with $a, b \in \Z$ . If $P = (x, y) \in E(\Q)$ is a torsion point, then $x, y \in \Z$ , and either $y = 0$ or $y^2 \mid 4a^3 + 27b^2$ . Moreover (Mazur) $E(\Q)_{\mathrm{tors}}$ is isomorphic to one of the fifteen groups $\Z/n$ for $1 \le n \le 10$ or $n = 12$ , and $\Z/2 \times \Z/2m$ for $1 \le m \le 4$ .

Nagell–Lutz is proved with the formal group (or by valuations of denominators) in Silverman–Tate, Chapter 2; it makes torsion computable: only finitely many candidates $y$ need testing. Mazur's theorem is much deeper (it rests on the arithmetic of the modular curves $X_0(N)$ and $X_1(N)$ ).

Theorem— Theorem 4 (Mordell 1922; Weil 1928)

For an elliptic curve $E$ over a number field $K$ , the group $E(K)$ is finitely generated.

The proof has two halves. The weak Mordell–Weil theorem says that $E(K)/2E(K)$ is finite. Over $L = K(E[2])$ , a Kummer map embeds $E(L)/2E(L)$ into $(L^\times/L^{\times 2})^2$ , landing in the classes that are unramified outside a finite set $S$ of primes; that group is finite by the finiteness of the class group and Dirichlet's $S$ -unit theorem, and finiteness over $L$ implies finiteness over $K$ . The descent half uses a height function and is purely group-theoretic; we prove it in full.

Theorem— Lemma 5 (the descent lemma)

Let $A$ be an abelian group and $h: A \to \R_{\ge 0}$ a function such that (i) for every $B$ the set $\{P : h(P) \le B\}$ is finite; (ii) there is a constant $C$ with $|h(P + Q) + h(P - Q) - 2h(P) - 2h(Q)| \le C$ for all $P, Q$ ; (iii) $A/2A$ is finite. Then $A$ is finitely generated.

Proof

Choose representatives $Q_1, \dots, Q_m$ of the cosets of $2A$ and let $c = \max_i h(Q_i)$ . Taking $Q = P$ in (ii) gives $h(2P) \ge 4h(P) - h(0) - C$ , and (ii) also gives $h(P - Q) \le 2h(P) + 2h(Q) + C$ . Now let $P \in A$ and write $P = Q_{i} + 2P_1$ . Then

4h(P_1) - h(0) - C \le h(2P_1) = h(P - Q_i) \le 2h(P) + 2c + C,

so $h(P_1) \le \tfrac12 h(P) + c'$ with $c' = \tfrac14 (2c + 2C + h(0))$ . Repeating, $P = Q_{i_1} + 2Q_{i_2} + \cdots + 2^{n-1}Q_{i_n} + 2^n P_n$ with

h(P_n) \le 2^{-n} h(P) + c'\left(1 + \tfrac12 + \cdots + 2^{1-n}\right) \le 2^{-n} h(P) + 2c'.

For $n$ large $h(P_n) \le 1 + 2c'$ . Hence $A$ is generated by $Q_1, \dots, Q_m$ together with the set $\{R : h(R) \le 1 + 2c'\}$ , which is finite by (i).

∎

For $E(K)$ one takes the naïve height $h(P) = \log H(x(P))$ , where $H(u/v) = \max(|u|, |v|)$ in lowest terms over $\Q$ (with the analogous product over places for number fields). Property (i) holds because there are finitely many rationals of bounded height, and (ii), the approximate parallelogram law, is a careful estimate with the duplication formula. The limit $\hat h(P) = \lim_n h(2^nP)/4^n$ is the canonical height, an exact quadratic form on $E(K)$ : this is the quadratic growth seen on Bachet's curve.

Theorem— Theorem 6 (Hasse 1933)

For an elliptic curve $E$ over $\mathbb{F}_q$ , $\big|\#E(\mathbb{F}_q) - (q + 1)\big| \le 2\sqrt q$ .

Proof

We use two standard facts about the endomorphism ring of $E$ over $\overline{\mathbb{F}}_q$ (Silverman III.6 and V.1). Let $\phi(x, y) = (x^q, y^q)$ be the Frobenius endomorphism; its fixed points are exactly $E(\mathbb{F}_q)$ , so $E(\mathbb{F}_q) = \ker(1 - \phi)$ .

The degree map $\deg : \operatorname{End}(E) \to \Z$ is a positive definite quadratic form: $\deg(\psi) \ge 0$ , with equality only for $\psi = 0$ , and $(\psi, \chi) \mapsto \deg(\psi + \chi) - \deg\psi - \deg\chi$ is bilinear. Also $\deg \phi = q$ .
$1 - \phi$ is separable (its differential is $1$ ), so $\#\ker(1 - \phi) = \deg(1 - \phi)$ .

Put $N = \#E(\mathbb{F}_q) = \deg(1 - \phi)$ and $a = q + 1 - N$ . By fact 1, for all integers $m, n$ ,

0 \le \deg(m - n\phi) = m^2 \deg(1) + n^2 \deg(\phi) - mn\big(\deg(1) + \deg(\phi) - \deg(1 - \phi)\big) = m^2 - a\,mn + q\,n^2.

A binary quadratic form that is non-negative on $\Z^2$ is non-negative on $\Q^2$ (scale) and hence on $\R^2$ (continuity), so its discriminant is $\le 0$ : $a^2 - 4q \le 0$ , that is $|a| \le 2\sqrt q$ .

∎

The same computation gives more. $\phi$ satisfies $\phi^2 - a\phi + q = 0$ in $\operatorname{End}(E)$ ; if $\alpha, \beta$ are the roots of $T^2 - aT + q$ (complex conjugates of absolute value $\sqrt q$ ), then $\#E(\mathbb{F}_{q^n}) = q^n + 1 - \alpha^n - \beta^n$ for every $n$ , and the zeta function

Z(E/\mathbb{F}_q, T) = \exp\Big(\sum_{n \ge 1} \#E(\mathbb{F}_{q^n}) \frac{T^n}{n}\Big) = \frac{1 - aT + qT^2}{(1 - T)(1 - qT)}

is rational, satisfies a functional equation under $T \mapsto 1/(qT)$ , and has its zeros on $|T| = q^{-1/2}$ — the Riemann hypothesis for $E$ . For $y^2 = x^3 + x + 1$ over $\mathbb{F}_5$ , $a = -3$ , so $\#E(\mathbb{F}_{25}) = 26 - (\alpha^2 + \beta^2) = 26 - (a^2 - 2q) = 27$ .

Theorem— Theorem 7 (the Weil conjectures; Weil, Dwork, Grothendieck, Deligne)

For a smooth projective variety $X$ of dimension $d$ over $\mathbb{F}_q$ , the zeta function $Z(X, T)$ is a rational function $\frac{P_1(T) P_3(T) \cdots P_{2d-1}(T)}{P_0(T) P_2(T) \cdots P_{2d}(T)}$ satisfying a functional equation, and the reciprocal roots of $P_i$ have absolute value $q^{i/2}$ . If $X$ lifts to characteristic $0$ , $\deg P_i$ is the $i$ -th Betti number of the complex variety.

Weil proved the case of curves (1940s); Dwork proved rationality (1960); Grothendieck and his school built $\ell$ -adic cohomology, which gives rationality and the functional equation via a Lefschetz trace formula; Deligne proved the Riemann hypothesis (1974). For an elliptic curve, $H^1$ has rank $2$ and Frobenius acts on it with eigenvalues $\alpha, \beta$ : Hasse's theorem is the case $d = 1$ , $g = 1$ .

Theorem— Theorem 8 (modularity; Wiles 1995, Taylor–Wiles 1995, Breuil–Conrad–Diamond–Taylor 2001)

Every elliptic curve over $\Q$ is modular. Consequently $L(E, s)$ has an analytic continuation to all of $\C$ and satisfies the functional equation $\Lambda(s) = \pm \Lambda(2 - s)$ , where $\Lambda(s) = N^{s/2} (2\pi)^{-s} \Gamma(s) L(E, s)$ .

Wiles (with Taylor–Wiles for a key step) proved the theorem for semistable curves, those with only multiplicative bad reduction; Breuil, Conrad, Diamond and Taylor completed the general case. Example: for $11a1$ , $\sum a_n q^n = q \prod_{n \ge 1} (1 - q^n)^2 (1 - q^{11n})^2$ , a weight- $2$ cusp form for $\Gamma_0(11)$ ; the Langlands lesson checks this numerically.

Theorem— Corollary 9 (Fermat's Last Theorem)

For $n \ge 3$ there are no positive integers with $a^n + b^n = c^n$ .

The route, in outline. It suffices to treat $n = 4$ (Fermat) and odd primes $n = \ell \ge 5$ ( $\ell = 3$ is Euler's case). Given a solution $a^\ell + b^\ell = c^\ell$ with $a, b, c$ coprime, suitably normalised, Frey (1984–86) considered

E_{a,b}: y^2 = x(x - a^\ell)(x + b^\ell),

whose discriminant is $16(abc)^{2\ell}$ : it is semistable, and its $\ell$ -torsion is "too lightly ramified". Ribet's theorem (1986–90, proving Serre's $\varepsilon$ -conjecture) then says that if $E_{a,b}$ were modular of level $N$ , its $\ell$ -torsion would come from a weight- $2$ newform of level $2$ . There are no such forms (the space $S_2(\Gamma_0(2))$ is zero). So $E_{a,b}$ is not modular, contradicting Wiles's theorem for semistable curves.

Theorem— Conjecture 10 (Birch and Swinnerton-Dyer, 1960s)

For $E/\Q$ , the order of vanishing of $L(E, s)$ at $s = 1$ equals the rank $r$ of $E(\Q)$ , and

\lim_{s \to 1} \frac{L(E, s)}{(s - 1)^r} = \frac{\#\text{Ш}(E/\Q)\ \Omega_E\ \operatorname{Reg}_E \prod_p c_p}{\big(\#E(\Q)_{\mathrm{tors}}\big)^2},

where $\Omega_E$ is the real period, $\operatorname{Reg}_E$ the determinant of the canonical height pairing on a basis of $E(\Q)/E(\Q)_{\mathrm{tors}}$ , $c_p$ the Tamagawa numbers, and $\text{Ш}$ the Tate–Shafarevich group (conjecturally finite).

The heuristic behind it: $L(E, 1)$ is formally $\prod_p (1 - a_p/p + 1/p)^{-1} = \prod_p p/N_p$ . If $E$ has many rational points, they reduce to many points mod $p$ , the $N_p$ are on average a little larger than $p$ , and the product is pulled towards $0$ . Birch and Swinnerton-Dyer computed $\prod_{p \le X} N_p/p$ on the EDSAC-2 computer at Cambridge and saw growth like $C(\log X)^r$ .

ExplanationH

The landscape: what is known, what is open

Established theorems.

Rank 0 and 1. If the analytic rank $\operatorname{ord}_{s=1} L(E, s)$ is $0$ or $1$ , then it equals the rank and Ш is finite: Gross–Zagier (1986) constructed Heegner points whose height is $L'(E, 1)$ up to a non-zero factor, Kolyvagin (1988–89) bounded Selmer groups with Euler systems, and modularity (Theorem 8) removes the hypothesis they needed. Earlier, Coates and Wiles (1977) proved that $L(E, 1) \neq 0$ implies $E(\Q)$ finite for curves with complex multiplication.
Averages. Ordering curves by height, Bhargava and Shankar (2010s) proved that the average rank is bounded (by $0.885$ , using $5$ -Selmer groups); a positive proportion of curves have rank $0$ and a positive proportion rank $1$ ; and Bhargava, Skinner and Zhang (2014) deduced that a majority of elliptic curves over $\Q$ satisfy the rank part of BSD.
Congruent numbers. Tian Ye (2014) proved that for every $k \ge 1$ there are infinitely many square-free congruent numbers with exactly $k$ prime factors.
Sato–Tate. For $E/\Q$ without complex multiplication the angles $\theta_p$ in $a_p = 2\sqrt p \cos\theta_p$ are equidistributed with density $\tfrac{2}{\pi}\sin^2\theta$ : proved by Clozel, Harris, Shepherd-Barron and Taylor (2008) when $j(E) \notin \Z$ , and by Barnet-Lamb, Geraghty, Harris and Taylor (2011) in general.
Higher genus. Faltings (1983) proved Mordell's conjecture: a curve of genus $\ge 2$ over a number field has finitely many rational points. The proof is not effective: it bounds the number of points but gives no algorithm to find them all.

Open problems.

The Birch and Swinnerton-Dyer conjecture — open for analytic rank $\ge 2$ , and the full leading-term formula is open in general even in ranks $0$ and $1$ (it is known for many individual curves). It is one of the Clay Millennium Problems.
Finiteness of Ш — known when the analytic rank is at most $1$ , open in general.
Computing the rank. No algorithm is known that provably computes the rank of every $E/\Q$ ; descent algorithms terminate if Ш is finite (or if BSD holds), which is why they work in practice.
Boundedness of ranks. Curves of rank at least $28$ are known (Elkies, 2006). Whether ranks over $\Q$ are bounded is open; the heuristics of Park, Poonen, Voight and Wood (2019) predict that only finitely many curves have rank greater than $21$ .
Uniformity. Is the number of rational points on curves of genus $g \ge 2$ bounded in terms of $g$ and the rank of the Jacobian alone? Major progress came in 2020–21 (Dimitrov, Gao and Habegger; Kühne), but effective versions remain open.

Formal mathematicsF

Elliptic curves in Lean and Mathlib

Mathlib has Weierstrass curves over any commutative ring, their discriminants and $j$ -invariants, nonsingular points, the group of points of an elliptic curve over a field, reduction, naïve heights and the formal $L$ -function of a curve over a number field. We formalise the algebra of the lesson and connect it to these definitions.

The discriminant of the short form, from Mathlib's general formula:

short_discriminantLean 4Proved here from basic factsFormally verified

/-- For a short Weierstrass equation `y² = x³ + a₄x + a₆` (so `a₁ = a₂ = a₃ = 0`), Mathlib's
general discriminant `Δ = −b₂²b₈ − 8b₄³ − 27b₆² + 9b₂b₄b₆` simplifies to
`Δ = −16(4a₄³ + 27a₆²)`. So the curve is smooth exactly when `4a³ + 27b² ≠ 0` (away from
characteristic 2). Proof: unfold `b₂, b₄, b₆, b₈` and compute. -/
theorem short_discriminant {R : Type*} [CommRing R] (W : WeierstrassCurve R)
    (h₁ : W.a₁ = 0) (h₂ : W.a₂ = 0) (h₃ : W.a₃ = 0) :
    W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) := by
  simp only [Δ, b₂, b₄, b₆, b₈, h₁, h₂, h₃]
  ring

Axioms used: propext, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

The closure step of Theorem 1. The Lean proof follows the human one with the Vieta argument unwound: subtracting the two curve equations and cancelling $x_2 - x_1$ solves for $a$ , the first equation solves for $b$ , and what remains is a polynomial identity.

chord_third_pointLean 4Proved here from basic factsFormally verified

/-- **The chord construction.** Let `P₁ = (x₁, y₁)` and `P₂ = (x₂, y₂)` lie on
`y² = x³ + ax + b` with `x₁ ≠ x₂`, and let `ℓ` be the slope of the chord, `y₂ − y₁ = ℓ(x₂ − x₁)`.
Then the point with `x₃ = ℓ² − x₁ − x₂` and `y₃ = ℓ(x₃ − x₁) + y₁` — the third intersection of
the chord with the curve — lies on the curve. (Its reflection `(x₃, −y₃)` is `P₁ + P₂`.)

Proof, as in the lesson: subtracting the two curve equations and cancelling `x₂ − x₁` expresses
`a` through the chord; the first equation expresses `b`; after substituting, the claim is a
polynomial identity — Vieta's formula `x₁ + x₂ + x₃ = ℓ²` in disguise. -/
theorem chord_third_point {F : Type*} [Field F] {a b x₁ y₁ x₂ y₂ ℓ : F}
    (h₁ : y₁ ^ 2 = x₁ ^ 3 + a * x₁ + b) (h₂ : y₂ ^ 2 = x₂ ^ 3 + a * x₂ + b)
    (hx : x₁ ≠ x₂) (hℓ : y₂ - y₁ = ℓ * (x₂ - x₁)) :
    (ℓ * ((ℓ ^ 2 - x₁ - x₂) - x₁) + y₁) ^ 2 =
      (ℓ ^ 2 - x₁ - x₂) ^ 3 + a * (ℓ ^ 2 - x₁ - x₂) + b := by
  have hy₂ : y₂ = y₁ + ℓ * (x₂ - x₁) := by linear_combination hℓ
  -- `h₂ − h₁`, factorised: `(x₂ − x₁) · (ℓ(2y₁ + ℓ(x₂ − x₁)) − (x₂² + x₁x₂ + x₁² + a)) = 0`.
  have key : (x₂ - x₁) *
      (ℓ * (2 * y₁ + ℓ * (x₂ - x₁)) - (x₂ ^ 2 + x₁ * x₂ + x₁ ^ 2 + a)) = 0 := by
    rw [hy₂] at h₂
    linear_combination h₂ - h₁
  have hne : x₂ - x₁ ≠ 0 := sub_ne_zero.mpr (Ne.symm hx)
  have ha : a = ℓ * (2 * y₁ + ℓ * (x₂ - x₁)) - (x₂ ^ 2 + x₁ * x₂ + x₁ ^ 2) := by
    have := (mul_eq_zero.mp key).resolve_left hne
    linear_combination -this
  have hb : b = y₁ ^ 2 - x₁ ^ 3 - a * x₁ := by linear_combination -h₁
  rw [hb, ha]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

tangent_third_pointLean 4Proved here from basic factsFormally verified

/-- **The tangent construction.** If `P₁ = (x₁, y₁)` lies on `y² = x³ + ax + b` and `ℓ` is the
slope of the tangent there, `2y₁ℓ = 3x₁² + a` (implicit differentiation), then the point with
`x₃ = ℓ² − 2x₁` and `y₃ = ℓ(x₃ − x₁) + y₁` lies on the curve; its reflection is `2P₁`.
The tangent meets the curve at `P₁` twice, so Vieta now reads `2x₁ + x₃ = ℓ²`. -/
theorem tangent_third_point {F : Type*} [Field F] {a b x₁ y₁ ℓ : F}
    (h₁ : y₁ ^ 2 = x₁ ^ 3 + a * x₁ + b) (hℓ : 2 * y₁ * ℓ = 3 * x₁ ^ 2 + a) :
    (ℓ * ((ℓ ^ 2 - 2 * x₁) - x₁) + y₁) ^ 2 =
      (ℓ ^ 2 - 2 * x₁) ^ 3 + a * (ℓ ^ 2 - 2 * x₁) + b := by
  have ha : a = 2 * y₁ * ℓ - 3 * x₁ ^ 2 := by linear_combination -hℓ
  have hb : b = y₁ ^ 2 - x₁ ^ 3 - a * x₁ := by linear_combination -h₁
  rw [hb, ha]
  ring

Axioms used: propext, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

Mathlib's general formula, for any Weierstrass equation, and associativity. Mathlib's proof of associativity (Angdinata and Xu, 2023) is elementary but not computational: it sends each point to the class of its ideal in the coordinate ring $K[x, y]/(W)$ , shows that this map into the ideal class group is injective and turns the chord rule into multiplication — an algebraic avatar of the map $E \to \operatorname{Pic}^0(E)$ in the proof of Theorem 1.

sum_on_curveLean 4Applies a library theoremFormally verified

/-- Mathlib's general version, for any Weierstrass equation
`y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆` over a field: unless `P₂ = −P₁`, the point
`(addX, addY)` built from the chord (or tangent) slope `W.slope` lies on the curve.
This applies `WeierstrassCurve.Affine.equation_add`. -/
theorem sum_on_curve {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    {x₁ x₂ y₁ y₂ : F} (h₁ : W.toAffine.Equation x₁ y₁) (h₂ : W.toAffine.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.toAffine.negY x₂ y₂)) :
    W.toAffine.Equation (W.toAffine.addX x₁ x₂ (W.toAffine.slope x₁ x₂ y₁ y₂))
      (W.toAffine.addY x₁ x₂ y₁ (W.toAffine.slope x₁ x₂ y₁ y₂)) :=
  Affine.equation_add h₁ h₂ hxy

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

add_assoc_pointsLean 4Applies a library theoremFormally verified

/-- The chord-and-tangent law is **associative**. This is the one genuinely hard group axiom;
Mathlib proves it (D. K. Angdinata and J. Xu) not by the classical page of algebra but by
showing that `P ↦ [ideal of P]` is an injective map into the ideal class group of the
coordinate ring `F[x, y]/(W)` that turns `+` into multiplication of ideal classes — so the
points inherit associativity from a group. This applies `add_assoc` for the instance
`AddCommGroup W.toAffine.Point`. -/
theorem add_assoc_points {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (P Q R : W.toAffine.Point) : P + Q + R = P + (Q + R) :=
  add_assoc P Q R

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

two_torsionLean 4Applies a library theoremFormally verified

/-- On a curve `y² + a₂… = x³ + …` with `a₁ = a₃ = 0` (for instance a short Weierstrass curve),
a point with `y = 0` is its own negative, so `P + P = 0`: the points of order 2 are the
roots of the cubic. This applies `WeierstrassCurve.Affine.Point.add_self_of_Y_eq`, since
`negY x 0 = −0 − a₁x − a₃ = 0`. -/
theorem two_torsion {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (h₁ : W.a₁ = 0) (h₃ : W.a₃ = 0) {x : F} (h : W.toAffine.Nonsingular x 0) :
    (Affine.Point.some x 0 h + Affine.Point.some x 0 h : W.toAffine.Point) = 0 :=
  Affine.Point.add_self_of_Y_eq (by simp [Affine.negY, h₁, h₃])

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

The worked examples, computed in Lean with Mathlib's addition law: the point of order six, Bachet's duplication and the curve $37a1$ .

torsionCurveLean 4Formally verified

/-- The curve `y² = x³ + 1` over `ℚ`, with Weierstrass coefficients
`(a₁, a₂, a₃, a₄, a₆) = (0, 0, 0, 0, 1)`. Its discriminant is `−16 · 27 = −432`. -/
def torsionCurve : WeierstrassCurve ℚ := ⟨0, 0, 0, 0, 1⟩

Axioms used: propext, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

torsionPointLean 4Formally verified

/-- The rational point `P = (2, 3)` on `y² = x³ + 1` (indeed `9 = 8 + 1`), as an element of the
group of points. The proof obligation is that `(2, 3)` is a nonsingular point of the curve. -/
noncomputable def torsionPoint : torsionCurve.toAffine.Point :=
  .some 2 3 (by
    rw [Affine.nonsingular_iff]
    norm_num [torsionCurve, Affine.Equation, Affine.evalEval_polynomial])

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

torsion_order_sixLean 4Proved here from basic factsFormally verified

/-- `P = (2, 3)` has **order exactly 6** on `y² = x³ + 1`. Lean computes the multiples with
Mathlib's addition law, exactly as in the lesson's table:
`2P = (0, 1)`, `3P = (−1, 0)`, `4P = (0, −1)`, `5P = (2, −3) = −P`, `6P = 0`;
none of `P, …, 5P` is the point at infinity, so the order is 6. (Mazur's theorem says that
torsion orders over `ℚ` are at most 12; this is one of the possible groups, `ℤ/6`.) -/
theorem torsion_order_six : addOrderOf torsionPoint = 6 := by
  have n2 : torsionCurve.toAffine.Nonsingular 0 1 := by
    rw [Affine.nonsingular_iff]; norm_num [torsionCurve, Affine.Equation, Affine.evalEval_polynomial]
  have n3 : torsionCurve.toAffine.Nonsingular (-1) 0 := by
    rw [Affine.nonsingular_iff]; norm_num [torsionCurve, Affine.Equation, Affine.evalEval_polynomial]
  have n4 : torsionCurve.toAffine.Nonsingular 0 (-1) := by
    rw [Affine.nonsingular_iff]; norm_num [torsionCurve, Affine.Equation, Affine.evalEval_polynomial]
  have n5 : torsionCurve.toAffine.Nonsingular 2 (-3) := by
    rw [Affine.nonsingular_iff]; norm_num [torsionCurve, Affine.Equation, Affine.evalEval_polynomial]
  -- the tangent at `P` has slope `3·2²/(2·3) = 2`
  have h2 : (2 : ℕ) • torsionPoint = .some 0 1 n2 := by
    rw [two_nsmul, torsionPoint, Affine.Point.add_self_of_Y_ne (by
      simp [torsionCurve, Affine.negY]; norm_num)]
    simp [torsionCurve, Affine.addY, Affine.negY]
    norm_num
  -- chords: `(0, 1) + P`, `(−1, 0) + P`, `(0, −1) + P`
  have h3 : (3 : ℕ) • torsionPoint = .some (-1) 0 n3 := by
    rw [succ_nsmul, h2, torsionPoint, Affine.Point.add_of_X_ne (by norm_num)]
    simp [torsionCurve, Affine.addY, Affine.negY]
    norm_num
  have h4 : (4 : ℕ) • torsionPoint = .some 0 (-1) n4 := by
    rw [succ_nsmul, h3, torsionPoint, Affine.Point.add_of_X_ne (by norm_num)]
    simp [torsionCurve, Affine.addY, Affine.negY]
    norm_num
  have h5 : (5 : ℕ) • torsionPoint = .some 2 (-3) n5 := by
    rw [succ_nsmul, h4, torsionPoint, Affine.Point.add_of_X_ne (by norm_num)]
    simp [torsionCurve, Affine.addY, Affine.negY]
    norm_num
  -- `5P = −P`, so `6P = 0`
  have h6 : (6 : ℕ) • torsionPoint = 0 := by
    rw [succ_nsmul, h5, torsionPoint, Affine.Point.add_of_Y_eq rfl]
    simp [torsionCurve, Affine.negY]
  rw [addOrderOf_eq_iff (by norm_num)]
  refine ⟨h6, fun m hm hm0 => ?_⟩
  interval_cases m
  · rw [one_nsmul, torsionPoint]; exact Affine.Point.some_ne_zero _
  · rw [h2]; exact Affine.Point.some_ne_zero _
  · rw [h3]; exact Affine.Point.some_ne_zero _
  · rw [h4]; exact Affine.Point.some_ne_zero _
  · rw [h5]; exact Affine.Point.some_ne_zero _

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

bachetCurveLean 4Formally verified

/-- Bachet's curve `y² = x³ − 2` over `ℚ`: coefficients `(0, 0, 0, 0, −2)`. -/
def bachetCurve : WeierstrassCurve ℚ := ⟨0, 0, 0, 0, -2⟩

Axioms used: propext, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

bachet_duplicationLean 4Proved here from basic factsFormally verified

/-- **Bachet's duplication (1621).** On `y² = x³ − 2`, doubling the point `(3, 5)` with the
tangent (slope `3·3²/(2·5) = 27/10`) gives `(129/100, −383/1000)`: a new rational solution from
an old one. (`(3, 5)` has infinite order — its double is not integral, so by the
Nagell–Lutz theorem it is not torsion — but that argument is not formalised here.) -/
theorem bachet_duplication :
    ∃ (h : bachetCurve.toAffine.Nonsingular 3 5)
      (h' : bachetCurve.toAffine.Nonsingular (129 / 100) (-383 / 1000)),
      Affine.Point.some 3 5 h + Affine.Point.some 3 5 h = Affine.Point.some _ _ h' := by
  have h : bachetCurve.toAffine.Nonsingular 3 5 := by
    rw [Affine.nonsingular_iff]; norm_num [bachetCurve, Affine.Equation, Affine.evalEval_polynomial]
  have h' : bachetCurve.toAffine.Nonsingular (129 / 100) (-383 / 1000) := by
    rw [Affine.nonsingular_iff]; norm_num [bachetCurve, Affine.Equation, Affine.evalEval_polynomial]
  refine ⟨h, h', ?_⟩
  rw [Affine.Point.add_self_of_Y_ne (by simp [bachetCurve, Affine.negY]; norm_num)]
  simp [bachetCurve, Affine.addY, Affine.negY]
  norm_num

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

curve37aLean 4Formally verified

/-- The curve `37a1`: `y² + y = x³ − x`, coefficients `(0, 0, 1, −1, 0)`. It has conductor 37
and rank 1, with `E(ℚ)` generated by `(0, 0)`; it is the first curve in Cremona's tables of
positive rank. -/
def curve37a : WeierstrassCurve ℚ := ⟨0, 0, 1, -1, 0⟩

Axioms used: propext, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

curve_37a_discriminantLean 4Proved here from basic factsFormally verified

/-- The discriminant of `y² + y = x³ − x` is `37`, so the curve has good reduction at every
prime except 37. (Proof: unfold `Δ` in terms of `b₂, b₄, b₆, b₈` and compute.) -/
theorem curve_37a_discriminant : curve37a.Δ = 37 := by
  simp only [curve37a, Δ, b₂, b₄, b₆, b₈]
  norm_num

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

Point counts over $\mathbb{F}_p$ , and an exhaustive kernel check of the Hasse bound for every curve over $\mathbb{F}_5, \mathbb{F}_7, \mathbb{F}_{11}, \mathbb{F}_{13}$ — a finite verification, clearly weaker than Theorem 6:

pointCountLean 4Formally verified

/-- The number of points of `y² = x³ + ax + b` over `𝔽_p`, computed naively: for each `x` and `y`
in `{0, …, p − 1}`, test `y² ≡ x³ + ax + b (mod p)`, then add one for the point at infinity.
(Plain natural-number arithmetic, so that the kernel can evaluate it with `decide`.) -/
def pointCount (p a b : ℕ) : ℕ :=
  ((List.range p).map fun x =>
    ((List.range p).filter fun y => (y * y) % p = (x ^ 3 + a * x + b) % p).length).sum + 1

Axioms used: propextformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

hasse_small_primesLean 4Proved here from basic factsFormally verified

/-- **The Hasse bound, checked exhaustively for small primes.** For `p ∈ {5, 7, 11, 13}` and
every `a, b ∈ 𝔽_p` with `4a³ + 27b² ≠ 0`, the curve `y² = x³ + ax + b` has
`(#E(𝔽_p) − (p + 1))² ≤ 4p`, i.e. `|#E(𝔽_p) − (p + 1)| ≤ 2√p`. The kernel evaluates all
`25 + 49 + 121 + 169` cases (`decide`). This is a finite verification, not Hasse's theorem,
which is not yet in Mathlib. -/
theorem hasse_small_primes : ∀ p ∈ [5, 7, 11, 13], ∀ a < p, ∀ b < p,
    (4 * a ^ 3 + 27 * b ^ 2) % p ≠ 0 → ((pointCount p a b : ℤ) - (p + 1)) ^ 2 ≤ 4 * p := by
  decide

Axioms used: propextformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

Mordell–Weil. Mathlib (work of M. Stoll and collaborators, 2026) contains the descent lemma, the naïve height with its approximate parallelogram law, and the Northcott property for number fields. So both the finiteness of torsion and the descent half of Theorem 4 are formal theorems; what is missing is the weak Mordell–Weil theorem.

torsion_finiteLean 4Applies a library theoremFormally verified

/-- The torsion subgroup of `E(ℚ)` is finite, for every elliptic curve over `ℚ`. Mathlib proves
this (M. Stoll) for any field with the Northcott property, using the naïve height and its
approximate parallelogram law. This applies `WeierstrassCurve.Affine.finite_torsion`. -/
theorem torsion_finite (W : WeierstrassCurve ℚ) [W.IsElliptic] :
    Finite (AddCommGroup.torsion W.toAffine.Point) :=
  Affine.finite_torsion

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

mordell_weil_of_weakLean 4Applies a library theoremFormally verified

/-- **Mordell–Weil, minus the weak theorem.** For an elliptic curve over a number field `K`:
if `2E(K)` has finite index in `E(K)` (the *weak* Mordell–Weil theorem), then `E(K)` is a
finitely generated abelian group. This is the descent half of the classical proof, assembled
from Mathlib's descent theorem `AddCommGroup.fg_of_descent'`, the non-negativity of heights, the
approximate parallelogram law `WeierstrassCurve.Affine.approx_parallelogram_law`, and the
Northcott property of number fields. The weak theorem itself (finiteness of `E(K)/2E(K)`,
proved with the finiteness of class groups and unit theorems) is not yet in Mathlib. -/
theorem mordell_weil_of_weak {K : Type*} [Field K] [NumberField K] [DecidableEq K]
    (W : WeierstrassCurve K) [W.IsElliptic]
    (hweak : (nsmulAddMonoidHom (α := W.toAffine.Point) 2).range.FiniteIndex) :
    AddGroup.FG W.toAffine.Point := by
  obtain ⟨C, hC⟩ := Affine.approx_parallelogram_law (W := W.toAffine)
  exact AddCommGroup.fg_of_descent' hweak (fun P => by
    rw [Affine.Point.naiveHeight_eq_logHeight]; exact Height.logHeight_nonneg _) hC

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

Fermat's Last Theorem for exponents $3$ and $4$ is in Mathlib, by elementary methods:

flt_threeLean 4Applies a library theoremFormally verified

/-- Fermat's Last Theorem for exponent 3: no positive integers satisfy `a³ + b³ = c³`
(Euler, with gaps later filled). This applies Mathlib's `fermatLastTheoremThree`. -/
theorem flt_three : FermatLastTheoremFor 3 := fermatLastTheoremThree

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

flt_fourLean 4Applies a library theoremFormally verified

/-- Fermat's Last Theorem for exponent 4, by Fermat's method of infinite descent (in fact
`a⁴ + b⁴ = c²` has no positive solutions). This applies Mathlib's `fermatLastTheoremFour`.
The general case follows from the modularity of semistable elliptic curves (Wiles,
Taylor–Wiles, 1995) via Frey curves and Ribet's theorem; that proof is not in Mathlib, and a
collaborative project led by Kevin Buzzard to formalise it in Lean began in 2024. -/
theorem flt_four : FermatLastTheoremFor 4 := fermatLastTheoremFour

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ArithmeticGeometry.leanTry it in the Lean web editor

What is and is not formalised. Formalised here or in Mathlib: Weierstrass curves, discriminants, the group law with associativity, the closure computation, finiteness of torsion over number fields, the descent step of Mordell–Weil, the worked examples, finite checks of the Hasse bound, FLT for $n = 3, 4$ . Not formalised: weak Mordell–Weil (hence Mordell–Weil), Nagell–Lutz and Mazur, Hasse's theorem in general and the Weil conjectures, modularity and FLT in general (a large collaborative project led by Kevin Buzzard began formalising FLT in Lean in 2024), and of course BSD, which is a conjecture.

ComputationC

Computing with points

The first experiment implements the group law with exact fractions. It recomputes the table of multiples of $(2, 3)$ on $y^2 = x^3 + 1$ , follows the multiples of Bachet's point $(3, 5)$ — whose denominators grow so that the number of digits divided by $n^2$ settles near a constant, a shadow of the canonical height — and checks associativity on every triple of points of a curve over $\mathbb{F}_{13}$ .

The chord-and-tangent group law in exact arithmeticPythonExact computationExhaustive finite checkComputationally tested

"""The chord-and-tangent group law over the rationals, in exact arithmetic.

We implement addition on a short Weierstrass curve y^2 = x^3 + a x + b with
Fraction arithmetic (None is the point at infinity, the identity). Then:

1. On y^2 = x^3 + 1 the point P = (2, 3) has order 6: its multiples are listed
   and every one has integer coordinates, as the Nagell-Lutz theorem demands
   of torsion points.
2. On Bachet's curve y^2 = x^3 - 2 the point P = (3, 5) has infinite order:
   2P is not integral, so (Nagell-Lutz) 2P is not torsion, hence neither is P.
   The number of digits of the denominators of nP grows roughly like n^2, the
   signature of the canonical height.
3. Associativity, the hard axiom, is checked on every triple of points of a
   curve over the finite field F_13 (exhaustive for that curve).

All arithmetic is exact. The order-6 computation is a complete proof for that
point; the associativity check covers one finite curve only.
"""

from fractions import Fraction
import itertools

def on_curve(P, a, b):
    """True if P is the point at infinity or satisfies y^2 = x^3 + a x + b."""
    if P is None:
        return True
    x, y = P
    return y * y == x ** 3 + a * x + b

def neg(P):
    """The negative of a point: reflect in the x-axis."""
    return None if P is None else (P[0], -P[1])

def add(P, Q, a):
    """Chord-and-tangent addition on y^2 = x^3 + a x + b (b is not needed)."""
    if P is None:
        return Q
    if Q is None:
        return P
    (x1, y1), (x2, y2) = P, Q
    if x1 == x2 and y1 == -y2:
        return None  # vertical line: P + (-P) = O
    if x1 == x2:
        slope = (3 * x1 * x1 + a) / (2 * y1)  # tangent
    else:
        slope = (y2 - y1) / (x2 - x1)  # chord
    x3 = slope * slope - x1 - x2
    y3 = slope * (x3 - x1) + y1  # third intersection point
    return (x3, -y3)  # reflect it

def multiple(n, P, a):
    """n * P for n >= 0, by repeated addition."""
    R = None
    for _ in range(n):
        R = add(R, P, a)
    return R

def order(P, a, limit=20):
    """The order of P if it is at most `limit`, otherwise None."""
    R = P
    for n in range(1, limit + 1):
        if R is None:
            return n
        R = add(R, P, a)
    return None

def is_integral(P):
    """True for the point at infinity or a point with integer coordinates."""
    return P is None or (P[0].denominator == 1 and P[1].denominator == 1)

def add_mod(P, Q, a, p):
    """The same chord-and-tangent formulas over the field Z/pZ (p prime > 3)."""
    if P is None:
        return Q
    if Q is None:
        return P
    (x1, y1), (x2, y2) = P, Q
    if x1 == x2 and (y1 + y2) % p == 0:
        return None
    if x1 == x2:
        slope = (3 * x1 * x1 + a) * pow(2 * y1, -1, p) % p
    else:
        slope = (y2 - y1) * pow(x2 - x1, -1, p) % p
    x3 = (slope * slope - x1 - x2) % p
    y3 = (slope * (x3 - x1) + y1) % p
    return (x3, -y3 % p)

def points_mod(a, b, p):
    """All points of y^2 = x^3 + a x + b over Z/pZ, the point at infinity first."""
    return [None] + [(x, y) for x in range(p) for y in range(p)
                     if (y * y - x ** 3 - a * x - b) % p == 0]

def associativity_failures(points, a, p):
    """Triples (P, Q, R) of points over Z/pZ with (P + Q) + R != P + (Q + R)."""
    bad = []
    for P, Q, R in itertools.product(points, repeat=3):
        if add_mod(add_mod(P, Q, a, p), R, a, p) != add_mod(P, add_mod(Q, R, a, p), a, p):
            bad.append((P, Q, R))
    return bad

def fmt(P):
    """Short text for a point."""
    return "O" if P is None else f"({P[0]}, {P[1]})"

def main():
    F = Fraction
    print("1. y^2 = x^3 + 1, P = (2, 3):")
    P = (F(2), F(3))
    for n in range(1, 7):
        print(f"   {n}P = {fmt(multiple(n, P, 0))}")
    print(f"   order of P = {order(P, 0)}; all multiples integral: "
          f"{all(is_integral(multiple(n, P, 0)) for n in range(1, 7))}")
    print()
    print("2. Bachet's curve y^2 = x^3 - 2, P = (3, 5):")
    a, b = F(0), F(-2)
    Q = (F(3), F(5))
    print(f"   2P = {fmt(multiple(2, Q, a))} (not integral, so P has")
    print("   infinite order by Nagell-Lutz)")
    print("    n   digits of denominator of x(nP)   ratio to n^2")
    R = None
    for n in range(1, 11):
        R = add(R, Q, a)
        assert on_curve(R, a, b)
        d = len(str(R[0].denominator))
        print(f"   {n:2d}   {d:30d}   {d / n ** 2:12.2f}")
    print()
    pts = points_mod(2, 3, 13)
    bad = associativity_failures(pts, 2, 13)
    print(f"3. y^2 = x^3 + 2x + 3 over F_13 has {len(pts)} points; "
          f"associativity fails")
    print(f"   for {len(bad)} of all {len(pts) ** 3} triples.")
    print()
    print("Epistemic status: exact arithmetic. Part 1 is a complete")
    print("computation of the order of (2, 3); that (3, 5) has infinite order")
    print("rests on the Nagell-Lutz theorem, quoted, not proved here. Part 3 is")
    print("exhaustive for one curve over one field; associativity in general is")
    print("a theorem (proved in the references, and in Mathlib).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second experiment counts points of $11a1$ , $37a1$ , $389a1$ and $5077a1$ over $\mathbb{F}_p$ for all $p \lt 1000$ . It checks the Hasse bound, compares the Sato–Tate angles of $37a1$ with the density $\tfrac2\pi \sin^2\theta$ , and recomputes Birch and Swinnerton-Dyer's products $\prod_{p \le X} N_p/p$ .

Point counts mod p: Hasse, Sato-Tate and Birch-Swinnerton-DyerPythonExact computationExhaustive finite checkNumerical approximationComputationally tested

"""Counting points over finite fields: Hasse, Sato-Tate and Birch-Swinnerton-Dyer.

For an elliptic curve E over Q with integer coefficients and a prime p, let
N_p be the number of points of E over F_p (including the point at infinity)
and a_p = p + 1 - N_p. We count points exactly for all p below a bound and

1. check Hasse's bound |a_p| <= 2 sqrt(p) (a theorem; here a finite check);
2. compare the angles theta_p in a_p = 2 sqrt(p) cos(theta_p) with the
   Sato-Tate density (2/pi) sin^2(theta) (a theorem for curves like 37a1,
   proved 2008-2011; here a small sample);
3. repeat Birch and Swinnerton-Dyer's 1960s experiment: the partial products
   prod_{p <= X} N_p / p for curves of rank 0, 1, 2 and 3. Their conjecture
   grew out of the observation that these grow roughly like (log X)^rank.

Ranks and conductors are quoted from Cremona's tables, not computed here.
"""

import math

#: Weierstrass coefficients (a1, a2, a3, a4, a6) and ranks from Cremona's tables.
CURVES = {
    "11a1": ((0, -1, 1, -10, -20), 0),
    "37a1": ((0, 0, 1, -1, 0), 1),
    "389a1": ((0, 1, 1, -2, 0), 2),
    "5077a1": ((0, 0, 1, -7, 6), 3),
}

def primes_below(n):
    """All primes p < n (sieve of Eratosthenes)."""
    sieve = bytearray([1]) * max(n, 2)
    sieve[0] = sieve[1] = 0
    for i in range(2, int(n ** 0.5) + 1):
        if sieve[i]:
            sieve[i * i::i] = bytearray(len(range(i * i, n, i)))
    return [i for i in range(n) if sieve[i]]

def count_points(coeffs, p):
    """N_p: points of y^2 + a1 xy + a3 y = x^3 + a2 x^2 + a4 x + a6 over F_p."""
    a1, a2, a3, a4, a6 = coeffs
    if p == 2:
        return 1 + sum(1 for x in range(2) for y in range(2)
                       if (y * y + a1 * x * y + a3 * y
                           - x ** 3 - a2 * x * x - a4 * x - a6) % 2 == 0)
    # Complete the square: (2y + a1 x + a3)^2 = 4(x^3 + a2 x^2 + a4 x + a6)
    # + (a1 x + a3)^2, and count square roots of the right-hand side.
    roots = [0] * p
    for y in range(p):
        roots[y * y % p] += 1
    total = 1  # the point at infinity
    for x in range(p):
        rhs = 4 * (x ** 3 + a2 * x * x + a4 * x + a6) + (a1 * x + a3) ** 2
        total += roots[rhs % p]
    return total

def trace_of_frobenius(coeffs, p):
    """a_p = p + 1 - N_p."""
    return p + 1 - count_points(coeffs, p)

def sato_tate_mass(lo, hi):
    """Integral of (2/pi) sin^2(t) dt from lo to hi."""
    def F(t):
        return (t - math.sin(t) * math.cos(t)) / math.pi
    return F(hi) - F(lo)

def euler_products(coeffs, checkpoints, primes):
    """prod_{p <= X} N_p / p at each X in checkpoints (sorted)."""
    out, prod, k = [], 1.0, 0
    for p in primes:
        while k < len(checkpoints) and p > checkpoints[k]:
            out.append(prod)
            k += 1
        prod *= count_points(coeffs, p) / p
    while k < len(checkpoints):
        out.append(prod)
        k += 1
    return out

def main():
    primes = primes_below(1000)
    coeffs37 = CURVES["37a1"][0]
    good = [p for p in primes if p != 37]
    ratios = [abs(trace_of_frobenius(coeffs37, p)) / (2 * math.sqrt(p))
              for p in good]
    worst = max(range(len(good)), key=lambda i: ratios[i])
    print(f"37a1: y^2 + y = x^3 - x, all {len(good)} good primes p < 1000")
    print(f"1. Hasse: max |a_p| / (2 sqrt p) = {ratios[worst]:.4f} "
          f"(at p = {good[worst]}); <= 1 every time")
    print()
    print("2. Sato-Tate angles theta_p, a_p = 2 sqrt(p) cos(theta_p):")
    print("   bin (degrees)   observed   Sato-Tate prediction")
    angles = [math.acos(trace_of_frobenius(coeffs37, p) / (2 * math.sqrt(p)))
              for p in good]
    for k in range(6):
        lo, hi = k * math.pi / 6, (k + 1) * math.pi / 6
        seen = sum(1 for t in angles if lo <= t < hi or (k == 5 and t == hi))
        expected = len(angles) * sato_tate_mass(lo, hi)
        print(f"   {30 * k:3d}-{30 * k + 30:3d}       {seen:8d}   {expected:10.1f}")
    print()
    print("3. Birch-Swinnerton-Dyer products prod_{p <= X} N_p / p:")
    checkpoints = [100, 250, 500, 1000]
    print("   curve   rank" + "".join(f"   X = {x:4d}" for x in checkpoints))
    for name, (coeffs, rank) in CURVES.items():
        values = euler_products(coeffs, checkpoints, primes)
        print(f"   {name:7s} {rank:3d}" + "".join(f"  {v:9.1f}" for v in values))
    print()
    print("Epistemic status: the point counts are exact and the Hasse check is")
    print("exhaustive for these primes, but only Hasse's theorem covers all p.")
    print(f"The Sato-Tate table ({len(angles)} angles) and the BSD products are "
          "numerical")
    print("illustrations: the products grow faster for larger rank, as Birch and")
    print("Swinnerton-Dyer saw, but finite data cannot prove or refute the")
    print("conjecture; ranks are quoted from Cremona's tables, not computed.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Be precise about what this shows. The counts are exact, and the Hasse check is exhaustive for these primes — but Hasse's theorem is what covers every prime. The Sato–Tate and BSD tables are numerical illustrations of asymptotic statements; the BSD products in particular converge very slowly and fluctuate (the rank- $1$ column dips between $X = 250$ and $X = 500$ ). The ordering by rank is visible, which is what Birch and Swinnerton-Dyer saw; a proof needs other tools entirely.

Explore

Seeing the curves

The family $y^2 = x^3 + ax + b$ . Move $a$ and $b$ . When $4a^3 + 27b^2 \lt 0$ the real points form two pieces (an "egg" and an unbounded branch); when it is positive, one piece. At $a = b = 0$ the curve acquires a cusp, and at $a = -3$ , $b = 2$ a node: these are the singular cubics excluded by $\Delta \neq 0$ .

Elliptic curves y² = x³ + ax + b

Two real components or one? Find the cusp at a = b = 0 and the node at a = −3, b = 2.

upper half
lower half

aa = −1bb = 1

Trace along xx = 1

upper half: y = 1
lower half: y = −1

Bachet's tangent. The tangent to $y^2 = x^3 - 2$ at $P = (3, 5)$ has slope $\tfrac{27}{10}$ . It meets the curve again at $R = (1.29, 0.383)$ , and reflecting gives $2P = \left(\tfrac{129}{100}, -\tfrac{383}{1000}\right)$ . Trace along the line to see it touch the curve at $P$ and cross it at $R$ .

Doubling a point on Bachet's curve

Move the sliders and trace along the curves to read off values.

y = √(x³ − 2)
y = −√(x³ − 2)
tangent at P

Trace along xx = 1

y = √(x³ − 2): y = undefined here
y = −√(x³ − 2): y = undefined here
tangent at P: y = −0.4

Sato–Tate in a histogram. These are the $120$ values $\cos\theta_p = a_p / (2\sqrt p)$ for $37a1$ and the first $120$ primes $p \neq 37$ (computed by the second experiment). Sato–Tate predicts the semicircle density $\tfrac{2}{\pi}\sqrt{1 - t^2}$ on $[-1, 1]$ : a hump in the middle, thin tails. With only $120$ primes the agreement is rough — evidence, not proof.

Normalised traces a_p / 2√p for the curve 37a1

Show the same data as tallies, pictures, bars or dots, and find the mean, median and mode.

Bin width0.25

Each bar counts the values from its left edge up to, but not including, its right edge.

Exercises

1. Arithmetic geometry and elliptic curves

Warm-upHuman

On $E: y^2 = x^3 + 1$ the point $P = (2, 3)$ has order $6$ , and $2P = (0, 1)$ . What is the order of the point $(0, 1)$ ?

2. Arithmetic geometry and elliptic curves

CoreHuman

Count the points of $E: y^2 = x^3 + 2$ over $\mathbb{F}_7$ , including the point at infinity. (The non-zero squares mod $7$ are $1, 2, 4$ .)

3. Arithmetic geometry and elliptic curves

CoreHuman

For $E: y^2 = x^3 + x + 1$ over $\mathbb{F}_5$ we found $\#E(\mathbb{F}_5) = 9$ , so $a = 5 + 1 - 9 = -3$ . Use $\#E(\mathbb{F}_{q^n}) = q^n + 1 - \alpha^n - \beta^n$ , where $\alpha, \beta$ are the roots of $T^2 - aT + q$ , to find $\#E(\mathbb{F}_{25})$ .

4. Arithmetic geometry and elliptic curves

CoreHuman

Let $E: y^2 = x^3 + 1$ , so $a = 0$ , $b = 1$ and $4a^3 + 27b^2 = 27$ . By the Nagell–Lutz theorem, a torsion point $(x, y) \neq O$ has integer coordinates with $y = 0$ or $y^2 \mid 27$ . List every integer $y$ that is allowed.

5. Arithmetic geometry and elliptic curves

CoreHuman

In the proof of Hasse's theorem we showed $m^2 - a\,mn + q\,n^2 = \deg(m - n\phi) \ge 0$ for all integers $m, n$ , and concluded $a^2 \le 4q$ . Which justification of the last step is correct?

Choose one

A quadratic form that is non-negative on

\Z^2

is non-negative on

\R^2

, so its discriminant

a^2 - 4q

is at most

0

.Because

\deg

is multiplicative:

\deg(\psi\chi) = \deg\psi \cdot \deg\chi

.Because

1 - \phi

is separable.Because

a

is an integer, so

a^2 - 4q

is an integer.

6. Arithmetic geometry and elliptic curves

StretchHuman

Let $E: y^2 = x^3 - 2$ . For which fields $K$ is $E(K)$ not finitely generated? (Choose all that apply.)

Choose all that apply

7. Arithmetic geometry and elliptic curves

CoreFormal

The lesson's Lean theorem chord_third_point has hypotheses h₁ : y₁ ^ 2 = x₁ ^ 3 + a * x₁ + b, h₂ : y₂ ^ 2 = x₂ ^ 3 + a * x₂ + b, hx : x₁ ≠ x₂ and hℓ : y₂ - y₁ = ℓ * (x₂ - x₁). What would go wrong if we deleted hx?

Choose one

The statement would become false: with

x_1 = x_2

and

y_1 = y_2

, hℓ holds for every

\ell

, and for most

\ell

the point

(\ell^2 - 2x_1, \dots)

is not on the curve.Nothing: the hypothesis is never used in the proof.It would still be true, but Lean could not prove it without hx.Lean would reject the statement as ill-typed.

8. Arithmetic geometry and elliptic curves

CoreComputational

Write count_points(p, a, b) returning $\#E(\mathbb{F}_p)$ for $y^2 = x^3 + ax + b$ over $\mathbb{F}_p$ ( $p$ an odd prime), including the point at infinity. Then use it to check the Hasse bound for every curve over $\mathbb{F}_p$ , $p \lt 50$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

9. Arithmetic geometry and elliptic curves

StretchHuman

Which of these statements about elliptic curves $E$ over $\Q$ are proved theorems (as of this lesson)? Choose all that apply.

Choose all that apply

L(E, s)

has a simple zero at

s = 1

, then

E(\Q)

has rank

1

.The rank of

E(\Q)

equals the order of vanishing of

L(E, s)

s = 1

, for every

E

.Every

E/\Q

is modular.The Tate–Shafarevich group of every

E/\Q

is finite.

E(\Q)

is finitely generated.The ranks of elliptic curves over

\Q

are unbounded.

Common misconceptionsH

Common misconceptions

Misconception

"Elliptic curves are ellipses." They are not: an ellipse is a conic (genus $0$ ), an elliptic curve is a cubic of genus $1$ . The name comes from elliptic integrals such as $\int dx/\sqrt{x^3 + ax + b}$ , which arise in computing the arc length of an ellipse; inverting them gives the elliptic functions that parametrise the complex points of $E$ .

Misconception

"The Mordell–Weil theorem gives an algorithm for the rank." The proof is ineffective at one point: the weak theorem bounds $E(\Q)/2E(\Q)$ by the computable $2$ -Selmer group, but the gap between them is measured by Ш, which is not known to be finite in general. No algorithm is known that provably computes the rank of every elliptic curve over $\Q$ ; in practice descent plus point search succeeds, and it would always succeed if Ш were finite.

Misconception

"Wiles proved the Taniyama–Shimura conjecture." Wiles (with Taylor–Wiles) proved modularity of semistable curves, which suffices for Fermat. The full modularity theorem was completed in 2001 by Breuil, Conrad, Diamond and Taylor, building on Wiles's methods.

Misconception

"BSD is known in ranks 0 and 1." What is known (Gross–Zagier, Kolyvagin, plus modularity) is that analytic rank $0$ or $1$ implies algebraic rank equal to it and Ш finite. The exact formula for the leading coefficient is proved only for many individual curves and families, not in general — and nothing comparable is known when the analytic rank is $2$ or more.

Misconception

" $a_p$ is small, so $\#E(\mathbb{F}_p)$ determines nothing interesting." The $a_p$ are anything but noise: they determine $E$ up to isogeny (Faltings), they are the Fourier coefficients of a modular form (Theorem 8), and their statistics follow Sato–Tate. Hasse's bound says only that the fluctuation is of size at most $2\sqrt p$ .

ViewpointsH

Viewpoints

Geometry— Genus decides

For a smooth projective curve $C$ over a number field the genus governs the rational points: genus $0$ — none or a $\mathbb{P}^1$ 's worth; genus $1$ — a finitely generated group (once there is one point); genus $\ge 2$ — finitely many (Faltings). Geometrically, the group law is the identification $E \cong \operatorname{Pic}^0(E)$ , $P \mapsto [P] - [O]$ , given by Riemann–Roch, and " $P + Q + R = O$ iff $P, Q, R$ are collinear" because a line cuts out a divisor linearly equivalent to $3[O]$ . For higher genus the analogue of $E$ is the Jacobian $J(C) = \operatorname{Pic}^0(C)$ , an abelian variety of dimension $g$ into which $C$ embeds — and Faltings's theorem says $C$ meets the finitely generated group $J(K)$ in only finitely many points. See algebraic geometry.

Topology— Tori, circles and the Lefschetz trace formula

Over $\C$ , an elliptic curve is a torus: the Weierstrass function $\wp$ for a lattice $\Lambda \subset \C$ gives a complex-analytic group isomorphism $\C/\Lambda \to E(\C)$ , $z \mapsto (\wp(z), \wp'(z))$ (for the equation $y^2 = 4x^3 - g_2x - g_3$ ). So $E(\C) \cong S^1 \times S^1$ as a group, and $E(\R)$ is a closed subgroup of dimension one: one circle when $\Delta \lt 0$ , two circles when $\Delta \gt 0$ — the components you see in the plot. The Weil conjectures are topology in disguise: Grothendieck's $\ell$ -adic cohomology gives the Lefschetz fixed-point formula $\#E(\mathbb{F}_{q^n}) = \sum_i (-1)^i \operatorname{tr}(\phi^n \mid H^i) = 1 - (\alpha^n + \beta^n) + q^n$ , and $\dim H^1 = 2$ because a torus has two independent loops. See algebraic topology.

Analysis— Elliptic functions and L-functions

Analysis enters twice. First, at the infinite place: $\wp$ is doubly periodic and satisfies $\wp'^2 = 4\wp^3 - g_2\wp - g_3$ , and the periods $\int dx/y$ are the elliptic integrals that gave the subject its name; the real period $\Omega_E$ appears in the BSD formula. Second, globally: $L(E, s) = \sum a_n n^{-s}$ converges for $\operatorname{Re} s \gt \tfrac32$ by Hasse's bound, and its continuation to $s = 1$ — the centre of the critical strip — needs modularity, i.e. it is the Mellin transform of a weight- $2$ cusp form. BSD then asks an analyst's question (the order of a zero) about an algebraist's object (a group). See analytic number theory.

Algebra— Galois representations and the Tate module

For a prime $\ell$ , the $\ell^n$ -torsion $E[\ell^n] \cong (\Z/\ell^n)^2$ over $\overline{\Q}$ , and the inverse limit $T_\ell E \cong \Z_\ell^2$ carries an action of $\operatorname{Gal}(\overline{\Q}/\Q)$ : a Galois representation $\rho_{E,\ell} : \operatorname{Gal}(\overline{\Q}/\Q) \to GL_2(\Z_\ell)$ , unramified at primes $p \nmid N\ell$ with $\operatorname{tr} \rho_{E,\ell}(\operatorname{Frob}_p) = a_p$ and $\det = p$ . Serre's open image theorem (1972) says the image is open for curves without complex multiplication. Modularity is the statement that $\rho_{E,\ell}$ is also attached to a modular form, the first non-abelian case of the Langlands correspondence; Wiles proved it by identifying a deformation ring with a Hecke algebra, " $R = T$ ". See the Langlands programme.

Computation— Cryptography and algorithms

Over a large prime field, the discrete logarithm problem in $E(\mathbb{F}_p)$ — given $P$ and $nP$ , find $n$ — has no known subexponential algorithm for well-chosen curves, so Koblitz and Miller (1985) proposed elliptic-curve cryptography, now standard for key exchange and signatures (see cryptography). The security is conditional on the hardness assumption, and Shor's algorithm would break it on a large quantum computer. Schoof's algorithm (1985) counts $\#E(\mathbb{F}_p)$ in time polynomial in $\log p$ by computing $a_p \bmod \ell$ for small primes $\ell$ from the action of Frobenius on $E[\ell]$ ; H. W. Lenstra's elliptic curve method (1987) factors integers by working in $E(\Z/n)$ as if $n$ were prime. Cremona's tables and the LMFDB list hundreds of thousands of curves with their ranks, generators and $L$ -values.

Logic— Hilbert's tenth problem

Hilbert asked for an algorithm to decide whether a polynomial equation has integer solutions. Matiyasevich (1970), completing work of Davis, Putnam and Robinson, proved that none exists. Over $\Q$ the question is open; Mazur's conjectures on the topology of rational points suggest that $\Z$ is not Diophantine in $\Q$ , which would block the standard approach. Over the ring of integers $\mathcal{O}_K$ of a number field, Poonen and Shlapentokh showed that a negative answer would follow from an elliptic curve over $\Q$ whose rank does not grow over $K$ . Proofs that such curves exist for every number field, and hence that Hilbert's tenth problem is undecidable over every $\mathcal{O}_K$ , were announced in 2024 by Koymans and Pagano and independently by Alpöge, Bhargava, Ho and Shnidman. See computability.

History & global context

History and global context

c. 250 CE. Diophantus of Alexandria's Arithmetica finds rational solutions of quadratic and cubic equations by intersecting with well-chosen lines.
628 and 1150. Brahmagupta composes solutions of $x^2 - Ny^2 = 1$ (his bhāvanā), in effect a group law on a conic; Bhāskara II's chakravala method finds the fundamental solution. Genus- $0$ curves with a group law were thus studied in India long before elliptic curves.
10th century. The congruent number problem appears in Arabic manuscripts; Fibonacci (1225) shows that $5$ is congruent.
1621–1670. Bachet's edition of Diophantus, with his duplication formula for $y^2 = x^3 + c$ ; in its margin Fermat writes his "Last Theorem" and later proves the case $n = 4$ by infinite descent.
18th–19th centuries. Euler treats $n = 3$ ; Abel and Jacobi invert elliptic integrals; Weierstrass introduces $\wp$ .
1901–1928. Poincaré formulates the group law and asks about the rank; Mordell proves finite generation over $\Q$ (1922); Weil extends it to number fields and abelian varieties (1928).
1933–1974. Hasse proves his bound; Weil proves the Riemann hypothesis for curves and states his conjectures (1949); Dwork (1960), Grothendieck's school and Deligne (1974) prove them.
1955–1967. Yutaka Taniyama poses problems at the Tokyo–Nikkō symposium suggesting a link between elliptic curves and modular forms; Goro Shimura sharpens it; Weil (1967) makes it precise with the conductor.
1960s. Bryan Birch and Peter Swinnerton-Dyer formulate their conjecture from EDSAC computations at Cambridge; Mikio Sato and John Tate independently conjecture the $\sin^2$ distribution.
1977–1989. Mazur classifies torsion over $\Q$ ; Coates–Wiles; Faltings proves Mordell's conjecture (1983); Tunnell's criterion (1983); Frey's curve and Ribet's theorem; Gross–Zagier and Kolyvagin.
1994–2001. Andrew Wiles, with Richard Taylor, proves modularity of semistable curves and Fermat's Last Theorem; Breuil, Conrad, Diamond and Taylor complete modularity.
2008–present. The Sato–Tate conjecture (Clozel, Harris, Shepherd-Barron, Taylor; Barnet-Lamb, Geraghty, Harris, Taylor); Bhargava and Shankar's average-rank theorems; Yuan, Zhang and Zhang's general Gross–Zagier formula (2013); Tian Ye's work on congruent numbers.

Rational points on cubic curves

Chords, tangents and a group

Definitions

Examples and non-examples

Central results

The landscape: what is known, what is open

Elliptic curves in Lean and Mathlib

Computing with points

Seeing the curves

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading