Theoretical computer science · Result 113

Approximate counting and entropy of perfect matchings

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs

OpenAI · September 23, 2026

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}\).

Read PDF Download Source

Cite

@misc{OAI:A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026,
  author = {{OpenAI}},
  title = {{A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/main.pdf}{OAI:A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026}},
  year = {2026}
}

Entropy and Face Dimension of the Perfect-Matching Polytope

OpenAI · September 23, 2026

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 F_x is the minimal face of the perfect-matching polytope containing x.

Read PDF Download Source

Cite

@misc{OAI:Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026,
  author = {{OpenAI}},
  title = {{Entropy and Face Dimension of the Perfect-Matching Polytope}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026/main.pdf}{OAI:Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

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.

Comparator links

Result	Comparator statement
Randomized approximation of the perfect-matching count	MatchingFPRAS.lean
Perfect-matching entropy bound	MatchingEntropy.lean
Deterministic approximate matching count	BinaryMatching.lean
Approximate counting with singleton loops	SingletonLoopMatching.lean
Refined pointwise perfect-matching entropy bounds	MatchingEntropyBounds.lean
Face correspondence under triangle expansion	TriangleFace.lean

Scope note on GitHub →