cert-machine · report · generated from the records

Three Lean proofs of bounded prime gaps, and the 16 premises Lean does not check

Three Lean proofs bound the gaps between primes: OpenAI’s (186), one whose repository credits “GPT-6 Astra (OpenAI), prompted by Romyar Sharifi.” (182), and Axiom Math’s (212). The proofs are theirs, and nothing on this page proves a premise or verifies any of the three bounds. Each proof starts from statements it takes as given, which Lean does not check. Here is the list, 16 in all, and what I could check about each, with Claude.

One square per premise. Solid: every case at the primes below 2,000 was decided in exact arithmetic, which is not a proof for all primes. Dashed: the authors’ numbers, reproduced with their own programs, or (≠) a quoted theorem that two readers found to differ from its source. Hatched: nothing here could decide it. No square is a proof of a premise.Records: certs/prime-gap-premises.json · sha256 e11e704a7b30; corpus/prime-gap-premises/ledger.jsonl · sha256 3c1384fe2474The build refuses this figure if a premise’s status is not the one its evidence gives, or a premise has no cell.

decided

exact arithmetic backs it

computed

float, or a number someone printed; nothing decided it

refused

no mark — the void is drawn

proofs

with the bounds 186, 182 and 212

premises proved here

0 of 16

they remain premises

decided on instances

every case at the 303 primes below 2,000

reproduced

the authors’ numbers, with their own programs

read: mismatch

against the papers they cite, by two readers

not decided

nothing here could decide them

The three proofs, their Lean developments and their numerical packages belong to their authors. This page lists what they assume and what could be checked about it; it is not new mathematics. The checks are mine, done with Claude (Anthropic’s AI model), which wrote the programs under my direction; the readings of the 212 were made by AI readers working blind.

read this first

What is still open

Nothing here proves a premise, and nothing here verifies 186, 182 or 212. Each proof says: if its premises hold, then its bound. This page is about the premises, not about the proofs.
Instances are not a proof. The rank-four bound was decided at every prime below 2,000 and at none above. A finite check can refute a premise that was written down wrongly; it cannot prove one. For all primes the bound is Deligne’s theorem, not this run’s.
The 182’s 262 numbers were reproduced, not decided. They came out of the authors’ own programs, run again by me. A replay of a claimant’s programs is never an independent decision. And the step from each computed bound to the integral it stands for is argued in the package’s comments: it is in no program and not in Lean.
Which number belongs to which Lean row is the package’s own assignment. My comparison re-derives that key from the Lean row and requires it to be equal, which checks the pairing against Lean’s own fields and no further.
The readings of the 212 are readings. Two AI readers compared each quoted premise with the paper it cites. A reading is not a decision, and neither reader is a human referee.
Not decided: the 182’s local Fourier hypothesis. Its constants are free, so no finite test can refute it: a larger threshold or a larger constant escapes any instance.
Not decided: the 212’s certificate. It asserts that a certain function exists, and no such function is published. The question is open with the authors as issue #2 of their repository.
Two of the 182’s premises are the 186’s, taken over. The 182 carries a copy of the 186’s Lean file that is byte-identical, so its two shared premises inherit the checks of the 186. That its names resolve to those definitions is my reading of the file; I did not ask Lean.
The replay ran on my own build of FLINT, on Linux. The package is tested by its authors on macOS with its bundled libraries. No byte of the package was changed; six things in the environment around it were, and each is listed in the records.
A recomputation of the 262 numbers by programs of mine has not been started. That is what would turn “reproduced” into something stronger for that row.

the ledger

The 16 premises, proof by proof

Each row is one statement a proof takes as given. The third column quotes or summarises it, as the ledger does: the Lean text, shortened, or for the 212 the theorem it cites. The status is in the ledger’s own words, and none of the four is a proof of the premise.

