All missions

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: the algorithm must compute a good solution and, through payments, make it in each agent's interest to report its input honestly. Nisan and Ronen introduced the field with the problem of scheduling tasks on unrelated machines, where each machine is an agent that privately knows how long it needs for every task (Nisan–Ronen 2001).

The classical tool for truthfulness, the Vickrey–Groves–Clarke (VGC) family of mechanisms, requires the allocation to be exactly optimal. Exact optimization is often computationally out of reach: minimizing the make-span on unrelated machines is NP-hard, and even approximating it within a factor below 3/2 is NP-hard (Lenstra–Shmoys–Tardos 1990). A mechanism designer would therefore like to plug an approximation algorithm into a truthful mechanism and keep truthfulness. This mission formalizes a result showing that the simplest way of doing so fails in the model with verification, where the mechanism may pay after the tasks are performed and observes the actual execution times.

Timeline.

• 1999/2001: Nisan and Ronen define mechanisms with verification and the Compensation-and-Bonus mechanism, prove it strongly truthful when its allocation algorithm is optimal (their Theorem 5.1), and prove that replacing the optimal algorithm by a non-optimal approximation algorithm destroys truthfulness (Theorem 5.6, the goal here). They remark that a similar argument applies to VGC mechanisms.
• 2002: Lehmann, O'Callaghan and Shoham show the analogous failure for VGC payments with approximate allocation in combinatorial auctions (JACM 2002).
• 2007: Nisan and Ronen study which approximation algorithms can be made truthful within the VGC framework (JAIR 2007).

Setting

