Graph Theory

Motivation

A vertex cover of a hypergraph is a set of vertices meeting every edge; the covering number $\tau(H)$ is the minimum size of a cover, and the matching number $\nu(H)$ is the maximum number of pairwise disjoint edges. An $r$-partite $r$-uniform hypergraph has $r$ disjoint vertex parts, and every edge takes exactly one vertex from each part. Ryser's covering conjecture asserts that every such hypergraph satisfies

$$\tau(H)\le(r-1)\,\nu(H).$$

For $r=2$ this is Kőnig's theorem for bipartite graphs, so the conjecture is a proposed higher-dimensional Kőnig theorem. Its intersecting case ($\nu=1$, bound $r-1$) is equivalent to Gyárfás's conjecture that every $r$-edge-coloured complete graph can be covered by $r-1$ monochromatic trees, which connects it to Ramsey-type covering problems.

Timeline

• 1971. Henderson's thesis contains an equivalent formulation of the conjecture (doi:10.7907/J1Z1-SK19); Best and Wanless discuss its attribution to Ryser (arXiv:1801.02893).
• 1983. Tuza proves the intersecting case for $r=5$; Gyárfás had handled $r\le4$ (historical account in Király–Tóthmérész, doi:10.37236/6448).
• 1991. Erdős, Gyárfás and Pyber record the equivalence with the monochromatic tree-cover formulation (doi:10.1016/0095-8956(91)90007-7).
• 2001. Aharoni proves the full case $r=3$ (doi:10.1007/s004930170001).
• 2012. Haxell and Scott prove $\tau\le(r-\varepsilon_r)\nu$ for $r=4,5$ (doi:10.37236/1175).
• 2017. Francetić, Herke, McKay and Wanless verify the linear intersecting case through rank nine (doi:10.1016/j.ejc.2016.10.004); Haxell and Scott construct intersecting examples with $\tau\ge r-4$ (doi:10.37236/6460).
• 2019. Abu-Khazneh, Barát, Pokrovskiy and Szabó construct intersecting $(q+2)$-partite hypergraphs with $\tau=q+1$, matching the conjectured bound, for prime powers $q$ (doi:10.1016/j.jcta.2018.07.011).
• 2025–2026. Clow, Haxell and Mohar disprove Lovász's stronger deletion conjecture at $r=3$ (doi:10.1007/s00493-026-00220-3); those examples do not contradict Ryser's bound.

The source of this mission, an OpenAI preprint dated September 27, 2026, claims counterexamples to the conjecture itself, already in the intersecting case and with all parts of equal size.

Setting

Fix $r=q+1$. A $(q+1)$-partite $(q+1)$-uniform hypergraph on parts $V_1,\dots,V_{q+1}$ is given by its edge set, each edge choosing one vertex in every part. It is intersecting if it has at least one edge and any two edges share a vertex (necessarily in the same part). A vertex is nonisolated if it lies in some edge. For an intersecting hypergraph $\nu(H)=1$, so Ryser's conjecture predicts $\tau(H)\le q$.

The natural extremal example comes from the affine plane $\mathbb F_q^2$: one part per direction, one vertex per line, one edge per point. It is intersecting with $\tau=q$, attaining the conjectured bound.

Formalization targets

Goal: Theorem 1.1

There is $q_0$ such that for every prime $q\ge q_0$ there exists a finite intersecting $(q+1)$-partite $(q+1)$-uniform hypergraph $H$ with

$$|V_1|=\dots=|V_{q+1}|=q+1,\qquad \tau(H)=q+1,$$

and every vertex lies in an edge. Lean: OAI.Balanced.main_result, open on the platform.

Significance

Since $\nu(H)=1$ and $\tau(H)=q+1>q=r-1$, the theorem would disprove Ryser's conjecture for infinitely many $r$, in its intersecting case. The value $\tau=r$ is the largest possible for an intersecting $r$-uniform hypergraph (any edge is a cover), and the part sizes $q+1$ are the smallest compatible with $\tau=r$, so the examples are extremal in both respects. Via the standard transfer (Corollary 1.2) they also disprove Gyárfás's tree-cover conjecture for $r=q+1$ colours. The threshold $q_0$ is not explicit. A companion preprint of the same family gives counterexamples over extension fields without balance. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

The affine-plane example sits exactly at the conjectured bound, and its minimum covers are rigid (parallel classes). Raising $\tau$ by one requires adding edges that destroy every $q$-element cover while keeping the hypergraph intersecting and keeping only $q+1$ vertices per part; adding a new part, as Abu-Khazneh et al. did, changes $r$ and only reaches equality. Verifying that no cover of size $q$ survives requires controlling all small sets of lines, which the paper does with stability results for line covers in prime-order planes and a probabilistic selection.

Formalization scope

• PartiteHypergraph r n has vertex set Fin r × Fin n and edges a Finset (Fin r → Fin n); an edge $e$ contains the vertices $(i,e(i))$.
• Intersecting: edges nonempty and any two edges agree in some coordinate. Nonisolated: every $(i,v)$ lies in some edge. HasCoverNumber H k: some cover has exactly $k$ vertices and every cover has at least $k$.
• MainResult: ∃ q₀, ∀ q ≥ q₀, q.Prime → ∃ H : PartiteHypergraph (q+1) (q+1), Intersecting ∧ Nonisolated ∧ HasCoverNumber (q+1).
• Finite fields of prime order are available in Mathlib as ZMod q.

Contributions formalizing the deterministic reduction (Proposition 2.1), the stability of affine line covers (Lemma 3.3, building on Szőnyi–Weiner), or the selection step (Proposition 5.1) are welcome, as is the monochromatic tree-cover corollary.

Selected references

• OpenAI, Balanced counterexamples to Ryser's conjecture at prime orders, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Balanced-Counterexamples-to-Rysers-Conjecture-at-Prime-Orders-September-27-2026/paper.pdf
• J. R. Henderson, Permutation decompositions of (0,1)-matrices and decomposition transversals, PhD thesis, Caltech, 1971. https://doi.org/10.7907/J1Z1-SK19
• R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica, 2001. https://doi.org/10.1007/s004930170001
• P. Haxell, A. Scott, On Ryser's conjecture, Electron. J. Combin., 2012. https://doi.org/10.37236/1175
• N. Francetić, S. Herke, B. D. McKay, I. M. Wanless, On Ryser's conjecture for linear intersecting multipartite hypergraphs, European J. Combin., 2017. https://doi.org/10.1016/j.ejc.2016.10.004
• A. Abu-Khazneh, J. Barát, A. Pokrovskiy, T. Szabó, A family of extremal hypergraphs for Ryser's conjecture, J. Combin. Theory Ser. A, 2019. https://doi.org/10.1016/j.jcta.2018.07.011
• P. Erdős, A. Gyárfás, L. Pyber, Vertex coverings by monochromatic cycles and trees, J. Combin. Theory Ser. B, 1991. https://doi.org/10.1016/0095-8956(91)90007-7
• Z. Király, L. Tóthmérész, On Ryser's conjecture for t-intersecting and degree-bounded hypergraphs, Electron. J. Combin., 2017. https://doi.org/10.37236/6448

Motivation

Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex $k$-tuples. For every fixed dimension $k$ this is a polynomial-time procedure, with running time $n^{O(k)}$. When $k$ is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.

This preprint answers that question for the joint-update convention: deciding $k$-WL equivalence of two explicit graphs with $k$ in binary is EXPTIME-complete, even on connected graphs of maximum degree three.