The bound 186. OpenAI’s. openai/PrimeGaps186 at 61340d0b · 3 premises.
The bound 182. Its repository’s notice reads: “Project attribution: GPT-6 Astra (OpenAI), prompted by Romyar Sharifi.” It carries no licence for its own material, so it is quoted and linked here, never copied. romyar1/prime-gaps-lean at b77bf175 · 5 premises.
The bound 212. Axiom Math’s. In its quoted rows, [1] is a Polymath paper and [2] a paper of Stadlmann. AxiomMath/BGP212 at 6641780b · 8 premises.

proof	premise	as quoted	status
186	A bound on a rank-three Kloosterman sum PrimeGap186.kloosterman3_bound · finite-field bound	∀ p [Fact p.Prime] (c : ZMod p), c ≠ 0 → ‖normalizedKloosterman3 p c‖ ≤ 3	DECIDED ON INSTANCES below 2000 Every case at the 303 primes below 2,000 holds, in two programs that share no code: 276,747 cases. From the earlier check of the 186.
186	A correlation bound for Kloosterman sums PrimeGap186.kloosterman2_correlation_bound · finite-field bound	∀ p [Fact p.Prime] (A B : ZMod p), A ≠ 0 → B ≠ 0 → ‖∑ t ≠ 0, −1, K2(A/t) K2(B/(t+1))‖ ≤ 8 p √p	DECIDED ON INSTANCES below 2000 Every case at the same primes holds, in two programs that share no code: 359,158,973 cases. From the earlier check of the 186.
186	152 numerical bounds on integrals PrimeGap186.physical_integral_bounds · real-inequality bundle	104 outer + 45 inner + 3 cap bounds, rationals / 10^18	REPRODUCED OpenAI’s program was run again and its 152 numbers were recomputed with no shared code. That each integral is at most its estimate is argued on paper.
182	The 186’s first premise, again PublicPrimeLocalBounds182 (first conjunct) · finite-field bound	∀ p [Fact p.Prime] (c : ZMod p), c ≠ 0 → ‖normalizedKloosterman3 p c‖ ≤ 3	DECIDED ON INSTANCES below 2000 Taken over from the 186: the 182 carries a byte-identical copy of that Lean file and states the same sum, so it inherits that check. That its names resolve to that file’s definitions is a reading.
182	The 186’s second premise, again PublicPrimeLocalBounds182 (second conjunct) · finite-field bound	∀ p [Fact p.Prime] (A B : ZMod p), A ≠ 0 → B ≠ 0 → ‖∑ t ≠ 0, −1, K2(A/t) K2(B/(t+1))‖ ≤ 8 p √p	DECIDED ON INSTANCES below 2000 Taken over from the 186: the 182 carries a byte-identical copy of that Lean file and states the same sum, so it inherits that check. That its names resolve to that file’s definitions is a reading.
182	A bound on a rank-four Kloosterman sum AllIncidenceRankFourBounds / IncidenceRankFourBound · finite-field bound	∀ c : ZMod p, c ≠ 0 → ‖∑ u v w : (ZMod p)ˣ, stdAddChar (u + v + w + c / (u v w))‖ ≤ 4 p √p	DECIDED ON INSTANCES below 2000 New in this work. Every case at the 303 primes below 2,000 holds, in two programs that share no code: 276,747 cases, none failing, none left undecided.
182	262 numerical bounds on integrals PhysicalSourceBounds182 · real-inequality bundle	cap (5) + outerRoot, outerFace (∀ j : Fin 60) + innerMass (∀ j : Fin 137): 262 inequalities between integrals and rationals	REPRODUCED The authors’ own numerical package, run again by me: it accepts its own run, and all 262 fresh values equal the numbers written in Lean. A replay, not an independent decision.
182	A local Fourier hypothesis with free constants LocalFourierHypothesis C D p₀ · free constants	∀ p, p₀ < p → ∀ α m m′ n n′ : ZMod p, … Finite/CurveExceptionalFourierBound p C D …	NOT DECIDED No finite test can refute it: a larger threshold or a larger constant escapes any instance.
212	A Type II estimate TypeIIPolymath · quoted asymptotic theorem	cited: [2] Lemma 3, [1] Thm 2.8(iv)	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A Type I estimate TypeIbPolymath · quoted asymptotic theorem	cited: [2] Lemma 4, [1] 2.8(ii)	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A Type I estimate TypeIBakerIrving · quoted asymptotic theorem	cited: [2] Lemma 5	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A Type I estimate TypeIStadlmann · quoted asymptotic theorem	cited: [2] Lemma 6	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A Type III estimate TypeIIIPolymath · quoted asymptotic theorem	cited: [2] Lemma 7, [1] 2.8(v)	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A reduction step Gap212HarmanReduction · quoted asymptotic theorem	cited: [2] Prop. 2, Def. 9	READ: MISMATCH Read twice, blind. Both readers: the Lean text bounds the error over all n, where the paper it cites sums over n between x and 2x.
212	A bilinear Bombieri–Vinogradov theorem BilinearBombieriVinogradov · quoted asymptotic theorem	cited: [1] Thm 2.9	READ: MISMATCH Read twice, blind. Both readers: the Lean text adds a condition that the theorem it cites does not have.
212	A certificate: a function with a stated property exists Gap212Certificate · real-inequality bundle	Certificate gap212Params 44 0 0: ∃ F, symmetric, L², 0 < I(F) < k·J(F)	NOT DECIDED It needs a witness, and none is published. The question is open with the authors.

