Riemann hypothesis for varieties over finite fields (Deligne)

Open

WeilConjectures.riemann_hypothesis

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

algebraic-geometrynumber-theoryzeta-function

Let $k=\mathbb F_q$ be a finite field with $q$ elements, of characteristic $p$ , and let $X$ be a non-singular projective variety of dimension $n$ over $k$ , i.e. $f: X\to\operatorname{Spec}k$ is smooth of relative dimension $n$ , geometrically irreducible and projective. Let $N_m=\#X(\mathbb F_{q^m})$ and $Z(X,T)=\exp\big(\sum_{m\ge1}N_mT^m/m\big)\in\mathbb Q[[T]]$ . Then there are integer polynomials $P_0,\dots,P_{2n}\in\mathbb Z[T]$ and finite multisets $\{\alpha_{ij}\}_j$ of nonzero complex numbers with

Z(X,T)\cdot P_0(T)P_2(T)\cdots P_{2n}(T)=P_1(T)P_3(T)\cdots P_{2n-1}(T),

$P_0(T)=1-T$ , $P_{2n}(T)=1-q^nT$ , and $P_i(T)=\prod_j(1-\alpha_{ij}T)$ in $\mathbb C[T]$ for $1\le i\le 2n-1$ ;

and moreover Riemann hypothesis: $|\alpha_{ij}|=q^{i/2}$ for all $1\le i\le 2n-1$ and all $j$ .

This is part 3 of the Weil conjectures, proved by Deligne (1974). It implies that the zeros of $P_k(q^{-s})$ lie on the line $\operatorname{Re}s=k/2$ .

Formalization Note The finite field is a type k with [Field k] [Finite k] [CharP k p], $q$ = Nat.card k; $\mathbb F_{q^m}$ is FiniteField.Extension k p m; $N_m$ counts $k$ -morphisms $\operatorname{Spec}\mathbb F_{q^m}\to X$ ; $Z(X,T)$ is zetaFunction p f. Projectivity is a closed immersion into projectiveSpace k N over $k$ .

Preamble

import Mathlib
import Definitions.Def_WeilConjectures_projectiveSpace
import Definitions.Def_WeilConjectures_zetaFunction

open AlgebraicGeometry CategoryTheory Polynomial

Formal statement

namespace WeilConjectures

theorem riemann_hypothesis (p : ℕ) [Fact p.Prime] (k : Type) [Field k] [Finite k] [CharP k p]
    (n : ℕ) (X : Scheme.{0}) (f : X ⟶ Spec (.of k))
    [SmoothOfRelativeDimension n f] [GeometricallyIrreducible f]
    (hproj : IsProjectiveOver k f) :
    ∃ (P : ℕ → ℤ[X]) (α : ℕ → Multiset ℂ),
      zetaFunction p f *
          (∏ i ∈ (Finset.range (2 * n + 1)).filter Even,
            ((P i).map (Int.castRingHom ℚ) : PowerSeries ℚ)) =
        ∏ i ∈ (Finset.range (2 * n + 1)).filter Odd,
            ((P i).map (Int.castRingHom ℚ) : PowerSeries ℚ) ∧
      P 0 = 1 - Polynomial.X ∧
      P (2 * n) = 1 - C ((Nat.card k : ℤ) ^ n) * Polynomial.X ∧
      (∀ i, 1 ≤ i → i ≤ 2 * n - 1 →
        (P i).map (Int.castRingHom ℂ) = ((α i).map fun a => 1 - C a * Polynomial.X).prod ∧
        ∀ a ∈ α i, a ≠ 0) ∧
      (∀ i, 1 ≤ i → i ≤ 2 * n - 1 → ∀ a ∈ α i,
        ‖a‖ = (Nat.card k : ℝ) ^ ((i : ℝ) / 2)) := by sorry

end WeilConjectures

Source

Wikipedia, "Weil conjectures", https://en.wikipedia.org/wiki/Weil_conjectures (PDF snapshot supplied by the proposer, 14 pp.), section "Statement of the Weil conjectures", items 1 and 3; section "Deligne's first proof of the Riemann hypothesis conjecture"

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