GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186

OpenAI released a Lean 4 formalization, GPT-6-Astra, proving that infinitely many pairs of consecutive primes are separated by at most 186, but the proof is conditional on three explicit axioms not yet verified in Lean. The project, named PrimeGaps186, includes a Python certificate that recomputes the numerical bounds, and the Lean build passed without errors, though it does not discharge the axioms.

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. For the sequence of primes The development derives The main declarations in PrimeGaps186.lean /openai/PrimeGaps186/blob/main/PrimeGaps186.lean , in namespace PrimeGap186 , are: | Declaration | Result | |---|---| dhl 40 2 | | infinite two prime translates admissibleTuple | Infinitely many two-prime translates of the explicit tuple. | primeGapLiminf le 186 | The consecutive-prime gap bound. | For a prime The axiom PrimeGap186.kloosterman3 bound assumes the following bound for every prime 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 https://web.math.princeton.edu/~nmk/Katz-GKM.pdf page=29 . With The axiom PrimeGap186.kloosterman2 correlation bound assumes the following bound for every prime This is Étienne Fouvry, Emmanuel Kowalski, and Philippe Michel, The Friedlander–Iwaniec character sum, 14 June 2013, Proposition 2, p. 1 https://people.math.ethz.ch/~kowalski/friedlander-iwaniec-sum.pdf page=1 . Their normalized These estimates are established in the cited literature, but remain unproved inputs in this Lean development. PrimeGap186.physical integral bounds assumes 104 outer and 45 inner physical-integral upper bounds, plus three cap bounds. The Python certificate /openai/PrimeGaps186/blob/main/prime gap 186 certificate.py 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. The project pins Lean 4.34.0-rc2 and its Mathlib dependencies. With elan https://github.com/leanprover/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 /openai/PrimeGaps186/blob/main/comparator/main.json 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 /openai/PrimeGaps186/blob/main/Challenge.lean specifies the statements and input assumptions, with three intentional theorem placeholders. See the Comparator instructions /openai/PrimeGaps186/blob/main/comparator/README.md and formalization metadata /openai/PrimeGaps186/blob/main/formalization.yaml for the checking setup and status. Project contributions use Apache 2.0 /openai/PrimeGaps186/blob/main/LICENSE ; existing third-party notices remain applicable.