There are $n \ge 1$ agents and $k$ tasks. The type of agent $i$ is a vector $t^i = (t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the minimum time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x = (x^1,\dots,x^n)$ gives each task to one agent. The make-span is

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j,$$

and $x$ is optimal for $t$ if $g(x,t)\le g(y,t)$ for every allocation $y$.

In the model with verification, an agent's strategy has two parts: a declaration $d^i$ (any positive vector) and an execution plan that, for every allocation the mechanism may choose, fixes the actual time $\tilde t_j \ge t^i_j$ in which the agent performs each task $j$ it receives. An allocation algorithm $x(\cdot)$ maps the declarations to an allocation $x(d)$; the tasks are then executed, producing actual times $\tilde t$.

The Compensation-and-Bonus mechanism based on $x(\cdot)$ pays agent $i$

$$p^i(d,\tilde t) = \sum_{j\in x^i(d)} \tilde t_j \;-\; g\bigl(x(d), \operatorname{corr}^i(x(d),d,\tilde t)\bigr),$$

a compensation for the time actually spent plus a bonus equal to minus the make-span computed from agent $i$'s actual times on its own tasks and the other agents' declared times on theirs (the corrected time vector $\operatorname{corr}^i$). The agent's utility is its payment minus the time it spends. A strategy is dominant if it is at least as good as every alternative whatever the other agents declare and execute; the mechanism is truthful if every agent of every type has a dominant strategy that declares its true type.

Formalization targets

Goal: Theorem 5.6

Let $x(\cdot)$ be an allocation algorithm such that, for some real $c$,

$$g\bigl(x(t),t\bigr) \le c\, g(y,t)\quad\text{for every positive } t \text{ and every allocation } y,$$

and such that $g(y,t) < g(x(t),t)$ for some positive $t$ and some allocation $y$. Then the Compensation-and-Bonus mechanism based on $x(\cdot)$ is not truthful.

The ratio $c$ is arbitrary and existentially quantified: the theorem holds for every finite approximation ratio, so it is stated without a constant.

Milestones

• Claim 5.7. If the mechanism based on $x(\cdot)$ is truthful, $o$ is optimal for $t$ and $M$ is at least every entry of $t$, then replacing one agent's type by $t^i_j$ on $o^i$ and $M$ elsewhere gives a type vector $t'$ with $g(x(t'),t') \ge g(x(t),t)$.
• Corollary 5.8. Under the same assumptions, the type vector $s$ that makes this replacement for every agent satisfies $g(x(s),s) \ge g(x(t),t)$.
• Final step. $g(o,s) = g(o,t)$, $o$ is optimal for $s$, and every allocation $y\ne o$ has $g(y,s)\ge M$.

Significance

The result. Theorem 5.1 of the same paper shows that with an optimal algorithm the Compensation-and-Bonus mechanism is a strongly truthful implementation of make-span minimization. Theorem 5.6 shows that this guarantee is tied to exact optimization: it does not survive replacing the optimizer by any non-optimal approximation algorithm, whatever its ratio. It explains why the paper then turns to a restricted problem (bounded scheduling) and a mechanism designed around a specific rounding algorithm, and it is an early instance of the general tension between approximation and incentive compatibility.

Formalizing it. The result is proved in the paper; to the best of the platform's catalog it has not been formalized. The mission produces a machine-checked model of mechanisms with verification (declarations together with execution plans that may depend on the decision), the Compensation-and-Bonus payment rule for an arbitrary allocation algorithm, and Definition 19 truthfulness, together with a checked proof of the impossibility.

Difficulty

The argument is short on paper; the difficulty lies in the model. The paper's "$\infty$" is not a number, and a faithful statement must replace it by a finite value that is large enough to conflict with the approximation ratio yet keeps every type positive and entrywise above the true types; both requirements refer to data fixed earlier in the argument. The incentive step compares utilities in a mechanism where an agent's strategy is a declaration and an execution plan that may depend on the decision, and where the bonus mixes the agent's actual times with the other agents' declarations, so a naive reading in which only declarations matter (the direct-revelation model of §2) does not capture the claim. Finally, Corollary 5.8 concerns a type vector modified at every agent, while Claim 5.7 modifies one agent at a time, so the claim must be applicable at type vectors that are no longer the original one.

Formalization scope

• Agents are Fin n with [NeZero n], tasks Fin k, allocations are functions Fin k → Fin n, types and declarations are positive real vectors. Make-spans are Finset.sup' over the nonempty set of agents. With no agents no allocation algorithm meets the hypotheses, so requiring $n\ge 1$ loses nothing.
• An execution plan is a function of the allocation; feasibility is $\tilde t_j \ge t^i_j$ on the agent's own tasks. In the dominance quantifier the other agents' declarations are positive and their execution plans arbitrary; the agent's alternative declarations are positive and its alternative plans feasible for its true type.
• The allocation algorithm is an arbitrary function of the declarations; "approximation algorithm" is the hypothesis $\exists c$ above, "non-optimal" the hypothesis of one positive witness. The optimal allocation $\mathrm{opt}(t)$ in the milestones is any optimal allocation $o$, supplied as a parameter.
• The paper's $\infty$ is a real parameter $M$ with $M \ge t^l_j$ for all $l,j$; extended reals are not used.
• Claim 5.7 is stated for an arbitrary agent $i$, not only for agent 1, so that Corollary 5.8 can iterate it.
• Running time is not modelled; "algorithm" means function.
• Dropping the approximation hypothesis makes the statement false: an allocation rule that ignores the declarations is non-optimal, yet its Compensation-and-Bonus mechanism is truthful. Stating only "not strongly truthful", or proving the theorem for a fixed instance, would be a weaker claim.

Welcome contributions: proofs of the milestones and the goal, and reusable lemmas about the corrected time vector and the monotonicity of the make-span in the time vector.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• 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
• D. Lehmann, L. I. O'Callaghan, Y. Shoham, Truth revelation in approximately efficient combinatorial auctions, Journal of the ACM 49 (2002) 577–602. https://doi.org/10.1145/585265.585266
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29 (2007) 19–47. https://doi.org/10.1613/jair.2046
• E. Horowitz, S. Sahni, Exact and approximate algorithms for scheduling nonidentical processors, Journal of the ACM 23 (1976) 317–327. https://doi.org/10.1145/321941.321951

Motivation

In quantum mechanics the energy levels of a system are the eigenvalues of a self-adjoint Hamiltonian $A$, and for almost every Hamiltonian of interest (atoms with more than one electron, molecules) they cannot be computed in closed form. What can be computed are expectation values $\langle \psi, A\psi\rangle$ of explicit trial functions $\psi$. The min-max principle turns such numbers into rigorous statements about the eigenvalues: every trial computation gives an upper bound, and the optimal choices reproduce the eigenvalues exactly. It goes back to Fischer (1905) for quadratic forms in finitely many variables and to Courant (1920) for differential operators; Temple (1928) added the matching lower bound. This mission formalizes the version for unbounded self-adjoint operators with essential spectrum, as stated in Chapter 4 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009), where eigenvalues below the essential spectrum are characterized and estimated.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$, its domain; $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A$ equals its adjoint. The resolvent set $\rho(A)$ is the set of $z \in \mathbb C$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is $\sigma(A) = \mathbb C \setminus \rho(A)$. For self-adjoint $A$, $\sigma(A) \subseteq \mathbb R$.

For $z \in \mathbb C$ the eigenspace is $\operatorname{Ker}(A - z) = \{\psi \in \mathfrak D(A) \mid A\psi = z\psi\}$; $z$ is an eigenvalue when it is nonzero, and its dimension is the multiplicity. The discrete spectrum $\sigma_d(A)$ consists of the eigenvalues that are isolated points of $\sigma(A)$ and have finite multiplicity, and the essential spectrum is $\sigma_{ess}(A) = \sigma(A) \setminus \sigma_d(A)$.

Let $\Sigma = \inf \sigma_{ess}(A) \in [-\infty, +\infty]$ ($+\infty$ if $\sigma_{ess}(A)$ is empty). The numbers $E_1 \le E_2 \le E_3 \le \cdots$ are the eigenvalues of $A$ below $\Sigma$, listed in increasing order and repeated according to multiplicity; if there are only $N$ of them, $E_n = \Sigma$ for $n > N$. For vectors $\psi_1, \dots, \psi_m \in \mathfrak H$ let

$$U(\psi_1, \dots, \psi_m) = \{\psi \in \mathfrak D(A) \mid \|\psi\| = 1,\ \psi \perp \psi_1, \dots, \psi_m\}.$$

Some statements involve the spectral projections $P_A(\Omega)$ of $A$, for Borel sets $\Omega \subseteq \mathbb R$: the projection-valued measure with $A = \int \lambda\, dP_A(\lambda)$. With the spectral measures $\mu_\psi(\Omega) = \langle \psi, P_A(\Omega)\psi\rangle$, the form domain is $\mathfrak Q(A) = \{\psi \mid \int |\lambda|\, d\mu_\psi(\lambda) < \infty\}$, and on it $\langle \psi, A\psi\rangle$ means $\int \lambda\, d\mu_\psi(\lambda)$.

Formalization targets

Goal: the min-max principle (Theorem 4.10)

For self-adjoint $A$ and every $n \ge 1$,

$$E_n = \sup_{\psi_1, \dots, \psi_{n-1} \in \mathfrak H} \ \inf_{\psi \in U(\psi_1, \dots, \psi_{n-1})} \langle \psi, A\psi\rangle .$$

Both sides are extended real numbers; the infimum over an empty set is $+\infty$.

Milestones

• Theorem 2.19 (the case $n = 1$ and its mirror image): $\inf \sigma(A) = \inf_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$ and $\sup \sigma(A) = \sup_{\psi \in \mathfrak D(A), \|\psi\| = 1} \langle\psi, A\psi\rangle$.
• Theorem 4.12 (i): if $\psi_1, \dots, \psi_k \in \mathfrak Q(A)$ are linearly independent and $\langle \psi, A\psi\rangle < \lambda\|\psi\|^2$ for every nonzero $\psi \in \operatorname{span}\{\psi_j\}$, then $\dim \operatorname{Ran} P_A((-\infty,\lambda)) \ge k$; with $>$, $\dim \operatorname{Ran} P_A((\lambda,\infty)) \ge k$.
• Theorem 4.12 (ii): if $\psi_1, \dots, \psi_k \in \mathfrak D(A)$ are linearly independent, $\lambda_1 < \lambda_2$, and $\|(A - \tfrac{\lambda_2+\lambda_1}{2})\psi\| < \tfrac{\lambda_2-\lambda_1}{2}\|\psi\|$ for every nonzero $\psi$ in their span, then $\dim \operatorname{Ran} P_A((\lambda_1,\lambda_2)) \ge k$.
• Corollary 4.11: if $A, B$ are self-adjoint, $\mathfrak D(A) \subseteq \mathfrak D(B)$ and $\langle \psi, (A - B)\psi\rangle \ge 0$ on $\mathfrak D(A)$, then $E_n(A) \ge E_n(B)$ for all $n \ge 1$.
• Theorem 4.13 (Temple's inequality): if $\lambda_1 < \lambda_2$, $\psi \in \mathfrak D(A)$, $\|\psi\| = 1$, $\lambda = \langle \psi, A\psi\rangle \in (\lambda_1, \lambda_2)$ and $\sigma(A) \cap (\lambda_1, \lambda_2) = \{E\}$, then

$$\lambda - \frac{\|(A-\lambda)\psi\|^2}{\lambda_2 - \lambda} \le E \le \lambda + \frac{\|(A-\lambda)\psi\|^2}{\lambda - \lambda_1}.$$

Significance

The min-max principle is the standard tool for comparing eigenvalues of different operators: Corollary 4.11 (monotonicity under operator inequalities) follows from it, and with it the stability of eigenvalues under perturbations, Dirichlet–Neumann bracketing and the Rayleigh–Ritz method used in computational quantum chemistry. Theorem 4.12 converts a finite-dimensional computation into a lower bound for the number of eigenvalues in an interval, and Temple's inequality supplies lower bounds on an eigenvalue to complement the variational upper bounds, which is what makes numerical eigenvalue enclosures rigorous.

All of these results are classical and proved in the literature. What is not available is a machine-checked version for unbounded operators: Mathlib has the Courant–Fischer characterization only for finite-dimensional or compact self-adjoint operators, and existing formal developments of Temple's inequality and min-max levels treat bounded operators. This mission formalizes the unbounded case, with the essential spectrum and the counting of eigenvalues by multiplicity made explicit, and with the edge cases (operators unbounded below, empty essential spectrum) covered by extended-real values.

Difficulty

The central difficulty is that $E_n$ is defined by spectral data (which points of the spectrum are isolated eigenvalues of finite multiplicity, and how many there are below a given level), while the right-hand side is defined by expectation values on the domain. Relating the two needs the spectral theorem for unbounded operators: for every level below $\Sigma$ the spectral subspace must be shown to be finite dimensional and spanned by eigenvectors, and for the level $\Sigma$ itself one needs infinite-dimensional spectral subspaces in every neighbourhood, which is where the essential spectrum enters. When $E_n = \Sigma$ the supremum and infimum need not be attained, so the finite-dimensional argument with eigenvectors does not transfer. For Corollary 4.11 and Temple's inequality the hypotheses concern only the operator and one vector, while the conclusions concern the spectrum.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space; self-adjointness is Mathlib's IsSelfAdjoint, which includes a dense domain. The Hilbert space is not assumed separable. The spectrum is the resolvent spectrum defined above, not Mathlib's Banach-algebra spectrum, and for self-adjoint operators it enters through its real points. Eigenspace dimensions are cardinals (Module.rank). $E_n$ is defined from the spectrum, the essential spectrum and these dimensions, as an element of EReal, indexed from $n = 1$; if $A$ is unbounded below its value is $-\infty$, and if the essential spectrum is empty and the eigenvalues run out it is $+\infty$. The min-max identity is stated in EReal, with $\langle\psi, A\psi\rangle$ entering through its real part.

A formalization that defines $E_n$ as the min-max expression itself would make the goal true by definition. This is ruled out: $E_n$ is defined only from the spectrum, the essential spectrum and the dimensions of eigenspaces.

The spectral theorem is not part of this mission. Theorem 4.12 takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int \lambda\, dP(\lambda)$ (domain $\{\psi \mid \int \lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int \lambda\, d\mu_\psi$), which is the form the spectral theorem guarantees; $P_A$ is then $P$, and $\mathfrak Q(A)$ and the quadratic form are defined from it. Nothing else the book derives is taken as a hypothesis. The goal, Theorem 2.19, Corollary 4.11 and Temple's inequality use no projection-valued measure. Corollary 4.11 states the domain inclusion $\mathfrak D(A) \subseteq \mathfrak D(B)$ explicitly, as the meaning of $A - B \ge 0$.

A complete development needs the spectral theorem for unbounded self-adjoint operators (or an equivalent functional calculus), the identification of $\sigma_{ess}$ with the points where spectral projections have infinite rank, and the orthogonality of eigenspaces. These are reusable across the rest of the book. Proofs of any milestone, and of lemmas connecting the resolvent spectrum with spectral projections, are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Theorem 2.19 (p. 77), Section 4.3–4.4 (pp. 117–120), essential spectrum (p. 145).
• E. Fischer, Über quadratische Formen mit reellen Koeffizienten, Monatshefte für Mathematik und Physik 16 (1905), 234–249. doi:10.1007/BF01693781.
• R. Courant, Über die Eigenwerte bei den Differentialgleichungen der mathematischen Physik, Mathematische Zeitschrift 7 (1920), 1–57. doi:10.1007/BF01199396.
• G. Temple, The theory of Rayleigh's principle as applied to continuous systems, Proceedings of the Royal Society of London A 119 (1928), 276–293. doi:10.1098/rspa.1928.0098.

Motivation

Algorithmic mechanism design studies optimization problems whose inputs are held by self-interested agents: an algorithm must not only compute a good solution but also pay the agents so that reporting their data truthfully is in their own interest. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001) with task scheduling on unrelated machines as the model problem. Each machine is owned by an agent who alone knows how long it takes for each task; the designer wants a schedule of small make-span.

The paper gives a truthful mechanism, MinWork, whose make-span is within a factor $n$ of optimal, and a lower bound of $2$ for every truthful mechanism. It conjectures that no truthful mechanism beats $n$ (Conjecture 4.9) and proves the conjecture for two natural classes. This mission is about one of them, additive mechanisms (Theorem 4.10, p. 180).

Timeline of the gap between $2$ and $n$:

• 1999/2001: Nisan and Ronen prove the lower bound $2$ for all truthful mechanisms and $n$ for additive and for local mechanisms.
• 2007: Christodoulou, Koutsoupias and Vidali raise the general lower bound to $1+\sqrt 2$ for $n\ge 3$ (SODA 2007; Algorithmica 2009).
• 2008: Christodoulou, Koutsoupias and Vidali characterize the truthful mechanisms for two machines (ESA 2008; arXiv 0807.3427); in parallel, Dobzinski and Sundararajan (EC 2008) characterize them and show that for two machines no truthful mechanism beats $2$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no truthful mechanism beats $n$ (STOC 2023; arXiv 2301.11905).

Setting

There are $n$ agents $i=1,\dots,n$ and $k$ tasks $j=1,\dots,k$. The type of agent $i$ is a vector $t^i=(t^i_1,\dots,t^i_k)$ of positive reals, $t^i_j$ being the time agent $i$ needs for task $j$; a type vector $t=(t^1,\dots,t^n)$ collects all types, and $t^{-i}$ denotes the types of the agents other than $i$. An allocation $x=(x^1,\dots,x^n)$ is a partition of the tasks, $x^i$ being the set given to agent $i$. For a set $X$ of tasks write $t^i(X)=\sum_{j\in X}t^i_j$. The make-span is

$$g(x,t)=\max_i t^i(x^i).$$

A direct mechanism $m=(x,p)$ maps every declared type vector $t$ to an allocation $x(t)$ and to payments $p^i(t)$ handed to the agents. An agent with true type $t^i$ gets utility $p^i(t)-t^i(x^i(t))$. The mechanism is truthful if, whatever the others declare, no agent gains by declaring a type other than its true one. It is a $c$-approximation if $g(x(t),t)\le c\,g(y,t)$ for every positive type vector $t$ and every allocation $y$.

The price offered for a set $X$ to agent $i$ (Definition 12) is the payment $p^i(t'^i,t^{-i})$ at any declaration $t'^i$ for which the mechanism gives agent $i$ exactly $X$, and $0$ if there is no such declaration. For truthful mechanisms this is well defined (Proposition 4.4, Independence). The mechanism is additive (Definition 13) if

$$p^i(X,t^{-i})=\sum_{j\in X}p^i(\{j\},t^{-i})$$

for every agent $i$, type vector $t$ and set $X$ of tasks. MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is additive.

Formalization targets

Goal: Theorem 4.10

For $n\ge 1$ agents and $k\ge n^2$ tasks, for every truthful additive mechanism $(x,p)$ and every real $c<n$,

$$\exists\,t,\ \exists\,y:\qquad g\bigl(x(t),t\bigr)>c\cdot g(y,t).$$

The goal leaves the mechanism, its tie-breaking and $c$ completely general. It says that the ratio $n$ of MinWork is optimal among additive mechanisms.

Milestones

1. Proposition 4.4 (Independence): the payment depends on agent $i$'s declaration only through its allocation.
2. Proposition 4.5 (Maximization): $x^i(t)$ maximizes $p^i(X,t^{-i})-t^i(X)$ over the sets $X$ agent $i$ can obtain against $t^{-i}$.
3. Pigeonhole: with $k\ge n^2$ tasks some agent receives at least $n$ tasks.
4. Claim 4.11: at the all-ones type vector $t$, lowering agent $i$'s times to $1-\epsilon$ on $x^i(t)$ and $\epsilon$ elsewhere keeps all of $x^i(t)$ with agent $i$, provided the empty set is attainable for agent $i$.
5. The ratio step: at that perturbed type vector, an allocation giving agent $i$ a fixed set of $n$ tasks has make-span at least $(1-\epsilon)n$, while some allocation has make-span at most $1+k\epsilon$.

Significance

Theorem 4.10 shows that the gap between MinWork's ratio $n$ and the general lower bound $2$ cannot be closed by any mechanism that prices tasks separately, and so any better mechanism would have to couple the prices of different tasks. It was the first class-restricted confirmation of Conjecture 4.9, which was eventually proved for all truthful mechanisms (Christodoulou–Koutsoupias–Kovács 2023). The additive case is the cleanest entry point: its proof needs only the two basic properties of truthful mechanisms, Independence and Maximization, which every later lower bound also uses.

All results here are proved on paper, and none has a machine-checked proof on Prove2Me as of this mission's drafting. The mission produces a formal model of scheduling mechanisms and prices that other lower bounds can reuse, formal statements of Independence and Maximization, and a formal proof of Theorem 4.10. Along the way the formalization corrects two points of the printed argument (see Formalization scope).

Difficulty

The work is to extract prices from an arbitrary truthful mechanism. Prices are defined through the attainable sets of Definition 12. A natural first idea replaces the mechanism by per-task prices $q^i_j(t^{-i})$ that the agent maximizes against. That gives a different class, because Definition 13 constrains the price of every set of tasks, including sets the mechanism never allocates, whose price is $0$.

Claim 4.11 is the critical step, and its printed argument does not go through for an arbitrary truthful additive mechanism. It needs the empty set to be attainable with price $0$. For a mechanism with a bounded ratio this holds, because a very slow agent must receive nothing, but this has to be derived from the approximation hypothesis. From that, one has to show that every task of $x^i(t)$ carries a single-task price of at least $1$. The final step also needs care. The paper's "w.l.o.g. $|x^1|=n$" is a further reduction, and the paper's bound $g\ge|x^1|$ has to be replaced by $(1-\epsilon)|x^1|$.

Formalization scope

• Representation. Agents are Fin n, tasks Fin k, type vectors Fin n → Fin k → ℝ, and an allocation is a map Fin k → Fin n sending each task to its agent. taskSet x i is $x^i$, and the make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]). A mechanism is a pair alloc, pay of arbitrary functions; nothing about its tie-breaking is fixed.
• Standing assumptions. Types are positive. Truthfulness, additivity and approximation quantify over positive type vectors only. Utility is quasi-linear, with payments handed to the agent.
• Prices. price follows Definition 12 literally: the payment at a Classical.choose witness declaration when the set is attainable, and $0$ otherwise. Additivity (IsAdditive) is required for every set of tasks, attainable or not, as Definition 13 states. It is a condition on prices, not on the payment function.
• Explicit threshold. The goal assumes $k\ge n^2$, the value the paper's proof starts from; the printed theorem does not mention $k$. It is stated for every $n\ge1$; at $n=1$ it holds because all allocations coincide.
• Printed slips, corrected. (1) Proposition 4.5 is stated over attainable sets: over all sets, with the price $0$ of unattainable sets, it fails for truthful mechanisms that never give the agent nothing and charge it. (2) Claim 4.11 carries the added hypothesis that $\emptyset$ is attainable for agent $i$. Without it the claim is false: a mechanism that always gives agent $i$ its $|x|$ cheapest tasks and pays nothing is truthful and additive. The claim is stated for an arbitrary agent $i$ instead of "agent 1 after relabelling". (3) The ratio step states $g\ge(1-\epsilon)n$ where the paper prints $g\ge|x^1|\ge n$, and states the paper's w.l.o.g. $|x^1|=n$ as a hypothesis of the step, not of the goal.
• Out of scope. Running time and the revelation principle are not modelled; the goal is stated for truthful direct mechanisms, as §4.3 fixes.
• Ruled out. A trivializing encoding would define additivity through the payment function instead of the prices of Definition 12, fix $n$, prove the ratio for one $c<n$ only, or drop truthfulness. The last makes the claim false: an optimal allocation rule with zero payments is additive and a $1$-approximation. The goal here quantifies over every $n$, every $c<n$ and every truthful additive mechanism.
• Non-vacuity. Every hypothesis of the goal except the ratio is satisfiable (a constant allocation with zero payments is truthful and additive), and the bound is tight by MinWork.
• Contributions welcome. Proofs of the milestones, a proof that a bounded-ratio mechanism makes $\emptyset$ attainable for every agent, and reuse of the model for the local-mechanism bound (Theorem 4.12).

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, SODA 2007; Algorithmica 55, 2009. https://doi.org/10.1007/s00453-008-9165-3
• G. Christodoulou, E. Koutsoupias, A. Vidali, A characterization of 2-player mechanisms for scheduling, ESA 2008. https://arxiv.org/abs/0807.3427
• S. Dobzinski, M. Sundararajan, On characterizations of truthful mechanisms for combinatorial auctions and scheduling, EC 2008, pp. 38–47.
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023. https://doi.org/10.1145/3564246.3585176 (arXiv:2301.11905)

Motivation

The capacitated vehicle routing problem (CVRP) asks for minimum-cost routes, starting and ending at a depot, that serve every customer exactly once without any vehicle carrying more than its capacity. It is one of the central problems of operations research and logistics, and exact algorithms for it have been built on branch-and-cut for three decades: a linear programming relaxation is strengthened at every node of a search tree by adding valid inequalities that the current LP solution violates.

The most important of these inequalities are the capacity inequalities. Deciding whether an LP solution violates one of them is strongly NP-hard, so practical codes rely on heuristics, and most heuristics first shrink the support graph: groups of customers are contracted into single supervertices so that the search runs on a smaller graph. Shrinking is only useful if it is safe, meaning it cannot hide a violated inequality. Before the work of Lysgaard, Letchford and Eglese, the standard safe rule allowed shrinking a single edge whose LP value is at least one (Augerat et al. 1998; Ralphs et al. 2003). Lysgaard, Letchford & Eglese (2004), whose separation routines were released as the widely used CVRPSEP package, generalized the rule to customer sets of any size in their Proposition 1, the only numbered result of the paper.

Setting

Let $G = (V, E)$ be the complete undirected graph on $V = \{0, 1, \dots, n\}$. Vertex $0$ is the depot and $V_c = \{1, \dots, n\}$ are the customers. Vehicles have capacity $Q > 0$ and each customer $i$ has an integer demand $q_i$ with $0 < q_i \le Q$. An LP point is a vector $x = (x_e)_{e \in E}$; $x_{ij}$ and $x_{ji}$ are the same variable, and LP solutions satisfy $x \ge 0$.

For a vertex set $S$, $\delta(S)$ is the set of edges with exactly one end-vertex in $S$ (edges to the depot included), and $x(\delta(S)) = \sum_{e \in \delta(S)} x_e$ is its cut value. For a customer set $S \subseteq V_c$:

• $q(S) = \sum_{i \in S} q_i$ is its total demand;
• $r(S)$, the bin-packing number, is the minimum number of bins of capacity $Q$ into which the items of sizes $q_i$, $i \in S$, can be packed;
• $k(S) = \lceil q(S)/Q \rceil \le r(S)$ is the rounded capacity bound.

The capacity inequalities and the rounded capacity inequalities (RCIs) are

$$x(\delta(S)) \ge 2r(S) \quad\text{and}\quad x(\delta(S)) \ge 2k(S), \qquad S \subseteq V_c,\ |S| \ge 2 .$$

The violation of such an inequality at $x$ is $2r(S) - x(\delta(S))$ (resp. $2k(S) - x(\delta(S))$); it is violated when this is positive.

Shrinking a customer set $S$ contracts it to one supervertex. The supervertices of the shrunk graph are then $S$ and the single customers outside $S$, so a union of supervertices is a customer set $T'$ with $S \subseteq T'$ or $S \cap T' = \emptyset$. Shrinking $S$ is safe if for every customer set $T$ with $|T| \ge 2$ whose inequality is violated, there is such a union $T'$ with $|T'| \ge 2$ and at least the same violation.

Formalization targets

Goal: Proposition 1

For every $x \ge 0$ and every customer set $S$ with

$$x(\delta(S)) \le 2 \qquad\text{and}\qquad x(\delta(R)) \ge 2 \ \text{ for every nonempty proper subset } R \subsetneq S,$$

shrinking $S$ is safe for the capacity inequalities $x(\delta(T)) \ge 2r(T)$.

Milestones (proof of Proposition 1, p. 426)

1. Monotonicity of the bin-packing number: $2r(S \cup T) - 2r(T) \ge 0$.
2. Submodularity of the cut function, in the paper's arrangement: $x(\delta(T)) - x(\delta(S \cup T)) \ge x(\delta(S \cap T)) - x(\delta(S))$ for $x \ge 0$.
3. The crossing-set inequality: if $T$ crosses $S$ ($T \cap S$, $T \setminus S$, $S \setminus T$ all nonempty), then $2r(T) - x(\delta(T)) \le 2r(S \cup T) - x(\delta(S \cup T))$.

Further statements on the same page

4. The same shrinking condition is safe for the rounded capacity inequalities $x(\delta(T)) \ge 2k(T)$, which are the inequalities the algorithm separates.
5. The paper's first separation heuristic checks the RCI for each connected component $S_i$ of the support graph on the customers, for each complement $V_c \setminus S_i$, and for the union of the components with no support edge to the depot. At an integer point satisfying the degree equations $x(\delta(\{i\})) = 2$ and the bounds $x_{ij} \in \{0,1\}$, $x_{0j} \in \{0,1,2\}$, this heuristic finds a violated RCI whenever one exists. This claim is stated in the paper without proof and is not needed for the goal.

Significance

Proposition 1 justifies contracting whole groups of customers before running separation heuristics, which shrinks the graph those heuristics work on while preserving every violated capacity inequality up to its violation. The rule is part of the separation routines of CVRPSEP and of later branch-and-cut and branch-cut-and-price codes for vehicle routing that reuse them.

The result is proved in the paper; to the best of the platform's records, none of it is formalized. The mission produces a reusable formal layer for the two-index CVRP formulation: cut values on the complete graph with a depot, the bin-packing number, the rounded capacity bound, and the notion of safe shrinking. Submodularity of the cut function (target 2) is a classical fact that the paper cites rather than proves; the platform already has a related statement for symmetric weight matrices on Boolean regions (EmergentGeometry.cutWeight_submodular), in a different representation. Target 5 records a claim of the paper that it asserts without proof.

Difficulty

When the violated set $T$ contains $S$ or misses it, $T$ itself is a union of supervertices and there is nothing to show. The difficulty is a set $T$ that crosses $S$: no union of supervertices is obviously as violated as $T$, because enlarging $T$ can raise its cut value — $x(\delta(S \cup T))$ can be smaller or larger than $x(\delta(T))$ depending on the edges leaving $S \setminus T$ — and the hypotheses on $S$ say nothing about $T$ directly. Both hypotheses on $S$ and the sign condition $x \ge 0$ matter here; for signed $x$ the statement fails. A violated $T$ strictly inside $S$ is not a crossing set in the paper's sense and has to be handled as well.

On the formal side, the bin-packing number is an optimum of a combinatorial problem; its properties must be derived from a definition by assignments to bins, and it is well defined only because every demand fits in one vehicle. Target 5 needs a structural understanding of integer points satisfying the degree equations, which the paper does not supply.

Formalization scope

Vertices are Fin (n+1), the depot is 0, and a customer set is a Finset (Fin (n+1)) not containing 0. The edge vector is a function x : Sym2 (Fin (n+1)) → ℝ on unordered pairs, and the cut value is ∑ i ∈ S, ∑ j ∈ Sᶜ, x s(i, j), which includes the edges to the depot. The capacity $Q$ is real (the paper does not say it is an integer) and demands are natural numbers with $0 < q_i \le Q$ for customers. The bin-packing number is the least number of bins over assignments of the customers of $S$ to bins of total demand at most $Q$; under $q_i \le Q$ this minimum exists. Of the LP point only $x \ge 0$ is assumed in Proposition 1 and targets 1–4, which is at least as strong as the paper's setting. The hypothesis "$x(\delta(R)) \ge 2$ for all $R \subset S$" ranges over nonempty proper subsets.

A formalization that lets $R = \emptyset$ in that hypothesis is vacuous, because $x(\delta(\emptyset)) = 0$; one that drops the condition "$S \subseteq T'$ or $S \cap T' = \emptyset$" from safe shrinking is trivial (take $T' = T$); and one that defines $r$ as $k$, as an arbitrary monotone function, or with a junk value $0$, or that omits the depot edges from the cut, states a different result. None of these is the mission's statement.

Needed infrastructure: finite sums over cuts of Sym2-indexed vectors, a working API for the bin-packing number, and, for target 5, connected components of the support graph (SimpleGraph.Reachable). The cut-function lemmas and the bin-packing number are reusable for any later formalization of CVRP polyhedra (framed capacity, comb and multistar inequalities). Contributions of general lemmas about cut functions on complete graphs are welcome as separate theorems.

Selected references

• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming Ser. A 100 (2004) 423–445. https://doi.org/10.1007/s10107-003-0481-8
• G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• P. Augerat, J. M. Belenguer, E. Benavent, A. Corberán, D. Naddef, Separating capacity constraints in the CVRP using tabu search, European Journal of Operational Research 106 (1998) 546–557. https://doi.org/10.1016/S0377-2217(97)00290-7
• T. K. Ralphs, L. Kopman, W. R. Pulleyblank, L. E. Trotter, On the capacitated vehicle routing problem, Mathematical Programming 94 (2003) 343–359. https://doi.org/10.1007/s10107-002-0323-0

Motivation

Column generation solves linear programs with far more columns than can be written down: a restricted master problem holds a few columns, its dual multipliers are passed to a pricing problem, and the pricing problem returns a column to add. It is the standard engine behind branch-and-price for vehicle routing, crew scheduling and cutting stock, where the master problem is very often a set-partitioning problem (Lübbecke and Desrosiers 2005; Desrosiers and Lübbecke 2005).

Which column the pricing problem returns matters. The classical Dantzig rule picks the column of most negative reduced cost, but in set-partitioning masters with identical subproblems this rule tends to produce columns that are "weak" in the dual: their dual constraint is implied by the constraints of smaller columns. Sol (1994, PhD thesis, Eindhoven) called such columns redundant and studied pricing rules that avoid them. In their survey, Lübbecke and Desrosiers state the key fact as Proposition 2 (Operations Research 53(6), p. 1016): under ratio pricing, a strictly redundant column is never the optimal choice.

Setting

Let the rows of a set-partitioning master problem be $\{1,\dots,m\}$. A column is a subset $s$ of the rows, with incidence vector $\mathbf a_s \in \{0,1\}^m$ ($(\mathbf a_s)_i = 1$ iff $i \in s$). Let $\mathcal A$ be a finite collection of nonempty columns with costs $c_s$. The master problem is

$$\min \sum_{s \in \mathcal A} c_s \lambda_s \quad\text{s.t.}\quad \sum_{s \in \mathcal A} \mathbf a_s \lambda_s = \mathbf 1,\ \lambda \ge 0,$$

with $\lambda$ integer in the integer program. Its dual has one free multiplier $u_i$ per row and one constraint $\mathbf u^{\mathsf T}\mathbf a_s \le c_s$ per column.

A column $s$ is redundant, eq. (30), p. 1015, if

$$\mathbf a_s = \sum_{r \subset s} \mathbf a_r \lambda_r \qquad\text{and}\qquad c_s \ge \sum_{r \subset s} c_r \lambda_r ,$$

with $\lambda_r \ge 0$ and $r$ ranging over the columns of $\mathcal A$ that are proper subsets of $s$; then its dual constraint is implied by those of its subcolumns. It is strictly redundant if the cost inequality is strict. The pair $(\mathcal A, \mathbf c)$ has the subcolumn property if $c_r < c_s$ for all $r, s \in \mathcal A$ with $r \subsetneq s$. Given dual multipliers $\bar{\mathbf u} \in \mathbb R^m$, the ratio pricing problem (31) is

$$\min\left\{ \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a} \;\middle|\; \mathbf a \in \mathcal A \right\},$$

the reduced cost per covered row. In Lean these objects are incidence, IsRedundant, IsStrictlyRedundant, SubcolumnProperty and pricingRatio in the namespace Lubbecke2005.SubcolumnPricing.

Formalization targets

Goal: Proposition 2 (p. 1016)

Let $(\mathcal A, \mathbf c)$ satisfy the subcolumn property, $\emptyset \notin \mathcal A$, and let $\bar{\mathbf u} \in \mathbb R^m$ be arbitrary. If $s \in \mathcal A$ is strictly redundant, then

$$\neg\Bigl(\forall \mathbf a \in \mathcal A:\ \frac{c_s - \bar{\mathbf u}^{\mathsf T}\mathbf a_s}{\mathbf 1^{\mathsf T}\mathbf a_s} \le \frac{c(\mathbf a) - \bar{\mathbf u}^{\mathsf T}\mathbf a}{\mathbf 1^{\mathsf T}\mathbf a}\Bigr),$$

that is, $\mathbf a_s$ is not an optimal solution of (31). The paper states the proposition and refers to Sol (1994) for the concept; it gives no proof.

Milestone: the cost shift (§5.1, p. 1016)

If only $c_r \le c_s$ holds for $r \subsetneq s$ in $\mathcal A$, the shifted costs $c'_s = c_s + |s|$ satisfy the subcolumn property, and on every $\lambda$ with $\sum_s \mathbf a_s \lambda_s = \mathbf 1$,

$$\sum_{s} c'_s \lambda_s = \sum_s c_s \lambda_s + m .$$

This is the paper's remark that the shift "adds to $z^\star$ a constant term equal to the number of rows and does not change the problem".

Significance

Proposition 2 is the paper's argument for alternative pricing rules (§5.2): it shows that dividing the reduced cost by the number of covered rows filters out a whole class of columns that contribute nothing to the dual polyhedron, whatever the current dual multipliers are. Steepest-edge pricing, Devex and the lambda pricing rule are motivated along the same lines. The cost-shift remark extends the proposition to cost structures that are only weakly monotone under inclusion, which covers the frequent case of costs that do not decrease when rows are added to a column.

The result is published and elementary once stated precisely, but the paper leaves the definition of redundancy informal (no sign on $\lambda$, no index set of the sum), and those choices decide whether the proposition is true. A formal statement pins them down. To our knowledge neither the proposition nor the vocabulary of redundant columns and ratio pricing has a machine-checked formalization; the definitions here are reusable for other statements about pricing rules in set-partitioning column generation.

Difficulty

The mathematical difficulty is modest; the difficulty is in the reading. With multipliers $\lambda_r$ of arbitrary sign in (30), the proposition is false: on rows $\{1,2,3\}$ take $s = \{1,2,3\}$, $r_1 = \{1,2\}$, $r_2 = \{2,3\}$, $r_3 = \{2\}$ with costs $2.2$, $2$, $2$, $1.9$ and $\bar{\mathbf u} = 0$; then $\mathbf a_s = \mathbf a_{r_1} + \mathbf a_{r_2} - \mathbf a_{r_3}$, $2.2 > 2.1$, the subcolumn property holds, and $s$ has the unique smallest ratio. The empty column is a second trap: its denominator $\mathbf 1^{\mathsf T}\mathbf a$ is zero. The formal statement has to exclude both, and has to keep the minimum in (31) over $\mathcal A$ only.

Formalization scope

Conventions committed to in Lean:

• Rows are Fin m (indexed from $0$); a column is a Finset (Fin m), and its incidence vector is the real 0/1 vector incidence s : Fin m → ℝ. The collection $\mathcal A$ is a Finset (Finset (Fin m)); costs are a function Finset (Fin m) → ℝ, of which only the values on $\mathcal A$ matter.
• Reading of (30): the multipliers are nonnegative ($\lambda_r \ge 0$), the Farkas form of "the corresponding constraint is redundant for the dual problem". The paper leaves the sign implicit; with signed multipliers the proposition fails (example above).
• Reading of $r \subset s$: proper inclusion, over columns $r \in \mathcal A$ only. With $r \subseteq s$ every column would be redundant via $\lambda_s = 1$.
• Strictly redundant: (30) with strict cost inequality; the equality part is unchanged.
• Reading of (31)'s denominator: $\emptyset \notin \mathcal A$ is a hypothesis of the goal ("a set-partitioning column covers at least one row"); it is named here as an addition to the literal text. The denominator is 1 ⬝ᵥ incidence a, which equals $|a|$.
• Dual multipliers: $\bar{\mathbf u} \in \mathbb R^m$ is arbitrary; no sign, no optimality for the restricted master.
• "Cannot be an optimal solution" is stated literally as the negation of "the ratio of $\mathbf a_s$ is at most the ratio of every column of $\mathcal A$"; this is equivalent to the existence of a column with strictly smaller ratio. No infimum over real sets is used.
• The subcolumn property is kept as a hypothesis because the paper states it, although the conclusion may hold without it.
• Cost shift: stated for real multipliers; the optimal value $z^\star$ is not formalized, and "does not change the problem" is rendered as the pointwise identity on the feasible set.

A trivializing formalization — a redundancy witness not tied to the proper subcolumns of $s$ in $\mathcal A$, signed multipliers, or an empty column with ratio $0$ — is ruled out by the definitions above.

Needed infrastructure is only finite sums of vectors in $\mathbb R^m$ and the identity $\mathbf 1^{\mathsf T}\mathbf a_s = |s|$. Contributions welcome: proofs of the goal and the milestone, and further statements from §5 (for example the redundancy characterisation of Sol 1994) built on the same definitions.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• M. Sol, Column Generation Techniques for Pickup and Delivery Problems, PhD thesis, Eindhoven University of Technology, 1994 (cited in the paper as Sol 1994).
• J. Desrosiers and M. E. Lübbecke, A Primer in Column Generation, in Column Generation, Springer, 2005. https://doi.org/10.1007/0-387-25486-2_1
• F. Vanderbeck, Decomposition and Column Generation for Integer Programs, PhD thesis, Université catholique de Louvain, 1994.

Motivation

Many problems in statistics, signal processing and machine learning have the form

$$\min_x\ h(x) + P(\mathcal M x),$$

where $h$ is smooth (a least-squares loss, for instance), $P$ is a nonsmooth regularizer or constraint, and $\mathcal M$ is a linear map such as a finite-difference operator. When $P$ is nonconvex — the cardinality function $\|\cdot\|_0$, the $\ell_{1/2}$ quasi-norm, the indicator of a nonconvex set — the problem is NP-hard in general, and the realistic goal is a stationary point. The alternating direction method of multipliers (ADMM) is widely used on such problems because each iteration splits into a proximal step on $P$ and a smooth step on $h$, but for nonconvex $P$ it was long used without a convergence theory.

Li and Pong (arXiv:1407.0753v6, SIAM J. Optim. 25(4), 2015) gave one of the first general analyses. Their Theorem 1 shows that, under explicit conditions on the penalty parameter and a proximal term, every cluster point of a proximal ADMM sequence is stationary, and that a suitable start is strictly improved on. Earlier, Ames and Hong (arXiv:1401.5492) proved convergence of the plain ADMM for one specific nonconvex quadratic problem with an $\ell_1$ and norm-ball term; Li–Pong's argument follows their idea of bounding the dual changes by the primal changes, together with a descent analysis of the augmented Lagrangian from Wen, Peng, Liu, Bai and Sun (Optimization Online 2013/01/3730).

Setting

Let $h : \mathbb{R}^n \to \mathbb{R}$ be twice continuously differentiable with bounded Hessian $\nabla^2 h$, let $P : \mathbb{R}^m \to (-\infty, +\infty]$ be proper (finite somewhere, never $-\infty$) and closed (lower semicontinuous), and let $\mathcal M : \mathbb{R}^n \to \mathbb{R}^m$ be linear with adjoint $\mathcal M^*$.

A vector $v$ is a regular subgradient of $f$ at $x$ (with $f(x)$ finite) if $\liminf_{z \to x} \frac{f(z) - f(x) - \langle v, z-x\rangle}{\|z - x\|} \ge 0$. The limiting subdifferential $\partial f(x)$ collects all limits $v = \lim v^t$ of regular subgradients $v^t$ at points $x^t \to x$ with $f(x^t) \to f(x)$. A point $x$ is stationary if

$$0 \in \nabla h(x) + \mathcal M^* \partial P(\mathcal M x).$$

For $\beta > 0$ the augmented Lagrangian is $L_\beta(x,y,z) = h(x) + P(y) - \langle z, \mathcal M x - y\rangle + \frac\beta2\|\mathcal M x - y\|^2$, and for a convex $C^2$ function $\phi$ the Bregman distance is $D_\phi(x_1,x_2) = \phi(x_1) - \phi(x_2) - \langle\nabla\phi(x_2), x_1 - x_2\rangle$. The proximal ADMM generates, from arbitrary $x^0, z^0$,

$$y^{t+1} \in \operatorname{Arg\,min}_y L_\beta(x^t, y, z^t),\quad x^{t+1} \in \operatorname{Arg\,min}_x \{L_\beta(x, y^{t+1}, z^t) + D_\phi(x, x^t)\},\quad z^{t+1} = z^t - \beta(\mathcal M x^{t+1} - y^{t+1}).$$

Assumption 1 requires $\mathcal M\mathcal M^* \succeq \sigma\mathcal I$ for some $\sigma > 0$ (so $\mathcal M$ is surjective), Loewner bounds $\mathcal Q_1 \succeq \nabla^2 h \succeq \mathcal Q_2$, $\mathcal T_1^2 \succeq [\nabla^2\phi]^2 \succeq \mathcal T_2^2$ with $\mathcal T_1 \succeq \mathcal T_2 \succeq 0$, $\mathcal Q_3 \succeq [\nabla^2 h + \nabla^2 \phi]^2$, a strong-convexity margin $\mathcal Q_2 + \beta\mathcal M^*\mathcal M + \mathcal T_2 \succeq \delta\mathcal I$, and some $\gamma \in (0,1)$ with $\delta\mathcal I + \mathcal T_2 \succ \frac{2}{\sigma\beta}\big(\frac1\gamma \mathcal Q_3 + \frac1{1-\gamma}\mathcal T_1^2\big)$. Here $\|x\|^2_{\mathcal T} := \langle x, \mathcal T x\rangle$.

Formalization targets

Goal: Theorem 1 (p. 7)

Under the standing assumptions and Assumption 1, for every proximal ADMM sequence:

1. (Global subsequential convergence) at every cluster point $(x^*, y^*, z^*)$,

$$\lim_{t\to\infty}\|y^{t+1}-y^t\|^2 + \|x^{t+1}-x^t\|^2 + \|z^{t+1}-z^t\|^2 = 0,\qquad \nabla h(x^*) = \mathcal M^* z^*,\ \ -z^* \in \partial P(y^*),\ \ y^* = \mathcal M x^*,$$

and $x^*$ is stationary; 2. (Strict improvement) if $x^0$ is not stationary, $h(x^0) + P(\mathcal M x^0) < \infty$ and $\mathcal M^* z^0 = \nabla h(x^0)$, then every cluster point satisfies

$$h(x^*) + P(\mathcal M x^*) < h(x^0) + P(\mathcal M x^0).$$

The theorem does not assert that a cluster point exists; that is the subject of Theorem 2 of the same paper.

Milestones

In attack order: the robustness (3) of $\partial$; the optimality relations (11) of each iterate; the passage from (9) and (10) to (12) and stationarity; the dual-step bound (14); the one-step estimate (20) and its summed form (21) for $L_\beta$; the vanishing of the primal steps (16); the convergence (10) of $P(y^{t_i+1})$; and, for part (ii), $x^1 \ne x^0$, the first-step estimate (27) and the strict decrease after (28).

Significance

Theorem 1 turns the proximal ADMM into a method with a guarantee for a nonconvex $P$: any limit it produces is a stationary point, and with the initialization of part (ii) — for example, a stationary point of a convex relaxation — it cannot return to a stationary point worse than its start. The conditions are checkable: Remark 1 of the paper shows that the choice $\phi(x) = \frac L2\|x\|^2 - h(x)$ turns the $x$-update into a convex quadratic program, and that the last condition of Assumption 1 can be enforced by taking $\beta$ large when $\phi$, $\mathcal T_1$, $\mathcal T_2$ do not depend on $\beta$. The estimate (20) is reused by the paper's boundedness result (Theorem 2), and its whole-sequence convergence result for semi-algebraic data (Theorem 3) starts from Theorem 1.

The result is proved in the paper; Mathlib contains neither the limiting subdifferential nor any convergence theorem for ADMM, so none of it is formalized yet. A formalization would give a verified library of the limiting subdifferential of extended-real-valued functions, its robustness and its Fermat rule with a smooth sum, and the first formally verified convergence theorem for ADMM with a nonconvex term.

Difficulty

The obvious argument — "the augmented Lagrangian decreases, so it converges" — fails: $L_\beta$ need not decrease, because the multiplier step increases it by $\frac1\beta\|z^{t+1}-z^t\|^2$. The proof has to bound this increase by primal steps, which uses surjectivity of $\mathcal M$ and the squared Hessian bounds, and it produces a two-step recursion (involving $x^{t-1}$) rather than a monotone sequence. Nor is $L_\beta$ known to be bounded below; the proof uses the cluster point and lower semicontinuity to get a lower bound along a subsequence. Passing to the limit in the inclusion for $\partial P$ requires $P(y^{t_i+1}) \to P(y^*)$, which lower semicontinuity alone does not give. For part (ii), the start $y^0$ is not an iterate at all, so the first step needs its own estimate.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $\mathcal M$ is a continuous linear map and $\mathcal M^*$ is ContinuousLinearMap.adjoint. $P$ and $L_\beta$ take values in EReal; inequalities involving $L_\beta$ are written additively ($a \le b + r$ with real $r$), never through EReal.toReal. The Hessian is the derivative of the gradient. $\succeq$ is Mathlib's Loewner order on self-maps, which includes symmetry of the difference; $\succ$ adds positive definiteness. $\|x\|^2_{\mathcal T} = \langle x, \mathcal T x\rangle$ for every $\mathcal T$, possibly indefinite. The witnesses of Assumption 1 are explicit parameters, universally quantified. A proximal ADMM sequence is any triple of sequences satisfying the three updates (global minimizers, not necessarily unique); $x^0, z^0$ are free and $y^0$ is unconstrained. A cluster point is the limit along a strictly increasing subsequence. Stationarity is the inclusion (4) itself.

The limiting subdifferential keeps all three requirements of its definition — $x^t \to x$, $f(x^t) \to f(x)$ and $v^t \to v$ — and the domain condition $f(x) < \infty$; dropping $f$-attentive convergence or replacing $\partial$ by the convex subdifferential would make stationarity a different, and for nonconvex $P$ wrong, notion. Part (ii) is a strict inequality for every cluster point, and its hypotheses are exactly non-stationarity of $x^0$, finiteness of the objective at $x^0$ and $\mathcal M^* z^0 = \nabla h(x^0)$. The paper's assumption that proximal maps of $P$ exist is not a hypothesis, since no statement asserts that the iteration can be run.

Needed infrastructure: Fermat's rule and the smooth sum rule for regular subgradients, a diagonal argument for (3), Taylor bounds for $C^2$ functions with Loewner-bounded Hessians (the paper's (5) and (6)), strong convexity from a Hessian lower bound, and the monotonicity of the positive square root in the Loewner order. These are reusable well beyond this mission; contributions of any of them as separate lemmas are welcome.