Background

• 1968. Weisfeiler and Leman introduce the refinement method.
• 1982. Luks shows isomorphism of graphs of bounded degree is decidable in polynomial time.
• 1992. Cai, Fürer and Immerman construct degree-three graphs with small color classes that remain indistinguishable with linearly many counting variables.
• 2019. Kiefer and Neuen record the joint-update convention and its bijective $(k+1)$-pebble game characterization.
• 2024–2025. Seppelt, and independently Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence with the dimension as input. Grohe, Lichter, Neuen and Schweitzer compress CFI graphs to obtain long refinement sequences.
• 2026. The OpenAI preprint Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs (dated September 25, 2026) proves EXPTIME-completeness; companion preprints treat identification and fixed-dimension time lower bounds. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a $k$-tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices $z$, of the vector of $k$ old colors obtained by replacing each coordinate in turn by $z$. Color names are common to both graphs, and $G \equiv_k H$ means their $k$-tuple color histograms agree at every round.

The language $\mathrm{WL}$ consists of encodings $(G, H, k)$ with $k \ge 2$ in binary and $G \equiv_k H$. The language $\mathrm{SubWL}$ additionally requires $G$ and $H$ to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.

In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of $k$, and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.

Formalization targets

Goal: Theorem 1.1

Both $\mathrm{WL}$ and $\mathrm{SubWL}$ are EXPTIME-complete under deterministic polynomial-time many-one reductions:

$$\mathrm{WL},\ \mathrm{SubWL} \in \mathrm{EXPTIME}, \qquad L \le_p \mathrm{WL} \text{ and } L \le_p \mathrm{SubWL} \text{ for every } L \in \mathrm{EXPTIME}.$$

Significance

The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with $k$ in unary.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.

Difficulty

Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since $k$ may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.

Formalization scope

• Graphs: SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.
• Equivalence quantifies over all rounds $s$; colors are nested Multiset types.
• Dimension $k \ge 2$ is encoded in binary after a unary length header.
• The Turing machine model is explicit; EXPTIME bounds are $2^{c(n+1)^d}$ and reductions run in $c(n+1)^d$ steps.

The statement is not trivial: both membership and hardness are required for both languages.

Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.

Selected references

• OpenAI, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf
• OpenAI, The complexity of identifying a graph by Weisfeiler–Leman refinement, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/main/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• E. M. Luks, Isomorphism of Graphs of Bounded Valence Can Be Tested in Polynomial Time, J. Comput. Syst. Sci. 25 (1982). https://doi.org/10.1016/0022-0000(82)90009-5
• S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978

Motivation

The Weisfeiler–Leman (WL) method colors $k$-tuples of vertices by repeatedly recording their local extension patterns; two graphs are $k$-WL equivalent when the stable color histograms agree. For each fixed $k$ the direct algorithm runs in time $n^{O(k)}$: there are $n^k$ tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.

This preprint proves that it is, unconditionally: for every sufficiently large fixed $k$, every deterministic sequential decider for $k$-WL equivalence needs time $n^{ck}$ at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.

Background

• 1966. Hennie and Stearns use padded machine indices and clocked self-simulation in their time-hierarchy proof.
• 1968. Weisfeiler and Leman introduce the refinement method.
• 1992. Cai, Fürer and Immerman's parity constructions establish limits of bounded-variable graph identification.
• 1996. Hella introduces the bijective pebble game characterizing counting-logic equivalence.
• 1999. Grohe proves equivalence in finite-variable logics is complete for polynomial time.
• 2013. Berkholz proves unconditional time lower bounds with exponent linear in the number of pebbles for existential pebble games.
• 2024–2025. Seppelt, and Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence when the dimension is part of the input. Grohe, Lichter, Neuen and Schweitzer prove $\Omega_k(n^{k/2})$ lower bounds on the number of refinement rounds via compressed CFI graphs; such bounds do not constrain other algorithms deciding the equivalence.
• 2026. The OpenAI preprint Unconditional time lower bounds for Weisfeiler–Leman equivalence (dated September 25, 2026) proves the bound stated below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given as $n \times n$ adjacency matrices. For a $k$-tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices $z$ of the $k$-vectors of colors obtained by replacing each coordinate by $z$; in the separate convention, one such multiset per coordinate. Two $n$-vertex graphs are $k$-WL equivalent if their color histograms agree at every round.

A decider for a convention and dimension $k$ is a deterministic machine that halts on every encoded pair of $n$-vertex graphs and accepts exactly the equivalent pairs. Its worst-case time $T_A(n)$ is the maximum running time over pairs of $n$-vertex graphs (optionally restricted to connected graphs of diameter at most two).

In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes $n$ and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.

Formalization targets

Goal: Theorem 1.1

There are absolute constants $c > 0$ and $k_0$ such that for every fixed $k \ge k_0$, either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider $A$ in either machine model, there is $n_0 = n_0(A, k)$ with

$$T_A(n) \ge n^{ck} \qquad \text{for every } n \ge n_0 .$$

The exponent constant $c$ is independent of $k$ and of the program; the threshold $n_0$ may depend on both. The bound holds at every large order, not only infinitely often.

Significance

The result. Theorem 1.1 rules out any running time $f(k)\,n^{g(k)}$ with $g(k) = o(k)$, unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).

Difficulty

Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in $k$. A polynomial-time computation with exponent proportional to $k$ has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.

Formalization scope

• Decides A c k p requires halting and correctness on every pair in the input class at every order $n$; worstTime is a Finset.sup over pairs in the class.
• Diameter two includes $n > 0$ and every pair of vertices equal, adjacent, or with a common neighbour (hence connected).
• Turing machines have finitely many tapes, states and symbols; RAM words have $O(\log(n+2))$ bits, and RAM instructions are fixed finite programs whose word operations carry a polynomial-time implementation.
• Time is a natural number; the bound $n^{ck}$ is compared in ℝ.

The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.

Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.

Selected references

• OpenAI, Unconditional time lower bounds for Weisfeiler–Leman equivalence, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• L. Hella, Logical Hierarchies in PTIME, Information and Computation 129 (1996). https://doi.org/10.1006/inco.1996.0070
• F. C. Hennie, R. E. Stearns, Two-Tape Simulation of Multitape Turing Machines, J. ACM 13 (1966). https://doi.org/10.1145/321356.321362
• C. Berkholz, Lower Bounds for Existential Pebble Games and k-Consistency Tests, Logical Methods in Computer Science 9 (2013).
• M. Grohe, Equivalence in Finite-Variable Logics Is Complete for Polynomial Time, Combinatorica 19 (1999). https://doi.org/10.1007/s004939970004
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, arXiv:2402.11531, 2024. https://arxiv.org/abs/2402.11531
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.

Motivation

The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension $k$ controls how much tuple information is used. A graph's Weisfeiler–Leman dimension $\mathrm{WLdim}(G)$ is the least $k$ for which $k$-WL refinement identifies $G$, i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the descriptive complexity of an individual graph, tied to counting logics and pebble games. The question here is how hard it is to compute: given $G$ and $k$, decide whether $\mathrm{WLdim}(G) \le k$.

Identification differs from testing whether a given pair of graphs is equivalent: it quantifies over every possible comparison graph. The preprint shows the problem is EXPTIME-complete when $k$ is part of the input.

Background

