OpenFrontiers
Join
← Back to the index
OP-12104OpenNumber theory

Bounded prime gap constant (C88aC_{88a})

Bounded prime gap constant: determine C88aC_{88a} or improve its bounds; the repository records 2 (lower) and 186 (upper).

MSC 11N05 · Distribution of primes

Editorial MSC2020 classification. Original article codes and source evidence are recorded in the literature directory.

Licensed source statementAs of Repository table at commit 2c1968c (2026-09-26); open while the recorded lower and upper bounds differSource & evidence ↓
Read original source ↗ 0Submit progressLean 4 ↓Discussion (0)

Problem statement

Let pnp_n denote the nn-th prime. The bounded prime gap constant is

C88a  =  H1  :=  lim inf⁡n→∞(pn+1−pn),C_{88a} \;=\; H_1 \;:=\; \liminf_{n \to \infty} (p_{n+1} - p_n),

the least limit point of the sequence of gaps between consecutive primes. That H1H_1 is finite — that some bounded gap recurs infinitely often — was proved by Zhang [Zha14] in 2013; the twin prime conjecture is exactly the assertion H1=2H_1 = 2.

More generally one writes Hm:=lim inf⁡n→∞(pn+m−pn)H_m := \liminf_{n\to\infty}(p_{n+m} - p_n) for m≥1m \ge 1. Maynard [May15] proved HmH_m finite for every mm; the growth rate of HmH_m in mm is recorded separately as C88bC_{88b}.

Lean 4

Not yet attached

No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.

Share a formalization →Verification guide ↗

Background

  • Reading the table. Rows are in chronological order, not in order of strength, so the last row is not the record. The record is H1≤186H_1 \le 186 [OAI26], of 30 August 2026; the two 240240 rows on either side of it are independent proofs of the previous record, deposited on 28 and 31 August. Three of the four came within four days of each other and none cites the others.

  • Conditional bounds. Assuming the Elliott–Halberstam conjecture, H1≤12H_1 \le 12 [May15], improving the bound H1≤16H_1 \le 16 of Goldston–Pintz–Yıldırım [GPY09]. Assuming the generalized Elliott–Halberstam conjecture, H1≤6H_1 \le 6 [Pol14b]. Reaching H1=2H_1 = 2 by these methods is obstructed by the parity problem.

  • Where the numbers come from. Each upper bound is the diameter of an explicit admissible kk-tuple, for a kk that the sieve analysis determines; narrow admissible tuples are catalogued at Sutherland's tables. Improvements therefore come either from lowering the admissible kk (better sieve) or from finding a narrower tuple of that size.

  • Relation to C66C_{66}. The level of distribution of the primes is what drives all of these bounds, and C66=1C_{66} = 1 (Elliott–Halberstam) would give H1≤12H_1 \le 12. Note however that the equidistribution estimates actually used here — Zhang's, Polymath's 12+7300\tfrac12+\tfrac7{300}, and Stadlmann's 12+140\tfrac12+\tfrac1{40} — are for smooth (friable) moduli with well-factorable weights, and so do not lower-bound C66C_{66}, which is defined over all moduli q≤Qq \le Q. See the caution on the C88bC_{88b} page.

  • Formalization status of the 186186 bound. [OAI26] is accompanied by a Lean 4 development, openai/PrimeGaps186, in which PrimeGap186.dhl_40_2 and PrimeGap186.primeGapLiminf_le_186 carry no sorry. The proofs are nonetheless conditional on three declared axioms: the rank-three hyper-Kloosterman bound ∣Kl3(c;p)∣≤3\lvert \mathrm{Kl}_3(c;p)\rvert \le 3, which follows from Deligne's theorem as stated in Katz, Gauss Sums, Kloosterman Sums, and Monodromy Groups, Theorem 4.1.1; the rank-two Kloosterman correlation bound of Fouvry–Kowalski–Michel, Proposition 2; and 104104 outer plus 4545 inner physical-integral bounds together with three cap bounds, which are checked by an accompanying Python/FLINT certificate rather than proved in Lean. The first two are established results quoted from the literature; the third is the numerical part of the argument. The repository reports that Comparator, Nanoda and the Lean kernel accepted all three results, and describes its own review status as self-assessed, with no independent human semantic review.

  • Wikipedia page on Polignac's conjecture