1 · the 182’s rank-four premise

Every case for the primes below 2,000

The 182 adds a premise the 186 does not have: a bound on a sum over a finite field, one for every prime p and every nonzero c. Its size is to be at most 4 times p√p. It is Deligne’s bound for the rank-four Kloosterman sum, taken as a hypothesis. A computer can decide it prime by prime, which proves nothing about all primes and still tests whether the Lean statement says something false.

All hold. 276,747 cases, for the 303 primes below 2,000, each decided by two programs that share no code: one in exact integers, one in interval arithmetic. None fails; none is left undecided.
The two programs agree case by case. On all 276,747 cases their enclosures of the sum overlap. A third program, a direct triple sum, recomputed the 149 cases at the primes up to 31 and landed inside both.
Wrong versions are caught. With 4 replaced by 3, 496 cases fail in both programs, the same 496, the earliest at p = 73. With 4 replaced by 2, 13,696 fail in both, the same number at every prime.
How close it comes. The sum reaches 3.6085 times p√p against the assumed 4, at p = 1,493 and c = 689.

The rank-four premise: the largest size of the sum at each prime, divided by p√p, against the assumed bound 4. Each point is the upper end of an interval enclosure, rounded up.Records: certs/prime-gap-premises.json · sha256 e11e704a7b30; corpus/prime-gap-premises/out/decider-b.jsonl · sha256 1eaa3c9b3857The build refuses this figure if a prime’s largest value reaches the bound, or the two programs disagree.

2 · the 182’s numbers

The authors’ numerical package, run again

Another premise of the 182 is a list of 262 inequalities between integrals and fractions: 5 cap bounds, 120 outer and 137 inner. Its authors support them with a numerical package, released as an archive. I ran it again.

What was run. The release archive, pinned by its hash, and the repository at its pinned commit, on a rented Linux machine. The arithmetic library is FLINT v3.6.0 with one upstream correction (7ad753d5), built from source. No byte of the package was changed.
The package accepts its own run. Its 14 audits pass, its 4 rejection tests all reject, and all 14 production stages pass, in 2 h 52 min. Its acceptance step reports a complete recomputation of the 262 inequalities.
My comparison. A script of mine, with its hash logged before production started, compares the 262 fresh values with the fractions it parses from the Lean files at the pinned commit, not with the package’s own targets. 262 of 262 are on the right side.
There is no slack. All 262 fresh values are equal to the numbers written in Lean, and equal to the published values. The Lean numbers are exactly what the package computes, so nothing separates a computed bound from the bound Lean assumes.
The comparison catches a wrong number. With one Lean number tightened past its value, it fails and names the row. With one row removed, it fails on the count.

