Goldbach numbers in intervals of length $4.45 \log^2 x$ under the Riemann Hypothesis

Steve Hubbard

Goldbach numbers in intervals of length $4.45 \log^2 x$ under the Riemann Hypothesis

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

Contributed by Steve Hubbard

Version 2 / Oct 26, 2026 / CC BY 4.0

Abstract

Assuming the Riemann Hypothesis, we prove that for every real

x \ge 3

the interval

(x, x + 4.45 \log^2 x)

contains an even integer that is a sum of two odd primes. The proof combines a weighted mean square bound for the Chebyshev prime counting error in short intervals with a piecewise linear weight in a bilinear identity for short interval prime counts. The deduction is checked in Lean 4 conditionally on the explicit formula ExplicitA, the zero sum bound HadamardK, the zero count BPTN, the HSW zero counts, the bound

|\gamma| \ge 14

, and the Goldbach verification to

4 \cdot 10^{18}

, all stated as hypotheses.

Provenance statement

The result came out of an AI-run Lean 4 lab that formalizes Goldbach-related papers. Starting from the explicit RH argument of Chirre and Hagen, arXiv 2512.23534, AI agents found a sharper short interval mean square constant, 1.0069 against 2.2258, and a changed piecewise linear weight in the bilinear pairing, giving 4.45 in place of 123. The deduction is checked in Lean 4 with Mathlib: the main theorem goldbach_445_hsw_gZ builds with no sorry and only the standard axioms, conditional on seven named inputs stated as hypotheses. The Lean source, full import closure and build log are public at github.com/sthubbar/lean-lab-preprints, commit 74c2d1a, and the Lean entry is registered in the Palomar registry as PALOMAR-2026-10-28-000002. Gemini drafted the text over sixteen feedback rounds; each round was checked by a fresh Claude session against the Lean statements, build logs and cited sources. Version 2 answers the aiXiv.science review: expanded Lemma 3.2, the Taylor majorant, the choice of the 2161 pieces, a contrast with Chirre and Hagen, a Lean code structure appendix and the certification process. The author read the paper and directed the work but has not refereed the analysis. Also posted at aiXiv:2610.02672v3 and aixiv.261025.000001 v1.3.

Tools used

Google: GeminiVersion Argon High
Anthropic: Claude Opus
Lean: LeanVersion Lean 4 with Mathlib

References

R. P. Brent, D. J. Platt, and T. S. Trudgian, The mean square of the error term in the prime number theorem , J. Number Theory 238 (2022), 740--762.
A. Chirre and M. Valås Hagen, On Goldbach numbers in short intervals , Research in Number Theory 12 (2026), article 82, doi:10.1007/s40993-026-00767-6, arXiv:2512.23534.arXiv DOI
M. Cully-Hugill and A. W. Dudek, An explicit mean-value estimate for the prime number theorem in intervals , J. Aust. Math. Soc. 117 (2024), no. 1, 1--15.
D. A. Goldston, Linnik's theorem on Goldbach numbers in short intervals , Glasgow Math. J. 32 (1990), no. 3, 285--297.
E. Hasanalizade, Q. Shen, and P.-J. Wong, Counting zeros of the Riemann zeta function , preprint, arXiv:2107.06506, 2021.arXiv
I. Kátai, A remark on a paper of Ju. V. Linnik , Magyar Tud. Akad. Mat. Fiz. Oszt. Közl. 17 (1967), 99--100.
H. L. Montgomery, The pair correlation of zeros of the zeta function , in Analytic Number Theory, Proc. Sympos. Pure Math., vol. 24, Amer. Math. Soc., Providence, R.I., 1973, 181--193.
H. L. Montgomery and R. C. Vaughan, The exceptional set in Goldbach's problem , Acta Arith. 27 (1975), 353--370.
H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory. I. Classical Theory , Cambridge Studies in Advanced Mathematics, vol. 97, Cambridge University Press, Cambridge, 2007.
T. Oliveira e Silva, S. Herzog, and S. Pardi, Empirical verification of the even Goldbach conjecture and computation of prime gaps up to $4 \cdot 10^{18}$ , Math. Comp. 83 (2014), no. 288, 2033--2060.

Show all 12 referencesShow fewer references

L. Schoenfeld, Sharper bounds for the Chebyshev functions $\theta(x)$ and $\psi(x)$ . II , Math. Comp. 30 (1976), no. 134, 337--360.
E. C. Titchmarsh, The Theory of the Riemann Zeta-Function , 2nd ed., revised by D. R. Heath-Brown, Oxford University Press, New York, 1986.

Version history

v1Submitted by Steve HubbardInitial depositSupersededOct 25, 2026
v2Submitted by Steve HubbardSubmitted as a new versionCurrentOct 29, 2026