No zeros of $\zeta$ with $\tfrac12<\operatorname{Re} s<1$ above height $100$ (equivalent to RH)

Open

zeta_ne_zero_of_strip_of_hundred_lt_im

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

analytic-number-theoryconjectureriemann-hypothesiszeta-functions

Let $\zeta$ denote the Riemann zeta function. The assertion is that $\zeta$ has no zero strictly to the right of the critical line inside the critical strip and above height $100$ :

\tfrac12<\operatorname{Re} s<1 \ \text{ and } \ \operatorname{Im} s>100 \ \Longrightarrow\ \zeta(s)\neq 0.

This is open, and it is equivalent to the Riemann hypothesis, because the region below height $100$ is settled: the rectangle $0<\operatorname{Re}s<1$ , $|\operatorname{Im}s|\le14$ is zero-free (zeta_ne_zero_of_mem_strip_of_abs_im_le_fourteen), and every zero with $14<\operatorname{Im}s\le100$ lies on the critical line (zeta_ne_zero_of_strip_of_fourteen_lt_im_of_im_le_hundred). The functional equation and the reflection $\zeta(\bar s)=\overline{\zeta(s)}$ transfer the remaining cases to this region. It is the height- $100$ member of the family zeta_ne_zero_of_strip_of_*_lt_im (heights $2,5,6,14$ ); the larger threshold makes it formally weaker than those.

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_hundred_lt_im (s : ℂ) (h0 : 1 / 2 < s.re) (h1 : s.re < 1)
    (him : 100 < s.im) : riemannZeta s ≠ 0 := by sorry

Source

E. C. Titchmarsh, The Theory of the Riemann Zeta-function, 2nd ed. (rev. D. R. Heath-Brown), Oxford 1986, Ch. 14 (the Riemann hypothesis), with the reduction to Re s > 1/2 via the functional equation (§2.1); zeros below height 100 per Odlyzko's tables (https://www-users.cse.umn.edu/~odlyzko/zeta_tables/).

View graph

No zeros of ζ\zetaζ with 12<Re⁡s<1\tfrac12<\operatorname{Re} s<121​<Res<1 above height 100100100 (equivalent to RH)

No zeros of $\zeta$ with $\tfrac12<\operatorname{Re} s<1$ above height $100$ (equivalent to RH)