Approximate counting and entropy of perfect matchings
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Gives a fully polynomial randomized approximation scheme for counting perfect matchings in arbitrary finite simple graphs, with exact detection of zero counts. Also proves the perfect-matching entropy conjecture of Anari, Oveis Gharan, and Vinzant, bounding the maximum entropy of a matching law at every feasible edge-marginal vector in a loopless labelled multigraph, including boundary points. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
The other possible matches are Theorem 1.1 in A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs () and Theorem 1.2(Deterministic approximate counting) in the same paper ().
Let G be a loopless multigraph on 2m\ge2 vertices with at least one perfect matching. For every x\in P(G),
F(x)-\left(2-\frac2m\right)B(x)
\le H(x)\le F(x).
Reported proof verification
Six Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
We give a fully polynomial randomized approximation scheme (FPRAS) for counting perfect matchings in arbitrary finite simple undirected graphs, resolving the general-graph perfect-matching approximation problem. The algorithm returns zero with certainty when no perfect matching exists. Otherwise, it achieves relative error ε with failure probability at most δ in worst-case bit time polynomial in the input length, \(\varepsilon ^{-1}\), and \(\log\delta^{-1}\).
We prove the perfect-matching entropy conjecture of Anari, Oveis Gharan, and Vinzant. For every feasible vector x of perfect-matching edge marginals in a loopless labelled multigraph on \(2m\ge2\) vertices, the maximum entropy \(H(x)\) of a matching law with marginals x satisfies \(\displaystyle F(x)-(2-2/m)B(x)\le H(x)\le F(x),\) where \(F(x)=-\sum_e x_e\log x_e\) and \(B(x)=-\sum_e(1-x_e)\log(1-x_e)\). This bound holds throughout the polytope, including its boundary. We also prove the sharp bound \(|\mathop{\mathrm{supp}}\nolimits x|-\dim F_x\le3m-2\), where Fx is the minimal face of the perfect-matching polytope containing x.
Six Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
There is a uniform classical randomized algorithm which, given G and rational parameters 0<\eps<1 and 0<\delta<1/2, returns a nonnegative rational number \widehat Z such that
If Z(G)=0, the output is zero with certainty. The worst-case bit running time is polynomial in the input encoding length, \eps^{-1}, and \log\delta^{-1}.
The words they share: encoding, time, input, length, bit, polynomial, graphs, perfect, matchings.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
BinaryMatching.lean, the release lists it as a main result.
theoremdeterministic_approximate_counting : ∃ A : Input → ℕ, ∃ machine : Turing.TM2ComputableInPolyTime encodeInput Nat.bits A, (∀ k, Finite (machine.tm.Γ k)) ∧ (∃ P : Polynomial ℕ, ∀ G,(A G).bits.length≤P.eval (encodeInput G).length) ∧ ∀ G,A G≤count G ∧ count G≤2^(9*G.n)*A G ∧ (A G=0 ↔ count G=0) := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
MatchingEntropy.lean, the release lists it as a main result.
theorementropy_main (G : LooplessGraph V E) (m : ℕ) (hm : 0 < m) (hV : Fintype.card V = 2 * m) (hPM : Nonempty G.Matching) (y : E → ℝ) (hy : y ∈ G.polytope) : marginalEntropy y - maxMatchingEntropy G y ≤8 * (m : ℝ) * (1 - Real.exp (-marginalEntropy y / (m : ℝ))) := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
MatchingEntropyBounds.lean, the release lists it as a supporting statement.
theoremRefined.pointwise_entropy (G : LooplessGraph V E) (m : ℕ) (hm : 0 < m) (hV : Fintype.card V = 2 * m) (hPM : Nonempty G.Matching) (x : E → ℝ) (hx : x ∈ G.polytope) : entropy x - (2 - 2 / (m : ℝ)) * complementEntropy x ≤ maxMatchingEntropy G x ∧ maxMatchingEntropy G x ≤ entropy x := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
There is a uniform classical randomized algorithm which, given G and rational parameters 0<\eps<1 and 0<\delta<1/2, returns a nonnegative rational number \widehat Z such that
If Z(G)=0, the output is zero with certainty. The worst-case bit running time is polynomial in the input encoding length, \eps^{-1}, and \log\delta^{-1}.
The words they share: 1/2, parameters, randomized, encoding, output, rational, returns, nonnegative, time, log, uniform, input, length, bit, polynomial, zero, approximation, scheme, fully, graphs, perfect, matchings, delta.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
MatchingFPRAS.lean, the release lists it as a supporting statement.
defMainStatement : Prop := ∃ (A : RandomMachine) (C d : ℕ), 0 < C ∧ ∀ (G : GraphInput) (ε δ : ℚ), 0 < ε → ε < 1 → 0 < δ → δ < 1 / 2 →let t := timeBound C d G ε δ (∀ bits : Fin t → Bool, ∃ q : ℚ, 0 ≤ q ∧ Outputs A (encodeInput G ε δ) bits q) ∧ (Z G = 0 → ∀ bits : Fin t → Bool, Outputs A (encodeInput G ε δ) bits 0) ∧ ((goodTapes A G ε δ t).card : ℚ) / (2 : ℚ) ^ t ≥ 1 - δ⋮theoremthm_main : MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
There is one uniform deterministic algorithm which, on a graph on n vertices with nonnegative binary integer pair multiplicities, returns an integer A\ge0 satisfying
N(G)/512^n\le A\le N(G).
Its running time and output length are polynomial in the input bit length. In particular, A=0 exactly when N(G)=0. The guarantee includes a compact input consisting of binary n and a list of positive pair records.
The words they share: algorithm, approximate, binary, counting, deterministic, graph, input, length, nonnegative, polynomial, returns, running, time, vertices.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
SingletonLoopMatching.lean, the release lists it as a main result.
defFullEndpoint : Prop := ∃ A : Input → ℕ × ℕ, ∃ machine : Turing.TM2ComputableInPolyTime encodeInput encodeOutput A, (∀ k, Finite (machine.tm.Γ k)) ∧ (∃ P : Polynomial ℕ, ∀ G, (encodeOutput (A G)).length ≤ P.eval (encodeInput G).length) ∧ ∀ G, 0 < (A G).2 ∧ (A G).1 ≤ (A G).2 * count G ∧ (A G).2 * count G ≤ 2 ^ (18 * G.n) * (A G).1 ∧ ((A G).1 = 0 ↔ count G = 0)⋮theoremfullEndpoint : FullEndpoint := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
TriangleFace.lean, the release lists it as a supporting statement.
theoremtriangle_expansion_face {V : Type uV} {E : Type uE} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LooplessGraph V E) (v : V) (hdeg : Fintype.card {e : E // G.Incident v e} = 3) (_hmatching : Nonempty G.Matching) : ∃ (c : E → Fin 3) (hc : LocalLabels G v c),let H := triangleExpansion G c v
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note:None for the FPRAS and the pointwise entropy bounds; the sharp face-dimension bound is not stated (TriangleFace is only the triangle-expansion face correspondence).
Definitions the group asks readers to compare with the paper:Randomized machine is hand-rolled: RandomMachine (single finite transition table on Turing.Tape (Fin 8), one fair coin per tick, tick = one write/move via Turing.TM0.Stmt), input encoded sparsely with binary encodeNat; maxMatchingEntropy := sSup (entropy '' feasibleLaws y) (nonempty and bounded on the matching polytope)
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
The formalization gives a fully polynomial randomized approximation scheme for counting perfect matchings in every finite simple undirected graph. For rational $0<\varepsilon<1$ and $0<\delta<1/2$, it returns a nonnegative rational estimate with relative error at most $\varepsilon$ with probability at least $1-\delta$. If the graph has no perfect matching, every execution returns zero.
The algorithm is a fixed finite-alphabet randomized machine. Its worst-case running time is polynomial in the binary input length, $\varepsilon^{-1}$, and $\log(\delta^{-1})$, including on unsuccessful random tapes.
For feasible edge marginals $x$ of perfect matchings in a loopless multigraph on $2m$ vertices, let $F(x)=-\sum_e x_e\log x_e$, $B(x)=-\sum_e(1-x_e)\log(1-x_e)$, and let $H(x)$ be the maximum entropy of a matching law with those marginals. The formalization proves $F(x)-(2-2/m)B(x)\le H(x)\le F(x)$ for $m\ge1$, including boundary points of the polytope. It retains the earlier coefficient-eight entropy bound and the deterministic counting approximations with factors $512^n$ for loopless graphs and $2^{18n}$ with singleton loops.
A further statement identifies the exact face obtained by expanding a degree-three vertex into a triangle and shows that minimal faces are carried to minimal faces by the expansion. The paper’s sharp global face-dimension bound is not part of that selected statement.
AI-drafted comparisons, with no recorded human review
Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s deterministic approximate counting theorem: a polynomial-time algorithm returning A with N(G)/512^n ≤ A ≤ N(G) for loopless graphs.
Perfect-matching entropy boundMatchingEntropy
Unreviewed AI draft: states a supporting result. States the earlier nonlinear entropy bound F − H ≤ 8m(1 − e^{−F/m}), a theorem in Section 12 of the paper that the note says is retained, rather than the headline pointwise bound with coefficient 2 − 2/m. Whether the headline bound implies it, which would make it a weaker form, was not settled here.
Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s pointwise entropy theorem F − (2 − 2/m)B ≤ H ≤ F for every point of the perfect matching polytope, including boundary points.
Randomized approximation of the perfect-matching countMatchingFPRAS
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: a fully polynomial randomised approximation scheme for the number of perfect matchings of every finite simple graph.
Approximate counting with singleton loopsSingletonLoopMatching
Unreviewed AI draft: states a supporting result. States the paper’s extension of deterministic counting to graphs with singleton loops, with factor 2^{18n} (a proposition in Section 13), rather than a headline theorem.
Face correspondence under triangle expansionTriangleFace
Unreviewed AI draft: states a supporting result. States a lemma on faces of the perfect matching polytope under triangle expansion of a degree-three vertex. The paper’s global face-dimension bound is outside it.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
The program that collects Atlas’s source records, Statement Map, could not obtain or interpret some source material. These notes describe those limits; they do not identify mathematical errors.
SingletonLoopMatching: Tracked source lean/OAI/Computability/LoopMatching/Endpoint.lean unavailable: bytes were not captured at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a algorithm and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 113The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Address a question raised in an independent assessment
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
finite, loopless, perfect, matchings
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Proposition A.2 (Supported face codimension)
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
face, loopless, graph
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary A.7 (An exact partition of the ambient edges)
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
loopless, graph, perfect, matching, vertex, bound
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 5.3 (Restriction on a universal entropy coefficient)
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
finite, loopless, graphs, bound
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 4.4 (Regular graphs with large odd cuts)
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
finite, loopless, graph, vertex
Review
Atlas records no review confirming that the two statements mean the same thing.
Why this passage is shown
Corollary 6.2 (Conservative weighted bracket)
In Entropy and Face Dimension of the Perfect-Matching Polytope, 23 September 2026
How it was found
Its words were compared with the words of the Lean statement TriangleFace.
Words they share
finite, loopless, perfect, matching
Review
Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
Their term
“full”
What their term means
The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state the headline as OpenAI wrote it.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 110 s; peak memory 6.3 GiB).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 429 s; peak memory 6.4 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 135 s; peak memory 6.1 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
No paper theorem is paired with this Lean statement.
Who ran the proof-verification program
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.