Bounded gaps between primes

Bounded gaps between primes is the subject of an OpenAI preprint dated 30 August 2026, Improved short gaps between primes, published outside the openai/math collection together with a conditional Lean 4 formalization and a numerical certificate. Writing H₁ for the lower limit of the differences p_n+1 − p_n between consecutive primes, the preprint claims H₁ ≤ 186. The unconditional record since Polymath 8b (2014) had been 246. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

The original result

Claim. DHL[40, 2] holds: every admissible set of forty integers has infinitely many translates containing at least two primes (Theorem 1.1). Applied to the admissible 40-tuple {0, 2, 6, 12, 20, 26, 30, 32, 36, 42, 48, 50, 56, 60, 68, 72, 78, 86, 90, 92, 98, 102, 110, 116, 120, 126, 132, 138, 140, 146, 152, 156, 158, 162, 168, 170, 176, 180, 182, 186} of diameter 186, this gives H₁ ≤ 186 (Corollary 1.2). Source: Improved short gaps between primes (OpenAI, 30 August 2026, 39 pages). The abstract states that the proof is due to GPT 6 Astra.
Method, as summarized in the preprint. The argument keeps the enlarged-support square completion of Polymath 8b and widens the allowed divisor supports of the multidimensional Selberg sieve. The mixed terms then need distribution estimates beyond the Bombieri–Vinogradov range for moduli that are suitable least common multiples of divisor products; these are supplied by the singly and doubly densely divisible estimates of Polymath 8a and by a triply densely divisible adaptation of a bilinear estimate of Stadlmann (arXiv:2309.00425). A signed minorant criterion and a numerical optimization over "physical integrals" complete the proof of DHL[40, 2]. The preprint records that, in independent concurrent work, Stadlmann proves H₁ ≤ 240.
Formalization, as described by the repository. openai/PrimeGaps186 (commit 61340d0, 2 September 2026; Lean 4.34.0-rc2) states that its Lean development derives DHL[40, 2] and the gap bound (declarations PrimeGap186.dhl_40_2 and PrimeGap186.primeGapLiminf_le_186) conditionally on three explicit input axioms: a bound |Kl₃(c; p)| ≤ 3 for the normalized rank-three Kloosterman sum (cited to Deligne's theorem as stated in Katz's Gauss Sums, Kloosterman Sums, and Monodromy Groups, Theorem 4.1.1), a bound 8p√p on a correlation of two classical Kloosterman sums (cited to Fouvry, Kowalski and Michel, The Friedlander–Iwaniec character sum, Proposition 2), and a block of 104 outer and 45 inner numerical integral bounds plus three cap bounds (physical_integral_bounds). The README states that the cited estimates and the numerical computations have not been turned into Lean proofs of those inputs, that Comparator matched the three results to Challenge.lean with the six axioms permitted, and that Nanoda and Lean's kernel accepted the proofs.
Numerical certificate. The repository's Python program prime_gap_186_certificate.py recomputes the numerical inputs; the README names Python 3.12, NumPy 2.2.6, python-flint 0.9.0 and "a custom FLINT 3.6.0 build with corrected signed polynomial convolution (not bundled)", and states that a successful run does not discharge any Lean axiom. An accompanying document, Numerical certificate for prime gaps at most 186, is included as short_gaps_numerics.pdf.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 15 October 2026)
2026-08-31	J. Stadlmann, Bounded gaps between primes (arXiv:2608.31126, v1)	Concurrent independent work	The abstract states that combining the Bombieri–Vinogradov theorem with newer equidistribution estimates for smooth moduli gives H₁ ≤ 240.	arXiv v1. The OpenAI preprint cites this work as forthcoming.
2026-10-14 (last update)	Formal Conjectures pull request #5558 (felixpernegger, open)	Statement; status tracking	Adds a constant `C88a` (the least prime-pair difference occurring infinitely often) with the upper bound 186 marked as a research-solved statement citing the OpenAI preprint, noting that the external Lean formalization is conditional; the earlier bounds 246, 600 and 70,000,000 are linked to a separate Lean development recorded as conditional on the Bombieri–Vinogradov theorem.	Open pull request; not merged.

Notes

The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.