Faltings’ Theorem Formalized

Take this equation:

$$y^2 = x(x-1)(x-2)(x-5)(x-6)$$

Let’s hunt for solutions where $x$ and $y$ are both rational numbers. Some come for free. Setting $x = 0, 1, 2, 5$ or $6$ makes the right side zero, so $y = 0$.

Try $x = 3$. The right side is $3 × 2 × 1 × (−2) × (−3) = 36$, so $y = \pm6$. Try $x = 10$. The right side is $10 × 9 × 8 × 5 × 4 = 14,400$, which is $120^2$, so $y = \pm 120$.

That makes nine solutions. Geometers also count one “point at infinity,” for ten in total. Now keep looking. A computer search through every reduced fraction having denominator up to 300 finds nothing new.

That is not bad luck. Mathematicians have proved that these ten points are the only ones. And this curve is not unusual: some curves of the same kind have hundreds of rational points, with the current record at $642$. Yet every one of them has only finitely many.

Why? If a curve can have $642$ rational points, what stops it from having $643$, and then infinitely many?

That is the question Louis Mordell raised in 1922. Gerd Faltings answered it in 1983, in one of the landmark proofs of twentieth-century mathematics. Today, Axiom announces the first complete, machine-verified proof of Faltings’ theorem, following the proof of Paul Vojta as simplified by Enrico Bombieri.

The answer depends on one number attached to every curve: its genus. Allow $x$ and $y$ to be complex numbers, and the solutions form a surface. The genus counts its holes. A sphere has genus $0$, a doughnut genus $1$, a two-holed pretzel genus $2$.

The number of holes, a purely geometric fact, turns out to control the arithmetic.

On the circle $x^2 + y^2 = 1$, Pythagorean triples are in perfect correspondence with rational points. For example, the triple $3, 4, 5$ gives $(\frac{3}{5}, \frac{4}{5})$. There are infinitely many more.

On the curve $y^2 = x^3 − 2$, an example of an elliptic curve, there is the point $(3, 5)$. Draw the tangent line there, and it meets the curve again at a new rational point, $(\frac{129}{100},\frac{383}{1000})$. Repeat the trick and new points keep coming, forever. Mordell proved in 1922 that on such elliptic curves, every rational point can be built this way from finitely many starting points.

Then Mordell conjectured that at genus 2 the supply dries up for good. Faltings proved him right. Here is the theorem in its general form:

Faltings’ theorem. Let $K$ be a number field.  If $C$ is a smooth, projective, geometrically irreducible curve over $K$ of genus at least $2$, then $C$ has only finitely many points with coordinates in $K$.

A number field is a finite extension of the rationals, such as all numbers $a + b\sqrt2$ with $a$ and $b$ rational. So the theorem holds well beyond fractions.

One striking consequence concerns Fermat’s equation. The curve $x^n + y^n = 1$ has genus $\frac{(n − 1)(n − 2)}{2}$, which is at least $3$ once $n \pm 4$. So for each such $n$, Faltings’ theorem says there are only finitely many solutions in fractions. That was a decade before Andrew Wiles proved that there are no nontrivial ones at all (as predicted by Fermat).

In 1929 Carl Ludwig Siegel proved an easier cousin of Mordell’s conjecture. On any curve of genus at least 1, there are only finitely many points with integer coordinates.

The curve $y^2 = x^3 − 2$ shows how different the two questions are. Its only integer solution is $x = 3, y = \pm5$: the number 26 is the only integer squeezed between a square $25$ and a cube $27$. Yet we just saw that its rational points never run out.

Why are integer points easier? An integer point cannot hide its size in a denominator. A huge integer solution would force certain algebraic numbers to have unusually good rational approximations. Siegel combined the theory of Diophantine approximation, which forbids this, with the Mordell–Weil theorem, André Weil’s 1928 extension of Mordell’s result on elliptic curves.

Rational points have no such leash. Large denominators let them creep up anywhere on the curve, so Siegel’s argument has nothing to grip. Mordell’s question, which asks about all rational points, resisted for another 54 years.

That contrast is the key to the story below. Vojta’s breakthrough was to make Siegel’s style of argument work for rational points after all.

To prove a set is finite, number theorists measure how complicated each point is. The tool is the height. For a fraction $\frac{p}{q}$ in lowest terms, the height is the larger of $|p|$ and $|q|$.

So $3$ has height $3$, and $\frac{129}{100}$ has height $129$. The key fact is simple: there are only finitely many fractions below any given height. Prove that a curve’s rational points have bounded height, and you have proved there are finitely many of them.

On a genus $1$ curve, heights can grow without bound, and in a very regular way. Here are the first few points built from $(3, 5)$ on $y^2 = x^3 − 2$:

By 8P the numerator has 38 digits. The digit count grows roughly like the square of the multiple. That is no accident. A refined version, the Néron–Tate height, is exactly quadratic. It turns the rational points into something like lattice points in ordinary space, with height playing the role of squared length.

A curve of genus $2$ or more has no such group law of its own. But it sits inside a larger object, its Jacobian, which does. There, the rational points again form a lattice, and heights again measure length. The curve’s own points are a thin slice of that lattice. Faltings’ theorem says the slice contains only finitely many of them.

There is more than one proof of Faltings’ theorem, and none of them is easy. We followed the route opened by Vojta and simplified by Bombieri.

Faltings did not attack the curve head-on. He proved two other major conjectures about abelian varieties, the higher-dimensional cousins of elliptic curves, and deduced Mordell’s conjecture from them. His proof draws on:

• the Shafarevich conjecture and the Tate conjecture for abelian varieties
• $\ell$-adic Galois representations
• moduli spaces of abelian varieties and the Faltings height
• finite flat group schemes
• Parshin’s trick, which turns a question about one curve into a question about many abelian varieties

