OAI Math

Motivation

Min-UnCut asks, for a finite simple graph $G=(V,E)$, for the minimum number of edges whose deletion makes $G$ bipartite. Equivalently, for a bipartition $V=S\sqcup(V\setminus S)$ let $\mathrm{Uncut}_G(S)$ count the edges with both endpoints on the same side, and set $\mathrm{OPT}_{\mathrm{uncut}}(G)=\min_S\mathrm{Uncut}_G(S)$. The quantity measures distance from bipartiteness. Although it equals $|E|$ minus the maximum cut, a good multiplicative approximation for Max-Cut gives nothing multiplicative for Min-UnCut on nearly bipartite graphs, which is exactly the regime of interest.

The best known algorithm (Agarwal, Charikar, Makarychev, Makarychev, STOC 2005) achieves an $O(\sqrt{\log|V|})$ factor. Before the source preprint, NP-hardness was known only for specific constant factors below about $1.49$, and hardness for every constant factor was known only under the Unique Games Conjecture.

This mission asks for a machine-checked proof that Min-UnCut has no polynomial-time approximation within any constant factor unless P = NP, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 2001 — Håstad's near-satisfiable gap for three-variable parity equations (JACM 2001); combined with parallel repetition (Raz, SICOMP 1998; Holenstein, ToC 2009) it is the preprint's starting point.
• 2005 — Agarwal, Charikar, Makarychev and Makarychev give $O(\sqrt{\log n})$ approximations for Min-UnCut and Min 2CNF Deletion (STOC 2005).
• 2007 — Under the Unique Games Conjecture, the near-satisfiable Max-Cut gap of Khot, Kindler, Mossel and O'Donnell implies arbitrarily large constant gaps for weighted Min-UnCut (SICOMP 2007).
• 2017 — Håstad, Huang, Manokaran, O'Donnell and Wright: NP-hard below $11/8$ for the weighted deletion formulation (ToC 2017).
• 2018 — Wiman: factors below $1.45685$ (KTH master's thesis, 2018).
• 2024 — Martinsson: factors below $73139148/49096883\approx1.48969$ for violated two-variable parity equations, transferring to weighted Min-UnCut (APPROX/RANDOM 2024).
• 2026 — The OpenAI preprint claims NP-hardness for every constant factor on simple unweighted graphs.

Setting

A graph is finite, simple, undirected and unweighted, given by a vertex count $N$ and a symmetric loopless Boolean adjacency table. A cut is a map $c:\{0,\dots,N-1\}\to\{0,1\}$; the parts may be empty or unbalanced. $\mathrm{Uncut}(c)$ counts unordered edges $\{u,v\}$ with $c(u)=c(v)$, and $\mathrm{OPT}_{\mathrm{uncut}}(G)$ is its minimum over all cuts.

3SAT formulas are conjunctions of three-slot clauses over natural-number variable names (repeated variables allowed), given to the reduction by a canonical prefix-free binary encoding.

Formalization targets

Goal: constant-factor hardness (Theorem 1.1, p. 2)

For every fixed integer $K\ge2$ there is a deterministic polynomial-time reduction $\varphi\mapsto(G,k)$ to an explicit simple graph $G$ and a binary integer $k\ge1$ with

with graph size and running time polynomial in the bit length of $\varphi$ for each fixed $K$. Choosing $K\ge C$ shows that a deterministic polynomial-time $C$-approximation for any real $C>1$ would imply P = NP. The positive threshold $k\ge1$ is what separates this from bipartiteness testing. In Lean this is OAI.MinUncut.main : Nonempty MinUncut.Reduction.

The preprint also derives Corollary 1.2 (p. 3): minimum 2CNF clause deletion is NP-hard to approximate within every fixed factor $C>1$. It is not formalized on the platform.

Significance

The result itself. Theorem 1.1 settles the constant-factor approximability of Min-UnCut in the hardness direction without the Unique Games Conjecture, and by an exact cost-preserving transformation the same holds for Min 2CNF Deletion. Together with the $O(\sqrt{\log n})$ algorithm, it places these problems strictly between constant-factor approximable and inapproximable within logarithmic factors (the remaining gap concerns super-constant factors).

Formalizing it. No machine-checked proof of super-constant-type inapproximability for any natural graph problem is known to exist. A complete development needs Håstad's parity gap (Theorem 2.2, p. 6) and uniform parallel repetition (Theorem 2.3, p. 7), used as external inputs, plus the preprint's inner decoding theorem (Theorem 3.2, p. 9), the composition gap for bit comparisons (Proposition 6.1, p. 27) and the finite constructions (Lemmas 7.1 and 7.2, pp. 31 and 34). PCP and parallel-repetition infrastructure would be reusable across many hardness missions.

Difficulty

A natural route is to compose a long-code test with a projection game, as in Håstad's work. The obstacle is extracting a label from an arbitrary folded bit proof with a probability and coefficient size independent of the label alphabet: the alphabet grows as the outer soundness is driven down, and every inner constant must be fixed before it (Introduction, pp. 3–4). In addition, the decoder's choices depend on shared background affine functions, so the outer game's soundness must survive such shared hints. Gadget-based approaches yield only isolated constants (up to about $1.49$); unbounded constants previously required the Unique Games hypothesis.

Formalization scope

• MinUncut.Output packages the graph (vertex count, symmetric loopless Bool adjacency) with a threshold threshold ≥ 1; uncut counts pairs u < v that are adjacent and on the same side, and opt is the minimum over all Fin N → Bool cuts (nonempty, so always defined).
• MinUncut.Reduction is a single TM2 machine taking the pair $(K,\varphi)$ (encoded by inputBits) with finite tape alphabets, a polynomial time K bounding the running time in the formula's bit length, and a polynomial size K bounding vertices plus output length; yes/no hold for every K ≥ 2.
• The reduction acts on decoded formulas, so malformed inputs do not arise; runtime is measured in formulaBits φ, the canonical encoding including variable names.
• The hypotheses are satisfiable and the conclusion demands an actual strict multiplicative gap with a positive integer threshold, so outputting a trivially bipartite graph cannot satisfy it.

Welcome contributions: Fourier and Gaussian analysis on $\mathbb F_2$-affine spaces, the long code with folding, parallel repetition for projection games, and Turing-machine complexity infrastructure.

Selected references

• OpenAI, Constant-factor hardness of Min-UnCut, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-Min-UnCut-September-23-2026/paper.pdf
• A. Agarwal, M. Charikar, K. Makarychev, Y. Makarychev, O(√log n) approximation algorithms for Min UnCut, Min 2CNF Deletion, and directed cut problems, STOC 2005. https://doi.org/10.1145/1060590.1060675
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
• J. Håstad, S. Huang, R. Manokaran, R. O'Donnell, J. Wright, Improved NP-inapproximability for 2-variable linear equations, Theory of Computing (2017). https://doi.org/10.4086/toc.2017.v013a019
• M. Wiman, Improved inapproximability of Max-Cut through Min-Cut, master's thesis, KTH, 2018. https://www.diva-portal.org/smash/get/diva2:1229467/FULLTEXT01.pdf
• B. Martinsson, On the NP-hardness approximation curve for Max-2Lin(2), APPROX/RANDOM 2024. https://doi.org/10.4230/LIPIcs.APPROX/RANDOM.2024.11
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• R. Raz, A parallel repetition theorem, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539795280895
• T. Holenstein, Parallel repetition: simplifications and the no-signaling case, Theory of Computing (2009). https://doi.org/10.4086/toc.2009.v005a008
• M. Bellare, O. Goldreich, M. Sudan, Free bits, PCPs, and nonapproximability — towards tight results, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539796302531

Motivation

A directed feedback vertex set of a finite digraph $G$ is a set $F$ of vertices meeting every directed cycle, equivalently one whose removal leaves $G-F$ acyclic; $\mathrm{DFVS}(G)$ is the minimum size of such a set. The problem arises wherever cyclic dependencies must be broken — deadlock resolution, circuit testing, scheduling — and a topological order of $G-F$ certifies a solution in polynomial time.

The best general approximation guarantee is $O(\log n\log\log n)$, originating in Seymour's work on fractional packing of directed circuits (Combinatorica 1995) and made constructive by Even, Naor, Schieber and Sudan (Algorithmica 1998). On the hardness side, NP-hardness was known only for particular constants (via Vertex Cover), while ruling out every constant factor required the Unique Games Conjecture. Whether a constant-factor approximation exists under P ≠ NP alone was open.

This mission asks for a machine-checked proof that approximating DFVS within any fixed factor $A\ge1$ is NP-hard on unweighted digraphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1995–1998 — Seymour's fractional packing bound (Combinatorica 1995) and the algorithm of Even–Naor–Schieber–Sudan (Algorithmica 1998) give $O(\log n\log\log n)$ approximation.
• 2005 — Dinur and Safra prove Vertex Cover NP-hard below $10\sqrt5-21\approx1.36$ (Annals 2005); doubling each undirected edge transfers this to DFVS.
• 2008–2011 — Guruswami, Manokaran and Raghavendra show every constant factor is Unique-Games-hard via maximum acyclic subgraph and feedback arc set (FOCS 2008); expanded with Håstad and Charikar (SICOMP 2011).
• 2013 — Svensson's direct Unique-Games-based construction for vertex deletion problems (ToC 2013).
• 2016 — Guruswami and Lee give a simpler UG-based proof (ToC 2016).
• 2018–2025 — The imperfect-completeness 2-to-1 Games Theorem is completed (Dinur–Khot–Kindler–Minzer–Safra, ToC 2025; Barak–Kothari–Steurer, ITCS 2019; Khot–Minzer–Safra, ECCC TR18-006), giving Vertex Cover, hence DFVS, hardness below $\sqrt2$.
• 2026 — Ghorbani and Mnich record the gap for general digraphs (ICALP 2026); the OpenAI preprint claims NP-hardness for every constant factor.

Setting

A digraph is finite and loopless, given by a vertex count $n$ and a duplicate-free list of arcs $(u,v)$ with $u\ne v$; opposite arcs $(u,v),(v,u)$ are allowed. A directed cycle is a cyclic sequence of $r+1\ge2$ distinct vertices with every successive arc present, including the closing one. $F$ is a feedback set if it meets every directed cycle, and $\mathrm{DFVS}(G)$ is the least size of one.

A language $L\subseteq\{0,1\}^*$ is in NP if there are a polynomial $p$ and a deterministic polynomial-time verifier $V$ (a multi-stack Turing machine with finite alphabets) with $x\in L$ iff some certificate $w$ with $|w|\le p(|x|)$ makes $V(x,w)$ accept.

Formalization targets

Goal: constant-factor hardness (Theorem 1.1, p. 2)

For every real $A\ge1$ and every language $L\in\mathrm{NP}$ there is a deterministic polynomial-time map $x\mapsto(G_x,k_x)$ with $k_x\ge1$ such that

In Lean this is OAI.DirectedFeedback.main : DirectedFeedback.MainStatement. The preprint states Theorem 1.1 as a reduction from an NP-hard promise problem (the 2-to-1 game gap of Theorem 2.1, p. 5) to $(G,k)$; composing with that promise problem's NP-hardness gives the Lean form, which quantifies over all NP languages directly. A deterministic polynomial-time $A$-approximation would then decide every NP language (proof of Theorem 1.1, p. 28).

The preprint also proves Corollary 8.3 (p. 28) for directed feedback arc set; it is not formalized on the platform.

Significance

The result itself. Theorem 1.1 shows that a constant-factor approximation for DFVS exists if and only if P = NP, removing the Unique Games hypothesis from the Guruswami–Manokaran–Raghavendra and Svensson results. It does not determine the true growth of the optimal factor between constants and $O(\log n\log\log n)$.

Formalizing it. No machine-checked inapproximability result of this kind is known to exist. A complete development needs the 2-to-1 Games Theorem with imperfect completeness (Theorem 2.1, p. 5, external input), Friedgut's junta theorem in a dyadic fixed-bias form (Theorem 2.2 and Corollary 2.3, p. 6), finite Ramsey theory and von Neumann's minimax theorem, and the preprint's rank-graph construction (Definition 3.1, p. 8; Proposition 3.7, p. 12), pivotality budget (Definition 6.1, p. 20) and weighted soundness (Proposition 7.4, p. 25). An NP and Karp-reduction library on TM2 machines (including Cook–Levin) would be reusable across the whole family of hardness missions.

Difficulty

The central difficulty (Introduction, pp. 3–4) is extracting a game labeling from an arbitrary acyclic remainder: a topological order exists, but it can interleave the many vertices representing one local test arbitrarily. Comparisons in that order must first be made consistent and then read as Boolean functions; Friedgut-type junta bounds must hold at many biases simultaneously for the same random function, so a separate influence bound at each scale does not suffice. The coordinate lists must also be fixed before the tested game edge is drawn, or they do not define a game labeling. Gadget reductions from Vertex Cover cannot go beyond the Vertex Cover constants.

Formalization scope

• DirectedFeedback.Digraph: n : ℕ, a Nodup list of arcs in Fin n × Fin n, loopless; cycles are injective maps Fin (r+1) → Fin n with all successive arcs (including the wrap-around) present, so 2-cycles count and 1-cycles cannot occur. dfvs is the least cardinality of a feedback Finset.
• NP is defined from scratch by NPVerifier: a polynomial certificate bound and a polynomial-time TM2 verifier with finite alphabets on the unary-framed pair encoding pairBits; no SAT-specific definition is used.
• GapReduction A L is a polynomial-time TM2 machine (finite alphabets, raw-bit input) producing a GapInstance (digraph plus k > 0), encoded explicitly in unary-framed form by GapInstance.bits; completeness and soundness are as displayed, with soundness compared in ℝ.
• The statement quantifies over all NP languages, so its proof must include (or reprove) NP-hardness of the source promise problem in this machine model — e.g. a Cook–Levin theorem for TM2 verifiers plus the 2-to-1 Games reduction.
• k > 0 and the strict inequality rule out a trivial reading (e.g. empty graphs with k = 0).

Welcome contributions: Friedgut's junta theorem, finite Ramsey and minimax in usable forms, the 2-to-1 Games Theorem, and Cook–Levin for Turing.TM2ComputableInPolyTime.

Selected references

• OpenAI, Constant-factor hardness of directed feedback vertex set, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-directed-feedback-vertex-set-September-23-2026/paper.pdf
• P. D. Seymour, Packing directed circuits fractionally, Combinatorica 15 (1995). https://doi.org/10.1007/BF01200760
• G. Even, J. Naor, B. Schieber, M. Sudan, Approximating minimum feedback sets and multicuts in directed graphs, Algorithmica (1998). https://doi.org/10.1007/PL00009191
• I. Dinur, S. Safra, On the hardness of approximating minimum vertex cover, Ann. of Math. 162 (2005). https://doi.org/10.4007/annals.2005.162.439
• V. Guruswami, R. Manokaran, P. Raghavendra, Beating the random ordering is hard: inapproximability of maximum acyclic subgraph, FOCS 2008. https://doi.org/10.1109/FOCS.2008.51
• O. Svensson, Hardness of vertex deletion and project scheduling, Theory of Computing 9 (2013). https://doi.org/10.4086/toc.2013.v009a024
• V. Guruswami, E. Lee, Simple proof of hardness of feedback vertex set, Theory of Computing 12 (2016). https://doi.org/10.4086/toc.2016.v012a006
• I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, ECCC TR18-006 (2018). https://eccc.weizmann.ac.il/report/2018/006/revision/2/download
• E. Friedgut, Boolean functions with low average sensitivity depend on few coordinates, Combinatorica (1998). https://doi.org/10.1007/PL00009809
• F. P. Ramsey, On a problem of formal logic, Proc. London Math. Soc. (1930). https://doi.org/10.1112/plms/s2-30.1.264

Motivation

A projection game (label cover) asks for labels on the two sides of a bipartite multigraph so that, on each edge, the right label is the image of the left label under a prescribed map. In a 2-to-1 game the left alphabet has $2q$ labels, the right alphabet $q$, and every edge map has exactly two preimages of each right label. Khot introduced the 2-to-1 and Unique Games conjectures in 2002 (STOC 2002) as hypotheses that yield tight hardness of approximation. The 2-to-1 Games Conjecture with perfect completeness asserts that, for every fixed $\delta>0$, it is NP-hard to tell satisfiable 2-to-1 games from games in which every labeling satisfies at most a $\delta$ fraction of edges. Perfect completeness matters for problems whose YES instances must be exactly satisfiable, such as graph coloring: hardness with completeness $1-\varepsilon$ does not imply it.

This mission asks for a formal proof of the conjecture, as stated in an OpenAI preprint dated September 23, 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

• 1998 — The PCP theorem (Arora–Safra, JACM 1998; Arora–Lund–Motwani–Sudan–Szegedy, JACM 1998) and Raz's parallel repetition theorem (SICOMP 1998).
• 2002 — Khot formulates the 2-to-1 and Unique Games conjectures.
• 2011 — Rao's parallel repetition for projection games (SICOMP 2011).
• 2014 — Austrin, O'Donnell, Tan and Wright prove perfect-completeness 2-to-1 label cover hardness with alphabets of sizes $6$ and $3$ and soundness $23/24+\varepsilon$ (ACM TOCT 2014).
• 2017–2023 — The Grassmann/shortcode programme: Khot–Minzer–Safra (STOC 2017; ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (STOC 2018), Barak–Kothari–Steurer (ITCS 2019), and the Grassmann expansion theorem of Khot–Minzer–Safra (Annals 2023), giving 2-to-1 hardness with completeness arbitrarily close to $1$.
• 2026 — Fei, Minzer and Wang prove perfect-completeness hardness for 4-to-1 games at arbitrarily small soundness (ECCC TR26-179).
• September 2026 — The OpenAI preprint claims perfect completeness for 2-to-1 games (Theorem 1.1, p. 1).

Setting

For an integer $q\ge2$, a 2-to-1 instance has finite left and right vertex sets and a nonempty list of edge occurrences $e=(u_e,v_e,\pi_e)$, where $\pi_e:[2q]\to[q]$ is given by an explicit table with $|\pi_e^{-1}(b)|=2$ for every $b\in[q]$. Parallel occurrences, possibly with different maps, are allowed and counted with multiplicity; there are no weights. A labeling $(a,b)$ assigns $a(u)\in[2q]$ and $b(v)\in[q]$ and satisfies $e$ when $\pi_e(a(u_e))=b(v_e)$. The value is the maximum, over labelings, of the fraction of satisfied occurrences. 3-SAT inputs are bit strings that decode to conjunctions of three-literal clauses (repetitions allowed); malformed inputs count as unsatisfiable.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every fixed rational $\delta\in(0,1)$ there are an integer $q=q(\delta)\ge2$ and a deterministic polynomial-time reduction $\varphi\mapsto G_\varphi$ from 3-SAT to 2-to-1 instances with alphabets $[2q]$ and $[q]$ such that

The running time is polynomial in the binary input length, with degree and constants depending only on $\delta$.

Significance

The result itself. It removes the conditional hypothesis from perfect-completeness reductions. The preprint derives NP-hardness for maximum $k$-colorable subgraph at soundness $1-\frac1k+C\frac{\log k}{k^2}$ through Guruswami and Sinop's reduction (Corollary 1.2, p. 3), and recovers satisfiable Not-Two and three-query PCP hardness (Corollary 1.3, p. 4), the latter already known unconditionally by Håstad (SICOMP 2014). A companion preprint uses it for hardness of finding large independent sets in three-colorable graphs.

Formalizing it. No PCP-style hardness result of this strength has been machine-checked. A complete development needs a perfect-completeness PCP gap (Theorem 2.1, p. 5), projection-game parallel repetition (Theorem 2.2, p. 6), the Grassmann expansion theorem (Theorem 2.3, p. 7) and inverse shortcode estimates (Theorem 2.6, p. 9), on top of a polynomial-time Turing-machine framework. These components are shared with the Unique Games formalization and would be reusable.

Difficulty

Near-perfect completeness does not give perfect completeness: the $1-\varepsilon$ reductions need not produce any finite satisfiable game. Amplifying a constant-soundness perfect-completeness game by parallel repetition destroys the 2-to-1 structure, since $k$-fold repetition gives $2^k$ preimages per right label. The preprint therefore builds a new tree-structured construction (Section 3) whose joint-partition questions keep two-element fibers and satisfy exact identities, and the soundness analysis must decode labelings through a rank test whose tested rows depend on the decoded form itself (Sections 5–6), before projection-game repetition gives the contradiction (Section 7).

Formalization scope

• ProjectionTable q is a Vector (Fin q) (2*q) with exactly two preimages of every b : Fin q. Instance q lists edges as a List with a nonemptiness proof, so value = maxSatisfied / edges.length never divides by zero; maxSatisfied is a Finset.sup over all labelings.
• BinaryGapReduction δ fixes alphabet ≥ 2, a construct map, a Turing.TM2ComputableInPolyTime witness from raw input bits (identity encoding) to the explicit bit encoding gameBits, finite tape alphabets, completeness value = 1 on encodings of satisfiable formulas, and soundness value ≤ δ on all other inputs.
• The goal quantifies over rational $\delta$ with $0<\delta<1$, as in the source; the alphabet and machine are fixed before the input.
• No vacuous reading: the 3-SAT language is nontrivial and value = 1 requires a labeling satisfying every edge.

Selected references

• OpenAI, Perfect completeness for 2-to-1 games, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Perfect-completeness-for-2-to-1-games-September-23-2026/paper.pdf
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017
• P. Austrin, R. O'Donnell, L.-Y. Tan, J. Wright, New NP-hardness results for 3-coloring and 2-to-1 label cover, ACM Trans. Comput. Theory 6 (2014).
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, STOC 2018. https://doi.org/10.1145/3188745.3188804
• B. Barak, P. K. Kothari, D. Steurer, Small-set expansion in shortcode graph and the 2-to-2 conjecture, ITCS 2019. https://doi.org/10.4230/LIPIcs.ITCS.2019.9
• Y. Fei, D. Minzer, S. Wang, On the hardness of 4-to-1 games with perfect completeness, ECCC TR26-179 (2026). https://eccc.weizmann.ac.il/report/2026/179/
• A. Rao, Parallel repetition in projection games and a concentration bound, SIAM J. Comput. 40 (2011). https://doi.org/10.1137/080734042
• R. Raz, A parallel repetition theorem, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539795280895
• V. Guruswami, A. K. Sinop, Improved inapproximability results for maximum k-colorable subgraph, Theory Comput. 9 (2013). https://doi.org/10.4086/toc.2013.v009a011
• M. Braverman, S. Khot, D. Minzer, On rich 2-to-1 games, ITCS 2021. https://doi.org/10.4230/LIPIcs.ITCS.2021.27
• J. Håstad, On the NP-hardness of Max-Not-2, SIAM J. Comput. (2014). https://doi.org/10.1137/120882718

Motivation: how hard is it to use the promise of three-colorability?

A graph is three-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding three-colorability is NP-complete. The approximate coloring problem asks how much a promise helps: given a graph promised to be three-colorable, can one efficiently find a coloring with a few more colors, or at least a large independent set? Every three-colorable graph on $n$ vertices has an independent set of size $n/3$ (its largest color class). The best polynomial-time algorithms use $n^{0.19\ldots}$ colors, while hardness results long reached only small palettes and needed extra conjectures for stronger gaps. Problems of this kind are central test cases for the PCP theorem, Label Cover and the theory of promise constraint satisfaction.

Background and timeline

• 2000 — Khanna, Linial and Safra prove NP-hardness of $4$-coloring three-colorable graphs (Combinatorica); Guruswami and Khanna give a different proof with bounded-degree variants (SIAM J. Discrete Math. 2004).
• 2009 — Dinur, Mossel and Regev obtain three-colorable completeness with arbitrarily small independent-set soundness, conditional on a fish-shaped Label Cover conjecture (SIAM J. Comput.).
• 2010 — Dinur, Khot, Perkins and Safra prove hardness of finding independent sets of density $1/9$ in almost-three-colorable graphs (FOCS 2010).
• 2020 — Guruswami and Sandeep show that the $d$-to-$1$ Games Conjecture with perfect completeness implies hardness of coloring three-colorable graphs with $O(1)$ colors (ICALP 2020).
• 2021 — Barto, Bulín, Krokhin and Opršal prove hardness of $(2k-1)$-coloring $k$-colorable graphs (five colors for $k=3$) via the algebraic theory of promise CSPs (J. ACM); Braverman, Khot, Lifshitz and Minzer obtain the independent-set gap from the Rich $2$-to-$1$ Games Conjecture (FOCS 2021).
• 2023 — Krokhin, Opršal, Wrochna and Živný give the arc-graph reduction to palette three (SIAM J. Comput.); Hecht, Minzer and Safra treat almost coloring almost-three-colorable graphs (APPROX/RANDOM 2023).
• 2024–2026 — Kawarabayashi, Thorup and Yoneda (STOC 2024) and Bansal, Huang and Lee (arXiv:2602.05904) improve coloring algorithms to $O(n^{0.19539})$ colors; Fei, Minzer and Wang prove the $4$-to-$1$ Games Conjecture with perfect completeness, giving constant-palette hardness and small independent-set density with an eight-colorable promise (ECCC TR26-179).
• 2026 — An OpenAI preprint, Hardness of finding large independent sets in three-colorable graphs (OpenAI Math Release, September 24, 2026), claims unconditional NP-hardness of distinguishing three-colorable graphs from graphs with independence ratio below any fixed $\delta>0$. It has not been peer reviewed, and its proof is not formally verified.

Setting

A 3-CNF formula is a conjunction of clauses, each a disjunction of at most three literals (variables or their negations); it is satisfiable if some truth assignment makes every clause true. For a finite simple undirected graph $G$ with $n=|V(G)|\ge1$ vertices, $\alpha(G)$ is the size of a largest independent set, a set of pairwise nonadjacent vertices. A polynomial-time reduction is a deterministic algorithm that, on an explicit binary encoding of its input, runs in time polynomial in the encoding length and outputs an explicit encoding (here the full adjacency matrix) of the output graph.

Formalization targets

Goal: NP-hardness of the three-colorable vs. small-independence-ratio gap (Theorem 1.1)

For every fixed real $0<\delta<1/3$ there is a deterministic polynomial-time algorithm $R_\delta$ mapping each explicitly encoded 3-CNF formula $\phi$ to a nonempty finite simple graph $G_\phi$ with

The running time and output size are polynomial in the binary length of $\phi$, with constants depending only on $\delta$. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.1 shows that, even with the full promise of three-colorability, it is NP-hard to find an independent set of any fixed positive density. It implies hardness of distinguishing $k$-colorable graphs from non-$c$-colorable graphs for all fixed $3\le k\le c$ (Corollary 1.2), the long-standing conjecture recorded by Barto–Bulín–Krokhin–Opršal. Unlike the routes through $d$-to-$1$ games and arc graphs, it keeps the independent-set soundness together with three-colorable completeness, and unlike Dinur–Khot–Perkins–Safra it does not delete vertices. Earlier results with this combination were conditional (Dinur–Mossel–Regev; Braverman–Khot–Lifshitz–Minzer).

Formalizing it. The statement is fully explicit: Mathlib's TM2ComputableInPolyTime fixes the machine model, and the formula and graph encodings are spelled out bit by bit. A formal proof would require a machine-checked PCP theorem with perfect completeness (Label Cover), a dimension-independent junta approximation theorem, and the paper's alignment and list-decoding lemmas. Any of these is a substantial and reusable formalization project; complexity-theoretic reductions are barely represented in Mathlib today.

Difficulty

Gap reductions from Label Cover to coloring traditionally use long-code or dictatorship tests whose soundness analysis loses control either of three-colorability of every vertex (completeness) or of independent sets of arbitrarily small density (soundness). Known unconditional routes reach constant-palette coloring hardness only by composing reductions that lose the independent-set guarantee, and routes keeping it required unproven games conjectures with structural assumptions. The proof must decode a labeling from any independent set of density $\delta$ in a graph that is genuinely three-colorable on every vertex when $\phi$ is satisfiable, without bounds on projection-fiber sizes.

Formalization scope

• Formulas are lists of clauses of width at most $3$ over literals named by natural numbers; satisfiability uses an assignment $\mathbb N\to\mathrm{Bool}$. Formulas and graphs are encoded as explicit bit strings (self-delimiting binary numbers; the graph encoding lists the vertex count and the full row-major adjacency matrix).
• Graphs are Graph records: $n\ge1$ vertices Fin n, a symmetric loopless Boolean adjacency. Independence number is the maximum card of an independent Finset; three-colorability is a proper map to Fin 3.
• RealGraphReduction δ packages a function reduce : List Bool → Graph with a Turing.TM2ComputableInPolyTime witness (identity input encoding, graphBits output encoding, finite stack alphabets), an explicit polynomial output-size bound, completeness and strict soundness $\alpha<\delta n$ on encoded formulas. The reduction must be total and polynomial-time on all bit strings, which is harmless since malformed inputs can be sent to a fixed graph.
• The goal quantifies over every real $\delta\in(0,1/3)$; the source notes that rational $\delta$ suffices by monotonicity.
• Needed infrastructure: polynomial-time Turing-machine composition, Label Cover with perfect completeness, Fourier analysis on product spaces and junta approximation. Contributions on any of these are welcome.

Selected references

• S. Khanna, N. Linial and S. Safra, On the hardness of approximating the chromatic number, Combinatorica (2000). https://doi.org/10.1007/s004930070013
• V. Guruswami and S. Khanna, On the hardness of 4-coloring a 3-colorable graph, SIAM J. Discrete Math. (2004). https://doi.org/10.1137/S0895480100376794
• I. Dinur, E. Mossel and O. Regev, Conditional hardness for approximate coloring, SIAM J. Comput. (2009). https://doi.org/10.1137/07068062X
• I. Dinur, S. Khot, W. Perkins and M. Safra, Hardness of finding independent sets in almost 3-colorable graphs, FOCS 2010. https://doi.org/10.1109/FOCS.2010.84
• V. Guruswami and S. Sandeep, d-to-1 hardness of coloring 3-colorable graphs with O(1) colors, ICALP 2020. https://doi.org/10.4230/LIPIcs.ICALP.2020.62
• L. Barto, J. Bulín, A. Krokhin and J. Opršal, Algebraic approach to promise constraint satisfaction, J. ACM (2021). https://doi.org/10.1145/3457606
• M. Braverman, S. Khot, N. Lifshitz and D. Minzer, An invariance principle for the multi-slice, with applications, FOCS 2021. https://doi.org/10.1109/FOCS52979.2021.00030
• A. Krokhin, J. Opršal, M. Wrochna and S. Živný, Topology and adjunction in promise constraint satisfaction, SIAM J. Comput. (2023). https://doi.org/10.1137/20M1378223
• N. Bansal, N. Huang and E. Lee, Improved SDP-based algorithm for coloring 3-colorable graphs, 2026. https://arxiv.org/abs/2602.05904v1
• OpenAI, Hardness of finding large independent sets in three-colorable graphs, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026/Hardness-of-finding-large-independent-sets-in-three-colorable-graphs-September-24-2026.pdf

Motivation: the matrix-multiplication exponent

Multiplying two $n\times n$ matrices by the schoolbook method costs about $n^3$ operations. The matrix-multiplication exponent $\omega_F$ of a field $F$ is the infimum of exponents $\tau$ such that $n\times n$ matrices over $F$ can be multiplied with $O(n^{\tau+o(1)})$ additions, subtractions and multiplications. It governs the asymptotic cost of a central bilinear operation and of the many algorithms built from it (determinants, inversion, linear systems). Bounding $\omega$ has driven algebraic complexity theory since 1969. In recent years the bounds have moved in the third and fourth decimal place, with each improvement coming from a finer analysis of the same tensor-power framework.

Background

• 1969 — Strassen's seven-product algorithm gives $\omega\le\log_27$ (Strassen 1969).
• 1980–1987 — Approximate bilinear algorithms (Bini 1980), the asymptotic sum inequality (Schönhage 1981) and the laser method (Strassen 1987).
• 1990 — Coppersmith and Winograd introduce the tensor family $\mathrm{CW}_q$ and progression-free extraction (J. Symbolic Comput. 1990).
• 2010–2014 — Higher tensor powers: Stothers (fourth power; with Davie, Proc. Roy. Soc. Edinburgh 2013), Vassilevska Williams (eighth power, STOC 2012), Le Gall (thirty-second power, ISSAC 2014).
• 2023–2024 — The refined laser method gives $\omega<2.3728596$ (Alman–Vassilevska Williams, TheoretiCS 2024). Asymmetric hashing reduces combination loss (Duan–Wu–Zhou). Finer variable sharing follows (Vassilevska Williams–Xu–Xu–Zhou).
• 2024–2026 — Successive asymmetric compatibility tests (Alman–Duan–Vassilevska Williams–Xu–Xu–Zhou, arXiv:2404.16349). Dupont et al. optimize the eighth-power instance of this framework to $\omega<2.371177$ (arXiv:2608.16884).
• 2026 — An OpenAI preprint, Staggered extraction for exact matrix multiplication over every field (OpenAI Math Release, September 24, 2026), claims $\omega_F<2.371054886006746$ for every fixed field $F$, including every positive characteristic. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Fix a field $F$. An arithmetic program is a straight-line sequence of gates, each a constant from $F$, an input entry, or the sum, difference or product of two earlier gates. Its cost counts the addition, subtraction and multiplication gates. A program multiplies $n\times n$ matrices if designated registers equal the entries of $AB$ for every pair of input matrices $A,B$ over $F$. A real number $\tau$ is admissible if for every $\varepsilon>0$ there is $C>0$ such that for every $n\ge1$ some correct program has cost at most $C\,n^{\tau+\varepsilon}$, and

In Lean this is MatrixAllFields.MatrixMultiplication.Arithmetic.omega F, defined for every F : Type u with [Field F].

Formalization targets

Goal: the exponent bound over every field (Theorem 1.1)

The Lean statement also contains the numerical comparison $2.371054886006746<2.371056$, which carries no mathematical content (the source writes the comparison as $<2.371054887$). This is Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's argument and certificate are correct, the theorem lowers the best stated bound on $\omega$ from $2.371177$ (Dupont et al.) to $2.371055$, and it does so uniformly over all fields, with exact algorithms in every positive characteristic. Any improvement in $\omega$ lowers the exponent of every algorithm reducible to matrix multiplication. The method — pooling directional capacities across extraction depths and staggering lots so that one lot sits at each splitting stage — shows that combination losses in the asymmetric framework can be traded across depths.

Formalizing it. Bounds of this type rest on long chains of tensor-power constructions, recovery arguments and large rational parameter tables, checked in the source by an accompanying verifier with interval certificates for logarithms. A machine-checked proof would certify the whole chain from the arithmetic model to the final rational inequality. It would also give Mathlib the asymptotic sum inequality and Coppersmith–Winograd machinery, which every future bound on $\omega$ needs.

Difficulty

Every recent improvement fights extraction losses. Restricting a tensor power to a direct sum of independent matrix products wastes variables whenever whole blocks must be disjoint, while the final products only need disjoint subsets. Prescribed marginals may also allow several joint distributions. Earlier analyses take the minimum of three directional capacities separately at each depth, so a shortage on one side at one depth is lost. Using capacity across depths requires that variables deleted in earlier extractions (to resolve conflicts or impose type conditions) can still be recovered exactly, over the original field and with only subexponentially many extra copies. Positive characteristic rules out arguments that divide by small integers or rely on characteristic-zero identities.

Formalization scope

• The model is division-free straight-line programs over an arbitrary field F : Type u, with free constants from $F$ and unit cost for add, sub and mul. This matches the source's "scalar additions and multiplications".
• AdmissibleExponent F τ asks, for each $\varepsilon>0$, for one constant $C>0$ that works for every $n\ge1$. omega F is the sInf of the admissible set, which is nonempty (schoolbook algorithm) and bounded below by the output size, so a junk value cannot make the strict inequality true.
• The goal quantifies over every field, including finite fields, so a proof cannot use characteristic-zero arguments or embeddings into $\mathbb C$.
• The second conjunct is a trivially true rational comparison and can be ignored.
• Infrastructure needed: tensor rank and border rank over arbitrary fields, the asymptotic sum inequality, the Coppersmith–Winograd tensor and its powers, method-of-types counting, and verified rational/logarithm interval arithmetic for the parameter certificate. All of this is reusable for other matrix-multiplication results.

Selected references

• V. Strassen, Gaussian elimination is not optimal, Numer. Math. 13 (1969), 354–356. https://doi.org/10.1007/BF02165411
• D. Bini, Relations between exact and approximate bilinear algorithms. Applications, Calcolo 17 (1980), 87–97. https://doi.org/10.1007/BF02575865
• A. Schönhage, Partial and total matrix multiplication, SIAM J. Comput. 10 (1981), 434–455. https://doi.org/10.1137/0210032
• V. Strassen, Relative bilinear complexity and matrix multiplication, J. reine angew. Math. 375/376 (1987), 406–443. https://doi.org/10.1515/crll.1987.375-376.406
• D. Coppersmith and S. Winograd, Matrix multiplication via arithmetic progressions, J. Symbolic Comput. 9 (1990), 251–280. https://doi.org/10.1016/S0747-7171(08)80013-2
• A. M. Davie and A. J. Stothers, Improved bound for complexity of matrix multiplication, Proc. Roy. Soc. Edinburgh Sect. A 143 (2013), 351–369. https://doi.org/10.1017/S0308210511001648
• V. Vassilevska Williams, Multiplying matrices faster than Coppersmith–Winograd, STOC 2012, 887–898. https://doi.org/10.1145/2213977.2214056
• F. Le Gall, Powers of tensors and fast matrix multiplication, ISSAC 2014, 296–303. https://arxiv.org/abs/1401.7714v1
• J. Alman and V. Vassilevska Williams, A refined laser method and faster matrix multiplication, TheoretiCS 3 (2024), Art. 21. https://doi.org/10.46298/theoretics.24.21
• R. Duan, H. Wu and R. Zhou, Faster matrix multiplication via asymmetric hashing, arXiv:2210.10173. https://arxiv.org/abs/2210.10173v5
• V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, New bounds for matrix multiplication: from alpha to omega, arXiv:2307.07970. https://arxiv.org/abs/2307.07970v2
• J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, More asymmetry yields faster matrix multiplication, arXiv:2404.16349v3. https://arxiv.org/abs/2404.16349v3
• E. Dupont et al., Improving the matrix multiplication exponent with modern optimization, arXiv:2608.16884 (2026). https://doi.org/10.48550/arXiv.2608.16884
• OpenAI, Staggered extraction for exact matrix multiplication over every field, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026.pdf

Motivation

In the $k$-server problem, $k$ servers sit at points of a metric space; requests arrive one at a time, and each request must be served by moving some server onto it, at a cost equal to the distance travelled. An online policy sees only the requests revealed so far, and its quality is measured by its competitive ratio: how much more it moves, in expectation, than the offline optimum that knows the whole sequence. The problem was introduced as a common framework for paging, caching and other online service problems, and the question of the best ratio achievable by randomized policies has driven the development of metric embeddings, online primal-dual methods and entropic regularization.

This mission asks for a formal proof that randomized $k$-server has competitive ratio $O(\log^2(k+1))$ on every metric space, 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

• 1988–1990 — Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic lower bound $k$ (STOC 1988; J. Algorithms 1990).
• 1991 — Paging (the uniform metric): Fiat, Karp, Luby, McGeoch, Sleator and Young give the randomized marking algorithm and the harmonic lower bound (J. Algorithms 1991); McGeoch and Sleator attain $H_k$ exactly (Algorithmica 1991). This suggested the randomized $k$-server conjecture, an $O(\log k)$ ratio on every metric.
• 1995 — Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$-competitive (J. ACM 1995).
• 1996–2004 — Probabilistic tree embeddings: Bartal (FOCS 1996) and Fakcharoenphol–Rao–Talwar with distortion $O(\log n)$ (JCSS 2004).
• 2012–2015 — Bansal, Buchbinder and Naor give $O(\log k)$ for weighted paging (J. ACM 2012); Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound $O(\log^2k\log^3n\log\log n)$ on arbitrary finite metrics (J. ACM 2015).
• 2018 — Bubeck, Cohen, Lee, Lee and Mądry achieve $O(\log^2 k)$ on hierarchically separated trees, hence $O(\log^2k\log n)$ on $n$-point metrics (STOC 2018).
• 2023 — Bubeck, Coester and Rabani disprove the randomized $k$-server conjecture: some $(k+1)$-point metrics need ratio $\Omega(\log^2k)$ (STOC 2023).
• 2026 — Coester and Cosson make the tree and finite-metric bounds polynomial-time, with ratio $O(\log n\log^2k)$ on general metrics (ICALP 2026).
• September 2026 — Two OpenAI preprints claim the matching upper bound $O(\log^2(k+1))$ on every metric space (source) and a uniform bit-level implementation on finite rational metrics (source).

Setting

Let $(X,d)$ be a metric space and $s=(s_1,\dots,s_k)\in X^k$ the initial positions of $k$ labelled servers; repeated positions are allowed. To serve a request $r_t$, a policy chooses one label $j$ and moves server $j$ to $r_t$, leaving the others fixed (a server already at $r_t$ may be chosen at zero cost). For a finite request sequence $\sigma$, $\mathrm{cost}_{A,s}(\sigma)$ is the total distance moved and $\mathrm{OPT}_s(\sigma)$ is the minimum of this cost over all label sequences, chosen with knowledge of $\sigma$. A randomized online policy chooses, at each step, a probability distribution over labels as a function of the past requests, its own past choices and the current request. Requests are fixed in advance, independently of the policy's randomness (the oblivious adversary).

Formalization targets

Goal: Theorem 1.1 (p. 2)

There is an absolute constant $C<\infty$ such that for every $k\ge2$, every metric space $(X,d)$ with at least $k+1$ points, and every $s\in X^k$, there are a randomized online policy $A$ and a finite $B\ge0$ with

for every finite request sequence $\sigma$. The same policy serves all sequences and horizons; $B$ may depend on $(X,d)$, $k$ and $s$ but not on $\sigma$; and $B=0$ when the entries of $s$ are distinct.

Significance

The result itself. Combined with the Bubeck–Coester–Rabani lower bound, it identifies $\Theta(\log^2 k)$ as the worst-case order of the randomized competitive ratio over all metrics. The bound has no dependence on the number of points, the aspect ratio, finiteness or boundedness of $X$, removing the $\log n$ factor left by static tree embeddings. No computational efficiency is claimed; a companion preprint turns the existence statement into a uniform algorithm on finite rational metrics.

Formalizing it. The statement is elementary to state, but its proof combines a rank-based allocation on separated trees, slowly varying simplex trackers, a compact potential for partition edits, online partitions with an embedded comparator, balanced rounding, and a compactness argument (Tychonoff) producing one policy for all finite inputs. None of these online-algorithm tools exist in a formal library, and a machine-checked competitive analysis of a randomized $k$-server algorithm on general metrics is not known.

Difficulty

Embedding the metric into a random hierarchically separated tree and running an $O(\log^2k)$ tree algorithm loses the embedding distortion, which is $\Theta(\log n)$ in the worst case and is not bounded in terms of $k$. Removing it requires changing the tree as requests arrive, and the cost of re-partitioning must be paid for. A previous dynamic approach (Lee's fusible HSTs) had its general claim withdrawn after a gap in that accounting (p. 3). In the preprint, the partition schedule is driven by the posterior measure of a hidden comparator, and the edit costs and the travel of parked mass are bounded separately (Sections 7–8). Passing from finite metrics and finite horizons to one policy on an arbitrary, possibly infinite and unbounded, space with a fixed constant requires a further compactness step (Section 10).

Formalization scope

• X : Type u carries an arbitrary MetricSpace instance; "at least $k+1$ points" is an injection Fin (k+1) → X. No finiteness, separability or boundedness is assumed.
• A Policy k X maps the history (list of past requests with the labels used) and the current request to a LabelDistribution k, i.e. a probability vector on Fin k. Every step moves exactly one server (Function.update), as in the source.
• expectedCost is the finite sum over all label sequences of the path probability times the service cost; optimalCost is the sInf over all label sequences of the service cost (nonempty finite set, so the infimum is a minimum). Restricting the offline optimum to one-server-per-request service does not change it (triangle inequality).
• The constant $C>0$ is chosen before $k$, $X$ and $s$; the policy and $B\ge0$ are chosen after $s$ and before the request list; Function.Injective s → B = 0 encodes the distinct-start clause.
• Logarithms are natural (Real.log).

Selected references

• OpenAI, Squared-logarithmic randomized k-server on arbitrary metrics, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf
• OpenAI, Uniform computation of the squared-logarithmic k-server bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf
• J. R. Lee, Fusible HSTs and the randomized k-server conjecture, FOCS 2018. https://doi.org/10.1109/FOCS.2018.00049
• A. Tychonoff, Über einen Funktionenraum, Math. Ann. 111 (1935). https://doi.org/10.1007/BF01472255
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). https://doi.org/10.1016/0196-6774(90)90003-W
• E. Koutsoupias, C. H. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). https://doi.org/10.1145/210118.210128
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12 (1991). https://doi.org/10.1016/0196-6774(91)90041-V
• N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A polylogarithmic-competitive algorithm for the k-server problem, J. ACM 62 (2015). https://doi.org/10.1145/2783434
• S. Bubeck, M. B. Cohen, J. R. Lee, Y. T. Lee, A. Mądry, k-server via multiscale entropic regularization, STOC 2018. https://doi.org/10.1145/3188745.3188798
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. https://doi.org/10.1145/3564246.3585132
• C. Coester, R. Cosson, Randomized k-server in polynomial time, ICALP 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.65
• J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, JCSS 69 (2004). https://doi.org/10.1016/j.jcss.2004.04.011

Motivation

In the $k$-server problem, $k$ labelled servers occupy points of a metric space, requests arrive online, and each request is served by moving one server onto it; the cost is the total distance moved, compared with the offline optimum through the competitive ratio. A companion OpenAI preprint claims that on every metric there exists a randomized policy with ratio $O(\log^2(k+1))$ against oblivious requests, matching the known worst-case lower bound. That result is an existence statement: it gives no procedure for computing the policy's probabilities.

This mission asks whether the bound can be realized by one uniform algorithm with explicit bit complexity on all 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

• 1988–1990 — Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic lower bound $k$ (STOC 1988; J. Algorithms 1990).
• 1991 — Paging (the uniform metric): Fiat, Karp, Luby, McGeoch, Sleator and Young give the randomized marking algorithm and the harmonic lower bound (J. Algorithms 1991); McGeoch and Sleator attain $H_k$ exactly (Algorithmica 1991). This suggested the randomized $k$-server conjecture, an $O(\log k)$ ratio on every metric.
• 1995 — Koutsoupias and Papadimitriou prove that the work function algorithm is $(2k-1)$-competitive (J. ACM 1995).
• 1996–2004 — Probabilistic tree embeddings: Bartal (FOCS 1996) and Fakcharoenphol–Rao–Talwar with distortion $O(\log n)$ (JCSS 2004).
• 2012–2015 — Bansal, Buchbinder and Naor give $O(\log k)$ for weighted paging (J. ACM 2012); Bansal, Buchbinder, Mądry and Naor give the first polylogarithmic bound $O(\log^2k\log^3n\log\log n)$ on arbitrary finite metrics (J. ACM 2015).
• 2018 — Bubeck, Cohen, Lee, Lee and Mądry achieve $O(\log^2 k)$ on hierarchically separated trees, hence $O(\log^2k\log n)$ on $n$-point metrics (STOC 2018).
• 2023 — Bubeck, Coester and Rabani disprove the randomized $k$-server conjecture: some $(k+1)$-point metrics need ratio $\Omega(\log^2k)$ (STOC 2023).
• 2026 — Coester and Cosson make the tree and finite-metric bounds polynomial-time, with ratio $O(\log n\log^2k)$ on general metrics (ICALP 2026).
• September 2026 — Two OpenAI preprints claim the matching upper bound $O(\log^2(k+1))$ on every metric space (source) and a uniform bit-level implementation on finite rational metrics (source).

Setting

Fix $n\ge3$ and $2\le k<n$. A rational metric on $X=\{1,\dots,n\}$ is a table $d(x,y)\in\mathbb Q$ that is nonnegative, zero exactly on the diagonal, symmetric, and satisfies the triangle inequality. An initial labelled tuple $s\in X^k$ may have repetitions. For a request word $\sigma$, $\mathrm{cost}_{A,s}(\sigma)$ is the algorithm's total movement and $\mathrm{OPT}_s(\sigma)$ the minimum over all choices of serving labels with knowledge of $\sigma$. $L$ denotes the total binary length of the encoding of $(n,k,d,s)$.

The computational model is a bit machine: a finite control with an input tape, finitely many work tapes over $\{0,1,\text{blank}\}$, an output channel, and one fresh unbiased random bit per step. At each request the input tape is replaced by the encoded request, the internal state is retained, and the output after the step budget names the server to move.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There are an absolute constant $C$ and a polynomial $p$ such that a single uniform randomized online algorithm, on every instance $(n,k,d,s)$ as above,

• preprocesses the instance in at most $p(L)$ bit operations;
• serves request $r_t$, for every reachable history and internal state, in at most $p\bigl(L+\lceil\log_2(t+1)\rceil\bigr)$ further bit operations, outputting a valid server label and moving exactly that server;
• for every fixed finite request sequence $\sigma$ independent of its random bits satisfies

with $B_{d,k,s}<\infty$ independent of $\sigma$ and of its length.

Significance

The result itself. It converts the existence theorem into an algorithm whose ratio is independent of $n$, using only unbiased random bits and polynomial work per request in the input length and the bit length of the request counter. The price is an additive constant $B_{d,k,s}$ with no size bound: the algorithm may serve a very long initial stretch with a fixed label while its constructor runs. Coester and Cosson obtain stronger time and randomness guarantees but with ratio $O(\log n\log^2k)$ on general metrics; the two results are incomparable.

Formalizing it. The goal is stated in an explicit machine model, so a formal proof certifies both the competitive bound and the bit-complexity bound. It needs the companion existence theorem (Theorem 2.1 here, p. 4) as an input; a full development therefore also requires formalizing that theorem or taking it as a separate milestone. Exact rational linear algebra (Fourier–Motzkin elimination), dyadic rounding of probabilities, and step-counted machine simulation are reusable.

Difficulty

Knowing that a good policy exists does not give its probabilities, and a finite horizon alone does not control a long input on which the optimum barely moves. The preprint (pp. 3–4) solves a rational linear system for each horizon, then filters requests so that only those missed by some strongly lazy service with bounded moves are retained, which bounds the retained word length; a marking fallback pays for trajectories exceeding the move cap. The constructor's running time is uncontrolled, so the algorithm simulates it for only $\lfloor\log_2(t+1)\rfloor$ steps at request $t$ (Proposition 4.2, p. 14), and the delayed activation is absorbed into $B_{d,k,s}$.

Formalization scope

• RationalMetric n is a Fin n → Fin n → ℚ table with the metric axioms; configurations are Fin k → Fin n; offlineCost is the sInf over label histories matching the request word (a finite, nonempty set of costs).
• BitMachine has finitely many controls and tapes and a transition consuming one coin per step. Preprocessing (boot) runs $c(L+1)^e$ steps with all coins $0$, so it is deterministic; this is satisfied by the source's deterministic constructor, and Theorem 1.1 does not require randomness there.
• Each request runs exactly requestBudget c e L t $=c(L+\lceil\log_2(t+1)\rceil+1)^e$ steps (Nat.clog 2 (t+1)) and must have yielded with output value $<k$ for every reachable state and every coin string; requests are encoded by a fixed self-delimiting binary code.
• machineExpectedCost averages over all coin strings of the step budget, i.e. uniformly random bits; the bound is required for every request list w, with $B\ge0$ chosen after $(d,s)$ and before w.
• The machine, the polynomial $(c,e)$ and $C$ are fixed before $n$, $k$, $d$, $s$: the algorithm is uniform.

Selected references

• OpenAI, Uniform computation of the squared-logarithmic k-server bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026/Uniform-computation-of-the-squared-logarithmic-k-server-bound-September-24-2026.pdf
• OpenAI, Squared-logarithmic randomized k-server on arbitrary metrics, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026/Squared-logarithmic-randomized-k-server-on-arbitrary-metrics-September-24-2026.pdf
• D. Komm, R. Královič, R. Královič, T. Mömke, Randomized online computation with high probability guarantees, Algorithmica (2022). https://doi.org/10.1007/s00453-022-00925-z
• G. B. Dantzig, B. C. Eaves, Fourier–Motzkin elimination and its dual, J. Combin. Theory Ser. A 14 (1973). https://doi.org/10.1016/0097-3165(73)90004-6
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). https://doi.org/10.1016/0196-6774(90)90003-W
• E. Koutsoupias, C. H. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). https://doi.org/10.1145/210118.210128
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12 (1991). https://doi.org/10.1016/0196-6774(91)90041-V
• N. Bansal, N. Buchbinder, A. Mądry, J. Naor, A polylogarithmic-competitive algorithm for the k-server problem, J. ACM 62 (2015). https://doi.org/10.1145/2783434
• S. Bubeck, M. B. Cohen, J. R. Lee, Y. T. Lee, A. Mądry, k-server via multiscale entropic regularization, STOC 2018. https://doi.org/10.1145/3188745.3188798
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. https://doi.org/10.1145/3564246.3585132
• C. Coester, R. Cosson, Randomized k-server in polynomial time, ICALP 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.65
• J. Fakcharoenphol, S. Rao, K. Talwar, A tight bound on approximating arbitrary metrics by tree metrics, JCSS 69 (2004). https://doi.org/10.1016/j.jcss.2004.04.011

