Theoretical Computer Science

Motivation: approximating the shortest common superstring

Given a finite collection $\mathcal S$ of strings, the shortest common superstring (SCS) problem asks for a shortest string $T$ that contains every member of $\mathcal S$ as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor $2$: the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.

Timeline

• 1988 — Tarhio and Ukkonen propose the factor-$2$ conjecture for the maximum-overlap Greedy procedure (Theor. Comput. Sci. 1988).
• 1994 — Blum, Jiang, Li, Tromp and Yannakakis give the first constant-factor algorithm a polynomial-time $3$-approximation (J. ACM 1994).
• 1997 — Breslauer, Jiang and Jiang use rotations of periodic strings to control overlaps (J. Algorithms 1997).
• 1999 — Sweedyk obtains factor $5/2$ (SIAM J. Comput. 1999).
• 2013 — Mucha obtains $2+11/23$ via Lyndon words (SODA 2013).
• 2019/2020 — Golovnev, Kulikov, Logunov, Mihajlin and Nikolaev introduce the all-substrings hierarchical graph and the Collapsing conjecture (APPROX/RANDOM 2019; arXiv:1809.08669).
• 2023 — Englert, Matsakis and Veselý obtain $(14+\sqrt{67})/9<2.466$ (ISAAC 2023).
• 2026 — Chukhin, Kulikov, Mihajlin and Smal report a $7/3$-approximation (ECCC TR26-157); Shibata reports a counterexample to the Greedy conjecture with ratio at least $9/4$ (arXiv:2609.01365).
• 2026 — An OpenAI preprint, A Polynomial-Time 2-Approximation for Shortest Common Superstring (OpenAI Math Release, September 24, 2026), claims a deterministic polynomial-time algorithm with ratio $2$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A string is a finite list of symbols; a string $s$ is a substring of $T$ if $T=usv$ for some strings $u,v$ (the empty string is a substring of everything). For a finite list $\mathcal S$ of strings, a common superstring is a string $T$ having every $s\in\mathcal S$ as a substring, and

$$\mathrm{OPT}(\mathcal S)=\min\{|T| : T \text{ is a common superstring of }\mathcal S\},$$

where $|T|$ counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length $N$. An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in $N$.

In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.

Formalization targets

Goal: a polynomial-time 2-approximation (Theorem 1.1)

There is a function $f$ from instances to words, computable in polynomial time in the encoded input length, such that for every instance $\mathcal S$

$$f(\mathcal S)\ \text{is a common superstring of } \mathcal S\qquad\text{and}\qquad |f(\mathcal S)|\le 2\,\mathrm{OPT}(\mathcal S).$$

The goal is published on the platform with status Open.

Significance

The result itself. Factor $2$ has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was $7/3$ (reported in 2026). Theorem 1.1 reaches factor $2$ with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor $2$.

Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.

Difficulty

The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above $2$. Greedy, the natural candidate for factor $2$, is reported to fail. Any factor-$2$ algorithm needs a lower bound on $\mathrm{OPT}$ that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.

Formalization scope

• Instances are List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.
• Coverage is contiguous substring containment (List.IsInfix), not subsequence containment.
• opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.
• Polynomial time uses Mathlib's Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.
• Needed infrastructure: the all-substrings graph and Euler tours, periodicity lemmas (Fine–Wilf), and a verified implementation on Mathlib's TM2 model. Contributions of reusable TM2 programming libraries are welcome.

Selected references

• J. Tarhio and E. Ukkonen, A greedy approximation algorithm for constructing shortest common superstrings, Theor. Comput. Sci. 57 (1988), 131–145. https://doi.org/10.1016/0304-3975(88)90167-3
• A. Blum, T. Jiang, M. Li, J. Tromp and M. Yannakakis, Linear approximation of shortest superstrings, J. ACM 41 (1994), 630–647. https://doi.org/10.1145/179812.179818
• D. Breslauer, T. Jiang and Z. Jiang, Rotations of periodic strings and short superstrings, J. Algorithms 24 (1997), 340–353. https://doi.org/10.1006/jagm.1997.0861
• Z. Sweedyk, A 2.5-approximation algorithm for shortest superstring, SIAM J. Comput. 29 (1999), 954–986. https://doi.org/10.1137/S0097539796324661
• M. Mucha, Lyndon words and short superstrings, SODA 2013, 958–972. https://doi.org/10.1137/1.9781611973105.69
• A. Golovnev, A. S. Kulikov, A. Logunov, I. Mihajlin and M. Nikolaev, Collapsing superstring conjecture, APPROX/RANDOM 2019. https://doi.org/10.4230/LIPIcs.APPROX-RANDOM.2019.26
• M. Englert, N. Matsakis and P. Veselý, Approximation guarantees for shortest superstrings: simpler and better, ISAAC 2023. https://doi.org/10.4230/LIPIcs.ISAAC.2023.29
• N. Chukhin, A. S. Kulikov, I. Mihajlin and A. Smal, A tight cycle-cover inequality for shortest common superstring, ECCC TR26-157, 2026. https://eccc.weizmann.ac.il/report/2026/157/
• H. Shibata, Disproving the greedy superstring conjecture, arXiv:2609.01365, 2026. https://arxiv.org/abs/2609.01365v1
• OpenAI, A Polynomial-Time 2-Approximation for Shortest Common Superstring, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/paper.pdf

Motivation

In metric $k$-median, a finite set $J$ (or $D$) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$, one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

$$\mathrm{cost}(S)=\sum_{j\in J}d(j,S),\qquad d(j,S)=\min_{i\in S}d(j,i),\qquad \mathrm{OPT}_k=\min_{S\subseteq F,\ 1\le|S|\le k}\mathrm{cost}(S).$$

Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. A lower bound has long been known: if $\mathrm P\ne\mathrm{NP}$, no polynomial-time algorithm achieves a factor below $1+2/e\approx1.736$ in this candidate-facility model, by a reduction from Feige's coverage gap. The best polynomial-time algorithms had reached $2+\varepsilon$, leaving a gap between $1.736$ and $2$.

