An independent audit of OpenAI’s ten-proofs

The object, at pinned bytes

The repository is 548,215 lines of Lean in ten chapter files, a twelve-entry formalization.yaml, and twelve Comparator challenge files. The PDF contains no verification appendix; the manuscript and its formal counterpart meet only through declaration names. That correspondence is what an audit can check, and it is what this one checked.

Build, kernel, axioms

lake build All at the pin: Build completed successfully (8666 jobs), exit 0, on a 16 GB laptop, mathlib from the community cache. A prior public build attempt deserves its credit here: Curtis Pyke (kingy.ai, 1 August) built most of the tree first-hand within a day of release, stopped short of completion when his local task runner terminated the process, and wrote plainly that his check “is not an independent proof audit.” His counts (8,820 of 9,007 jobs compiled) sit beside ours (8,666 completed); the runs used different targets and toolchain states, and we report all three numbers rather than reconcile them.

#print axioms through the built environment, for all twelve declarations named in formalization.yaml: every one depends on exactly [propext, Classical.choice, Quot.sound] — the minimal classical base — with no sorryAx, no native_decide axiom, nothing else. A tree-wide sweep found zero escape hatches — no sorry, no admit, no unsafe, no @[implemented_by], no axiom declarations — in 548K lines, outside the challenge statement files, which carry sorry by design (they are the statements Comparator matches proofs against). And two theorems the manifest never mentions check to the same three axioms — more on those below, because they are the audit’s most interesting class of finding.

The ten advances, one by one

Each advance, its claim in one line, and this audit’s verdicts as tags. green = a check that ran and passed · teal = the machine-checked statement is stronger than the paper’s claim · slate = a referee note · oxblood = a finding that needs attention. “cross-kernel” means the shipped Comparator challenge passed both the Lean kernel and nanoda; “faithful” means the challenge statement matches the paper’s theorem at statement level.

• 1Sphere packing — the exact exponential rate of the Cohn–Elkies linear program: LP_d^1/d → √(e/2π), the conjectured rate of Afkhami-Jeddi–Cohn–Hartman–de Laat–Tajdini, proved.
  builds3 axiomscross-kernelfaithfulpriority corroboratedthm 1.2 unchallenged

  The challenge pins the headline theorem and a genuine packing-density bridge (density defined, not assumed). The second theorem (sign-uncertainty radii) is outside the challenge set; its in-tree half covers one of the two signs, over a narrower class than the paper states, and is kernel-clean.

• 2Binary & spherical codes — strict improvements over the optimized 1977 (MRRW) and 1978 (Kabatianskii–Levenshtein) exponents, the general records of five decades.
  builds3 axiomscross-kernel ×2faithfulpriority shared

  Survives the trap its own chapter names: strict inequality against the fully optimized second bound, for every distance; the spherical hierarchy is machine-stated down to the kissing-number corollary. The flag: Alrabiah–Guruswami improved the same two binary bounds by a different method, nine days later — a shared first, human and machine.

• 3Non-sofic groups — an explicit non-sofic group exists (the unit group of the binary Leavitt algebra), answering Gromov’s question.
  builds3 axiomscross-kerneltwo-way seammachine > paperproof restructured in week 1

  The sharpest finding of the audit: the chapter’s stated theorem is not the machine-checked statement, and the machine-checked statement (a finitely presented non-sofic group exists — stronger) is not stated in the paper. Week one also restructured this chapter’s proof and added a hypothesis to the cited Kun–Thom theorem that its source does not state — while Kun and Thom’s own revision credited the manuscript by name.

• 4Connes rigidity — infinitely many pairwise nonisomorphic ICC property-(T) groups with isomorphic group factors; Popa’s finite-to-one question answered in the negative.
  builds3 axiomscross-kernelfaithfulnormality def flagged

  The challenge does not shortcut the operator algebra: ℓ²(G), the left regular representation, the group von Neumann algebra and its trace are constructed, and Popa’s question sits verbatim at the cited page of his 2013 problem list. One referee question is flagged, not resolved: normality is rendered via projection suprema rather than the textbook continuity definition.

• 5Permanent complexity — superquadratic circuit lower bounds (n²·log log n scale) and near-quartic formula bounds for the permanent.
  builds3 axiomscross-kernel (formulas)faithful (formulas)headline unchallenged

  Both formula bounds are challenged and pass. The chapter’s headline circuit theorem is fully proved in the tree — we kernel-checked it to the same three axioms — but absent from the manifest and the challenge set: the clearest instance of the audit surface under-reporting the tree.

• 6Quantum parallel repetition — uniform exponential decay of the entangled value under parallel repetition, for every finite two-player game.
  builds3 axiomscross-kernelfaithful

  The bespoke machinery is the right machinery: finite-dimensional entangled strategies, POVMs with completeness, the Born rule, and the ε¹³/(ε+log|A||B|) exponent exactly as stated; the boundedness lemmas that keep its suprema honest are in the tree.

