Prove2Me

RH verified for 104≤Im⁡(s)≤10510^4 \le \operatorname{Im}(s) \le 10^5

Open
TaoFivePrimes.rh_verified_block_1e4_1e5

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

number-theorynumerical-verificationriemann-zetatao-five-primes

Riemann hypothesis on the slab 104≤Im⁡(s)≤10510^4 \le \operatorname{Im}(s) \le 10^5. Let s∈Cs\in\mathbb C be a zero of the Riemann zeta function, ζ(s)=0\zeta(s)=0, lying in the open critical strip 0<Re⁡(s)<10<\operatorname{Re}(s)<1 with imaginary part in the range

104  ≤  Im⁡(s)  ≤  105.10^4 \;\le\; \operatorname{Im}(s) \;\le\; 10^5.

Then ss lies on the critical line: Re⁡(s)=12\operatorname{Re}(s)=\tfrac12.

This is one block of the numerical verification of the Riemann hypothesis up to height T0=3.29×109T_0=3.29\times10^9 (Theorem 1.5 of Tao's five-primes paper). The slabs [14,102],[102,103],…,[108,109],[109,3.29⋅109][14,10^2],[10^2,10^3],\dots,[10^8,10^9],[10^9,3.29\cdot10^9], together with the zero-free range 0≤Im⁡(s)≤140\le\operatorname{Im}(s)\le 14, cover the whole range 0≤Im⁡(s)≤T00\le \operatorname{Im}(s)\le T_0; each slab is an independent, finite computation (e.g. sign changes of Hardy's ZZ-function combined with Turing's method), so it can be certified separately.

Formalization Note The zero is not assumed simple; only its location is asserted. Endpoints of the slab are included, so consecutive slabs overlap in a line.

Preamble
import Mathlib
Formal statement
namespace TaoFivePrimes

theorem rh_verified_block_1e4_1e5 (s : ℂ) (hs : riemannZeta s = 0) (h0 : 0 < s.re)
    (h1 : s.re < 1) (ha : 10 ^ 4 ≤ s.im) (hb : s.im ≤ 10 ^ 5) : s.re = 1 / 2 := by
  sorry

end TaoFivePrimes
Source
D. J. Platt, Isolating some non-trivial zeros of zeta, Mathematics of Computation 86 (2017), 2449-2467 (rigorous verification of RH up to height 3.0610046e10); quoted as 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, which also cites the independent verifications of van de Lune-te Riele-Winter (1986), Wedeniwski (ZetaGrid) and Gourdon (2004). This node is the restriction of that verified statement to one horizontal slab of the critical strip.

View graph