This mission asks for a formal proof that the threshold is exactly $1+2/e$, as stated in an OpenAI preprint dated September 24, 2026 (source): a deterministic polynomial-time $(1+2/e+\varepsilon)$-approximation for every fixed $\varepsilon>0$, and hence, under $\mathrm P\ne\mathrm{NP}$, an infimal approximation factor of exactly $1+2/e$. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 2001–2002 — Jain and Vazirani connect $k$-median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
• 2004 — Arya et al. show that bounded-swap local search achieves $3+\varepsilon$ (SICOMP 2004).
• 2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor-$3$ barrier (SICOMP 2016).
• 2017–2023 — Bi-point rounding: $2.675+\varepsilon$ (Byrka et al., TALG 2017) and $2.613$ (Gowda et al., SODA 2023).
• 2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT $(1+2/e+\varepsilon)$-approximation in time $k^{O(k)}\mathrm{poly}$ (ICALP 2019).
• 2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach $2+\varepsilon$ (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with $2+\varepsilon$ (arXiv:2604.06046).
• September 2026 — Two OpenAI preprints claim a deterministic $(1+2/e+\varepsilon)$-approximation, matching the known hardness threshold (source), and an independent randomized $(2-\sigma)$-approximation via anchor recovery and bounded-price strictness (source).
• Hardness — Feige proves the $\ln n$ threshold for set cover and the perfect-completeness Max-$k$-Coverage gap (J. ACM 1998, Theorem 5.3); Anand and Lee record the resulting $1+2/e$ lower bound for $k$-median with specified facilities under $\mathrm P\ne\mathrm{NP}$ (IPCO 2024).

Setting

An instance consists of $n$ points with a rational distance table $d$ that is a metric (nonnegative, zero exactly on the diagonal, symmetric, triangle inequality), a client set $J$, a facility set $F$ (index sets that may overlap), and an integer $1\le k\le|F|$, encoded in binary. A feasible solution is a nonempty $S\subseteq F$ with $|S|\le k$. An algorithm is an $\alpha$-approximation if it always outputs a feasible $S$ with $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$, and it is polynomial-time if it runs on a deterministic multi-stack Turing machine with finite alphabets in time polynomial in the encoding length.

Formalization targets

Milestone: Theorem 1.1 (p. 1)

For every fixed $\varepsilon>0$ there is a deterministic polynomial-time algorithm which, on every instance, returns a feasible $S$ with

$$\sum_{j\in J}d(j,S)\le\Bigl(1+\frac2e+\varepsilon\Bigr)\mathrm{OPT}_k .$$

Goal: Corollary 1.2 (p. 2)

If $\mathrm P\ne\mathrm{NP}$, then

$$\inf\{\alpha:\ \text{a deterministic polynomial-time }\alpha\text{-approximation exists}\}=1+\frac2e .$$

The infimum is not asserted to be attained.

Significance

The result itself. It closes the approximability of metric $k$-median with specified candidate facilities up to arbitrarily small additive error in the factor, ending a sequence of improvements from LP rounding through local search ($3+\varepsilon$), bi-point rounding ($2.675$, $2.613$) to $2+\varepsilon$. It shows that the FPT factor $1+2/e$ of Cohen-Addad et al. is achievable in polynomial time. The case $F=J$ has a different and still separate lower-bound question.

Formalizing it. The goal combines an algorithmic theorem with a hardness reduction. A formal proof needs: the Li–Svensson reduction from constant-additive pseudo-approximations (Theorem 2.2, p. 4); the grid preparation and iterative rounding with a finite directed comparison inequality whose scalar estimates are proved by rational polynomial certificates (Sections 3–5, Appendix A); derandomization by moment-matching distributions of polynomial size (Section 6); and, for the lower bound, NP-hardness of Feige's coverage gap in the Lean computation model. All are reusable for other clustering and covering problems.

Difficulty

Two obstacles meet. The cardinality budget is hard: allowing a constant number of extra facilities makes good connection cost much easier, and earlier rounding analyses in the iterative graph framework only certify factors at least $2$ (p. 2). The preprint's new ingredient is a potential that keeps track of surviving assignment copies after an opening and a finite directed comparison inequality (Theorem 4.1, p. 13) that pays for erasures. Then the randomized rounding must be made deterministic and polynomial-time while keeping the analysis valid, which requires preserving exactly the low-order moments the analysis uses (Lemma 6.1, p. 28; Theorem 6.2, p. 33), before Li–Svensson removes the additive surplus. The hardness side is classical but rests on the PCP-based Max-$k$-Coverage gap.

Formalization scope

• Instance carries n, a Fin n → Fin n → ℚ metric (distance_eq_zero is an iff, so a true metric), client and facility Finsets, and 1 ≤ k ≤ facilities.card. cost sums nearest distances over clients; optimum is the minimum over nonempty facility subsets of size $\le k$.
• Outputs are membership bit masks of an actual feasible set; FactorCorrect α I out requires that mask to describe a nonempty $S\subseteq F$ with $|S|\le k$ and $\mathrm{cost}(S)\le\alpha\,\mathrm{OPT}_k$.
• Polynomial time is Turing.TM2ComputableInPolyTime with finite tape alphabets, on the fixed binary instance encoding.
• approximationFactors is the set of $\alpha$ admitting such an algorithm, and the goal is sInf approximationFactors = 1 + 2/Real.exp 1 under the hypothesis Complexity.PNeNP, where P and NP are defined in the same machine model (NP via polynomial-length witnesses and a finite-alphabet polynomial-time verifier). The set is nonempty by the milestone and bounded below, so sInf is meaningful.
• The hypothesis $\mathrm P\ne\mathrm{NP}$ is not provable, so the goal is a conditional statement; deriving the lower bound requires a Cook–Levin-type NP-hardness of the coverage gap in this model.

Selected references

• OpenAI, The approximation threshold for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf
• OpenAI, Single-exponential recovery and bounded-price strictness for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf
• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45 (1998). https://doi.org/10.1145/285055.285059
• A. Anand, E. Lee, Separating k-median from the supplier version, IPCO 2024. https://doi.org/10.1007/978-3-031-59835-7_2
• K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
• M. Charikar, S. Li, A dependent LP-rounding approach for the k-median problem, ICALP 2012. https://doi.org/10.1007/978-3-642-31594-7_17
• R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, J. ACM 53 (2006). https://doi.org/10.1145/1147954.1147956
• K. N. Gowda, T. Pensyl, A. Srinivasan, K. Trinh, Improved bi-point rounding algorithms and a golden barrier for k-median, SODA 2023. https://doi.org/10.1137/1.9781611977554.ch38
• K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
• M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
• S. Li, O. Svensson, Approximating k-median via pseudo-approximation, SIAM J. Comput. 45 (2016). https://doi.org/10.1137/130938645
• J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
• V. Cohen-Addad, A. Gupta, A. Kumar, E. Lee, J. Li, Tight FPT approximations for k-median and k-means, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.42
• V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2

Motivation

In metric $k$-median, a finite set $J$ (or $D$) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$, one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

$$\mathrm{cost}(S)=\sum_{j\in J}d(j,S),\qquad d(j,S)=\min_{i\in S}d(j,i),\qquad \mathrm{OPT}_k=\min_{S\subseteq F,\ 1\le|S|\le k}\mathrm{cost}(S).$$

Candidate facilities are part of the input and need not coincide with the clients. It is one of the basic clustering and facility-location objectives, and its approximability has been a testing ground for LP rounding, primal-dual methods and local search. The hard part of the problem is the facility budget: a solution with small connection cost is much easier to find if a few extra facilities may be opened, and every approximation algorithm must eventually enforce $|S|\le k$ on its output.

This mission concerns two tools for enforcing that budget and their combination into a randomized approximation strictly below factor $2$ on arbitrary finite rational metrics, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 2001–2002 — Jain and Vazirani connect $k$-median to facility location by Lagrangian relaxation and primal-dual methods (J. ACM 2001); Charikar, Guha, Tardos and Shmoys give the first constant-factor approximation by LP rounding (JCSS 2002); Jain, Mahdian and Saberi introduce greedy dual fitting (STOC 2002; J. ACM 2003).
• 2004 — Arya et al. show that bounded-swap local search achieves $3+\varepsilon$ (SICOMP 2004).
• 2016 — Li and Svensson show that constant-additive pseudo-approximations can be converted to true approximations at arbitrarily small loss, breaking the factor-$3$ barrier (SICOMP 2016).
• 2017–2023 — Bi-point rounding: $2.675+\varepsilon$ (Byrka et al., TALG 2017) and $2.613$ (Gowda et al., SODA 2023).
• 2019 — Cohen-Addad, Gupta, Kumar, Lee and Li give a tight FPT $(1+2/e+\varepsilon)$-approximation in time $k^{O(k)}\mathrm{poly}$ (ICALP 2019).
• 2025–2026 — Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson reach $2+\varepsilon$ (arXiv:2503.10972); Byrka et al. develop iterative randomized rounding with $2+\varepsilon$ (arXiv:2604.06046).
• September 2026 — Two OpenAI preprints claim a deterministic $(1+2/e+\varepsilon)$-approximation, matching the known hardness threshold (source), and an independent randomized $(2-\sigma)$-approximation via anchor recovery and bounded-price strictness (source).

Setting

Write $n=|D|$ and $N=|D|+|F|$. A comparison solution $O\subseteq F$ of size $h$ assigns each client to a nearest member of $O$ (ties broken by fixed priorities); $C_i$ is the cluster of $i\in O$ and $P_i=\sum_{p\in C_i}d(p,i)$, with $P=\mathrm{cost}(O)$. An anchor is a supplied feasible $S\subseteq F$ with $|S|=h$. A certificate partitions $O$ into good and bad centres and gives distinct proxies $\varphi_i\in S$ for the good centres. A randomized polynomial-time algorithm is a polynomial-time multi-stack Turing machine that reads the encoded instance together with a string of fair random bits whose length is a fixed polynomial in the input length.

Formalization targets

Milestone: refined recovery (Theorem 1.1, p. 2)

Let $D,F$ be disjoint, with distances between distinct indices positive integers bounded by a fixed polynomial in $N$. Fix $\varepsilon>0$, $0<L_0<\infty$ and a rational $0<\mu\le\min\{1/4,\varepsilon/12\}$. There is a randomized algorithm that, given an anchor $S$ with $|S|=h\ge1$ and a failure parameter $\zeta\in(0,1)$, always returns $\hat S\subseteq F$ with $|\hat S|\le h$, runs in time polynomial in $N$ and $\log(1/\zeta)$, and, whenever some comparison solution $O$ of size $h$ and cost $P>0$ admits a certificate with

$$\sum_{i\ \mathrm{good}}\sum_{p\in C_i}d(p,\varphi_i)\le \sum_{i\ \mathrm{good}}P_i+\mu P,\qquad \#\{i\ \mathrm{bad}\}\le L_0\log N,$$

satisfies $\mathrm{cost}(\hat S)\le(1+2/e+\varepsilon)P$ with probability at least $1-\zeta$. The algorithm is not given $O$, $P$ or the certificate.

Goal: global application (Theorem 1.2, p. 3)

There is an absolute constant $\sigma>0$ such that for every fixed $a>0$ some randomized polynomial-time algorithm for metric $k$-median always returns a feasible $S$ (nonempty, $S\subseteq F$, $|S|\le k$) and satisfies

$$\Pr\bigl[\mathrm{cost}(S)\le(2-\sigma)\,\mathrm{OPT}_k\bigr]\ \ge\ 1-(|D|+|F|+2)^{-a},\qquad \mathbb E\,\mathrm{cost}(S)\le(2-\sigma)\,\mathrm{OPT}_k .$$

Significance

The result itself. Theorem 1.1 makes the running time single-exponential in the number of clusters without accurate proxies, so logarithmically many exceptions are tractable; FPT methods with $k^{O(k)}$ dependence do not give this by setting $k=O(\log N)$. Combined with a new proof of bounded-price strictness for one compatible execution of the logarithmic-surplus construction of Cohen-Addad, Grandoni, Lee, Schwiegelshohn and Svensson (Lemma 8.1, p. 43), it yields Theorem 1.2: a randomized approximation strictly below $2$, both with high probability and in expectation, that opens at most $k$ facilities on every output. A companion preprint proves a stronger deterministic $(1+2/e+\varepsilon)$ bound by an independent route; Theorem 1.2's interest is the way recovery and payment accounting together enforce the budget.

Formalizing it. The statements are fully explicit about the machine model, the random bits, and the input encoding. A formal proof would need local-search anchoring (Theorem 3.3), leader/ball sampling with amortized radius guesses (Section 4), a finite categorical continuous-greedy algorithm with explicit error (Lemma 5.1, p. 21), the surplus construction as an external interface (Theorem 7.1, p. 35), and metric rounding and transfer (Lemma 2.1, p. 6). The submodular-optimization and local-search components are reusable.

Difficulty

Every factor-$2$ dual-fitting argument charges $\lambda+2P_C$ to a client set $C$ served by a comparison facility, which gives exactly $2$; improving the constant requires saving on connection cost while still paying for all $h$ regular openings with one final price, one set of copy lengths and the budgets of one actual replay of the construction (Section 1.2, p. 3). On the recovery side, guessing a good solution from an anchor naively costs $k^{O(k)}$; keeping the dependence single-exponential in the number of bad clusters requires interleaving leader sampling and removals and amortizing radius guesses over disjoint client sets (Section 4). Theorem 1.1 holds only for normalized integral metrics; the global application must construct its anchors after normalization and transfer the final cost bound back (Lemma 2.1, p. 6).

Formalization scope

• RationalMetricInput: points Fin pointCount, a rational pseudometric table (zero on the diagonal, symmetric, triangle inequality), client and facility Finsets covering all points (they may overlap, so clients and facilities may share locations), a nonempty facility set and a positive budget $k$. Feasible S is $S\subseteq F$, $|S|\le k$, and $S$ nonempty when there are clients; optimum minimizes over nonempty subsets of size $\le k$.
• A BinaryRandomizedAlgorithm is a TM2ComputableInPolyTime function of (input bits, random bits) with finite alphabets, using randomBits.eval (input length) fair bits; probabilities and expectations are uniform averages over all seeds.
• In the goal, feasibility holds for every seed; the success bound is $1-(N+2)^{-a}$ with $N=|D|+|F|$ (Real.rpow); the same algorithm must also satisfy the expectation bound.
• In the milestone, Input adds disjointness of $D$ and $F$, integral distances, positivity between distinct indices, and an anchor with anchor.card = budget; Bounded bound caps distances by a fixed polynomial in $N$; ζ is passed in unary precision $\lceil\log_2(1/\zeta)\rceil$, and PolynomialWork bounds work by $c(N+1)^d(1+\log(1/\zeta))^d$. A Certificate encodes $O$ with $|O|=h$, $P>0$, the good set, injective proxies into the anchor, the proxy-cost promise with lexicographic tie-breaking, and at most $L_0\log N$ bad centres.

Selected references

• OpenAI, Single-exponential recovery and bounded-price strictness for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Single-Exponential-Recovery-and-Bounded-Price-Strictness-for-Metric-k-Median-September-24-2026/paper.pdf
• OpenAI, The approximation threshold for metric k-median, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Approximation-Threshold-for-Metric-k-Median-September-24-2026/main.pdf
• V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, Breaching the 2 LMP approximation barrier for facility location with applications to k-median, arXiv:2207.05150 (2026 version). https://arxiv.org/abs/2207.05150v2
• V. Cohen-Addad, C. Schwiegelshohn, On the local structure of stable clustering instances, FOCS 2017. https://doi.org/10.1109/FOCS.2017.14
• G. Călinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput. 40 (2011). https://doi.org/10.1137/080733991
• J. Vondrák, Optimal approximation for the submodular welfare problem in the value oracle model, STOC 2008. https://doi.org/10.1145/1374376.1374389
• K. Jain, M. Mahdian, E. Markakis, A. Saberi, V. V. Vazirani, Greedy facility location algorithms analyzed using dual fitting with factor-revealing LP, J. ACM 50 (2003). https://doi.org/10.1145/950620.950621
• K. Jain, V. V. Vazirani, Approximation algorithms for metric facility location and k-median problems using the primal-dual schema and Lagrangian relaxation, J. ACM 48 (2001). https://doi.org/10.1145/375827.375845
• M. Charikar, S. Guha, É. Tardos, D. B. Shmoys, A constant-factor approximation algorithm for the k-median problem, JCSS 65 (2002). https://doi.org/10.1006/jcss.2002.1882
• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local search heuristics for k-median and facility location problems, SIAM J. Comput. 33 (2004). https://doi.org/10.1137/S0097539702416402
• S. Li, O. Svensson, Approximating k-median via pseudo-approximation, SIAM J. Comput. 45 (2016). https://doi.org/10.1137/130938645
• J. Byrka, T. Pensyl, B. Rybicki, A. Srinivasan, K. Trinh, An improved approximation for k-median and positive correlation in budgeted optimization, ACM TALG 13 (2017). https://doi.org/10.1145/2981561
• V. Cohen-Addad, A. Gupta, A. Kumar, E. Lee, J. Li, Tight FPT approximations for k-median and k-means, ICALP 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.42
• V. Cohen-Addad, F. Grandoni, E. Lee, C. Schwiegelshohn, O. Svensson, A (2+ε)-approximation algorithm for metric k-median, arXiv:2503.10972 (2026 version). https://arxiv.org/abs/2503.10972v2

Motivation

A set of unit-length jobs with precedence constraints is to be run on a fixed number of identical machines so that all jobs finish as early as possible. For two machines this was solved in 1969–1972; for a number of machines given as part of the input the problem is NP-complete (Ullman, 1975). Whether the problem is polynomial-time solvable for three machines, written $P3\mid\mathrm{prec},p_j=1\mid C_{\max}$, is problem OPEN8 in the appendix of Garey and Johnson's 1979 book and is one of the best-known open questions on the complexity of scheduling.

Timeline

• 1969–1971. Fujii, Kasami and Ninomiya solve the two-processor case by matching (doi:10.1137/0117070, erratum doi:10.1137/0120018).
• 1972. Coffman and Graham give an optimal list-scheduling algorithm for two processors (doi:10.1007/BF00288685).
• 1975. Ullman proves NP-completeness when the number of machines is part of the input (doi:10.1016/S0022-0000(75)80008-0).
• 1979. Garey and Johnson list the fixed-three-machine problem as OPEN8; Graham, Lawler, Lenstra and Rinnooy Kan introduce the standard notation (doi:10.1016/S0167-5060(08)70356-X).
• 1983. Garey, Johnson, Tarjan and Yannakakis give a linear-time algorithm on three processors for opposing forests (doi:10.1137/0604011).
• 1984. Dolev and Warmuth give an $O(n^{h(m-1)+1})$ algorithm for precedence graphs of height $h$ (doi:10.1016/0196-6774(84)90039-7).
• 2016–2022. Approximation schemes for fixed machine counts: Levey and Rothvoß via LP hierarchies (doi:10.1145/2897518.2897532), Garg's quasi-PTAS (doi:10.4230/LIPIcs.ICALP.2018.59), Li (doi:10.1137/1.9781611976465.178), Das and Wiese (doi:10.4230/LIPIcs.ESA.2022.40).
• 2025. Nederlof, Swennenhuis and Węgrzycki give an exact algorithm in time $2^{O(\sqrt n\log n)}$ for three machines (doi:10.1137/1.9781611978322.16).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims a deterministic polynomial-time algorithm.

Setting

The input is a directed acyclic graph $G=(V,E)$ on $V=\{1,\dots,n\}$, $n\ge1$, given as an explicit list of arcs, and optionally an integer deadline $T$ with $1\le T\le n$. A feasible schedule with makespan at most $T$ is a map

$$\tau:V\to\{1,\dots,T\}$$

such that each value is taken at most three times (three machines) and $\tau(u)<\tau(v)$ for every arc $(u,v)\in E$ (precedence). Slot $t$ means execution during $[t-1,t)$. There are no release dates, communication delays or other resources. The input length $L$ is the length of the binary encoding of the graph and deadline.

Formalization targets

Goal: Theorem 1.1

There is a single deterministic multitape Turing machine $M$ and a constant $C$ such that, on every such input of length $L$, $M$ halts within

$$C\,(L+2)^{150020}$$

steps and

• without a deadline, outputs a feasible schedule of minimum makespan;
• with a deadline $T$, outputs "infeasible" exactly when no feasible schedule with makespan at most $T$ exists, and otherwise outputs one.

The exponent is the one stated in the paper and is not optimized; the content of the theorem is that a fixed polynomial bound exists. The Lean statement OAI.ThreeMachine.main_theorem is open on the platform.

Significance

The theorem resolves the polynomial-time side of Garey and Johnson's OPEN8: unit-job makespan scheduling with arbitrary precedence constraints on three identical machines lies in P. Previous exact algorithms were either restricted to special precedence structures (forests, bounded height) or subexponential, and approximation schemes did not decide the optimum. The structural statement behind the algorithm, that feasible schedules admit recursive decompositions whose interval job sets have descriptions of bounded size, may be of independent use for other fixed-machine scheduling problems. No practical running time is claimed.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formal proof would also certify the running-time analysis in an explicit machine model, which is rarely done for algorithmic results of this size.

Difficulty

Removing selected slots from a feasible schedule leaves gaps that can be rescheduled independently, which suggests a recursive search over the job sets of gaps. The obstacle is their number: naming a gap by its two boundary triples does not determine its job set, and intersecting descriptions inherited from ancestors can make the descriptions grow without bound along a recursion of linear depth. The subexponential decomposition of Nederlof–Swennenhuis–Węgrzycki controls the number of subproblems only up to $2^{O(\sqrt n\log n)}$; a polynomial bound needs every subproblem to have a global description of constant size.

Formalization scope

• Instance n is a list of arcs on Fin n; acyclic forbids a Relation.TransGen cycle. Jobs are Fin n (shifted to $1,\dots,n$ in the encoding).
• Feasible G T τ: slots in $[1,T]$, at most three jobs per slot, strict precedence.
• CorrectOutput distinguishes the optimization mode (none) and the decision mode (some T).
• The machine model is a custom multitape Turing machine Machine k q g over Fin (g+3) with $k+1$ tapes; input on tape 0 encoded by encodeInput (self-delimiting binary numbers), output read from tape 0 after halting. The time bound is $C\,(L+2)^{150020}$ with $L$ the encoded length.
• The quantifiers are ordered so that the machine and constant are fixed before the instance (uniformity).

A complete development needs the combinatorics of the decomposition (separators and bounded global descriptions), a dynamic program over polynomially many descriptions, and its implementation and time analysis on the given Turing machine model. Contributions formalizing the purely combinatorial structure theorem, independently of the machine model, are welcome.

Selected references

• OpenAI, A Polynomial-Time Algorithm for Three-Machine Unit-Job Scheduling, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-algorithm-for-three-machine-unit-job-scheduling-September-24-2026/paper.pdf
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• E. G. Coffman Jr., R. L. Graham, Optimal scheduling for two-processor systems, Acta Inform., 1972. https://doi.org/10.1007/BF00288685
• J. D. Ullman, NP-complete scheduling problems, J. Comput. System Sci., 1975. https://doi.org/10.1016/S0022-0000(75)80008-0
• D. Dolev, M. K. Warmuth, Scheduling precedence graphs of bounded height, J. Algorithms, 1984. https://doi.org/10.1016/0196-6774(84)90039-7
• J. Nederlof, C. M. F. Swennenhuis, K. Węgrzycki, A subexponential time algorithm for makespan scheduling of unit jobs with precedence constraints, SODA 2025. https://doi.org/10.1137/1.9781611978322.16
• E. Levey, T. Rothvoß, A $(1+\epsilon)$-approximation for makespan scheduling with precedence constraints using LP hierarchies, STOC 2016. https://doi.org/10.1145/2897518.2897532

Motivation: how many deletion traces does it take to recover a word?

In the trace reconstruction problem an unknown binary word $x\in\{0,1\}^n$ is passed repeatedly through a deletion channel: each bit is deleted independently with known probability $q\in(0,1)$ and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many independent traces are needed to recover every word $x$ exactly with a fixed success probability. The problem arises in DNA storage and sequencing, in multiple sequence alignment, and as a basic test of how much information a channel with synchronization errors destroys. Its central open question has been whether a polynomial number of traces suffices at a fixed deletion probability.

Timeline

• 2001 — Levenshtein studies efficient reconstruction of sequences from corrupted copies, in combinatorial and memoryless-channel versions (IEEE Trans. Inf. Theory 2001).
• 2004 — Batu, Kannan, Khanna and McGregor introduce the independent-deletion trace problem in connection with multiple sequence alignment and outline a linear lower bound at fixed deletion probability (SODA 2004).
• 2008 — Holenstein, Mitzenmacher, Panigrahy and Wieder give the first worst-case upper bound $\exp(\widetilde O(\sqrt n))$ at constant deletion probability (SODA 2008).
• 2014 — McGregor, Price and Vorotnikova analyze lower bounds via a single displaced one among zeros (ESA 2014).
• 2017 — De, O'Donnell and Servedio (STOC 2017) and, independently, Nazarov and Peres (STOC 2017) improve the upper bound to $\exp(O(n^{1/3}))$.
• 2020 — Holden and Lyons prove the lower bound $\Omega(n^{5/4}/\sqrt{\log n})$ (Ann. Appl. Probab. 2020; erratum 2022).
• 2021 — Chase improves the lower bound to $\Omega(n^{3/2}/\log^7 n)$ (Ann. Inst. Henri Poincaré Probab. Stat. 2021) and the upper bound to $\exp(O(n^{1/5}\log^5 n))$ (STOC 2021).
• 2026 — Burudgunte, Valiant and Wang give a quasipolynomial sample upper bound $\exp(p^{-7/3}(\log_2 n)^{C_0})$ with $p=1-q$ (arXiv:2607.04073).
• 2026 — An OpenAI preprint, Quantitative lower bounds for trace reconstruction (OpenAI Math Release, September 24, 2026), claims that $n^{\Omega(\log\log n)}$ traces are necessary at every fixed $q$, answering the polynomial-sample question negatively. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

Fix $n$ and $q\in(0,1)$. A deletion mask $a\in\{0,1\}^n$ keeps bit $i$ when $a_i=1$; it has probability $\prod_i (1-q)^{a_i} q^{1-a_i}$. The trace of $x$ under $a$ is the list of the bits $x_i$ with $a_i=1$, in order. Write $\mathcal D_q(x)$ for the law of the trace of $x$ under a random mask.

An estimator with budget $m$ receives $m$ independent traces of $x$ and returns a random word; it may be randomized and its computation is unrestricted. For $s\in(0,1]$, the sample complexity $T_{q,s}(n)$ is the least $m$ such that some estimator recovers every $x\in\{0,1\}^n$ with probability at least $s$; it is $+\infty$ if no finite $m$ works. The one-trace distance is

$$\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=\tfrac12\sum_{w}\bigl|\mathcal D_q(x)(w)-\mathcal D_q(y)(w)\bigr|,$$

the sum running over all finite binary words.

In Lean (namespace OAI.TraceReconstruction), words are Fin n → Bool, traceMass q x w is the probability of output w, an estimator is a function A : (Fin m → Trace) → Word n → ℝ giving a probability vector for each sample, sampleComplexity n q s : ℝ≥0∞ is the infimum of sufficient budgets, and minTraceTV n q is the minimum of traceTV q x y over $x\neq y$.

Formalization targets

Goal: quantitative sample lower bound (Theorem 1.1)

Fix $s\in(0,1]$ and $0<c<1/(4\log 2)$. For every sequence of instances $(n_k,q_k)$ with $n_k\to\infty$, $q_k\in(0,1)$ and $q_k^3\log n_k\to\infty$,

$$T_{q_k,s}(n_k)\;\ge\; n_k^{\,c\log(q_k^3\log n_k)}\qquad\text{for all sufficiently large }k.$$

At fixed $q$ this gives $T_{q,s}(n)\ge n^{\Omega(\log\log n)}$, so no polynomial number of traces suffices. The goal is published on the platform with status Open.

Milestones: superpolynomial indistinguishability (Theorem 1.2)

For every fixed $q\in(0,1)$ and every $A>0$,

$$\lim_{n\to\infty} n^{A}\min_{x\neq y\in\{0,1\}^n}\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=0, \qquad \lim_{n\to\infty}\frac{T_{q,s}(n)}{n^{A}}=\infty\quad (s\in(0,1]).$$

Significance

The result itself. Theorem 1.1 is the first superpolynomial lower bound for exact worst-case trace reconstruction at a fixed deletion probability; previous lower bounds were of order $n^{3/2}$ up to logarithms. It holds against unrestricted computation and any fixed positive success probability, and it settles in the negative the question of whether polynomially many traces suffice. Combined with the 2026 quasipolynomial upper bound of Burudgunte, Valiant and Wang, the sample complexity at fixed $q$ is now known to lie between $\exp(\Theta(\log n\log\log n))$ and $\exp((\log n)^{O(1)})$. Theorem 1.2 isolates the underlying phenomenon: some pairs of distinct words have single-trace laws closer than every inverse polynomial.

Formalizing it. The definitions fix exactly what an estimator may see (only the complete traces, no positions or boundaries) and what "sample complexity" means, including the value $+\infty$. A formal proof would certify a lower bound whose argument is a long multi-scale construction with many quantitative error budgets, the kind of argument where an overlooked loss would invalidate the conclusion.

Difficulty

Earlier lower bounds compare two words that differ by a single local defect and compute their trace distance directly; such pairs are distinguishable from polynomially many traces, so no single-defect construction can give a superpolynomial bound. A superpolynomial bound needs pairs of words whose trace laws agree to every polynomial order, while the argument must remain uniform in the deletion probability (which may tend to $0$ slowly), keep all constants below scale margins that shrink as the number of construction stages grows with $n$, and transfer a bound for one trace to a bound for $m$ independent traces and for arbitrary randomized estimators.

Formalization scope

• Traces are List Bool; traceTV sums over the finite set of all lists of length at most $n$, which contains the support of every trace law, so it agrees with the source's total variation over all finite words.
• sampleComplexity is an sInf in ℝ≥0∞; the infimum of the empty set is $\top$, matching $T_{q,s}(n)=+\infty$. The lower bound is compared after ENNReal.ofReal, and the right-hand side $n^{c\log(q^3\log n)}$ uses the real power.
• Theorem 1.1 is encoded with sequences n q : ℕ → …, Tendsto n atTop atTop, and Tendsto (q k ^ 3 * log (n k)) atTop atTop; the conclusion is ∀ᶠ k in atTop. Logarithms are natural.
• Estimators are arbitrary real-valued probability kernels from samples to words; success is the exact probability of returning the true word, required to be at least $s$ for every input.
• minTraceTV n q is a real sInf, attained for $n\ge1$; at $n=0$ the set is empty and the junk value $0$ does not affect the limit.
• Needed infrastructure: the deletion channel and its trace law, total variation and Hellinger distance for finite laws and their tensorization, and the reduction from sample complexity to pairwise distinguishability. These are reusable for other deletion-channel problems.

Selected references

• V. I. Levenshtein, Efficient reconstruction of sequences, IEEE Trans. Inform. Theory, 2001. https://doi.org/10.1109/18.904499
• T. Batu, S. Kannan, S. Khanna and A. McGregor, Reconstructing strings from random traces, SODA 2004. https://people.cs.umass.edu/~mcgregor/papers/04-soda.pdf
• T. Holenstein, M. Mitzenmacher, R. Panigrahy and U. Wieder, Trace reconstruction with constant deletion probability and related results, SODA 2008. https://www.eecs.harvard.edu/~michaelm/postscripts/soda2008c.pdf
• A. McGregor, E. Price and S. Vorotnikova, Trace reconstruction revisited, ESA 2014. https://doi.org/10.1007/978-3-662-44777-2_57
• A. De, R. O'Donnell and R. A. Servedio, Optimal mean-based algorithms for trace reconstruction, STOC 2017. https://doi.org/10.1145/3055399.3055450
• F. Nazarov and Y. Peres, Trace reconstruction with $\exp(O(n^{1/3}))$ samples, STOC 2017. https://doi.org/10.1145/3055399.3055494
• N. Holden and R. Lyons, Lower bounds for trace reconstruction, Ann. Appl. Probab., 2020. https://doi.org/10.1214/19-AAP1506
• Z. Chase, New lower bounds for trace reconstruction, Ann. Inst. Henri Poincaré Probab. Stat. 57 (2021), 627–643. https://doi.org/10.1214/20-AIHP1089
• Z. Chase, Separating words and trace reconstruction, STOC 2021. https://doi.org/10.1145/3406325.3451118
• A. Burudgunte, P. Valiant and H. Wang, Quasipolynomial trace reconstruction, preprint, 2026. https://arxiv.org/abs/2607.04073
• OpenAI, Quantitative lower bounds for trace reconstruction, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1; Theorem 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quantitative-lower-bounds-for-trace-reconstruction-September-24-2026/paper.pdf

Motivation

Sparsest cut asks for a partition of a weighted graph whose crossing capacity is small compared with the demand it separates. It is a basic graph-partitioning primitive (used for divide-and-conquer algorithms, clustering and expansion testing), and its relaxations are the main bridge between approximation algorithms and the geometry of finite metric spaces. In the uniform version every pair of vertices has demand one. The best known polynomial-time approximation, due to Arora, Rao and Vazirani, uses the Goemans–Linial semidefinite relaxation and achieves ratio $O(\sqrt{\log n})$. How good this relaxation can be, i.e. its integrality gap on uniform instances, has been a long-standing question.

Timeline

• 1995. Linial, London and Rabinovich develop the metric approach to cuts: $\ell_1$ metrics are combinations of cut metrics, so embeddings into $\ell_1$ round to cuts (doi:10.1007/BF01200757).
• 1997 and 2002. Goemans and Linial propose the semidefinite relaxation with triangle inequalities and the conjecture that negative-type metrics embed into $\ell_1$ with constant distortion (doi:10.1007/BF02614315).
• 2003 and 2008. Rabinovich relates uniform sparsest cut to average distortion of embeddings into the line and into $L_1$ (doi:10.1145/780542.780609, doi:10.1007/s00454-007-9047-5).
• 2004/2009. Arora, Rao and Vazirani prove the $O(\sqrt{\log n})$ upper bound for uniform demands (doi:10.1145/1502793.1502794).
• 2005/2015. Khot and Vishnoi disprove the Goemans–Linial conjecture for general demands (doi:10.1145/2629614).
• 2006. Devanur, Khot, Saket and Vishnoi give an $\Omega(\log\log n)$ uniform integrality gap (doi:10.1145/1132516.1132594). Lee and Naor propose the Heisenberg-group approach for general demands (doi:10.1109/FOCS.2006.47).
• 2009–2011. Cheeger, Kleiner and Naor prove a $(\log n)^{\Omega(1)}$ general-demand gap (arXiv:0910.2024) and note that their examples cannot give a diverging uniform gap.
• 2013. Kane and Meka improve the uniform gap to $\exp(\Omega(\sqrt{\log\log n}))$ (doi:10.1145/2488608.2488610).
• 2018 and 2025. Naor and Young obtain the sharp general-demand lower bound $\Omega(\sqrt{\log n})$ (doi:10.4007/annals.2018.188.1.4); Chang, Naor and Ren prove the matching upper bound (doi:10.1145/3717823.3718285).

For uniform demands the gap between the lower bound $\exp(\Omega(\sqrt{\log\log n}))$ and the upper bound $O(\sqrt{\log n})$ remained. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a lower bound matching the upper bound up to a power of $\log\log n$.

Setting

Let $C=(c_{ij})$ be symmetric nonnegative capacities on pairs of distinct vertices of $[n]$. The uniform sparsest-cut value is

$$\mathrm{OPT}(C)=\min_{\varnothing\ne B\subsetneq[n]}\frac{\sum_{i\in B,\,j\notin B}c_{ij}}{|B|\,(n-|B|)}.$$

A negative-type semimetric is $d(i,j)=\|x_i-x_j\|^2$ for vectors $x_i$ in a real Hilbert space, satisfying all triangle inequalities $d(i,k)\le d(i,j)+d(j,k)$; distinct points may have distance zero. The Goemans–Linial value is

$$\mathrm{GL}(C)=\min\Bigl\{\sum_{i<j}c_{ij}\,d(i,j)\ :\ \sum_{i<j}d(i,j)=1,\ d\ \text{negative type}\Bigr\}.$$

Normalized cut metrics are feasible, so $\mathrm{GL}(C)\le\mathrm{OPT}(C)$. The integrality gap of $C$ is $\mathrm{OPT}(C)/\mathrm{GL}(C)$.

Formalization targets

Goal: Theorem 1.1

There are an absolute $c>0$ and instances $C^{(j)}$ on $n_j\to\infty$ vertices with $\mathrm{GL}(C^{(j)})>0$ such that, for all large $j$,

$$\frac{\mathrm{OPT}(C^{(j)})}{\mathrm{GL}(C^{(j)})}\ \ge\ c\,\frac{\sqrt{\log n_j}}{(\log\log n_j)^3}.$$

The Lean statement OAI.UniformSparsestCut.mainGap is open on the platform.

Significance

The bound reaches the exponent $1/2$ in $\log n$, so the Arora–Rao–Vazirani analysis of the Goemans–Linial SDP is tight for uniform demands up to the factor $(\log\log n)^3$. It strengthens the Devanur–Khot–Saket–Vishnoi and Kane–Meka refutations of the uniform constant-gap conjecture. Geometrically, it gives a finite negative-type metric for which every $1$-Lipschitz map into $\ell_1$ preserves only a $(\log\log n)^3/\sqrt{\log n}$ fraction of the average distance. The theorem concerns the basic Goemans–Linial SDP only, not strengthened hierarchies.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.

Difficulty

The sharp general-demand lower bounds (Heisenberg group, Naor–Young) control worst-pair distortion, and Cheeger–Kleiner–Naor note that those examples have constant average distortion into a line, so they cannot give a diverging uniform gap. A uniform-demand example must force every $\ell_1$ contraction to lose most of the average distance over all pairs, not merely on a few pairs. At the same time the constructed distance must remain of negative type and satisfy all triangle inequalities exactly, and the passage from a probability measure on points to an exactly uniform demand with positive SDP value must be carried out without losing the bound.

Formalization scope

• Capacity n stores cap : Fin n → Fin n → ℝ, nonnegative, symmetric, zero on the diagonal.
• cutRatio C B is the crossing capacity of $B$ divided by $|B|(n-|B|)$; OPT C is the sInf over nonempty proper Finsets $B$.
• NegativeType d requires points x : Fin n → EuclideanSpace ℝ (Fin n) with $d=\|x_i-x_j\|^2$ and all triangle inequalities; Feasible d adds $\sum_{i<j}d(i,j)=1$; glValue C is the sInf of $\sum_{i<j}c_{ij}d(i,j)$ over feasible $d$.
• The goal asks for a sequence $n_j\ge2$, $n_j\to\infty$, with $\mathrm{GL}>0$ for every $j$ (ruling out a gap that is trivial because of division by zero) and the bound eventually.

A complete development needs cut-cone duality, a Hilbert-space kernel construction with rounded charts, Gaussian direction families, and contraction estimates for maps into $\ell_1$. Cut-cone duality and the reduction to exactly uniform demands are reusable. Contributions formalizing Lemma 6.1 (cut-cone duality) or the weak duality $\mathrm{GL}\le\mathrm{OPT}$ are welcome first steps.

Selected references

• OpenAI, Near-square-root logarithmic integrality gaps for uniform sparsest cut, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026.pdf
• S. Arora, S. Rao, U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM, 2009. https://doi.org/10.1145/1502793.1502794
• N. R. Devanur, S. A. Khot, R. Saket, N. K. Vishnoi, Integrality gaps for sparsest cut and minimum linear arrangement problems, STOC 2006. https://doi.org/10.1145/1132516.1132594
• D. M. Kane, R. Meka, A PRG for Lipschitz functions of polynomials with applications to sparsest cut, STOC 2013. https://doi.org/10.1145/2488608.2488610
• S. A. Khot, N. K. Vishnoi, The Unique Games Conjecture, integrality gap for cut problems and embeddability of negative type metrics into $\ell_1$, J. ACM, 2015. https://doi.org/10.1145/2629614
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica, 1995. https://doi.org/10.1007/BF01200757
• Y. Rabinovich, On average distortion of embedding metrics into the line, Discrete Comput. Geom., 2008. https://doi.org/10.1007/s00454-007-9047-5
• J. Cheeger, B. Kleiner, A. Naor, A $(\log n)^{\Omega(1)}$ integrality gap for the Sparsest Cut SDP, FOCS 2009. https://arxiv.org/abs/0910.2024
• A. Naor, R. Young, Vertical perimeter versus horizontal perimeter, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.188.1.4

Motivation

A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any $\varepsilon,\delta\in(0,1)$, returns a $(1\pm\varepsilon)$-approximation with probability at least $1-\delta$ in time polynomial in the input length, $1/\varepsilon$ and $\log(1/\delta)$.

Timeline

• 1986. Jerrum, Valiant and Vazirani relate approximate counting and sampling through self-reducibility.
• 1995. Diaconis and Gangolli survey fixed-margin arrays (doi:10.1007/978-1-4612-0801-3_3).
• 1997. Dyer, Kannan and Mount prove #P-completeness for two-row tables and give geometric methods for large margins; Morris improves the margin requirements in 2002 (doi:10.1002/rsa.10049).
• 2000–2003. Dyer and Greenhill (two rows), Cryan and Dyer (fixed number of rows), Dyer (dynamic programming) give approximate counting for a bounded number of rows.
• 2004. Jerrum, Sinclair and Vigoda's permanent algorithm yields an FPRAS for all 0/1 caps (doi:10.1145/1008731.1008738).
• 2009–2010. Barvinok bounds weighted table counts within $N^{O(m+n)}$ (doi:10.1093/imrn/rnn133); Barvinok, Luria, Samorodnitsky and Yong give quasipolynomial randomized approximations for smooth margins (doi:10.1002/rsa.20301).
• 2010. Cryan, Dyer and Randall give an FPRAS for integral flows with large tight capacities and for cell-bounded tables with a fixed number of rows, and list unrestricted approximation as open (doi:10.1137/060650544).
• 2023. Brändén, Leake and Pak give capacity lower bounds via Lorentzian polynomials (doi:10.1007/s11856-022-2364-9); Guo and Jerrum count vertices of certain 0/1 polytopes (doi:10.1007/s00454-022-00406-8).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.

Setting

For positive integers $m,n$, margins $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with equal totals, and bounds $b\in\mathbb Z_{\ge0}^{m\times n}$,

$$\Omega(r,c,b)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j,\ X_{ij}\le b_{ij}\Bigr\},\qquad Z(r,c,b)=|\Omega(r,c,b)|.$$

