Riemann zeta — RH slice at heights 105–106

Open

TaoFivePrimes.rh_verified_slice_105_106

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 $105$ and $106$ (both endpoints included) lies on the critical line:

\zeta(s)=0,\quad 0<\operatorname{Re} s<1,\quad 105\le \operatorname{Im} s\le 106\ \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_105_106 (s : ℂ) (hs : riemannZeta s = 0) (h0 : 0 < s.re) (h1 : s.re < 1) (ha : 105 ≤ s.im) (hb : s.im ≤ 106) : s.re = 1/2 := by sorry

Source

Exact-rational continuation of sometik179's theta/Mellin and polynomial-certificate method, with theta/Mellin foundations attributed to Gabewhigham. Retains accepted moment data; new radius-106.5 approximation, 40-term local expansion and finite tensor Bernstein certificates are validated by ordinary Lean proofs. Original statement and proof: Prove2Me theorem 0b6e7864-1667-4118-8b2e-b3218fcaa25d (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