cert-machine · report · generated from the records
OpenAI’s prime-gap bound of 186, checked from every side I could reach
In August 2026 OpenAI’s GPT-6 Astra proved that infinitely many pairs of primes lie at most 186 apart, and released a Lean proof of it that rests on three stated assumptions. The result and the proof are theirs. I checked the release as far as an outside party can, with Claude: the Lean proof holds as written, its 152 numerical inputs reproduce and were recomputed with no shared code, and the three assumptions remain assumptions.
What was checked, and what was not. The Lean proof was checked as a proof. The three assumptions it starts from were tested, not proved: the first two on every case for the 303 primes below 2,000, the third by re-running and recomputing its 152 numbers.Record: certs/prime-gaps-186.json · sha256 5d2c84f356d3
assumptions proved here
0 of 3
they remain assumptions
the Lean proof
3 kernels accept
Lean, nanoda, lean4lean
numerical inputs
152 of 152
reproduced, and recomputed with no shared code
cases of the two quoted assumptions
359,435,720
every prime below 2,000 · all hold
The bound, its proof, the Lean development and the numerical certificate are OpenAI’s, attributed to GPT-6 Astra. This page checks their release; it is not new mathematics, and it does not verify the bound. The checks are mine, run with Claude (Anthropic’s AI model), which wrote the programs under my direction.
read this first
What is still open
This does not verify the bound 186. The Lean proof shows: if three assumptions hold, then 186. Nothing here proves the assumptions.
Two assumptions are theorems quoted from the literature. A bound on a rank-three Kloosterman sum, after Deligne and Katz, and a correlation bound of Fouvry, Kowalski and Michel. In Lean they are assumed for every prime. Every instance was decided for the primes below 2,000, and nothing above.
The third assumption is about integrals; every program computes estimates. It asserts 149 upper bounds for integrals and three more bounds. OpenAI’s certificate, and the recomputation here, evaluate upper estimates of the 149 integrals. That each integral is at most its estimate is argued in OpenAI’s note and re-derived by hand in four AI sessions here; it is not in Lean. Its base is: OpenAI’s Lean proves that the underlying law is a probability measure with the expected density. The chain from each integral to its estimate is what is missing.
One reading choice. For 61 of the 149 rows the note picks an ingredient by a test whose outcome it does not print. The reading was fixed before anything was compared; under the other reading two rows would exceed their printed bound. The values match OpenAI’s own intervals under the reading taken.
The recomputation and its review were done by AI sessions. Under one person’s direction, with the rules sealed first. No human referee has read the hand derivations.
Two defects of our own statement-checking tool surfaced on the way. An absent checker was counted as a kernel that did not accept, and two generated files did not build under the release’s linter option. Both were fixed in public before the records they touched were derived; neither changed a prediction.
1 · the Lean proof
The Lean proof holds as written
It builds as shipped. In 11 minutes, with no warning.
OpenAI’s own checker gives the same result. Comparator, the tool the release names, reports that the three theorems and the three assumptions match the statement file. Given a statement file with 186 made 185, and one with a constant changed in the first assumption, it rejects both.
Nothing else is assumed. Each of the three theorems rests on exactly the three standard axioms of Lean and the three declared assumptions, by two computations that agree.
Three kernels accept the proof. Lean’s own, also with every import replayed from scratch (26 minutes); nanoda (99,189 declarations); and lean4lean (96,354 declarations). Two further checkers, con-ron and con-leche, decline any proof that declares assumptions, so they say nothing here.
It proves the stated statement. The proof file and the statement file agree, theorem by theorem and assumption by assumption, through every definition under them. Of 45 statements planted to test that comparison, all 11 rewordings were accepted and none of the 34 altered ones was; 6 copies of the proof broken on purpose were all caught.
The planted tests. Each square is one statement or one proof changed on purpose; hover for what it was. Six altered statements stopped before the comparison, because Lean could not read them as written: not accepted, but not refused by the comparison either.Record: certs/prime-gaps-186.json · sha256 5d2c84f356d3The build refuses this figure if a rewording is refused, an altered statement is accepted, or a broken proof is not caught.
2 · the two quoted assumptions
Every case for the primes below 2,000
Two of the three assumptions are bounds on sums over a finite field, one for every prime. A computer can decide them prime by prime, which proves nothing about all primes and still tests whether the Lean statements say something false.
All hold. 276,747 cases of the first and 359,158,973 of the second, for the 303 primes below 2,000, each decided in exact arithmetic by two programs that share no code. None fails; none is left undecided.
How close they come. The first sum reaches 2.81 against the assumed 3, at p = 887. The second reaches 5.25 against 8, at p = 1,283.
The programs read the definitions as Lean does. The values at p = 2 and 3 are proved in Lean, in 9 small theorems, and equal both programs’ values.
Wrong versions are caught. Four deliberately wrong assumptions (a missing factor, smaller constants) are refuted, the first at p = 5, the last at p = 83.
The Lean statements say what the cited theorems say. By two readings of the sources, made without sight of the Lean text.
The first assumption: the largest size of the sum at each prime, against the assumed bound 3. Square roots are for the drawing; the decisions are made on the squares, exactly.Records: certs/prime-gaps-186.json · sha256 5d2c84f356d3; corpus/prime-gaps-186/records/a2/results.jsonl · sha256 6f68a1e5154aThe build refuses this figure if a prime’s largest value reaches the bound, or the two programs disagree.
The second assumption: the largest size of the sum at each prime, divided by p√p, against the assumed bound 8.Records: certs/prime-gaps-186.json · sha256 5d2c84f356d3; corpus/prime-gaps-186/records/a2/results.jsonl · sha256 6f68a1e5154aThe build refuses this figure if a prime’s largest value reaches the bound, or the two programs disagree.
3 · the third assumption
The 152 numbers
The third assumption is a list of 152 numerical bounds: 149 upper bounds for integrals, in six tables, and three bounds on two further quantities. OpenAI supports them with a Python program, the certificate.
Reproduced. On the released versions of its arithmetic library the certificate stops at its own startup check: a known bug, corrected in flintlib/flint#2790 by Fredrik Johansson in August 2026 and in no release yet. OpenAI’s numerics note cites the correction; the README’s list of versions does not. With that one correction applied, their program, unmodified, runs to “passed” in 65 minutes and prints all 152 numbers as published.
Recomputed. Programs written from the Lean statement file and the note alone, in sessions that never saw OpenAI’s program, enclose all 152 quantities. The three cap bounds hold, with the two quantities known to about 42 digits; all 149 row values are at or below their printed bounds.
Inside OpenAI’s own intervals. Both cap quantities and 147 of the 149 row values lie inside the interval OpenAI’s run prints for the same quantity. The other 2 came out just below their intervals, so still below their bounds; computed with a recurrence exactly as the note writes it, both land in the middle.
Re-run. Every one of these programs was run again from a clean copy on a second machine, and every recorded number came back.
Reviewed. A separate session, told to look for errors, went through the 33 steps of the hand derivations: 28 hold, 3 hold under a condition it then checked, 2 it did not re-derive in full. None was found wrong. It is not a human referee.
The final inequality holds on these numbers. Total loss 696,075,106 units against the published 696,075,110. The proof needs a margin above zero: the loss could grow 12.8% before that fails, and 1.8% before the 1/50000 the papers state.
Where each recomputed value falls in the interval OpenAI’s own run prints for it: 0 is the interval’s lower end, 1 its upper end, and each printed bound is that upper end rounded up. Two computations that share no code agree to within OpenAI’s stated uncertainty, except the two rank-two values left of 0. The 17 dots exactly at 0 are low-row values that are all but zero, in intervals that start at zero. Dots in a row are spread vertically only so that they do not hide each other.Record: certs/prime-gaps-186.json · sha256 5d2c84f356d3The build refuses this figure if a value lies above its interval, or a value is missing from the drawing.
along the way
What the check found about the release
The certificate does not run on the versions the README lists. It needs the one upstream correction above, which the numerics note cites and the README omits.
The certificate never compares its results with the published numbers. It tests only the final margin. That its numbers are the published ones is the comparison made here.
Each published row bound is the upper end of that run’s own interval, rounded up. All 149 of them. A reader with only the note can confirm the bounds, not regenerate their last digits.
The note is ambiguous in two places. Which cells one sum runs over, and which recurrence one table used. The Lean file settles the first; the second was settled here by a stated reading.
Some published bounds are generous. One is about twice what the same method gives, and one column carries a floor of thousands of units. That is slack, not error.
The startup check tests a multiplication the program itself never performs. It guards against the known bug; it does not show where the program is exposed to it.
Planted errors on every check. A wrong statement, a broken proof, a wrong assumption, a changed input: each check had to catch its own.
Recomputation apart. The sessions that recomputed the numbers were given the Lean statement file, the note and the paper, and nothing of OpenAI’s program. They are sessions of one AI model under one person’s direction: independent by construction, not by authorship.
Size. One day, 10 November 2026, on a laptop and 4 rented machines: about US$10.
who did what
Each step is a separate job
The bound, its proof, the Lean development and the certificate. OpenAI, attributed to GPT-6 Astra.
The two quoted theorems. Deligne and Katz; Fouvry, Kowalski and Michel.
The correction to FLINT. Fredrik Johansson.
The checkers. Comparator, nanoda, lean4lean, con-ron, con-leche and Mathlib: their authors.
The checks on this page. Carlos Toledo, with Claude (Anthropic), which wrote the programs, the small Lean theorems and the hand derivations under his direction.
check it yourself
How to re-run it
The record.node tools/record-prime-gaps-186.js --check re-derives every number on this page from corpus/prime-gaps-186 (71 files, each pinned by its hash) and refuses on any difference.