Graph Theory

Motivation

Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main theorem says that first-order model checking is fixed-parameter tractable on every class of graphs of bounded twin-width, provided a witnessing contraction sequence is given. This turns every class shown to have bounded twin-width into a class on which a whole logic becomes algorithmically tractable, so the question "which natural classes have bounded twin-width?" has direct algorithmic content.

Section 4 of the paper answers that question for several classes. This mission covers the geometric part of Section 4: $d$-dimensional grids, grids with diagonals, and unit $d$-dimensional ball graphs with bounded clique number. Geometric intersection graphs are a standard source of hard instances in parameterized algorithms. Width parameters designed for dense graphs (rank-width, clique-width, boolean-width) are unbounded already on the planar $n\times n$ grid, whereas twin-width stays bounded on grids of every fixed dimension and transfers from there to ball graphs.

Setting

All graphs are finite and simple. Two vertex sets $X,Y$ of a graph $G$ are homogeneous if every pair $(x,y)\in X\times Y$ is an edge or no pair is. For a partition $\mathcal P$ of $V(G)$, the red degree of a part $X$ is the number of other parts not homogeneous to $X$; $\mathcal P$ is a $d$-partition if every red degree is at most $d$. The graph $G$ has twin-width at most $d$, $\operatorname{tww}(G)\le d$, if there is a sequence $\mathcal P_0,\dots,\mathcal P_N$ of $d$-partitions of $V(G)$ that starts with the partition into singletons, ends with at most one part, and in which each partition arises from the previous one by merging two parts. This is the paper's partition form of its definition by contractions of trigraphs (graphs with black and red edges, §3).

For the all-red trigraph $H^r=(V,\emptyset,E(H))$, in which every edge of $H$ is red, the paper's contraction rule never produces a black edge, and two parts are red-adjacent exactly when some edge of $H$ joins them. The red twin-width $\operatorname{tww}(H^r)\le d$ is defined as above with this adjacency.

For $d,n\ge 1$, the $d$-dimensional $n$-grid $P^d_n$ has vertex set $[n]^d$, with $x\sim y$ iff $\sum_{i}|x_i-y_i|=1$. The grid with diagonals $K_{n,d}$ has the same vertices, with distinct $x\sim y$ iff $\max_i|x_i-y_i|\le 1$, and $K^r_{n,d}$ is its all-red trigraph; $R^d_n$ is the all-red trigraph of $P^d_n$.

Given centres $c(v)\in\mathbb R^d$ for $v$ in a finite set $V$, the unit ball graph $G$ joins distinct $u,v$ iff the closed unit balls around $c(u)$ and $c(v)$ meet, that is $\|c(u)-c(v)\|_2\le 2$. Its clique number is the largest size of a set of pairwise adjacent vertices. A subgraph of $G$ is obtained by deleting vertices and edges.

Formalization targets

Goal: Theorem 4.5 (p. 3:15)

For every $d,k$, every subgraph $H$ of a unit $d$-dimensional ball graph $G$ with clique number at most $k$ satisfies

$$\operatorname{tww}(H)\le (3\lceil\sqrt d\,\rceil)^d\,k .$$

Milestones, in the order the paper uses them

1. Red paths have twin-width at most $2$ (§3, p. 3:12).
2. Induced subgraphs do not increase twin-width, for graphs and for all-red trigraphs (§4.1, p. 3:12).
3. $\operatorname{tww}(R^d_n)\le 3d$ for positive $d,n$ (the statement proved inside Theorem 4.3, p. 3:15).
4. Theorem 4.3: $\operatorname{tww}(P^d_n)\le 3d$ for positive $d,n$.
5. Every subgraph of $P^d_n$ has twin-width at most $3d$ (p. 3:15).
6. Lemma 4.4: every subgraph of $K^r_{n,d}$ has twin-width at most $2(3^d-1)$.
7. In a unit ball graph without a clique of size $k+1$, each half-open cell of side $2/\sqrt d$ contains at most $k$ centres (proof of Theorem 4.5, p. 3:16).

A companion item, Theorem 4.1 (p. 3:13, graph case), states that adding one vertex joined to an arbitrary set at most changes twin-width from $t$ to $2(t+1)$.

Significance

The goal theorem places unit ball graphs of bounded clique number, in every fixed dimension, among the classes of bounded twin-width. Combined with the paper's main theorem, and with the paper's remark that a contraction sequence can be computed in polynomial time from a geometric representation, it gives fixed-parameter tractable first-order model checking on these graphs. The clique-number hypothesis is needed: unit disk graphs without a clique bound have unbounded twin-width (p. 3:16), as shown in Twin-width II. Theorem 4.3 and Lemma 4.4 are of independent use as twin-width bounds for grids, and the subgraph statements show that grids are an exception to the general fact that bounded twin-width is not preserved by taking (non-induced) subgraphs (p. 3:13).

All results here are proved in the paper. To our knowledge none of them, and no notion of twin-width with red degree, is machine-checked in Lean or Mathlib. The work is to formalize the paper's arguments: the parallel contraction of grid layers, the supercell contraction, and the geometric counting.

Difficulty

Twin-width is not monotone under subgraphs, so the obvious route, "a unit ball graph of bounded clique number is a subgraph of a grid-like graph, hence has bounded twin-width", fails as stated. The paper repairs it by working with all-red trigraphs throughout: for an all-red trigraph, removing edges can only remove red adjacencies, and this is why Theorem 4.3 is proved in its red form and Lemma 4.4 is stated for $K^r_{n,d}$. A second difficulty is bookkeeping: the bound $3d$ comes from contracting the $n$ layers of $P^d_n$ "in parallel" and tracking the red degree of every vertex at each step, and Lemma 4.4 is asserted "by the arguments of Theorem 4.3" without a separate proof, so its argument has to be reconstructed.

Formalization scope

Lean represents twin-width by the predicates TwinWidthLE G d and RedTwinWidthLE H d on finite vertex types: an explicit sequence of Finpartitions of the vertex set from ⊥ (singletons) to at most one part, consecutive partitions differing by one merge of two distinct parts. Twin-width is never a number, so no infimum over an empty set enters. $[n]^d$ is Fin d → Fin n; centres live in EuclideanSpace ℝ (Fin d) with the Euclidean distance; balls are closed of radius $1$, so centres at distance exactly $2$ are adjacent. $\lceil\sqrt d\,\rceil$ is the natural-number ceiling of the real square root. "Clique number $k$" is encoded as CliqueFree (k+1) (clique number at most $k$), which is the same theorem because the bound is monotone in $k$; subgraphs are a finite vertex set $S$ together with a graph $H\le G[S]$ on it.

The hypotheses $1\le d$, $1\le n$ appear in Theorem 4.3, its red form, and the grid-subgraph statement, as on the page ("positive integers"). No other hypothesis is added; Lemma 4.4, the cell bound and the goal hold as stated also for $d=0$ or $n=0$. The red-degree count uses "some edge joins the two parts", which is derived from the paper's contraction rule for trigraphs without black edges and is used only for all-red trigraphs; the twin-width of graphs counts non-homogeneous parts. This rules out the trivializing readings: a twin-width defined as an infimum that defaults to $0$, a sequence allowed to jump to one part, homogeneity counted as adjacency for graphs, or a bound depending on the graph. The polynomial-time sentence of Theorem 4.5 is not formalized.

