Operations Research

Motivation

The proximal point algorithm is a basic iterative scheme of convex optimization and monotone operator theory. To solve a problem governed by a monotone operator, it replaces the problem by a sequence of better-conditioned problems, each regularized by a quadratic term centred at the previous iterate. Augmented Lagrangian methods, the Douglas–Rachford and ADMM splitting schemes, and many bundle methods can all be read as instances of it.

The scheme first appeared in a five-page note by Bernard Martinet in the Revue française d'informatique et de recherche opérationnelle (1970), under the name régularisation par approximations successives. Martinet stated it for a monotone variational inequality on a bounded closed convex subset of a Hilbert space and proved that the weak cluster points of the iterates are solutions. This mission formalizes that first convergence theorem as it was originally stated.

Timeline.

• 1966–1967: Hartman–Stampacchia and Lions–Stampacchia prove existence of solutions for monotone, hemicontinuous variational inequalities on bounded closed convex sets (Lions–Stampacchia 1967). Minty's lemma characterizes the solution set by the inequality with the operator evaluated at the variable point.
• 1970: Martinet introduces the regularization iteration (2) and proves Théorème 1 below (Martinet 1970). In §IV of the same note he states the convex-minimization version.
• 1976: Rockafellar extends the method to maximal monotone operators, allowing inexact steps and variable step sizes, and proves weak convergence of the whole sequence when a zero exists (Rockafellar 1976).
• 1991: Güler constructs an example in which the iterates converge weakly but not strongly (Güler 1991).

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. Let $H'$ be its dual, and write $(\varphi, y)$ for the value of a functional $\varphi\in H'$ at $y\in H$. Let $C\subseteq H$ be convex, closed and bounded, and let $T:H\to H'$ be

• monotone on $C$: $(Tx-Ty,\,x-y)\ge0$ for all $x,y\in C$;
• hemicontinuous on $C$: for all $x,y\in C$, the map $t\mapsto T((1-t)x+ty)$, $t\in[0,1]$, is continuous into $H'$ with its weak topology.

The variational inequality (1) asks for $\bar x\in C$ such that

$$(T\bar x,\, x-\bar x)\ge 0\qquad\forall x\in C .$$

Its solution set is denoted $M$ (solSet T C in Lean).

Martinet's regularization algorithm starts from $x^0\in C$. Given $x^n\in C$, it determines $x^{n+1}\in C$ such that

$$(Tx^{n+1},\, x-x^{n+1})+\langle x^{n+1}-x^n,\, x-x^{n+1}\rangle\ge 0\qquad\forall x\in C. \tag{2}$$

In words, $x^{n+1}$ solves the variational inequality for the operator $T+(\,\cdot\,-x^n)$, which is strongly monotone. A point $\tilde x$ is a weak cluster point of $(x^n)$ if every neighbourhood of $\tilde x$ in the weak topology contains $x^n$ for infinitely many $n$.

Formalization targets

Goal: Théorème 1

$$\tilde x \text{ a weak cluster point of } (x^n)\ \Longrightarrow\ \tilde x\in M .$$

Every weak cluster point of the regularized iterates solves (1). The paper's Lemme 2 states the same thing. The goal assumes neither that (1) has a solution nor that $T$ is bounded on $C$.

Milestones, in the order the paper uses them

1. §2.1: (1) has at least one solution when $C\neq\emptyset$, so $M\neq\emptyset$.
2. §2.2: the step (2) has exactly one solution $x^{n+1}\in C$ for every $x^n\in C$.
3. §2.3, (5): Minty's characterization $M=\{\bar x\in C\mid (Tx,\,x-\bar x)\ge0\ \forall x\in C\}$.
4. §2.3, (7): for every $\bar x\in M$, $\|x^{n+1}-\bar x\|^2\le\|x^n-\bar x\|^2-\|x^{n+1}-x^n\|^2$.
5. Lemme 1: $\|x^{n+1}-x^n\|\to0$.
6. §2.3, (8): $\liminf_n (Tx^{n+1},\,x-x^{n+1})\ge0$ for every $x\in C$.
7. §2.3, (9): $\liminf_n (Tx,\,x-x^{n})\ge0$ for every $x\in C$.
8. Corollaire (stronger than the goal): if $M=\{\bar x\}$, then $x^n\rightharpoonup\bar x$.

Significance

The result. Théorème 1 is the first convergence theorem for the proximal point method. The method only needs to solve strongly monotone subproblems, and those are well posed even when the original problem is not. Together with the existence result, the theorem says the iterates accumulate weakly only at solutions. When the solution is unique, the whole sequence converges weakly (the Corollaire). The later theory of Rockafellar, Brézis–Lions and the splitting literature refines this statement.

Formalizing it. The result has been proved since 1970. What this mission adds is a machine-checked version that follows the original hypotheses: an operator into the dual, hemicontinuity rather than continuity, and no maximality assumption. The cited ingredients, the Lions–Stampacchia existence theorem in an infinite-dimensional Hilbert space and Minty's lemma, are not in Mathlib as far as this mission is aware. Formalizing them is part of the work and is reusable well beyond this paper. The milestone items on the platform are statements awaiting proof. None of them has a machine-checked proof yet.

Difficulty

Lemme 1 and inequality (7) follow from the defining inequality (2) and the algebra of the inner product. The difficulty is at two other points.

First, the iterates satisfy the variational inequality only approximately, and only with $T$ evaluated at the iterate. A weak cluster point gives no control over $Tx^{n}$, because $T$ is merely hemicontinuous and is not assumed weakly continuous or bounded. The obvious idea, to pass to the limit in $(Tx^{n+1},\,x-x^{n+1})\ge -\varepsilon_n$, fails for this reason. Passing to the limit requires the reformulation in which $T$ is evaluated at a fixed point of $C$. That reformulation is Minty's characterization (5), and proving it uses hemicontinuity along segments.

Second, the proof of Lemme 1 needs a solution of (1) to exist. In infinite dimensions that is the Lions–Stampacchia theorem. Its standard proof goes through Brouwer's fixed point theorem on finite-dimensional sections together with weak compactness of $C$, and this is the heaviest item of the mission.

Formalization scope

• $H$ is a real Hilbert space: NormedAddCommGroup H, InnerProductSpace ℝ H, CompleteSpace H. The paper says only "espace de Hilbert". Its ordered inequalities force real scalars.
• $H'$ is StrongDual ℝ H, and $(\varphi,y)$ is φ y. $T$ is not replaced by a map $H\to H$ through the Riesz isomorphism.
• Hemicontinuity is weak-* continuity: for $x,y\in C$ and every $z\in H$, the map $t\mapsto (T((1-t)x+ty),z)$ is continuous on $[0,1]$. Since $H$ is reflexive, this is the paper's weak topology on $H'$. It is not strengthened to continuity of $T$.
• The algorithm is a relation (IsRegSeq): any sequence with $x^0\in C$ that satisfies (2) at every step. Existence and uniqueness of the step are milestone 2, not built into a definition.
• A weak cluster point is MapClusterPt in WeakSpace ℝ H, a cluster point in the weak topology. It is not a cluster point in the norm topology, which would make the goal weaker.
• $\liminf_n a_n\ge0$ in (8) and (9) is stated as $\forall\varepsilon>0$, eventually $a_n\ge-\varepsilon$. Filter.liminf on $\mathbb R$ returns a junk value on sequences that are unbounded below.
• "C nonempty" is added to the existence milestone. The paper leaves it implicit, and the claim is false for $C=\emptyset$.
• In Lean the sequence is called $x$ and an arbitrary point of $C$ is called $y$. The paper uses the letter $x$ for both.

