OpenAI's Lean proof shows prime gaps never exceed 186 infinitely often
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI has released a Lean 4 formalization and Python certificate for a famous number theory result: there are infinitely many pairs of consecutive primes differing by at most 186. The proof is conditional on three explicit axioms, including bounds on Kloosterman sums that rely on Deligne's theorem and a result by Fouvry, Kowalski, and Michel. The repository includes a numerical certificate that recomputes the required bounds, and the Lean build passes without errors.
The Lean results remain conditional on three explicit input axioms; the cited mathematical estimates and numerical computations have not been turned into Lean proofs of those inputs.
- ks2048
Context - according to Wikipedia [0], just a few days ago someone posted a proof of a bound of 240 [1].
- dang
Related ongoing thread:
GPT-6 Astra - https://news.ycombinator.com/item?id=49554643
(see also https://news.ycombinator.com/item?id=49555621 from there)
- quuxplusone
What is this AI-generated gobbledygook actually trying to say? That there are infinitely many pairs of primes p,q with q=p+186?
The first equation under "The result" seems to be saying they found an infinite sequence of primes whose density is forever greater than 1/186, which doesn't match my understanding of how prime density works.