Reusable infrastructure: the partition-form twin-width predicates (shared with the other missions of this series), grids and grids with diagonals in coordinates, and unit ball graphs. Contributions are welcome on the general lemmas (induced subgraphs, red-to-black transfer, small explicit sequences) as well as on the grid theorems themselves.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, R. Watrigant, Twin-width I: Tractable FO Model Checking, Journal of the ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655 (preprint: https://arxiv.org/abs/2004.14789)
• É. Bonnet, C. Geniet, E. J. Kim, S. Thomassé, R. Watrigant, Twin-width II: small classes, Combinatorial Theory 2(2), 2022. https://arxiv.org/abs/2006.09877

Motivation

Deciding whether a planar graph is 3-colorable is NP-complete, so a large part of the theory of planar graph coloring looks for simple local conditions that guarantee 3-colorability. Grötzsch's theorem (1959) is the model result: every triangle-free planar graph is 3-colorable. Forbidding triangles is not the only possibility, and in 1976 Richard Steinberg asked whether forbidding cycles of two other lengths suffices.

Steinberg's Conjecture (1976). Every planar graph with no cycles of length four or five is 3-colorable.

The conjecture drove four decades of work on planar coloring. It was surveyed by Borodin as one of the central problems of the area (Borodin 2013, §7), and it was one of the six graph theory problems ranked with the highest importance in the Open Problem Garden.

Timeline:

• 1976. Steinberg poses the conjecture (Steinberg 1993 records its history).
• 1991. Erdős suggests the relaxation: find the smallest $k$ such that every planar graph with no cycles of lengths $4, \dots, k$ is 3-colorable. Abbott and Zhou show $k \le 11$ (Ars Combin. 32, 1991).
• 1995. Sanders and Zhao improve this to $k \le 9$ (Graphs Combin. 11, 1995).
• 2005. Borodin, Glebov, Raspaud and Salavatipour prove $k \le 7$: planar graphs without cycles of lengths 4 to 7 are 3-colorable (JCTB 93).
• 2007. Voigt shows that the list-coloring analogue fails: there is a planar graph without 4- and 5-cycles that is not 3-choosable (Discrete Math. 307, 2007).
• 2016. Cohen-Addad, Hebdige, Král', Li and Salgado construct a counterexample, so the conjecture is false (arXiv:1604.05108; J. Combin. Theory Ser. B, 2017).

Setting

All graphs are finite and simple. A cycle of length $k$ in a graph $H$ is a sequence of $k \ge 3$ pairwise distinct vertices $v_0, \dots, v_{k-1}$ with $v_i v_{i+1}$ an edge for each $i$ (indices mod $k$). $H$ has no cycles of length four or five if no cycle of $H$ has length $4$ or $5$; triangles and cycles of length at least six are allowed. A 3-coloring of $H$ assigns one of three colors to each vertex so that adjacent vertices get different colors, and $H$ is 3-colorable if it has one. The distance $d_H(u,v)$ is the number of edges of a shortest $u$–$v$ path. $H$ is planar if it can be drawn in the plane without crossing edges.

The paper builds its counterexample in three steps, from three concrete graphs given as drawings.

1. $G_1$ (Figure 1) has 15 vertices $a, \dots, o$ and 23 edges. Its contact vertices are $a$, $b$, $c$.
2. $G_2$ (Figure 2) consists of three copies of $G_1$ glued along contact vertices around a central triangle $def$. It has 42 vertices and 72 edges, and its contact vertices are $a$, $b$, $c$.
3. $G$ (Figure 3) consists of four copies of $G_2$ glued at a central vertex $a$, together with the extra vertices $b$, $e$, $e'$ and twelve extra edges. It has 166 vertices and 300 edges.

In the Lean development these are the definitions G1, G2 and G. The hypothesis "no cycles of length four or five" is the definition NoFourFiveCycle.

Formalization targets

Goal: Theorem 3 (p. 4)

$$\exists\, H \text{ finite, planar}:\quad H \text{ has no cycle of length } 4 \text{ or } 5 \ \text{ and } \ H \text{ is not 3-colorable}.$$

This is the paper's main theorem and exactly the negation of Steinberg's Conjecture. It leaves the witness free, so any counterexample proves it.

Milestones

1. Lemma 1 (p. 2): $G_1$ has no 4- or 5-cycle; no 3-coloring gives $a, b, c$ the same color; and $d(a,b) = d(a,c) = 3$, $d(b,c) = 4$.
2. Lemma 2 (p. 3): $G_2$ has no 4- or 5-cycle; no 3-coloring gives $a, b, c$ the same color; and the contacts are pairwise at distance $4$.
3. $G$ has no cycle of length four or five (proof of Theorem 3, p. 5).
4. $G$ has no 3-coloring (proof of Theorem 3, p. 5).
5. $G$ is planar (§2, p. 2, and Figure 3).
6. $G_1$ and $G_2$ are planar (§2, p. 2, and Figures 1–2).

Milestones 3–5 together give the goal, with $G$ as the witness.

Significance

The result. Theorem 3 settles a 40-year-old problem negatively. It shows that forbidding 4- and 5-cycles is not a local condition that forces 3-colorability, which redirects the Erdős relaxation: the threshold $k$ for "no cycles of lengths $4, \dots, k$" lies in $\{6, 7\}$, since $k \le 7$ is known and $k = 5$ is now excluded. The paper notes that the same graph also disproves the Strong Bordeaux Conjecture and the Novosibirsk 3-Color Conjecture.

Formalizing it. The theorem is proved, and the proof is short. As far as is known it has no machine-checked version. Every claim in the proof is a finite statement about explicit graphs, so the work here is to verify the three gadgets and the gluing arguments in Lean, including planarity of an explicit 166-vertex graph, which is asserted in the paper only through its figures. Planarity, cycle structure and coloring of a concrete graph of this size are a useful benchmark for computational verification in Lean.

Difficulty

The obvious approach is brute force: $G$ is a fixed finite graph, so in principle each claim can be decided. In practice decide is not workable at this size. Excluding 4- and 5-cycles means quantifying over walks of a 166-vertex graph. Non-3-colorability is a search over $3^{166}$ assignments unless it is reduced, as the paper does, through the gadget lemmas. The planarity witness needs explicit coordinates for 166 points and a check of all $\binom{300}{2}$ pairs of segments, in exact arithmetic. The gluing arguments ("a cycle through two copies has length at least six") are where the paper's distance claims are used. Turning those claims into statements about Mathlib walks on unions of embedded copies is the conceptual work.

Formalization scope

Lean representation and conventions:

• Graphs are Mathlib SimpleGraphs. G1 lives on Fin 15, with $a, \dots, o \mapsto 0, \dots, 14$. G2 lives on Fin 42, with $a, b, c, d, e, f \mapsto 0, \dots, 5$, and G lives on Fin 166, with $a, b, c, c', e, e', d, f, d', f' \mapsto 0, \dots, 9$.
• Copies. G2 is literally (⨆ k, G1.map (copy2 k)) ⊔ the triangle $def$, with explicit embeddings copy2 k : Fin 15 ↪ Fin 42. G is (⨆ k, G2.map (copyG k)) ⊔ the twelve extra edges, with copyG k : Fin 42 ↪ Fin 166. The contact tables are in each definition's statement. A local check confirms the edge counts 23, 72 and 300, and that G agrees edge for edge with an independent transcription of Figure 3.
• Cycles are Mathlib walks p : H.Walk v v with p.IsCycle, and their length is p.length.
• 3-colorings are H.Coloring (Fin 3), and 3-colorability is H.Colorable 3. "No 3-coloring gives $a, b, c$ one color" is ∀ C, ¬ (C a = C b ∧ C b = C c). Colorings in which two of the three share a color are still allowed, as in the paper.
• Distance is SimpleGraph.dist. Its junk value $0$ for unreachable pairs is never hit, because every asserted distance is positive.
• Planarity is the published straight-line predicate OPG37357.IsPlanar: an injective placement of the vertices in $\mathbb R^2$ in which no vertex lies inside an edge segment and edges with four distinct endpoints have disjoint segments. For finite simple graphs it is equivalent to planarity by Fáry's theorem, and it implies topological planarity.
• The goal's witness is a graph on Fin n. This loses no generality for finite graphs, and the empty graph cannot serve as a trivial witness because it is 3-colorable.

The following trivializing formalizations are ruled out. Closed walks, instead of cycles, would exclude every graph with an edge. Girth is not used: $G$ contains triangles. Lemmas 1 and 2 do not assert that $a$ and $b$ get different colors, which would be false for $G_1$. An infinite or unspecified vertex type is not allowed for the witness.

Welcome contributions: decision procedures or certificates for short cycles and colorings of explicit finite graphs; a straight-line embedding of $G$ with rational coordinates; lemmas on cycles and distances in graphs glued from embedded copies, which are reusable for other gadget constructions; and proofs of Lemmas 1–2 by computation or by the paper's arguments.

Selected references

• V. Cohen-Addad, M. Hebdige, D. Král', Z. Li, E. Salgado, Steinberg's Conjecture is false, J. Combin. Theory Ser. B 122 (2017), 452–456; preprint arXiv:1604.05108v2. https://arxiv.org/abs/1604.05108v2
• O. V. Borodin, Colorings of plane graphs: A survey, Discrete Math. 313 (2013), 517–539. https://doi.org/10.1016/j.disc.2012.11.011
• O. V. Borodin, A. N. Glebov, A. Raspaud, M. R. Salavatipour, Planar graphs without cycles of length from 4 to 7 are 3-colorable, J. Combin. Theory Ser. B 93 (2005), 303–331. https://doi.org/10.1016/j.jctb.2004.11.001
• D. P. Sanders, Y. Zhao, A note on the three color problem, Graphs Combin. 11 (1995), 91–94. (Reference [11] of arXiv:1604.05108v2.)
• R. Steinberg, The state of the three color problem, in: Quo Vadis, Graph Theory?, Ann. Discrete Math. 55 (1993), 211–248. (Reference [12] of arXiv:1604.05108v2.)
• M. Voigt, A non-3-choosable planar graph without cycles of length 4 and 5, Discrete Math. 307 (2007), 1013–1015. (Reference [13] of arXiv:1604.05108v2.)

Motivation

A matrix $A \in \mathbb C^{n\times n}$ is singular exactly when the pair of linear systems $\mathbf x^\top A = 0$, $A\mathbf y = 0$ has a solution with both $\mathbf x$ and $\mathbf y$ nonzero, and this is decided in polynomial time by Gaussian elimination. The natural analogue for a 3-tensor replaces the two linear systems by three families of bilinear equations, one for each way of contracting the tensor against two vectors. For tensors whose dimensions satisfy the Gelfand–Kapranov–Zelevinsky condition, solvability of that system is equivalent to the vanishing of the hyperdeterminant, and for any tensor it is equivalent to $0$ being a singular value in the sense of Lim (2005). The same system appears in multiview geometry (Cohen and Tomasi 1997).

C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013; arXiv:0911.1393), show that, unlike the matrix case, this feasibility question is NP-hard over $\mathbb R$ and over $\mathbb C$ (their Theorem 3.7). The proof is a reduction from graph 3-colorability through the polynomial color encoding of a graph, an idea the authors trace to Bayer's thesis (1982) and to Lovász (1994) and De Loera (1995). This mission formalizes that reduction and its consequence for tensor singular values (Theorem 6.2).