A trivializing formalization is ruled out. The goal does not assume $M\neq\emptyset$, boundedness of $T$, or strong cluster points. Its hypotheses are satisfiable: $H=\mathbb R$, $C=[-1,1]$, $(Tx,y)=xy$, $x^n=2^{-n}$ is an instance, checked locally.

Not formalized: Remarques 1 and 2 of §II (a variable-weight variant of (2), whose printed form is apparently misprinted, and the removal of boundedness of $C$ under a coercivity condition), because the paper gives neither a proof. Théorème 2 (§III) and the convex-minimization §IV are not formalized either. §IV is the subject of the companion mission.

Contributions are welcome on each milestone, and especially on the general infrastructure: Minty's lemma, Hartman–Stampacchia/Lions–Stampacchia existence for monotone hemicontinuous operators, and the fact that bounded sequences in a Hilbert space have weak cluster points. A proved Brouwer fixed point theorem (AGT.brouwer_fixed_point) and a Banach–Alaoglu theorem (FamousTheorems.banach_alaoglu) are available on the platform as tools.

Selected references

• B. Martinet, Brève communication. Régularisation d'inéquations variationnelles par approximations successives, Revue française d'informatique et de recherche opérationnelle, série rouge, 4(R-3) (1970), 154–158. https://doi.org/10.1051/m2an/197004R301541
• J.-L. Lions, G. Stampacchia, Variational inequalities, Communications on Pure and Applied Mathematics 20 (1967), 493–519. https://doi.org/10.1002/cpa.3160200302
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM Journal on Control and Optimization 14 (1976), 877–898. https://doi.org/10.1137/0314056
• O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM Journal on Control and Optimization 29 (1991), 403–419. https://doi.org/10.1137/0329022

Motivation

Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation

$$0\in f(x)+\partial\psi_C(x),$$

where $\partial\psi_C$ is the normal-cone operator of a closed convex set $C$. S. M. Robinson introduced strong regularity of such an inclusion at a solution $x_0$ in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).

Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set $C$ the paper's appendix does this by a reduction: locally around $x_0$ the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.

Setting

Work in $\mathbb R^n$ with the standard inner product, which identifies $\mathbb R^n$ with its dual. For $C\subseteq\mathbb R^n$ the normal cone at $x$ is

$$\partial\psi_C(x)=\{y:\langle y,c-x\rangle\le 0\ \text{for all } c\in C\}\ \text{if } x\in C,\qquad \partial\psi_C(x)=\emptyset\ \text{if } x\notin C.$$

A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex $C$, an $n\times n$ real matrix $A$ and $a\in\mathbb R^n$, and consider

$$0\in Ax+a+\partial\psi_C(x).\qquad\text{(A.1)}$$

It is strongly regular at a solution $x_0$ with constant $\lambda$ if there are neighbourhoods $U$ of $0$ and $V$ of $x_0$ such that for each $y\in U$ the perturbed inclusion

$$y\in Ax+a+\partial\psi_C(x)\qquad\text{(A.2)}$$

has exactly one solution $x=s(y)$ in $V$, and $\|s(y_1)-s(y_2)\|\le\lambda\|y_1-y_2\|$ on $U$.

The reduction uses the following objects, all built from the data:

• $y_0:=Ax_0+a$;
• the face $F:=\partial\psi_C^*(-y_0)$, the set of maximisers of $\langle -y_0,\cdot\rangle$ over $C$ (it contains $x_0$);
• the tangent cone $T:=T_F(x_0)=\partial\psi_F(x_0)^\circ$, the polar of the normal cone of $F$ at $x_0$;
• the subspace $L$ parallel to $F$ (the direction of its affine hull) and the orthogonal projector $P_L$;
• the lineality space $M$ of $T$, the subspace $L\cap M^\perp$, and the cone $K:=T\cap M^\perp$.

The reduced form of (A.1) at $x_0$ is the inclusion $z\in P_LAw+\partial\psi_T(w)$ for $z\in L$; in an orthonormal basis adapted to $M$, $L\cap M^\perp$ and $L^\perp$ it is $z\in Bw+\partial\psi_{\mathbb R^r\times K}(w)$ with an $(r+s)\times(r+s)$ matrix $B$. It is vacuous when $L=\{0\}$.

Formalization targets

Goal: Theorem A.4 (p. 60)

If $x_0$ solves (A.1), then (A.1) is strongly regular at $x_0$ if and only if

$$L=\{0\}\quad\text{or}\quad\forall z\in L\ \exists!\,w\in\mathbb R^n:\ z\in P_LAw+\partial\psi_T(w).$$

No Lipschitz constant is fixed: the left side is "strongly regular for some $\lambda$".

Milestones

1. Proposition A.1 (p. 58): for $x_0\in C$, $(C-x_0)\cap U=T_C(x_0)\cap U$ for some neighbourhood $U$ of $0$.
2. Proposition A.2 (p. 58): on $F=\partial\psi_C^*(-y_0)$, $\partial\psi_F(x)=\partial\psi_C(x)+y_0\mathbb R_+$, and $\partial\psi_C^*(-y)\subset F$ for $y$ near $y_0$.
3. Proposition A.3 (p. 58): for $x_0\in F$, near the origin, $0\in(y_0+k)+\partial\psi_C(x_0+h)$ iff $0\in P_Lk+\partial\psi_T(h)$.
4. The correspondence (A.4) (p. 60): for $x$ near $x_0$ and small $y$, (A.2) holds iff $0\in P_L(Ah-y)+\partial\psi_T(h)$ with $h=x-x_0$.

Companions

• Corollary 3.2 (p. 53), in two items. Sufficiency: the reduced form is vacuous, or $B_{11}$ is nonsingular and the Schur complement $B/B_{11}$ is positive definite. Characterisation when $K=\mathbb R^s_+$: strongly regular iff vacuous, or $B_{11}$ nonsingular and $B/B_{11}$ a P-matrix.
• The 3 × 3 linear complementarity example of §4 (p. 53): strongly regular at $x_0=(1,0,0)$, and not strongly regular once the entry $5$ of $A$ becomes $4$.

Significance

Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where $A$ itself is neither positive definite nor a P-matrix.

The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.

Difficulty