All numbers are written in binary, so a capacity can be exponentially larger than its description. $L$ denotes the total binary input length including the rational accuracy parameters $\varepsilon,\delta$. The algorithm uses independent unbiased random bits and is charged for every bit operation.

Formalization targets

Goal: Theorem 1.1 (FPRAS)

One randomized algorithm, given $(r,c,b)$ and rational $\varepsilon,\delta\in(0,1)$, outputs a nonnegative rational $\widehat Z$ with

$$\Pr\bigl[(1-\varepsilon)Z(r,c,b)\le\widehat Z\le(1+\varepsilon)Z(r,c,b)\bigr]\ge1-\delta,$$

outputs exactly $0$ on every execution when $\Omega(r,c,b)=\emptyset$, and performs at most $\mathrm{poly}(L,\varepsilon^{-1},\log\delta^{-1})$ bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.

Significance

The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).
• Inputs are delimited binary encodings of $m,n,r,c,b$ and of $\varepsilon,\delta$ as reduced fractions (encodeCountingInput); outputs are encoded rationals.
• count r c b is Fintype.card of bounded tables.
• CountingStatement: one machine and constants $C>0$, $d$; with $t=C(|\text{input}|+\lceil1/\varepsilon\rceil+\lceil\log_2\lceil1/\delta\rceil\rceil+1)^d$, every tape of length $t$ halts with a rational $q\ge0$; if count = 0 every tape outputs $0$; and the fraction of tapes with $(1-\varepsilon)Z\le q\le(1+\varepsilon)Z$ is at least $1-\delta$.
• $m,n\ge1$ and equal margin totals are hypotheses, as in the paper.

Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.