Setting

A 3-tensor over a field $F$ is an array $\mathcal A = [\![a_{ijk}]\!] \in F^{l\times m\times n}$. Its slices are the matrices $A_i(j,k) = B_j(i,k) = C_k(i,j) = a_{ijk}$, all read off the same array.

Tensor bilinear feasibility (Problem 3.1) asks, for a rational tensor $\mathcal A \in \mathbb Q^{l\times m\times n}$ and $F = \mathbb R$ or $\mathbb C$, whether the system (9)

$$\mathbf v^\top A_i\mathbf w = 0\ (i \le l),\qquad \mathbf u^\top B_j \mathbf w = 0\ (j \le m),\qquad \mathbf u^\top C_k \mathbf v = 0\ (k \le n)$$

has a solution $\mathbf u \in F^l$, $\mathbf v\in F^m$, $\mathbf w \in F^n$ with each of the three vectors nonzero. In Lean this is TBF A.

The color encoding $C_G$ of a graph $G = (V,E)$ on $v$ vertices (Definition 2.9) is the set of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$:

$$x_iy_i - z^2,\quad y_iz - x_i^2,\quad x_iz - y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2 + x_ix_j + x_j^2),\qquad i = 1,\dots,v .$$

The tensor $\mathcal A_G \in \mathbb Z^{l\times m\times n}$ of the proof of Theorem 3.7 has $m = n = 2v+1$ and $l = v(2v+5)$ slices: $v(2v+1)$ slices whose bilinear forms are the $2\times 2$ minors of the matrix $[\mathbf v\ \mathbf w]$, then $3v + v$ slices whose bilinear forms restrict, on $\mathbf w = \mathbf v$, to the polynomials of $C_G$ (Lean: AG G).

The tensor $\mathcal B$ of Lemma 3.6 doubles a real tensor $\mathcal A$ into $\mathbb R^{2l\times 2m\times 2n}$ through the slices $B_i = \left[\begin{smallmatrix} A_i & 0 \\ 0 & -A_i\end{smallmatrix}\right]$, $B_{l+i} = \left[\begin{smallmatrix} 0 & A_i \\ A_i & 0\end{smallmatrix}\right]$ (Lean: doubling A).

An $\ell^2$-singular value $\sigma$ of $\mathcal A$ (Definition 6.1) admits nonzero $\mathbf u,\mathbf v,\mathbf w$ with $\sum_{j,k}a_{ijk}v_jw_k = \sigma u_i$ and the two analogous equations; an $\ell^3$-singular value has $\sigma u_i^2$, $\sigma v_j^2$, $\sigma w_k^2$ on the right. At $\sigma = 0$ both reduce to (9).

Formalization targets

Goal: Theorem 3.7

$$\textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb R} \quad\text{and}\quad \textsf{3-COLORABILITY} \le_p \textsf{TBF}_{\mathbb C},$$

polynomial-time many-one reductions between languages of binary codes. NP-hardness of tensor bilinear feasibility then follows from the NP-completeness of 3-colorability (Karp 1972), which is cited and not part of the statement.

Milestones, in the order the proof uses them

1. Lemma 2.10. $C_G$ has a nonzero complex zero iff $G$ is 3-colorable.
2. The minors (proof of Theorem 3.7). For nonzero $\mathbf v, \mathbf w \in \mathbb C^N$, all $2\times2$ minors of $[\mathbf v\ \mathbf w]$ vanish iff $\mathbf v = c\mathbf w$ for some $c \in \mathbb C$.
3. Correctness over $\mathbb C$ (proof of Theorem 3.7). For $v \ge 1$, $\mathrm{TBF}_{\mathbb C}(\mathcal A_G) \iff G$ is 3-colorable.
4. Lemma 3.6. $\mathrm{TBF}_{\mathbb R}(\mathcal B) \iff \mathrm{TBF}_{\mathbb C}(\mathcal A)$ for real $\mathcal A$.
5. Theorem 6.2 (further result). 3-colorability reduces to deciding whether $0$ is an $\ell^2$-singular value, and whether it is an $\ell^3$-singular value, over $\mathbb R$ and over $\mathbb C$.

Significance

Theorem 3.7 is the hub of the paper's bilinear results: Section 6 derives from it the NP-hardness of deciding whether $0$ is a tensor singular value (Theorem 6.2), and the triple bilinear problem (Theorem 3.8) is handled by the same techniques. It separates tensors from matrices in a precise sense: the matrix analogue of (9) is decided by a determinant, while the tensor version encodes a classical NP-complete problem. It does not settle the hardness of the hyperdeterminant, since the dimensions $l = v(2v+5)$, $m = n = 2v+1$ of $\mathcal A_G$ violate the GKZ condition; the paper leaves that as a conjecture.

The result is proved in the paper; none of it is formalized on Prove2Me or, to our knowledge, elsewhere. A complete development produces a machine-checked polynomial-time reduction in Cook's Turing-machine model between two concrete algebraic problems, the color-encoding lemma for 3-colorability (reusable by any reduction that goes through polynomial systems, including Theorems 1.3 and 2.6 of the same paper), and the realification of bilinear systems.

Difficulty

The algebra of the reduction is short; two places need care. First, the bilinear system does not see $C_G$ directly: (9) involves two independent vectors $\mathbf v, \mathbf w$, and the reduction recovers the quadratic system only because the minors force $\mathbf v = c\mathbf w$, which requires both vectors to be nonzero. Second, the converse direction must produce a nonzero $\mathbf u$ satisfying the second and third families, a homogeneous linear system of $4v+2$ equations in $l = v(2v+5)$ unknowns; this works only when $l > 4v+2$, which fails for the empty graph, so the reduction has to treat $v = 0$ separately.

The goal also asks for polynomial-time computability in a Turing-machine model: decoding a graph code, rejecting malformed words, and writing the binary code of $\mathcal A_G$ (or of its doubling over $\mathbb R$). This bookkeeping, not the algebra, is the bulk of a complete proof.

Formalization scope

