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

Introduction

Assuming the Riemann Hypothesis, Kátai [6] and Montgomery and Vaughan [8] proved that for some constant $C > 0$ every interval $(x,x+C\log^{2}x)$ with $x$ sufficiently large contains a Goldbach number, and Goldston [4] gave a proof comparing the measure of prime-free short intervals with Selberg’s mean square bound. Cully-Hugill and Dudek [3 Theorem 1.3] made this result explicit with $C = 9696$ for all $x \ge2$. Chirre and Hagen [2] reduced the constant to $C = 123$. The binary Goldbach conjecture itself remains open; the result here concerns Goldbach numbers in short intervals under the Riemann Hypothesis.

Our proof follows the mean square framework of Chirre and Hagen [2] and makes three changes. First, in the mean square over $[1,x]$, we replace the sharp cutoff by the smooth weight $W(u)=\min(1,u^{-4})$, which produces the positive kernel $4/(4+(\gamma_i-\gamma_j)^2)$ and bounds the inner sum over zero ordinates directly by $\log|\gamma_i|$. Second, we bound the diagonal sum using the exact modulus squared of the short interval coefficient, Taylor majorants for $1-\cos$, and a partition of the scaled mid-range $[1,139.984375]$ into 2161 pieces with dyadic rational endpoints, reducing the mean square constant from 2.2258 in [2] to 1.0069. Third, instead of deducing the theorem directly from the mean square on an interval $[ax,x]$ with $\delta=h/(2x)$ as in [2 Section 5], we integrate $A(t)A(x-t)=0$ against the weight $\varphi(t)=11t/(5x)$ on $[x/64,5x/11]$ and $\varphi(t)=1$ on $[5x/11,x/2]$, which produces a nonincreasing weight on the quadratic error term and allows direct Abel summation over 256 equal steps. The resulting constants are new as far as we know.

In comparison with [2], each of these three changes replaces a step in their argument to tighten the resulting constants. First, the smooth weight $W$ replaces their unweighted mean square expansion on $[1,x]$ and makes every off-diagonal term carry the positive kernel $4/(4+(\gamma_i-\gamma_j)^2)$, so the inner sum is bounded directly by Lemma 2.2. Second, the exact modulus with the 2161 certified pieces replaces their bound for $|c_\delta(\gamma)|^2$; together with the smooth weight $W$, this lowers the mean square constant from 2.2258 in [2] to 1.0069 here. Third, the weight $\varphi$ with 256 step Abel summation replaces their direct deduction from the unweighted short interval mean square, combining with the smaller mean square constant to reduce the interval length constant from $C = 123$ in [2] to 4.45.

The deduction of Theorem 1.1 from seven stated hypotheses is checked in Lean 4 with Mathlib as the theorem goldbach_445_hsw_gZ. Lean checks the smooth mean square bound, the 2161-piece diagonal certificate, the transfer from $\psi$ to $\theta$, the 256-step Abel summation in the bilinear identity, and the combination with the finite Goldbach verification conditionally on the seven hypotheses ExplicitA, HadamardK, Ordinates14, BPTN, EvenGoldbachUpTo, HSWN70, and HSWHead14. Among these, HadamardK is proved in this paper (Lemma 2.2) but assumed as a hypothesis in Lean, and ExplicitA, HadamardK, and BPTN are assumed under the Riemann Hypothesis. See Table 3 in Appendix A for the full list of hypotheses and their status, and Table 4 for representative pieces of the diagonal certificate.

Lean hypothesis	Source	In this paper	In Lean 4
ExplicitA	[9], Equation (12.1), Lemma 2.1	Cited	Assumed as hypothesis
HadamardK	Lemma 2.2	Proved under RH	Assumed as hypothesis
Ordinates14	[12], Chapter XV, Lemma 2.3	Cited	Assumed as hypothesis
BPTN	[1], Lemma 1, Lemma 2.4 for $T \ge10^{13}$	Cited	Assumed as hypothesis
HSWN70	[5], Corollary 1.2 for $T \ge70$	Cited	Assumed as hypothesis
HSWHead14	[5], Corollary 1.2 for $T \ge14$	Cited	Assumed as hypothesis
EvenGoldbachUpTo	[10], Lemma 2.6	Cited	Assumed as hypothesis

$A$	$B$	$Q$	$\lambda$	Majorant
1	1.0029296875	0.9194789	0.0029296875	pt_norm, lo = 0.99999
5.67578125	5.6884765625	0.0111334	1.7905011127125	pt_raw with hu_poly, k = 1
139.6982421875	139.984375	0.0001399	4.9456581952875	pt_raw with hu_pi, k = 22

Notation and inputs

