qedbot

Analytic number theory·primes:bounded-gaps

Bounded gaps between primes

record target minimiserecord held by a machine F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through a Comparator challenge and an alignment table.

The smallest H for which infinitely many pairs of consecutive primes are at most H apart. The twin prime conjecture says H is 2; before 2013 no finite bound was known.

Source

Record history

8 steps·gap between consecutive primes, lower is better
1001,00010k100k1M10M100M20152020202570,000,000, Yitang Zhang, 2013-054,680, Polymath8a, 2013-07600, James Maynard, 2013-11-19246, Polymath8b, 2014240, Julia Stadlmann, 2026-08-31236, Shiva Kintali, with Claude, ChatGPT, Codex and open-weight models, 2026-09-01212, François Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin Swaminathan, Jesse Thorner and Yunzhou Xie (Axiom Math), with AxiomProver, 2026-09-03186, GPT-6 Astra (OpenAI), 2026-09-03
Ink marks are steps by people and clay marks steps where AI took part; grey marks did not move the record, and hollow marks are candidates. How frontiers are drawn

Zhang gave the first finite bound in 2013, and within a year the Polymath projects and Maynard's multidimensional sieve brought it to 246, where it stayed for twelve years. On 31 August 2026 Julia Stadlmann posted 240. Within three days Shiva Kintali, directing several AI models, reached 236; Axiom Math reached 212, with a Lean certificate of the deduction produced by AxiomProver; and OpenAI released a report reaching 186, which it says is due to GPT-6 Astra. Science News reports that OpenAI's release came within two hours of Axiom's announcement, on 3 September, and the two steps are ordered that way here.

186

GPT-6 Astra (OpenAI)·3 Sep 2026·Source·Artifact

The report, dated 30 August, says the proof is due to GPT 6 Astra; its Lean formalisation is conditional on stated numerical bounds and exponential-sum estimates. Science News reports it was released with the model on 3 September, within two hours of Axiom's announcement.

AI took partbest known
212

François Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin Swaminathan, Jesse Thorner and Yunzhou Xie (Axiom Math), with AxiomProver·3 Sep 2026·Source

Builds on Stadlmann's work. AxiomProver generated a Lean certificate of the deduction from natural-language specifications, taking the equidistribution estimates as hypotheses, as Appendix A of the preliminary draft says.

AI took partmoved the record
236

Shiva Kintali, with Claude, ChatGPT, Codex and open-weight models·1 Sep 2026·Source·Artifact

Extends Stadlmann's framework with exactly checked computer certificates. The paper's statement on AI: a harness the author built directed several models, and the author is responsible for the proofs and the code.

AI took partmoved the record
240

Julia Stadlmann·31 Aug 2026·Source

Combines the Bombieri–Vinogradov theorem with newer equidistribution estimates for smooth moduli.

moved the record
246

Polymath8b·2014·Source

Published in Research in the Mathematical Sciences in 2014; the record for twelve years.

moved the record
600

James Maynard·19 Nov 2013·Source

The multidimensional sieve, needing only the Bombieri–Vinogradov theorem; published in the Annals of Mathematics in 2015.

moved the record
4,680

Polymath8a·Jul 2013·Source

Reached by the Polymath8a project in 2013, sharpening Zhang's method; published in Algebra & Number Theory in 2014.

moved the record
70,000,000

Yitang Zhang·May 2013·Source

The first finite bound; published in the Annals of Mathematics in 2014.

moved the record

AI activity

How grades work
Claude, ChatGPT, Codex

1 Sep 2026·with Shiva Kintali

Proved that infinitely many pairs of consecutive primes are at most 236 apart, improving Stadlmann's 240.

superseded A1 V2 F2
Reasoning and sources

Autonomy

The author ran a harness directing several models, corrected and redirected them, and takes responsibility for the proofs and the code, as the paper's statement on AI use says.

AxiomProver

3 Sep 2026·with François Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Yunzhou Xie

Proved a bound of 212, building on Stadlmann's work, with a Lean certificate of the deduction.

superseded A1 V2 F2
Reasoning and sources

Autonomy

The mathematics is the authors'; AxiomProver played a supporting role, producing the Lean certificate of the deduction from their natural-language specifications (Appendix A).

Details

formalisation: A Lean certificate of the deduction, taking the equidistribution estimates as hypotheses

GPT-6 Astra

3 Sep 2026

Proved that infinitely many pairs of consecutive primes are at most 186 apart.

record A3 V2 F2
Reasoning and sources

Autonomy

OpenAI's report says the proof is due to GPT 6 Astra and describes no human contribution to it.

Details

formalisation: Lean 4, conditional on stated numerical integral and cap bounds and on exponential-sum estimates

F2 declared. The correspondence is declared through a Comparator challenge and an alignment table.

declares axioms beyond the standard three: PrimeGap186.kloosterman2_correlation_bound, PrimeGap186.kloosterman3_bound, PrimeGap186.physical_integral_bounds reviewed by its authors only

Declared by the projects

1

As each project's formalization.yaml states it.

PrimeGaps186openai/PrimeGaps186 · joined by artifact · no independent check

Read formalization.yaml

authors
OpenAI
method
agent — GPT 6 Astra
review
self-assessed
axioms
Classical.choice, PrimeGap186.kloosterman2_correlation_bound, PrimeGap186.kloosterman3_bound, PrimeGap186.physical_integral_bounds, Quot.sound, propext
results
3 main results named, checked with Comparator, with an alignment table
sources
Improved Gaps Between Primes — formalizes; Numerical certificate for prime gaps at most 186 — adapts
checked by
nobody independent of its authors yet

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Recorded elsewhere

Compare the registries
  • vibemathed — Prime Gaps at Most 186

    formal-reported·machine-led·their labels: lean-checked, ai-discovered

Sources

Cite this record

qed.bot, “Bounded gaps between primes”, https://qed.bot/t/primes-bounded-gaps, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.