Complexity Theory

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

• 1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
• 1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
• 2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$.

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

• Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$, has processing time $4$ on the two machines of $x$, and cannot run anywhere else.
• Every clause $c$ has one c-job, released at time $3$, with processing time $0$. It may run on the false machine of $x$ when $x$ occurs in $c$, on the true machine of $x$ when $\neg x$ occurs in $c$, and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$, with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$. The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$, and

$$\mathrm{VAL}(S_0)=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I),\qquad \mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{VAL}(S_0)$$

for every feasible schedule $S$. These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$.

Milestones

1. Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$.
2. Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$.
3. The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$.
4. The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$.
5. The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$.

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$.

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$, and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$. The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$, and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

• Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$" would fail.
• Every variable occurs at least once. The bound $n\le 3m$, and with it the constant $32$, needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$.

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$. Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$, but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$, c-jobs at time $3$ or $4$), and on the existence of optimal schedules.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
• J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
• C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$. Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$, $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$, $m\ge0$, $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider

$$\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .$$

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$, $s>0$, $Ax=b$, and $A^Ty+s=c$ for some $y$. For such a pair the duality gap is $x^Ts$, and the duality measure is $\mu=x^Ts/n$. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$.

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$, $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$. For $\beta\in(0,1)$ the wide neighbourhoods are

$$\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.$$

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$.

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$,

$$Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}$$

and the step is $x(\theta)=x+\theta d_x$, $s(\theta)=s+\theta d_s$. The scaled quantities $p=X^{-1/2}S^{1/2}d_x$, $q=X^{1/2}S^{-1/2}d_s$, $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$. The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$.

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$. While $(x^k)^Ts^k>2^{-t}$, it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$, and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$.

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$, and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$. Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

$$k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .$$

The paper states "$O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

• Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$.
• Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$, $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$, $\|Pq\|_\infty\le\|r\|^2/4$.
• Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$; in $\mathcal N_\infty(\beta)$, $\|r\|_\infty^2\le(1+\beta)\mu$.
• Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$, and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$.
• Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$).
• (15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$.

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$, $\mathcal N_\infty^-$, of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

• The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$, which comes from $Ad_x=0$ and $d_s=-A^Td_y$. Those relations hold only for a solution of the full system (2), not for the first equation alone.
• Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
• "The largest $\bar\theta$" is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$, but the formal run must say what $\bar\theta$ is.
• Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$, real powers of $2$, and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$, and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$.

Committed conventions and repairs:

• The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
• "The largest $\bar\theta$" is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$. When no maximum exists (always the case for $n=1$, where $Pq=0$), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$.
• A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$. Its behaviour after the stopping test is unconstrained.
• In $\theta_2$ and $\theta_2^-$, a zero norm makes the quotient $+\infty$ and the minimum $1$. Since Lean's real division by zero is $0$, this case is defined explicitly.
• The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$. At $n=1$ it can fail (e.g. $\beta=1/2$, $\gamma=0.9$), and Algorithm 2 makes no iterations there.
• The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
• Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
• R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$, and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$. The primal problem minimizes $c^Tx$ over $Ax=b$, $x\ge0$. Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$, $s\ge0$. The dual slack is $s$. The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$, with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$, $S=\operatorname{diag}(s)$, and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$. For $0<\beta<1$, the Euclidean central-path neighborhood is

$$N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.$$

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$, $Ad_x=0$, and $A^Td_y+d_s=0$. A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$. Algorithm 1 begins in $N_2(1/4)$. It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$, then takes one full corrector direction with $\gamma=1$. The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$, every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

$$k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.$$

The paper states the iteration order as $O(\sqrt n\,t)$. The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$, rather than with $n$, in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$. The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$: Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$, because its printed lower bound on the predictor length fails at $n=1$.

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

Selected references

• Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$, $b\in\mathbb R^m$, $c\in\mathbb R^n$ and $N:=n+m$, the paper considers the linear program in slack form and its dual,

$$\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .$$

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$. The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

$$\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),$$

and for $0<\theta<1$ the wide neighborhood of the central path is

$$\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.$$

The central path itself is the set of points where all products $x_js_j$, $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$, for $r\ge1$ and $t>0$:

$$\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .$$

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$, $m=3r-1$, $N=5r-1$. Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$. A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$. The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$. The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$, with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$. Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$.

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$, and suppose that

$$t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}$$

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$, then

$$p\ge2^{r-1}.$$

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$.

Milestones

1. Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$.
2. Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$, $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$, have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$.
3. Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$,

$$d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .$$

4. Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$, $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$.
5. Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$, where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$.

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$, uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$. The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$, and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$, is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$, a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$. That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$. The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$, but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$), so it is stated for $t>1$. Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$. Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$, $t=2$, $\theta=1/2$. A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$.

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
• A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
• M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
• X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746

Motivation

Nash's theorem guarantees that every finite game has a mixed equilibrium, but says nothing about how hard one is to find. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) showed that computing a Nash equilibrium is complete for the class PPAD of total search problems whose solutions are guaranteed by a parity argument on a directed graph (Papadimitriou 1994). Their proof simulates an arithmetic circuit by a graphical game: a multiplayer game in which each player's payoff depends on a few neighbours only, built from small game gadgets whose equilibria compute $x \mapsto \alpha x$, $x + y$, $xy$, constants and comparisons on mixed-strategy probabilities.

These gadgets are the reusable core of the reduction. The PPAD-completeness results for three-player games, and the later results for two-player games and for approximate equilibria, all rest on gadget analyses of this kind.

Timeline.

• 1994: Papadimitriou defines PPAD and shows that Nash equilibrium computation lies in it (JCSS 48).
• 2001: Kearns, Littman and Singh introduce graphical games (UAI 2001).
• 2005–2006: Goldberg and Papadimitriou reduce $r$-player games to four-player games, and Daskalakis, Goldberg and Papadimitriou prove PPAD-completeness for four players (STOC 2006). The three-player case is obtained independently by Daskalakis and Papadimitriou and by Chen and Deng (ECCC reports, 2005); the two-player case by Chen and Deng (FOCS 2006; J. ACM 56(3), 2009, with Teng).
• 2009: the journal version unifies the three-player argument; its Proposition 4.18 is the gadget $\mathcal G_{+,*}$ that makes the reduction to three players work.

Setting

A game has finitely many players; player $p$ has a finite set $S_p$ of pure strategies and a nonnegative payoff $u^p_s$ for each pure profile $s$. A mixed profile $x$ gives each player a probability distribution $(x^p_j)_{j\in S_p}$, and $x_s$ denotes the product of the probabilities of the components of a partial profile $s$. The expected payoff of a pure strategy $j$ of $p$ is $\sum_{s\in S_{-p}} u^p_{js}x_s$.

An $\epsilon$-Nash equilibrium (the paper's notion, an $\epsilon$-approximately well-supported equilibrium, Eq. (2)) is a mixed profile in which no player puts weight on a pure strategy that another of its pure strategies beats by more than $\epsilon$:

$$\forall p,\ j, j' \in S_p:\quad \sum_{s\in S_{-p}} u^p_{js}x_s > \sum_{s\in S_{-p}} u^p_{j's}x_s + \epsilon \implies x^p_{j'} = 0 .$$

For $\epsilon = 0$ this characterizes Nash equilibria.

A player with strategies $\{0,1\}$ is binary; $\mathbf p[v]$ is the probability that it plays $1$, and $\mathbf p[v : s]$ is the probability that $v$ plays $s$. The affects graph (Definition 2.2) has an edge $(v_1, v_2)$ between distinct players when the payoff of $v_2$ is a nonconstant function of the action of $v_1$. A legal $k$-coloring (Definition 4.8) gives each player one of $k$ colors so that the two ends of an edge differ and two distinct players with a common successor differ.

The game $\mathcal G_{+,*}$ (Fig. 11) has inputs $v_1, v_2$, output $v_3$ and intermediate players $w_1, v_1', w_2, v_2', w_3, w, u$, all binary except $v_2'$, which has strategies $\{0, 1, *\}$. Its payoff tables are fixed by nonnegative integers $\alpha, \beta, \gamma$; the inputs' payoffs are unconstrained.

Formalization targets

Goal: Proposition 4.18

For nonnegative integers $\alpha, \beta, \gamma$ with $\alpha + \beta + \gamma \le 3$, the affects graph of $\mathcal G_{+,*}$ has a legal 3-coloring, and for every $\epsilon \in [0, 0.01]$, at every $\epsilon$-Nash equilibrium,

$$\Big|\,\mathbf p[v_3] - \min\{1,\ \alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2]\}\Big| \le 81\,\epsilon .$$

The case $\epsilon = 0$ is exact computation at every Nash equilibrium.

Milestones: the four claims of the proof

