An outside check of OpenAI's conditional Lean proof that prime gaps are at most 186

On 30 August 2026 OpenAI released a proof, attributed to the model GPT-6 Astra, that liminf (p_{n+1} − p_n) ≤ 186, with a Lean 4 development (openai/PrimeGaps186) whose three main theorems are conditional on three declared axioms: two finite-field bounds quoted from the literature and one numerical axiom of 152 inequalities supported by a Python/FLINT certificate. The bound and its proof are OpenAI's. This note reports what an outside party could re-do, under rules sealed before each stage. The Lean development builds as shipped; Comparator's result reproduces and it rejects two altered statement files; three kernels accept; the theorems rest on exactly the three standard axioms and the three declared ones. The two finite-field axioms hold on every instance for the 303 primes below 2,000, by two exact deciders that share no code. The certificate cannot run on any released FLINT (a defect fixed upstream and cited by OpenAI's own numerical note); on FLINT 3.6.0 plus that one fix it passes and reproduces all 152 printed integers. Programs written from the Lean statement file and the numerical note alone enclose all 152 quantities, each inside the interval the certificate's own run prints (two of them only once a recurrence of the note is used as written), and the final inequality holds on these numbers. None of this proves an axiom, and none of it verifies the bound 186. The numerical axiom bounds integrals, while every program computes upper estimates of them; that each integral is at most its estimate is argued in OpenAI's note and re-derived here by hand, and is not formalized. No human has refereed the hand derivations. The programs, the Lean anchors and the hand derivations were written by Claude (Anthropic) under the author's direction. The records (rules, verdict records with their gaps first, programs, results) are in the accompanying archive.