Selected references

• OpenAI, An FPRAS for Cell-Bounded Contingency Tables, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-FPRAS-for-Cell-Bounded-Contingency-Tables-September-24-2026/main.pdf
• M. Cryan, M. Dyer, D. Randall, Approximately counting integral flows and cell-bounded contingency tables, SIAM J. Comput., 2010. https://doi.org/10.1137/060650544
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM, 2004. https://doi.org/10.1145/1008731.1008738
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• A. Barvinok, Asymptotic estimates for the number of contingency tables, integer flows, and volumes of transportation polytopes, IMRN, 2009. https://doi.org/10.1093/imrn/rnn133
• A. Barvinok, Z. Luria, A. Samorodnitsky, A. Yong, An approximation algorithm for counting contingency tables, Random Structures Algorithms, 2010. https://doi.org/10.1002/rsa.20301
• P. Brändén, J. Leake, I. Pak, Lower bounds for contingency tables via Lorentzian polynomials, Israel J. Math., 2023. https://doi.org/10.1007/s11856-022-2364-9
• H. Guo, M. Jerrum, Counting vertices of integral polytopes defined by facets, Discrete Comput. Geom., 2023. https://doi.org/10.1007/s00454-022-00406-8

Motivation

A contingency table with margins $r=(r_1,\dots,r_m)$ and $c=(c_1,\dots,c_n)$ is a nonnegative integer matrix whose row sums are $r$ and column sums are $c$. Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.

