Numerical verification of the Riemann hypothesis up to height 3.29 * 10^9

Open

TaoFivePrimes.riemann_verified

by Jack McCarthy · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorynumerical-verificationriemann-zeta

With $T_0 := 3.29 \times 10^9$ , every zero of the Riemann zeta function $\zeta$ in the strip $\{s : 0 < \Re(s) < 1,\ 0 \le \Im(s) \le T_0\}$ lies on the critical line $\Re(s) = 1/2$ , and there are at most $10^{10}$ such zeroes.

This is Theorem 1.5 of Tao's paper, obtained independently by van de Lune, Wedeniwski, Gourdon and Platt. Tao deliberately uses the conservative value $T_0 = 3.29 \times 10^9$ , verified by four independent computations, rather than the larger heights available.

Finiteness is asserted explicitly and is not redundant. In Lean, Set.ncard evaluates to $0$ on an infinite set, so the cardinality bound ncard ≤ 10 ^ 10 alone would hold vacuously for an infinite zero set. The conjunction with Set.Finite is what makes the count meaningful.

Like Theorem 1.6, this is a quoted large-scale computation, included for graph fidelity.

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem riemann_verified :
    (∀ s : ℂ, riemannZeta s = 0 → 0 < s.re → s.re < 1 → 0 ≤ s.im →
        s.im ≤ 3.29 * 10 ^ 9 → s.re = 1 / 2) ∧
      {s : ℂ | riemannZeta s = 0 ∧ 0 < s.re ∧ s.re < 1 ∧ 0 ≤ s.im ∧
        s.im ≤ 3.29 * 10 ^ 9}.Finite ∧
      {s : ℂ | riemannZeta s = 0 ∧ 0 < s.re ∧ s.re < 1 ∧ 0 ≤ s.im ∧
        s.im ≤ 3.29 * 10 ^ 9}.ncard ≤ 10 ^ 10 := by
  sorry

end TaoFivePrimes

Source

Terence Tao, https://arxiv.org/abs/1201.6656, Theorem 1.5 (p. 7); numerical verifications by van de Lune, Wedeniwski, Gourdon, and Platt

Read-back

What the Lean code literally says, in plain math · claude-opus-5

The declaration asserts a single three-part conjunction about the Riemann zeta function $\zeta$ — specifically Mathlib's total function $\zeta : \mathbb{C} \to \mathbb{C}$ , which agrees with $\sum_{n \ge 1} n^{-s}$ where that series converges and is its analytic continuation elsewhere. Throughout, $s$ ranges over complex numbers, $\operatorname{Re} s$ and $\operatorname{Im} s$ are its real and imaginary parts, and the height bound is the exact real number $3.29 \cdot 10^{9} = 3{,}290{,}000{,}000$ . Define the region

R \;=\; \{\, s \in \mathbb{C} \;:\; 0 < \operatorname{Re} s < 1,\ \ 0 \le \operatorname{Im} s \le 3.29 \cdot 10^{9} \,\}

and the zero set

Z \;=\; \{\, s \in \mathbb{C} \;:\; \zeta(s) = 0 \ \wedge\ 0 < \operatorname{Re} s \ \wedge\ \operatorname{Re} s < 1 \ \wedge\ 0 \le \operatorname{Im} s \ \wedge\ \operatorname{Im} s \le 3.29 \cdot 10^{9} \,\} \;=\; \{\, s \in R : \zeta(s) = 0 \,\}.

The same set $Z$ is written out verbatim in both of the last two conjuncts, and the hypotheses of the first conjunct are exactly its defining conditions, so all three parts speak about one and the same collection of points.

First conjunct. For every complex number $s$ : if $\zeta(s) = 0$ , and $0 < \operatorname{Re} s$ , and $\operatorname{Re} s < 1$ , and $0 \le \operatorname{Im} s$ , and $\operatorname{Im} s \le 3.29 \cdot 10^{9}$ , then $\operatorname{Re} s = \tfrac12$ — an exact equality of real numbers, with $\tfrac12$ the real number one half. Equivalently, every element of $Z$ lies on the line $\operatorname{Re} s = \tfrac12$ . The strip inequalities are strict on both sides, so nothing is claimed about possible zeros with $\operatorname{Re} s = 0$ or $\operatorname{Re} s = 1$ ; the imaginary-part bounds are non-strict on both sides, so the segment $\operatorname{Im} s = 0$ (i.e. real $s$ with $0 < s < 1$ ) and the horizontal line $\operatorname{Im} s = 3.29 \cdot 10^{9}$ are both included. Nothing whatsoever is asserted about zeros with $\operatorname{Im} s < 0$ , nor about zeros of any height above $3.29 \cdot 10^{9}$ ; the statement is not symmetrized to the lower half-plane. This conjunct is a conditional: if $Z$ happened to be empty it would hold vacuously.

Second conjunct. The set $Z$ is finite (it can be put in bijection with an initial segment of the natural numbers). No lower bound on its size is claimed, and it is not asserted to be nonempty; the empty set satisfies this.

Third conjunct. The natural-number cardinality of $Z$ satisfies

\#Z \;\le\; 10^{10} \;=\; 10{,}000{,}000{,}000 .

Here $\#$ is Set.ncard, i.e. $\operatorname{Nat.card}$ of the coercion of $Z$ to a type: it returns the number of elements when the set is finite, and returns the junk value $0$ when the set is infinite. Consequently this third conjunct, taken on its own, would be satisfied automatically by an infinite $Z$ (its value would then be $0 \le 10^{10}$ ); it is the second conjunct that rules out that reading and makes the bound a genuine count. Because $Z$ is a set of complex numbers, this counts distinct zeros only — zeros are not weighted by multiplicity, and a multiple zero contributes exactly one to the count. The count is an upper bound only: no lower bound is given, no exact value is claimed, and the numbers $3.29 \cdot 10^{9}$ and $10^{10}$ are unrelated constants within the statement, with no asserted relationship between the height cutoff and the number of zeros below it.

The three parts are joined by conjunction, so the declaration asserts all of them simultaneously: every zero of $\zeta$ in the closed-in-imaginary-part, open-in-real-part box $R$ has real part exactly $\tfrac12$ ; there are finitely many such zeros; and there are at most $10^{10}$ of them. No statement is made about the location of zeros outside $R$ , about the trivial zeros, about the pole of $\zeta$ at $s = 1$ (which lies outside $R$ since $\operatorname{Re} s < 1$ is strict), or about any zero being simple.

Human review

Endorsed by marwahaha · Sep 7, 2026
Endorsed by Jack McCarthy · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph