Esquisse d'un Programme I: Dessins d'Enfants and the Faithfulness of the Galois ActionResearch Paper
## Motivation
In *Esquisse d'un Programme* (1984), Alexandre Grothendieck describes a discovery that reorganised his mathematical interests: a finite oriented combinatorial map drawn on a surface — a **dessin d'enfant**, a child's drawing — determines canonically a smooth projective algebraic curve together with a map to the projective line ramified only above $0$, $1$ and $\infty$, and that curve and map are defined over the field $\overline{\mathbb{Q}}$ of algebraic numbers (Esquisse, §3, pp. 14–16 of the French text). Consequently the absolute Galois group $\Gamma = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ acts on these purely combinatorial objects; in the spherical case, where the structural map is a rational function $f(z) = P(z)/Q(z)$, the action of $\gamma \in \Gamma$ is obtained simply by applying $\gamma$ to the coefficients of $P$ and $Q$. Grothendieck states in §2 (p. 9) that the resulting outer action of $\Gamma$ on the profinite fundamental group $\hat{\pi}_{0,3}$ of $\mathbb{P}^1 \smallsetminus \{0,1,\infty\}$ is **faithful**, and in §3 that the theorem of Belyi, announced at the 1978 Helsinki congress, is what makes the dictionary between combinatorics and arithmetic exact.
Timeline of the results this mission formalizes. Belyi (1979, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR) proved that a smooth projective curve over $\mathbb{C}$ is defined over a number field if and only if it admits a map to $\mathbb{P}^1$ unramified outside $\{0,1,\infty\}$; the "only if" half is an explicit construction with polynomials over $\mathbb{Q}$. Grothendieck (1984) drew the consequence that $\Gamma$ acts on dessins and asserted faithfulness of the action on $\hat{\pi}_{0,3}$. Lenstra, in an appendix to L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants* (LMS Lecture Notes 200, CUP 1994), showed that the action is already faithful on the much smaller class of **plane trees**, equivalently on **Shabat polynomials**. That tree-level statement is the goal of this mission, because it is the sharpest form of faithfulness that can be stated without first building the theory of étale fundamental groups.
## Setting
Work over $\overline{\mathbb{Q}}$, realized as the algebraic closure of $\mathbb{Q}$, and write $\Gamma$ for its group of field automorphisms fixing $\mathbb{Q}$ pointwise.
A nonconstant polynomial $P$ over a field $K$ is a **Belyi polynomial** (classically a *Shabat polynomial*) when every critical value of $P$ lies in $\{0,1\}$: for every $z \in K$ with $P'(z) = 0$ one has $P(z) = 0$ or $P(z) = 1$. Over an algebraically closed field of characteristic zero this says exactly that $P$, viewed as a degree-$n$ map $\mathbb{P}^1 \to \mathbb{P}^1$, is unramified outside the fibres over $0$, $1$ and $\infty$. The associated dessin is the preimage $P^{-1}([0,1])$, a plane tree with $n$ edges whose vertices are the points above $0$ and $1$, with vertex orders equal to the multiplicities of the corresponding roots of $P$ and of $P - 1$.
Two Belyi polynomials define the same dessin exactly when they are **affinely equivalent**: $Q = P(aX + b)$ for some $a \neq 0$ and some $b$. The target coordinate is already rigidified by the normalisation of the critical values to $\{0,1\}$; only the source coordinate remains free.
The group $\Gamma$ acts coefficientwise: $P^{\gamma}$ is the polynomial obtained from $P$ by applying $\gamma$ to each coefficient. This is exactly the action described in §3 of the Esquisse. It sends Belyi polynomials to Belyi polynomials, and it descends to an action on affine equivalence classes, i.e. on dessins.
## Formalization targets
### Goal — faithfulness of the Galois action on plane trees
$$\forall\, \gamma \in \Gamma,\quad \gamma \neq 1 \ \Longrightarrow\ \exists\, P \in \overline{\mathbb{Q}}[X] \text{ a Belyi polynomial with } P \not\sim_{\mathrm{aff}} P^{\gamma}.$$
Equivalently: no nontrivial element of the absolute Galois group fixes every plane tree. This is the weakest stable form of the faithfulness assertion in the Esquisse: it fixes no degree, no genus and no tree, asserting only that some dessin is moved.
### Supporting targets
- **Belyi's theorem, polynomial form.** For every finite set $S \subseteq \overline{\mathbb{Q}}$ there is a Belyi polynomial $f \in \mathbb{Q}[X]$ with $f(S) \subseteq \{0,1\}$.
- **Descent to $\overline{\mathbb{Q}}$.** Every Belyi polynomial over $\mathbb{C}$ is affinely equivalent to one whose coefficients are algebraic over $\mathbb{Q}$.
- **Galois equivariance and invariants.** $P^{\gamma}$ is again a Belyi polynomial of the same degree, and the multiplicity of $z$ as a root of $P - c$ equals the multiplicity of $\gamma(z)$ as a root of $P^{\gamma} - \gamma(c)$: the dessin's vertex and face orders are Galois invariants.
- **Finiteness of the orbit.** The set of Galois conjugates of a fixed polynomial over $\overline{\mathbb{Q}}$ is finite — the "visibly finite number of conjugates" of §3.
- **Finiteness in a fixed degree.** For each $n$ there are only finitely many monic Belyi polynomials of degree $n$ over $\overline{\mathbb{Q}}$ with vanishing subleading coefficient.
- **Separation.** For every $\alpha \in \overline{\mathbb{Q}}$ there is a Belyi polynomial $P$ such that every $\gamma$ fixing the class of $P$ fixes $\alpha$. The goal follows from this by taking $\alpha$ with $\gamma(\alpha) \neq \alpha$.
## Significance
The result itself. Faithfulness turns the combinatorics of finite maps into a faithful representation of $\Gamma$: every nontrivial automorphism of $\overline{\mathbb{Q}}$ is detected by a finite tree, so invariants of dessins (degree, valency lists, monodromy group, field of moduli) are in principle a complete set of tools for distinguishing Galois elements. It is also the entry point to the anabelian programme described in §3 of the Esquisse, since the same statement expresses that $\Gamma$ embeds into the outer automorphism group of $\hat{\pi}_{0,3}$.
Formalizing it. Belyi's theorem and the faithfulness of the Galois action on trees are both established results. Mathlib at the environment revision of this mission contains no declaration mentioning Belyi maps or dessins d'enfants, and no étale fundamental group, so both statements have to be built from the polynomial and Galois-theoretic libraries. What this mission produces is a formal version of the combinatorial half of the dictionary, in a form that avoids scheme theory entirely: everything is phrased with polynomials over $\overline{\mathbb{Q}}$ and $\mathbb{C}$, so the development rests only on Mathlib's existing polynomial, field theory and Galois theory libraries.
## Difficulty
The naive attack on the goal — exhibit one tree and one Galois element moving it — does not scale: the statement quantifies over all $\gamma \neq 1$, and $\Gamma$ has no accessible presentation. The real work is the separation statement, which demands, for an arbitrary algebraic number $\alpha$, a tree whose isomorphism class remembers $\alpha$; the construction must control both the existence of a Belyi polynomial with prescribed arithmetic and the rigidity that makes affine equivalence classes finite. Belyi's theorem in polynomial form is itself an induction on the degree of the field of definition of the critical values, and each step changes the polynomial, so bookkeeping of critical values through composition is the bulk of the formal proof. The descent statement over $\mathbb{C}$ is not a formal manipulation either: it needs the finiteness of the set of Belyi polynomials of a given degree up to affine equivalence, which is where the combinatorial classification enters.
## Formalization scope
Conventions fixed in the Lean development, and not to be re-litigated by solvers:
- $\overline{\mathbb{Q}}$ is `AlgebraicClosure ℚ`, and $\Gamma$ is its group of $\mathbb{Q}$-algebra automorphisms.
- "Belyi polynomial" means: positive degree, and every root of the formal derivative is sent to $0$ or $1$. Critical values are required to lie *in* $\{0,1\}$, not to be exactly $\{0,1\}$; degenerate cases such as $X^n$ (one finite critical value) are therefore included.
- Being a Belyi polynomial is stated over an arbitrary field but is only intended over algebraically closed fields ($\overline{\mathbb{Q}}$, $\mathbb{C}$), where quantifying over the field's own elements captures all critical points.
- Dessin isomorphism is modelled as affine equivalence of the source variable only; conjugating by an affine map of the target is excluded, since the target is rigidified by $\{0,1\}$.
- The Galois action is coefficientwise application of $\gamma$.
Trivialization is ruled out as follows: the goal asserts the *existence* of a moved Belyi polynomial for each nontrivial $\gamma$, with the nondegeneracy `0 < deg P` built into the definition, so no constant or empty witness satisfies it, and no hypothesis of the goal is vacuous ($\gamma \neq 1$ is satisfiable).
A complete development needs: critical values and their behaviour under composition of polynomials; the classification of Belyi polynomials of fixed degree up to affine equivalence; Galois descent for a finite set of polynomials stable under conjugation; and, for the descent target, the identification of the coefficients of a Belyi polynomial over $\mathbb{C}$ as algebraic numbers. All of these are reusable outside this mission. Contributions of general polynomial-ramification infrastructure are welcome, as are alternative formalizations of the same statements over a general algebraically closed field of characteristic zero.
## Selected references
- A. Grothendieck, *Esquisse d'un Programme* (1984), published in L. Schneps and P. Lochak (eds.), *Geometric Galois Actions 1*, LMS Lecture Note Series 242, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511758874
- G. V. Belyi, *On Galois extensions of a maximal cyclotomic field*, Izv. Akad. Nauk SSSR Ser. Mat. 43 (1979), 267–276. English translation: Math. USSR-Izv. 14 (1980), 247–256. https://doi.org/10.1070/IM1980v014n02ABEH001096
- L. Schneps (ed.), *The Grothendieck Theory of Dessins d'Enfants*, LMS Lecture Note Series 200, Cambridge University Press, 1994. https://doi.org/10.1017/CBO9780511569302
- S. K. Lando and A. K. Zvonkin, *Graphs on Surfaces and Their Applications*, Encyclopaedia of Mathematical Sciences 141, Springer, 2004. https://doi.org/10.1007/978-3-540-38361-1
8 thms2 active usersReviewed
Captain: korbonits
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