OpenAI Pushed the Bound on Short Prime Gaps From 246 to 186: Both Papers Credit the Proof to GPT-6 Astra

OpenAI released two new results on gaps between prime numbers alongside its GPT-6 Astra announcement on September 3, 2026. The first establishes that infinitely many consecutive prime pairs fall within 186 of each other, improving on 246, which had stood as the best known bound for more than a decade. The second concerns the opposite extreme, unusually large gaps, and improves Rankin's classical lower bound by a factor of log₂X. Both papers carry the same sentence in their abstracts: "The proof is due to GPT 6 Astra." ASAP works only from OpenAI's published papers and GitHub repositories to separate what was actually proved from what was not, and to show how differently the two results are verified.

The drop from 246 to 186 sits on top of more than a decade of prior work

The paper "Improved short gaps between primes" is dated August 30, 2026 and lists OpenAI as its author. What it proves is that lim inf(pₙ₊₁ − pₙ) ≤ 186, where pₙ denotes the nth prime. The twin prime conjecture asserts that this same quantity equals 2, so the new result lowers a bound rather than settling the conjecture.

The paper lays out its own lineage. Goldston, Pintz and Yıldırım showed that the limit inferior of (pₙ₊₁ − pₙ)/log pₙ is zero, and Zhang built on that sieve method to prove the first unconditional bound of under 70,000,000. Polymath 8a strengthened the distribution estimates and refined the sieve, cutting the bound to 4,680. Maynard's multidimensional Selberg sieve, developed independently by Tao, gave 600 using only the Bombieri-Vinogradov theorem, and Polymath 8b brought it to 246. OpenAI's footnote credits Julia Stadlmann with a recent improvement to 240, and the paper itself notes that Stadlmann proves 240 in independent concurrent work.

The paper is equally explicit about where 186 comes from. Its central theorem is that DHL[40, 2] holds, meaning every admissible 40-element set has infinitely many translates containing at least two primes. The paper exhibits a specific admissible set of 40 integers running from 0 to 186, and since that set has diameter 186, the bound follows. The technical gain came from combining the equidistribution estimates of Polymath 8a and Stadlmann with complementary factorization conditions that make certain products triply densely divisible, which permitted a larger support for the multidimensional Selberg sieve and an improved numerical optimization.

The second result works the opposite end, where primes spread furthest apart

OpenAI's second paper, "Improved long gaps between primes," proves that for all sufficiently large X, the largest gap G(X) between consecutive primes not exceeding X is at least a constant times log X(log₂X)²log₄X/(log₃X)², where logⱼ denotes the j-fold iterated logarithm. That is the opposite extreme from the first result: how far apart primes can spread rather than how tightly they cluster.

This lineage runs even longer. Westzynthius first proved that G(X)/log X diverges to infinity, Erdős obtained log X log₂X/(log₃X)², and Rankin improved that by a factor of log₄X. Erdős wrote about the difficulty of improving Rankin's estimate and later asked whether its constant could be made arbitrarily large, originally offering a $10,000 prize for the improvement. That question was settled independently by Maynard and by Ford, Green, Konyagin and Tao, whose subsequent joint work gave a quantitative bound. The new Theorem 1.1 improves Rankin's estimate by a factor of log₂X. OpenAI's footnote summarizes this as Astra improving a term in a bound that had remained unchanged for more than 80 years.

One entry in the bibliography deserves attention on its own. Reference 13 is authored by GPT 5.6 Sol, titled "A tilted residue-class construction for long prime-free intervals," and listed as a preprint posted to the Erdős Problems website for problem 4. The new result stands on the bound that argument produced. A chain in which one model's output is cited by the next model's paper has already taken formal shape inside a reference list.

The abstracts assign the proof to the model, not to any person

Both papers list only the institution, OpenAI, in the author position, and both hand the proof's attribution to the model in the abstract's closing sentence. That is a different move from a conventional acknowledgment or a tool-use disclosure, because it splits authorship from proof authorship and puts a product name in the second slot.

Reading this only as favorable framing misses what it costs. As long as the author remains the institution, responsibility for errors stays with OpenAI. But assigning the creative contribution to the model rather than the institution means that under ordinary academic authorship criteria, this result has no human author at all. Whether the mathematical community accepts that form is a question independent of whether the results are correct, and these two papers raise it in document form rather than sidestepping it. Set against Anthropic's own framing of its Fermat's Last Theorem formalization, where the company stated plainly that the novelty was verification rather than new mathematics, OpenAI's attribution here moves one step further in the opposite direction.

The two Lean formalizations in the same announcement guarantee different things

