HEXAGONbeta

A lower explicit threshold for Chen's theorem under GRH

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

Contributed by Steve Hubbard

Version 2 / Oct 26, 2026 / CC BY 4.0

Abstract

Assume the Generalized Riemann Hypothesis (GRH). We show that every even integer N≥exp⁡(exp⁡(13.375))N \ge \exp(\exp(13.375)) can be written as N=p+P2N = p + P_2, where pp is a prime and P2P_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 (Ramanujan J. 64, 2024), together with their auxiliary lemmas, Table 1 and display (6) 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 uu 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⋅10−34\cdot 10^{-3}, because the inequality π2′(N)≥π2(N)−N−1\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+P2N = p + P_2 as soon as π2(N)>N+1\pi_2(N) > \sqrt{N} + 1. In Lean 4 the threshold statement itself is stated with GRH as an explicit hypothesis and proved conditional on the journal's Theorems 5, 6, 7 and the linear sieve Theorem 4 at the constants used; Lemma 9, the Section 5.5 step, ε(1500)<1/8349\varepsilon(1500) < 1/8349 and the Section 5.4 bracket arithmetic are proved in Lean. Theorems 5, 6, 7 and Theorem 4 are not formalized.

Provenance statement

An AI research lab run by Claude, Anthropic, found the parameter re-choice in Section 5.4 of Bordignon and Starichkova and wrote the Lean 4 check. Gemini Argon High, Google, drafted the LaTeX from Claude's briefs over eleven rounds; each round was checked by a fresh Claude session against the Lean source, the build logs and the journal pages, and the checker protocol is described in the paper. No human expert has verified the transcriptions of the journal's Theorems 4 to 7. Version 2 corrects version 1: the Lean statement is now stated with GRH as a hypothesis and proved conditional on the journal's Theorems 4 to 7; an earlier transcription of Theorems 5 to 7 omitted 0 < eps < 1/63 and N even, which made the conditional theorem vacuous, fixed and stated in Limitations. The Lean source, build logs and numerics script are public at github.com/sthubbar/lean-lab-preprints, commit 2fdf0dc, and the entry is registered in the Palomar registry as PALOMAR-2026-10-28-000016. Grok and DeepSeek were used only for the prior-art search. Also posted as aiXiv:2610.02760v2 and aixiv.261026.000001 v1.5.

References

  1. M. Bordignon and V. Starichkova, An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis , Ramanujan J.\ 64 (2024), no. 4, 1213--1242, https://doi.org/10.1007/s11139-024-00866-x.DOI
  2. M. Bordignon and V. Starichkova, An explicit version of Chen's theorem assuming the Generalized Riemann Hypothesis , arXiv:2211.08844, v1, 2022.arXiv
  3. M. Bordignon, D. R. Johnston and V. Starichkova, An explicit version of Chen's theorem and the linear sieve , Int.\ J.\ Number Theory 21 (2025), 2497--2572, https://doi.org/10.1142/S1793042125501192; arXiv:2207.09452.arXivDOI
  4. J. R. Chen, On the representation of a larger even integer as the sum of a prime and the product of at most two primes , Sci.\ Sinica 16 (1973), 157--176.
  5. D. R. Johnston and V. V. Starichkova, Some explicit results on the sum of a prime and an almost prime , Acta Math.\ Hungar.\ 177 (2025), 163--192, https://doi.org/10.1007/s10474-025-01572-w; arXiv:2208.01229.arXivDOI
  6. subfish-zhou, goldbach-lean , https://github.com/subfish-zhou/goldbach-lean.link
  7. J. B. Rosser and L. Schoenfeld, Approximate formulas for some functions of prime numbers , Illinois J.\ Math.\ 6 (1962), 64--94.
  8. T. Yamada, Explicit Chen's theorem , arXiv:1511.03409, 2015.arXiv

Version history

  1. v1Submitted by Steve HubbardInitial depositSupersededOct 26, 2026
  2. v2Submitted by Steve HubbardSubmitted as a new versionCurrentOct 29, 2026