Throughout the paper, $\Lambda(n)$ denotes the von Mangoldt function, $\psi(x) = \sum_{n \le x} \Lambda(n)$, and $\theta(x) = \sum_{p \le x} \log p$, where $p$ runs over primes. Under the Riemann Hypothesis, the nontrivial zeros of the Riemann zeta function $\zeta(s)$ take the form $\rho= 1/2 + i\gamma$ with $\gamma\in\mathbb{R}$. We write $N(T)$ for the number of nontrivial zeros $\rho= \beta+ i\gamma$ with $0 < \gamma\le T$, counted with multiplicity. For $\delta> 0$ and $\rho= 1/2 + i\gamma$, we define the short interval coefficient

For $x \ge2$ and $\delta> 0$, we define the short interval mean squares

We state the inputs used in the formal proof together with their published sources, and we prove the second input, Lemma 2.2, directly.

Equation (3) is the difference of von Mangoldt’s explicit formula [9 Equation (12.1)] at $(1+\delta)y$ and $y$ for $y \ge2$ when neither endpoint is a prime power. In the Lean formalization, SmoothT2.ExplicitA states (2.3) as the limit of $-\sum_{\rho\in Z_n} c_\delta(\rho)y^\rho$ along truncations $Z_n$, for almost every $y \ge2$, with $B(y) = \frac{1}{2}\log\frac{1-y^{-2}}{1-((1+\delta)y)^{-2}}$ included as the function Bf; the main theorem assumes it, under RH, for each $0 < \delta\le10^{-13}$.

Proof. Since each summand is positive, it suffices to bound the sum over all nontrivial zero ordinates $\gamma'$ counted with multiplicity, where $\rho' = 1/2 + i\gamma'$. Setting $s = 5/2 + i\gamma$, we have

By the partial fraction decomposition of $\xi'(s)/\xi(s)$ [9 Corollary 10.14],

For $\operatorname{Re}z>0$, Binet’s integral formula gives $\frac{\Gamma'}{\Gamma}(z)=\log z-\frac{1}{2z}-\int_0^\infty f(t)e^{-tz}\,dt$, where $f(t)=\frac{1}{2}-\frac{1}{t}+\frac{1}{e^t-1}$ satisfies $f(0)=0$ and $f'(t)=\frac{1}{t^2}-\frac{1}{4\sinh^2(t/2)}$ decreases monotonically from $f'(0)=\frac{1}{12}$ to $0$ on $(0,\infty)$. Integrating by parts twice gives $\int_0^\infty f(t)e^{-tz}\,dt=\frac{1}{12z^2}+\frac{1}{2z}\int_0^\infty f''(t)e^{-tz}\,dt$, which has modulus at most $\frac{1}{12|z|^2}+\frac{1}{|z|^2}\int_0^\infty(-f''(t))\,dt=\frac{1}{|z|^2}\le\frac{\operatorname{Re}z}{2|z|^2}=\operatorname{Re}\frac{1}{2z}$ whenever $\operatorname{Re}z\ge\frac{1}{3}$, so $\operatorname{Re}\frac{\Gamma'}{\Gamma}(z)\le\log|z|$. Applying this at $z=\frac{9}{4}+\frac{i\gamma}{2}$ with $|\gamma|\ge14$ from Lemma 2.3 yields

