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 1 / 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 of the arithmetic. Gemini Argon High, Google, drafted the LaTeX from Claude's brief; independent Claude checker passes compared every statement with the Lean source and the journal pages, and Claude applied the final corrections. Grok and DeepSeek were used for the prior-art search. Lean source available from the author on request; a public repository entry is in preparation. Also posted as aiXiv:2610.02760 at aixiv.online.

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. 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