• 1968. Weisfeiler and Leman introduce the refinement method.
• 1992. Cai, Fürer and Immerman relate WL to counting logic and pebble games and construct parity graphs needing linear dimension.
• 2017. Arvind, Köbler, Rattan and Verbitsky prove P-hardness of identification by color refinement (dimension one).
• 2019. Kiefer and Neuen give a game formulation used to analyze WL decompositions.
• 2024. Seppelt proves coNP-hardness of variable-dimension pair equivalence.
• 2025. Lichter, Raßmann and Schweitzer prove P-hardness of identification for each fixed $k \ge 2$ and NP-hardness when the dimension is part of the input, including on simple uncolored graphs; they also prove coNP-hardness of pair equivalence independently. Grohe, Lichter, Neuen and Schweitzer introduce compressed CFI graphs for round lower bounds.
• 2026. The OpenAI preprint The complexity of identifying a graph by Weisfeiler–Leman refinement (dated September 25, 2026) proves EXPTIME-completeness, building on the companion preprint on variable-dimension WL equivalence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

All graphs are finite, simple, undirected and uncolored. For $k \ge 2$ the joint-update convention is used: a $k$-tuple starts with its equality and adjacency type, and each round adjoins the multiset over vertices $z$ of the vector of colors obtained by replacing each coordinate by $z$. For $k = 1$ ordinary color refinement is used. Colors are shared between graphs. $G \equiv_k H$ means the tuple-color histograms agree at every round. $k$-WL identifies $G$ if $G \equiv_k H$ implies $G \cong H$ for every graph $H$, and $\mathrm{WLdim}(G)$ is the least positive such $k$.

The decision problem takes a nonempty graph $G$ by its adjacency matrix and a positive integer $k$ in binary, and asks whether $\mathrm{WLdim}(G) \le k$; malformed inputs are rejected.

In Lean (OAI.WLIdentification), Graph is an order with a symmetric loopless Boolean adjacency on Fin order; Equivalent, Identifies and WLdim follow the definitions above; inputs are bit words consisting of a unary order header, the row-major matrix and the binary dimension; complexity classes are defined from an explicit deterministic single-tape Turing machine model (Machine, run, DecidesWithin, InEXPTIME, PolytimeManyOne, EXPTIMEComplete).

Formalization targets

Goal: Theorem 1.1

The language

$$\{\langle G, k\rangle : G \text{ nonempty},\ k \ge 1,\ \mathrm{WLdim}(G) \le k\}$$

is EXPTIME-complete under deterministic polynomial-time many-one reductions: it is decidable in time $2^{C(n+1)^d}$, and every EXPTIME language reduces to it in polynomial time.

Significance

The result. Theorem 1.1 settles the complexity of the input-dimension identification problem, strengthening the NP-hardness of Lichter, Raßmann and Schweitzer to EXPTIME-completeness. By Corollary 7.3 hardness persists with $k$ in unary, so it does not come from exponentially large numerical dimensions.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formal proof would include a verified reduction from arbitrary exponential-time Turing machine computations to graphs, and a verified upper bound for WL identification. The Turing-machine model and the WL definitions in the Lean statement are reusable for the companion missions on WL equivalence.

Difficulty

Hardness must handle the all-mates quantifier: an encoding of a computation into a graph must ensure that every graph $H$ that is $k$-WL equivalent to it is isomorphic to it exactly when the computation accepts. Local recognition of gadgets, as in earlier NP-hardness proofs, shows each incidence piece of $H$ has an allowed pattern, but the encoding here admits a whole family of shifted constraints, and one must show every shift arising from an equivalent mate lifts to a single global isomorphism on accepting instances. Membership in EXPTIME is also not immediate, since identification quantifies over infinitely many comparison graphs.

Formalization scope

• Graphs are Fin n-indexed Boolean adjacency matrices; the problem language requires a nonempty graph, a binary word with leading bit true, and a positive value.
• WLdim G is sInf of the positive identifying dimensions; this set is nonempty for finite graphs (dimension equal to the order identifies), so the infimum is not the default value.
• Time is counted in steps of the explicit Turing machine on the input length; EXPTIME uses bounds $2^{C(n+1)^d}$ and reductions use bounds $C(n+1)^d$.

The goal is not trivial: membership in EXPTIME and hardness under the explicit machine model are both required.

Needed infrastructure: WL refinement monotonicity, pebble games or an equivalent characterization, CFI-type gadget constructions, and Turing-machine simulation. Contributions toward the upper bound (Proposition 7.1) or the reconstruction results of Sections 3–5 are welcome.

Selected references