The work earned Faltings the Fields Medal in 1986.

Around 1990, Paul Vojta found a completely different proof. It returns to the spirit of Siegel’s approximation methods, which seemed powerless against rational points.

Vojta works on the product of the curve with itself, which is a surface. On this surface, he builds a carefully chosen auxiliary function that vanishes heavily at a pair of rational points. Weighing the function’s size against its vanishing yields Vojta’s inequality, a strong constraint on how rational points can sit in the Jacobian’s lattice.

To build that function, Vojta used Arakelov theory. The idea is a beautiful analogy. The integers behave like the points of a curve, with each prime as a point. Arakelov theory completes that “curve” by adding a point at infinity, handled with complex analysis. Heights then become intersection numbers, as in classical geometry. Vojta’s argument leans on:

• arithmetic surfaces and Arakelov intersection theory
• Hermitian line bundles
• the arithmetic Riemann–Roch theorem of Gillet and Soulé
• analytic torsion

Faltings soon reworked Vojta’s argument. Building on that, Enrico Bombieri in 1990 gave a far more elementary version in a paper titled “The Mordell Conjecture Revisited.” He removed Arakelov theory entirely.

In its place, Bombieri used classical heights and Siegel’s lemma. Siegel’s lemma is a refined pigeonhole principle: a linear system with more unknowns than equations has a solution in small integers. That is enough to build the auxiliary function by hand.

The endgame then fits in a picture. Group the curve’s rational points in the Jacobian lattice by direction, into finitely many narrow cones. Within one cone, two forces squeeze the points:

• Mumford’s gap principle pushes them apart: each large point is at least about twice as long as the one before.
• Vojta’s inequality pulls them together: beyond a certain size, one point cannot be too much longer than another.

Points that must keep doubling, yet cannot grow too far apart, can only be finitely many. Do this for each cone, and the curve has finitely many rational points.

“Elementary” here is relative. Bombieri’s proof is still a graduate-level tour of algebraic geometry. It is the Bombieri–Vojta proof that Axiom has formalized.

Even the gentler path rests on a mountain of modern algebraic geometry. Before a computer can check a single step of Bombieri’s argument, every one of these objects must be defined precisely and connected to the others.

Foundations. General scheme theory: fiber products; base change across field extensions and rings of integers; morphisms that are proper, smooth, flat, finite and étale.

Curves. Smooth projective curves over arbitrary bases; the canonical sheaf; the Riemann–Roch theorem; Hurwitz’s theorem; intersection pairings on surfaces.

Embeddings and heights. Ample and very ample invertible sheaves; projective embeddings; Weil heights and Néron–Tate heights; the interplay between geometric intersection numbers and arithmetic heights.

Jacobians. The Picard functor; the construction of the Jacobian variety; the Abel–Jacobi map embedding a curve in its Jacobian; the quadratic nature of the canonical height; the Mordell–Weil theorem.

Only on top of all this come the parts specific to the proof: Siegel’s lemma, the auxiliary sections on the product surface, Mumford’s gap principle and Vojta’s inequality.

That list is intimidating, and it should be. Building it from scratch for one theorem would take years. This is why formalizing the Stacks Project first was such a large win.

We built our formalization of the Stacks Project as a general-purpose library for modern algebraic geometry, not as scaffolding for one result. Its definitions were designed to compose cleanly across domains: sheaf cohomology, derived categories, smoothness, properness, Picard schemes.

That design paid off when our team moved from the Weil conjectures, set over finite fields, to Faltings’ theorem, set over number fields.

• Our scheme theory works over arbitrary base schemes rather than assuming an algebraically closed field. Moving between a number field, its completions, its ring of integers and its finite residue fields required no refactoring.
• The sheaf cohomology, Euler characteristic and Riemann–Roch interfaces built for the Weil conjectures carried over directly. They control global sections of line bundles on curves and their products, exactly what the auxiliary construction needs.
• The infrastructure for group schemes, Picard functors and abelian varieties served as a shared backbone for both projects.

So instead of spending months re-proving basic facts about proper morphisms, Kähler differentials or ample line bundles, we could focus on the arithmetic heart of the Bombieri–Vojta argument.  All in all, our formalization of the Bombieri–Vojta proof of Mordell’s conjecture contains roughly 110,000 lines of proof-specific Lean code, building on library modules containing roughly 6,400,000 lines from our Stacks Project formalization.  Our formalization of Mordell’s conjecture is available at github.com/AxiomMath/Mordell.

Formalizing a famous theorem has often meant building a tall, narrow tower aimed at one final statement. Definitions get trimmed to what the target needs, and the result is hard to build on.

We take a different view: formal mathematics should compound, the way good software infrastructure does. Each general layer makes the next result faster and safer to reach. Formalize the Stacks Project at full generality, and the Weil conjectures and Faltings’ theorem follow in quick succession. Each milestone in turn enriches the library for the next. This is a modern-day manifestation of Alexander Grothendiek’s “rising sea” philosophy of how to approach difficult mathematics.

Mordell asked his question about curves like the one at the top of this post more than a century ago. Its answer now rests on a foundation that a computer has checked line by line, and that the next proof can stand on.

• Enrico Bombieri, The Mordell Conjecture Revisited (1990), the simplified proof we followed.
• Marc Hindry and Joseph Silverman, Diophantine Geometry: An Introduction, Part E, a textbook account of Bombieri’s proof.
• Niven Achenjang, notes on Vojta’s approach, a readable overview of the gap principle and Vojta’s inequality.
• William McCallum, Introduction to Explicit Chabauty Methods, which determines all rational points on our opening curve.
• Many Rational Points on a Genus-2 Curve, on the 642-point record curve.
• Github: https://github.com/AxiomMath/Mordell