Timeline

• 1995. Diaconis and Gangolli survey enumeration and random generation of rectangular arrays with fixed margins (doi:10.1007/978-1-4612-0801-3_3).
• 1997–2002. Dyer, Kannan and Mount sample dense tables via the transportation polytope; Morris improves the dense bounds (doi:10.1002/rsa.10049).
• 2000. Dyer and Greenhill give polynomial-time approximate counting and sampling for two-rowed tables.
• 2003. Kijima and Matsui give exact sampling for two rows by coupling from the past; Cryan and Dyer approximately count for a fixed number of rows (doi:10.1016/S0022-0000(03)00014-X); Dyer gives an exact dynamic-programming sampler for fixed row count.
• 2006. Cryan, Dyer, Goldberg, Jerrum and Martin prove rapid mixing of the heat-bath chain for every fixed number of rows (doi:10.1137/S0097539703434243).
• 2016. DeSalvo and Zhao give an exact divide-and-conquer sampler whose polynomial runtime is conditional on a conjecture (arXiv:1507.00070).
• 2021. Arman, Gao and Wormald give linear-time exact generation for sparse margins with $5\Delta^4<N$, and report that no polynomial-time approximately uniform sampler for arbitrary margins was known (arXiv:2104.09413).
• 2024. Göbel, Liu, Manurangsi and Pappik turn sufficiently accurate samplers into perfect samplers (arXiv:2410.00882).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.