• OpenAI, The complexity of identifying a graph by Weisfeiler–Leman refinement, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf
• OpenAI, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/main/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, Nauchno-Technicheskaya Informatsiya, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• V. Arvind, J. Köbler, G. Rattan, O. Verbitsky, Graph Isomorphism, Color Refinement, and Compactness, Computational Complexity 26 (2017).
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13 (full version https://arxiv.org/abs/2402.11531)
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
• S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.

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

$$\phi\ \text{satisfiable}\ \Longrightarrow\ G_\phi\ \text{three-colorable}, \qquad \phi\ \text{unsatisfiable}\ \Longrightarrow\ \alpha(G_\phi)<\delta\,|V(G_\phi)| .$$

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

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

$$x\in L\ \Rightarrow\ \mathrm{DFVS}(G_x)\le k_x,\qquad x\notin L\ \Rightarrow\ \mathrm{DFVS}(G_x)>A\,k_x .$$

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

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

$$\varphi\ \text{satisfiable}\Rightarrow \mathrm{OPT}_{\mathrm{uncut}}(G)\le k,\qquad \varphi\ \text{unsatisfiable}\Rightarrow \mathrm{OPT}_{\mathrm{uncut}}(G)>K\,k,$$

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 vertex cover of a graph is a set of vertices meeting every edge; $\tau(G)$ denotes the minimum size of one. Computing $\tau(G)$ exactly is NP-hard, but a two-line algorithm — take both endpoints of a maximal matching — always returns a cover of size at most $2\tau(G)$. Whether any polynomial-time algorithm achieves a fixed factor $2-\varepsilon$ is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below $10\sqrt5-21\approx1.36$ and, after the 2-to-2 Games Theorem, below $\sqrt2$; factor-two hardness was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that every fixed approximation factor below two is NP-hard, as claimed in an OpenAI preprint dated September 23, 2026 (source, Corollary 1.2, p. 1). The preprint's direct reduction starts from ordinary perfect-completeness Label Cover. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1972 — Karp proves Node Cover NP-complete (Karp 1972); the maximal-matching algorithm gives factor $2$.
• 1992–1998 — Feige–Goldwasser–Lovász–Safra–Szegedy (JACM 1996) link proof checking to approximation; the PCP theorem (Arora–Safra, JACM 1998; Arora–Lund–Motwani–Sudan–Szegedy, JACM 1998) gives a constant gap; Raz's parallel repetition (SICOMP 1998) yields Label Cover with arbitrarily small soundness.
• 2001 — Håstad: NP-hard below factor $7/6$ (JACM 2001).
• 2005 — Dinur–Safra: NP-hard below $10\sqrt5-21\approx1.36068$ (Annals 2005).
• 2002–2008 — Khot's Unique Games Conjecture (STOC 2002); Khot–Regev prove factor-$(2-\varepsilon)$ hardness assuming it (JCSS 2008).
• 2009 — Karakostas's algorithm achieves $2-\Theta(1/\sqrt{\log n})$ (TALG 2009), a saving that vanishes with $n$.
• 2017–2023 — The 2-to-2 Games programme (Khot–Minzer–Safra, ToC 2025; Dinur–Khot–Kindler–Minzer–Safra, ToC 2025; Barak–Kothari–Steurer, ITCS 2019; Khot–Minzer–Safra expansion, Annals 2023) gives NP-hardness below $\sqrt2$.
• 2026 — The OpenAI preprint claims NP-hardness for every fixed factor below $2$.

Setting

A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count $n$ and a duplicate-free list of edges $\{u,v\}$ with $u<v$. A set $S$ of vertices is a cover if every edge has an endpoint in $S$, and $\tau(G)$ is the least size of a cover. An $\alpha$-approximation algorithm is a deterministic polynomial-time machine that, on every graph, outputs a duplicate-free list of vertices that covers all edges and has length at most $\alpha\,\tau(G)$.

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses; malformed strings are NO instances. A 3SAT decider is a deterministic polynomial-time machine answering membership correctly on every input.

Formalization targets

Milestone: the explicit cover gap (Theorem 1.1, p. 1)

For every integer $m\ge4$ there is a deterministic polynomial-time reduction $\varphi\mapsto G_\varphi$ from 3SAT to explicit simple graphs with

$$\varphi\text{ satisfiable}\Rightarrow \tau(G_\varphi)<\Bigl(\tfrac12+\tfrac1m\Bigr)|V(G_\varphi)|,\qquad \varphi\text{ unsatisfiable}\Rightarrow \tau(G_\varphi)>\Bigl(1-\tfrac1m\Bigr)|V(G_\varphi)|.$$

The ratio of the thresholds is $2-6/(m+2)\to2$. In Lean: OAI.VertexCover.explicit_cover_gap.

Goal: factor-two threshold (Corollary 1.2, p. 1)

For every real $\alpha$ with $1\le\alpha<2$, an $\alpha$-approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:

$$\forall\,\alpha\in[1,2):\quad \mathrm{Approximation}(\alpha)\;\Longrightarrow\;\mathrm{ThreeSATDecision}.$$

In Lean: OAI.VertexCover.every_fixed_factor_below_two. The preprint derives it from Theorem 1.1 in its final section (pp. 23–24) by choosing $m$ from $\alpha$ and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies $2$ as the approximation threshold unless P = NP.

Significance

The result itself. The statement removes the Unique Games hypothesis from the Khot–Regev theorem and closes the gap between the elementary factor-$2$ algorithm and hardness. The density gap of Theorem 1.1 is also a statement about independent sets: YES graphs have independent sets of density nearly $1/2$, NO graphs have none of density above $1/m$.

Formalizing it. No machine-checked proof of any super-constant Vertex Cover hardness bound is known to exist. A complete development requires the perfect-completeness Label Cover theorem (Theorem 2.1, p. 4; PCP theorem plus parallel repetition, used as an external input), the explicit graph construction and its polynomial-time implementation (Proposition 3.3, p. 7), and the preprint's analytic soundness argument. The Label Cover input and a library for polynomial-time gap reductions on TM2 machines are reusable for many other hardness missions.

Difficulty

Soundness requires extracting short lists of candidate labels from an arbitrary large independent set, where each list may depend only on its own position's query. If a list also sees the opposite endpoint of a constraint or its occurrence index, the pair-decoding argument against Label Cover soundness breaks down (Introduction, pp. 3–4). Classical approaches either need the stronger Unique Games source promise (Khot–Regev) or only reach densities near $1-1/\sqrt2$ (the 2-to-2 route), which gives factor $\sqrt2$ rather than $2$. Averaging to impose the information restriction can erase all variance; the analytic core is retaining it without any dependence on the label alphabet sizes.

Formalization scope

• Graphs are VertexCover.ExplicitGraph: n : ℕ and a Nodup list of pairs in Fin n × Fin n with e.1 < e.2; coverNumber is the least cardinality of a covering Finset (always defined since univ covers).
• Encodings: inputs are raw bits; graphs are encoded by ExplicitGraph.bits (vertex count, all vertex names, edge count, edge endpoints, each with prefix-free binary framing); an approximation's output list is encoded by natListBits.
• Approximation α bundles a polynomial-time TM2 program on graph encodings with finite tape alphabets, whose output is duplicate-free, in range, covers every edge and has length at most α * coverNumber. ThreeSATDecision is a polynomial-time TM2 decider correct on every input.
• The goal is an implication from an algorithm to a decider: no assumption P ≠ NP is built in, and the hypothesis $1\le\alpha<2$ is satisfied by real algorithms only if 3SAT is easy, which is exactly the content. It cannot be discharged trivially because Approximation α must be correct on every graph.
• The milestone's thresholds are compared in ℝ with strict inequalities as in the source.

Welcome contributions: Label Cover hardness (PCP theorem + parallel repetition), Efron–Stein decompositions and variance inequalities on product spaces, and general complexity-theoretic infrastructure for Turing.TM2ComputableInPolyTime.

Selected references

• OpenAI, The Factor-Two Hardness Threshold for Vertex Cover, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026/paper.pdf
• R. M. Karp, Reducibility among combinatorial problems, Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• 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
• S. Khot, O. Regev, Vertex cover might be hard to approximate to within 2−ε, J. Comput. Syst. Sci. 74 (2008). https://doi.org/10.1016/j.jcss.2007.06.019
• G. Karakostas, A better approximation ratio for the Vertex Cover problem, ACM Trans. Algorithms (2009). https://doi.org/10.1145/1597036.1597045
• R. Raz, A parallel repetition theorem, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539795280895
• 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?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

Motivation: cut metrics, flows and the planar embedding conjecture

A finite metric space embeds into $L_1$ exactly when its metric is a nonnegative combination of cut metrics $\delta_S(x,y)=|\mathbf 1_S(x)-\mathbf 1_S(y)|$. For this reason the least distortion with which a graph metric embeds into $L_1$ governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst $L_1$ distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into $L_1$ with uniformly bounded distortion. The planar case has been the central open instance.

Timeline

• 1981 — Okamura and Seymour: multicommodity flows in planar graphs with all terminals on one face (JCTB 1981), giving isometric $L_1$ representations of one-face metrics.
• 1993 — Klein, Plotkin and Rao: decompositions of graphs excluding a fixed minor (STOC 1993).
• 1999 — Rao: every $n$-vertex planar metric embeds into $L_1$ (via Euclidean space) with distortion $O(\sqrt{\log n})$ (SoCG 1999).
• 2003 — Newman and Rabinovich: series-parallel metrics may need $\Omega(\sqrt{\log n})$ distortion into Euclidean space, so the Euclidean route cannot give a constant (DCG 2003).
• 2004 — Gupta, Newman, Rabinovich and Sinclair: constant distortion for series-parallel graphs, and the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: $k$-outerplanar graphs, with a bound exponential in $k$ (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent: sharp bound $2$ for series-parallel graphs (FOCS 2008); Lee and Raghavendra: matching lower bound (DCG 2010). Lee and Sidiropoulos relate the planar case to the full conjecture (STOC 2009).
• 2013 — Sidiropoulos: constant distortion for planar metrics realized in nonpositively curved simply connected surfaces (FOCS 2013).
• 2019–2025 — Face-cover bounds by Krauthgamer, Lee and Rika (SODA 2019) and Filtser (TALG 2025); Abraham, Filtser, Gupta and Neiman recover Rao's bound via shortest-path decompositions (SICOMP 2022).
• 2026 — An OpenAI preprint, Planar Graph Metrics Embed into $L_1$ with Constant Distortion (OpenAI Math Release, September 23, 2026), claims the planar case of the GNRS conjecture. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite connected simple graph on vertex set $V=\{0,\dots,n-1\}$ with symmetric edge lengths $\ell(u,v)=\ell(v,u)>0$ on edges. The graph metric $d_G(x,y)$ is the infimum of $\sum\ell(e)$ over walks from $x$ to $y$. $G$ is planar if it has a drawing in $\mathbb R^2$: distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.

A map $f:V\to L_1(\Omega,\mu)$ into the real $L_1$ space of some measure space has distortion at most $C$ if $d_G(x,y)\le\|f(x)-f(y)\|_1\le C\,d_G(x,y)$ for all $x,y$.

Formalization targets

Goal: Theorem 1.1 (planar graph metrics in $L_1$)

There is a constant $C\ge1$ such that for every $n$, every connected planar graph $G$ on $n$ vertices and every symmetric positive edge-length function $\ell$, there are a measure space $(\Omega,\mathcal F,\mu)$ and $f:V\to L_1(\Omega,\mathcal F,\mu;\mathbb R)$ with

$$d_G(x,y)\;\le\;\|f(x)-f(y)\|_1\;\le\;C\,d_G(x,y)\qquad(x,y\in V).$$

The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.

Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an $L^1$ space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.

Difficulty

Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show $\Omega(\sqrt{\log n})$ Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.

Formalization scope

• Vertices are Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so $n\ge1$). Singletons are allowed.
• IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.
• Edge lengths are a function Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.
• The target space is MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into $f$).
• Infrastructure needed: plane drawings and their combinatorial consequences (rotation systems, noncrossing column models), cut-metric representations of $L_1$ metrics, and the probabilistic multiscale construction. Plane-drawing and cut-metric infrastructure is reusable.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995). https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An $O(\log k)$ approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica (2004). https://doi.org/10.1007/s00493-004-0015-x
• S. Rao, Small distortion and volume preserving embeddings for planar and Euclidean metrics, SoCG 1999. https://doi.org/10.1145/304893.304983
• I. Newman, Y. Rabinovich, A lower bound on the distortion of embedding planar metrics into Euclidean space, Discrete Comput. Geom. (2003). https://doi.org/10.1007/s00454-002-2813-5
• C. Chekuri, A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Embedding $k$-outerplanar graphs into $\ell_1$, SIAM J. Discrete Math. (2006). https://doi.org/10.1137/S0895480102417379
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, A. Sidiropoulos, On the geometry of graphs with a forbidden minor, STOC 2009. https://doi.org/10.1145/1536414.1536450
• A. Sidiropoulos, Non-positive curvature and the planar embedding conjecture, FOCS 2013. https://doi.org/10.1109/FOCS.2013.27
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. (2022). https://doi.org/10.1137/19M1296021
• A. Filtser, A face cover perspective to $\ell_1$ embeddings of planar graphs, ACM Trans. Algorithms (2025). https://doi.org/10.1145/3686800
• OpenAI, Planar Graph Metrics Embed into $L_1$ with Constant Distortion, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf

