Proved
Conditional formal endpoint for 186 ↗
The implication from the three stated input axioms.
Observed Oct 13, 2026
Theorem · version 3
A gap bound of 186 from explicit input assumptions
Statement
Assuming the rank-three Kloosterman estimate, the rank-two correlation estimate, and all integral and cap bounds in the precise forms specified by the cited proof, .
Assumptions
- The rank-three Kloosterman bound in the source.
- The rank-two correlation bound in the source.
- All source physical-integral and cap bounds.
Scope
A proved conditional deduction. The two literature estimates and numerical input remain project axioms; OpenMath has not verified or discharged them.
Explanation
Bounds & computations · 1
Compare the quantity and hypotheses within each group. A finite check, conditional theorem and proposed improvement cover different scopes.
| Result | Value | Conditions |
|---|---|---|
| A gap bound of 186 from explicit input assumptions → Proved Selected source date: | ≤ 186 | Conditional on the rank-three Kloosterman estimate, rank-two correlation estimate, and the precise integral and cap bounds in the cited proof. |
Evidence
Source reports
Formal proofs
Lean: 186 with three input axioms ↗
Complete formal proof reported externally
Complete as a conditional deduction. The formal input names are PrimeGap186.kloosterman3_bound, PrimeGap186.kloosterman2_correlation_bound and PrimeGap186.physical_integral_bounds; they remain assumptions, not discharged proof obligations.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
PrimeGap186.primeGapLiminf_le_186Commit 61340d0b74163003b32756bb16e91d9209a5e330
Connections
In this problem · publication v7 · Selected context
How small can prime gaps be? →
Conditional result · Proved
Scope: The formal source derives 186 only from its three documented mathematical input axioms.
Limit: Discharge or independently justify all input assumptions before treating this as an unconditional improvement.
Nested results concern the same prime-gap limit; they are not separate portions of a solved problem.
Relationship not independently reviewed. This concerns its use in this problem.
Sources
Prime gaps at most 186: a conditional Lean development →
- README input axioms and verification; PrimeGaps186.lean → · Original passage ↗
Recorded wording
The endpoint derives a gap bound of 186 from two unproved-in-Lean exponential-sum estimates and an unproved-in-Lean physical integral input. A separate numerical certificate does not discharge those axioms.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
OpenAI · PrimeGaps186 contributors · Project documentation · Publication date Sep 2, 2026
Public formal source; build and independent mathematical review are separate checks.
Prime gaps at most 186: a conditional Lean development — pinned source ↗No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Revision & attribution
Source revision: 61340d0b74163003b32756bb16e91d9209a5e330. Observed Oct 13, 2026.
The project is an OpenAI formal development. Its explicit assumptions and certificate work are recorded separately from an unconditional mathematical improvement.
Source updated Sep 2, 2026.
Prime gaps at most 186: a conditional Lean development — pinned source: 61340d0b74163003b32756bb16e91d9209a5e330.
Variants of the Selberg sieve, and bounded intervals containing many primes →
- Main bounded-gap results and introduction → · Original passage ↗
Recorded wording
The published Polymath8b argument establishes an unconditional recurring prime gap at most 246; the twin-prime target remains out of reach.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
D. H. J. Polymath · Published · Publication date 2014
Peer-reviewed historical result.
Revision & attribution
Source revision: 2014. Observed Oct 13, 2026.
No AI contribution is asserted by this source record.
A new bound for small gaps between primes →
- Theorem 1.1; introduction’s prior bounds; Appendix A, Formal certificate by AxiomProver → · Original passage ↗
Recorded wording
The preliminary draft states H₁ ≤ 212 and explains the analytic and exact rational calculations. Its appendix reports a formal deduction with analytic and variational hypotheses.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
François Charton · Letong Hong · Kenny Lau · Ken Ono · Guillaume Remy · Ho Chung Siu · Ashvin A. Swaminathan · Jesse Thorner · Yunzhou Xie · Preprint · Publication date Sep 3, 2026
Public manuscript or exposition; publication does not imply independent OpenMath review.
Revision & attribution
Source revision: 2026-09-03. Observed Oct 13, 2026.
The nine authors supply the mathematics, building on Julia Stadlmann and earlier sieve work. AxiomProver is credited with generating a formal deduction; this is not a claim that the model independently discovered the mathematical bound.
Source updated Sep 3, 2026.
Bounded gaps between primes →
- Abstract → · Original passage ↗
Recorded wording
Zhang proves that lim inf (pₙ₊₁ − pₙ) < 7 × 10⁷, refining Goldston–Pintz–Yıldırım with a stronger Bombieri–Vinogradov estimate for moduli without large prime factors.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Yitang Zhang · Published · Publication date May 1, 2014
Annals of Mathematics 179(3), 1121–1174 (2014); DOI checked against Crossref.
Revision & attribution
Source revision: 2014-05-01. Observed Oct 21, 2026.
No AI contribution is asserted by this source record.
Small gaps between primes →
- Abstract → · Original passage ↗
Recorded wording
Maynard shows that lim inf (pₙ₊₁ − pₙ) ≤ 600, and ≤ 12 assuming the Elliott–Halberstam conjecture.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
James Maynard · Published · Publication date 2015
Annals of Mathematics 181, 383–413 (2015), DOI 10.4007/annals.2015.181.1.7 checked against Crossref; arXiv v3 pinned by content hash.
Revision & attribution
Source revision: 2015. Observed Oct 21, 2026.
No AI contribution is asserted by this source record.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Conditional formal endpoint for 186 ↗
The implication from the three stated input axioms.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-prime-gaps-186-conditional
- Statement version
- 3
- SHA-256
- 0ee02494b2dd3ce0a27e17799502c55bf5eb5afdaf55e48fe517496056325bdd