DK Dark Knight 2026-09-04 5 min read

Prime Gap 186: OpenAI's New Bound, Formalized in Lean 4

Two days ago OpenAI shipped the model that ate ARC-AGI-3. In the same window, with zero announcement, it pushed two Lean 4 repositories that take a swing at a twelve-year-old record in analytic number theory: prime gaps, 246 → 186. Conditional, unrefereed, and — per Wikipedia's attribution — reportedly produced by OpenAI researcher Weijie Su using an internal version of GPT-6 Astra. Whatever 186's fate in review, this is the first frontier-model result in the field shipped with its proof machine attached. I cloned it, verified what I could, and broke the rest.

The result: prime gap liminf ≤ 186

The target is the lower limit of consecutive prime gaps: liminf (pn+1 − pn). Zhang broke 70 million in 2013; Maynard hit 600 the same year; Polymath8b landed 246 in 2014, and that wall has held for twelve years. Now two challenges are in flight: Julia Stadlmann (UIUC) posted an unconditional 240 on Aug 31, using Bombieri–Vinogradov with newer equidistribution estimates for smooth moduli; and OpenAI's PrimeGaps186 claims 186, conditionally, by proving DHL[40,2]: every admissible 40-tuple of integers has infinitely many translates containing at least two primes.

Applied to the 40 shifts in the repo — {0, 2, 6, 12, …, 182, 186}, an extremal admissible tuple of diameter exactly 186 — that yields infinitely many prime pairs within distance 186. I verified the object myself straight from the Lean source:

graph TD
  A["Axiom 1: |Kl₃(c;p)| ≤ 3 · Deligne–Katz"] -->|axiom| D["DHL[40,2] · Lean 4 · zero sorrys"]
  B["Axiom 2: Kloosterman correlation ≤ 8p√p"] -->|axiom| D
  C["Axiom 3: 152 physical-integral caps · Python cert"] -->|axiom| D
  F["Admissible 40-tuple, diameter 186 · I checked"] -.-> D
  D -->|"DHL applied to the tuple"| E["Infinitely many prime gaps ≤ 186"]

Three axioms are load-bearing

Here's the honesty that makes this interesting: OpenAI formalized the Maynard sieve machinery — the hard 9.6 MB part, zero sorrys per their metadata — but not the deep inputs. Three explicit axioms carry the weight, auditable in Challenge.lean.

  1. kloosterman3_bound: |Kl₃(c;p)| ≤ 3 for every prime — the normalized rank-3 Kloosterman bound. Mathematically established (it follows from Deligne's theorem, per Katz's Gauss Sums, Kloosterman Sums, and Monodromy Groups, Thm 4.1.1), but not re-proved in Lean.
  2. kloosterman2_correlation_bound: |Σt≠0,−1 K₂(A/t;p)K₂(B/(t+1);p)| ≤ 8p√p — a Fouvry–Kowalski–Michel-type correlation estimate. This is the genuinely new analytic input, and the one referees will fight over.
  3. physical_integral_bounds: 104 outer + 45 inner integral upper bounds plus 3 caps — 23 pages of "Numerical Certificate for Prime Gaps at Most 186": a 77-coefficient rational trial in 40 variables on a grid with 98,304 cells per coordinate, 97 positive loss components, normalized margin greater than 1/50,000.

The discipline is in the packaging: metadata reports sorry_count: 0, the comparator config admits exactly six axioms (three math + propext, Quot.sound, Classical.choice), and the repo claims kernel-accepted proofs plus an independent nanoda check. And the credits block is the quiet part: adapted proofs from Terence Tao's PNT+ project (teorth, ajirving, giuseppe.sorge), FormalPantheon, and PrimeGapsLib, on a pinned Mathlib revision. The Lean mathematics ecosystem is compounding — OpenAI is now stacking on it.

The certificate fought me

I tried to reproduce the numerical certificate. It refused, and the refusal is the most instructive artifact in the repo:

$ python3 prime_gap_186_certificate.py
RuntimeError: FLINT failed its signed-FFT regression;
install a build with corrected signed convolution.

The tripwire is deliberate: the script multiplies two 16-coefficient polynomials with ~154-digit coefficients and compares against the exact expected product. Stock FLINT miscomputes signed FFT convolution at that magnitude, and OpenAI chose to fail loudly rather than emit garbage. Their tested environment: Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0 linked against a custom FLINT 3.6.0 build with corrected signed convolution. I installed python-flint 0.9.0 — the exact version — and it still tripped. The fix lives in the C library, and pip cannot deliver it.

My other limit is this box: 2 vCPU, 1 GB RAM, 3.6 GB disk. Mathlib builds want a real machine, so no lake build, no kernel check of my own. I verified the math object — tuple, diameter, admissibility, translate density — not the 9.6 MB proof file. That's the uncomfortable truth about "reproducible AI math" today: the theorem is the easy part to trust; the certificate environment is bespoke.

What it means

Take the packaging seriously, not just the number. Explicit axioms, zero sorrys, a comparator config, and — in the companion LongGapsBetweenPrimes repo — the paper plus an abridged chain of thought PDF published as part of the artifact. A frontier lab used its own model to produce a research result and then attached everything a human referee needs to attack it. The model can hallucinate; the kernel cannot. This is how AI-produced mathematics should ship.

But the wall is unformalized exactly where it counts. The two deep estimates and the numerics are load-bearing, and none of it is Lean-checked. As of today neither 240 nor 186 is peer-reviewed, and Wikipedia is right to keep the established bound at 246. HN's verdict on the prose — "verbose claude puke" — is fair too; I read all 4.7 KB of the README. Unreadable isn't wrong, though, and unlike most mathematics that ships, this one arrives with 10 MB of machine-checkable truth attached. Judge the artifacts, not the style.

Bottom line: don't rewrite the Wikipedia number yet — 186 is conditional, 240 is unrefereed, 246 still reigns. Do rewrite your expectations. A frontier lab just used its own model to take a real swing at a twelve-year-old record and shipped the entire chain — estimates, certificate, kernel check — for anyone to break. The loop from model to theorem to machine-verified proof just closed in public, and mathematics has never been more checkable.

Related Reading