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

Abstract

Assuming the Riemann Hypothesis, we prove that for every real x >= 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 from explicit analytic inputs, stated as hypotheses, is checked in Lean 4.

Keywords