Motivation

Proving that explicit Boolean functions need large circuits is the central problem of circuit complexity. Even for very shallow circuits the known bounds are far from what counting arguments suggest. A depth-three OR–AND–OR circuit is an OR of CNFs, with unbounded fan-in and arbitrary sharing; most functions need $2^{\Omega(n)}$ gates in this model, yet for every explicit function in P the best known lower bounds had the form $2^{c\sqrt n}$ for a constant $c$. Håstad's switching lemma gave $2^{\Omega(\sqrt n)}$ for parity (1989), and Paturi, Pudlák and Zane showed this is tight for parity up to a constant factor (1999), so parity cannot go further. Moving the exponent beyond any constant multiple of $\sqrt n$ for an explicit language was identified as an open problem in the depth-three literature (Gurumukhani, Paturi, Pudlák, Saks and Talebanfard, CCC 2024; Gurumukhani, Kleber, Paturi, Rosin and Talebanfard, CCC 2026). Depth-three lower bounds are also tied to satisfiability algorithms and to Valiant's approach to lower bounds for logarithmic-depth circuits.

This mission asks for a formal proof that one polynomial-time language requires $2^{\omega(\sqrt n)}$ depth-three gates, as stated in an OpenAI preprint dated September 23, 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

• 1989 — Håstad's switching lemma yields $2^{\Omega(\sqrt n)}$ depth-three lower bounds for parity (Almost optimal lower bounds for small depth circuits, Adv. Comput. Res. 5, 1989).
• 1995 — Håstad, Jukna and Pudlák's top-down method improves the constants for parity and majority (Comput. Complexity 1995) and asks for $2^{n^{1/2+\varepsilon}}$.
• 1999–2000 — Paturi, Pudlák and Zane prove the sharp parity bound via the satisfiability coding lemma (Chicago J. TCS 1999); Paturi, Saks and Zane prove $2^{n-o(n)}$ bounds for bottom fan-in two (Comput. Complexity 2000).
• 2001 — Impagliazzo, Paturi and Zane's sunflower sparsification (JCSS 2001).
• 2005 — Paturi, Pudlák, Saks and Zane's code-membership bound with exponent $(\pi/\sqrt6)\sqrt n$ (JACM 2005).
• 2024–2026 — Local enumeration and bottom-fan-in-three bounds (CCC 2024); optimal depth-three circuits for inner product (CCC 2026).
• September 2026 — The OpenAI preprint claims a polynomial-time language with $S_3(f_n)=2^{\omega(\sqrt n)}$ (Theorem 1.1, p. 1).

