Hasse's theorem: point counts of elliptic curves

Proved

WeilConjectures.hasse_elliptic_curve

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryelliptic-curvesnumber-theory

Let $E$ be an elliptic curve over a finite field $k=\mathbb F_q$ , given by a Weierstrass equation with nonzero discriminant. Then there are complex numbers $\alpha,\beta$ with $\beta=\bar\alpha$ and $|\alpha|=|\beta|=\sqrt q$ such that for every $m\ge1$

\#E(\mathbb F_{q^m})=1-\alpha^m-\beta^m+q^m.

Equivalently $\zeta(E,s)=\dfrac{(1-\alpha q^{-s})(1-\beta q^{-s})}{(1-q^{-s})(1-q^{1-s})}$ . This is the first non-trivial case of the Weil conjectures, proved by Hasse.

Formalization Note $E$ is a WeierstrassCurve k with [E.IsElliptic]; $E(\mathbb F_{q^m})$ is the type of points (affine points together with the point at infinity) of the base change of $E$ to FiniteField.Extension k p m.

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem hasse_elliptic_curve (p : ℕ) [Fact p.Prime] (k : Type) [Field k] [Finite k] [CharP k p]
    (E : WeierstrassCurve k) [E.IsElliptic] :
    ∃ α β : ℂ, β = (starRingEnd ℂ) α ∧ ‖α‖ = Real.sqrt (Nat.card k) ∧ ‖β‖ = Real.sqrt (Nat.card k) ∧
      ∀ (m : ℕ) [NeZero m],
        (Nat.card (E.baseChange (FiniteField.Extension k p m)).toAffine.Point : ℂ) =
          1 - α ^ m - β ^ m + (Nat.card k : ℂ) ^ m := by sorry

end WeilConjectures

Source

Wikipedia, "Weil conjectures", https://en.wikipedia.org/wiki/Weil_conjectures (PDF snapshot supplied by the proposer, 14 pp.), section "Examples", subsection "Elliptic curves"

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph