Conditional Lean 4 formalization claims prime gaps of at most 186

What was released

A repository named PrimeGaps186, published under OpenAI's GitHub account and promoted to the Hacker News front page, contains a Lean 4 formalization of a prime-gap result alongside a Python program that rechecks the numerical work. The headline statement is that the limit inferior of consecutive prime gaps p(n+1) − p(n) is at most 186 — in plain terms, infinitely many pairs of neighbouring primes differ by 186 or less. The README is blunt about the project's status: the Lean results are conditional on three explicitly declared input axioms, and the analytic estimates and numerical computations those axioms encode have not been turned into Lean proofs.

The mathematical route

The formalization derives what number theorists call DHL[40,2]: any admissible set of forty integer shifts admits infinitely many translates in which at least two members are prime. Admissibility here means that, for every prime, the set fails to occupy every residue class modulo that prime. The repository ships an explicit admissible tuple of diameter 186 — its smallest and largest elements sit 186 apart — and applying DHL[40,2] to that tuple yields the gap bound, since two primes inside a window of width 186 force a consecutive gap no wider than the window. The three headline theorems live in PrimeGaps186.lean under the PrimeGap186 namespace: dhl_40_2, infinite_two_prime_translates_admissibleTuple and primeGapLiminf_le_186.

The three assumed inputs

The conditional part sits in three axioms. The first, kloosterman3_bound, asserts that a normalised hyper-Kloosterman sum Kl3(c;p) is bounded in absolute value by 3 for every prime p and non-zero c. According to the README, this follows from Deligne's theorem in the form stated in Nicholas Katz's 1988 book Gauss Sums, Kloosterman Sums, and Monodromy Groups (Theorem 4.1.1(1)–(2), page 49), where rank three and weight two give a raw bound of 3p before the normalisation divides by p.

The second, kloosterman2_correlation_bound, bounds a correlation of classical Kloosterman sums by 8p·√p for all primes p and non-zero parameters A and B, with the two pole terms excluded even when A equals B. The attribution is Proposition 2 of "The Friedlander–Iwaniec character sum" by Étienne Fouvry, Emmanuel Kowalski and Philippe Michel, dated 14 June 2013; the README explains that their normalisation differs by a factor of √p once the summation variable is inverted.

The third, physical_integral_bounds, packages the numerics: 104 outer and 45 inner physical-integral upper bounds together with three cap bounds. The first two estimates are established in the cited literature, the README says, but all three remain unproved inputs inside this Lean development.

The numerical certificate

The certificate, prime_gap_186_certificate.py, recomputes the trial from scratch rather than replaying stored values. The tested environment used Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0 and a custom FLINT 3.6.0 build with a corrected signed polynomial convolution, which the project notes is not bundled. A run must pass mandatory floating-point and signed-convolution checks and produces a receipt marked "passed": true. Crucially, the receipt discharges no Lean axiom — the certificate and the kernel-checked proof remain separate artefacts.

Rebuilding and verifying

The project pins Lean 4.34.0-rc2 with its Mathlib dependencies; with elan installed, lake exe cache get followed by lake build PrimeGaps186 reproduces the build, which the maintainers report passed without errors or warnings. A comparator matched all three results against Challenge.lean, a file stating the theorems and input assumptions with three intentional theorem placeholders, and both Nanoda and Lean's kernel accepted the proofs in a local Colima Linux virtual machine. The axiom configuration allows exactly six axioms — the three project inputs plus Lean's standard propext, Quot.sound and Classical.choice — so the machine verification covers the conditional proofs, not the inputs themselves. Project contributions are licensed Apache 2.0.

Why it matters

Bounded gaps between primes became a theorem in 2013 through Yitang Zhang's breakthrough and the Maynard–Tao refinements that followed, with the Polymath collaboration pushing the unconditional bound down to 246. A fully proved bound of 186 would edge that record lower, but this repository does not claim that, and its own accounting shows exactly where the remaining distance lies.

What the project demonstrates is a verification architecture. The entire chain from named analytic inputs to the headline statement is machine-checked modulo a short, explicit axiom list, and the numerical component ships as an independently re-runnable program with pinned environments and mandatory sanity checks. That pattern — precise statements, declared assumptions, reproducible certificates — is a workable trust model for computational mathematics and for proof artefacts produced with automated tooling. A sceptical reader can rebuild the Lean project, re-run the certificate, and see precisely which lemmas remain open: the Kloosterman estimates and the integral bounds. Turning the cited literature and the numerics into Lean proofs is the obvious next milestone, and until it happens the number 186 stays conditional.