\documentclass[11pt,reqno]{amsart}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{booktabs}
\usepackage{array}
\usepackage{url}

\DeclareUnicodeCharacter{03B1}{\ensuremath{\alpha}}
\DeclareUnicodeCharacter{03B5}{\ensuremath{\varepsilon}}
\DeclareUnicodeCharacter{2081}{\ensuremath{_1}}
\DeclareUnicodeCharacter{2082}{\ensuremath{_2}}
\DeclareUnicodeCharacter{211D}{\ensuremath{\mathbb{R}}}
\DeclareUnicodeCharacter{2264}{\ensuremath{\le}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\land}}

\newtheorem{theorem}{Theorem}
\theoremstyle{remark}
\newtheorem{remark}{Remark}

\title{A lower explicit threshold for Chen's theorem under GRH}
\author{Steve Hubbard}
\address{Independent Researcher}

\begin{document}

\begin{abstract}
Assume the Generalized Riemann Hypothesis (GRH). We show that every even integer $N \ge \exp(\exp(13.375))$ can be written as $N = p + P_2$, where $p$ is a prime and $P_2$ is either a prime or a product of two primes. This result is conditional on GRH and on Theorems 5, 6, 7 and Lemma 9 of Bordignon and Starichkova \cite{BS-RJ}, together with the auxiliary lemmas, Table 1 and display (6) of \cite{BS-RJ} that their Section 5.4 uses, used at new parameter values inside their own Section 5.4. It is not a new method; it is a re-choice of the parameters $u$ and $\alpha$ in their argument, combined with the observation that Chen's theorem itself needs only that the Section 5.4 main-term combination be positive, not that it exceed $4\cdot 10^{-3}$, because the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of their Corollary 1 (Section 5.5, p.\ 1241), which does not involve the threshold, gives $N = p + P_2$ as soon as $\pi_2(N) > \sqrt{N} + 1$. The arithmetic of Section 5.4 at the new parameters and the associated parameter range inequalities are verified unconditionally in Lean 4.
\end{abstract}

\maketitle

\section{Introduction}

In 1973, Chen \cite{Chen} proved that every sufficiently large even integer $N$ can be represented as
\[
N = p + P_2,
\]
where $p$ is a prime and $P_2$ is a prime or a product of two primes. While the binary Goldbach conjecture remains open, and this note makes no progress on it, substantial work has gone into making the threshold for Chen's theorem explicit.

The first explicit threshold for Chen's theorem was obtained by Yamada \cite{Yamada}. Unconditionally, the current record is due to Bordignon, Johnston and Starichkova \cite{BJS}, who established Chen's theorem for all even integers $N \ge \exp(\exp(32.7))$. Johnston and Starichkova \cite{JS} proved related explicit results on writing even integers as a prime plus an almost prime. In related formal work, a qualitative Lean 4 formalization of Chen's theorem with an existential, non-explicit threshold is claimed in the unrefereed repository \cite{Lean}.

Assuming the Generalized Riemann Hypothesis (GRH), Bordignon and Starichkova lowered the explicit threshold considerably. In the arXiv version \cite{BS-arXiv} (v1, the only arXiv version), they obtained the threshold $\exp(\exp(15.85))$ with lower-bound constant $4\cdot 10^{-4}$. In the published journal version \cite{BS-RJ} (Theorem 3, p.\ 1214), they proved under GRH that
\[
\pi_2(N) > 4\cdot 10^{-3} U_N \frac{N}{\log^2 N}
\quad\text{for } N > \exp(\exp(14)),
\]
from which their Corollary 1 (p.\ 1214) gives Chen's theorem for these $N$. We are not aware of a published GRH threshold below $\exp(\exp(14))$.

In this note we establish the threshold $\exp(\exp(13.375))$ under GRH. This is conditional on GRH and on Theorems 5, 6, 7 and Lemma 9 of Bordignon and Starichkova \cite{BS-RJ}, together with the auxiliary lemmas, Table 1 and display (6) of \cite{BS-RJ} that their Section 5.4 uses, used at new parameter values inside their own Section 5.4. It is not a new method. It is a re-choice of the parameters $u$ and $\alpha$ in their argument.

\begin{theorem}[Main statement]\label{thm:main}
Assume the Generalized Riemann Hypothesis, and assume Theorems 5, 6, 7 and Lemma 9 of Bordignon and Starichkova \cite{BS-RJ}, together with the auxiliary lemmas, Table 1 and display (6) of \cite{BS-RJ} that their Section 5.4 uses, used at new parameter values inside their own Section 5.4. Then every even integer $N \ge \exp(\exp(13.375))$ can be written as $N = p + P_2$, with $p$ a prime and $P_2$ a prime or a product of two primes.
\end{theorem}

\section{The parameter re-choice in Section 5.4 of \cite{BS-RJ}}

Throughout, $\pi_2(N)$, $\pi_2'(N)$, $U_N$, $X_2$, $y$, $u$, $A$, $\alpha_i$, $\varepsilon_1$, $\varepsilon(u)$, $C_1$, $C_2$, $\bar c$ and $\bar m$ are as in \cite{BS-RJ}, and $\gamma$ is Euler's constant.

We begin by recording what the paper of Bordignon and Starichkova \cite{BS-RJ} does in full detail:
\begin{itemize}
\item In \cite{BS-RJ}, Theorem 3, p.\ 1214, under GRH, they prove
\[
\pi_2(N) > 4\cdot 10^{-3} U_N \frac{N}{\log^2 N}
\]
for $N > \exp(\exp(14))$. Their Corollary 1 (p.\ 1214) gives Chen's theorem for these $N$, passing from $\pi_2(N)$ to $\pi_2'(N)$ via the relation $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ (Section 5.5, p.\ 1241).
\item Their Section 5.4, p.\ 1241, combines Theorem 5 (p.\ 1228, with proof on p.\ 1229), Theorem 6 (p.\ 1231), Theorem 7 (pp.\ 1234 to 1235), and Lemma 9 (p.\ 1227, the weighted sieve inequality of Chen that bounds $\pi_2(N)$ below by sifting functions, minus $2N^{7/8} + N^{1/3}$), and takes the parameters
\[
u = 1000, \quad \alpha_1 = \alpha_2 = \alpha_3 = 10^{-3}, \quad A = 10, \quad \varepsilon_1 = 10^{-20},
\]
together with $\varepsilon(1000) < 1/5235$, $C_1 = 113$, and $C_2 = 114$.
\item The arXiv version \cite{BS-arXiv}, v1, the only arXiv version, had the threshold $\exp(\exp(15.85))$, with constant $4\cdot 10^{-4}$.
\end{itemize}

All changes in the present note take place inside Section 5.4 of \cite{BS-RJ} (p.\ 1241):
\begin{enumerate}
\item We choose the parameters
\[
u = 1500, \quad \alpha_1 = \alpha_2 = \alpha_3 = 0.00256, \quad A = 10, \quad \varepsilon_1 = 10^{-20}.
\]
\item From display (6) of \cite{BS-RJ}, p.\ 1221, we have $\varepsilon(1500) < 1/8349$. An independent recomputation with primes to $10^9$ and an explicit tail bound gave $\varepsilon(1500) = 1/8349.32$.
\item We take $C_1 = 112$ and $C_2 = 114$, which is the row $\varepsilon^{-1} = 6100$ of Table 1 of \cite{BS-RJ}, pp.\ 1217 to 1218. This is valid since inequality (2) with $\varepsilon(1500)$ implies it with the larger $1/6100$; the journal itself pairs $\varepsilon(1000) < 1/5235$ with the row $4500$.
\item The key observation is that Chen's theorem itself needs only that the Section 5.4 combination be positive, not that it exceed $4\cdot 10^{-3}$: the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of Corollary 1 (Section 5.5, p.\ 1241), which does not involve the threshold, gives $N = p + P_2$ as soon as $\pi_2(N) > \sqrt{N} + 1$. Asking only for a positive constant lets $\log\log X_2$ drop to $13.375$.
\end{enumerate}

\begin{table}[htbp]
\centering
\caption{Comparison of Section 5.4 parameters in \cite{BS-RJ} and in this note.}
\label{tab:params}
\begin{tabular}{@{}lcc@{}}
\toprule
Quantity & \cite{BS-RJ}, \S5.4 & This note \\
\midrule
$\log\log X_2$ & $14$ & $13.375$ \\
$u$ & $1000$ & $1500$ \\
$\alpha_1 = \alpha_2 = \alpha_3 = \alpha$ & $10^{-3}$ & $0.00256$ \\
$A$ & $10$ & $10$ \\
$\varepsilon_1$ & $10^{-20}$ & $10^{-20}$ \\
Upper bound on $\varepsilon(u)$ & $\varepsilon(1000) < 1/5235$ & $\varepsilon(1500) < 1/8349$ \\
Table 1 row $\varepsilon^{-1}$ (pp.\ 1217 to 1218) & $4500$ & $6100$ \\
$(C_1, C_2)$ & $(113, 114)$ & $(112, 114)$ \\
\bottomrule
\end{tabular}
\end{table}

\subsection{Definition of the main-term constant $\mathrm{K3J}$}

We define $\mathrm{K3J}$ exactly as in the Lean formalization, with $g = e^\gamma$, $\varepsilon = 1/8349$, and $\bar{c}$ the constant of Lemma 15 of \cite{BS-RJ} satisfying $\bar{c} < 0.363084$:
\begin{equation}\label{eq:K3J}
\begin{aligned}
\mathrm{K3J} &= 8\,\Bigl( 2g\log(3-8\alpha)/(4-8\alpha) - \varepsilon C_2\cdot 3\, e^{8\alpha-2}/(4-8\alpha) \Bigr) \\
&\, - \tfrac12\cdot 8\Bigl( (1+5\cdot10^{-5}) \Bigl(\tfrac{g}{4}\bigl(\log 6 + \log\tfrac{3-8\alpha}{3-18\alpha}\bigr)/\bigl(\tfrac12-\alpha\bigr) + \log(8/3)\,\varepsilon C_1 \Bigr) \Bigr) \\
&\, - \tfrac12 \Bigl( 2g/\bigl(\tfrac12-\alpha\bigr) + 3\varepsilon C_1 \Bigr)\,\bar c.
\end{aligned}
\end{equation}
Here the factor $1 + 5\cdot 10^{-5}$ is the journal's Lemma 11 (p.\ 1228) factor on Theorem 6's $l_1$, p.\ 1231. In words, the three pieces of $\mathrm{K3J}$ are $8$ times the main term of Theorem 5, minus one half of $8$ times the main term $l_1$ of Theorem 6, minus one half of the main term of Theorem 7.

\subsection{Numerical evaluation at $\log\log X_2 = 13.375$ and $\alpha = 0.00256$}

At $\log\log X_2 = 13.375$ and $\alpha = 0.00256$, the relevant numerical values are as follows:
\begin{itemize}
\item $\log X_2 = e^{13.375} = 643707.69$; Lean proves $e^{13.375} \ge 643700$.
\item The binding condition, which is the second part of displays (19), (21), and (25) of \cite{BS-RJ}, is
\[
\alpha \log X_2 - 11 \log\log X_2 = 1500.767 \ge 1500 = u.
\]
At this $X_2$ the condition needs $\alpha \ge 0.0025588$, leaving a slack of $0.00047$ in $\log\log X_2$.
\item The main-term constant $\mathrm{K3J}$ defined in \eqref{eq:K3J} satisfies $\mathrm{K3J} > 10^{-4}$, proved in Lean; the Python value recorded in the Lean file is $1.586\cdot 10^{-4}$, and an independent recomputation gave $1.596\cdot 10^{-4}$.
\item With the terms $\mathrm{K3J}$ leaves out, namely the factors $1 + 1/y$ and the $1/\log^2 N$ terms of Theorems 6 and 7, which amount to about $6\cdot 10^{-6}$, the Python total is $1.535\cdot 10^{-4}$.
\end{itemize}

The error terms $2N^{7/8} + N^{1/3}$ in the lower bound for $\pi_2(N)$, and the term $\sqrt{N} + 1$ lost in passing from $\pi_2(N)$ to $\pi_2'(N)$, are negligible: against $9\cdot 10^{-5} U_N N/\log^2 N$ with $U_N > 0.37$ (Lemma 10 of \cite{BS-RJ}, p.\ 1227) their ratio is below $10^{5} \log^2 N \cdot N^{-1/8}$, whose logarithm at $\log N = 643707.69$ is about $11.5 + 26.8 - 80463.5 < 0$ and decreases for larger $N$. The remainder $R$ of bound (33) of \cite{BS-RJ}, p.\ 1241, measured against $U_N N/\log^2 N$, carries the factor $0.053\,\bar m(N,A,N^{1/8})(1+\varepsilon_1)^{1/2}/(U_N\log(1+\varepsilon_1)\log^{6} N)$ with $A = 10$; since $1/\log(1+\varepsilon_1)$ is about $10^{20}$, $\bar m \le 8$ by (31) of \cite{BS-RJ}, pp.\ 1239--1240, with $M_\varphi(D^*) \le 1.08$, and $\log^6 N > 10^{34}$ at $\log N = 643707.69$, this contribution is also negligible.

\begin{itemize}
\item Hence, on GRH and the cited results,
\[
\pi_2(N) > 9\cdot 10^{-5} U_N \frac{N}{\log^2 N} > 0
\]
for every even $N \ge \exp(\exp(13.375))$, and the inequality $\pi_2'(N) \ge \pi_2(N) - \sqrt{N} - 1$ from the proof of Corollary 1 of \cite{BS-RJ} (Section 5.5, p.\ 1241), which does not involve the threshold, then gives $N = p + P_2$.
\end{itemize}

\begin{remark}[Threshold with the printed constant $4\cdot 10^{-3}$ kept]
With the printed constant $4\cdot 10^{-3}$ kept, the same method at $u = 1500$ and $\alpha = 0.0024$ gives $\exp(\exp(13.45))$, with $\mathrm{K3J} = 0.0051793$ in Python and the binding condition $1517.3 \ge 1500$.
\end{remark}

\subsection{Verification of other parameter ranges at $13.375$}

All remaining parameter conditions required by the lemmas and theorems in \cite{BS-RJ} hold at $\log\log X_2 = 13.375$ and $\alpha_1 = \alpha_2 = \alpha_3 = \alpha = 0.00256$:
\begin{itemize}
\item Lemma 7, p.\ 1222, needs $z > \exp(2753)$; here $\log z \ge 80463$.
\item Theorem 5's proof, p.\ 1229, needs $s = 4 - 8\alpha_1 \in [3, 4]$ (here $s = 3.97952$) and $\log X_2 \ge (A+1)/\alpha = 4296.9$.
\item Theorem 6, p.\ 1231, needs $\alpha_2 < 1/24$ and $k_{\alpha_2} = 8(1/6 - \alpha_2) > 1$ (here $k = 1.31285$).
\item Theorem 7, pp.\ 1234 to 1235, display (25), needs $\log X_2 \ge 11/\alpha_3$, $\log X_2 \ge 544$ and $X_2^{1/48}/\log^{34/3} X_2 \ge 0.44$, which in log form is $13258.99 \ge -0.82$.
\item Remark 1, p.\ 1230, requires $H = \sqrt{N}/\log^{A+1} N \ge 10^8$, which follows from (19).
\item Lemma 11, p.\ 1228, needs $N \ge \exp(\exp(10))$.
\item Lemmas 12 and 13 need $X_2 \ge 4\cdot 10^{18}$.
\item Lemma 14, p.\ 1238, needs $y \ge 2657$.
\item Theorem 6's proof, p.\ 1234, needs $y \ge 286$.
\item Theorems 5 to 7 need $400 \le u \le 10^8$.
\end{itemize}
An independent second reading of the hypotheses found no range that holds at $\log\log X_2 = 13.45$ but fails at $13.375$.

\section{Formal verification, Lean 4}
\sloppy

AI wrote the Lean code; it was checked by the Lean kernel, Lean v4.35.0 with Mathlib v4.35.0. The Lean proves the arithmetic of Section 5.4 at the new parameters and the parameter ranges, unconditionally. It does not formalize GRH, the linear sieve, or the journal's Theorems 5 to 7 and Lemma 9; the step from these cited results plus the Lean inequalities to the main statement is done by hand in the paper.

All paths below are relative to the \texttt{LeanLab} repository root, within the namespace \texttt{LeanLab.BS2022GRH.Journal}.

The file \texttt{LeanLab/BS2022GRH/JournalMargin.lean} defines \texttt{K3J}:
{\footnotesize
\begin{verbatim}
noncomputable def K3J (α g ε C₁ C₂ cb : ℝ) : ℝ :=
  8 * (2 * g * log (3 - 8 * α) / (4 - 8 * α)
    - ε * C₂ * 3 * exp (8 * α - 2) / (4 - 8 * α))
  - 1 / 2 * (8 * ((1 + 5e-5)
    * (g / 4 * (log 6 + log ((3 - 8 * α) / (3 - 18 * α)))
    / (1 / 2 - α) + log (8 / 3) * ε * C₁)))
  - 1 / 2 * ((2 * g / (1 / 2 - α) + 3 * ε * C₁) * cb)
\end{verbatim}
}

The file \texttt{LeanLab/BS2022GRH/JournalPositive.lean} contains the three headline results:
{\footnotesize
\begin{verbatim}
theorem theorem3_positive_main :
    (0.0001 : ℝ)
      < K3J 0.00256 (exp eulerMascheroniConstant) (1 / 8349) 112 114
        LeanLab.ChenExplicit.BJS.cbar

theorem conditions_13375 :
    (1500 : ℝ) ≤ 0.00256 * exp 13.375 - 11 * 13.375
      ∧ 11 / 0.00256 ≤ exp (13.375 : ℝ)

theorem params_ok_13375 :
    (0.00256 : ℝ) < 1 / 24 ∧ (400 : ℝ) ≤ 1500 ∧ (1500 : ℝ) ≤ 10 ^ 8
      ∧ (0 : ℝ)
        < K3J 0.00256 (exp eulerMascheroniConstant) (1 / 8349) 112 114
          LeanLab.ChenExplicit.BJS.cbar
\end{verbatim}
}
In Lean, $e^\gamma$ is bracketed by $1.7810699 < e^\gamma < 1.7810725$, \texttt{LeanLab.Helfgott2013.GammaFine.exp\_gamma\_gt} and \texttt{exp\_gamma\_lt}, and $\bar{c} < 0.363084$ is \texttt{LeanLab.ChenExplicit.BJS.cbar\_lt}.

The file \texttt{LeanLab/BS2022GRH/RangeCheck13375.lean} proves eight range lemmas:
\texttt{lemma7\_range}, \texttt{display25\_first}, \texttt{display25\_third}, \texttt{remark1\_H}, \texttt{remark1\_H\_vacuity}, \texttt{mono\_step}, \texttt{mono\_range\_13375}, and \texttt{sieve\_ranges\_13375}. Two of these statements are:
{\footnotesize
\begin{verbatim}
theorem display25_first :
    max ((10 + 1) / (0.00256 : ℝ)) (48 * (10 + 4 / 3)) ≤ exp 13.375

theorem sieve_ranges_13375 :
    (3 : ℝ) ≤ 4 - 8 * 0.00256 ∧ 4 - 8 * (0.00256 : ℝ) ≤ 4
      ∧ (1 : ℝ) < 8 * (1 / 6 - 0.00256)
\end{verbatim}
}

The build logs are recorded in \texttt{LeanLab/BS2022GRH/build/}:
\begin{itemize}
\item \texttt{20261020T0802Z-20406-JournalPositive.log}: Build completed successfully, \texttt{EXIT 0}, \texttt{sorry} count $0$; \texttt{theorem3\_positive\_main}, \texttt{conditions\_13375}, and \texttt{params\_ok\_13375} each depend on axioms \texttt{[propext, Classical.choice, Quot.sound]}.
\item \texttt{20261020T1303Z-22201.log}, a fresh rebuild by a second run: \texttt{JournalPositive} and \texttt{RangeCheck13375} both \texttt{EXIT 0}, $0$ \texttt{sorry}, and all $11$ theorems depend only on \texttt{[propext, Classical.choice, Quot.sound]}.
\end{itemize}

Table \ref{tab:status} summarizes the verification status of each input to Theorem \ref{thm:main}.

\begin{table}[htbp]
\centering
\caption{Hypothesis and verification status.}
\label{tab:status}
\begin{tabular}{@{}p{0.44\textwidth}p{0.50\textwidth}@{}}
\toprule
Input & Status \\
\midrule
GRH & assumed \\
\addlinespace[3pt]
\cite{BS-RJ} Theorems 5, 6, 7 at the new parameters & cited, not formalized; their stated ranges checked at $13.375$, by hand on the published pages and in Lean \\
\addlinespace[3pt]
\cite{BS-RJ} Lemma 9 & cited, not formalized; no parameter hypotheses, p.\ 1227 \\
\addlinespace[3pt]
\cite{BS-RJ}, the step $\pi_2' \ge \pi_2 - \sqrt{N} - 1$ of Corollary 1 & cited, not formalized \\
\addlinespace[3pt]
$\varepsilon(1500) < 1/8349$ & computed in Python twice, not in Lean \\
\addlinespace[3pt]
$C_1 = 112, C_2 = 114$, Table 1 row $6100$ & read from the journal, not in Lean \\
\addlinespace[3pt]
omitted terms, about $6\cdot 10^{-6}$ & Python only \\
\addlinespace[3pt]
error terms $2N^{7/8} + N^{1/3}$, $\sqrt{N} + 1$ and the remainder of bound (33) & hand computation, negligible \\
\addlinespace[3pt]
$\mathrm{K3J} > 10^{-4}$ & proved in Lean, \texttt{theorem3\_positive\_main} \\
\addlinespace[3pt]
displays (19), (21), (25) at $13.375$ & proved in Lean, \texttt{conditions\_13375}, \texttt{display25\_first}, \texttt{display25\_third} \\
\addlinespace[3pt]
other ranges & proved in Lean, \texttt{RangeCheck13375.lean} \\
\bottomrule
\end{tabular}
\end{table}

\section*{Use of AI}

AI, namely Claude by Anthropic, wrote all Lean code and drafted the text; AI tools were used for the literature search; the statements, the numbers and the references were checked by independent AI checker passes against the Lean source and the published pages of \cite{BS-RJ}; the author is responsible for the content.

\section*{Data availability}

The Lean source is available from the author on request; a public repository entry is in preparation.

\section*{Acknowledgement}

The author thanks M.\ Bordignon and V.\ Starichkova for their paper \cite{BS-RJ}, whose method this note uses unchanged.

\begin{thebibliography}{9}

\bibitem{BS-RJ}
M.~Bordignon and V.~Starichkova,
\emph{An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis},
Ramanujan J.\ \textbf{64} (2024), no.~4, 1213--1242,
\url{https://doi.org/10.1007/s11139-024-00866-x}.

\bibitem{BS-arXiv}
M.~Bordignon and V.~Starichkova,
\emph{An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis},
arXiv:2211.08844, v1, 2022.

\bibitem{BJS}
M.~Bordignon, D.~R.~Johnston and V.~Starichkova,
\emph{An explicit version of Chen's theorem and the linear sieve},
Int.\ J.\ Number Theory \textbf{21} (2025), 2497--2572,
\url{https://doi.org/10.1142/S1793042125501192}; arXiv:2207.09452.

\bibitem{Chen}
J.~R.~Chen,
\emph{On the representation of a larger even integer as the sum of a prime and the product of at most two primes},
Sci.\ Sinica \textbf{16} (1973), 157--176.

\bibitem{JS}
D.~R.~Johnston and V.~V.~Starichkova,
\emph{Some explicit results on the sum of a prime and an almost prime},
Acta Math.\ Hungar.\ \textbf{177} (2025), 163--192,
\url{https://doi.org/10.1007/s10474-025-01572-w}; arXiv:2208.01229.

\bibitem{Lean}
subfish-zhou,
\emph{goldbach-lean},
\url{https://github.com/subfish-zhou/goldbach-lean}.

\bibitem{Yamada}
T.~Yamada,
\emph{Explicit Chen's theorem},
arXiv:1511.03409, 2015.

\end{thebibliography}

\end{document}