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.
Public formal source; build and independent mathematical review are separate checks.
1 cited passage ↓1 problem ↓Record 61340d0b74163003b32756bb16e91d9209a5e330 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
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.
Passage ID: prime-gaps:entry:186-lean:v1
Source item: 186-lean
Source record: prime-gaps:source:186-lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v7
Source assessment
Proved
Conditional formal endpoint for 186
The implication from the three stated input axioms.
Observed Oct 13, 2026
Formal declaration
Lean: 186 with three input axioms
Research activity
The 186 numerical certificate and Lean assumptions
The numerical program and the conditional Lean development are distinct artifacts with different checking boundaries.
A passing numerical receipt does not discharge the three Lean input axioms.
History
A conditional formal deduction for 186
Question
How small can prime gaps be?
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Resource revision: 61340d0b74163003b32756bb16e91d9209a5e330
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
PrimeGap186.primeGapLiminf_le_186Commit 61340d0b74163003b32756bb16e91d9209a5e330
Recorded authorship
OpenAI · PrimeGaps186 contributors
OpenAI, PrimeGaps186 contributors
The project is an OpenAI formal development. Its explicit assumptions and certificate work are recorded separately from an unconditional mathematical improvement.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Prime gaps at most 186: a conditional Lean development
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