HEXAGONbeta

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

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theory

Contributed by Steve Hubbard ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

We report on a Lean 4 formalization of Theorem 2 of Dudek, 2015, as numbered in arXiv v2, which states that if the Riemann hypothesis is true, then for every real x≥2x \ge 2 there is a prime in the interval (x−(4/π)xlog⁡x,x](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. Four cited inputs of the printed proof are replaced in the formal proof. The two that carry the argument are these: first, the prime power contribution ψ−θ\psi - \theta is required only across the moving window (x−h,x+h](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≥70T \ge 70 by trading slack between the head and tail sums at the split point T=2x/hT = 2x/h. The Riemann hypothesis is open and this note makes no progress on it.

Author comments: 11 pages. Version 2 of the note, first deposit on Hexagon.

Provenance statement

Steve Hubbard designed the research program and directed this work. AI tools, Claude and Gemini, wrote the Lean code and drafted the text, and AI agents did the checks of the Lean against the source. No human expert has reviewed the mathematics. The Lean source is public at github.com/sthubbar/goldbach-lean, entries/dudek2014, commit da5cf9e, and the entry is registered in the Palomar registry as PALOMAR-2026-11-01-000028. Agent session logs are not attached, since they hold private email. Also posted as aiXiv:2611.00364v2 and aixiv.261103.000003 v1.1.

References

  1. A. W. Dudek, On the Riemann hypothesis and the difference between primes , Int.\ J.\ Number Theory 11 (2015), no.\ 3, 771--778, doi:10.1142/S1793042115500426, arXiv:1402.6417.arXivDOI
  2. E. Hasanalizade, Q. Shen and P.-J. Wong, Counting zeros of the Riemann zeta function , J.\ Number Theory 235 (2022), 219--241, arXiv:2107.06506.arXiv
  3. E. Carneiro, M. B. Milinovich and K. Soundararajan, Fourier optimization and prime gaps , arXiv:1708.04122v2, first posted 2017, doi:10.4171/CMH/467.arXivDOI
  4. H. Davenport, Multiplicative Number Theory , Springer, 1980.
  5. A. W. Dudek, L. Grenié and G. Molteni, Primes in explicit short intervals on RH , Int.\ J.\ Number Theory 12 (2016), no.\ 5, 1391--1407, arXiv:1503.05403.arXiv
  6. S. Skewes, On the difference π(x)−li⁡(x)\pi(x) - \operatorname{li}(x) II , Proc.\ London Math.\ Soc.\ (3) 5 (1955), 48--70.
  7. J. B. Rosser and L. Schoenfeld, Approximate formulas for some functions of prime numbers , Illinois J.\ Math.\ 6, 1962, no.\ 1, 64--94.
  8. O. Ramaré and Y. Saouter, Short effective intervals containing primes , J.\ Number Theory 98, 2003, no.\ 1, 10--33.
  9. T. S. Trudgian, An improved upper bound for the argument of the Riemann zeta-function on the critical line , Math.\ Comp.\ 81, 2012, no.\ 278, 1053--1061.
  10. Palomar registry, entry PALOMAR-2026-11-01-000028 , version 1, https://palomar-registry.org/entry.html?id=PALOMAR-2026-11-01-000028&version=1.link
Show all 13 referencesShow fewer references
  1. S. Hubbard, goldbach-lean repository, directory entries/dudek2014 , commit da5cf9edad7896290771dfcab8feee2906399e3d , https://github.com/sthubbar/goldbach-lean.link
  2. PrimeNumberTheoremAnd , https://github.com/AlexKontorovich/PrimeNumberTheoremAnd, commit c39a751132c88b6e8080b74c74023fd95b3d8be0 .link
  3. The mathlib Community, The Lean mathematical library , https://github.com/leanprover-community/mathlib4, version v4.35.0-rc3 .link

Version history

  1. v1 · 11 pagesSubmitted by Steve Hubbard11 pages. Version 2 of the note, first deposit on Hexagon.CurrentNov 06, 2026