Riemann zeta — zero-free rectangle at heights 100–101

Open

TaoFivePrimes.zeta_zero_free_rectangle_100_101

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

analytic-number-theorynumerical-verificationriemann-hypothesiszeta-functions

The Riemann zeta function has no zeros in the open critical strip at heights between $100$ and $101$ (both endpoints included):

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

This is a certified zero-free unit slice used to extend the unconditional part of the Riemann-hypothesis decomposition above height $100$ . (The first zeros above $100$ are near $101.32$ , $103.73$ , $105.45$ , so slices containing them are stated instead as "every zero lies on the critical line".)

Preamble

import Mathlib.NumberTheory.LSeries.RiemannZeta

Formal statement

theorem TaoFivePrimes.zeta_zero_free_rectangle_100_101 (s : ℂ) (h0 : 0 < s.re) (h1 : s.re < 1)
    (ha : 100 ≤ s.im) (hb : s.im ≤ 101) : riemannZeta s ≠ 0 := by sorry

Source

Exact-rational continuation of sometik179's theta/Mellin and polynomial-certificate method (original c9908072-d99a-4431-aad8-a72c6352619a, now ordinary-syntax accepted as 30db8e24-e604-49d7-ab5c-f7b6f516651a), with theta/Mellin foundations attributed to Gabewhigham. The original accepted moments are retained; the height-100.5 Taylor coefficients and degree-16 tensor Bernstein certificate are new computations, verified by ordinary Lean kernel proofs. Original statement and proof: Prove2Me theorem ddaf7211-be4a-4c6f-9e4a-8f78d30d5bf7 (env 0df444a, proof by raresbuhai), re-published here in the RH mission's environment (Mathlib 777aaa6) so it can be used in the mission tree. Numerical background: zeros of zeta per Odlyzko's tables (https://www-users.cse.umn.edu/~odlyzko/zeta_tables/); RH verification as in Platt, Math. Comp. 86 (2017) 2449-2467.

View graph