openai/LongGapsBetweenPrimes

openai/LongGapsBetweenPrimes

Description: A Lean formalization of a bound concerning long gaps between primes

Language: Lean

License: Apache-2.0

Stars: 24

Forks: 2

Open issues: 0

Created: 2026-09-02T18:26:05Z

Pushed: 2026-09-03T22:45:19Z

Default branch: master

Fork: no

Archived: no

README:

Improved Long Gaps Between Primes

This repository contains a Lean 4 formalization of the results presented in Improved Long Gaps Between Primes by OpenAI.

• Read the paper
• Read the abridged chain of thought

Main result

We prove that, for all sufficiently large $X$,

G(X) \gg \frac{\log\,X\,(\log \; \log\,X)^2\,\log \; \log \; \log \; \log\,X}
{(\log \; \log \; \log\,X)^2},

where $G(X)$ is the largest gap between consecutive primes not exceeding $X$. Here, $\log$ denotes the natural logarithm and $\gg$ denotes a lower bound up to a positive multiplicative constant independent of $X$.

Building the formalization

The project uses Lean 4.33.0, mathlib, and Lake. With elan installed, fetch the mathlib cache and build the formalization with:

lake exe cache get
lake build

Independent proof checking

Install landrun, lean4export, and nanoda_bin, and make them available on PATH. Then, from the repository root:

lake exe cache get
lake exe comparator comparator.json