Graph Theory

Motivation

The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points $n$, when the distances satisfy the triangle inequality.

The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with $n$: the tour is less than twice the optimal (Theorem 4), and more precisely at most $2(1-1/n)$ times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant $2(1-1/n)$ is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.

Setting

A traveling salesman graph $(N,d)$ has a finite node set $N$ with $|N| = n$ and a distance $d : N\times N\to\mathbb R$ that is symmetric, nonnegative and satisfies the triangle inequality $d(i,k)\le d(i,j)+d(j,k)$. A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.

A subtour $T$ is a tour on a subset of $N$ (a one-node subtour has no edges). For $k\notin T$, $\mathrm{TOUR}(T,k)$ inserts $k$ into $T$ where it is cheapest: if $T$ has at least two nodes, choose an edge $(x,y)$ of $T$ minimizing $d(x,k)+d(k,y)-d(x,y)$ and replace it by $(x,k),(k,y)$; if $T=\{i\}$, form the two-node tour on $i,k$. $\mathrm{COST}(T,k)$ is the length of $\mathrm{TOUR}(T,k)$ minus the length of $T$.

An insertion method builds subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some $a_i\notin T_i$, $1\le i<n$; INSERT is the length of $T_n$. With $d(T,p)=\min_{x\in T}d(x,p)$:

• nearest insertion chooses each $a_i$ with $d(T_i,a_i)=\min\{d(T_i,x): x\in N-T_i\}$;
• cheapest insertion chooses each $a_i$ with $\mathrm{COST}(T_i,a_i)=\min\{\mathrm{COST}(T_i,x): x\in N-T_i\}$.

The start node $a_0$ and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of $(N,d)$.

Formalization targets

Goal: Corollary to Theorem 4, eq. (4.12)

For every traveling salesman graph on $n\ge1$ nodes and every run of nearest insertion or of cheapest insertion,

Milestones

1. Lemma 2, (3.3): $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for $k\notin T$, $j\in T$.
2. Eq. (3.7): for every insertion method, $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
3. Eqs. (4.9)–(4.10): nearest insertion satisfies $\mathrm{COST}(T_i,a_i)\le 2\,d(p,q)$ for all $p\in T_i$, $q\notin T_i$ (4.5).
4. Proof of Theorem 4: cheapest insertion satisfies (4.5) as well.
5. Lemma 3: every insertion run satisfying (4.5) has $\mathrm{INSERT}\le 2\cdot\mathrm{TREE}$ (4.6).
6. Eq. (4.11): $\mathrm{TREE}\le(1-1/n)\cdot\mathrm{OPTIMAL}$.

Theorem 4 itself, $\mathrm{INSERT}<2\cdot\mathrm{OPTIMAL}$ when $d$ is not identically zero, is included as a companion statement.

Significance

The bound says that two simple $O(n^2)$ and $O(n^2\log n)$ construction rules are never worse than a factor $2(1-1/n)$ from optimal on any metric instance, a guarantee independent of $n$, in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound $2\cdot\mathrm{TREE}$, and the paper notes that similar arguments apply to nearest addition and nearest merger.