Setting

For nonnegative integer vectors $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with common total $N=\sum_ir_i=\sum_jc_j$, let

$$\Omega(r,c)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j\Bigr\}.$$

The input is $(m,n,r,c)$ with margins in binary, so its length is polynomial in $m$, $n$ and $\log(N+1)$. An algorithm uses unbiased random bits. For laws on a finite set, $\mathrm{TV}(\mu,\nu)=\tfrac12\sum_x|\mu(x)-\nu(x)|$.

Formalization targets

Milestone: Theorem 1.1(i) (almost-uniform, bounded time)

For each $k\ge1$, an algorithm halts on every execution in time $\mathrm{poly}(m,n,\log(N+1),k)$ and outputs $X\in\Omega(r,c)$ with

$$\mathrm{TV}\bigl(\mathrm{law}(X),\ \mathrm{Unif}\,\Omega(r,c)\bigr)\le2^{-k}.$$

Goal: Theorem 1.1(ii) (exact uniform sampling)

An algorithm outputs $X\in\Omega(r,c)$ with

$$\Pr[X=Y]=\frac1{|\Omega(r,c)|}\quad(Y\in\Omega(r,c)),$$

terminates almost surely, and has expected running time $\mathrm{poly}(m,n,\log(N+1))$, with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.

Significance

The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.
• Inputs are binary encodings with delimiters (encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).
• tableMass A input t X and haltMass A input t are the fractions of the $2^t$ random tapes of length $t$ that halt with output $X$, respectively halt at all, within $t$ ticks.
• ExactSamplingStatement: one machine and constants $C>0$, $d$ such that for all $m,n,r,c$ with equal totals: every halted output is in $\Omega(r,c)$; tableMass → 1/|Ω| for each table; haltMass → 1; and $\sum_t(1-\text{haltMass}_t)$, the expected running time, is at most $C(m+n+\lceil\log_2(N+1)\rceil+1)^d$.
• BoundedSamplingStatement: every tape of length $t=C(m+n+\lceil\log_2(N+1)\rceil+k+1)^d$ halts with a feasible table, and the TV distance to uniform is at most $2^{-k}$.
• Dimensions $m,n$ vary freely (zero allowed); the machine is uniform, not one per size.

Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.

Selected references

• OpenAI, Exact Uniform Sampling of Contingency Tables with Arbitrary Margins, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/main.pdf
• P. Diaconis, A. Gangolli, Rectangular arrays with fixed margins, Discrete Probability and Algorithms, 1995. https://doi.org/10.1007/978-1-4612-0801-3_3
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• M. Cryan, M. Dyer, A polynomial-time algorithm to approximately count contingency tables when the number of rows is constant, J. Comput. System Sci., 2003. https://doi.org/10.1016/S0022-0000(03)00014-X
• M. Cryan, M. Dyer, L. A. Goldberg, M. Jerrum, R. Martin, Rapidly mixing Markov chains for sampling contingency tables with a constant number of rows, SIAM J. Comput., 2006. https://doi.org/10.1137/S0097539703434243
• S. DeSalvo, J. Y. Zhao, Random sampling of contingency tables via probabilistic divide-and-conquer, preprint, 2016. https://arxiv.org/abs/1507.00070
• A. Arman, P. Gao, N. Wormald, Linear-time uniform generation of random sparse contingency tables with specified marginals, preprint, 2021. https://arxiv.org/abs/2104.09413
• A. Göbel, J. Liu, P. Manurangsi, M. Pappik, Perfect sampling from rapidly mixing Markov chains, preprint, 2024. https://arxiv.org/abs/2410.00882

Motivation: counting common bases of two matroids

A matroid abstracts linear independence: a finite ground set with a family of "independent" subsets that is closed under subsets and satisfies the augmentation axiom. Its maximal independent sets, the bases, all have the same size, the rank. Matroid intersection, finding a common basis of two matroids, is one of the central polynomially solvable problems of combinatorial optimization (Edmonds, 1979). Counting common bases is much harder. It contains counting bases of a single matroid (take both matroids equal) and counting perfect matchings of a bipartite graph (take two partition matroids), and exact counting is #P-hard. The natural goal is therefore a fully polynomial randomized approximation scheme (FPRAS): an algorithm whose output is within relative error $\epsilon$ with probability at least $1-\delta$, in time polynomial in the input size, $\epsilon^{-1}$ and $\log\delta^{-1}$. The matroids should be accessible only through independence oracles.

Background and timeline

• 1979 — Edmonds gives a polynomial-time algorithm for matroid intersection (Ann. Discrete Math. 4).
• 1992 — Feder and Mihail give sampling and approximate counting for balanced matroids (STOC 1992).
• 2004 — Jerrum, Sinclair and Vigoda give an FPRAS for the permanent of nonnegative matrices, covering bipartite perfect matchings (J. ACM 51).
• 2007 — Barvinok and Samorodnitsky obtain coarse logarithmic estimates via random weighting (Israel J. Math. 158).
• 2016–2017 — Anari, Oveis Gharan and Rezaei prove rapid mixing for strongly Rayleigh distributions (COLT 2016); Anari and Oveis Gharan obtain exponential-factor approximations from real-stable polynomials (arXiv:1702.02937).
• 2020 — Brändén and Huh develop Lorentzian polynomials (Ann. of Math. 192).
• 2021 — Anari, Oveis Gharan and Vinzant give a deterministic $2^{O(r)}$-factor approximation for common bases of rank-$r$ matroids (Duke Math. J. 170); Cryan, Guo and Mousa ask for a rapidly mixing chain for common bases (Ann. Probab. 49).
• 2023–2024 — Liu's dissertation records the FPRAS question for two arbitrary oracle matroids (Section 13.2, Problem 1, thesis); Anari, Liu, Oveis Gharan and Vinzant give an FPRAS for bases of a single matroid (Ann. of Math. 199).
• 2026 — An OpenAI preprint, Approximate counting of common bases of two matroids (OpenAI Math Release, September 23, 2026), claims an independence-oracle FPRAS for common bases of two arbitrary matroids of equal rank. It has not been peer reviewed, and its proof is not formally verified.

Setting

Let $M_1,M_2$ be matroids of the same rank $r$ on the ground set $[n]$, supplied by exact independence oracles: a query is an $n$-bit indicator of a subset, and the answer says whether it is independent. The quantity to estimate is

$$Z(M_1,M_2)=\bigl|\mathcal B(M_1)\cap\mathcal B(M_2)\bigr|,$$

the number of common bases. The input also contains rationals $\epsilon,\delta\in(0,1)$; $\ell$ denotes the binary encoding length of $n,r,\epsilon,\delta$. Oracle calls are counted separately from the bit operations used to build queries and process answers.

Formalization targets

Goal: an FPRAS for common bases in the independence-oracle model (Theorem 1.1)

There is a single randomized oracle algorithm and a fixed polynomial $p$ such that, for all rank-$r$ matroids $M_1,M_2$ on $[n]$ and rational $\epsilon,\delta\in(0,1)$, it outputs a nonnegative rational $\widehat Z$ with

$$\Pr\bigl[(1-\epsilon)Z\le\widehat Z\le(1+\epsilon)Z\bigr]\ \ge\ 1-\delta,$$

the output is always $0$ when $Z=0$, and on every execution the numbers of oracle calls and bit operations are at most $p(n,\ell,\epsilon^{-1},\log\delta^{-1})$. The algorithm uses only independent fair random bits. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 answers the question recorded by Liu (2023) and extends both the single-matroid FPRAS of Anari–Liu–Oveis Gharan–Vinzant and, in the bipartite-matching case, the permanent FPRAS of Jerrum–Sinclair–Vigoda. It needs no representation of either matroid and holds for unrestricted rank, whereas the previous oracle-model scheme was fully polynomial only for $r=O(\log n)$. The source derives FPRASs and almost-uniform samplers for common independent sets of prescribed, unrestricted or maximum size, even for matroids of different ranks (Corollary 9.1).

Formalizing it. The Lean goal fixes a concrete machine model, so it states a complete complexity-theoretic claim with no informal "polynomial-time" left. A proof would combine Lorentzian-polynomial inequalities (Brändén–Huh), a transport inequality, a Markov-chain Poincaré bound, and simulated annealing with explicit bit accounting. Each layer is reusable: Mathlib has matroids, but no Lorentzian polynomials, no mixing-time theory of this kind and no randomized-algorithm framework.

Difficulty

For one matroid, the bases-exchange walk mixes rapidly because the basis generating polynomial is log-concave. The intersection of two matroids has no such structure: its common bases need not be connected by short exchanges, and the natural chain on transversals of the paired construction passes through states of exponentially small weight, so positivity and connectivity alone give no polynomial bound. Earlier approaches either lost exponential factors or needed real-stable polynomials that an independence oracle does not provide. The proof must balance defect classes, as in Jerrum–Sinclair–Vigoda, and establish a Poincaré inequality for observables from matroid-theoretic inequalities alone.

Formalization scope

