Primary evidence
- Improved short gaps between primesS1 · Primary research · Paper · 2026-08-30
- Prime Gaps at Most 186S1 · Primary research · Repository
- PrimeGaps186 formalization metadataS1 · Primary research · Formal artifact
GPT-6 Astra is credited with improving the bounded prime-gap record to 186
The public PrimeGaps186 repository contains a Lean 4 development for DHL[40,2] and the 186 prime-gap consequence together with a Python/FLINT numerical certificate.
What happened?
OpenAI's 30 August 2026 preprint claims that GPT-6 Astra found a proof establishing DHL[40,2], which, when applied to an explicit admissible 40-tuple of diameter 186, yields liminf_(n->infinity)(p_(n+1)-p_n) <= 186 for consecutive prime gaps. The result improves the prior 246 record associated with Polymath8b and predates Julia Stadlmann's independently obtained 240 bound by one day.
The public PrimeGaps186 repository contains a Lean 4 development for DHL[40,2] and the 186 prime-gap consequence together with a Python/FLINT numerical certificate. The registered main Lean declarations contain no sorry, and OpenAI reports that Comparator, Nanoda and Lean's kernel accepted the conditional proofs. The formal development nevertheless depends on three explicit project axioms: a rank-three hyper-Kloosterman estimate, a rank-two Kloosterman correlation estimate, and a collection of physical-integral and cap bounds. The first two are attributed to established literature; the numerical input is checked by the companion certificate rather than proved inside Lean. OpenAI's own metadata labels the review self-assessed and states that no independent human semantic review had been completed.
Why it matters
The bounded-prime-gap problem is one of the best-known modern examples of sustained progress on the distribution of primes. Moving the unconditional published record from 246 to 186 after roughly twelve years would be mathematically notable on its own; having the proof publicly attributed to a frontier AI model makes the event a direct test case for AI systems contributing new frontier mathematics. The accompanying formal artifact also illustrates a new verification boundary: machine checking can strongly validate a large conditional derivation while still leaving cited and numerical inputs outside the proof assistant.
Significance rationale: This result is a Historical Milestone because it is an AI-attributed advance on a prominent frontier problem in analytic number theory rather than a benchmark or a reformulation of known mathematics. The OpenAI preprint claims the bound liminf(p_(n+1)-p_n) <= 186, improving the long-standing 246 record of Polymath8b; Terence Tao's Optimization Problems record lists 186 as the current best known upper bound and notes that 246 had stood for twelve years. The result is accompanied by a substantial Lean and numerical verification artifact. Historical significance is recorded separately from the still-incomplete verification of the mathematical inputs and provenance.
Historical context
Earlier developments
—
Later developments
—
Evidence & status at a glance
- Significance
- H1 · Historical milestone
- Verification
- Under verification
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- New result
- Interface
- Informal, Formal, Symbolic, Hybrid
- AI contribution
- OpenAI and the public formalization metadata attribute the proof to GPT-6 Astra operating through Codex. The metadata also states that the artifact was refined through human-guided edits and automated proof checks. This AI-role classification records the disclosed workflow; it does not mean that Chronicle independently reconstructed the full model-human derivation trace.
- Human contribution
- Humans selected and released the research target and artifacts, guided refinement of the generated formal development, connected unproved mathematical estimates to the literature, and built or reviewed the numerical-certificate and checking pipeline. The public metadata does not provide a complete person-by-person division of intellectual labor.
- Verification
- Under verification · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-27
Technical details
- Systems
- gpt-6-astra, lean, comparator, nanoda
- Organizations
- openai
- Problems
- bounded-prime-gaps
- Methods
- maynard-tao-sieve, multidimensional-selberg-sieve, prime-equidistribution, numerical-optimization, formal-verification
Sources & artifacts
- Improved short gaps between primesS1 · Primary research · Paper · accessed 2026-09-27
- Prime Gaps at Most 186S1 · Primary research · Repository · accessed 2026-09-27
- PrimeGaps186 formalization metadataS1 · Primary research · Formal artifact · accessed 2026-09-27
- Bounded prime gap constantS3 · Independent scholarly · Independent analysis · accessed 2026-09-27
- PrimeGaps186 Lean 4 developmentArtifact · Proof artifact
- Prime-gap numerical certificateArtifact · Supplement
Verification history
- 2026-08-30 · Paper released · E3 · Inspectable artifact
OpenAI released the preprint and a public Lean/numerical verification artifact. The repository records machine-checked conditional proofs of DHL[40,2] and the 186 bound, with three explicit non-standard input axioms.
- 2026-09-27 · Under verification · E3 · Inspectable artifact
Terence Tao's Optimization Problems record independently lists 186 as the current best known bounded-prime-gap upper bound, records the 30 August preprint and the GPT-6 Astra attribution, and separately documents the same three-axiom formalization caveat. Chronicle has not located an independent semantic review or full replay that discharges the project inputs, so the Event remains under verification rather than independently_verified.
Corrections
No corrections recorded.