Setting

A literal is a variable $x_i$ or its negation; negations are free. A depth-three OR–AND–OR circuit on $n$ inputs has bottom OR gates (clauses) reading literals and optional constants, middle AND gates reading bottom gates, and one top OR gate reading middle gates. Fan-in and fan-out are unbounded and gates may be shared. Its size counts every bottom gate, every middle gate and the output gate. For $f:\{0,1\}^n\to\{0,1\}$, $S_3(f)$ is the least size of such a circuit computing $f$ exactly. For a language $L\subseteq\{0,1\}^*$, $f_n$ is its membership function on $\{0,1\}^n$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There are a language $L\subseteq\{0,1\}^*$, a deterministic multi-tape Turing machine deciding $L$, and positive integers $C,a$ such that the machine halts within $C(n+1)^a$ steps on every input of length $n$, and for every real $A>0$ there is $N_A$ with

The language and machine are fixed before $A$; no uniformity or bottom fan-in restriction is imposed on the circuits.

Significance

The result itself. It is the first explicit depth-three lower bound whose exponent is not $O(\sqrt n)$, crossing the barrier at which parity, majority and the earlier code-membership functions stop. It is weaker than the $2^{n^{1/2+\varepsilon}}$ bound asked by Håstad, Jukna and Pudlák and gives no fixed improvement of the exponent's power. Because every function has a single-CNF representation when bottom fan-in is unbounded, the result depends on counting all gates, as stated.