• Tensors are functions I → J → K → F over finite index types, 0-based: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). Problem 3.1 requires $\mathbf u$, $\mathbf v$, $\mathbf w$ each nonzero, not merely $(\mathbf u, \mathbf v, \mathbf w) \neq 0$, and the three equation families come from one tensor.
• The doubled tensor of Lemma 3.6 is indexed by I ⊕ I, J ⊕ J, K ⊕ K, with Sum.inr i standing for the paper's index $l+i$. Lemma 3.6 is stated for this explicit $\mathcal B$; a bare existential would be witnessed by any tensor with the right truth value. Only the equivalence of existence is stated, not the paper's "one-to-one" correspondence (which pairs $\mathbf u' = (\mathbf p,\mathbf q)$ with the conjugate-type vector $\mathbf p - i\mathbf q$).
• The paper does not print the matrices of the last $4v$ slices of $\mathcal A_G$. The mission fixes the bilinearizations $x_i\hat y_i - z\hat z$, $y_i\hat z - x_i\hat x_i$, $x_i\hat z - y_i\hat y_i$ and $\sum_{j\sim i}(x_i\hat x_i + x_i\hat x_j + x_j\hat x_j)$; each restricts to the printed polynomial on $\mathbf w = \mathbf v$.
• "Nontrivial zero" in the minors claim is read as both $\mathbf v$ and $\mathbf w$ nonzero; the correctness milestone over $\mathbb C$ assumes $v \geq 1$, since for $v = 0$ the printed tensor has no slices and its system (9) is infeasible.
• "Polynomially reducible" is formalized as Cook–Karp many-one reducibility (CookPvsNP.PolyReducible), which the paper's proof constructs and which implies the paper's oracle notion of §1.4. "NP-hard" in Theorem 6.2 is rendered the same way, and "($\ell^2$ or $\ell^3$)" as the claim for each notion. Rational inputs are coded as numerator and denominator in binary; tensors as $l, m, n$ and then their entries in lexicographic order.
• The singular-value equations (20)–(21) are taken literally over $\mathbb C$, without conjugates and without normalization; only $\sigma = 0$ is used, where they are scale-free.
• NP-completeness of 3-colorability is cited, not formalized; no statement mentions P, NP-membership, or hyperdeterminants.
• A trivializing formalization is ruled out: the goal is the polynomial-time reduction, not the bare equivalence of yes-instances, and the reduction must handle every input word.

The mission reuses the published definitions CookPvsNP_defs (Turing machines, polynomial-time computability, many-one reducibility) and ProjSchedTW.Complexity.Encoding (the binary alphabet and number codes), and Mathlib's SimpleGraph.Colorable. Contributions welcome: the algebraic milestones (Lemma 2.10, the minors, Lemma 3.6) are independent and self-contained; a library of polynomial-time computable list and arithmetic operations on BSym codes would serve both this goal and Theorem 6.2.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Art. 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393)
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP, 2005. https://arxiv.org/abs/math/0607648
• I. M. Gelfand, M. M. Kapranov, A. V. Zelevinsky, Discriminants, Resultants, and Multidimensional Determinants, Birkhäuser, 1994. https://doi.org/10.1007/978-0-8176-4771-1
• S. A. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Eigenvalues of matrices are computable in polynomial time to any accuracy, and numerical linear algebra rests on that fact. Higher-order tensors appear in statistics (moment and cumulant tensors), signal processing, quantum information and polynomial optimization, and several notions of tensor eigenvalue were proposed for them, independently by Lim and by Qi in 2005 (Lim 2005; Qi 2005). Hillar and Lim (J. ACM 60(6), 2013, Art. 45; arXiv:0911.1393) showed that most of the natural tensor analogues of tractable matrix problems are NP-hard. Their first example, Theorem 1.3, concerns the simplest one: deciding whether a given number is an eigenvalue of a 3-tensor.

This mission formalizes that theorem together with the lemmas its proof uses. The reduction starts from graph 3-colorability, and its intermediate step, quadratic feasibility (Theorem 2.6), is reused throughout the paper: the bilinear, singular value and triple-bilinear results all go through the same color encoding.

Setting

A 3-tensor over a field $F$ is an array $\mathcal A=[\![a_{ijk}]\!]\in F^{n\times n\times n}$. A scalar $\lambda\in F$ is an eigenvalue of $\mathcal A$ (eq. (3) of the paper) if there is a nonzero $\mathbf x\in F^n$ with

$$\sum_{i,j=1}^{n}a_{ijk}\,x_ix_j=\lambda x_k,\qquad k=1,\dots,n.$$

The sum is over the first two indices. For $\lambda=0$ the condition is invariant under scaling of $\mathbf x$, so no normalization enters.

Problem 1.2 (tensor $\lambda$-eigenvalue) fixes $F\in\{\mathbb R,\mathbb C\}$ and $\lambda\in\mathbb Q$, and asks, for a rational tensor $\mathcal A\in\mathbb Q^{n\times n\times n}$, whether $\lambda$ is an eigenvalue of $\mathcal A$ with an eigenvector in $F^n$.

Problem 2.2 (quadratic feasibility) asks, for rational matrices $A_1,\dots,A_m\in\mathbb Q^{n\times n}$, whether the system $\mathbf x^\top A_i\mathbf x=0$ ($i=1,\dots,m$) has a nonzero solution $\mathbf x\in F^n$.

A proper 3-coloring of a simple graph $G=(V,E)$ assigns one of three colors to each vertex so that adjacent vertices receive different colors.

The color encoding $C_G$ of a graph on vertices $1,\dots,v$ (Definition 2.9) is the family of $4v$ quadratics in $x_1,\dots,x_v,y_1,\dots,y_v,z$:

$$x_iy_i-z^2,\quad y_iz-x_i^2,\quad x_iz-y_i^2,\quad \sum_{j:\{i,j\}\in E}(x_i^2+x_ix_j+x_j^2),\qquad i=1,\dots,v.$$

Lemma 2.7 replaces a complex quadratic system by a real one of twice the size, and Lemma 2.8 pads a real system to a square one. Applied to $C_G$, they give $N$ real quadratics $\mathbf x^\top B_k\mathbf x$ in $N$ unknowns. The tensor $T_G$ with $a_{ijk}=(B_k)_{ij}$ is the output of the reduction.

Formalization targets

Goal: Theorem 1.3

$$\textsf{3-COL}\ \le_p\ \textsf{TENSOR-0-EIG}_{\mathbb R}.$$

Graph 3-colorability is polynomial-time many-one reducible to the language of binary codes of rational tensors having $0$ as a real eigenvalue.

Milestones, in the order the proof uses them

1. Lemma 2.10. $C_G$ has a nonzero complex solution if and only if $G$ is 3-colorable.
2. Lemma 2.7. The $2m$ real equations with matrices $\begin{bmatrix}A_i&0\\0&-A_i\end{bmatrix}$ and $\begin{bmatrix}0&A_i\\A_i&0\end{bmatrix}$ have a nonzero real solution iff $\{\mathbf z^\top A_i\mathbf z=0\}$ has a nonzero complex solution.
3. Lemma 2.8. Padding to $r\ge m+1$ equations in $s\ge n$ unknowns preserves real feasibility.
4. Theorem 2.6. $\textsf{3-COL}\le_p$ quadratic feasibility over $\mathbb R$ and over $\mathbb C$.
5. Proof of Theorem 1.3, first step. $0$ is a real eigenvalue of $\mathcal A$ iff the square system $\mathbf x^\top A_k\mathbf x=0$, $A_k(i,j)=a_{ijk}$, has a nonzero real solution.
6. Proof of Theorem 1.3, the construction. $G$ is 3-colorable iff $0$ is a real eigenvalue of $T_G$.

Significance

The result. Theorem 1.3 shows that deciding whether $0$ is an eigenvalue of a rational 3-tensor over $\mathbb R$ is NP-hard, in contrast to the matrix case. Because the instance is a single rational tensor with small integer entries, the hardness does not come from numerical precision: it is a property of the exact problem. The same encoding underlies the paper's hardness of approximating an eigenvector (Theorem 1.5) and its remarks on counting eigenvectors (Corollary 1.16).

Formalizing it. The result is proved in the paper, but no part of it is machine-checked. The mission adds three things. It gives a precise language-level statement of what "polynomially reducible" means for this problem. It gives a checked equivalence between 3-colorability and the eigenvalue condition for the explicit tensor $T_G$. And it gives reusable statements about homogeneous quadratic systems (realification and padding), which the bilinear and singular value missions of this series also need.

Difficulty

The algebraic core is Lemma 2.10, and its reverse direction is where a first attempt fails. The fourth family of $C_G$ does not say that each term $x_i^2+x_ix_j+x_j^2$ vanishes; it says only that their sum over the neighbours of $i$ vanishes, over $\mathbb C$, where nonzero terms can cancel. A common zero yields a coloring only after the first three families have pinned down each coordinate, and the case $z=0$ must be excluded separately.

Lemma 2.7 needs care because the matrices $A_i$ are not assumed symmetric: the imaginary part of $\mathbf z^\top A\mathbf z$ is $\mathbf u^\top A\mathbf v+\mathbf v^\top A\mathbf u$, not $2\mathbf u^\top A\mathbf v$. Lemma 2.8 uses that $\mathbb R$ is formally real; it fails over $\mathbb C$.

At the language level, the reduction must be exhibited as a Turing machine computation on binary codes in polynomial time. That is bookkeeping, but it is the part the paper does not write down.

Formalization scope

• Tensors and vectors. Tensors are arrays Fin n → Fin n → Fin n → F, vectors Fin n → F, and indices are 0-based. The eigenvalue condition is eq. (3) verbatim, without normalization; for $\lambda=0$ none is needed. Rational data are cast into $\mathbb R$ or $\mathbb C$.
• Quadratic polynomials. A homogeneous quadratic is a (not necessarily symmetric) rational matrix $M$, read as $\mathbf x^\top M\mathbf x$, and the monomial $x_ax_b$ is the matrix unit $E_{ab}$. A vertex without neighbours contributes the zero polynomial to $C_G$.
• Choices in the construction. The square size is $N=8v+2$. It meets Lemma 2.8's bounds $r\ge 8v+1$ and $s\ge 4v+2$ for every $v\ge 0$; Example 1.4's count differs and is not used.
• Reducibility. "Polynomially reducible" is Cook's polynomial-time many-one reducibility (CookPvsNP.PolyReducible, published definition CookPvsNP_defs). The paper's reduction maps one graph to one tensor, and a many-one reduction implies the oracle notion of its §1.4.
• Binary codes. Instances are coded over the alphabet BSym with the binary codes of the published definition ProjSchedTW.Complexity.Encoding. A graph is $\nu$ followed by its adjacency matrix. A rational is its numerator then its denominator. A tensor is $n$ followed by its entries in lexicographic order. The target language contains all rational tensors, not only integral ones.
• Not formalized. NP-completeness of 3-colorability (Karp 1972) is cited, not formalized, and the goal states only the reduction. Approximation (Theorem 1.5), counting (Corollary 1.16) and the solution count of Example 1.4 are out of scope.
• Trivializations ruled out. Every feasibility statement requires a nonzero solution, since the zero vector solves every homogeneous system. The goal includes polynomial-time computability of the reduction, not just the existence of an equivalence-preserving map, which would be trivial. The milestones concern the paper's explicit $C_G$ and $T_G$, not an arbitrary tensor.

Contributions are welcome in four places:

• proofs of the milestones;
• a polynomial-time Turing machine computing $G\mapsto T_G$ on codes;
• general lemmas on homogeneous quadratic systems over formally real fields;
• a composition (transitivity) lemma for CookPvsNP.PolyReducible.

Selected references

• C. J. Hillar and L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393)
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 2005, pp. 129–132. https://doi.org/10.1109/CAMAP.2005.1574201
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40(6), 2005, pp. 1302–1324. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, pp. 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problem description, 2000. https://www.claymath.org/millennium/p-vs-np/

