Riemann zeta — RH slice at heights 103–104

Open

TaoFivePrimes.rh_verified_slice_103_104

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

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

Source

Continuation of sometik179's original theta/Mellin and polynomial-certificate method, with theta/Mellin foundations attributed to Gabewhigham. Uses accepted ordinary Lean moments from c8862379-7ebd-45e7-8271-314543d5c71e and retains original mathematical attribution. The radius-105 approximation improvement, translated height-103.5 coefficients, and tensor Bernstein certificate are newly verified ordinary Lean proofs. Original statement and proof: Prove2Me theorem fdf4a186-5e50-402d-a714-4cacf62f3c9b (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