The announcement says proofs, abridged chains of thought, and verification materials are being shared for both results, but the two formalizations do not cover the same ground. The short gaps paper states that its Lean 4 formalization of Theorem 1.1 is conditional, resting on numerical integral and cap bounds and on finite-field exponential-sum estimates that ultimately come from Deligne's results on the Riemann hypothesis over finite fields. The repository openai/PrimeGaps186 holds that formalization with the precise exponential-sum bounds of Lemma A.4 stated as explicit assumptions, a Python-FLINT program that verifies the numerical bounds, and a separate numerical certificate PDF with coefficient tables, interval algorithms and complete verification records. The long gaps paper, by contrast, states that openai/LongGapsBetweenPrimes contains a complete Lean proof of its Theorem 1.1.

That distinction is not a technicality. In a conditional formalization, what the Lean compiler certifies is an implication: if the listed assumptions hold, the conclusion follows. The truth of the assumptions themselves lives outside the compiler, and here those assumptions rest on two different kinds of ground, a deep theorem of Deligne on one side and numerical computation on the other. So the single phrase "the AI proof was machine-checked" points at two different things across these papers. The long gaps claim can be read at face value; the short gaps claim has to be read together with its assumption list. Both repositories are Apache-2.0 and were created on September 2, 2026, carrying 146 and 35 stars respectively as of September 8, 2026, so anyone can check the distinction directly.

The inputs the papers cite rule out any solo-breakthrough summary

Compressing this into "an AI solved a long-standing problem on its own" contradicts the papers themselves. The raw material for the short gaps improvement is the equidistribution estimates of Polymath 8a and Stadlmann; what is new is the factorization conditions, the widened sieve support, and the numerical optimization. That is closer to swapping parts into an existing machine to raise its output than to building a new one. The long gaps paper likewise stands successively on Erdős and Rankin's constructions, the solutions of Maynard and of Ford, Green, Konyagin and Tao, and the GPT-5.6 Sol preprint.

Stadlmann's independent proof of 240 in the same season belongs in the same reading. A human researcher moved from 246 to 240 while the model moved from below 240 down to 186, and those two stretches overlap in time. What follows from that is not a scoreboard of humans against machines but a shift in where the bottleneck sits. Progress in this lineage has for years depended less on having an idea than on being able to push massive combinatorial optimization and case analysis all the way through, and that is precisely the part large models have started to absorb cheaply.

The distance between 186 and 2 is still 184

The size of the number is worth stating plainly. The twin prime conjecture asserts 2 and the new bound is 186, leaving a factor of 93. Most of the improvements to date have come from shaving constants inside the same sieve framework, and 186 is a value inside that framework as well. It has long been understood in this area that the multidimensional Selberg sieve faces a ceiling within the Bombieri-Vinogradov range, and this paper too lowered its value by importing equidistribution estimates that reach beyond that range in order to widen the sieve's support.

So how close this brings anyone to the twin prime conjecture cannot be answered from the numbers alone. Moving from 246 to 186 is a refinement of an existing method rather than a methodological break, and the pattern this lineage has shown is that reaching 2 will require a different kind of idea. Read the other way, the sudden acceleration of refinement is itself the substance of this announcement. When the unit cost of shaving a constant falls, the judgment of which constants are worth shaving becomes relatively more expensive.

What research teams can actually open this week

The immediately usable asset here is the verification material rather than the arguments. Both GitHub repositories are open under Apache-2.0, so anyone can download the Lean 4 files, compile them, and see exactly where the assumption list ends. The short gaps repository is especially instructive because the separated lemma assumptions and the numerical verification program sit in one place, making it a working example of how to document a conditional formalization.

The work design to take from this is simple. When accepting model-produced output, check what kind of verification artifact comes with it first: whether the formalization is complete or conditional, whether the assumptions are stated explicitly if conditional, and whether a program ships alongside to reproduce the numerical part. Those three checks are not specific to mathematics papers. They transfer to any task with a checker, such as codebases with dense type checking and tests, or data transformations with explicit constraints. They do not transfer to work whose correctness rests on human judgment.

What has not been established yet

OpenAI's two prime gap papers leave at least three items without answers. First, peer review. Both are preprints published by OpenAI and are not presented as having cleared journal review, and the conditional nature of the short gaps formalization leaves its assumptions particularly open to independent scrutiny.

Second, search cost. OpenAI stated in its August 1 announcement that the tokens needed to find solutions to ten open problems amounted to roughly $2,000, but neither the announcement nor either paper gives a cost or runtime figure for these two results, and the volume of failed attempts is not disclosed either.

Third, the division of labor. The abstracts assign the proofs to the model, but neither paper describes how far human involvement extended into drafting the manuscripts, assembling the literature, or structuring the formalization files. If moving attribution toward the model is to become a standard form, a description of exactly that boundary has to travel with it.

Source: ASAP analysis based on footnotes 9 and 10 of OpenAI's official announcement "GPT-6 Astra: A new generation of intelligence" (September 3, 2026), the papers "Improved short gaps between primes" (August 30, 2026) and "Improved long gaps between primes," and the GitHub repositories openai/PrimeGaps186 and openai/LongGapsBetweenPrimes