Selected references

• G. Li, T. K. Pong, Global Convergence of Splitting Methods for Nonconvex Composite Optimization, SIAM J. Optim. 25(4), 2015. arXiv:1407.0753v6, https://arxiv.org/abs/1407.0753 (cited version), DOI https://doi.org/10.1137/140998135
• B. P. W. Ames, M. Hong, Alternating direction method of multipliers for sparse zero-variance discriminant analysis and principal component analysis, preprint, 2014. https://arxiv.org/abs/1401.5492
• Z. Wen, X. Peng, X. Liu, X. Bai, X. Sun, Asset allocation under the Basel accord risk measures, preprint, 2013. http://www.optimization-online.org/DB_HTML/2013/01/3730.html
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$. For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$, the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$. It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$, and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$. The class of maximally monotone operators is $\mathcal M(\mathcal H)$, and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$, the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$. It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$.

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).$$

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

$$x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).$$

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$.

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$. A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$. The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$. Its optimal value is $\mathcal B_D(h)$.

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$, every $\lambda>0$, every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$,

$$\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.$$

The constant is the paper's, and nothing is left unfixed.

Milestones

1. Lemma 4.1. For every $N\ge1$, $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$, $b_N=\frac2N$, $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$.
2. Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$.
3. Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$.
4. Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$, uniformly in $N$. The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$. The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$.

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$. For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$, so its initial-distance condition is on $y_0$, as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$. $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$, the correction term is dropped or has the wrong sign, the initial point is decoupled ($x_0\ne y_0$), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

• D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
• O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
• Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
• G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
• F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
• J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5