OpenAI Publishes a Lean 4 Formalization of Prime Gaps ≤ 186, Conditional on Three Unproven Axioms

GitHub (openai/PrimeGaps186)·medium signalXBlueskyLinkedInCopy link

The openai/PrimeGaps186 repository, created September 2, 2026 under Apache-2.0 and now at 117 stars, formalizes lim inf(p_{n+1} - p_n) ≤ 186 via the Dickman-Hardy-Littlewood conjecture applied to a 40-element admissible tuple. The Lean 4 development proves three theorems (`dhl_40_2`, `infinite_two_prime_translates_admissibleTuple`, `primeGapLiminf_le_186`) but remains conditional on three unproven axioms: a Kloosterman3 bound from Deligne, a Kloosterman2 correlation bound from Fouvry-Kowalski-Michel 2013, and 104 outer plus 45 inner integral bounds verified only numerically. The repo ships a Python certificate for the numerical part, so the honest framing is a conditional machine-checked result, not a proof.