The definition of strong regularity is local, while condition (ii) is global on $L$. The obvious argument, "linearise and read off the inverse", does not apply, because $\partial\psi_C$ is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of $y_0$ may move the solution off the face $F$, and only polyhedrality, through the finitely many values of $\partial\psi_C$ on $F$ and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near $0$ to uniqueness on all of $L$. The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is $y-(Ax+a)\in\partial\psi_C(x)$. A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause $x\in C$, so $\partial\psi_C(x)=\emptyset$ off $C$; without it every inclusion would be satisfiable at points outside $C$ and the statements would change meaning.
• $T_C(x_0)$ is the polar of the normal cone, as on p. 58, not the closure of the cone of feasible directions. $F$ is the set of maximisers of $\langle -y_0,\cdot\rangle$ (the sign matters: the opposite face would make the theorem false). $L$ is the direction of the affine span of $F$, and $P_L$ is Mathlib's Submodule.starProjection.
• The reduced form is stated basis-free on $L$; $\partial\psi_T$ is the normal cone of $T$ in all of $\mathbb R^n$. In Corollary 3.2, $B_{11}$ and $B/B_{11}$ are expressed through projectors onto $M$ and $L\cap M^\perp$. Only the case $K=\mathbb R^s_+$ is stated in a basis, an orthonormal basis of $L\cap M^\perp$ in which $K$ is the orthant.
• "Positive definite" does not require symmetry. "Strongly regular" without a constant is existential in $\lambda$, with $\lambda$ real.
• Corollary 3.2's second sentence refers on the page to "(3.8)", an evident slip for (3.9); it is formalized for (3.9).
• The standing assumption "C nonempty polyhedral convex" is a hypothesis of every item.
• A trivializing formalization is ruled out: strong regularity requires existence, uniqueness in $V$ and the Lipschitz bound together, and condition (ii) requires existence and uniqueness for every $z\in L$.
• Needed infrastructure: faces and tangent cones of polyhedra and their local structure (Minkowski–Weyl, finitely many faces), orthogonal decompositions, and Lipschitz continuity of single-valued polyhedral inverses. All of this is reusable beyond this mission. Proofs of the propositions, of the correspondence, and of the companions are welcome independently.

Selected references

• S. M. Robinson, Strongly regular generalized equations, Mathematics of Operations Research 5(1), 43–62, 1980. https://doi.org/10.1287/moor.5.1.43
• S. M. Robinson, Generalized equations and their solutions, Part I: Basic theory, Mathematical Programming Study 10, 128–141, 1979. https://doi.org/10.1007/BFb0120850
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• A. L. Dontchev and R. T. Rockafellar, Implicit Functions and Solution Mappings, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-1-4939-1037-3
• R. W. Cottle, Manifestations of the Schur complement, Linear Algebra and its Applications 8, 189–211, 1974. https://doi.org/10.1016/0024-3795(74)90066-4

Motivation

The job-shop scheduling problem asks how to time a set of tasks on shared machines so that every product is finished as early as possible. Around 1959 several authors proposed to solve it with Gomory's then new integer programming (Gomory 1958). The obstacle is the noninterference condition: two tasks on the same machine must not overlap, so one of them must finish before the other starts. That is an "either-or" condition. It describes a nonconvex set, and classical linear programming cannot express it.

A. S. Manne's note On the Job-Shop Scheduling Problem (Operations Research 8 (1960) 219–223) writes the either-or condition as two linear inequalities in integers. It adds one 0–1 variable per pair of tasks that compete for a machine, and it uses a large constant derived from a bound $T$ on the start days. This is the origin of the big-M disjunctive formulation, which remains the standard textbook integer program for job shops and, more broadly, the standard way to linearize a disjunction of two linear inequalities.

Timeline. Johnson (1954) introduced the make-span criterion for two- and three-stage production schedules. Bowman (1959) and Wagner (1959) proposed integer programs for machine scheduling. Manne (1960), stimulated by Bowman's paper, gave the formulation stated here. He counted its unknowns as 275 for 5 machines with 10 tasks each, against 600 for Wagner's formulation on the same example (p. 222).

Setting

There are $n\ge1$ tasks and $M$ machines. Task $j$ requires the single machine $\mu(j)$ for $a_j$ consecutive days, where $a_j$ is an integer. An integer horizon $T$ bounds the start days: the integer unknown $x_j\in\{0,1,\dots,T\}$ is the day on which task $j$ begins. A pair $(j,k)$ with $j<k$ and $\mu(j)=\mu(k)$ is a conflicting pair. For each such pair the tasks must not overlap:

$$x_j-x_k\ge a_k\quad\text{or else}\quad x_k-x_j\ge a_j. \tag{1}$$

The instance may also impose precedence $x_j+a_j\le x_k$ for given pairs (5a), exact delays $x_j+a_j+\Theta_{jk}=x_k$ for given pairs (5c), and delivery dates $x_j+a_j\le d_j$ for given tasks (6). A schedule is an $x\in\{0,\dots,T\}^n$ satisfying (1), (5a), (5c) and (6). Its make-span is

$$\operatorname{ms}(x)=\max_{j}\,(x_j+a_j),$$

the calendar time needed for all jobs when the shop starts on day $0$.

Manne's integer program has integer unknowns $x_j$ with $0\le x_j\le T$, one integer $y_{jk}$ for each conflicting pair, and the minimand $t$, subject to (5a), (5c), (6),

$$0\le y_{jk}\le 1,\tag{2}$$ $$(T+a_k)\,y_{jk}+(x_j-x_k)\ge a_k,\tag{3}$$ $$(T+a_j)(1-y_{jk})+(x_k-x_j)\ge a_j,\tag{4}$$

and $x_j+a_j\le t$ for every $j$ (7). The value $y_{jk}=1$ means that $j$ precedes $k$; $y_{jk}=0$ means that $k$ precedes $j$.

Formalization targets

Goal: the integer program solves the make-span problem

For every instance and every integer $t^\ast$,

$$t^\ast=\min\{t:\ \exists\,x,y\ \text{integer satisfying } 0\le x_j\le T \text{ and } (2)\text{–}(7)\}\iff t^\ast=\min_{x\ \text{schedule}}\operatorname{ms}(x).$$

Both minima are required to exist. In particular the program has an optimum exactly when a schedule exists. The paper claims this when it says that "the problem now consists of the minimization of $t$" subject to (2)–(7) (p. 221).

Milestones

1. Pair equivalence (p. 220). If $|x_j-x_k|\le T$, some integer $y_{jk}$ satisfies (2)–(4) if and only if (1) holds.
2. Equal start days are excluded (p. 220). If $x_j=x_k$ and $a_j,a_k>0$, no $y_{jk}$ satisfies (2)–(4).
3. Feasibility correspondence (pp. 220–221). For fixed $x$ and $t$, some $y$ makes $(x,y,t)$ feasible for (2)–(7) if and only if $x$ is a schedule with $x_j+a_j\le t$ for all $j$.
4. The $y_{jk}$ must be discrete (p. 222). With $y_{jk}$ real in $[0,1]$ and $0<a_j,a_k\le T$, conditions (3)–(4) admit $x_j=x_k$, where (1) fails.
5. Counting unknowns (pp. 221–222). With $M$ machines of $p$ tasks each, $n=Mp$ and there are $M\,p(p-1)/2$ conflicting pairs; for $M=5$, $p=10$ this gives $50+225=275$ unknowns.