Motivation

The Hadwiger–Nelson problem asks for the chromatic number of the plane $\chi(\mathbb R^2)$: the least number of colours needed to colour every point of the Euclidean plane so that any two points at distance exactly $1$ receive different colours. Equivalently, it is the chromatic number of the infinite graph whose vertices are the points of the plane and whose edges are the unit-distance pairs. Since 1950 the answer has been known to lie between $4$ and $7$, and it is one of the best known open problems in combinatorial geometry. Its difficulty is that the colour classes may be arbitrary sets: no measurability or regularity is assumed, so analytic tools that work for measurable colourings do not apply directly.

This mission asks for a formal proof that five colours do not suffice, as claimed in an OpenAI preprint dated September 23, 2026 (source), so that $6\le\chi(\mathbb R^2)\le7$. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1950 — Nelson poses the problem and observes $\chi\ge4$; Isbell finds a hexagonal $7$-colouring (recounted by Soifer, Mathematics Competitions 2003).
• 1951 — de Bruijn and Erdős: an infinite graph is $k$-colourable iff every finite subgraph is (Indag. Math. 1951).
• 1961 — Hadwiger publishes the problem with bounds $4$ and $7$ (Elem. Math. 1961); the Moser spindle gives a 7-vertex obstruction to three colours (Canad. Math. Bull. 1961).
• 1973–2005 — Woodall studies region colourings (JCTA 1973); Townsend proves map-type colourings need six colours (JCTA 1981; Geombinatorics 2005).
• 1981 — Falconer proves that measurable colourings need at least five colours (JCTA 1981).
• 2018–2020 — de Grey constructs a finite unit-distance graph that is not $4$-colourable, so $\chi\ge5$ (arXiv:1804.02385); Heule and Parts shrink it (arXiv:1805.12181, arXiv:2010.12665); Exoo–Ismailescu give another proof (DCG 2020).
• 2025 — Sokolov and Voronov prove seven colours are needed for polygonal map-type colourings (arXiv:2502.01958).
• September 2026 — The OpenAI preprint claims $\chi(\mathbb R^2)\ge6$ for arbitrary colourings (Theorem 1.1, p. 2).

Setting

A proper $k$-colouring of the plane is any function $c:\mathbb R^2\to\{1,\dots,k\}$ such that $c(x)\ne c(y)$ whenever $\|x-y\|=1$, with $\|\cdot\|$ the Euclidean norm. No measurability, continuity or regularity of the colour classes $c^{-1}(i)$ is assumed. $\chi(\mathbb R^2)$ is the least $k$ admitting a proper $k$-colouring.

Formalization targets

Milestone: the upper bound $\chi(\mathbb R^2)\le7$ (Theorem 1.1, p. 2)

There is a proper $7$-colouring of the plane: colour the Voronoi hexagons of a triangular lattice (circumradius $r=2/5$) by the seven cosets of an index-seven similar sublattice, assigning boundary points to any incident hexagon. This classical construction is reproved in the deduction of Theorem 1.1 (pp. 2–3), including all boundary points.

Goal: no proper five-colouring (Theorem 1.1, p. 2)

There is no function $c:\mathbb R^2\to\{1,\dots,5\}$ with $c(x)\ne c(y)$ whenever $\|x-y\|=1$. Together with the milestone this gives $6\le\chi(\mathbb R^2)\le7$.

Significance

The result itself. It raises the lower bound for the chromatic number of the plane from five (de Grey, 2018) to six, leaving only $6$ and $7$. Unlike de Grey's bound it is not witnessed by a finite graph; the proof transfers the problem to measurable colourings for every number of colours (Theorem 1.3, p. 2) and then excludes weak measurable five-colourings (Theorem 1.4, p. 2). The transfer theorem is of independent interest: in ZFC, a proper $k$-colouring exists iff a weak measurable $k$-colouring does. The preprint also derives a positive lower bound on the invariant-mean frequency of monochromatic unit pairs for every five-colouring (Corollary 1.5, p. 5).

Formalizing it. The statements are elementary, but the proof uses ergodic theory (a Furstenberg–Zimmer compact-extension tower and rigidity of invariant measures on a character group, Theorem 2.3, p. 6), spectral theory, density points, Fourier decay of circle measure, and planar topology. A formal proof would remove any doubt about a long and varied argument. The finite-graph bound $\chi\ge5$ has been checked by SAT solvers, but no formal proof of a bound that is not witnessed by a finite graph is known.

Difficulty