Formalizing it. Circuit lower bounds are combinatorial statements well suited to formal proof, but the libraries are thin: a complete development needs a Turing-machine time bound for a concrete polynomial-evaluation language, restriction arguments for CNFs, the Erdős–Rado sunflower lemma, and limited-independence estimates from hashing and polynomial interpolation. All of these are reusable in complexity theory. No machine-checked depth-three lower bound beyond small cases is known.

Difficulty

The classical switching lemma changes the normal form and loses a constant in the exponent, which keeps bounds at the $c\sqrt n$ scale, and parity is provably no harder than $2^{O(\sqrt n)}$, so a different hard function and a different argument are needed. The preprint needs a function whose sign has small correlation with every moderately wide CNF, independently of the number of clauses. Its key step (Lemma 3.1, p. 4) expresses each randomly restricted width-$k$ CNF as a signed combination of width-$b$ CNFs with expected coefficient mass at most two, with no dependence on the clause count. A uniform polynomial-time language cannot search for a hard function at each length, so hardness must come from inputs that carry the parameters selecting a hard slice (Section 5).

Formalization scope

• Circuit3 (Fin n) has bottomCount raw clauses (lists of literals or Boolean constants), middleCount AND gates given as Finsets of bottom indices, and a top Finset of middle indices; gateCount = bottomCount + middleCount + 1. Computes requires exact agreement with L (List.ofFn x) on every input.
• The machine model FiniteMultiTapeMachine has finitely many tapes, a finite alphabet, finite states, an input tape initialized with the input, and an accept predicate on the halting state. MultiTapeHaltsIn M w (L w) (C*(|w|+1)^a) requires halting within the bound with output L w.
• The order of quantifiers is $\exists L, M, C, a$ before $\forall A>0\ \exists N\ \forall n\ge N\ \forall$ circuits, with a strict inequality $2^{A\sqrt n}<\mathrm{gateCount}$ in ℝ.
• The statement is not vacuous: circuits exist for every function, so the claim is a genuine lower bound on all of them.