Significance

The result. The goal certifies that a single integer program, with one binary variable per conflicting pair, computes the optimal make-span of a job shop with precedence, exact delays and delivery dates. The same pattern is used whenever a disjunction $f\ge0$ or $g\ge0$ of bounded linear forms has to be put into a mixed-integer program: a binary variable selects the active branch, and a constant at least as large as the range of the inactive form switches the other branch off. Milestone 1 is that pattern in its simplest form, and milestone 4 shows why the binary variable cannot be relaxed.

Formalizing it. The paper's argument is informal. It rests on a summary table of admissible values of $y_{jk}$ that holds only when the gap $|x_j-x_k|$ is large enough. A machine-checked version fixes the exact hypotheses: integrality of $y_{jk}$, the bound $|x_j-x_k|\le T$, and nonemptiness of the task set. To the best of the curators' knowledge, no machine-checked proof of the correctness of the big-M job-shop formulation exists; the definitions here can serve later scheduling missions that need a disjunctive integer program.

Difficulty

The mathematics is elementary, and the difficulty lies in stating it exactly. The obvious reading, "(3)–(4) are equivalent to (1)", is false without the bound $|x_j-x_k|\le T$. For instance, with $y_{jk}=0$ condition (4) reads $x_j-x_k\le T$, which cuts off valid orders if start days may lie beyond the horizon. It is also false for real $y_{jk}$. Equally, "minimize $t$ subject to (7)" equals the maximum of $x_j+a_j$ only after the optimum over $t$ and over $x$ are interchanged and the empty task set is excluded. A naive formalization that states the schedule side as "the least $t$ with (7)" proves nothing about the make-span.

Formalization scope

Tasks are Fin n (the paper's task $j$ is index $j-1$), machines Fin M. Start days, durations, horizon, delays, delivery dates, $y_{jk}$ and $t$ are integers (ℤ), so that $x_j-x_k$ and $1-y_{jk}$ are not truncated. Durations are not assumed positive except in milestones 2 and 4, where positivity is necessary. One definitions file, ManneJobShop.Formulation.Model, holds the instance, the conflicting pairs, schedules, the make-span (Finset.sup', so $n\ge1$ is required via [NeZero n]) and the integer program.

Explicit readings of loose phrases:

• "a (large) integer $T$ that will constitute a redundant upper bound upon the unknowns $x_j$" (p. 219): both the schedule problem and the integer program restrict start days to $0\le x_j\le T$. Redundancy is not assumed.
• "The effect of conditions (3) and (4) may therefore be summarized as follows" (p. 220): stated as the equivalence of milestone 1 and the exclusion of milestone 2, not row by row (for $0<x_j-x_k<a_k$, condition (3) forces $y_{jk}=1$, not $\{0,1\}$).
• "the minimization of $t$" (p. 221): IsLeast of the feasible values of $t$, matched against IsLeast of the set of make-spans of schedules.
• "necessarily of a discrete nature" (p. 222): existence of a real $y_{jk}\in[0,1]$ satisfying (3)–(4) at $x_j=x_k$ when $0<a_j,a_k\le T$ ("large" $T$ read as $T\ge a_j,a_k$).
• "$m$ possible conflicting pairs of machine assignments" (p. 222): pairs $j<k$ on the same machine, one $y_{jk}$ each.
• "If task $j$ is the last task which the shop is to perform upon the item" (p. 221): a delivery date may be attached to any task, which contains the paper's case.

Trivializing formalizations are ruled out: the make-span is a maximum, not a restatement of (7); $y_{jk}$ is an integer; the horizon appears on both sides; the goal is stated for every instance with $n\ge1$, including infeasible ones. The (5b) example is (5a) for two pairs. Wagner's comparison, the remarks on Gomory's algorithm, Dantzig's secondary constraints and Monte Carlo methods, and the economic discussion of the make-span are not formalized. Proofs of every milestone and of the goal are welcome.

Selected references

• A. S. Manne, On the Job-Shop Scheduling Problem, Operations Research 8(2) (1960) 219–223. https://doi.org/10.1287/opre.8.2.219
• E. H. Bowman, The Schedule-Sequencing Problem, Operations Research 7(5) (1959) 621–624. https://doi.org/10.1287/opre.7.5.621
• H. M. Wagner, An Integer Linear-Programming Model for Machine Scheduling, Naval Research Logistics Quarterly 6(2) (1959) 131–140. https://doi.org/10.1002/nav.3800060205
• R. E. Gomory, Outline of an Algorithm for Integer Solutions to Linear Programs, Bulletin of the AMS 64(5) (1958) 275–278. https://doi.org/10.1090/S0002-9904-1958-10224-4
• S. M. Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, Naval Research Logistics Quarterly 1(1) (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

Prediction with expert advice asks a learner to predict a binary label in each of a sequence of trials, having seen the predictions of a pool of $n$ prediction algorithms (the experts), and to make not many more mistakes than the best of them, with no probabilistic assumption on how the instances and labels are generated. Littlestone and Warmuth's Weighted Majority Algorithm (Littlestone, Warmuth 1994) maintains a weight for each pool member, predicts by a weighted vote, and shrinks the weights of members that err. Its mistake bounds are the origin of the multiplicative-weights method used throughout online learning, game theory and optimization (Arora, Hazan, Kale 2012).

A deterministic master with binary predictions can be forced to err in every trial in which the weight is split evenly, which costs it a factor of about two against the best expert. Section 6 of the paper introduces a randomized master, WMR, which predicts $1$ with probability equal to the weighted average prediction of the pool. Theorem 6.1 bounds its expected number of mistakes under a precisely stated condition on how its randomization interacts with the choice of instances and labels.

Timeline:

• 1989: Littlestone and Warmuth's technical report and FOCS paper introduce the Weighted Majority Algorithm and its randomized variant.
• 1991: Maass independently analyses the case $\beta = 0$ with binary pool predictions and a lazy update ([Maa91], cited in the paper).
• 1994: the journal version states the weak independence condition and proves Theorem 6.1 (p. 240).
• 1997: Freund and Schapire's Hedge algorithm recasts the randomized master as a distribution over experts in a decision-theoretic setting (Freund, Schapire 1997).

Setting

A pool of $n$ algorithms is run for $t$ trials on a probability space $(\Omega, \mathcal F, P)$. In trial $j$ the pool member $i$ predicts $x_i^{(j)} \in [0,1]$, the label is $\rho^{(j)} \in \{0,1\}$, and the master predicts $\lambda^{(j)} \in \{0,1\}$. All of these are random variables; deterministic sequences are a special case. Write $x^{(j)} = (x_1^{(j)}, \dots, x_n^{(j)})$.

Each member carries a weight. The initial weights $w_i^{(1)}$ are positive, and the update step (5.1) multiplies the weight of member $i$ in trial $j$ by a factor $F$ that depends on $\beta$, $x_i^{(j)}$ and $\rho^{(j)}$:

$$w_i^{(j+1)} = F\,w_i^{(j)}, \qquad \beta^{|x_i^{(j)}-\rho^{(j)}|} \le F \le 1-(1-\beta)\,|x_i^{(j)}-\rho^{(j)}|,$$

where $0 \le \beta < 1$ and $0^0 = 1$. WMR updates in every trial. Let $s^{(j)} = \sum_i w_i^{(j)}$, so $s^{(1)} = w_{\mathrm{init}}$ and $s^{(t+1)} = w_{\mathrm{fin}}$, and let

$$\gamma^{(j)} = \frac{\sum_{i=1}^n w_i^{(j)} x_i^{(j)}}{s^{(j)}}$$

be the weighted average prediction. WMR predicts $1$ with probability $\gamma^{(j)}$. Its number of mistakes is $m = \sum_{j=1}^t |\lambda^{(j)} - \rho^{(j)}|$.

The weak independence condition (p. 238) requires, for $j = 1, \dots, t$,

$$\mathbf E\big(\lambda^{(j)} \,\big|\, (x^{(1)},\rho^{(1)}), \dots, (x^{(j)},\rho^{(j)})\big) = \gamma^{(j)} \quad \text{almost surely}.$$

The conditioning includes the current predictions of the pool and the current label. It allows instances and labels to depend on the master's past predictions, and it holds, for instance, when WMR draws one uniform number $r \in [0,1]$ and predicts $1$ whenever $\gamma^{(j)} \ge r$, provided the instances and labels are generated independently of $r$.

Formalization targets

Goal: Theorem 6.1

Under the weak independence condition, and with $w_{\mathrm{fin}} > 0$ almost surely,

$$\mathbf E(m) \le \frac{\mathbf E\big(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})\big)}{1-\beta}.$$