Motivation

A standard way to build a random network with a prescribed degree sequence is to choose a graph uniformly at random from the set of all simple graphs with that degree sequence. The model arises in testing whether the exponential family with the degree sequence as sufficient statistic fits network data, in simulating networks with given degrees, and, for constant degrees, as the random regular graph (Blitzstein–Diaconis, Chatterjee–Diaconis–Sly). Quantities such as the expected number of triangles of such a graph are usually estimated by simulation.

For dense graphs, those whose number of edges is of order $n^2$, the Lovász–Szegedy theory of graph limits (Lovász–Szegedy 2006) describes a large graph by a symmetric function $W:[0,1]^2\to[0,1]$. Chatterjee, Diaconis and Sly identify this limit for uniformly random graphs with a given degree sequence. The answer is the limit of the β-model, a random graph with independent edges whose edge probabilities are $e^{\beta_i+\beta_j}/(1+e^{\beta_i+\beta_j})$. The limit gives exact asymptotic formulas for subgraph counts without simulation.

Setting

Graphs and densities. For a finite simple graph $H$ on $[k]=\{1,\dots,k\}$ and a simple graph $G$ on $n$ vertices, the homomorphism density is

$$t(H,G)=\frac{|\hom(H,G)|}{n^k},$$

where $\hom(H,G)$ is the set of edge-preserving maps $V(H)\to V(G)$. For $W:[0,1]^2\to\mathbb R$,

$$t(H,W)=\int_{[0,1]^k}\prod_{\{i,j\}\in E(H)}W(x_i,x_j)\,dx_1\cdots dx_k,$$

with one factor per edge. Graphs $G_n$ on $n$ vertices converge to the limit represented by $W$ if $t(H,G_n)\to t(H,W)$ for every finite simple graph $H$.

Degree sequences and scaling limits. For each $n$ let $d^n=(d^n_1\ge\dots\ge d^n_n)$ be the degree sequence of some simple graph on $n$ vertices. The sequence $\{d^n\}$ has scaling limit $f$, a nonincreasing function on $[0,1]$, if

$$\left|\frac{d^n_1}{n}-f(0)\right|+\left|\frac{d^n_n}{n}-f(1)\right|+\frac1n\sum_{i=1}^n\left|\frac{d^n_i}{n}-f\!\left(\frac in\right)\right|\longrightarrow0 .$$

$D'[0,1]$ is the set of nonincreasing functions on $[0,1]$ that are left continuous on $(0,1)$. It carries the modified $L^1$ norm $\|f\|_{1'}=|f(0)|+|f(1)|+\int_0^1|f|$. $\mathcal F\subseteq D'[0,1]$ is the set of all scaling limits of degree sequences.

The random graphs. $G_n$ is chosen uniformly from the simple graphs on $\{1,\dots,n\}$ with degree sequence $d^n$. In a random graph with independent edges each pair $\{i,j\}$ is an edge with probability $p_{ij}$, independently of the other pairs. The β-model $P_\beta$ is the case $p_{ij}=e^{\beta_i+\beta_j}/(1+e^{\beta_i+\beta_j})$.

Formalization targets

Goal: Theorem 1.1 (pp. 4–5)