Selected references

• OpenAI, Beyond the Square-Root Exponent for Depth-Three Boolean Circuits, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026/main.pdf
• J. Håstad, Almost optimal lower bounds for small depth circuits, Randomness and Computation, Adv. Comput. Res. 5 (1989), 143–170.
• J. Håstad, S. Jukna, P. Pudlák, Top-down lower bounds for depth-three circuits, Comput. Complexity 5 (1995), 99–112. https://doi.org/10.1007/BF01268140
• R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma, Chicago J. Theor. Comput. Sci. (1999), Article 11.
• R. Paturi, M. E. Saks, F. Zane, Exponential lower bounds for depth three Boolean circuits, Comput. Complexity 9 (2000), 1–15. https://doi.org/10.1007/PL00001598
• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?, J. Comput. Syst. Sci. 63 (2001), 512–530. https://doi.org/10.1006/jcss.2001.1774
• R. Paturi, P. Pudlák, M. E. Saks, F. Zane, An improved exponential-time algorithm for k-SAT, J. ACM 52 (2005), 337–364. https://doi.org/10.1145/1066100.1066101
• M. Gurumukhani, R. Paturi, P. Pudlák, M. Saks, N. Talebanfard, Local enumeration and majority lower bounds, CCC 2024. https://doi.org/10.4230/LIPIcs.CCC.2024.17
• M. Gurumukhani, D. Kleber, R. Paturi, C. Rosin, N. Talebanfard, Optimal depth-three circuits for inner product, CCC 2026. https://doi.org/10.4230/LIPIcs.CCC.2026.27
• H. Dell, T. Husfeldt, D. Marx, N. Taslaman, M. Wahlén, Exponential time complexity of the permanent and the Tutte polynomial, ACM Trans. Algorithms 10 (2014). https://doi.org/10.1145/2635812
• P. Erdős, R. Rado, Intersection theorems for systems of sets, J. London Math. Soc. (1960). https://doi.org/10.1112/jlms/s1-35.1.85

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

(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;

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

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

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

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

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

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