• 7Closest vector problem — deterministic NP-hardness of GapCVP with polynomial factor n^1/400, without the PCP theorem, with coding-theory consequences.
  builds3 axiomscross-kernelmachine > paperTMs in the statementchecked off-VM

  The audit’s biggest fear answered structurally: NP and polynomial-time reductions are defined via mathlib’s Turing machines inside the trusted statement, and the challenge proves hardness for all of NP where the paper states a 3SAT reduction. All three consequences are pinned. The slate tag: this module’s checks ran on our own machine after exceeding hosted-VM memory three times — deviations recorded in the log.

• 8Ehrhart’s volume conjecture — the sharp bound vol(K) ≤ (n+1)ⁿ/n! for convex bodies whose barycenter is their only interior lattice point, in every dimension.
  builds3 axiomscross-kernelfaithfulsharpness witnessed

  Hypothesis-for-hypothesis the paper’s theorem, over honest measure-theoretic definitions — and the challenge also proves the centered simplex attains the constant, so the bound’s sharpness is machine-checked, not asserted.

• 9Multicolor Ramsey — R_k(3) ≥ (ck^1/3/log k)^k, settling R_k(3) = k^Θ(k).
  builds3 axiomscross-kernelmachine > paperprior record verified

  The machine-checked constant is explicit — 1/(6e³⁸) — where the paper leaves c unnamed, and the credited prior record’s 380 base is verbatim in its source’s own amplification inequality.

• 10Compactness & degeneracy — the Erdős–Simonovits compactness conjecture and Erdős’s degeneracy conjecture (at r = 2) both disproved, quantitatively.
  builds3 axiomscross-kernel ×2faithfulquantitative

  Both counterexamples are challenged and pass, with the exponent identity 21/16 = 4/3 − 1/48 pinned as an explicit arithmetic conjunct — the gap between the family bound and its members is machine-checked, not narrated.

Score at a glance: ten of ten build and kernel-check to the minimal classical base; twelve of twelve shipped challenges pass both kernels; the attention items are chapter 3’s seam, chapter 5’s unchallenged headline, and chapter 2’s shared priority. The sections below carry the detail behind every tag.

The repository’s own audit protocol, executed

The repo ships twelve challenge configurations for Comparator, the Lean FRO’s cross-kernel proof judge: each pins the exact statements, permits exactly the three classical axioms, and enables nanoda — an independent second kernel — alongside Lean’s. Comparator’s sandbox (landrun) requires the Linux Landlock LSM, so these runs executed on fresh single-use Linux VMs, with the Landlock probe as the first step of every job and every tool’s commit recorded in every log.

One configuration observation, credited where it belongs: the repository pins a Comparator from one merge before the fix in comparator PR #60 (merged 31 July 2026 — before the manuscript’s release), which inserts the -- terminator that current landrun’s CLI otherwise consumes. Followed exactly as shipped — the pinned manifest plus Comparator’s instruction to build landrun from main — every challenge fails before reaching the mathematics, with the same symptom PR #60 fixed. The mechanism and fix are upstream’s — matteo-ax’s, by that PR — not ours; our contribution is only the measurement that the shipped pin predates it, and the workaround (build landrun at its pre-cli-v3 commit, or bump Comparator past the fix) that makes the shipped protocol runnable.

The verdicts: eleven of the twelve challenges — sphere packing, binary codes, spherical codes, the permanent formula bounds, the non-sofic existence, Connes rigidity, Ehrhart, quantum parallel repetition, Ramsey, and both chapter-10 counterexamples — completed with “Your solution is okay!” and exit 0 under the hardened invocation from Comparator’s README: per its contract, each proves the same statements as the challenge files, uses no more than the three permitted axioms, and is accepted by both the Lean kernel and nanoda. The twelfth (GapCVP) is the tree’s largest module, and its run failed in three hosted configurations — an oom-kill at 7.0 GB inside the hardening scope, a VM shutdown under swap, and a rebuild-forcing trace mismatch when pre-built artifacts were seeded (the rebuild then re-hitting the same memory ceiling). Its checks therefore ran on a 16 GB machine of ours, through Comparator’s own COMPARATOR_LANDRUN environment hook, with the sandbox replaced by a flag-compatible passthrough — a deviation the run log itself records, and a defensible one: the sandbox’s threat model is an adversarial solution build, and nothing was built there beyond artifacts we had already built ourselves. Result: nanoda accepts; the Lean kernel accepts; “Your solution is okay!” Twelve of twelve.

Every log carries its environment record — tool commits, kernel, LSM list, toolchain, UTC date — and the one macOS log additionally records the passthrough and one replaced foreign-platform binary, so the deviations are in the artifact, not in a footnote.