The statement fixes neither the pool, nor the update factors within (5.1), nor the distribution of instances and labels.

Milestone: expected mistakes equal expected loss of the weighted average

The step of the proof on p. 240: under the weak independence condition, $\mathbf E(|\lambda^{(j)}-\rho^{(j)}| \mid \mathcal F_j) = |\gamma^{(j)}-\rho^{(j)}|$ almost surely, and hence

$$\mathbf E(m) = \mathbf E\Big(\sum_{j=1}^t |\gamma^{(j)}-\rho^{(j)}|\Big).$$

Significance

Theorem 6.1 gives the randomized master the same bound that Theorem 5.2 gives the deterministic master WMC, whose predictions are allowed to lie in $[0,1]$. With equal initial weights, $\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}) \le \ln n + m_i \ln(1/\beta)$ for every pool member $i$ with total loss $m_i$, and the bound yields Corollary 6.1 (p. 241): $\mathbf E(m) \le (\ln n + \mathbf E(m_i)\ln(1/\beta))/(1-\beta)$. For $\beta$ close to $1$ this is better by nearly a factor of two than the bound for the deterministic binary master WMG. The weak independence condition is also what makes the bound valid against labels that adapt to the master's past predictions, which is the setting of later regret analyses.

The result is proved in the paper; this mission produces a machine-checked version. The platform has proofs of the randomized weighted majority bound in the form of Hazan's Lemma 1.4 and of Mohri et al.'s Theorem 8.4, but both state an expectation over the algorithm's internal distribution with deterministic data, unit weights and one fixed update rule. Neither covers random instances and labels, the conditional-expectation condition, or the whole class of updates (5.1).

Difficulty

The pathwise part of the argument is the loss bound for the weighted average (Lemma 5.3, posed in the companion mission on WMC). The new difficulty is probabilistic. The predictions, labels and weights are random and may depend on each other across trials, so the mistake indicator $|\lambda^{(j)}-\rho^{(j)}|$ cannot be replaced by $|\gamma^{(j)}-\rho^{(j)}|$ pointwise. The replacement holds only after conditioning on the $\sigma$-algebra $\mathcal F_j$, and requires that $\rho^{(j)}$ is $\mathcal F_j$-measurable and binary, so that the indicator is affine in $\lambda^{(j)}$. A reading that conditions on less (dropping the current label) or uses unconditional expectations does not support this step when the label depends on earlier randomness.

A second difficulty is that $\mathbf E(\ln(w_{\mathrm{init}}/w_{\mathrm{fin}}))$ may be infinite: the weights can become arbitrarily small with positive probability.

Formalization scope

The pool is Fin n; trials are indexed from $0$ to $t-1$, so totalWeight … 0 is $w_{\mathrm{init}}$ and totalWeight … t is $w_{\mathrm{fin}}$. The probability space is a measure P with IsProbabilityMeasure P. Predictions, labels and master predictions are real-valued measurable random variables; pool predictions lie in $[0,1]$ and labels and master predictions in $\{0,1\}$ on every sample path. Initial weights are deterministic and positive. The update factor of member $i$ in trial $j$ is a measurable function $F_{j,i}(x, r)$ of the member's prediction and the label, satisfying (5.1) on every sample path; the weights are computed from it, so they are random variables determined by the predictions and labels. $\mathcal F_j$ is the supremum of the $\sigma$-algebras generated by the pairs $(x^{(k)}, \rho^{(k)})$, $k \le j$, and the weak independence condition is stated with Mathlib's conditional expectation P[λ j | 𝓕 j].

Expectations in the goal are lower Lebesgue integrals in $[0,\infty]$, so the right-hand side may be $+\infty$ and no integrability of the logarithm is assumed. The hypothesis $w_{\mathrm{fin}} > 0$ almost surely excludes the case where the paper's bound is infinite and Lean's $\ln 0 = 0$ would make the literal statement false. A formalization that replaces the conditional expectation by the unconditional one, takes the logarithm's Bochner integral (which is $0$ when the logarithm is not integrable), or restricts to deterministic instances and labels does not state Theorem 6.1.

A complete development needs the pathwise loss bound of Lemma 5.3 for this weight model, the pull-out property of conditional expectations for bounded measurable factors, and the exchange of expectation and finite sums. The weight model and the filtration are reusable for Theorem 6.3 and for the lazy variant of the Appendix. Proofs of the milestone and of the goal are welcome, as are formalizations of Corollary 6.1.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

Motivation

In prediction with expert advice, a master algorithm predicts a binary label in each of a sequence of trials, after seeing the predictions of a pool of other algorithms (the "experts"), and is charged one mistake whenever its prediction differs from the label. No probabilistic assumption is made on the sequence: the goal is a bound on the master's mistakes, valid for every sequence, in terms of the mistakes of the best pool member. The Weighted Majority Algorithm of Littlestone and Warmuth (Inform. and Comput. 108, 1994) achieves this for a finite pool of $n$ members with $O(\log n + m_i)$ mistakes, where $m_i$ is the number of mistakes of member $i$.

