We compiled OpenAI’s Lean proof of the perfect-matching counting theorem. Here is what that does and does not show.
By The Lockadin · ExoAI-S research note · October 10, 2026
On October 6, 2026, OpenAI released a collection of mathematical manuscripts produced by an internal model, with Lean formalizations for some of them. Entry 113 claims a result that had been open since 1989: a fully polynomial randomized approximation scheme for counting perfect matchings in general graphs. Jerrum, Sinclair and Vigoda settled the bipartite case in 2004; Štefankovič, Vigoda and Wilmes showed in 2017 that the obvious extension of their method fails on general graphs.
A public discussion of the release asked that three facts be recorded separately for each result: that a Lean artifact exists, that someone outside compiled it, and that the formal statement says what the paper claims. For entry 113 we could find no public record of the other two, so we did them on one ordinary PC.
What we did
- Fetched the Lean development for the result at commit fd4aeeb2 of the repository: 415 files, 3.1 MB, about 4,400 declarations, all in the import closure of the file that proves the main statement. A text sweep found no "sorry", no "axiom", no "admit" and no "native_decide".
- Compiled it with Lean 4.34.1 against the Mathlib revision the repository pins (d13f23b7), using the Mathlib community's build cache for Mathlib itself. All 415 modules compiled. The main theorem elaborates with the type OAI.MatchingFPRAS.MainStatement, and the axiom check reports exactly propext, Classical.choice and Quot.sound, the three the repository's own comparator configuration permits.
- Read the formal statement against the paper's Theorem 1.1. The formal version ranges over every finite simple graph, defines the count as the number of perfect matchings, fixes a single-tape machine with an eight-symbol alphabet that consumes one fair random bit per step, demands a polynomial time bound on every execution, requires the output to lie within the stated relative error with the stated probability, and forces output zero whenever no perfect matching exists. We found no loophole: no restricted graph class, no padded encoding, no way for the machine to do unbounded work per step, and no way for the correctness predicate to hold vacuously. Where it differs from the paper it is slightly stronger. The details are in Appendix B.
What this shows
The Lean kernel accepts a proof of a statement that we read as a faithful rendering of the theorem, from the standard axioms, on an independent machine. Relative to the kernel, the definitions and those axioms, the theorem is established.
What this does not show
We did not run OpenAI's comparator, whose sandbox component is Linux-only, and we did not re-check the kernel's work with an independent checker. The statement is an existence claim: a finite machine exists; the proof builds it through non-computable definitions, so the program is not extractable from the proof as written. "Polynomial time" is relative to the single-tape model, which is polynomially equivalent to the usual ones, with an unspecified exponent, as in the paper. The paper's corollary on sampling and f-factors is outside the formal statement. We did not referee the written proof. The repository's own catalogue records its Lean library as produced by an agent with review status "unchecked"; a kernel check does not depend on who wrote the proof, but whether the formal statement means what the paper means is exactly what a human review covers, and we have supplied one reading of that match, not a review. And none of this bears on whether the algorithm is practical: a faithful implementation needs more steps for a two-vertex graph than there are atoms in the universe, which the manuscript itself anticipates.
The repository accepts neither issues nor discussions, so we have no way to ask its maintainers why their catalogue of formalized main results does not yet list this entry while their documentation describes it as formalized. If that is a lag, this receipt may save someone a step; if there is a reason, we would welcome the correction.
Our direction remains human-supervised research with clear limits and results that can be checked.
Onward and outward.
Appendix A. Verification receipt
| Item | Value |
|---|---|
| Repository and commit | github.com/openai/math at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb (October 7, 2026) |
| Formal statement | lean/ComparatorChallenges/MatchingFPRAS.lean, SHA-256 4abf101356d20df631636dd209a4a659206be321f287fb151c7958adc2c454d0 (states thm_main with sorry; the challenge) |
| Proof entry point | lean/OAI/Combinatorics/MatchingCount/Main.lean, SHA-256 12782e5d66d5ab395ad4f3cff9e4432e1fa63cdfece2ce70aa34023ee6f9edf6; Model.lean SHA-256 c88b96ff052daab63e1daf89342152a7a30a32b222fbb0ea9b5d7b1561597fc9, byte-identical to the challenge file minus the sorried theorem |
| Sources | 415 .lean files, 3,158,129 bytes, all in the import closure of Main.lean; 0 files containing sorry, axiom, admit or native_decide |
| Toolchain | Lean 4.34.1 (commit 5045d0056413266e57c625dcd7c365b10e377c52, x86_64-w64-windows-gnu), Lake 5.0.0 |
| Mathlib | d13f23b723b8a846827a245b89c10fc7d3f11612 (the revision pinned by the repository's lake-manifest.json), artifacts from the community cache (8,908 files) |
| Build | lake build of the development as a library against that Mathlib: "Build completed successfully (9338 jobs)"; 415 of 415 object files present; a second pass reported everything up to date. The first pass had three transient out-of-memory or stack-overflow process crashes under six parallel jobs on a 31 GB machine; the retry compiled the same files. |
| Main theorem | OAI.MatchingFPRAS.thm_main : OAI.MatchingFPRAS.MainStatement |
| Axioms | propext, Classical.choice, Quot.sound (exactly the permitted_axioms of MatchingFPRAS.json) |
| Artifacts | Main.olean SHA-256 6760e367299db5a18694cd167b191998cb8cd42eeddf655f0dbc42abb8494909; build log SHA-256 e3a62ced208c9f3b075330ce49b127743bc546ef1ed621bf6e5567f30eaab342 |
| Manuscript | build/main.tex of the preprint, SHA-256 dcf28553d442dfc53a9f90f7c52bd48c9e2e7e5e27b197aa7ca4be1c8daed703 |
| Date | October 10, 2026 |
Reproduction: a Mathlib checkout at the pinned revision with the cache fetched before any edit to its lakefile (an edited lakefile changes every cache key); the proof sources copied in and declared as a library whose globs cover every module under OAI.Combinatorics.MatchingCount; lake build with Lean's thread count limited; then a one-file module importing the proof's Main that runs #check and #print axioms on thm_main. Files must be written without a byte-order mark.
Appendix B. Statement-fidelity review
Question: does the formal statement say what the paper's Theorem 1.1 claims, with no loophole? Line numbers refer to the challenge file (CH) and to the manuscript's main.tex.
| Formal object (CH lines) | Paper notion (tex lines) | Relation |
|---|---|---|
| GraphInput (8–11): n : ℕ, edges : Finset (Fin n × Fin n), every edge (i, j) with i < j | finite simple undirected graph G = (V, E) (121–122) | equal up to vertex relabelling |
| Z G (14–23): the number of subsets of the edge set in which every vertex meets exactly one edge | Z(G), the number of perfect matchings (124–125); the empty graph has one (345) | equal, including Z(∅) = 1 |
| encodeInput (38–42): binary n, binary edge count, lexicographically sorted edge list, ε and δ as reduced numerator and denominator | "standard explicit encoding", binary vertex count (2853–2858) | one concrete instance; no padding; the formal bound is at least as strong |
| RandomMachine, tick, run (45–72): states : ℕ, a transition table on (state, symbol, random bit), symbols Fin 8, one bi-infinite tape, halt or move or write per step | "uniform classical randomized algorithm", bit cost, fair bits (133, 2971, 3030) | a concrete single-tape Post–Turing machine with one fair bit per step; polynomially equivalent |
| timeBound (81–82): C·(encoded length + ⌈1/ε⌉ + ⌈log₂⌈1/δ⌉⌉ + 1)^d, with C > 0, and clause 1 (98) demanding a halt and a well-formed output on every tape | worst-case bit time polynomial in the input length, 1/ε and log(1/δ), on every execution (140–142) | equal |
| Outputs (74–77) and 0 ≤ q (98): the head's cell and the right half of the tape equal the encoding of a reduced rational | returns a nonnegative rational estimate (134–135) | equal; the output is unique per tape |
| goodTapes (84–89) and clause 3 (100): the fraction of t-bit tapes whose output lies in [(1−ε)Z, (1+ε)Z] is at least 1 − δ | P[(1−ε)Z ≤ estimate ≤ (1+ε)Z] ≥ 1 − δ (136–139) | equal; the counting fraction is the probability under fair bits |
| clause 2 (99): Z G = 0 implies output 0 on every tape | zero with certainty when no perfect matching exists (140) | equal |
| hypotheses (96): 0 < ε < 1 and 0 < δ < 1/2 over ℚ | rational 0 < ε < 1, 0 < δ < 1/2 (133–134) | equal |
| not present | Corollary 10.1: f-factors, k-matchings, near-uniform sampling (3098–3122) | not covered by the formal statement |
Points checked in detail: every finite simple graph is isomorphic to some GraphInput and the count is isomorphism-invariant, so coverage is complete, including n = 0 and odd n; the transition function's domain and codomain are finite types, so any Lean function of that type is a finite table and the existential quantifier ranges over finite programs, with the machine and the constants bound before the graph and the parameters, which is uniformity; the step function sees only the state, the head symbol and one bit, so no oracle, no unbounded per-step work and no access to the graph beyond the tape; the output encoding uses no blank symbol and parses uniquely, so at most one rational per tape and the correctness predicate cannot hold vacuously; a time bound too small to read the input would simply falsify clause 3 for some graph rather than make anything vacuous. Where the formal statement differs from the paper it is more concrete or slightly stronger: a fixed machine model, a fixed encoding, output in reduced form, an explicit bound on random bits as well as time.
Residual caveats: the witness machine is built through non-computable definitions and is not extractable as a program from this proof; classical choice is a permitted axiom, so the proof may be nonconstructive, which is standard for an existence claim; polynomial time is relative to the single-tape model with an unspecified exponent, as in the paper; the comparator's own checks (statement equality enforced by tool, axiom allow-list enforced by tool) were replaced here by a byte comparison against the challenge file and by #print axioms; no independent kernel re-check was run.
