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

> Source: <https://github.com/openai/PrimeGaps186>
> Published: 2026-09-03 19:18:56+00:00

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.