3 · the 212’s quoted theorems

Seven quoted premises, read blind twice

7 of the 8 premises of the 212 are theorems quoted from two papers. For these the question is whether the Lean text says what the paper says.

How they were read. By two AI readers. Each read the cited paper and recorded what it states before opening the Lean file; the second reader did not see the other’s work.
What both found. All 7 differ from the statements they cite. In 6, the Lean text bounds an error over all n, where the paper sums over n between x and 2x; a helper for the paper’s version is defined in the file and never used. The other one adds a condition its source does not have.
Already public. The readings, hypothesis by hypothesis, are in corpus/bgp212-readings-2026-11-12, and the main difference is reported to the authors as issue #1 of their repository.
Readings, not decisions. A reading compares two texts. Neither reader is a human referee, and no program decided anything in this section.

4 · the 212’s certificate

A certificate with no published witness

What it asks for. The remaining premise of the 212 says that a function with a stated property exists. To check it, one needs the function.
None is published. I looked in the repository at its pinned commit, whose own README says the certificate is assumed, and in the library it depends on, which holds such functions for two other bounds. Finding one myself would be a research computation, and was not attempted.
Asked. The question is open with the authors as issue #2 of their repository. The row stays NOT DECIDED.

the method

How it was done

Rules before results. The rules for each stage, with its verdict words and its predictions, were written and sealed before the stage ran: a salted fingerprint of the private work, posted to a public registry, which proves the date without showing the content. There are 4 fingerprints (the rules; the results; amendment A1, the rules; amendment A1, the results), and the rules are now public: corpus/prime-gap-premises/PREREGISTRATION.md.
A wrong version on every check. A bound made too small, a number tightened, a row removed: each check had to catch its own.
Departures are listed. Among them: the first rented machine was deleted partway through the long run, and the whole step was run again from the start on a second one.
Size. One day, 12 November 2026: a laptop and 2 rented machines, about US$2.50 by the clock.

who did what

Each step is a separate job

The three proofs. OpenAI (186); “GPT-6 Astra (OpenAI), prompted by Romyar Sharifi.”, in the words of that repository’s notice (182); Axiom Math (212).
The theorems the premises quote. Deligne and Katz, and Fouvry, Kowalski and Michel, for the sums over finite fields; Polymath and Stadlmann, for the 212’s estimates.
The numerical package of the 182, and FLINT. Their authors.
The checks on this page. I did them, with Claude, Anthropic’s AI model, which wrote the programs under my direction.
The readings of the 212. Two AI readers that I ran, each working blind.

check it yourself

How to re-run it

The record. node tools/record-prime-gap-premises.js --check re-derives every number on this page from corpus/prime-gap-premises (45 files, each pinned by its hash) and refuses on any difference.
The two deciders. In that folder, python3 decider_a.py (it needs NumPy; about 109 minutes) and node decider_b.js (about 3 minutes) decide the rank-four premise again; a smaller bound on the command line makes a shorter run. Given --values and a file name, each also writes its value for every case, and compare.py compares the two files and runs the direct triple sum.
The comparison script. corpus/prime-gap-premises/step5/compare182.py needs a run of the authors’ package and a copy of their repository at the pinned commit.
What is withheld, and why. The package’s own output from my run is not published, because the 182 repository carries no licence: what I read from it is published, with the hashes of the files. Two large files of per-case values are given by hash; the deciders write them again. corpus/prime-gap-premises/PUBLICATION-NOTES.md says what differs from the private files.
What was checked. openai/PrimeGaps186 at 61340d0b, romyar1/prime-gaps-lean at b77bf175, AxiomMath/BGP212 at 6641780b. The earlier check of the 186: its report.
The results as written. With what stays open at the top: corpus/prime-gap-premises/RESULT-2026-11-12.md.