Many natural pools are infinite: all programs in an enumeration, all hypotheses of a countable class, all values of a discretised parameter. Section 4 of the paper asks whether a master can compete with every member of a countably infinite pool $A_1, A_2, \dots$, making at most $c(\log i + m_i)$ mistakes for every $i$, while keeping only finitely many weights at any time. Running the Weighted Majority Algorithm on infinitely many weights would give such a bound, but cannot be implemented.

Timeline. Barzdin and Freivalds (1972, 1974) studied prediction of a sequence by an enumerable family of functions and gave an essentially optimal bound for the case of a pool containing a member consistent with the whole sequence ($\beta = 0$ below). Littlestone and Warmuth's earlier versions of the paper (1989) introduced an algorithm WMI for infinite pools; the journal version (1994) replaced it by $\mathrm{WMI}_2$, which matches the Barzdin–Freivalds bound when $\beta = 0$ and a consistent member exists, and extends it to pools in which every member may err.

Setting

Fix a parameter $\beta$ with $0 \le \beta < 1$ and put $u = (1+\beta)/2$. Fix two real functions $W$ and $\hat W$ on the positive integers with

$$W(i) > 0, \qquad \sum_{i} W(i) < \infty, \qquad \hat W(i) \ge \sum_{j \ge i} W(j), \qquad \lim_{i \to \infty} \hat W(i) = 0 .$$

$W(i)$ is the initial weight of the pool member $A_i$, and $\hat W(i)$ bounds the weight of the tail $A_i, A_{i+1}, \dots$.

A sequence of $T$ trials gives, for each trial $t$, the prediction $x_t(i) \in \{0,1\}$ of every pool member and a label $\rho_t \in \{0,1\}$. Member $A_i$ makes at most $m_i$ mistakes: $x_t(i) \ne \rho_t$ for at most $m_i$ trials $t$.

The master $\mathrm{WMI}_2$ keeps an active pool $A_1, \dots, A_l$ and a weight for each active member. With $m$ the number of its own mistakes so far, let

$$\theta(m) = \frac{u^{m+1}\,\hat W(1)}{(1-\beta)(m+1)(m+2)} .$$

Initially, and after each trial in which it errs, $\mathrm{WMI}_2$ raises $l$ (starting from $l = 0$) to the least value with $\hat W(l+1) \le \theta(m)$; a newly activated $A_i$ gets weight $W(i)$. In a trial it computes the active weight $q_0$ predicting $0$ and $q_1$ predicting $1$; it predicts $0$ if $q_0 > q_1 + \theta(m)$, predicts $1$ if $q_1 > q_0 + \theta(m)$, and may predict either otherwise. After a mistake, every active member that disagreed with the label has its weight multiplied by $\beta$. The weights $\omega_i$ of the analysis are the current weight of an active member and $W(i)$ for an inactive one.

Formalization targets

The goal is Theorem 4.1, part 3 (p. 227). Let $m$ be the total number of mistakes of $\mathrm{WMI}_2$ on the sequence.

Goal: the mistake bound of $\mathrm{WMI}_2$

If $0 < \beta < 1$, then

$$m \le \inf_{i \ge 1} \frac{\log\bigl(\hat W(1)/W(i)\bigr) + m_i \log(1/\beta) + \log 2}{\log(1/u)} ,$$

and if $\beta = 0$ and $m_i = 0$ for some $i$, then $m \le 1 + \log_2\bigl(\hat W(1)/W(i)\bigr)$.

Milestone: the size of the active pool (Theorem 4.1, part 1)

At the beginning of any trial, $l$ is the minimum $l$ with $\hat W(l+1) \le \theta(m)$, where $m$ counts the mistakes made in prior trials.

Milestone: the weight invariant (Theorem 4.1, part 2)

After any initial sequence of trials in which $m$ mistakes have been made,

$$\sum_{i=1}^{\infty} \omega_i \le \Bigl(2 - \frac{1}{m+1}\Bigr) u^{m}\, \hat W(1) .$$

Significance

