PrimeGaps186 README

The project's README from github.com/openai/PrimeGaps186. As one markdown file: README.md.

Prime Gaps at Most 186

This repository contains a Lean 4 formalization of a prime-gap bound and a Python numerical certificate. 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.

The result

For the sequence of primes $p_n$, the target bound is

\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186.

The development derives $\mathrm{DHL}[40,2]$ from the inputs below: every admissible set of forty integer shifts has infinitely many translates containing at least two primes. Admissibility means omitting a residue class modulo every prime. Applying this to the included tuple of diameter 186 gives the gap bound.

The main declarations in PrimeGaps186.lean, in namespace PrimeGap186, are:

Declaration Result
dhl_40_2 $\mathrm{DHL}[40,2]$ for every admissible integer tuple.
infinite_two_prime_translates_admissibleTuple Infinitely many two-prime translates of the explicit tuple.
primeGapLiminf_le_186 The consecutive-prime gap bound.

Assumed Deligne-type estimates

For a prime $p$, write $e_p(x)=\exp(2\pi i\widetilde{x}/p)$, where $\widetilde{x}$ is any integer representative of $x\in\mathbb{F}_p$. Define

\mathrm{Kl}_3(c;p)
=\frac1p\sum_{\substack{x_1,x_2,x_3\in\mathbb{F}_p\\x_1x_2x_3=c}}
e_p(x_1+x_2+x_3),

K_2(c;p)=\sum_{u\in\mathbb{F}_p^\times}e_p(u+c/u).

The axiom PrimeGap186.kloosterman3_bound assumes the following bound for every prime $p$ and all $c\in\mathbb{F}_p^\times$:

\left|\mathrm{Kl}_3(c;p)\right|\le 3.

This follows from Deligne's theorem as stated in Nicholas M. Katz, Gauss Sums, Kloosterman Sums, and Monodromy Groups, Annals of Mathematics Studies 116, Princeton University Press (1988), Theorem 4.1.1(1)–(2), p. 49. With $n=3$, trivial multiplicative characters, and $b_1=b_2=b_3=1$, rank three and weight two give the raw bound $3p$; our normalization divides by $p$.

The axiom PrimeGap186.kloosterman2_correlation_bound assumes the following bound for every prime $p$ and all $A,B\in\mathbb{F}_p^\times$:

\left|\sum_{t\in\mathbb{F}_p\setminus\{0,-1\}}
K_2(A/t;p)\,K_2(B/(t+1);p)\right|\le 8p\sqrt p.

This is Étienne Fouvry, Emmanuel Kowalski, and Philippe Michel, The Friedlander–Iwaniec character sum, 14 June 2013, Proposition 2, p. 1. Their normalized $\mathrm{Kl}_2(c)$ equals $K_2(c;p)/\sqrt p$ after inverting the summation variable, so their $8\sqrt p$ bound becomes $8p\sqrt p$ here. No condition $A\ne B$ is imposed; the two poles are excluded even when $A=B$.

These estimates are established in the cited literature, but remain unproved inputs in this Lean development.

Numerical input and certificate

PrimeGap186.physical_integral_bounds assumes 104 outer and 45 inner physical-integral upper bounds, plus three cap bounds.

The Python certificate recomputes the trial from scratch. 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 corrected signed polynomial convolution (not bundled).

python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json

Use a new output path. Keep PYTHONOPTIMIZE unset and do not use -O or -OO. Mandatory floating-point and signed-convolution checks must pass. A successful run produces a receipt with passed: true; it does not discharge any Lean axiom.

Building and verification

The project pins Lean 4.34.0-rc2 and its Mathlib dependencies. With elan installed, run:

lake exe cache get
lake build PrimeGaps186

The registered Lean build passed without errors or warnings. Comparator matched all three results to Challenge.lean, and Nanoda and Lean’s kernel accepted their proofs in a local Colima Linux VM. The configuration permits the three documented project axioms plus propext, Quot.sound, and Classical.choice (six total); this verifies conditional proofs, not the inputs themselves. The numerical certificate is unchanged from its earlier passing run.

Challenge.lean specifies the statements and input assumptions, with three intentional theorem placeholders. See the Comparator instructions and formalization metadata for the checking setup and status.

Project contributions use Apache 2.0; existing third-party notices remain applicable.

PrimeGaps186 (openai/PrimeGaps186)

Searching Database…

166 ·GitHub
PrimeGaps186
What is this?This is a Lean 4 formalization proving a bound on gaps between consecutive primes (gap at most 186), along with a Python script that numerically verifies the inputs used by the proof.
Is this a finished mathematical proof or still conditional on unproven assumptions?The Lean proof derives the gap bound from three explicit axioms (two Deligne-type estimates and a set of numerical bounds) that are cited from published papers but not themselves proved inside Lean.
How do I build and verify it?Install elan, then run the registered Lean build, which pins Lean 4.34.0-rc2 and its Mathlib dependencies; results are checked against Challenge.lean using the Comparator tooling.
What do I need to run the Python numerical certificate?You need 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 patch (not included in the repo).
Does passing the numerical certificate prove the theorem?No — a successful certificate run just confirms the numerical inputs recompute correctly; it does not discharge the Lean axioms, so the overall result stays conditional.
Who would actually use this repository?This is aimed at researchers in analytic number theory and formal verification who want to check or extend a conditional proof of a specific prime-gap bound, not general developers.
What environment was the Lean build actually tested on?The Lean build and kernel checking were run and verified in a local Colima Linux VM, with Nanoda and Lean's kernel both accepting the proofs.
What exactly is DHL[40,2] and why does it matter here?DHL[40,2] says every admissible set of 40 integer shifts has infinitely many translates containing at least two primes; applying it to a specific diameter-186 tuple yields the bound on gaps between consecutive primes.
What are the three axioms the proof depends on?Two are Deligne-type Kloosterman sum bounds (kloosterman3bound and kloosterman2correlationbound) cited from Katz's book and a Fouvry-Kowalski-Michel paper, and the third (physicalIntegralBounds) is a set of 104 outer and 45 inner numerical integral bounds plus three cap bounds.
What is Challenge.lean?It is the file specifying the target statements and input assumptions as three intentional theorem placeholders, used by the Comparator tool to check that the main Lean file actually proves those exact statements.
How many trusted axioms does the verified build rely on in total?Six: the three project-specific input axioms plus the standard Lean/Mathlib axioms propext, Quot.sound, and Classical.choice.
What are similar projects?fermats-last-theorem, integer-mult-bounds, math, NavierStokesAndEuler, XRAG, fluid_lean, wikiskill, OpenWAM
Which topics is it in?lean, arxiv, mathematics, academic-research, research, apache-2.0, python, cross-platform, windows, macos, linux
Creator
openai
Size
2.2 MB
Stars
166
Updated
CommitSep 02
Age
1mo
Commits · 90 Days