The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant $2$ (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of $\mathrm{TREE}\le\mathrm{OPTIMAL}$ (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant $2(1-1/n)$, and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.

Difficulty

Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step $i$ to the tree edge joining $a_i$ to its nearest node of $T_i$, but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds $2\cdot\mathrm{TREE}$. Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant $2(1-1/n)$ is sharper than the bound $2\cdot\mathrm{OPTIMAL}$ obtained from $\mathrm{TREE}\le\mathrm{OPTIMAL}$, so the weaker spanning-tree bound already in the library does not suffice.

Formalization scope

Nodes are Fin n with $n\ge1$ (the paper's nodes $1,\dots,n$ shifted to $0,\dots,n-1$). The distance satisfies the paper's three axioms plus the normalization $d(i,i)=0$, which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. $\mathrm{TOUR}(T,k)$ is encoded as insertion of $k$ at a list position whose resulting length is minimal over all $|T|+1$ positions, which is the minimization of (3.1) over the edges of $T$; COST is the corresponding minimum increase. The subtour index is 1-based as printed ($T_1=\{a_0\}$, $T_n$ final). The distance $d(T,p)$ is taken in $\mathbb R\cup\{+\infty\}$, so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).

A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.

A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, GSIA, Carnegie Mellon University, 1976. https://doi.org/10.1007/s43069-021-00101-z (reprint in Operations Research Forum 3, 2022)
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10 (Theorem 10.7). https://doi.org/10.1002/9781119584445

Motivation

Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?

Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.

Setting

All graphs are finite, undirected and loopless. A stable set of a graph $G=(V,E)$ is a set of vertices no two of which are adjacent. Write $S(G)\subseteq\mathbb R^V$ for the set of incidence vectors of stable sets (the zero–one vectors $x$ with $\{u:x_u=1\}$ stable), and

for the stable set polytope. A finite system of linear inequalities in the variables $(x_u:u\in V)$ is a defining linear system of $P(G)$ when its set of solutions is exactly $P(G)$.

Let $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ be graphs with $V_1\cap V_2=\emptyset$, and let $v\in V_1$. The graph $G$ obtained from $G_1$ by substituting $G_2$ for $v$ has vertex set $(V_1-\{v\})\cup V_2$. Its edges are the edges of $G_1-v$, the edges of $G_2$, and every edge joining a vertex of $G_2$ to a neighbour of $v$ in $G_1$. In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.

Formalization targets

Goal: Theorem 5.1

For $k\in\{1,2\}$ let

be a defining linear system of $P(G_k)$, with $J_1,J_2$ finite index sets and real coefficients, and put $a^+_{iv}=\max\{a_{iv},0\}$ for $i\in J_1$. Then

is a defining linear system of $P(G)$. The statement fixes no particular system for $G_1$ or $G_2$: any defining systems of the two pieces produce one for $G$, with $|J_1|\cdot|J_2|$ rows besides nonnegativity.

Milestones

1. Validity of (5.1) (§5, p. 145): every $x\in S(G)$ satisfies (5.1), hence so does every point of $P(G)$.
2. Proposition 2.1 (pp. 139–140): for a finite nonempty set $S$ of solutions of a system with nonnegativity rows $-x_u\le 0$, the solution set equals $\operatorname{conv}S$ if and only if for every integer vector $c$ the value $\max\{cx:x\in S\}$ equals the minimum of the associated dual linear program, the minimum being attained.
3. Decomposition of the optimum (§5, pp. 145–146): for an integer vector $c$ on $V_2\cup W$, $W=V_1-\{v\}$, with $d_u=\max\{c_u,0\}$,

where $m_0$ and $m_1$ are the maxima of $\sum_{u\in W}d_ux_u$ over $x\in S(G_1)$ with $x_v=0$ and $x_v=1$ respectively, and $m_2$ is the maximum of $\sum_{u\in V_2}d_ux_u$ over $S(G_2)$.

Significance

Theorem 5.1 gives an explicit construction: from a polyhedral description of $P(G_1)$ and $P(G_2)$ it writes one of $P(G)$, row by row, with no loss. Specialized to $G_1=K_2$ it gives Corollary 5.2 of the paper, a defining linear system for the join $G_1+G_2$; applied repeatedly it gives defining systems for lexicographic products, and applied with $G_2=\overline{K_2}$ it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of $G$, so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.

The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of $S(G)$, $P(G)$ and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.

Difficulty

That every point of $P(G)$ satisfies (5.1) is a short case check on stable sets of $G$. The difficulty is the reverse inclusion: that no point outside $P(G)$ satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of $P(G_1)$ and a point of $P(G_2)$, fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part $a^+_{iv}$ in place of $a_{iv}$ is what keeps the system valid when $a_{iv}<0$.

The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.

Formalization scope

• Graphs are SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in $V_1\cap V_2=\emptyset$.
• $S(G)$ is the set of real incidence vectors of finite stable sets (IsIndepSet); $P(G)$ is convexHull ℝ (S G), never the solution set of an inequality system.
• A linear system is a finite index type $J$ with real a : J → V → ℝ, b : J → ℝ. The nonnegativity rows $-x_u\le0$ are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with $P(G)$.
• No sign conditions on the $a_{iu}$ or $b_i$ are assumed; the paper assumes none.
• Implicit hypothesis made explicit: $V_2\ne\emptyset$ ([Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of $G_2$; with $V_2=\emptyset$, $J_2=\emptyset$ and $V_1\ne\{v\}$, (5.1) is just $x\ge0$ and the theorem fails. The validity milestone does not need it.
• In Proposition 2.1 the set $S$ is assumed nonempty, which the paper's $\max\{cx:x\in S\}$ presupposes. "max = min" is stated as a lower bound for every feasible dual vector plus a feasible dual vector attaining the maximum.
• In the decomposition milestone each maximum is a real sSup over a finite set that always contains the zero vector or the incidence vector of $\{v\}$, so no junk value of sSup can occur.
• A trivializing formalization is excluded: $P(G)$ is the convex hull of stable-set vectors rather than a set defined through the same inequalities, and the goal is the full set equality, not the validity inclusion alone.

Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• F. Harary, Graph Theory, Addison-Wesley, 1969.

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

• 1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
• 1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
• 1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
• 1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
• 2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$. Given a weight $w_x \in \mathbb{N}$ for each element $x$, the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$, and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$, with $m = |E|$. A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$. The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$, the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$.

The algorithm of §4 is:

1. Step 1. Compute $|B|$ and obtain $w$, the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$.
2. Step 2. Compute $\operatorname{adj}(B)$.
3. Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$,

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

1. Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$-element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$.
2. Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$, the minimum weight perfect matching is unique with probability $\ge 1/2$.
3. Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
4. Lemma 2: if the minimum weight perfect matching is unique, of weight $w$, then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$.
5. Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
6. Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$.

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$, each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$, which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$.

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). "$x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$.

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$, $|B|$, $\operatorname{adj}(B)$, the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

• K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947) 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
• L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
• S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
• O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

Motivation

The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of $(n+1)\times(n+1)$ matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator $N_+$, is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.

For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of $N_+$ already implies four of the classical families of facets of the stable set polytope.

Timeline:

• 1975: Chvátal shows that the rank constraint of a connected α-critical graph defines a facet of its stable set polytope (Chvátal 1975); clique, odd hole and odd antihole constraints are special rank constraints.
• 1981–88: Grötschel, Lovász and Schrijver show that the weighted stable set problem is solvable in polynomial time for perfect and $h$-perfect graphs, through the theta body $\mathrm{TH}(G)$ (Grötschel, Lovász, Schrijver 1988).
• 1991: Lovász and Schrijver define the operators $N$ and $N_+$ and prove Corollary 2.15: clique, odd hole, odd wheel and odd antihole constraints have $N_+$-index 1.

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$. The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$. Let $Q$ be the cone spanned by the 0–1 vectors with $x_0 = 1$. For a convex cone $K \subseteq Q$, the matrix cone $M_+(K)$ consists of the symmetric positive semidefinite matrices $Y = (y_{ij})$ with $y_{ii} = y_{0i}$ for $1 \le i \le n$ and $u^{\mathsf T}Yv \ge 0$ for all $u \in K^*$, $v \in Q^*$. The operator is

and $N_+^0(K) = K$, $N_+^t(K) = N_+(N_+^{t-1}(K))$.

Let $G = (V, E)$ be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). $\mathrm{STAB}(G)$ is the convex hull of incidence vectors $\chi^A$ of stable sets $A$. $\mathrm{FRAC}(G)$ is the polytope given by $x_i \ge 0$ and $x_i + x_j \le 1$ for $ij \in E$. $\mathrm{FR}(G) \subseteq \mathbb R^{V\cup\{0\}}$ is the cone $x_i \ge 0$, $x_i + x_j \le x_0$. The relaxations are

so $N_+^0(G) = \mathrm{FRAC}(G) \supseteq N_+^1(G) \supseteq \dots \supseteq \mathrm{STAB}(G)$. The $N_+$-index of an inequality $a^{\mathsf T}x \le b$ valid for $\mathrm{STAB}(G)$ is the least $r$ with $a^{\mathsf T}x \le b$ valid for $N_+^r(G)$.

The four constraint families are:

• clique: $\sum_{i\in B} x_i \le 1$ for a clique $B$;
• odd hole: $\sum_{i\in C} x_i \le \frac12(|C|-1)$ for $C$ inducing a chordless odd cycle;
• odd wheel: $\sum_{i\in U\setminus\{u_0\}} x_i + \frac{|U|-2}{2}x_{u_0} \le \frac{|U|-2}{2}$ for $U$ inducing an odd wheel with center $u_0$ (an odd hole plus a node adjacent to all of it);
• odd antihole: $\sum_{i\in D} x_i \le 2$ for $D$ inducing a chordless odd cycle in the complement of $G$.

The contraction of a node $v$ turns $a^{\mathsf T}x \le b$ into the inequality with the coefficients of $v$ and its neighbours removed and right-hand side $b - a_v$.

Formalization targets

Goal: Corollary 2.15

For every graph $G$ without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has $N_+$-index exactly 1:

Milestones

1. Lemma 1.5: for a closed convex cone $K \subseteq Q$ and $a$ with $a_i \le 0$ ($i \ge 1$), $a_0 \ge 0$, if $a^{\mathsf T}x \ge 0$ holds on $K \cap G_i$ (where $G_i = \{x_i = x_0\}$) for every $i$ with $a_i < 0$, then it holds on $N_+(K)$.
2. Lemma 2.14: if $a^{\mathsf T}x \le b$ is valid for $\mathrm{STAB}(G)$, and the contraction of every node with positive coefficient is valid for $N_+^r(G)$, then $a^{\mathsf T}x \le b$ is valid for $N_+^{r+1}(G)$.
3. Bipartite support (Section 2.c): an inequality valid for $\mathrm{STAB}(G)$ whose nonzero-coefficient nodes induce a bipartite graph is valid for $\mathrm{FRAC}(G)$.
4. Contraction property (Section 2.d): contracting a node with positive coefficient in any of the four constraints leaves positive-coefficient nodes that induce a bipartite subgraph.

Further result

Corollary 2.19 (first sentence): the $N_+$-index of a $\mathrm{STAB}(G)$-valid inequality $a^{\mathsf T}x \le b$ is at most the independence number of the subgraph induced by the nodes with positive coefficient.

Significance

Corollary 2.15 shows that a single round of $N_+$, a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently $N_+(G) = \mathrm{STAB}(G)$ for every $h$-perfect graph, in particular for perfect and $t$-perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding $N_+$-ranks.

The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver $N_+$ operator, its iterates, and the stable set relaxations $\mathrm{STAB}$, $\mathrm{FRAC}$, $\mathrm{FR}$ in Lean.

Difficulty

The lower bound (each constraint fails on $\mathrm{FRAC}(G)$) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix $Y$ alone, cannot succeed: those conditions define the linear operator $N$, and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in $\mathbb R^{n+1}$, including closedness of the iterates $N_+^r(\mathrm{FR}(G))$, which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι, with none the special coordinate $x_0$. For graphs, ι := V.
• $M$ is defined by condition (iii) with polar cones, not by its reformulations. Only $M_+$, $N_+$ and their iterates are defined; the linear operator $N$ is not used.
• Lemma 1.5 carries the hypothesis that $K$ is closed. The paper takes it tacitly (all its cones are polyhedral); without it the lemma fails, since $N_+(K)$ depends only on the closure of $K$.
• $\mathrm{FR}(G)$ is defined by its constraints, which agree with the paper's "cone spanned by the vectors $(1,x)$, $x \in \mathrm{FRAC}(G)$" because $G$ has no isolated nodes. Every graph statement carries the no-isolated-nodes hypothesis.
• Contraction is written on the same graph $G$ as a zeroed coefficient vector, rather than on the subgraph $G - \Gamma(v) - v$.
• Odd holes include triangles; odd antiholes have at least 5 nodes (a 3-node "antihole" is a stable set, for which the constraint is false); odd wheels are an odd hole plus a center adjacent to all its nodes.
• Clique constraints in the goal are restricted to cliques with at least 3 nodes: cliques of size 1 or 2 give inequalities already valid on $\mathrm{FRAC}(G)$, of index 0.
• "$N_+$-index at most $r$" is stated as validity on $N_+^r(G)$; the index itself is stated with IsLeast, never with an infimum that would default to 0 on an empty set.

A formalization asserting only validity on $N_+^1(G)$, or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.

Not formalized: the linear operator $N$ and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.

Reusable infrastructure includes the polar cone, the matrix cone $M_+$ and the $N_+$ operator (usable for any 0–1 program), the polytopes $\mathrm{STAB}$ and $\mathrm{FRAC}$, and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of $\mathrm{FRAC}$ for bipartite graphs, or the $M$-cone reformulations (iii′)–(iii″) are welcome.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2), 1991, 166–190. https://doi.org/10.1137/0801013
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988 (2nd ed. 1993). https://doi.org/10.1007/978-3-642-78240-4
• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory B 18, 1975, 138–154. https://doi.org/10.1016/0095-8956(75)90041-6

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$.

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $v$ and $w$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(v,w)$. It is a subroutine in string and graph algorithms.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of $n$ vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree $C$ whose sizes double along every edge, and $C$ is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about $C$ and Lemma 9.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1979: Tarjan (Applications of path compression on balanced trees, J. ACM 26) uses the decomposition of a tree by the doubling rule on subtree sizes to compute functions on paths; Lemmas 5–7 of Harel–Tarjan are cited from there without proof.
• 1983: Sleator and Tarjan (A data structure for dynamic trees, J. Comput. System Sci. 26) use the same heavy/light split of edges for dynamic trees.
• 1984: Harel and Tarjan give the $O(n)$-preprocessing, $O(1)$-query algorithm, with the compressed tree and its plies (§4).