• Matroids are Mathlib Matroid (Fin n) with ground set univ and eRank = r for both. Oracles are functions Bool → (Fin n → Bool) → Bool, required to answer independence queries exactly.
• The algorithm is one fixed Program k s for a register machine with $k+8$ binary stacks: push/pop, fair coin, oracle query on an $n$-bit register, and halt with output (register 6)/(register 7) as a rational. Inputs $n,r,\epsilon,\delta$ are loaded in binary.
• The resource bound is $B=C(1+n+\ell+\lceil\epsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil)^d$ with constants $C>0,d$ fixed before the instance. For every infinite bit stream, the run halts within $B$ steps with at most $B$ oracle calls and $B$ bit operations, outputs a nonnegative rational, and outputs $0$ when $Z=0$.
• The success probability is expressed by counting: at least $(1-\delta)2^B$ of the $2^B$ bit strings of length $B$ lead to an output within relative error $\epsilon$ of $Z$.
• A trivializing reading is excluded: the program and constants come first and must work for every $n,r$, matroid pair, oracle and $\epsilon,\delta$.
• Needed infrastructure: Lorentzian polynomials and the homogeneous Tutte inequalities, Markov chains on finite state spaces with Poincaré/variance bounds, annealing estimators, and correctness proofs for the register machine. Contributions on any layer are welcome.

Selected references

• J. Edmonds, Matroid intersection, Ann. Discrete Math. 4 (1979), 39–49. https://doi.org/10.1016/S0167-5060(08)70817-3
• T. Feder and M. Mihail, Balanced matroids, STOC 1992. https://doi.org/10.1145/129712.129716
• M. Jerrum, A. Sinclair and E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• A. Barvinok and A. Samorodnitsky, Random weighting, asymptotic counting, and inverse isoperimetry, Israel J. Math. 158 (2007). https://doi.org/10.1007/s11856-007-0008-8
• P. Brändén and J. Huh, Lorentzian polynomials, Ann. of Math. 192 (2020), 821–891. https://doi.org/10.4007/annals.2020.192.3.4
• N. Anari, S. Oveis Gharan and C. Vinzant, Log-concave polynomials I, Duke Math. J. 170 (2021). https://doi.org/10.1215/00127094-2020-0091
• M. Cryan, H. Guo and G. Mousa, Modified log-Sobolev inequalities for strongly log-concave distributions, Ann. Probab. 49 (2021). https://doi.org/10.1214/20-AOP1453
• N. Anari, K. Liu, S. Oveis Gharan and C. Vinzant, Log-concave polynomials II: high-dimensional walks and an FPRAS for counting bases of a matroid, Ann. of Math. 199 (2024). https://doi.org/10.4007/annals.2024.199.1.4
• K. Liu, Spectral Independence: A New Tool to Analyze Markov Chains, PhD thesis, University of Washington, 2023. https://kuikuiliu.github.io/files/dissertation.pdf
• OpenAI, Approximate counting of common bases of two matroids, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Approximate-counting-of-common-bases-of-two-matroids-September-23-2026/main.pdf

Motivation: how much randomness fits under prescribed edge probabilities?

Prescribing the probability $x_e$ that each edge belongs to a random perfect matching does not determine the distribution of the whole matching. The largest entropy compatible with those edge probabilities, $H(x)$, measures how many matching choices can coexist with them, and it links three topics: lower bounds on the number of perfect matchings, convex-optimization approaches to approximate counting, and the facial geometry of the perfect-matching polytope. For bipartite graphs, Schrijver's permanent inequality (Schrijver 1998) and Gurvits' weighted Bethe inequality (Gurvits 2011) give the clean comparison $H\ge F-B$ between $H$ and sums of one-coordinate entropies. For general graphs, odd cuts make such comparisons harder, and Anari, Oveis Gharan and Vinzant (2018) asked (FOCS version, Conjecture 6) whether the maximum binary-coordinate entropy over the polytope exceeds $\log N(G)$ by only a linear function of the number of vertices.

Timeline

• 1965 — Edmonds describes the perfect-matching polytope by degree equations, nonnegativity and odd-cut inequalities (Edmonds 1965).
• 1982 — Naddef (Math. Program. 1982) and Edmonds, Pulleyblank and Lovász (Combinatorica 1982) determine the dimension of the perfect-matching polytope.
• 1986 — Chung, Graham, Frankl and Shearer: Shearer's entropy inequality (JCTA 1986), which gives $H\le F$.
• 1998–2011 — Schrijver's lower bound for regular bipartite graphs and Gurvits' Bethe-approximation form give $H\ge F-B$ in the bipartite case.
• 2011 — Esperet, Kardoš, King, Král' and Norine: exponentially many perfect matchings in bridgeless cubic graphs (Adv. Math. 2011).
• 2018 — Anari, Oveis Gharan and Vinzant propose the entropy framework and the linear-error question (FOCS 2018).
• 2022 — Ebrahimnejad, Nagda and Oveis Gharan count perfect matchings in regular expanding nonbipartite graphs (ITCS 2022).
• 2026 — Abdi, Cornuéjols, Dadush and Dalirrooyfard bound the rank of tight odd cuts by $3m-1$ and give exponential lower counts for regular graphs of degree at least four with an odd-cut condition (Proc. LMS 2026). An OpenAI preprint, Entropy and Face Dimension of the Perfect-Matching Polytope (OpenAI Math Release, September 23, 2026), claims the pointwise bound $F-(2-2/m)B\le H\le F$ and a positive answer to the Anari–Oveis Gharan–Vinzant question. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite loopless multigraph with vertex set $V$, $|V|=2m\ge2$, and edge set $E$ (parallel edges are distinct coordinates). A perfect matching is a set of edges covering each vertex exactly once; $\mathcal M(G)$ is the set of them and $N(G)=|\mathcal M(G)|$. The perfect-matching polytope is

$$P(G)=\operatorname{conv}\{\mathbf 1_M: M\in\mathcal M(G)\}\subseteq\mathbb R^E .$$

For $x\in P(G)$ put, with natural logarithms and $0\log 0=0$,

$$H(x)=\max\Big\{-\sum_M p_M\log p_M:\ p\text{ a probability law on }\mathcal M(G),\ \sum_M p_M\mathbf 1_M=x\Big\},$$ $$F(x)=-\sum_{e}x_e\log x_e,\qquad B(x)=-\sum_e(1-x_e)\log(1-x_e).$$

Formalization targets

The milestones are listed in attack order: the face of a triangle expansion (Lemma 5.1), the coefficient-eight nonlinear bound (Theorem B.1), deterministic approximate counting (Theorem 1.2) and its singleton-loop variant (Proposition C.1).

Goal: Theorem 1.1 (pointwise entropy bounds)

If $G$ has at least one perfect matching, then for every $x\in P(G)$

$$F(x)-\Big(2-\frac 2m\Big)B(x)\;\le\;H(x)\;\le\;F(x).$$

The bound holds on the whole polytope, boundary included. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The upper bound is Shearer's inequality; the content is the lower comparison with coefficient $2-2/m$, valid in nonbipartite graphs where the bipartite coefficient $1$ fails (the source gives an eight-vertex counterexample, and Corollary 5.3 shows any universal coefficient is at least $\ln3/(2\ln(3/2))$). Optimizing over $x$ gives $\log N(G)\le\max_{P(G)}(F+B)\le\log N(G)+3m-2$, answering the Anari–Oveis Gharan–Vinzant question. Plugging in uniform marginals gives $N(G)\ge e^{-2(m-1)}k^m$ for graphs with $k$ edge-disjoint perfect matchings, and for $k$-regular graphs whose odd cuts all have at least $k$ edges. The same entropy framework yields a deterministic polynomial-time algorithm approximating $N(G)$ within a factor $512^n$ for graphs with binary edge multiplicities (Theorem 1.2).

Formalizing it. The goal is a finite-dimensional inequality about polytopes and entropies, accessible to Mathlib's convexity and analysis libraries. The milestones extend the mission to a certified polynomial-time counting algorithm in Mathlib's Turing-machine model, a rare example of a formally specified approximation algorithm for a #P-hard quantity.

Difficulty

Shearer's inequality gives the upper bound in one line, and in bipartite graphs the lower bound follows from permanent inequalities that have no analogue for general graphs. A direct convexity argument fails because $H$ is not differentiable across faces of $P(G)$: at a boundary mean the maximum-entropy law lives on a lower-dimensional face, and its covariance is singular in the ambient edge space. The lower bound must therefore be proved face by face, and it needs the sharp geometric estimate $|\operatorname{supp}x|-\dim F_x\le 3m-2$ for the minimal face $F_x$ containing $x$; the earlier rank bound $3m-1$ would not give the coefficient $2-2/m$.

Formalization scope

• Graphs are LooplessGraph V E: endpoint maps left right : E → V with left e ≠ right e, on finite types with decidable equality, so parallel edges are distinct elements of E. A perfect matching is a Finset E with exactly one edge at each vertex.
• polytope G is the convex hull of matching indicator vectors in E → ℝ; maxMatchingEntropy G x is sSup of the entropies of probability vectors on matchings with mean x. On the polytope this set is nonempty, compact and bounded, so the sSup is the attained maximum; off the polytope it would be junk, which is why the hypothesis x ∈ G.polytope is required.
• entropy uses Real.negMulLog, so $0\log0=0$; complementEntropy x is $B(x)$.
• Hypotheses: 0 < m, Fintype.card V = 2 * m, and a perfect matching exists. The coefficient is the real number 2 - 2 / m.
• The counting milestones use Turing.TM2ComputableInPolyTime with finite alphabets, binary encodings of the vertex count and of positive multiplicity records, and require polynomially bounded output length.
• Infrastructure needed: Edmonds' polytope description, faces and minimal faces of polytopes, exponential families and covariance, and polynomial-time computability of rational arithmetic in TM2. The polytope and entropy definitions are reusable for other counting missions.

Selected references

• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards B 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• L. G. Valiant, The complexity of computing the permanent, Theoret. Comput. Sci. 8 (1979), 189–201. https://doi.org/10.1016/0304-3975(79)90044-6
• D. Naddef, Rank of maximum matchings in a graph, Math. Program. 22 (1982), 52–70. https://doi.org/10.1007/BF01581025
• J. Edmonds, W. R. Pulleyblank, L. Lovász, Brick decompositions and the matching rank of graphs, Combinatorica 2 (1982), 247–274. https://doi.org/10.1007/BF02579233
• F. R. K. Chung, R. L. Graham, P. Frankl, J. B. Shearer, Some intersection theorems for ordered sets and graphs, J. Combin. Theory Ser. A 43 (1986), 23–37. https://doi.org/10.1016/0097-3165(86)90019-1
• A. Schrijver, Counting 1-factors in regular bipartite graphs, J. Combin. Theory Ser. B 72 (1998), 122–135. https://doi.org/10.1006/jctb.1997.1798
• N. Linial, A. Samorodnitsky, A. Wigderson, A deterministic strongly polynomial algorithm for matrix scaling and approximate permanents, Combinatorica 20 (2000), 545–568. https://doi.org/10.1007/s004930070007
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• L. Esperet, F. Kardoš, A. D. King, D. Král', S. Norine, Exponentially many perfect matchings in cubic graphs, Adv. Math. 227 (2011), 1646–1664. https://doi.org/10.1016/j.aim.2011.03.015
• L. Gurvits, Unleashing the power of Schrijver's permanental inequality with the help of the Bethe approximation (2011). https://arxiv.org/abs/1106.2844v11
• M. Cygan, M. Pilipczuk, R. Škrekovski, A bound on the number of perfect matchings in Klee-graphs, Discrete Math. Theor. Comput. Sci. 15 (2013), 37–52. https://doi.org/10.46298/dmtcs.633
• A. Barvinok, Approximating permanents and hafnians, Discrete Analysis (2017). https://doi.org/10.19086/da.1244
• N. Anari, S. Oveis Gharan, C. Vinzant, Log-concave polynomials, entropy, and a deterministic approximation algorithm for counting bases of matroids, FOCS 2018, 35–46. https://doi.org/10.1109/FOCS.2018.00013
• F. Ebrahimnejad, A. Nagda, S. Oveis Gharan, Counting and sampling perfect matchings in regular expanding non-bipartite graphs, ITCS 2022, 61:1–61:12. https://doi.org/10.4230/LIPIcs.ITCS.2022.61
• A. Abdi, G. Cornuéjols, D. Dadush, M. Dalirrooyfard, Lower bounds for cube-ideal set-systems, Proc. London Math. Soc. 133 (2026), e70199. https://doi.org/10.1112/plms.70199
• OpenAI, Entropy and Face Dimension of the Perfect-Matching Polytope, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Entropy-and-Face-Dimension-of-the-Perfect-Matching-Polytope-September-23-2026/main.pdf

Motivation: approximately counting perfect matchings

A perfect matching of a graph is a set of edges covering every vertex exactly once. Finding one is easy — Edmonds (1965) gave a polynomial-time algorithm for general graphs — but counting them is hard: Valiant (1979) proved exact counting #P-complete already for bipartite graphs, where the count is the permanent of a 0–1 matrix. Exact counting is tractable only in special classes, such as planar graphs via Pfaffians (Kasteleyn 1963). The natural relaxation is a fully polynomial randomized approximation scheme (FPRAS): an algorithm that, with probability at least $1-\delta$, returns the count within relative error $\varepsilon$, in time polynomial in the input size, $1/\varepsilon$ and $\log(1/\delta)$. Whether perfect matchings in general (nonbipartite) graphs admit an FPRAS was explicitly raised by Jerrum and Sinclair in 1989 and has been a benchmark question in approximate counting since. Perfect-matching counts are partition functions of the monomer–dimer model, so the question also connects to statistical physics.

Timeline

• 1963 — Kasteleyn: exact counting of perfect matchings in planar graphs (J. Math. Phys. 1963).
• 1965 — Edmonds: polynomial-time maximum matching in general graphs (Canad. J. Math. 1965).
• 1979 — Valiant: computing the permanent is #P-complete (TCS 1979).
• 1986 — Jerrum, Valiant and Vazirani: equivalence of approximate counting and almost-uniform sampling for self-reducible problems (TCS 1986).
• 1989 — Jerrum and Sinclair: FPRAS for the number of all matchings in any graph, and for perfect matchings when the near-perfect/perfect ratio is polynomially bounded; they raise the general question (SIAM J. Comput. 1989, Section 7(i)).
• 2004 — Jerrum, Sinclair and Vigoda: FPRAS for the permanent of every nonnegative matrix, i.e. bipartite perfect matchings (J. ACM 2004); accelerated by Bezáková, Štefankovič, Vazirani and Vigoda (SIAM J. Comput. 2008).
• 2018 — Štefankovič, Vigoda and Wilmes: graphs on which every chain of Jerrum–Sinclair–Vigoda type either gives perfect matchings exponentially small mass or mixes exponentially slowly (LATIN 2018).
• 2020–2025 — Cai and Liu relate the problem to the eight-vertex model (ICALP 2020); Fei, Goldberg and Lu locate it among two-state spin systems (Inf. Comput. 2025).
• 2026 — Further permanent speedups by Chen, Vigoda and Yang (arXiv:2608.26599) and Chen, Guo, Vigoda and Yang (arXiv:2609.20717); deterministic hafnian approximation for dense graphs by Yi (arXiv:2609.04079). An OpenAI preprint, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs (OpenAI Math Release, September 23, 2026), claims an FPRAS for every finite simple graph. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A finite simple undirected graph $G$ on vertices $\{0,\dots,n-1\}$ is given by a set of edges, each written once as a pair $(u,v)$ with $u<v$. A set $M\subseteq E$ is a perfect matching if every vertex lies in exactly one edge of $M$, and

$$Z(G)=\#\{M\subseteq E: M\text{ is a perfect matching of }G\}.$$

(The graph with no vertices has $Z=1$; any graph with an odd number of vertices has $Z=0$.)

A randomized algorithm is modelled as a single fixed machine with a finite transition table over a finite tape alphabet, which at each step reads the current tape symbol and one fresh fair random bit, then writes, moves, or halts. The input is the graph in binary (number of vertices, number of edges, the sorted edge list) followed by the rationals $\varepsilon$ and $\delta$ in reduced form; the output is a rational number written on the tape when the machine halts.

Formalization targets

Goal: Theorem 1.1 (FPRAS for perfect matchings)

There are a machine $A$ and constants $C>0$, $d$ such that for every graph $G$ and rationals $0<\varepsilon<1$, $0<\delta<1/2$, with $t=C\,(|\mathrm{input}|+\lceil\varepsilon^{-1}\rceil+\lceil\log_2\lceil\delta^{-1}\rceil\rceil+1)^d$:

• on every random string of length $t$, $A$ halts within $t$ steps with a nonnegative rational output $\widehat Z$;
• if $Z(G)=0$, the output is $0$ on every random string;

$$\Pr_{\text{bits}}\big[(1-\varepsilon)Z(G)\le\widehat Z\le(1+\varepsilon)Z(G)\big]\;\ge\;1-\delta.$$

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem answers the Jerrum–Sinclair question affirmatively: perfect matchings in arbitrary graphs can be approximately counted as efficiently, up to polynomial factors, as in the bipartite case. The worst-case time bound holds for every execution, not just in expectation. Via standard reductions, the source also derives counting schemes for edge subsets with prescribed vertex degrees and for matchings of a fixed size (Corollary 10.1). The accompanying samplers for those families always return a feasible object and approximate the uniform law in total variation.

Formalizing it. The statement fixes a concrete machine model, input encoding and time bound, so a formal proof would certify both correctness of the estimator and the polynomial running time of an explicit algorithm — a level of rigor rarely reached for Markov-chain Monte Carlo results, whose analyses involve many interacting constants.

Difficulty

The natural approach extends the Jerrum–Sinclair–Vigoda Markov chain on perfect and near-perfect matchings, with weights learned while edge activities are gradually lowered. In general graphs this approach provably fails: Štefankovič, Vigoda and Wilmes constructed graphs on which every chain of that type, for any hole-dependent weights, has either exponentially small stationary mass on perfect matchings or exponentially slow mixing. Odd cycles (blossoms) are the reason the bipartite canonical-path arguments do not carry over. A solution needs a different state space and a different mixing analysis.

Formalization scope

• GraphInput is a vertex count n and a Finset (Fin n × Fin n) of edges with strictly increasing endpoints, so loops and duplicate edges are excluded. Perfect G M requires M ⊆ edges and that each vertex is incident to exactly one edge of M; Z G is the number of such M.
• The machine model is RandomMachine: a finite transition table on Fin 8 symbols, whose step consumes one random bit and performs a Turing.TM0 write or move, or halts. run folds tick over a list of t bits; halted configurations are absorbing.
• encodeInput writes the vertex count, edge count and lexicographically sorted edges in binary, then encodeRat ε and encodeRat δ (reduced numerator with sign, denominator). Outputs requires that the machine has halted and the tape to the right of the head is exactly the encoding of the output rational.
• The time bound is a fixed polynomial with natural ceilings; the success probability is the fraction of good tapes among all $2^t$ tapes.
• The scheme must be uniform: one machine for all inputs, quantified before the graph. A trivializing reading is excluded because every tape must halt within the bound with a nonnegative output, and zero must be returned exactly when $Z(G)=0$.
• Infrastructure needed: a compiler-style layer turning structured randomized algorithms into RandomMachine transitions, Markov-chain spectral-gap bounds, and sampling-to-counting reductions. The machine model and encodings are reusable for other approximate-counting missions.

Selected references

• P. W. Kasteleyn, Dimer statistics and phase transitions, J. Math. Phys. 4 (1963), 287–293. https://doi.org/10.1063/1.1703953
• J. Edmonds, Paths, trees, and flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• L. G. Valiant, The complexity of computing the permanent, Theoret. Comput. Sci. 8 (1979), 189–201. https://doi.org/10.1016/0304-3975(79)90044-6
• M. R. Jerrum, L. G. Valiant, V. V. Vazirani, Random generation of combinatorial structures from a uniform distribution, Theoret. Comput. Sci. 43 (1986), 169–188. https://doi.org/10.1016/0304-3975(86)90174-X
• M. Jerrum, A. Sinclair, Approximating the permanent, SIAM J. Comput. 18 (1989), 1149–1178. https://doi.org/10.1137/0218077
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM 51 (2004), 671–697. https://doi.org/10.1145/1008731.1008738
• I. Bezáková, D. Štefankovič, V. V. Vazirani, E. Vigoda, Accelerating simulated annealing for the permanent and combinatorial counting problems, SIAM J. Comput. 37 (2008), 1429–1454. https://doi.org/10.1137/050644033
• D. Štefankovič, E. Vigoda, J. Wilmes, On counting perfect matchings in general graphs, LATIN 2018, LNCS 10807, 873–885. https://doi.org/10.1007/978-3-319-77404-6_63
• J.-Y. Cai, T. Liu, Counting perfect matchings and the eight-vertex model, ICALP 2020, LIPIcs 168, 23:1–23:18. https://doi.org/10.4230/LIPIcs.ICALP.2020.23
• Y. Fei, L. A. Goldberg, P. Lu, Two-state spin systems with negative interactions, Inf. Comput. 307 (2025), 105340. https://doi.org/10.1016/j.ic.2025.105340
• OpenAI, A Fully Polynomial Randomized Approximation Scheme for Perfect Matchings in General Graphs, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Fully-Polynomial-Randomized-Approximation-Scheme-for-Perfect-Matchings-in-General-Graphs-September-23-2026/main.pdf