Prime Gaps at Most 186

[mklabgr]

New result by OpenAI on Prime gaps

Summary
OpenAI’s PrimeGaps186 repository presents a Lean 4 formalization of a result on bounded gaps between prime numbers, together with a Python program that checks the necessary numerical estimates. The target theorem is
$\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186$,
meaning that there are infinitely many pairs of consecutive primes whose difference is at most 186. The proof proceeds by establishing the sieve-theoretic statement $\mathrm{DHL}[40,2]$: every admissible collection of 40 integer shifts has infinitely many translates containing at least two primes. An explicit admissible 40-element tuple of diameter $186$ then yields the stated bound.

The important qualification is that this is not a completely self-contained formal proof of the prime-gap theorem in Lean. The Lean development relies on three explicit assumptions. Two concern deep estimates for Kloosterman-type exponential sums, derived from established work by Deligne/Katz and Fouvry–Kowalski–Michel. The third consists of a substantial collection of numerical integral bounds. These results are mathematically known or computationally checked, but they have not themselves been formally proved inside Lean. The accompanying Python certificate recomputes the numerical part and verifies that the required bounds pass, but successfully running it does not eliminate the corresponding Lean axiom.

What makes the project particularly interesting is its combination of analytic number theory, rigorous numerical computation, and formal verification. The Lean kernel has checked the logical deductions from the stated assumptions, and the numerical certificate provides an independently reproducible computational check. Thus the repository should be understood as a conditional machine-verified formalization of the bound $186$, rather than as a new unconditional proof of a previously unknown prime-gap result. It is also a useful example of how advanced mathematical arguments can be split into formally verified reasoning, literature-backed theorems, and certified computation.

Key takeaways

• Main result: $\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186$.
  
• It formalizes the implication $\mathrm{DHL}[40,2]\Rightarrow$ infinitely many prime gaps $\le 186$.
  
• The Lean proof is conditional on three explicit axioms; therefore it is not yet a fully formalized end-to-end proof.
  
• A Python certificate verifies the large numerical component independently.
  
• The project illustrates a promising model for combining AI-assisted/formal mathematics, Lean, numerical certification, and classical analytic number theory.
  
  

In simple terms: the interesting achievement is not discovering that prime gaps can be bounded by $186$, but showing how a sophisticated prime-gap argument can be turned into a largely machine-checkable mathematical object, with the remaining unformalized assumptions clearly isolated.

ARTICLE