Setting

A rooted tree $T$ (Appendix, p. 354) consists of a finite vertex set $V$ with $n = |V|$, a root $r \in V$ and a parent map $p_T$, defined for $v \ne r$, such that every vertex reaches $r$ by iterating $p_T$. The edges of $T$ are the pairs $v \to p_T(v)$ for $v \ne r$. If $p_T^i(v) = w$ for some $i \ge 0$, then $v$ is a descendant of $w$ and $w$ an ancestor of $v$. Every vertex is its own ancestor and descendant. The depth of $v$ is the number of edges from $v$ to $r$. $\mathrm{size}_T(v)$ is the number of descendants of $v$, including $v$.

An edge $v \to p_T(v)$ is light if $2\cdot\mathrm{size}_T(v) \le \mathrm{size}_T(p_T(v))$ and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition $V$ into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and $\mathrm{apex}(v)$ denotes the apex of the heavy path containing $v$.

The compressed tree $C$ has the same vertices and root as $T$, and its edges are

Write $p_C(v) = \mathrm{apex}(p_T(v))$, and let $\mathrm{size}_C(v)$ be the number of descendants of $v$ in $C$. The rank of $v$ is $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$, where $\lg = \log_2$. Let $\lg^{(i)}$ denote the $i$-fold iterate of $\lg$. Ply three is the set of vertices of rank at least $\lfloor\lg^{(2)} n\rfloor$. Ply two is the set of vertices whose rank lies between $\lfloor\lg^{(3)} n\rfloor$ and $\lfloor\lg^{(2)} n\rfloor - 1$, inclusive. Ply one is the set of vertices of rank below $\lfloor\lg^{(3)} n\rfloor$.

Formalization targets

Goal: Lemma 9 in the explicit form of its proof

For every rooted tree on $n \ge 4$ vertices:

and for every vertex $v$ in ply one, every $C$-descendant of $v$ lies in ply one and $\mathrm{size}_C(v) \le \lg^{(2)} n$.

The paper states the first two bounds as $O(n/\log n)$ and $O(n/\log^{(2)} n)$. The constants $4$ and $4$ are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of $C$ containing at most $\log^{(2)} n$ vertices", read vertex by vertex. Ply one is closed under $C$-descendants, so the component of a ply-one vertex is the $C$-subtree of its shallowest ply-one ancestor.

Milestones

1. Lemma 5 (p. 344): $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ if $v$ is an apex, and $\mathrm{size}_C(v) = 1$ otherwise.
2. Lemma 6 (p. 344): $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$ for every $v \ne r$.
3. Lemma 8 (p. 344): for every $i$, at most $n/2^i$ vertices have rank $i$.
4. Proof of Lemma 9, first sentence (p. 345): at most $n/2^{k-1}$ vertices have rank $k$ or greater.

A further item states Lemma 7 (p. 344): $C$ has depth at most $\lfloor\lg n\rfloor$. The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.