References (from the repository page)

  • [GPY09] Goldston, Daniel A.; Pintz, János; Yıldırım, Cem Y. Primes in tuples I. Annals of Mathematics 170 (2009), no. 2, 819–862. DOI: 10.4007/annals.2009.170.819.
  • [Zha14] Zhang, Yitang. Bounded gaps between primes. Annals of Mathematics 179 (2014), no. 3, 1121–1174. DOI: 10.4007/annals.2014.179.3.7.
  • [Pol14a] D. H. J. Polymath. New equidistribution estimates of Zhang type. Algebra & Number Theory 8 (2014), no. 9, 2067–2199. DOI: 10.2140/ant.2014.8.2067. arXiv:1402.0811.
  • [Pol14b] D. H. J. Polymath. Variants of the Selberg sieve, and bounded intervals containing many primes. Research in the Mathematical Sciences 1 (2014), Art. 12. DOI: 10.1186/s40687-014-0012-7. Erratum: ibid. 2 (2015), Art. 15, DOI: 10.1186/s40687-015-0033-x. arXiv:1407.4897.
  • [May15] Maynard, James. Small gaps between primes. Annals of Mathematics 181 (2015), no. 1, 383–413. DOI: 10.4007/annals.2015.181.1.7.
  • [Sta25] Stadlmann, Julia. On primes in arithmetic progressions and bounded gaps between many primes. Advances in Mathematics 468 (2025), Paper No. 110190. DOI: 10.1016/j.aim.2025.110190. arXiv:2309.00425.
  • [Zha26] Zhang, Hanxin. A bound of 240 for gaps between primes. Preprint, 28 August 2026. Zenodo. DOI: 10.5281/zenodo.22135842. Computational certificate and verification code: https://github.com/hanxinzhang/prime-bound.
  • [Sta26] Stadlmann, Julia. Bounded gaps between primes. Preprint, 31 August 2026. arXiv:2608.31126.
  • [OAI26] OpenAI. Improved short gaps between primes. Preprint, 30 August 2026. PDF. Conditional Lean 4 formalization and Python numerical certificate: openai/PrimeGaps186 (Apache-2.0). A companion document, Numerical certificate for prime gaps at most 186, carries the coefficient tables and verification records.

Progress & source assessment

Repository table (commit 2c1968c, 26 September 2026): best known lower bound 2; best known upper bound 186. Values marked with an asterisk have minimal verification.

Known upper bounds

Bound Reference Comments
70 000 00070\,000\,000 [Zha14] The first finiteness proof, via a bounded-level equidistribution estimate for smooth moduli beyond the Bombieri–Vinogradov range.
46804680 [Pol14a] Polymath8a, by optimizing Zhang's equidistribution estimates.
600600 [May15] Maynard, via a multidimensional generalization of the Selberg sieve, using only Bombieri–Vinogradov. Obtained independently by Tao.
246246 [Pol14b] Polymath8b, generalizing the Maynard sieve further together with extensive numerical work. Stood as the record for twelve years.
240240 [Zha26] Zhang: proof discovered with GPT-5.6 Sol. Preprint publicly deposited on Zenodo on 28 August 2026, with an exact-arithmetic verification code released separately.
186186 [OAI26] Establishes DHL[40,2]\mathrm{DHL}[40,2]: every admissible 4040-tuple has infinitely many translates containing at least two primes. Combines the equidistribution estimates of [Pol14a] and [Sta25] with factorization conditions making suitable least common multiples of divisor products triply densely divisible, which widens the support of the multidimensional Selberg sieve, together with an improved numerical optimization. Applied to the admissible 4040-tuple {0,2,6,…,182,186}\{0, 2, 6, \dots, 182, 186\} of diameter 186186. Preprint of 30 August 2026, one day before [Sta26], which it describes as independent concurrent work; the proof is attributed to the model GPT 6 Astra. See the note on its formalization below.
240240 [Sta26] Stadlmann: independent proof using the Bombieri–Vinogradov theorem combined with newer equidistribution estimates for smooth moduli. Preprint of 31 August 2026.

Known lower bounds

Bound Reference Comments
22 Trivial pn+1−pn≥2p_{n+1} - p_n \ge 2 for every n≥2n \ge 2. Equality, H1=2H_1 = 2, is the twin prime conjecture.
References
  1. [1]Davis, Damek; Ivanisvili, Paata; Tao, Terence (maintainers). Optimization Constants in Mathematics, github.com/teorth/optimizationproblems (commit 2c1968c, 26 September 2026). — Bounded prime gap constant ($C_{88a}$) linkApache-2.0 (repository license); constant pages reproduced with attribution; repository references retained.

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Sign in to run an attempt. New accounts start with enough credits for ten.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.

Sign in to add a note.