No zeros of $\zeta$ with $\tfrac12<\operatorname{Re} s<1$ and $14<\operatorname{Im} s\le 100$

Proved

zeta_ne_zero_of_strip_of_fourteen_lt_im_of_im_le_hundred

by Ethan Cheung Wang · Oct 22, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analytic-number-theorynumerical-verificationriemann-hypothesiszeta-functions

Let $\zeta$ denote the Riemann zeta function. The Riemann zeta function has no zero strictly to the right of the critical line in the critical strip at heights between $14$ and $100$ :

\tfrac12<\operatorname{Re} s<1,\quad 14<\operatorname{Im} s\le 100 \ \Longrightarrow\ \zeta(s)\neq 0.

This is the part of the classical numerical verification of the Riemann hypothesis covering the first $29$ nontrivial zeros (ordinates $14.13\ldots$ up to $98.83\ldots$ ), which all lie on the critical line. Together with the open statement zeta_ne_zero_of_strip_of_hundred_lt_im it yields zeta_ne_zero_of_strip_of_fourteen_lt_im; the strict inequality $\tfrac12<\operatorname{Re}s$ is essential, since $\zeta$ does vanish on the critical line in this range.

It is a direct consequence of the location theorem TaoFivePrimes.rh_verified_block_14_1e2 (env 0df444a, proved by @raresbuhai from @sometik179's certificate): every zero with $0<\operatorname{Re}s<1$ , $14\le\operatorname{Im}s\le100$ has $\operatorname{Re}s=\tfrac12$ .

Formalization Note. riemannZeta is Mathlib's analytically continued zeta function; s.re, s.im are the real and imaginary parts of s.

Preamble

import Mathlib.NumberTheory.LSeries.RiemannZeta
import Mathlib.NumberTheory.LSeries.Nonvanishing

open Complex

Formal statement

theorem zeta_ne_zero_of_strip_of_fourteen_lt_im_of_im_le_hundred (s : ℂ) (h0 : 1 / 2 < s.re)
    (h1 : s.re < 1) (him : 14 < s.im) (him' : s.im ≤ 100) : riemannZeta s ≠ 0 := by sorry

Source

Numerical verification of RH up to height 100: e.g. A. M. Odlyzko, tables of zeros of the Riemann zeta function (https://www-users.cse.umn.edu/~odlyzko/zeta_tables/), and T. Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656, Theorem 1.5 (RH verified to height 3.29e9). Formal certificate: Prove2Me theorem TaoFivePrimes.rh_verified_block_14_1e2 (4a25d5fd-e124-4e2c-8ca1-9d998179d1c2, env 0df444a).

View graph

No zeros of ζ\zetaζ with 12<Re⁡s<1\tfrac12<\operatorname{Re} s<121​<Res<1 and 14<Im⁡s≤10014<\operatorname{Im} s\le 10014<Ims≤100

No zeros of $\zeta$ with $\tfrac12<\operatorname{Re} s<1$ and $14<\operatorname{Im} s\le 100$