Proved
Conditional formal endpoint for 186 ↗
The implication from the three stated input axioms.
Observed Oct 13, 2026
Theorem · version 2
A gap bound of 186 from explicit input assumptions
Earlier version 2. View current version 3 →
Statement
If PrimeGap186.kloosterman3_bound, PrimeGap186.kloosterman2_correlation_bound and PrimeGap186.physical_integral_bounds hold in the precise forms specified by the pinned development, then .
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.
Evidence
Source reports
Formal proofs
Lean: 186 with three input axioms ↗
Complete formal proof reported externally
Reported complete as a conditional theorem. Its numerical receipt does not turn the input axioms into Lean proofs.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
PrimeGap186.primeGapLiminf_le_186Commit 61340d0b74163003b32756bb16e91d9209a5e330
Connections
In this problem · publication v2 · 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.
In this problem · publication v3
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.
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
- 2
- SHA-256
- b9a3eb32fea1f8d378da259848fe787e315a8e0c9a970b6b2340d8acac2922da