The result. The bound holds simultaneously for every pool member, so the master competes with the best member of an infinite pool, paying $\log(\hat W(1)/W(i))$ for the position of that member in the enumeration. With $W(i) = 1/(i(i+1))$ and $\hat W(i) = 1/i$ (the paper's Corollary 4.1) this is $O(\log i + m_i)$ mistakes, with an active pool that grows exponentially in the number of mistakes but is finite at every time. Different choices of $W$ trade the mistake bound against the growth of the active pool. The same analysis shows how the predictions can be computed from finite-precision approximations of the weights, which is the reason for the slack band in the prediction rule. Its $\beta = 0$ case recovers the Barzdin–Freivalds bound.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known to exist, and there is no formalization of the Weighted Majority Algorithm on infinite pools on Prove2Me. The work is to formalize the paper's proof: the size statement for the active pool, the inductive invariant for the total weight, and the final logarithmic bound. The definition of a run of $\mathrm{WMI}_2$, with free predictions in the slack band and lazily activated weights, is reusable for other lazy-activation algorithms on countable pools, and the paper's Corollaries 4.1–4.3 are direct instances once the goal is proved.

Difficulty

The ordinary Weighted Majority analysis tracks the total weight of the whole pool, which shrinks by the factor $u$ after each mistake. For $\mathrm{WMI}_2$ that argument does not apply as is: the master only sees the active weights, and the inactive tail, whose weight is unknown to the algorithm and charged at its initial value, may vote with the label. The obvious bound on the tail is too weak if applied with a fixed slack; it must shrink with the number of mistakes at the right rate so that the accumulated overhead stays below a constant factor. The slack band in the prediction rule interacts with this: when the master errs inside the band, the active majority may not have been wrong by much, and the shrinkage factor must be recovered from the band's width. The factor $2 - 1/(m+1)$ is where these effects are balanced.

Formalization scope

The pool is indexed by ℕ+ and trials by Fin T; false encodes the prediction $0$, true the prediction $1$. IsWMI2Run is a relation between the input sequence and the master's predictions, the weights $w_t(i)$ and the active-pool sizes $l_t$ at every trial boundary $t \in \{0, \dots, T\}$; a prediction inside the slack band is unconstrained, so the theorems hold for every run. Only active weights are constrained; the analysis uses omega, which counts inactive members at $W(i)$. The bound $m_i$ is any upper bound on the mistakes of $A_i$. The tail hypothesis is stated with a tsum together with Summable W, and the milestone on the total weight asserts summability of $\omega$ in its conclusion, so it cannot hold through the value $0$ that Lean assigns to a divergent series. The infimum in the goal is stated as a bound for every $i$, which is equivalent. Logarithms in the ratio are natural logarithms (the base cancels); the $\beta = 0$ bound uses Real.logb 2. The paper requires $W$ and $\hat W$ to be computable; this only makes the algorithm implementable, and the formal statements hold for arbitrary real functions with the stated analytic properties.

A statement for an algorithm whose runs do not exist would be vacuous; runs of $\mathrm{WMI}_2$ exist for every sequence under the hypotheses (this has been checked locally in Lean), because $\hat W \to 0$ and $\theta(m) > 0$ keep the active pool finite.

Needed infrastructure: finite sums over the active pool, tsum manipulations for sequences that agree with $W$ outside a finite set, and real logarithm inequalities. Contributions welcome: proofs of the two milestones and the goal, and the Corollaries 4.1–4.3 as follow-up statements.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• J. M. Barzdin, R. V. Freivalds, On the prediction of general recursive functions, Soviet Mathematics Doklady 13, 1224–1228, 1972.
• J. M. Barzdin, R. V. Freivalds, Prognozirovanie i predel'nyi sintez effektivno perechislimykh klassov funktsii [Prediction and limit synthesis of effectively enumerable classes of functions], in Theory of Algorithms and Programs (J. M. Barzdin, ed.), Vol. 1, 101–111, Latvian State University, 1974 (in Russian).
• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proceedings of the 30th Annual Symposium on Foundations of Computer Science, 256–261, IEEE, 1989 (cited in the journal paper as [LW89a]).

Motivation

Scheduling unrelated parallel machines to minimize the makespan, written $R\,\|\,C_{\max}$, is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within $2\sqrt m$ times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines $m$.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee $2$, independent of $m$. Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.

Setting

There are $n$ jobs and $m\ge 1$ machines. If job $j$ is scheduled on machine $i$, it takes $p_{ij}$ time units, a positive integer. A schedule $\sigma$ assigns every job $j$ to one machine $\sigma(j)$. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$, the makespan of $\sigma$ is the largest load, and $\mathrm{OPT}$ is the minimum makespan over all schedules.

For deadlines $d_1,\dots,d_m$ and a threshold $t$, let $J_i(t)=\{j: p_{ij}\le t\}$ and $M_j(t)=\{i : p_{ij}\le t\}$. The linear program (LP) has variables $x_{ij}\ge 0$ for $j\in J_i(t)$ and constraints

$$\sum_{i\in M_j(t)}x_{ij}=1\quad(j=1,\dots,n),\qquad \sum_{j\in J_i(t)}p_{ij}x_{ij}\le d_i\quad(i=1,\dots,m).$$

The integer program (IP) replaces $d_i$ by $d_i+t$ and requires $x_{ij}\in\{0,1\}$. A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point $\tilde x$ is the bipartite graph on machines and jobs with an edge $(i,j)$ whenever $\tilde x_{ij}>0$.

A $\rho$-relaxed decision procedure answers, for a deadline $d$, either 'no' or a schedule, such that (1) every schedule it returns has makespan at most $\rho d$, and (2) if it answers 'no', no schedule has makespan at most $d$. The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan $t$ is an upper bound $u$, with lower bound $l=\lceil t/m\rceil$, queries the procedure at $d=\lfloor(u+l)/2\rfloor$, moves $u$ to $d$ on a schedule and $l$ to $d+1$ on 'no', and outputs the best schedule found once $l=u$.

The LP rounding procedure answers, on deadline $d$, by solving (LP) with $d_1=\dots=d_m=t=d$: 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex $\tilde x$ chosen by the LP solver, supported on $\tilde x$.

Formalization targets

Goal: Theorem 2

For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure $D$ exists, and for every such $D$ the output $\sigma_D$ of the binary search satisfies

$$\operatorname{makespan}(\sigma_D)\le 2\cdot\mathrm{OPT}.$$

Milestones

1. The support graph of every vertex of (LP) is a pseudoforest: every set $S$ of machines and $T$ of jobs spans at most $|S|+|T|$ edges (§2, p. 4).
2. In a machine–job pseudoforest, every set of jobs of degree at least $2$ can be matched injectively into the machines (§2, pp. 4–5).
3. A schedule supported on a feasible $\tilde x$ with at most one fractional job per machine has loads at most $d_i+t$ (§2, p. 5).
4. Theorem 1 (Rounding Theorem): every vertex $\tilde x$ of (LP) has a schedule $\sigma$ supported on $\tilde x$ with

$$\sum_{j:\sigma(j)=i}p_{ij}\le d_i+t\qquad(i=1,\dots,m).$$

5. Lemma 1: for every $\rho$-relaxed decision procedure, the binary search outputs a schedule of makespan at most $\rho\cdot\mathrm{OPT}$.
6. A schedule with makespan at most $d$ gives a feasible point of (LP) with $d_i=t=d$ (§3, p. 5).
7. The LP rounding procedure is $2$-relaxed (§3, pp. 5–6).

Significance

Theorem 2 gives a constant-factor approximation for $R\,\|\,C_{\max}$ that does not depend on $m$. The same rounding theorem drives the paper's second algorithm, a $(1+\epsilon)$-approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below $3/2$ unless $\mathrm{P}=\mathrm{NP}$. The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.

The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over $T$, optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines $d_i$, arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.

Difficulty

The obvious rounding, putting each job on a machine where $\tilde x_{ij}$ is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound $d_i+t$ requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because $\tilde x$ is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.

On the algorithmic side, the binary search must be shown to return a schedule within $\rho\cdot\mathrm{OPT}$ although the decision procedure is only approximately correct; the invariants (the lower bound stays below $\mathrm{OPT}$, the stored schedule stays within $\rho$ times the upper bound) have to be tracked through a recursion.

Formalization scope

• Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix $(p_{ij})$; $\mathrm{OPT}$ is the makespan of a schedule σopt with IsOptimalSchedule.
• (LP) is modelled on full $m\times n$ real matrices with the entries $p_{ij}>t$ fixed to $0$; this polytope is affinely isomorphic to the paper's, so vertices (Mathlib's Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real $t\ge 0$, more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral $t$.
• Algorithmic wording not formalized. Theorem 2 states "a 2-approximation algorithm ... that runs in time bounded by a polynomial in the input size"; Lemma 1 speaks of polynomial procedures; Theorem 1 adds "this rounding can be done in polynomial time". Running time, the ellipsoid method and vertex finding are not formalized. What is formalized is the guarantee the proofs establish: the binary search, written as a Lean function, returns a schedule within $\rho\cdot\mathrm{OPT}$ (Lemma 1, for every $\rho$-relaxed procedure) and within $2\cdot\mathrm{OPT}$ for every LP rounding procedure and every choice of vertex (Theorem 2).
• Explicit constants: the factor $2$ of Theorem 2 and of the $2$-relaxed procedure, which comes from $d_i+t$ with $d_i=t=d$; the overshoot $t$ of Theorem 1; the initial bounds $u=$ greedy makespan and $l=\lceil u/m\rceil$ (the paper's $t/m$, rounded up because $\mathrm{OPT}$ is an integer); the query point $\lfloor(u+l)/2\rfloor$.
• The LP solver's choice is quantified over by a vertex selector, returning a vertex when (LP) is feasible and nothing otherwise; one always exists, since the polytope is compact.
• Trivializing formalization ruled out. "There is a schedule with makespan at most $2\cdot\mathrm{OPT}$" is trivially witnessed by an optimal schedule; the goal instead bounds the output of the binary search, whose every 'almost' answer must be a rounding of the solver's vertex, supported on it and feasible for (IP).
• Needed infrastructure: extreme points of polytopes given by linear constraints and their tight-constraint rank characterization; bipartite pseudoforests and Hall-type matchings; well-founded recursion for the search. Proofs of any milestone, and reusable lemmas on extreme points of assignment polytopes, are welcome.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source of this mission's statements and numbering); also Proc. 28th IEEE Symposium on Foundations of Computer Science (1987) 217–224
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271, https://doi.org/10.1007/BF01585745
• E. Davis, J. M. Jaffe, Algorithms for scheduling tasks on unrelated processors, Journal of the ACM 28 (1981) 721–736, https://doi.org/10.1145/322276.322284
• D. B. Shmoys, É. Tardos, An approximation algorithm for the generalized assignment problem, Mathematical Programming 62 (1993) 461–474, https://doi.org/10.1007/BF01585178
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3, https://doi.org/10.1007/978-3-540-30717-4

Motivation

The assignment problem asks how to assign $n$ men to $n$ jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.

The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.

• 1931: Kőnig and Egerváry prove the theorem on lines and independent zeros of a matrix that the method rests on.
• 1955: H. W. Kuhn gives the Hungarian method, with finiteness argued for integer matrices through a decreasing integer sum (Kuhn 1955). M. Flood restates it as Steps A–D.
• 1957: J. Munkres gives a fully specified version, in which Step B of Flood's outline (find a minimal set of lines containing all zeros and a maximal set of independent zeros) is carried out by an explicit marking procedure with starred and primed zeros. He proves it correct, shows that the integrality assumption is unnecessary, and bounds the work by a polynomial in $n$ (Munkres 1957).

The mission formalizes Munkres' correctness proof for §1 of that paper.

Setting

Let $A=(x_{ij})$ be a real $n\times n$ matrix, $x_{ij}$ being the cost of assigning man $i$ (row $i$) to job $j$ (column $j$). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation $\sigma$, with $\sigma(r)$ the man doing job $r$. Its cost is $\sum_r x_{\sigma(r)\,r}$, and $\sigma$ is an optimal assignment if this cost is at most that of every permutation $\tau$. Choosing $n$ independent entries of minimum sum is the same as choosing an optimal assignment.

The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros $0^*$, a set of primed zeros $0'$, a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.

• Preliminaries. Subtract from each row its smallest element, then from each column its smallest entry. Consider the zeros in turn and star each one that has no starred zero in its row or column. Cover the columns containing a $0^*$.
• Step 1. Prime a non-covered zero. If its row contains no $0^*$, go to Step 2. Otherwise cover its row and uncover the column of that $0^*$. When no non-covered zero remains, go to Step 3.
• Step 2. Build the alternating sequence $Z_0,Z_1,\dots,Z_{2k}$. It starts at the $0'$ just found. Each $Z_{2i+1}$ is the $0^*$ in the column of $Z_{2i}$, each $Z_{2i+2}$ is the $0'$ in the row of $Z_{2i+1}$, and the sequence stops at a $0'$ with no $0^*$ in its column. Unstar its starred zeros and star its primed zeros. Erase all primes, uncover all rows and cover the columns containing a $0^*$. Stop if all columns are covered; otherwise return to Step 1.
• Step 3. Let $h$ be the smallest non-covered element. Add $h$ to each covered row, subtract $h$ from each uncovered column, and return to Step 1 with all marks kept.

The quantity $n_k$, the maximal number of independent zeros of the matrix $A_k$, measures progress.

Formalization targets

Goal: correctness of the algorithm

For every real $n\times n$ matrix $A$:

$$\exists\,\text{start};\quad \text{every run is finite};\quad \text{no reachable non-final state is stuck};\quad \text{at a final state } \{0^*\}=\{(\sigma(r),r)\}\ \text{with}\ \sum_r x_{\sigma(r)r}=\min_\tau \sum_r x_{\tau(r)r}.$$

The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.

Milestones

1. Remark (2): subtracting row constants $u_i$ and column constants $v_j$ does not change the optimal assignments.
2. The zeros starred in the Preliminaries are independent.
3. At Step 2 the sequence $Z_0,\dots,Z_{2k}$ exists, is unique and has distinct elements.
4. Step 2 leaves an independent set of starred zeros, larger by one.
5. Lines containing all the zeros number at least the maximal number of independent zeros.
6. At Step 3 the starred zeros are a maximal independent set and the covered lines a minimal cover.
7. At Step 3, $h>0$; the transformation subtracts $h$ from non-covered entries, adds $h$ to twice-covered ones, keeps every $0^*$ and $0'$ a zero, and $n_{k+1}\ge n_k$.
8. If $n_{k+1}=n_k$, Step 2 does not occur before the next Step 3, which begins with more covered rows.
9. While $n_k$ is constant, Step 3 is applied at most $n$ times.
10. Every row and column of the matrix always contains a zero.
11. Step 3 decreases the sum of the entries by $n(n-n_k)h$.

Significance

Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its $O(n^3)$ refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.

The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.

Difficulty

Optimality at termination is short once the invariants are known. The work lies in two places.

First, the invariants hold only along runs. "Each $0^*$ is covered by precisely one line", "no column contains more than one $0^*$" and "no row contains more than one $0'$" fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.

Second, termination. The obvious measure, the sum of the entries, decreases by $n(n-n_k)h$ at each Step 3, but for real entries $h$ can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.

Formalization scope

• Matrices and positions. Entries are arbitrary reals, as on p. 35. Positions are Fin n × Fin n (row, column).
• Output orientation. The output permutation follows the published definition HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are $(\sigma(r),r)$, and optimality is IsOptimalAssignment A σ with respect to the original input matrix.
• Nondeterminism. The algorithm is an inductive move relation Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.
• Relational steps. Step 2's sequence and Step 3's $h$ are described relationally. Their existence, and $h>0$, are theorems, not built into the moves.
• Reachable states. Invariants are stated for states reachable from a start state, never for arbitrary states.
• Finiteness. Finiteness of every run is accessibility (Acc) of each start state for the reversed move relation.
• Termination test after the Preliminaries. "If all columns are covered, stop" is also applied when leaving the Preliminaries. The page goes to Step 1 unconditionally there. If the Preliminaries already star $n$ zeros, Step 3 would then have no non-covered element.
• Independent zeros. The maximal number of independent zeros is a finite maximum of cardinalities, so it has no junk value.
• Edge case $n=0$. No positivity of $n$ is assumed. For $n=0$ the start state is final.
• Ruled out. A goal stating only optimality at final states, or invariants stated for arbitrary states, would be a trivializing formalization; the goal states termination of every run and absence of stuck states as well.

Not formalized: the operation count $(11n^3+12n^2+31n)/6$ of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.

Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.

Selected references

• J. Munkres, Algorithms for the assignment and transportation problems, J. Soc. Indust. Appl. Math. 5 (1957), 32–38. https://doi.org/10.1137/0105003
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955), 83–97. https://doi.org/10.1002/nav.3800020109
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223 (source of the published assignment-cost definitions reused here)