If $f$ lies in the interior of $\mathcal F$ for $\|\cdot\|_{1'}$, there is a function $g\in D'[0,1]$, unique on $[0,1]$, such that

$$W(x,y)=\frac{e^{g(x)+g(y)}}{1+e^{g(x)+g(y)}}\quad\text{satisfies}\quad f(x)=\int_0^1W(x,y)\,dy\ \ \text{for all }x\in[0,1],$$

and almost surely $t(H,G_n)\to t(H,W)$ for every finite simple graph $H$.

Milestones (in the order the proof uses them)

• Lemma 2.2 (p. 14): the fixed-point map $\varphi$ of the β-model likelihood equations satisfies $|\varphi(x)-\varphi(y)|_1\le2e^{2K}|x-y|_1$ when $|x|_\infty,|y|_\infty\le K$.
• §6.2, p. 30: for nonincreasing $d$, the Erdős–Gallai slack $\mathcal E(B)$ over sets of size $k$ is minimized at $\{1,\dots,k\}$.
• Lemma 6.1 (p. 26): for independent-edge random graphs, $\mathbb P(|t(H,G)-\mathbb E t(H,G)|>\varepsilon)\le2e^{-C\varepsilon^2n^2}$ with $C=C(H)$.
• Claim 6.3 (p. 27): integer margins close to the row and column sums of a matrix with entries in $[\delta,1-\delta]$ are realized by a 0–1 contingency table.
• Lemma 6.2 (p. 26): if $\delta\le p_{ij}\le1-\delta$ and $d_i=\sum_{j\ne i}p_{ij}$, the independent-edge graph has degree sequence $d$ with probability at least $\tfrac12\delta^{\,n^{3/2+\varepsilon}}$ for large $n$.
• p. 34: conditioned on its degree sequence being $d$, the β-model graph is uniform on graphs with degree sequence $d$.

The proof also uses three results posed in sibling missions of this series: Proposition 1.2 (mission 4, the interior of $\mathcal F$), Lemma 4.1 (mission 3, existence and boundedness of the MLE) and Theorem 1.5 (mission 1, geometric convergence of the iteration $x\mapsto\varphi(x)$). They are not restated here.

Significance

The theorem turns questions about a uniformly random graph with given degrees, a law with no independence, into questions about an explicit graphon. Every subgraph density, the limiting degree distribution, and every graph parameter continuous for the graph-limit topology of the uniform model is computed from $W$. The function $g$ solves a continuum version of the β-model maximum-likelihood equations, which connects the combinatorial model with exponential-family statistics.

The result is proved in the paper, which is published in the Annals of Applied Probability (2011). To our knowledge it has no machine-checked proof. Formalizing it requires a Lean development of dense graph limits (homomorphism densities, graphon densities, graph-limit convergence), none of which exists in Mathlib. It also requires a bounded-differences concentration inequality, and a transfer argument from independent-edge models to models conditioned on degrees. Each of these is reusable beyond this mission.

Difficulty

The uniform measure on graphs with a fixed degree sequence has no independence, so concentration inequalities do not apply to it directly. The obvious route is to condition an independent-edge model on its degree sequence. This works only if the probability of the conditioning event is larger than the concentration bound, which is $e^{-cn^2}$. A crude lower bound of $\delta^{\binom n2}$ is too small. Lemma 6.2 supplies $\delta^{n^{3/2+\varepsilon}}$, and it needs a combinatorial completion step (Claim 6.3).

The second difficulty is analytic. The maximum-likelihood parameters $\beta^n$ for different $n$ live in different dimensions. One must show that their step-function profiles converge in $L^1$ to a limit $g$ and that this $g$ solves the continuum equation at every point of $[0,1]$, not only almost everywhere. Several steps of the paper's argument are only sketched. Among them are the almost-sure convergence of the β-model graphs to $W$ and the estimate $f_n(x)=d^n_{\lceil nx\rceil}/n+O(1/n)$ (pp. 33–34).

Formalization scope

• Vertices are Fin n (the paper's vertex $i$ is $i-1$), graphs are SimpleGraph (Fin n), and a test graph $H$ is a SimpleGraph (Fin k), which loses nothing because densities are invariant under relabelling.
• Functions on $[0,1]$ are ℝ → ℝ, and only their values on $[0,1]$ matter. Uniqueness of $g$ is equality on $[0,1]$.
• $t(H,W)$ takes one factor per unordered edge, and the integral is the Lebesgue integral over $[0,1]^k$.
• Laws on graphs are finite sums of Dirac masses. The σ-algebra on SimpleGraph (Fin n) is discrete.
• The interior of $\mathcal F$ is taken in $D'[0,1]$ for $\|\cdot\|_{1'}$, as the ball form "every $h\in D'[0,1]$ with $\|h-f\|_{1'}<\varepsilon$ lies in $\mathcal F$".
• The paper does not say how the $G_n$ for different $n$ are coupled. The goal quantifies over every probability space and every family of measurable $G_n$ with the uniform marginals, so the almost-sure convergence holds for every joint law. The almost-sure event contains "for every $H$".
• Lemma 6.2's printed bound $\tfrac12\exp(-\log(\delta)n^{3/2+\varepsilon})$ exceeds $1$. The milestone states the intended bound $\tfrac12\exp(\log(\delta)n^{3/2+\varepsilon})$, with $N$ depending only on $(\delta,\varepsilon)$.
• Constants are explicit quantifiers. In Lemma 6.1, $C>0$ is chosen from $H$ before $n$, $p$ and $\varepsilon$.

A formalization that replaces almost-sure convergence by convergence in expectation or in probability, that fixes a single coupling, or that asserts the existence of $g$ only almost everywhere states a weaker theorem and does not close this mission.

Welcome contributions include a general graph-limit library (densities, convergence, the counting lemma), McDiarmid's bounded-differences inequality for finitely many independent Bernoulli variables, the Gale–Ryser theorem in the form needed by Claim 6.3, and proofs of the milestones.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4), 1400–1435, 2011. https://arxiv.org/abs/1005.1136v5
• L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96, 933–957, 2006. https://doi.org/10.1016/j.jctb.2006.05.002
• C. Borgs, J. Chayes, L. Lovász, V. Sós, K. Vesztergombi, Convergent sequences of dense graphs I, Adv. Math. 219, 1801–1851, 2008. https://doi.org/10.1016/j.aim.2008.07.008
• J. Blitzstein, P. Diaconis, A sequential importance sampling algorithm for generating random graphs with prescribed degrees, Internet Math. 6(4), 489–522, 2011. https://doi.org/10.1080/15427951.2010.557277

Motivation

A degree sequence records how many neighbours each vertex of a graph has. In network statistics it is often the only summary of a graph that is observed or trusted, and the natural probability models for graphs in which "the degree sequence captures the information" are exponential families whose sufficient statistic is the degree sequence. Chatterjee, Diaconis and Sly (arXiv:1005.1136, Ann. Appl. Probab. 2011) call the resulting model the β-model and study its maximum likelihood theory and its use for sampling random graphs with a prescribed degree sequence.

For any exponential family, the first question about estimation is which values of the sufficient statistic can be matched by a parameter: the maximum likelihood equations say exactly "the expected statistic equals the observed one". Theorem 1.4 of the paper answers this for the β-model. Up to taking a closure, the expected degree sequences of the β-model fill the whole convex hull of the degree sequences. The paper notes that the result can also be derived from classical results on the mean space of exponential families (Barndorff-Nielsen 1978; Brown 1986; Wainwright and Jordan 2008, Theorem 3.3), and gives a self-contained proof in §3. Lemma 4.1 of the same paper uses Theorem 1.4 to show that the maximum likelihood estimator exists.

Setting

Fix $n\ge 0$ and the vertex set $\{1,\dots,n\}$. A graph $G$ is undirected and simple: no loops and no multiple edges. Its degree sequence is $d(G)=(d_1,\dots,d_n)\in\mathbb R^n$, and

$$\mathcal D=\{d(G):\ G\text{ a simple graph on }n\text{ vertices}\}$$

is the finite set of all degree sequences. Its convex hull $\operatorname{conv}(\mathcal D)$ is a polytope in $\mathbb R^n$.

For $\beta\in\mathbb R^n$, the β-model $\mathbb P_\beta$ is the law of the random graph in which each pair $\{i,j\}$, $i\neq j$, is an edge with probability

$$p_{ij}=\frac{e^{\beta_i+\beta_j}}{1+e^{\beta_i+\beta_j}},$$

independently of all other pairs. The expected degree sequences form the set

$$\mathcal R=\big\{\big(\mathbb E_\beta[d_1],\dots,\mathbb E_\beta[d_n]\big):\ \beta\in\mathbb R^n\big\}.$$

Two functions on $\mathbb R^n$ appear in the proof. The first is $g=(g_1,\dots,g_n)$ with

$$g_i(x)=\sum_{j\neq i}\frac{e^{x_i+x_j}}{1+e^{x_i+x_j}}.$$

The second is, for each $y\in\mathbb R^n$,

$$f_y(x)=\sum_{i=1}^n x_iy_i-\log\prod_{1\le i<j\le n}\big(1+e^{x_i+x_j}\big).$$

The Lean development names these objects betaModel, D, R, g and fy in the namespace GivenDegreeSeq.MeanPolytope.

Formalization targets

Goal: Theorem 1.4 (p. 8)

$$\operatorname{conv}(\mathcal D)=\overline{\mathcal R}\qquad\text{for every }n.$$

The statement fixes no constants. The closure cannot be dropped: for $n\ge2$ the degree sequence $0$ of the empty graph lies in $\mathcal D$ but not in $\mathcal R$, because every expected degree is positive.

Milestones, in the order the proof uses them

1. The probability formula (p. 6): $\mathbb P_\beta$ is a probability measure, and

$$\mathbb P_\beta(\{G\})=\frac{e^{\sum_i\beta_id_i}}{\prod_{i<j}(1+e^{\beta_i+\beta_j})}.$$

2. Expected degrees (p. 15): $\mathbb E_x[d_i]=g_i(x)$, so $\mathcal R=g(\mathbb R^n)$.
3. The easy inclusion (p. 15): $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$.
4. A uniform bound (p. 16): $f_y(x)\le 0$ for all $y\in\operatorname{conv}(\mathcal D)$ and $x\in\mathbb R^n$.
5. Smoothness (p. 16): $f_y$ is twice differentiable and $\nabla^2 f_y$ is uniformly bounded.
6. Lemma 3.1 (pp. 14–15): if $f$ is twice differentiable, $M=\sup f<\infty$ and $\|\nabla^2 f\|_{\mathrm{op}}\le C$, then

$$|\nabla f(x)|^2\le 2C\big(M-f(x)\big),$$

and $\nabla f(x_k)\to0$ along some sequence. 7. The gradient (p. 16): $\nabla f_y(x)=y-g(x)$.

Significance

The theorem describes the mean space of the β-model. Its interior contains every degree sequence that lies strictly inside the polytope, and for these sequences maximum likelihood estimation is well posed. The paper's consistency result (Theorem 1.3) and the existence part of Lemma 4.1 start from this description. The polytope $\operatorname{conv}(\mathcal D)$ is studied in its own right; its extreme points are the degree sequences of threshold graphs (Mahadev and Peled 1995).

Theorem 1.4 is proved, and as far as this mission's authors know it is not machine-checked anywhere. Formalizing it means turning the paper's short proof into a complete argument. That includes the steps the page dismisses as easy: the exponential-family formula for the independent-edge law, the expectation computation, the Hessian bound for $f_y$, and the passage from a sequence of approximate critical points to the closure. Lemma 3.1, a descent-type gradient bound for a function bounded above, is a general fact of real analysis and is independent of graphs.

Difficulty

The inclusion $\overline{\mathcal R}\subseteq\operatorname{conv}(\mathcal D)$ is direct: an expectation is an average. The reverse inclusion is the content. For $y$ in the interior of the polytope, one would like to find $x$ with $g(x)=y$ by maximizing the concave function $f_y$. For $y$ on the boundary of the polytope, however, $f_y$ need not attain its supremum. So the argument cannot rely on the existence of a maximizer, and it has to produce points $x_k$ with $g(x_k)\to y$ without ever solving $g(x)=y$. Compactness arguments on $\beta$ fail for the same reason: the relevant sequences $x_k$ are unbounded.

Formalization scope

• Graphs and measure. Vertices are Fin n, so the paper's vertex $i$ is the index $i-1$. Graphs are SimpleGraph (Fin n), a finite type. Its σ-algebra is Mathlib's SimpleGraph.instMeasurableSpace, under which every set of graphs on Fin n is measurable.
• The law and its expectations. $\mathbb P_\beta$ is the finite sum of Dirac masses weighted by the independent-edge product over pairs $i<j$. $\mathcal R$ is defined through Bochner expectations under $\mathbb P_\beta$, not as the range of $g$. Defining $\mathcal R$ as $g(\mathbb R^n)$ would erase the link to the probability model and is ruled out.
• Vector spaces. $\mathcal D$ and $\mathcal R$ are subsets of Fin n → ℝ, whose product topology is the Euclidean topology, so the closure is unambiguous. Gradients and Hessians are taken on EuclideanSpace ℝ (Fin n). There "twice differentiable" means that $f$ and its Fréchet derivative are differentiable, and the Hessian norm is the norm of the second Fréchet derivative, which equals the $L^2$ operator norm of the Hessian matrix.
• No size hypothesis. The goal holds for every $n$; for $n\le1$ both sides are $\{0\}$.
• Readings of the page.
  • On p. 15 the paper prints $\log\sum_{1\le i<j\le n}(1+e^{x_i+x_j})$ in $f_y$. The formalization uses $\log\prod$, the only reading under which "taking logs, we get $f_d(x)\le0$" and $\nabla f_y=y-g$ hold. The milestone text keeps the printed version.
  • The "Lemma 11" of p. 16 is Lemma 3.1.
  • The probability-measure property of $\mathbb P_\beta$ is stated as a conjunct of milestone 1.
  • The differentiability of $f_y$ is stated alongside the Hessian bound in milestone 5.

Contributions of any milestone are welcome. Lemma 3.1 and the gradient identity are self-contained calculus. The probability formula and the expected-degree identity are finite computations on graphs.

Selected references

• S. Chatterjee, P. Diaconis, A. Sly, Random graphs with a given degree sequence, Ann. Appl. Probab. 21(4) (2011), 1400–1435. https://arxiv.org/abs/1005.1136 (v5), https://doi.org/10.1214/10-AAP728
• O. Barndorff-Nielsen, Information and Exponential Families in Statistical Theory, Wiley, Chichester, 1978. MR0489333, https://mathscinet.ams.org/mathscinet-getitem?mr=0489333
• L. D. Brown, Fundamentals of Statistical Exponential Families with Applications in Statistical Decision Theory, IMS Lecture Notes–Monograph Series 9, 1986. MR0882001, https://mathscinet.ams.org/mathscinet-getitem?mr=0882001
• M. J. Wainwright, M. I. Jordan, Graphical models, exponential families, and variational inference, Found. Trends Mach. Learn. 1 (2008), 1–305. https://doi.org/10.1561/2200000001
• N. V. R. Mahadev, U. N. Peled, Threshold Graphs and Related Topics, Ann. Discrete Math. 56, North-Holland, 1995. MR1417258, https://mathscinet.ams.org/mathscinet-getitem?mr=1417258

Motivation

A $T$-join of a graph $G$ is a set of edges $F$ such that exactly the vertices of a prescribed even set $T$ have odd degree in $F$. Minimum $T$-joins are a classical object of combinatorial optimization: they contain shortest paths ($|T|=2$), Chinese postman tours and perfect matchings as special cases, and their duality with $T$-cuts connects them to integral multiflows. Whether the minimum size $\tau(G,T)$ of a $T$-join equals the maximum number $\nu(G,T)$ of disjoint $T$-cuts has been studied extensively; equality always holds in bipartite graphs (Seymour 1981).

Sebő and Tannier (Math. Oper. Res. 2004) study the number of connected components of a minimum $T$-join, motivated by the observation that a minimum $T$-join with few components yields a large integral packing of $T$-cuts. Deciding whether some minimum $T$-join has at most $k$ components is NP-complete in general (their Theorem 5). This mission formalizes the opposite end, $k=1$: Theorem 6 characterizes exactly when a minimum $T$-join can be chosen connected, in terms of the shortest-path metric of $G$ restricted to $T$. The result first appeared in the authors' IPCO paper Connected joins in graphs (2001); the 2004 article derives it from its theory of isometric embeddings.

Setting

All graphs are finite, simple, undirected and connected. For vertices $x,y$ of $G$, $\mu_G(x,y)$ is the number of edges of a shortest $x$–$y$ path. For $T\subseteq V(G)$, $\mu_G|_T$ is the restriction of $\mu_G$ to pairs of vertices of $T$.

For an edge set $F\subseteq E(G)$, $\deg_F(v)$ is the number of edges of $F$ at $v$; $F$ is a $T$-join if $\deg_F(v)$ is odd exactly when $v\in T$. A minimum $T$-join has the fewest edges among all $T$-joins; a minimal one has no proper subset that is a $T$-join. $V(F)$ is the set of endpoints of edges of $F$; $F$ is connected (a tree) when the graph $(V(F),F)$ is connected (a tree), and $\mu_F$ is the distance in $(V(F),F)$.

An isometry from $(X,\mu)$ to $(Y,\nu)$ is a map $f$ with $\nu(f(x),f(y))=\mu(x,y)$ for all $x,y$. A metric $\mu$ on a finite set $X$ is a tree metric if there is a tree $A$ (unit edge lengths) and an isometry $g$ from $(X,\mu)$ to $A$; the pair $(A,g)$ is a realization. A realization is inclusionwise minimal if no proper subtree of $A$ contains $g(X)$. A tree $A$ is an $S$-join if its vertices of odd degree are exactly those of $S$.

Formalization targets

Goal: Theorem 6

For $G$ connected and $T$ nonempty of even cardinality,

$$\exists\,F\ \text{minimum connected }T\text{-join} \iff \begin{cases}\mu_G|_T \text{ is a tree metric, and for its minimal realization }(A,g),\ T':=g(T):\\ A \text{ is a } T'\text{-join},\\ \exists\,\varphi:V(A)\to V(G)\ \text{isometry with } \varphi(g(t))=t\ (t\in T).\end{cases}$$

The conditions are required of every minimal realization; all of them are isomorphic.

Milestones

1. (p. 389) A minimal $T$-join is the edge-disjoint union of $|T|/2$ paths pairing the vertices of $T$.
2. (p. 391) In every realization of $\mu$, the distance from $g(x)$ to the $g(y)$–$g(z)$ path equals $\tfrac12(\mu(x,y)+\mu(x,z)-\mu(y,z))$.
3. (p. 391) A tree metric has an inclusionwise minimal realization, unique up to an isomorphism respecting the realization maps.
4. (Lemma 2, p. 392) A connected $T$-join $F$ is minimum if and only if $F$ is a tree and $\mu_F=\mu_G$ on $V(F)$.
5. (p. 392) If $A$ is a $T'$-join and $\varphi$ an isometry from $A$ to $G$ extending $g^{-1}$, the image of $A$ under $\varphi$ is a $T$-join that is a tree with $\mu_F=\mu_G$ on $V(F)$.

Significance

Theorem 6 turns the existence of a connected minimum $T$-join, a question about all $T$-joins of $G$, into conditions on the finite metric $\mu_G|_T$ alone plus one isometric embedding of a tree into $G$. Tree metrics can be recognized and their minimal realization constructed efficiently (Buneman 1974), and the embedding problem is the one solved in §2 of the paper, since $T'$ contains all leaves of $A$. The authors deduce that connected minimum $T$-joins can be found in polynomial time, which contrasts with the NP-completeness of the same question for $k$ components. A consequence stated in the paper: if the minimal realization of $\mu_G|_T$ is not a $T'$-join, then no minimum $T$-join is connected.

The result is proved in the paper. No machine-checked version of Theorem 6, of Lemma 2, or of the uniqueness of minimal tree realizations is known to exist; Mathlib has graph distances, trees and walks, but neither $T$-joins nor tree metrics. The mission produces these definitions and a formal proof of the characterization; the complexity consequence is out of scope.

Difficulty

The central difficulty is in the necessity direction. A connected minimum $T$-join $F$ is itself a minimal realization of $\mu_G|_T$ (Lemma 2), so $F$ satisfies the conditions; but the conditions concern the minimal realization, and transferring them from $F$ to an arbitrary minimal realization requires that minimal realizations are unique up to a label-preserving isomorphism. That uniqueness (milestone 3) is the step where the obvious approach stops: it is a statement about all trees realizing a metric, not about the graph $G$.

Formalization scope

• Graphs are SimpleGraph V with [Fintype V] [DecidableEq V]; G.Connected is a hypothesis of every statement about $G$ (SimpleGraph.dist is $0$ on unreachable pairs). Distances are natural numbers (SimpleGraph.dist).
• Edge sets are Finset (Sym2 V). Connectivity, the tree property and $\mu_F$ refer to the graph with edge set $F$ induced on $V(F)$, not on all of $V$.
• "Minimum" is "$|F|\le|F'|$ for every $T$-join $F'$", never an infimum over $\mathbb N$.
• A realization is a tree on Fin N together with a map $g:X\to$ Fin N; this avoids quantifying over a universe. A tree metric must satisfy $\mu(x,y)=0\Rightarrow x=y$.
• "The unique minimal realization" is encoded by quantifying over all inclusionwise minimal realizations. A goal that only asks for some minimal realization satisfying the conditions is a different, weaker statement (its necessity half needs no uniqueness) and is not this mission's target.
• $T\neq\emptyset$ is added: for $T=\emptyset$ the minimum $T$-join is empty and its connectivity is only a convention.
• "$f$ is the inverse of $g$ and $\varphi$ extends $f$" is encoded as $\varphi(g(t))=t$. Isometries preserve all distances, not only adjacency.
• Halving and subtraction (milestone 2) are multiplied out.

Reusable beyond this mission: the $T$-join vocabulary, the path decomposition of minimal $T$-joins, and tree metrics with the uniqueness of minimal realizations. Contributions to any milestone are welcome, as are alternative proofs of milestone 3.

Selected references

• András Sebő, Eric Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• András Sebő, Eric Tannier, Connected joins in graphs, Integer Programming and Combinatorial Optimization (IPCO 2001), Lecture Notes in Computer Science 2081, 383–395, 2001. https://doi.org/10.1007/3-540-45535-3
• Peter Buneman, A note on the metric properties of trees, Journal of Combinatorial Theory, Series B 17:48–50, 1974. https://doi.org/10.1016/0095-8956(74)90047-1
• Paul Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981. https://doi.org/10.1112/plms/s3-42.1.178