By de Bruijn–Erdős, $\chi\ge6$ is equivalent to the existence of a finite unit-distance graph that is not $5$-colourable, but no such graph is known, and SAT-based searches have not produced one. Measurable methods (Falconer's density-point argument) cannot be applied to arbitrary colour classes, and a measurable colouring can have boundaries far too irregular for map-type interface arguments such as Townsend's or Sokolov–Voronov's. The preprint must therefore (i) produce measurable data from an arbitrary colouring without losing the unit-distance exclusions, via invariant averaging over algebraic rotations and translations and the rigidity Theorem 2.3, and (ii) construct the connected interfaces needed for a geometric contradiction from measure estimates alone (Sections 5–7), before excluding label cycles of length $3$, $4$ and $5$ (Section 8).

Formalization scope

• The goal works in ℂ with ‖p - q‖ = 1; a colouring is any function ℂ → Fin 5. ProperColoring 5 c requires distinct colours at every unit-distance pair. No measurability is assumed, so the statement is about arbitrary colourings, as in the source.
• The milestone works in EuclideanSpace ℝ (Fin 2) with dist x y = 1 and asks for some c : Plane → Fin 7; the two planes are isometric.
• Both statements are in ZFC-style classical Lean; no choice-free reading is intended. Neither is vacuous.

Welcome contributions: the de Bruijn–Erdős compactness theorem, the Moser spindle, Lebesgue density points in $\mathbb R^2$, and the measurable/unrestricted transfer of Theorem 1.3.

Selected references

• OpenAI, The Euclidean plane is not five-colorable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf
• H. Hadwiger, Ungelöste Probleme Nr. 40, Elem. Math. (1961).
• L. Moser, W. Moser, Solution to Problem 10, Canad. Math. Bull. (1961). https://doi.org/10.1017/S0008439500025765
• N. G. de Bruijn, P. Erdős, A colour problem for infinite graphs and a problem in the theory of relations, Indag. Math. (1951). https://users.renyi.hu/~p_erdos/1951-01.pdf
• K. J. Falconer, The realization of distances in measurable subsets covering $\mathbb R^n$, J. Combin. Theory Ser. A (1981). https://doi.org/10.1016/0097-3165(81)90014-5
• D. R. Woodall, Distances realized by sets covering the plane, J. Combin. Theory Ser. A (1973). https://doi.org/10.1016/0097-3165(73)90020-4
• S. P. Townsend, Every 5-coloured map in the plane contains a monochrome unit, J. Combin. Theory Ser. A (1981). https://doi.org/10.1016/0097-3165(81)90046-7
• A. D. N. J. de Grey, The chromatic number of the plane is at least 5, Geombinatorics (2018). https://arxiv.org/abs/1804.02385v3
• M. J. H. Heule, Computing small unit-distance graphs with chromatic number 5, Geombinatorics (2018). https://arxiv.org/abs/1805.12181
• G. Exoo, D. Ismailescu, The chromatic number of the plane is at least 5: a new proof, Discrete Comput. Geom. (2020). https://doi.org/10.1007/s00454-019-00058-1
• G. Sokolov, V. Voronov, On the chromatic number of the plane for map-type colorings, arXiv:2502.01958 (2025). https://arxiv.org/abs/2502.01958v1
• A. Soifer, The 50th anniversary of one problem: the chromatic number of the plane & its relatives, Mathematics Competitions (2003). https://www.wfnmc.org/Journal%202003%201.pdf

Motivation

Scheduling jobs on identical parallel machines to minimize the total weighted completion time $\sum_j w_jC_j$, the problem $P\,|\,|\sum w_jC_j$, is one of the basic NP-hard problems of machine scheduling. On a single machine it is solved by Smith's ratio rule (Smith 1956); with several machines the only hard decision is which jobs share a machine. Section 6 of M. Skutella's paper Convex quadratic and semidefinite programming relaxations in scheduling (J. ACM 48 (2001)) observes that this decision is a graph partitioning problem: the cost of a schedule is, up to a constant, the weight of the edges that a partition of a weighted complete graph does not cut. Minimizing $\sum_j w_jC_j$ on $m$ machines is therefore equivalent to Max-$m$-Cut on that graph, and the paper shows that the equivalence preserves approximation in a quantified way.

The reduction explains, from the graph side, why semidefinite rounding works for two machines: with the 0.878-approximation for MaxCut of Goemans and Williamson (1995) it gives a 1.122-approximation for $P2\,|\,|\sum w_jC_j$ (Corollary 6.2 of the paper). For general $m$, the uniform random partition is both a $(1-1/m)$-approximation for Max-$m$-Cut and randomized rounding of the optimum of the convex quadratic relaxation (CQP).

Setting

There are $n$ jobs $J=\{1,\dots,n\}$ and $m\ge 1$ identical machines. Job $j$ has a processing time $p_j>0$ and a weight $w_j\ge 0$. Smith's order $\prec$ puts $j\prec k$ when $w_j/p_j>w_k/p_k$, ties broken by index. An assignment $\sigma:J\to\{1,\dots,m\}$ is a partition $J_1,\dots,J_m$ of the jobs; each machine processes its jobs in the order $\prec$ without idle time, so the completion time of $j$ is

$$C_j(\sigma)=p_j+\sum_{k\prec j,\ \sigma(k)=\sigma(j)}p_k .$$

The value of $\sigma$ is $\sum_j w_jC_j(\sigma)$, and $Z^*$ is the minimum value over all assignments.

The graph $G_J$ is the complete graph on $J$ in which the edge $\{j,k\}$ with $k\prec j$ has weight $c(jk)=w_jp_k$; $c(E_J)$ is its total weight. A partition induces the $m$-cut $E_{\mathrm{cut}}$, the edges whose endpoints lie in different parts, of weight $c(E_{\mathrm{cut}})$; $Z^*_{\mathrm{cut}}$ is the maximum weight of an $m$-cut.

The convex quadratic relaxation (CQP) of §2.2, specialised to identical machines, has variables $a_{ij}\ge 0$ with $\sum_i a_{ij}=1$ and objective $Z_{CQP}(a)=\sum_j w_jC_j$ where

$$C_j=\sum_{i=1}^m a_{ij}\Big(\frac{1+a_{ij}}{2}\,p_j+\sum_{k\prec j}a_{ik}\,p_k\Big)\qquad(11).$$

Its optimum value is $Z^*_{CQP}$.

Formalization targets

Goal: Theorem 6.1

For $\rho\le 1$, any assignment $\sigma$ whose $m$-cut weighs at least $\rho\cdot Z^*_{\mathrm{cut}}$ satisfies

$$\sum_j w_jC_j(\sigma)\le\big(\rho+m(1-\rho)\big)\,Z^* .$$

That is, a $\rho$-approximation algorithm for Max-$m$-Cut translates into a $(\rho+m(1-\rho))$-approximation algorithm for $Pm\,|\,|\sum w_jC_j$. The constant $\rho$ is a parameter, so the goal does not depend on the best known cut algorithm.

Milestones

1. (36): for every partition, $c(E_J)=\sum_j w_jC_j-\sum_j w_jp_j+c(E_{\mathrm{cut}})$.
2. Lemma 2.5: $\bar a_{ij}=1/m$ is an optimum of (CQP), unique when the ratios $w_j/p_j$ are pairwise different and positive.
3. (37): $Z^*\ge Z^*_{CQP}=\frac1m c(E_J)+\big(\frac12+\frac1{2m}\big)\sum_j w_jp_j$.
4. (38): $Z^*_{\mathrm{cut}}\le\frac{m-1}{m}c(E_J)+\big(\frac12-\frac1{2m}\big)\sum_j w_jp_j$.
5. Theorem 2.6 b) (supplementary): assigning each job independently and uniformly at random has expected value at most $\big(\frac32-\frac1{2m}\big)Z^*$.

Significance

The result. Theorem 6.1 makes Max-$m$-Cut algorithms usable for scheduling with an explicit loss: a cut algorithm with ratio $\rho$ close to $1$ yields a schedule within $1+m(1-\rho)$ of optimal. For $m=2$ and the Goemans–Williamson ratio $0.878$ the guarantee is $1.122$, better than the $5/4$ of Theorem 2.6 b) and the $1.2752$ of the paper's semidefinite rounding in §5. In the other direction, (38) bounds the maximum cut of $G_J$ by the scheduling lower bound $Z^*_{CQP}$, which is how a relaxation for scheduling becomes a bound for a cut problem. The problem itself is better understood today: $P\,|\,|\sum w_jC_j$ has a polynomial-time approximation scheme (Skutella and Woeginger 2000), and a fully polynomial one for fixed $m$ (Sahni 1976). The reduction remains of interest as a structural identity between the two problems and as the source of the closed-form relaxation bound (37).

Formalizing it. All statements are proved in the paper; none is known to have a machine-checked proof. The mission produces a formal model of identical-machine scheduling under Smith's rule, of the weighted graph $G_J$ and its $m$-cuts, and of (CQP) for identical machines, together with the closed-form optimum of (CQP) (Lemma 2.5), which is the basis of the $\frac32-\frac1{2m}$ guarantee of Theorem 2.6 b).

Difficulty

The bookkeeping identity (36) and the final chain of inequalities are finite-sum manipulations. The substance is Lemma 2.5: that the uniform vector $\bar a$ minimizes the quadratic objective (11) over the product of simplices. The objective is not separable, since the term $\sum_{k\prec j}a_{ik}p_k$ couples jobs through Smith's order, and its convexity on the feasible region (the positive semidefiniteness established in Lemma 2.4 of the paper) is the fact on which optimality and, with distinct positive ratios, uniqueness rest. The relaxation half of (37), that $Z^*_{CQP}$ is at most the value of every schedule, needs the observation that $Z_{CQP}$ evaluated at the 0/1 vector of an assignment equals the value of that assignment.

Formalization scope

Jobs are Fin n and machines Fin m, 0-based; Smith's order is cross-multiplied ($w_jp_k>w_kp_j$, or equality and $j<k$), equal to the ratio definition because $p>0$. Assignments are functions Fin n → Fin m, and every machine is sequenced by $\prec$; by Smith's rule (p. 7 of the paper, a classical result it cites) this loses no optimality, so $Z^*$ is the minimum over assignments and is never a primitive: "within factor $\alpha$ of $Z^*$" is stated against the value of every assignment. Likewise "weight at least $\rho\cdot Z^*_{\mathrm{cut}}$" is stated as $\rho\,c(E_{\mathrm{cut}}(\tau))\le c(E_{\mathrm{cut}}(\sigma))$ for every assignment $\tau$, so no supremum of an empty or unbounded set can enter. The edge weight is attached to the ordered pair $(j,k)$ with $k\prec j$ and is zero on the other orientation, so each edge of $G_J$ is counted once. Standing hypotheses on every theorem: $p_j>0$, $w_j\ge 0$ (p. 2 of the paper) and $m>0$ (needed for $1/m$). Theorem 6.1 keeps the page's $\rho\le 1$.

Not formalized: polynomial running time, the phrase "approximation algorithm" beyond the value bound it asserts, and the semidefinite results of §5 and Corollary 6.2. A trivializing reading, such as stating the cut condition against a junk-valued supremum or replacing $Z^*$ by a free variable, is excluded by the encodings above.

The development needs only finite sums over Fin types and real arithmetic; the model of identical-machine scheduling under Smith's rule and the closed form of (CQP) are reusable for other results on $P\,|\,|\sum w_jC_j$. Proofs of the milestones, alternative proofs of Lemma 2.5 (the KKT argument the paper mentions, or Goemans' symmetrization argument it gives), and a proof of Theorem 2.6 b) are all welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• A. Frieze and M. Jerrum, Improved approximation algorithms for MAX k-CUT and MAX BISECTION, Algorithmica 18, 1997. https://doi.org/10.1007/BF02523689
• M. Skutella and G. J. Woeginger, A PTAS for minimizing the total weighted completion time on identical parallel machines, Mathematics of Operations Research 25(1), 2000. https://doi.org/10.1287/moor.25.1.63.15212
• S. Sahni, Algorithms for scheduling independent tasks, Journal of the ACM 23(1), 1976. https://doi.org/10.1145/321921.321934