On the line $\operatorname{Re}(s)=5/2$, the Dirichlet series for $\zeta'/\zeta$ yields $\operatorname{Re}\frac{\zeta'}{\zeta}(s)\le-\frac{\zeta'(5/2)}{\zeta(5/2)}=0.28874\cdots<0.2888$, while $2\operatorname{Re}\frac{1}{s-1}=\frac{3}{9/4+\gamma^2}<\frac{3}{\gamma^2}$. For $|\gamma|\ge14$, we obtain

so the right-hand side of (6) is at most $\log|\gamma|-1.1933<\log|\gamma|$; the lemma states the weaker bound $\log|\gamma|$ because that is the form used later. □

The lowest nontrivial zero has ordinate $\gamma_1=14.134725\cdots>14$.

Inequality (12) follows immediately from (11) because $u^{-1/2}\log^2 u$ is decreasing for $u > e^4$ and equals $5.4005\cdots\times10^{-7}\cdot8\pi< 8\pi\cdot10^{-6}$ at $u=10^{16}$. In the Lean formalization, inequality (11) is not assumed; it is proved under RH for $u \ge10^{11}$ from the explicit formula and the zero counting bound of Hasanalizade, Shen, and Wong [5 Corollary 1.2] (assumed as the hypotheses HSWN70 and HSWHead14), together with the numerical fact, taken as the hypothesis Ordinates14 in Lean, that every nontrivial zero has ordinate of absolute value at least 14.

The mean square bound

We bound the mean square on $[1,x]$ of a finite Dirichlet polynomial supported on nontrivial zeros of $\zeta(s)$.

Proof. Define $W(u)=\min(1,u^{-4})$ for $u>0$. Since $W(u)\ge0$ for all $u>0$ and $W(y/x)=1$ for $1\le y\le x$, the substitution $y=xu$ gives

For any $\Delta\in\mathbb{R}$, splitting the integral at $u=1$ yields

Since $\frac{4}{4+(\gamma_i-\gamma_j)^2}>0$ is symmetric in $i$ and $j$, applying $|c_i\overline{c_j}x^{i(\gamma_i-\gamma_j)}|\le\frac{1}{2}(|c_i|^2+|c_j|^2)$ in (15) gives the first inequality in (14). Applying Lemma 2.2 to the inner sum over $j$ gives the second inequality. □

We next bound the diagonal sum $\sum_\gamma|c_\delta(\gamma)|^2\log|\gamma|$.

Proof. By symmetry of the nontrivial zeros with respect to the real axis, $\sum_{\gamma} |c_{\delta}(\gamma)|^2 \log|\gamma| = 2\sum_{\gamma>0} |c_{\delta}(\gamma)|^2 \log\gamma$, and every term has $\gamma\ge14$ by Lemma 2.3. Let $\eta= \log(1+\delta)$ and $\Lambda= \log(1/\delta)$. From (1), the exact modulus squared of $c_{\delta}(\gamma)$ is

For all real $t$, the alternating Taylor series for $\cos t$ gives the degree-6 majorant (one_sub_cos_le)

Write $v=\delta|\gamma|$ for the scaled variable, and set

The certified bound is organized in two cases, split at $\delta=2^{-188}$.

Pieces. The bound on an individual piece is formalized as the lemma piece_sum in LeanLab/ChirreHagen2025/U1263Core.lean, conditional on BPTN (Lemma 2.4) and Ordinates14 (Lemma 2.3). Let $0<\delta\le10^{-13}$, let $1\le A\le B$, let $\log B\le\lambda\le5$, let $Q\ge0$, and assume the majorant hypothesis on the piece that $|c_{\delta}(\gamma)|^2\le Q\delta^2$ whenever $A/\delta<|\gamma|\le B/\delta$. Then piece_sum states that for any finite set of zero ordinates,

In the structure of this Lean lemma, the zeros on the piece are counted with Lemma 2.4, $\log|\gamma|\le\Lambda+\lambda$ there because $|\gamma|\le B/\delta$ and $\log B\le\lambda$, and the term $2QE$ collects the lower order part of the count.

To obtain $Q$ on a piece $A/\delta<|\gamma|\le B/\delta$, write $t=|\gamma|\log(1+\delta)$ for the phase; the lemma phase_range gives $A(1-10^{-13})<t\le B$ on the piece. The majorant hypothesis $|c_{\delta}(\gamma)|^2\le Q\delta^2$ is established by one of two Lean routes in U1263Core.lean: pt_norm for pieces nearest $v=1$, and pt_raw elsewhere. In pt_norm, for $0\le\operatorname{lo}\le A(1-10^{-13})$, $Q$ satisfies $2(1+10^{-13})(1/2-\operatorname{lo}^2/24+B^4/720)+10^{-26}\le Q$. In pt_raw, given an upper bound $1-\cos t\le u$ for $A(1-10^{-13})<t\le B$, $Q$ satisfies

The bound $u$ in pt_raw comes from hu_poly, the degree-6 majorant (19) after shifting $t$ by $2k\pi$, or from U6743.hu_pi, the majorant $1-\cos t\le2-s^2/2+s^4/24$ with $s$ the shift of $t$ by an odd multiple of $\pi$; both use $3.141592<\pi<3.141593$. The piece endpoints are dyadic rationals; the piece endpoints and $\lambda$ were chosen by a numerical search and certified piece by piece. Here $\lambda$ is any number with $\log B\le\lambda\le5$, certified in Lean through a dyadic bound on $\log B$; $Q$ is a rational number at least the pt_raw or pt_norm bound. For example, the first piece has $A=1$, $B=1.0029296875$, $Q=0.9194789$, $\lambda=0.0029296875$, and the last piece has $A=139.6982421875$, $B=139.984375$, $Q=0.0001399$, $\lambda=4.9456581952875$.

Case $2^{-188}<\delta\le10^{-13}$. On the head range $|\gamma|\le1/\delta$ the sum is at most $\delta\Lambda^2/\pi\le0.31831X$. On the range $v>1$ it is at most

This range consists of 2161 pieces covering $1<v\le139.984375$, each bounded by (20), a further range $139.984375<v\le599.734375$, and a tail $v>599.734375$ bounded by $0.002182674424X+0.027980492816Y+0.089673014185\delta$. Table 1 lists the coefficients of $X=\delta\Lambda^2$. They sum to 1.014962249211, and the bound $1.0068\,\delta\log^2(2.0001/\delta)$ follows because $\log(2.0001/\delta)=\Lambda+\log2.0001$ with $\log2.0001\ge0.6931$, and $\Lambda\le130.3116699904$ when $\delta>2^{-188}$; together these absorb the lower order terms.

Range	Method	Coefficient of $\delta\Lambda^2$
Head $|\gamma|\le1/\delta$	Bound $\delta\Lambda^2/\pi$	0.31831
$1<v\le139.984375$	2161 pieces, (3.8)	0.690304599302
$139.984375<v\le599.734375$	Certified chain	0.004164975485
$v>599.734375$	Tail bound	0.002182674424
Total		1.014962249211

Case $\delta\le2^{-188}$. The head range is $|\gamma|\le10^{-20}/\delta$, followed by a dyadic chain of 64 steps, which gives

All of these bounds are certified by exact rational arithmetic and checked in Lean as diag_u6806, conditional on BPTN and Ordinates14. □

The lower order terms and $\Lambda\le130.3116699904$ bring the total to 1.0068 relative to $\delta\log^2(2.0001/\delta)$.

Combining Lemma 2.1, Lemma 3.1, and Lemma 3.2 with the $L^2$ convergence of the truncated explicit formula as proved in [2 Section 3] yields the short interval mean square bound.

Proof. Write $V(y)=\psi((1+\delta)y)-\psi(y)-\delta y$ and let

be the secondary term of Lemma 2.1, so $V(y)-B(y)$ is the zero sum. By Lemma 2.1, the $L^2$ limit argument of [2 Section 3], and Lemmas 3.1 and 3.2, we have

For $y\ge2$ and $0<\delta\le1$, we have $|B(y)|\le\delta$, so $\int_2^xB(y)^2\,dy\le\delta^2x$. Since $(u+b)^2\le(1+\eta)u^2+(1+1/\eta)b^2$ for every $\eta>0$, taking $\eta=10^{-5}$ with $L=\log(2.0001/\delta)$ gives

On $[1,2]$, since $\psi(y)=0$ for $y<2$, the difference $\psi((1+\delta)y)-\psi(y)$ is nonzero only for $y\in[2/(1+\delta),2)$, an interval of length at most $2\delta$, where it is at most $\log2$; with $u=\psi((1+\delta)y)-\psi(y)\ge0$ and $v=\delta y\ge0$ we have $(u-v)^2\le u^2+v^2$, so $\int_1^2V(y)^2\,dy\le2\delta(\log2)^2+\frac{7}{3}\delta^2\le3\delta$. For $x\ge10^{13}$ and $0<\delta\le10^{-13}$, we have $L\ge\log(2\cdot 10^{13})>30. Dividing by $\delta L^{2}x^{2}$, the first term is $1.0068(1+10^{-5})=1.00681007$, the second term is at most $10^{5}\cdot10^{-13}/(900\cdot10^{13})<10^{-30}$, and the third is at most $3/(900\cdot10^{26})<10^{-28}$. The sum is below $1.0069$, so $J_{\psi}(x,\delta)\leq1.0069\,\delta L^{2}x^{2}$.

We now pass from $J_{\psi}(X,\delta)$ to $J_{\theta}(X,\delta)$. Write $D(y)=(\psi-\theta)((1+\delta)y)-(\psi-\theta)(y)\geq0$ and $u=\psi((1+\delta)y)-\psi(y)-\delta y$, so $\theta((1+\delta)y)-\theta(y)-\delta y=u-D(y)$. Applying $(u-D)^{2}\leq(1+\eta)u^{2}+(1+1/\eta)D^{2}$ with $\eta=0.001$ gives $J_{\theta}(X,\delta)\leq1.001J_{\psi}(X,\delta)+1001\int_{1}^{X}D(y)^{2}\,dy$. By Fubini’s theorem, $\int_{1}^{X}D(y)\,dy\leq\delta X(\psi-\theta)((1+\delta)X)$. When $\delta\sqrt{y}<1$, every interval $(y^{1/k},((1+\delta)y)^{1/k}]$ with $k\geq2$ has length at most $\frac{1}{2}\delta\sqrt{y}<1$ and contains at most one prime, so $D(y)\leq\log^{2}((1+\delta)y)/\log2$. Multiplying this pointwise bound by the $L^{1}$ bound and using $(\psi-\theta)((1+\delta)X)\leq(1+\delta)X\log((1+\delta)X)\leq2\sqrt{(1+\delta)X}\log((1+\delta)X)$ shows that $1001\int_{1}^{X}D(y)^{2}\,dy<0.0019\,\delta\log^{2}(2.0001/\delta)X^{2}$ for $X\geq5\cdot10^{17}$ and $0<\delta\leq10^{-13}$. Thus, if $J_{\psi}(X,\delta)\leq J\delta\log^{2}(2.0001/\delta)X^{2}$, then for $X\geq5\cdot10^{17}$, $0<\delta\leq10^{-13}$, and $\delta\sqrt{X}<1$, we have

With $J=1.0069$ from Proposition 3.3, this gives $c=1.0098069$.

The bilinear argument

To prove Theorem 1.1, we split the range of $x$ at $2\cdot10^{18}$. For $3\leq x\leq2\cdot10^{18}$, the interval length satisfies $4.45\log^{2}x\geq4.45\log^{2}3>5.36$, so $(x,x+4.45\log^{2}x)$ contains an even integer $2n$ in $[6,4\cdot10^{18}]$, which is a sum of two odd primes by Lemma 2.6. The analytic argument runs for $x\geq1.1\cdot10^{18}$, where $\log x\geq41$.

Let $x\geq1.1\cdot10^{18}$ and fix $H$ with $4\leq H\leq61.5$. Put $h=H\log^{2}x$ and $\delta=h/x$, so $0<\delta\leq10^{-13}$ and $\delta\sqrt{x}<1$. Let

As observed by Goldston [4, p. 285], if no Goldbach number lies in $(x,x+h]$, then for every $t\in[x/64,x/2]$ the intervals $(t,(1+\delta)t]$ and $(x-t,(1+\delta)(x-t)]$ cannot both contain an odd prime, and since $t\geq x/64>10^{16}>2$, we have

We weight (28) by the continuous piecewise linear function

Substituting $A(t)=\delta t+E(t)$ and $A(x-t)=\delta(x-t)+E(x-t)$ into $0=\int_{x/64}^{x/2}\varphi(t)A(t)A(x-t)\,dt$ gives the weighted identity

By the arithmetic-geometric mean inequality, for every $t\in[x/64,x/2]$ we have

Integrating (31) over $t \in[x/64,x/2]$ and substituting $u=x-t$ in the second term yields

where the combined weight $w(u)$ on $[x/64,63x/64]$ is

At the junction $u=6x/11$, both expressions in (33) equal $1/2$. Thus $w(u)$ is positive, continuous, and nonincreasing on $[x/64,63x/64]$.

Proof of Theorem 1.1. Assume $x\geq1.1\cdot10^{18}$, fix $H$ with $4\leq H\leq61.5$, put $h=H\log^2 x$ and $\delta=h/x$, and suppose that no Goldbach number lies in $(x,x+h]$. Evaluating the main term on the left-hand side of (30) with $\varphi(t)$ from (29) gives $\delta^2x^3M$, where

To bound the cross terms in (30), write $R(u)=\theta(u)-u$, so $E(u)=R((1+\delta)u)-R(u)$. Substituting $u=x-t$ in $\int_{x/64}^{x/2}\varphi(t)tE(x-t)\,\mathrm{d}t$ splits the cross-term integral into four smooth pieces; the first two are written in the variable $t$ and the last two in $u=x-t$: $[x/64,5x/11]$ with weight $\frac{11}{10}\cdot\frac{2}{x}t(x-t)$, $[5x/11,x/2]$ with weight $x-t$, $[6x/11,63x/64]$ with weight $\frac{11}{10}\cdot\frac{2}{x}(x-u)^2$, and $[x/2,6x/11]$ with weight $x-u$. On each piece $[ax,bx]$ with normalized weight $g(u)$, the substitution $v=(1+\delta)u$ transforms $\int_{ax}^{bx}g(u)R((1+\delta)u)\,\mathrm{d}u$ into $\int_{(1+\delta)ax}^{(1+\delta)bx}\frac{1}{1+\delta}g\left(\frac{v}{1+\delta}\right)R(v)\,\mathrm{d}v$ with new limits of integration $(1+\delta)ax$ and $(1+\delta)bx$, which gives

Since $1-(1+\delta)^{-k}\leq k\delta$ for $k=1,2,3$ and $0<u\leq x$, the interior factor $\left|\frac{1}{1+\delta}g\left(\frac{v}{1+\delta}\right)-g(v)\right|$ is bounded on $[0,x]$ by $2(2+3)\delta x=10\delta x$ for $\frac{2}{x}u(x-u)$, by $(1+2)\delta x=3\delta x$ for $x-u$, and by $2(1+4+3)\delta x=16\delta x$ for $\frac{2}{x}(x-u)^2$. Since $u\geq x/64>10^{16}$ throughout all four intervals, Lemma 2.5 gives $|R(v)|\leq10^{-6}v\leq10^{-6}x$ on $[ax,bx]$ of length $(b-a)x$, and $|R(v)|\leq10^{-6}v\leq10^{-6}(1+\delta)x\leq2\cdot10^{-6}x$ on the boundary intervals $[bx,(1+\delta)bx]$ and $[ax,(1+\delta)ax]$ of lengths $\delta bx$ and $\delta ax$. Summing the four bounds shows that the left-hand side of (30) is at least $\delta^2x^3(M-K)$, where

To bound the right-hand side of (32), take 256 equal steps

so $s_0=6/11$, $s_{256}=63/64$, and $w_0=1/2$. The weight $w(u)$ on $E(u)^2$ in (33) is $1/2$ on $[x/64,6x/11]$ and at most $w_j$ on $[s_jx,s_{j+1}x]$. Since $s_jx \ge(6/11)x > 6\cdot10^{17} > 5\cdot10^{17}$, $w$ is nonincreasing, and

by (26), Abel summation bounds the right-hand side of (32) by $c\,\delta\log^2(2.0001/\delta)x^2U$, where

Since $h\ge2.0001$, we have $\log(2.0001/\delta)\le\log x$. Using $\delta=H\log^2x/x$ and dividing by $\delta x^2\log^2x$, no Goldbach number in $(x,x+h]$ forces $H(M-K)\le c\cdot0.24922$. Thus it is enough that

With $J=1.0069$ from Proposition 3.3, the left-hand side of (39) is 0.2516641, and $H=4.44$ gives right-hand side 0.2517492; the smallest $H$ that works is $H_{\min}=4.43850$. This gives a Goldbach number $n$ with $x<n\le x+4.44\log^2x$, and the extra $0.01\log^2x$ in the theorem gives the strict upper bound in $(x,x+4.45\log^2x)$. □

By (39), $H_{\min}=(1.001J+0.0019)\cdot0.24922/(M-K)$, so $H_{\min}$ is proportional to $c$ and the mean square constant $J$ is the main limiting input; at $J=1.0069$ the weight scan gives about 4.43, and the 4.43 figure is a numerical scan of this weight family at $J=1.0069$, not a proven lower limit. Lowering the order of the interval length below $\log^2x$ from the Riemann Hypothesis alone would require an upper bound on the pair correlation of zeros of $\zeta(s)$ that is not known; under the Riemann Hypothesis together with Montgomery’s pair correlation conjecture [7], Goldston [4] already reaches $(2+\epsilon)\log x$.

Numerical verification

All numerical constants in Lemma 3.2, Proposition 3.3, and the proof of Theorem 1.1 are certified in the Lean 4 kernel conditionally on the seven hypotheses of goldbach_445_hsw_gZ. The certification uses finite grids with explicit rational parameters: in Lemma 3.2, the case $2^{-188}<\delta\le10^{-13}$ uses 2161 pieces on $1<v\le139.984375$, a further range $139.984375<v\le599.734375$, and a tail $v>599.734375$, while the case $\delta\le2^{-188}$ uses a head range $|\gamma|\le10^{-20}/\delta$ and a dyadic chain of 64 steps; in Section 4, the interval $[6/11,63/64]$ is split into 256 equal Abel steps in $u/x$. Every constant is a decimal or rational number checked by norm_num and linarith in the Lean kernel, so no floating point arithmetic enters the certificate and no rounding error analysis is needed; transcendental quantities enter only through certified bounds such as $3.141592<\pi<3.141593$, $\log2.0001\ge0.6931$, and dyadic bounds on $\log B$. The Lean build completes successfully in 9183 jobs with exit code 0, and #print axioms for goldbach_445_hsw_gZ, theorem2_u6806, and goldbach_445_of_J_hsw lists only the standard foundational axioms propext, Classical.choice, and Quot.sound. Table 2 records the certified parameters and margin checks around $H_{\min}=4.43850$.

Quantity	Certified value	Role in proof
End of the 2161 pieces	139.984375	In $v=\delta|\gamma|$, Lemma 3.2
Pieces	2161	Dyadic rational endpoints on $1<v\le139.984375$
Diagonal constant $C_{\mathrm{diag}}$	1.0068	Bound in (17) for $0<\delta\le10^{-13}$
Mean square constant $J$	1.0069	Bound in (22) for $x\ge10^{13}$
Transfer constant $c$	1.0098069	$c=1.001J+0.0019$ in (26) for $X\ge5\cdot10^{17}$
Abel summation steps	256	Equal steps in $u/x$ from $6/11$ to $63/64$ in (37)
Main term constant $M$	0.0567215028 . . .	Exact integral in (34) with weight $\varphi$
Cross-term constant $K$	$2.1226\cdot10^{-5}$	Cross-term bound in (36)
Abel constant $U$	$0.2492140\cdots<0.24922$	Upper bound factor in (38)
Minimum admissible $H_{\min}$	4.43850	Threshold in (39); 4.44 gives 0.2517492 > 0.2516641

Appendix A. Formal verification

The deduction of Theorem 1.1 from the seven stated hypotheses is formalized in Lean 4 with Mathlib at https://github.com/sthubbar/lean-lab-preprints, commit 74c2d1a. The diagonal estimate of Lemma 3.2 is formalized conditionally on BPTN and Ordinates14 as diag_u6806, the short interval mean square bound of Proposition 3.3 conditionally on ExplicitA, HadamardK, Ordinates14, and BPTN as theorem2_u6806, and the main result Theorem 1.1 conditionally on all seven hypotheses as goldbach_445_hsw_gZ in LeanLab/Routes/U1508Compose445.lean. The proof of Lemma 2.2 (HadamardK) uses the partial fraction expansion of $\xi'(s)/\xi(s)$ over all zeros and Binet’s formula for the digamma function. These ingredients were not formalized in this project, so HadamardK enters Lean as a hypothesis.

The headline theorem is in file LeanLab/Routes/U1508Compose445.lean, namespace LeanLab.Routes.U1508, and has the exact statement:

theorem goldbach_445_hsw_gZ {Z : N → Finset ZIdx}
(hE : RiemannHypothesis → ∀ δ, 0 < δ → δ ≤ 1 / 10 ^ 13 →
  SmoothT2.ExplicitA gZ Z δ)
(hH : RiemannHypothesis → SmoothT2.HadamardK gZ)
(h14 : SmoothT2.Ordinates14 gZ)
(hB : RiemannHypothesis → Lemma26B.BPTN gZ)
(hEv : EvenGoldbachUpTo (4 * 10 ^ 18))
(hN : HSWN70 gZ) (hHd : HSWHead14 gZ) :
RiemannHypothesis → ∀ x : R, 3 ≤ x →
  ∃ n : N, IsGoldbachNumber n ∧ x < n ∧
  (n : R) < x + 4.45 * Real.log x ^ 2

Here gZ is the family of ordinates of the nontrivial zeros of $\zeta(s)$ with multiplicity; ExplicitA states (3) of Lemma 2.1 as the limit of $-\sum_{\rho\in Z_n}c_\delta(\rho)y^\rho$ along truncations $Z_n$, for almost every $y\ge2$, with $B(y)$ included as the function Bf, assumed under RH for each $0<\delta\le10^{-13}$; HadamardK is Lemma 2.2; Ordinates14 states that every ordinate has absolute value at least 14; BPTN is Lemma 2.4 for $T\ge10^{13}$; HSWN70 and HSWHead14 are [5 Corollary 1.2] read as counts of ordinates of both signs, for $T\ge70$ and $T\ge14$; and EvenGoldbachUpTo is Lemma 2.6. The bound SchoenfeldTheta is not a hypothesis of this theorem. Table 3 lists the status of each hypothesis in the paper and in Lean; the formal verification is conditional on these seven hypotheses, and the main theorem assumes ExplicitA, HadamardK, and BPTN under RH.

Structure of the Lean formalization

The formal proof is organized along the following chain of Lean 4 files and theorems; items 1 to 4 are in LeanLab/ChirreHagen2025/ and items 5 and 6 in LeanLab/Routes/:

1. U1263Core.lean (namespace LeanLab.ChirreHagen2025.U1263) proves piece_sum (the piece bound (20)), pt_raw, pt_norm, and one_sub_cos_le, while U6743Core.lean provides U6743.hu_pi:

lemma piece_sum (hN : BPTN γ) (h14 : Ordinates14 γ) {δ : ℝ} (hδ : 0 < δ)

(hδ1 : δ ≤ 1 / 10 ^ 13) (A B Q lam : R) (hA : 1 ≤ A) (hAB : A ≤ B)
(hlam : Real.log B ≤ lam) (hlam5 : lam ≤ 5) (hQ : 0 ≤ Q)
(hc : ∀ i, A / δ < |γ i| → |γ i| ≤ B / δ →
  ∥cδ γ δ i∥ ^ 2 ≤ Q * δ ^ 2)
(s : Finset ι) :
∑ i ∈ s.filter (fun i => A / δ < |γ i| ∧ |γ i| ≤ B / δ),
  ∥cδ γ δ i∥ ^ 2 * Real.log |γ i|
  ≤ 0.31831 * (Q * (B - A)) * (δ * Real.log (1 / δ) ^ 2
      + (2 * lam - 1.8) * (δ * Real.log (1 / δ))
      + (lam ^ 2 - 1.8 * lam) * δ)
    + 2 * Q * (δ ^ 2 * (Real.log (1 / δ) + 5) ^ 2)

lemma pt_raw ... (A B Q u : R) (hA : 1 ≤ A)
  (hu : ∀ t, A * (1 - 1 / 10 ^ 13) < t → t ≤ B →
    1 - Real.cos t ≤ u)
  (hQ : (1 / 10 ^ 26 + 2 * (1 + 1 / 10 ^ 13) * u) / A ^ 2 ≤ Q) :
  ∀ i, A / δ < |γ i| → |γ i| ≤ B / δ → ∥cδ γ δ i∥ ^ 2 ≤ Q * δ ^ 2
lemma pt_norm ... (A B lo Q : R) (hA : 1 ≤ A) (hlo0 : 0 ≤ lo)
  (hlo : lo ≤ A * (1 - 1 / 10 ^ 13))
  (hQ : 2 * (1 + 1 / 10 ^ 13) *
    (1 / 2 - lo ^ 2 / 24 + B ^ 4 / 720) + 1 / 10 ^ 26 ≤ Q) : ...
lemma one_sub_cos_le (x : R) :
  1 - cos x ≤ x ^ 2 / 2 - x ^ 4 / 24 + x ^ 6 / 720

(2) The 2161 pieces on $[1, 139.984375]$ are spread over nine split files U6806DiagASpS1.lean to U6806DiagASpS3.lean, U6806DiagBSpS1.lean to U6806DiagBSpS3.lean, and U6806DiagCSpS1.lean to U6806DiagCSpS3.lean, with 241, 240, 240, 240, 240, 240, 259, 259, and 202 applications of piece_sum, respectively. Table 4 gives three representative pieces exactly as certified in Lean.

(3) U6806DiagCSpS3.lean (namespace LeanLab.ChirreHagen2025.U6806) assembles the diagonal bound diag_u6806, conditional on BPTN and Ordinates14:

theorem diag_u6806 (hN : BPTN γ) (h14 : Ordinates14 γ) {δ : R}
  (hδ : 0 < δ) (hδ1 : δ ≤ 1 / 10 ^ 13) (s : Finset ι) :
  ∑ i ∈ s, ∥cδ γ δ i∥ ^ 2 * Real.log |γ i|
    ≤ 1.0068 * δ * Real.log (2.0001 / δ) ^ 2

(4) U6806Theorem2Sp.lean (namespace LeanLab.ChirreHagen2025.SmoothT2) proves the short interval mean square bound theorem2_u6806:

theorem theorem2_u6806 {γ : ι → R} {Z : N → Finset ι}
  (hE : ∀ δ, 0 < δ → δ ≤ 1 / 10 ^ 13 → ExplicitA γ Z δ)
  (hH : HadamardK γ) (h14 : Ordinates14 γ)
  (hN : Lemma26B.BPTN γ) :
  ∀ x δ : R, 10 ^ 13 ≤ x → 0 < δ → δ ≤ 1 / 10 ^ 13 →
    ψψ x δ ≤ 1.0069 * δ * Real.log (2.0001 / δ) ^ 2 * x ^ 2

(5) U1505Theta6HSW.lean (namespace LeanLab.Routes.U1505) proves the bilinear reduction theorem goldbach_445_of_J_hsw.

(6) U1508Compose445.lean (namespace LeanLab.Routes.U1508) applies LeanLab.Routes.U1505.goldbach_445_of_J_hsw to SmoothT2.theorem2_u6806 to obtain the headline theorem goldbach_445_hsw_gZ.

Running #print axioms for goldbach_445_hsw_gZ, theorem2_u6806, and goldbach_445_of_J_hsw in Lean 4 prints only the standard foundational axioms of Lean and Mathlib: propext, Classical.choice, and Quot.sound. The Lean code was written with AI assistance and checked by the Lean kernel.

Use of AI

The argument and the text of this paper were developed with AI tools; the main deduction is checked in Lean 4 as described in the appendix.

Data availability

The Lean source of every theorem named in this paper, with its full import closure and the original build log, is public at https://github.com/sthubbar/lean-lab-preprints, commit 74c2d1a; the headline theorem is in LeanLab/Routes/U1508Compose445.lean and Papers/GoldbachRH445.lean prints its statement and axioms. The README states exactly what the Lean proves and which inputs are hypotheses.

References

Email address: [email protected]