Re-checking OpenAI’s
189 formal maths results
A checked proof establishes its Lean statement—not every claim in the paper.
Research record
- Published
- Draft date · preview only
- Work done
- Found by
- Claude Opus 5.5Statement audit
- Cross-checked by
- Grok 4.7Flags and a blind sampleGemini 3.1 Pro & fresh Claude reviewersThe three flags
- Verdicts by
- Lean kernel · nanoda · ComparatorKernel checks and published-statement checks, not paper-scope judgements
- Checked with
- Lean 4.34.1
Mathlibd13f23b7…
Repofd4aeeb - Topics
- Lean · formal proofs · OpenAI · statement audit
- Lean kernel · both runs
- 189/189
- nanoda · 7 without a verdict
- 182/189
- Statement audit · AI judgement
- 186 match
3 gaps
Summary
What this does not show
A pass here means a valid proof of the stated Lean theorem. It does not establish every claim in the paper, or that every formal statement captures its paper. Neither a wrong proof nor a wrong paper is shown.
The statement audit is AI judgement, not a proof-checker verdict. It remains open to human review.
On 9 October 2026, we re-ran all 189 formal proofs in OpenAI’s collection of recent mathematics papers, using OpenAI’s pinned versions of Lean and Mathlib.
The Lean kernel accepted all 189, in both runs. The second run built from source; a fingerprint check found no changed or missing statement or library build files. Comparator agreed in both runs that each proof proves its published statement.
nanoda, an independent Lean checker, accepted 182 of the 189. The other seven runs crashed because of stack or memory limits. Those are neither rejections nor second confirmations.
We used Claude Opus 5.5 to compare the statements with the papers and OpenAI’s scope notes. The audit recorded 186 as matching the headline claim or as openly scoped partial formalizations. It flagged three statements that prove less than the papers’ headline claims.
The reviewers agreed on the facts of those three gaps. They differed on how clearly OpenAI’s notes disclose them. In particular, Gemini 3.1 Pro’s final view on EntangledGames was that the note does disclose the narrower bound.
What we checked
OpenAI’s repository contains 189 challenges, each with a Lean statement, a proof and a short scope note. We checked commit fd4aeeb with its exact toolchain: Lean 4.34.1, Mathlib revision d13f23b7…, 42 pinned library versions and OpenAI’s compatibility patches.
All 42 library revisions were identical after a fresh dependency update. Two challenges depend on about 24,000 lines of OpenAI’s Lean definitions across 69 files; their passes cover those definitions as written.
One challenge, HarmonicGrowth, declares an axiom it never uses. The unused declaration was noted; it was not used by the proof.
How we checked
The proofs
Each proof was compiled and checked by the Lean kernel inside a fixed container image. We did this twice. The strict second run built everything from source and compared SHA-256 fingerprints of all 177,641 build files before and after. None changed or went missing. Every library file in the image matched the git blob hash of its upstream repository.
Build files changed or missing in the strict run’s before-and-after fingerprint check.
An independent kernel
We also ran nanoda on each result. It accepted 182. Six of the remaining runs overflowed the stack even at 4 GiB; one ran out of memory at 340 GB. Two of the 182 passes required a nanoda build with a larger stack, made with a one-line change. OpenAI’s configuration requested nanoda for just one of the 189.
The published statements
Comparator checked that each proof proves exactly the published Lean statement. This is separate from asking whether that statement captures the paper’s headline claim.
The papers and scope notes
We used Claude Opus 5.5 as Claude Code sub-agents, with 16 running in parallel and about 12 results per reviewer. Each read the Lean statement, OpenAI’s scope note and the paper’s LaTeX source. The audit’s match category allowed a partial formalization when the scope note disclosed it.
Grok 4.7 re-checked every flag and a blind sample of match verdicts. Gemini 3.1 Pro and fresh Claude reviewers then re-checked the three flags. They first saw each statement blind and were asked to defend it before being shown the finding.
Recorded re-check · work done 9 Oct 2026
Different questions,
different checks.
Proof verdicts and scope judgements are different kinds of evidence.
- 189 challenges A Lean statement, a proof and a short scope note.
- Lean kernel 189 / 189 · Accepted in both runs
- nanoda 182 / 189 · Seven checker crashes gave no verdict.
- Comparator Each proof proves exactly the published Lean statement.
- Claude Opus 5.5 Statement audit · 186 match / 3 gaps
- Grok 4.7 Flags and a blind sample
- Gemini 3.1 Pro & fresh Claude reviewers The three flags
The proof verdicts
All 189 configurations pass the Lean kernel, with zero failures in both runs. Comparator agreed in both runs. nanoda supplied an additional kernel verdict for 182.
Accepted in both runs; Comparator agreed.
Accepted. Seven checker crashes gave no verdict.
AI scope judgements, not additional kernel verdicts.
The strict-run summary records total: 189, lean_kernel_accepts: 189 and both_kernels: 182, alongside the seven results without a nanoda verdict.
The first run took place from 02:35 to 04:00 UTC; the strict run from 07:26 to 11:50 UTC on 9 October 2026. nanoda retries ended at 15:37 UTC.
The three gaps
Claude alone judged 157 statements a match. Another 28 were confirmed in Grok’s blind sample. One, QuasiRiemannHypothesis, on which Grok disagreed, was settled by the Lean kernel in OpenAI’s favour. That accounts for 186.
The other three are statement-vs-headline gaps, not wrong proofs. The reviewer assessments below concern scope and disclosure.
EntangledGames
- Lean statement
- A bound with δ13
- Paper’s theorem
- A bound with δ5
The Lean theorem proves the δ13 bound, not the paper’s δ5 bound.
- Claude Opus 5.5
- Rated the gap major.
- Grok 4.7
- Confirmed the gap as real.
- Gemini 3.1 Pro
- Initially partial agreement; final view: OK, because the δ13 bound is stated openly.
- Fresh Claude
- A mismatch, rated minor.
Shared finding: the bounds differ. Gemini’s final view was that OpenAI’s note discloses this.
YauCounterexample
- Lean statement
- √λ growth
- Paper’s title result
- A power law
The Lean theorem establishes √λ growth rather than the paper’s title result.
- Claude Opus 5.5
- Rated the gap major.
- Grok 4.7
- Confirmed the gap as real.
- Gemini 3.1 Pro
- A real mismatch.
- Fresh Claude
- Faithful to its label; a minor disclosure gap.
Shared finding: the Lean theorem covers less than the title result. Reviewers differed on the disclosure.
SurfaceConeCandidateSupport
- Lean statement
- Satisfied by ℂ[[x,y,z]]
- Scope gap
- Checks nothing about the paper’s ring
The textbook ring ℂ[[x,y,z]] satisfies the Lean statement, so that statement does not check the paper’s ring.
- Claude Opus 5.5
- Rated the gap major.
- Grok 4.7
- Confirmed the gap as real.
- Gemini 3.1 Pro
- Found it independently in the blind review and rated it critical.
- Fresh Claude
- Near-empty but disclosed; rated minor.
Shared finding: the statement does not constrain the paper’s ring. Reviewers differed on the significance of the scope note.
All four reviewer passes agreed on the facts of each gap. Their assessments of OpenAI’s disclosure were not unanimous. We report that spread as found rather than collapsing it into a single verdict.
Limits of the audit
- No wrong proof or wrong paper is shown. The three flags concern the relationship between a formal statement and a headline claim.
- Scope matching is AI judgement. The lowest reviewer confidence was on the deepest definition stacks: CharacterVarieties at 0.6 and CartierChart at 0.7.
- The blind spot-check was incomplete. Grok covered 29 of a planned 51 match verdicts. Its blind pass independently caught only one of the three gaps.
- Seven results lack a nanoda verdict. Crashes are not rejections, but they are not independent confirmations either.
- The swarm’s 72 proofs are re-proofs. They re-prove lemmas OpenAI had already proved: evidence of the swarm working, not new mathematics.
Who did what
We used Claude. Claude Opus 5.5 performed the statement audit as Claude Code sub-agents on 9 October 2026. Grok 4.7 cross-checked the flags and a blind sample. Gemini 3.1 Pro and fresh Claude reviewers re-checked the three flags; the fresh Claude reviewers’ exact model was not recorded.
The proof verdicts belong to the Lean kernel. nanoda supplied the second kernel verdicts, and Comparator confirmed that each proof proves its published statement. These checks do not turn the models’ paper-scope judgements into formal proofs.
No human expert has reviewed the three statement gaps. Human review may be added at any time; it is not a gate.
The evidence
The recorded evidence separates the checker runs from the statement audit.
Checker records
apps/supercomputer/data/checker/strict/
The per-result run summary, build and fingerprint logs, the seven nanoda crash logs, environment and library manifests, and container image ID.
Statement-audit records
apps/supercomputer/data/audit/
The per-result Claude and Grok passes, Gemini and fresh-Claude reviews, and the final table.
These are record locations, not download links. This preview does not bundle the repository or its logs.
Recorded results are never rewritten. Any correction to this page is a new, dated entry below.
Corrections
No corrections recorded in this draft.
Keep reading
Sample cards · no research articles attached