An explicit prime gap under the Riemann hypothesis, formalized in Lean with its prime power input made elementary

Abstract

We report on a Lean 4 formalization of Theorem 2 of Dudek, 2015, which states that if the Riemann hypothesis is true, then for every real x >= 2 there is a prime in the interval (x - (4/pi) sqrt(x) log x, x]. In the formalization, Theorem 2 is proved assuming the Riemann hypothesis and one cited explicit zero-counting bound of Hasanalizade, Shen and Wong, arXiv:2107.06506. Two inputs in the formal proof differ from those printed in Dudek's paper: first, the prime power contribution psi - theta is required only across the moving window (x - h, x + h] and is proved outright in Lean by an elementary counting argument with no cited input and without assuming the Riemann hypothesis; second, the sum over nontrivial zeros is bounded from the cited Hasanalizade, Shen and Wong zero count for T >= 70 by trading slack between the head and tail sums at the split point T = 2x/h. The Riemann hypothesis is open and this note makes no progress on it. Lean source: https://github.com/sthubbar/goldbach-lean, entries/dudek2014, commit da5cf9e. Palomar registry PALOMAR-2026-11-01-000028.

Keywords