Motivation

In a multihop radio network, links that are close to each other interfere, so only certain sets of links can transmit in the same time slot. Tassiulas and Ephremides (IEEE TAC 1992) modelled this as a constrained queueing system and asked which arrival rates any scheduler can sustain. Their answer has two halves. The first, Theorem 3.2, shows that a maximum-weight ("back-pressure") policy stabilizes the network for every rate vector in an explicit region $C'$, and that no stationary policy does better than its closure. The second, Theorem 4.1 and the subject of this mission, removes the restriction to stationary policies: outside the closure $\bar C'$, every scheduler, however it uses the past, lets the queues grow without bound almost surely.

The pair of results is the origin of throughput-optimal scheduling in wireless and switched networks: max-weight scheduling in input-queued switches, back-pressure routing, and the Lyapunov-drift framework of network utility maximization all start from this region and this converse. The converse is what makes "throughput-optimal" a meaningful claim: it certifies that $\bar C'$ is a hard limit, not merely the limit of one policy class.

Setting

There are $L$ queues and $N$ servers (links). Server $i$ serves queue $q(i)$ and sends each served customer to a queue $h(i)$ or out of the system. Time is slotted and a service takes one slot. An activation set is a set of servers that may be active in the same slot; the constraint set $S$ is the family of all activation sets, and assumption C.1 says that every subset of an activation set is an activation set. The activation vector of a set $c$ is its indicator vector in $\{0,1\}^N$, and $\mathrm{co}(S)$ is the convex hull of the activation vectors.

A history-dependent policy $\pi\in\tilde G$ chooses, at the start of slot $t$, an activation set $E(t)\in S$ as a function of the queue-length vectors $X(0),\dots,X(t-1)$, never activating more servers of a queue than it has customers. The queue lengths evolve by

$$X_l(t)=X_l(t-1)-\#\{i\in E(t):q(i)=l\}+\#\{i\in E(t):h(i)=l\}+A_l(t),$$

where the arrivals $A_l(t)$ are i.i.d. over $t$, independent across queues, with finite second moments and means $a_l$.

The routing matrix $R$ has $r_{li}=1$ if $h(i)=l$ and $r_{li}=-1$ if $q(i)=l$. A vector $f\ge0$ indexed by servers is an $a$-admissible flow if $a=-Rf$. The region $C'$ is the set of $a\ge0$ that admit such a flow and a point $c\in\mathrm{co}(S)$ with $f_i<c_i$ wherever $f_i>0$ and $f_i=0$ wherever $c_i=0$.

The proof uses the flow network $N_{af}$: the queues plus an originator $o$ and a terminal $d$, an edge $(o,l)$ of capacity $a_l$ for every queue, and an edge of capacity $f_k$ from $q(k)$ to $h(k)$ (or to $d$) for every server $k$. A cut is a set $W$ of queues on the originator's side; its capacity $C_{af}$ is the total capacity of the edges leaving $W\cup\{o\}$.

Formalization targets

Goal: Theorem 4.1

$$a\notin\bar C'\ \Longrightarrow\ \lim_{t\to\infty}\sum_{l=1}^L X_l(t)=\infty\quad\text{a.s., for every }\pi\in\tilde G\text{ and every initial state.}$$

Milestones, in the order the proof uses them

1. Lemma A.1: under C.1, $c\in\mathrm{co}(S)$ and $0\le x\le c$ imply $x\in\mathrm{co}(S)$.
2. Lemma 3.1 (one class, unit service): $\bar C'=\{a\ge0:\exists f\in F_a,\ c\in\mathrm{co}(S),\ f\le c\}$.
3. Lemma 4.1: if $a\notin\bar C'$, the maximum over $f\in\mathrm{co}(S)$ of the mincut capacity of $N_{af}$ is attained and is strictly below $\sum_l a_l$.
4. Corollary 4.1: there is one $\epsilon>0$ such that $\sum_{l\in W_{af}}a_l-\epsilon$ bounds the server capacity leaving $W_{af}$, for every $f\in\mathrm{co}(S)$ and every mincut.
5. (4.7), pathwise: $\sum_l X_l(t)\ge\min_{Q}\sum_{\tau=1}^t\big(\sum_{l\in Q}(A_l(\tau)-a_l)+\epsilon\big)$ for every policy and every arrival sequence.
6. (4.12): each of these $2^L$ partial sums tends to $+\infty$ almost surely.

Significance

Theorem 4.1 closes the characterization of the throughput region of a constrained queueing network. With Theorem 3.2 it says that the set of sustainable rates is $C'$ up to its boundary, for all policies and not only stationary ones, and that allowing schedules to depend on the entire history, on time, or on long-range planning cannot enlarge it. Every later throughput-optimality result for max-weight-type policies in switches and wireless networks cites this converse, and the region $\mathrm{co}(S)$ of "average activation vectors" is the standard capacity region of interference-constrained networks.

The result has been proved since 1992 and has not, to our knowledge, been machine-checked. A formalization adds a precise statement of the policy class $\tilde G$ (history-dependent, non-anticipating, never serving empty queues), a sample-path inequality (4.7) that is independent of probability and reusable for any arrival model, and a cut-based description of $\bar C'$ through Lemma 4.1 and Corollary 4.1.

Difficulty

The obvious argument fails at the policy class. For a stationary policy the queue-length process is a Markov chain and an instability argument can use its ergodic behaviour; a history-dependent policy has no such structure, and the time-average activation vector $\lambda(t)=\frac1t\sum_{\tau\le t}E(\tau)$ wanders in $\mathrm{co}(S)$ without converging. The argument must therefore find, for every possible average $\lambda$, a set of queues whose net inflow exceeds its outflow by a margin that does not depend on $\lambda$. That uniformity is the content of Lemma 4.1 and Corollary 4.1: it needs the max-flow/min-cut theorem on $N_{af}$, the continuity of the mincut capacity in $f$, the compactness of $\mathrm{co}(S)$, and Lemma A.1 to bring a maximum flow back into $\mathrm{co}(S)$. Comparing $\sum_l a_l$ with the total service capacity, or using a single fixed cut, does not work: the bottleneck set of queues depends on how the policy spreads its activations.

Formalization scope

Queues are Fin L and servers Fin N, indexed from 0. A server's destination is Option (Fin L), none meaning out of the system. $S$ is a Set (Finset (Fin N)); C.1 is a predicate, and every theorem that needs it also assumes $\emptyset\in S$ (otherwise $S$ may be empty and no policy exists). Rate vectors are Fin L → ℝ, and $C'$ includes $a\ge0$. Service times are one slot, so $M=I$. The goal's hypothesis is $a\notin\bar C'$ with $C'$ defined from flows, as in the introduction of §IV; the printed theorem uses the closure of the stability region $C$, which equals $\bar C'$ by Theorem 3.2 of the paper. A policy is a function from the history $X(0),\dots,X(t)$ to the activation set of slot $t+1$, required to choose sets in $S$ and to activate no more servers of a queue than it has customers; the queue dynamics are written in $\mathbb N$, where this requirement makes the subtraction exact. Arrivals are random vectors in $\mathbb N^L$, i.i.d. in time (iIndepFun, IdentDistrib), independent across queues, with integrable squares; $a$ is their mean, not a free parameter.

The statement does not hold vacuously: a one-queue, one-server example with constant arrivals of two customers per slot satisfies every hypothesis of the goal, including the existence of runs, and lies outside $\bar C'$ (checked in a sanity file). A formalization in which policies may see future arrivals, or may serve empty queues, or in which $a$ is unrelated to the arrival law, is a different theorem.

A complete development needs: the max-flow/min-cut theorem for finite networks with parallel edges (posed elsewhere on the platform in other encodings, not proved), continuity of a minimum of finitely many linear functions, compactness of a convex hull of finitely many points, and Mathlib's strong law of large numbers. The pathwise bound (4.7) and the cut lemmas are reusable for any interference-constrained network. Proofs of any milestone, and alternative routes to Lemma 4.1 (for instance through linear-programming duality), are welcome.

Selected references

• L. Tassiulas and A. Ephremides, Stability properties of constrained queueing systems and scheduling policies for maximum throughput in multihop radio networks, IEEE Transactions on Automatic Control 37(12):1936–1948, 1992. https://doi.org/10.1109/9.182479
• C. H. Papadimitriou and K. Steiglitz, Combinatorial Optimization: Algorithms and Complexity, Prentice-Hall, 1982 (reference [17] of the paper, for the max-flow/min-cut theorem).
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