• Claim 1: $\mathbf p[v_1'] = \tfrac18\mathbf p[v_1] \pm \epsilon$.
• Claim 2: $\mathbf p[v_2' : 1] = \tfrac18\mathbf p[v_2] \pm \epsilon$.
• Claim 3: $\mathbf p[v_2' : *] = \tfrac{\alpha}{8}\mathbf p[v_1] + \tfrac{\beta}{8}\mathbf p[v_2] + \tfrac{\gamma}{8}\mathbf p[v_1]\mathbf p[v_2] \pm 10\epsilon$.
• Claim 4: the output bound of the goal.

Milestones: the elementary gadgets

• Proposition 4.2 ($\mathcal G_{\times\alpha}$): $\mathbf p[v_2] = \min(\alpha\mathbf p[v_1], 1) \pm \epsilon$ for real $\alpha \ge 0$, $\epsilon < 1$.
• Proposition 4.3: $\mathbf p[v_3] = \min(\alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2], 1) \pm \epsilon$ for real $\alpha, \beta, \gamma \ge 0$.
• Proposition 4.5 ($\mathcal G_\alpha$): $\mathbf p[v_1] = \min(\alpha, 1) \pm \epsilon$.
• Lemma 5.3 (comparator $\mathcal G_<$): $\mathbf p[d] = 1$ if $\mathbf p[a] < \mathbf p[b] - \epsilon$ and $\mathbf p[d] = 0$ if $\mathbf p[a] > \mathbf p[b] + \epsilon$.

Significance

The result. The paper reduces $r$-player games to three-player games by building a graphical game from gadgets, legally coloring it with three colors, and turning each color class into one player of a normal-form game (§4.2, §4.5). Proposition 4.18 supplies a gadget that computes $\min\{1, \alpha x + \beta y + \gamma xy\}$ and can be glued into such a construction while keeping it legally 3-colorable (p. 233), at the price of an error constant $81$ instead of the constant $1$ of the elementary gadgets. The error bound is what carries the reduction over to approximate equilibria: an $\epsilon$-Nash equilibrium of the gadget computes its function to within $81\epsilon$.

Formalizing it. All results here are proved in the paper (Proposition 4.5 is stated with the remark that its proof is similar to those of Propositions 4.2 and 4.3). None of them has a machine-checked proof, and no graphical-game or gadget infrastructure exists in Lean. The mission formalizes the known proofs and produces a library of verified gadgets with explicit error bounds, the first layer of any formal treatment of the PPAD-hardness of Nash equilibria.

Difficulty

Each claim is a case analysis on which strategy of an intermediate player is dominated by more than $\epsilon$, but the cases interact. Claim 3 needs Claims 1 and 2 as inputs, and it is the step where both $\alpha + \beta + \gamma \le 3$ and $\epsilon \le 0.01$ are used: without them one of the regimes of $w$ cannot be excluded. The three-strategy player $v_2'$ cannot be handled by the "binary player copies or disagrees" argument of the elementary gadgets; its weight on $1$ and on $*$ must be tracked separately. The error constants $10$ and $81$ propagate through products of approximate quantities, so a proof that is loose at any step does not reach them.

On the Lean side, the expected payoff of a pure strategy is a sum over all pure profiles of a ten-player game; every claim first has to reduce it to the few coordinates the player's payoff actually depends on.

Formalization scope

Games, mixed profiles and expected payoffs are those of the published agt_games bundle: a finite player type, strategy types S i, payoffs u : ι → (∀ i, S i) → ℝ, AGT.IsMixedProfile, AGT.expectedPayoff. The expected payoff of a pure strategy $j$ is the expected payoff of the profile with $p$'s strategy replaced by the point mass at $j$. An $\epsilon$-Nash equilibrium requires a genuine mixed profile.

Each gadget is one explicit game on its own player type, with the payoff tables of the paper. Binary strategies are Fin 2 with the paper's labels $0, 1$, and $\mathbf p[v]$ is the weight on 1; $v_2'$'s strategies are an inductive type {zero, one, star}. The input players' payoffs are unconstrained in the paper; here they are $0$, which makes the $\epsilon$-condition at the inputs vacuous. Since every non-input payoff depends only on gadget players, "$\epsilon$-Nash equilibrium of the standalone gadget" quantifies over all mixed strategies of the inputs and imposes the condition exactly on the other players, which is the paper's meaning when the gadget sits inside a larger game. The affects graph is computed from the payoff functions, without self-loops, and colors $\{1,\dots,k\}$ are Fin k. The ranges $\alpha, \beta, \gamma \in \mathbb N$ (Proposition 4.18) and $\alpha, \beta, \gamma \in \mathbb R_{\ge 0}$ (Propositions 4.2, 4.3, 4.5) follow the paper; $\epsilon \ge 0$ is added where the paper writes only $\epsilon < 1$.

The paper states Proposition 4.18 and Lemma 5.3 as "there is a graphical game"; an existential statement would be met by a game whose output has a dominant strategy and whose inputs are forced, so both are stated for the explicit game of the proof, with free inputs.

A complete development needs a computation lemma for the pure-strategy payoff in each gadget (reusable for any gadget on these definitions) and the case analyses of the claims. Proofs of the elementary gadgets, which are short, and of Claims 1 and 2 are good first contributions; Claim 3 is the main step.

Selected references

• C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM J. Comput. 39(1):195–259, 2009. https://doi.org/10.1137/070699652
• C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Comput. System Sci. 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7
• M. Kearns, M. L. Littman, S. Singh, Graphical Models for Game Theory, UAI 2001. https://arxiv.org/abs/1301.2281
• X. Chen, X. Deng, S.-H. Teng, Settling the complexity of computing two-player Nash equilibria, J. ACM 56(3):14, 2009. https://doi.org/10.1145/1516512.1516516

Motivation

Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.

In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has $2^{\Omega(\sqrt n)}$ inequalities.

Timeline.

• 1990: De Simone shows that the correlation polytope is linearly isomorphic to the cut polytope.
• 1991: Yannakakis proves the factorization theorem (extension complexity equals the nonnegative rank of a slack matrix) and the exponential lower bound for symmetric formulations of the TSP and perfect matching polytopes.
• 1992: Razborov proves the distributional lower bound for set disjointness.
• 2003: de Wolf shows that the support of $M(n)_{ab}=(1-a^\top b)^2$ needs $2^{\Omega(n)}$ rectangles to cover.
• 2012/2015: Fiorini et al. prove $\mathrm{xc}(\mathrm{CUT}(n))=2^{\Omega(n)}$, $\mathrm{xc}(\mathrm{TSP}(n))=2^{\Omega(\sqrt n)}$, and a $2^{\Omega(\sqrt n)}$ bound for stable set polytopes of some graphs on $n$ vertices.
• 2013: Kaibel and Weltge give a short combinatorial proof of the correlation-polytope bound, with constant $C=\log_2(3/2)$.
• 2014: Rothvoss proves $2^{\Omega(n)}$ for the perfect matching polytope.

Setting

Let $\iota$ be a finite index set. An extended formulation (EF) of a set $P\subseteq\mathbb R^{\iota}$ is a linear system $E^{=}x+F^{=}y=g^{=}$, $E^{\le}x+F^{\le}y\le g^{\le}$ in variables $(x,y)\in\mathbb R^{\iota}\times\mathbb R^{k}$ such that $x\in P$ exactly when some $y$ satisfies it. Its size is the number of inequalities. The extension complexity $\mathrm{xc}(P)$ is the least size of an EF of $P$.

A polytope is the convex hull of finitely many points. A face of $P$ is $P$ itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope $Q$ is an extension of $P$ if $\pi(Q)=P$ for some linear map $\pi$. Given $P=\{x : Ax\le b\}=\mathrm{conv}(V)$, the slack matrix has entries $S_{ij}=b_i-A_iv_j$. The nonnegative rank $\mathrm{rank}_+(M)$ is the least $r$ with $M=TU$, where $T\ge 0$ has $r$ columns and $U\ge 0$ has $r$ rows.

For $n$-bit strings $a,b$, $a^\top b$ is the number of common ones, and $M(n)$ is the $2^n\times 2^n$ matrix $M_{ab}=(1-a^\top b)^2$. A 1-monochromatic rectangle cover of its support is a family of products $R_1\times R_2$, each containing only entries with $M_{ab}\ne 0$, that together contain all of them.

On the complete graph $K_n=(V_n,E_n)$, $\chi^F\in\mathbb R^{E_n}$ is the characteristic vector of an edge set $F$ and $\delta(X)$ is the cut of $X\subseteq V_n$. The polytopes are

$$\mathrm{CUT}(n)=\mathrm{conv}\{\chi^{\delta(X)}\},\qquad \mathrm{COR}(n)=\mathrm{conv}\{bb^\top : b\in\{0,1\}^n\}\subseteq\mathbb R^{n\times n},$$ $$\mathrm{TSP}(n)=\mathrm{conv}\{\chi^F : F\subseteq E_n \text{ is a tour (Hamiltonian cycle) of } K_n\}.$$

Formalization targets

Goal: Theorem 12

$$\exists\,C>0\ \exists\,N\ \forall n\ge N:\qquad \mathrm{xc}(\mathrm{TSP}(n))\ \ge\ 2^{C\sqrt n}.$$

The constant is left unfixed, so the goal survives any improvement of it.

Milestones, in attack order

• Razborov's distributional bound (displayed in the proof of Theorem 1) and Theorem 1: every 1-rectangle cover of the support of $M(n)$ has $2^{\Omega(n)}$ rectangles.
• Lemma 2 and Theorem 3 (Yannakakis): $\mathrm{rank}_+(S)\le r$ $\iff$ an extension with at most $r$ facets $\iff$ an EF with at most $r$ inequalities.
• Theorem 4: $\mathrm{rank}_+(M)$ is at least the rectangle covering bound of its support (already proved on the platform, referenced).
• Theorem 5: $\mathrm{COR}(n)$ is linearly isomorphic to $\mathrm{CUT}(n+1)$. Lemma 6: $\langle 2\,\mathrm{diag}(a)-aa^\top,x\rangle\le 1$ is valid for $\mathrm{COR}(n)$, with slack $M_{ab}$ at $bb^\top$.
• Theorem 7: $\mathrm{xc}(\mathrm{CUT}(n+1))=\mathrm{xc}(\mathrm{COR}(n))\ge 2^{Cn}$.
• Lemma 9: $\mathrm{xc}$ does not increase under taking faces or linear images. Lemma 11: $\mathrm{TSP}(q)$ with $q=O(n^2)$ has a face that is an extension of $\mathrm{COR}(n)$.
• Stable sets: Lemma 8 and Theorem 10, $\mathrm{xc}(\mathrm{STAB}(G_n))=2^{\Omega(\sqrt n)}$ for some graph $G_n$ on $n$ vertices.

Significance

The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.

Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.

Difficulty

The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because $M(n)$ has rank $O(n^2)$. The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of $\mathrm{TSP}(q)$ with $q=O(n^2)$. Theorem 12 also needs a monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ that the paper only indicates.

Formalization scope

• Everything is over $\mathbb R$. Points of $\mathbb R^d$ are functions $\iota\to\mathbb R$ on a finite type. $\mathbb R^{E_n}$ has one coordinate per unordered edge of $K_n$ (non-diagonal elements of Sym2 (Fin n)). $\mathbb R^{n\times n}$ is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.
• $\mathrm{xc}$ and $\mathrm{rank}_+$ are natural numbers (sInf of the attainable sizes), never $\infty$, so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.
• Every $2^{\Omega(f(n))}$ is $\exists C>0\,\exists N\,\forall n\ge N$, $2^{Cf(n)}\le\cdot$ (real power). Every $O(n^2)$ is a constant $c$ with $\le c\,n^2$, uniform in $n$.
• Theorem 7 and Lemma 11 carry an added $n\ge 1$: at $n=0$ the printed statements fail, since $\mathrm{COR}(0)$ is a point with $\mathrm{xc}=0$ and no positive $q\le c\cdot 0$ exists.
• "Linearly isomorphic" in Theorem 5 is an injective linear map carrying $\mathrm{CUT}(n+1)$ onto $\mathrm{COR}(n)$, because the two ambient spaces have different dimensions.
• In Theorem 3, $\dim P\ge 1$ is "$P$ has two distinct points". Faces include $\emptyset$ and $P$, facets are maximal proper faces, and facets are counted with an explicit finite family.
• Ruled out: a TSP polytope over ordered pairs, all cycles or directed tours, a weakened isomorphism in Theorem 5, and an extension complexity valued in $\mathbb N\cup\{\infty\}$ that is infinite on a broken EF definition.
• Welcome contributions: proofs of any milestone, in particular Lemma 2 and the factorization theorem (reusable for every later extension-complexity result), Theorem 5, and the face construction of Lemma 11; a proof of the monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ as a supporting lemma.

Selected references

• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, J. ACM 62(2), Art. 17, 2015. https://doi.org/10.1145/2716307
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. Syst. Sci. 43(3), 441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• A. A. Razborov, On the distributional complexity of disjointness, Theoret. Comput. Sci. 106(2), 385–390, 1992. https://doi.org/10.1016/0304-3975(92)90260-M
• R. de Wolf, Nondeterministic quantum query and communication complexities, SIAM J. Comput. 32(3), 681–699, 2003. https://doi.org/10.1137/S0097539702407345
• C. De Simone, The cut polytope and the Boolean quadric polytope, Discrete Math. 79(1), 71–75, 1990. https://doi.org/10.1016/0012-365X(90)90056-N
• V. Kaibel, S. Weltge, A short proof that the extension complexity of the correlation polytope grows exponentially, Discrete Comput. Geom. 53, 397–401, 2015. https://doi.org/10.1007/s00454-014-9655-9
• T. Rothvoss, The matching polytope has exponential extension complexity, J. ACM 64(6), Art. 41, 2017. https://doi.org/10.1145/3127497