Statement faithfulness: no weakening found — and two patterns the other way

All twelve challenge statements were read in full against the manuscript’s own theorem statements and definitions. The traps a referee would look for do not fire. Chapter 2’s challenge pins strict inequality against the fully optimized second MRRW bound for every distance — the exact trap the chapter itself warns about (“improving M₁ alone need not improve M₂”) — and decomposes the theorem’s chain faithfully. Chapter 7 defines NP and polynomial-time reductions via mathlib’s actual Turing-machine machinery inside the trusted statement. Chapter 6’s entangled value is the genuine finite-dimensional supremum, and the boundedness lemmas that keep its suprema honest (winProbability_le_one, entangledValue_le_one) are present and kernel-checked with the module. Chapter 8’s hypotheses map one-for-one onto measure-theoretic definitions. No published statement-level comparison of this repository was located — a documented search, stated with its limits in the closing section; the question itself had been posed publicly.

The discrepancies we did find run in the repository’s favor, in two systematic patterns:

• The machine sometimes proves more than the paper claims. The chapter-3 challenge proves a finitely presented non-sofic group exists — a statement the manuscript never makes (“finitely presented” occurs three times in 253 pages — twice describing tools, once as a non-example). The chapter-7 challenge proves hardness for all of NP where the paper states a 3SAT reduction. The chapter-9 challenge makes the Ramsey constant explicit where the paper leaves it unnamed.
• The audit surface under-reports the tree. Chapter 5’s headline circuit lower bound and the in-tree half of chapter 1’s second theorem are fully proved — same three axioms, we checked — but absent from the manifest and the challenge set. A reader who “runs all the challenges” has checked 13 of the 16 numbered main claims.

Chapter 3 deserves its own sentence, because it is the sharpest seam we found: the chapter’s stated Theorem 1.1 (“the unit group L_F₂(1,2)^× is not sofic”) is not the pinned Lean statement, and the pinned Lean statement is not stated in the paper. Neither object is wrong; their correspondence is asserted by nothing but proximity. That is precisely the kind of gap a verification appendix would close, and this manuscript has none.

The week the humans wrote back

The 6 August revision (the original is preserved at a public URL — an auditable diff pair, and no published analysis of it was located) was not cosmetic. It added the table of contents; strengthened attribution in the front abstract — Kun, Kun–Thom, and Thompson’s group V named where the original said only “property-(T) expanders”; added citations (Cohn–Miller in chapter 1, Fujita in chapter 8, and a clarification of Connes’s original formulation credited — in chapter 4’s own acknowledgments — to Ionuţ Chifan); restructured chapter 3’s proof, replacing a multi-page expander-repair argument; and quietly inserted the word “infinite” into the stated hypothesis of the cited Kun–Thom theorem. We fetched the source: Kun–Thom’s own Theorem 1.1 reads “countable Kazhdan group,” with no infiniteness clause — the added hypothesis is harmless if the group it is applied to is infinite there — plausible, as that group is Thompson’s V — but it is not textually sourced.

The traffic ran both ways, and this is the part of the story we located nowhere else. Kun and Thom posted their own revision on 4 August — their v3’s preface says the paper was finished in mid-July 2026, and continues: “On August 1, 2026, we learned about the breakthrough result of OpenAI. The proof of their key Proposition 2.3 in [20] is a creative and effective application of the results and techniques of this paper and the ones in [18].” Chapter 4’s revised acknowledgments disclose independent concurrent work by Shuoxing Zhou on Connes rigidity. And on 10 August, Alrabiah and Guruswami posted an improvement of the same two 1977 binary-code bounds by an entirely different method, writing: “Concurrent work by OpenAI also improves the first and second MRRW bounds, albeit using a different approach” — and, separately, that the quantitative improvements to the first bound “match,” with the second-bound improvement “captured by our framework” (quotes from the paper’s HTML body). The manuscript’s dated priority claims check out at their sources — the intervening sphere-packing literature calls its own gains constant-factor in its own abstracts — but chapter 2’s “first improvements since 1977” is now a shared first, human and machine arriving nine days apart.

What the repository discloses that the manuscript does not

The PDF’s entire methodology disclosure is “an internal OpenAI model.” The repository’s formalization.yaml says more: model “Astra (OpenAI)”, framework “Codex”, wall time “1 week”, review status “agent-reviewed” — not human-reviewed. The repository has issues disabled, zero pull requests ever, and six forks, none carrying an independent commit; its repository object dates to 5 August, and its single commit is authored 2 August 2026 under a human name — Boris Alexeev — with the one-character commit message “.” (public commit metadata, read from the GitHub API). The manuscript names no humans; the repository, read closely, names one. Whatever conversation this work deserves is not currently happening on the artifact itself.

What this audit does not establish