Motivation

Many graph problems in routing, VLSI layout and scheduling ask for a cut that separates a lot of demand while cutting little capacity. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest flow equals the smallest cut. For several commodities sharing one network this equality fails, and the question becomes how far apart the two quantities can be. Leighton and Rao (J. ACM 46 (1999), extending their FOCS 1988 paper) proved that for uniform demands the gap is at most logarithmic in the number of nodes, and turned the proof into approximation algorithms for a range of NP-hard cut problems.

Their §2.4 extends the result to directed networks, where every edge carries flow in one direction only. The directed version is the one behind their approximation algorithms for directed problems, most prominently the minimum feedback arc set problem (§3 of the paper), where the cut structure of a digraph, not of its underlying undirected graph, is what matters.

Timeline. Ford and Fulkerson (1956): max-flow = min-cut for one commodity. Hu (1963): equality for two commodities in undirected graphs. Shahrokhi and Matula (1990, circulated 1986): the uniform concurrent flow problem and its LP dual. Leighton and Rao (FOCS 1988; J. ACM 1999): $\Omega(\mathcal S/\log n)\le f\le\mathcal S$ for uniform and product demands, undirected and directed, tight up to the constant for undirected uniform problems. Klein, Rao, Agrawal and Ravi (1990s) and Linial, London and Rabinovich (1995) extended the undirected theorem to general demands with an $O(\log k)$ gap. For directed graphs with general demands the gap is polynomial in $n$ (Chuzhoy and Khanna 2009), so the uniform-demand directed theorem is the setting where a logarithmic gap holds.

Setting

A directed network is a finite vertex set $V$ with $n=|V|$ nodes and a capacity $C(u,v)\ge0$ for each ordered pair, with $C(u,u)=0$; there is an edge directed from $u$ to $v$ when $C(u,v)>0$. For $U\subseteq V$ write $\bar U=V\setminus U$ and let $C(U,\bar U)=\sum_{u\in U,\,v\in\bar U}C(u,v)$ be the capacity of the edges directed from $U$ to $\bar U$.

The directed uniform multicommodity flow problem (directed UMFP) has one commodity for every ordered pair $(u,v)$ with $u\ne v$, each with demand $1$. A concurrent flow of value $\lambda$ routes $\lambda$ units of every commodity simultaneously, each edge carrying flow only in its own direction, with total flow on the edge $u\to v$ at most $C(u,v)$. The max-flow $f$ is the largest such $\lambda$.

The ratio cost of a cut is $C(U,\bar U)/(|U|\,|\bar U|)$, and the min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

A distance function assigns a length $d(u,v)\ge0$ to each directed edge; $d(u,v)$ then also denotes the length of a shortest directed path from $u$ to $v$, its total weight is $W=\sum_{u,v}C(u,v)\,d(u,v)$, and the distance constraint is $\sum_{(u,v)\in V^2}d(u,v)\ge1$. The sets $\mathcal N^\Delta_{\mathrm{in}}(v,G)$ and $\mathcal N^\Delta_{\mathrm{out}}(v,G)$ are the nodes from which $v$ can be reached, respectively which can be reached from $v$, by a directed path of length at most $\Delta$. Logarithms are to base $2$.

In Lean these are DiNetwork, diCutCap, diRatio, diMinCut, diDemand, IsDiConcurrentFlow, diMaxFlow, diDist, diTotalWeight, SatisfiesDiConstraint, inBall and outBall, in the namespace LeightonRao.Directed.

Formalization targets

Goal: Theorem 12 (p. 804)

There is an absolute constant $c>0$ such that every directed UMFP on $n\ge2$ nodes satisfies

$$c\,\frac{\mathcal S}{\log n}\le f\le\mathcal S.$$

The constant is left unfixed, as in the paper's $\Omega(\cdot)$; any improvement of the constant leaves the goal intact.

Milestones

1. Weak duality (p. 804): every concurrent flow of value $\lambda$ has $\lambda|U||\bar U|\le C(U,\bar U)$ for every proper cut.
2. LP duality (§2.2, p. 796, used for directed graphs in §2.4): every feasible distance function has $W\ge f$, and an optimal one has $W=f$.
3. Lemma 13 (p. 804): for every $\Delta>0$, an ordered partition $V_1,\dots,V_r$ whose backward edges (from $V_i$ to $V_j$, $j<i$) have capacity at most $8W\log n/\Delta$, each part containing a node whose in- and out-balls of radius $\Delta$ are at least as large as the part.
4. Corollary 14 (p. 806): with $\Delta=1/4n^2$, either a node whose in- and out-balls both have at least $2n/3$ nodes, or a directed cut of ratio cost at most $8W\log n/(\Delta(n/6)(5n/6))$.
5. Lemma 15 (p. 806): a set $T$ with $|T|\ge2n/3$ and $\sum_{u\notin T}d(T,u)\ge1/4n$ or $\sum_{u\notin T}d(u,T)\ge1/4n$ gives a directed cut of ratio cost at most $12W$.
6. Lemma 16 (p. 807): a distance function satisfying the distance constraint gives a directed cut of ratio cost at most $\tfrac{1152}{5}W\log n$.

Significance

The result. Theorem 12 says that the directed sparsest cut and the directed uniform concurrent flow agree within an $O(\log n)$ factor. Since the flow is an LP, this gives an $O(\log n)$-approximation for the directed uniform sparsest cut, and through divide and conquer, polylogarithmic approximations for directed problems such as minimum feedback arc set and minimum directed cut linear arrangement (§3 of the paper). It is also the case in which a logarithmic flow–cut gap survives for digraphs: with arbitrary demands, the directed gap is polynomial.

Formalizing it. The theorem has been proved since 1988, but no part of it is formalized: Mathlib has no multicommodity flows, no directed path metrics over real lengths, and no region-growing arguments. This mission produces the directed concurrent-flow model, its LP duality, and the directed region-growing decomposition of Lemma 13, each reusable beyond this paper (directed multicut, feedback arc set, low-diameter decompositions of digraphs).

Difficulty

The obvious route copies the undirected proof: grow a ball around a node until the capacity on its boundary is small compared with the capacity inside, cut it off, and repeat. In a digraph this fails at two places. A ball of small out-radius can have large in-radius, so a piece cut off by out-distances is not small in the sense needed later; and cutting off a piece only controls the edges leaving it in one direction, so edges pointing back into earlier pieces are not paid for. Lemma 13 has to bound the capacity of all backward edges of an ordered partition while keeping each part inside both an in-ball and an out-ball around one of its own nodes. The final averaging step also changes: the undirected argument sums $d(T,u)+d(T,v)$ over symmetric pairs, which has no directed counterpart, so the distance constraint over ordered pairs has to be split between distances into one set and out of another.

Formalization scope

Vertices form a Fintype with decidable equality, and every goal-level statement assumes $n\ge2$. Commodities are ordered pairs with demand $1$; a flow is in arc form, $f_{st}(i,j)\ge0$ with conservation, and the capacity constraint is per directed edge. The max-flow is the supremum (sSup) of the achievable values $\lambda\ge0$; the min-cut is an infimum over nonempty proper subsets, since the ratio is $0/0$ otherwise. Shortest-path distances are infima over directed walks (lists of vertices along edges of positive capacity); for nonnegative lengths these equal shortest-path lengths. An unreachable pair would get Lean's junk value $0$, so every statement using $d(u,v)$ assumes strong connectivity ($C(U,\bar U)>0$ for every proper $U$), the directed analogue of the paper's standing assumption on p. 789; the balls are defined through the existence of a walk and need no such assumption. $W$ counts each directed edge once, and the distance constraint sums over ordered pairs. "We can find" is read as existence; running times are not formalized. The $\Omega$ of Theorem 12 is one absolute constant chosen before the network; the explicit constants $8$, $1152/5$ and $12$ of the milestones are the ones computed in the paper's proofs.

Two printed slips are corrected and disclosed: Lemma 13 (1) prints $1\le j<i<r$ where the proof uses $i\le r$, and the proof's last line prints $|\mathcal N^\Delta_{\mathrm{out}}(v,G)|\le|V_i|$ where the statement has $\ge$.

The statement cannot be trivialized by a degenerate cut or flow: cuts range over nonempty proper subsets, the flow's capacity constraint is directional, and the goal's constant is quantified before the network, so a constant depending on $n$ does not count.

Needed infrastructure: LP duality for the concurrent flow LP (or a direct proof of the max-flow/distance duality), shortest directed paths with real lengths, and the region-growing bookkeeping. Contributions to any milestone are welcome, as are alternative proofs of Lemma 13 by continuous region growing.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
• N. Linial, E. London and Yu. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• J. Chuzhoy and S. Khanna, Polynomial flow-cut gaps and hardness of directed cut problems, J. ACM 56(2):6, 2009. https://doi.org/10.1145/1502793.1502795