Hasse's theorem: $|q+1-\#E(\mathbb{F}_q)| \le 2\sqrt{q}$ for elliptic curves over finite fields

Open

BSD.hasse_bound

by korbonits · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

birch-swinnerton-dyerelliptic-curvesfinite-fieldsnumber-theory

Let $\mathbb{F}$ be a finite field with $q$ elements and let $E$ be an elliptic curve over $\mathbb{F}$ , given by a Weierstrass equation with non-zero discriminant. Let $\#E(\mathbb{F})$ denote the number of $\mathbb{F}$ -rational points of $E$ , including the point at infinity. Then

\bigl(q + 1 - \#E(\mathbb{F})\bigr)^2 \le 4q,

equivalently $|q + 1 - \#E(\mathbb{F})| \le 2\sqrt{q}$ .

This is Hasse's theorem (1933), the Riemann hypothesis for elliptic curves over finite fields. The integer $a = q + 1 - \#E(\mathbb{F})$ is the trace of Frobenius, and the inequality says that the roots of $1 - aT + qT^2$ have absolute value $q^{-1/2}$ .

Formalization Note $E$ is a WeierstrassCurve F with [E.IsElliptic]; $\#E(\mathbb{F})$ is Nat.card E.toAffine.Point, where Mathlib's type of points of the affine model already includes the point at infinity (the constructor zero). The field is arbitrary finite (any characteristic, including 2 and 3), with $q$ given by Nat.card F.

Preamble

import Mathlib

Formal statement

namespace BSD
theorem hasse_bound {F : Type*} [Field F] [Finite F] (E : WeierstrassCurve F) [E.IsElliptic] :
    ((Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point) ^ 2 ≤ 4 * Nat.card F := by sorry
end BSD

Source

J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer 2009, Chapter V, Theorem 1.1 (Hasse); H. Hasse, Zur Theorie der abstrakten elliptischen Funktionenkörper I–III, J. Reine Angew. Math. 175 (1936).

View graph

Hasse's theorem: ∣q+1−#E(Fq)∣≤2q|q+1-\#E(\mathbb{F}_q)| \le 2\sqrt{q}∣q+1−#E(Fq​)∣≤2q​ for elliptic curves over finite fields

Hasse's theorem: $|q+1-\#E(\mathbb{F}_q)| \le 2\sqrt{q}$ for elliptic curves over finite fields