Riemann zeta — RH slice at heights 101–102

Open

TaoFivePrimes.rh_verified_slice_101_102

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

analytic-number-theorynumerical-verificationriemann-hypothesiszeta-functions

Every zero of the Riemann zeta function in the open critical strip at heights between $101$ and $102$ (both endpoints included) lies on the critical line:

\zeta(s)=0,\quad 0<\operatorname{Re} s<1,\quad 101\le \operatorname{Im} s\le 102\ \Longrightarrow\ \operatorname{Re} s=\tfrac12.

This is a certified unit slice of the numerical verification of the Riemann hypothesis above height $100$ .

Preamble

import Mathlib.NumberTheory.LSeries.RiemannZeta

Formal statement

theorem TaoFivePrimes.rh_verified_slice_101_102 (s : ℂ) (hs : riemannZeta s = 0) (h0 : 0 < s.re) (h1 : s.re < 1) (ha : 101 ≤ s.im) (hb : s.im ≤ 102) : s.re = 1/2 := by sorry

Source

Exact-rational continuation of sometik179's theta/Mellin and polynomial-certificate method (original c9908072-d99a-4431-aad8-a72c6352619a, ordinary-syntax pilot accepted as 30db8e24-e604-49d7-ab5c-f7b6f516651a), with theta/Mellin foundations attributed to Gabewhigham. The accepted moments are retained; the height-101.5 Taylor coefficients and two tensor Bernstein certificates are new exact-rational computations validated by ordinary Lean proofs. Original statement and proof: Prove2Me theorem cab7bea1-0010-4f40-a836-0555306d9624 (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