Prime gaps at most 186, conditional on three unproved Lean axioms
An OpenAI repository derives a bound of 186 on infinitely many prime gaps in Lean, from three inputs it states as axioms rather than proving.
- Lab
- OpenAI
- Model
- GPT-6 Astra
- Field
- Mathematics
- Date
- 2026-09-02
- Problem posed
- 1849 · open 177 yrs
Sources
Original work
Independent commentary
What was found
This is numerically the strongest of three bounded prime-gap claims from the same window, ahead of the Axiom Math 212 recorded separately here and the 246 already in the registry, and it is the weakest evidentially. The development derives DHL[40,2], and so the bound, from three stated inputs. Those inputs are not proved in Lean: the repository's own README says the results remain conditional on three explicit input axioms and that the cited estimates and numerical computations have not been turned into Lean proofs.
Novelty check
The claimed bound is below every published figure in the bounded-gaps line, which runs through Polymath8b's 246 and Stadlmann's 240, and below the Axiom Math 212 from the same window. No earlier claim at 186 or lower was found in the four registries. Priority is not really the open question here; whether the claim is established at all is, and the caveats address that.
Caveats and known objections
The grade is capped by the artifact's own structure rather than by caution. Three load-bearing statements are axioms rather than theorems, so what the kernel establishes is an implication: granted those three, the bound follows. Until they are proved in Lean or cited to the literature, the development certifies a conditional statement, and the numerical work does not discharge the corresponding axiom. No human author is named on the repository, so nobody is on record as having reviewed it. Autonomy is ai-led rather than autonomous: the disclosure describes the model working to specific formalization instructions, including which inputs to retain as axioms, which is steering even without a named human.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Prime gaps at most 186, conditional on three unproved Lean axioms. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-02-prime-gaps-186BibTeX
@misc{whataifound-openai-2026-186,
title = {Prime gaps at most 186, conditional on three unproved Lean axioms},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-02-prime-gaps-186}
}