$\zeta(s)\ne0$ for $0<\operatorname{Re}(s)<1$ , $2\le\operatorname{Im}(s)\le14$

Proved

TaoFivePrimes.zeta_ne_zero_strip_im_two_to_fourteen

by Gabewhigham · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorynumerical-verificationriemann-zetatao-five-primeszero-free-region

No zeros of $\zeta$ below height $14$ (beyond $2$ ). For every $s\in\mathbb C$ with

0<\operatorname{Re}(s)<1,\qquad 2\le \operatorname{Im}(s)\le 14,

we have $\zeta(s)\neq 0$ .

The lowest non-trivial zero of $\zeta$ is $\tfrac12 + i\,14.134725\ldots$ , so the rectangle above is zero-free. Together with the already proved zero-free rectangle $|\operatorname{Im}(s)|\le 2$ (zeta_ne_zero_of_mem_strip_of_abs_im_le_two) this gives the bottom block $0\le\operatorname{Im}(s)\le14$ of the numerical verification of the Riemann hypothesis up to height $3.29\times10^9$ (Tao, Theorem 1.5). It is a small, self-contained computation (an explicit lower bound for $|\zeta|$ or the argument principle on a rectangle).

Preamble

import Mathlib

Formal statement

namespace TaoFivePrimes

theorem zeta_ne_zero_strip_im_two_to_fourteen (s : ℂ) (h0 : 0 < s.re) (h1 : s.re < 1)
    (ha : 2 ≤ s.im) (hb : s.im ≤ 14) : riemannZeta s ≠ 0 := by
  sorry

end TaoFivePrimes

Source

Lowest zero ordinate 14.134725... (Gram 1903; see A. M. Odlyzko's tables of zeros and E. C. Titchmarsh, The Theory of the Riemann Zeta-Function, 2nd ed., Section 15.1); bottom block of Theorem 1.5 (p. 7) of T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656.

View graph

ζ(s)≠0\zeta(s)\ne0ζ(s)=0 for 0<Re⁡(s)<10<\operatorname{Re}(s)<10<Re(s)<1, 2≤Im⁡(s)≤142\le\operatorname{Im}(s)\le142≤Im(s)≤14

$\zeta(s)\ne0$ for $0<\operatorname{Re}(s)<1$ , $2\le\operatorname{Im}(s)\le14$