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 4 / 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. The linear sieve is used in the printed fixed level form; see Remark 1.

Author comments: Version 1.8 of the note, skipping 1.7. Adds Remark 1 and an abstract sentence: the proof of the linear sieve Theorem 4 passes to sifting level p below z, so it uses inequality (2) at every level, while Theorems 5 to 7 check (2) at level z only; the note uses Theorem 4 in its printed fixed z form as a hypothesis, claims no error in the source, and the question is open. Adds a proof block for Theorem 1, the full brackets, and a list of deviations from the printed statements. Replaces the near the limit sentence: the sieve table of Bordignon, Johnston and Starichkova would give about 13.345 by script, not certified in Lean. Headline unchanged. 21 pages.

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, with edits by Claude; Claude checked each round against the Lean source, the build logs and the journal pages. No human expert has verified the transcriptions of the journal's Theorems 4 to 7. Version 4 of this record is version 1.8 of the note. It adds Remark 1 on the level at which the linear sieve input is used, which is an open question with no error claimed in the source, and corrects the points listed in the author comments. The headline is unchanged. Version 2 had corrected version 1, whose transcription of Theorems 5 to 7 omitted 0 < eps < 1/63 and N even. 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.02760v5 and aixiv.261026.000001 v1.8.

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. v1 · 7 pagesSubmitted by Steve HubbardInitial depositSupersededOct 26, 2026
  2. v2 · 20 pagesSubmitted by Steve HubbardSubmitted as a new versionSupersededOct 29, 2026
  3. v3 · 19 pagesSubmitted by Steve HubbardSubmitted as a new versionSupersededOct 31, 2026
  4. v4 · 21 pagesSubmitted by Steve HubbardVersion 1.8 of the note, skipping 1.7. Adds Remark 1 and an abstract sentence: the proof of the linear sieve Theorem 4 passes to sifting level p below z, so it uses inequality (2) at every level, while Theorems 5 to 7 check (2) at level z only; the note uses Theorem 4 in its printed fixed z form as a hypothesis, claims no error in the source, and the question is open. Adds a proof block for Theorem 1, the full brackets, and a list of deviations from the printed statements. Replaces the near the limit sentence: the sieve table of Bordignon, Johnston and Starichkova would give about 13.345 by script, not certified in Lean. Headline unchanged. 21 pages.CurrentNov 05, 2026