A new OpenAI GitHub project, PrimeGaps186, packages a notable number-theory claim in Lean 4: there are infinitely many consecutive pairs of primes whose gap is at most 186.
More precisely, the project derives
\[ \liminf_{n\to\infty}(p_{n+1}-p_n) \le 186. \]
That is a meaningful formalization milestone—but it is not a fully end-to-end machine-verified proof of the underlying mathematical result. The repository is unusually clear about that distinction: its Lean theorem depends on three explicit axioms covering two advanced analytic estimates and a set of numerical integral bounds.
What the project actually proves
Within its stated assumptions, the Lean development proves a chain of results. It derives a version of the Dickson/Hardy–Littlewood-style statement known as `DHL[40,2]`: every admissible collection of 40 integer shifts has infinitely many translates containing at least two primes.
The project then applies that result to an explicit 40-element tuple with diameter 186. From there, it concludes that infinitely many consecutive prime gaps are no larger than 186.
The formal code exposes the main stages as Lean declarations, including `dhl_40_2`, a theorem about infinitely many two-prime translates of the chosen tuple, and `primeGapLiminf_le_186`.
Lean’s kernel accepted the conditional proofs, according to the project documentation, and the repository pins its toolchain to Lean 4.34.0-rc2 and associated Mathlib dependencies. That makes the logical plumbing—from assumptions to final conclusion—independently checkable and reproducible in a way that a conventional paper proof generally is not.
The important qualification: three inputs are assumed
The repository does not claim to have formalized every ingredient. Two axioms represent Deligne-type exponential-sum estimates cited from published mathematical literature, including bounds involving Kloosterman sums. A third axiom represents a large numerical input: 104 outer and 45 inner physical-integral upper bounds, plus three cap bounds.
The supplied Python certificate can recompute the numerical trial and emit a passing receipt, but the project explicitly says this does not discharge the corresponding Lean axiom. It also specifies a narrow tested environment, including Python, NumPy and FLINT versions, and notes a custom FLINT build with a corrected signed polynomial convolution.
For operators building on formal methods, this distinction is the story. A verified kernel can establish that a conclusion follows from supplied premises; it cannot establish that those premises are true unless they, too, have been formalized or otherwise brought into the trusted base.
Why this matters beyond number theory
The project is a useful example of how AI-assisted research and formal verification may meet in practice. The near-term value is less about replacing expert mathematical review than making dependencies visible, machine-readable and testable.
That has direct analogues in software, security and regulated systems. A team may formally verify that an implementation satisfies a specification, while still needing to scrutinize the specification, model assumptions, external data and numerical tooling. Formal proof narrows the surface for error; it does not eliminate the need to manage the boundary between verified logic and unverified inputs.
The repository also demonstrates a pragmatic workflow: formalize the proof structure first, isolate the hard external claims, attach citations and reproducible computational checks, and make the trusted assumptions explicit. That approach can be valuable even before every component is fully machine-checked.
What to watch next
The central next step is whether the three axioms can be replaced with formal proofs or with more tightly verified computational certificates. The analytic estimates are established in the cited literature, but translating those arguments into Lean would be a substantial undertaking. The numerical component poses a different challenge: reducing dependence on a particular floating-point and library environment.
For now, PrimeGaps186 should be read as a conditional formalization of a prime-gap bound, not as a standalone, fully formal proof. Its contribution is to make that condition precise—and to show what a more auditable mathematical research artifact can look like.
