Theoretical Computer Science

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements that turns one string into the other. It underlies spelling correction, sequence alignment in computational biology, and file comparison. Wagner and Fischer (J. ACM 21, 1974) computed it for strings of length $n$ in time $O(n^2)$ by filling an $(n+1) \times (n+1)$ matrix. Masek and Paterson (J. Comput. System Sci. 20, 1980) lowered this to $O(n^2/\log n)$ with a "Four Russians" block method: the matrix is cut into $m \times m$ blocks, and the effect of every possible block is tabulated in advance.

The tabulation only pays off if the number of possible blocks is small. The paper guarantees this under two hypotheses: the alphabet is finite, and the edit costs are discrete, that is, all integer multiples of one constant. Its §4 asks whether discreteness can be dropped, and answers no with an explicit example whose costs are $0$, $1$, $\pi$ and $5$. This mission formalizes that example.

Timeline:

• 1974, Wagner and Fischer: the $O(|A|\,|B|)$ matrix algorithm and its recurrence, for nonnegative costs.
• 1980, Masek and Paterson: the $O(n^2/\log n)$ algorithm for a finite alphabet and discrete costs (§2, Lemma 4), and the example of §4 showing the discreteness hypothesis cannot simply be removed (Theorem 5).
• 2015, Backurs and Indyk (STOC 2015): no strongly subquadratic algorithm under the Strong Exponential Time Hypothesis, which places the gap the paper left open in context.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. An edit operation $a \to b$ is a pair of strings of length at most one other than $(\lambda, \lambda)$: a replacement when both are symbols, a deletion when $b = \lambda$, an insertion when $a = \lambda$. $B$ results from $A$ by $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$. A cost function $\gamma$ assigns a nonnegative real to each edit operation; $R_{a,b} = \gamma(a \to b)$, $D_a = \gamma(a \to \lambda)$, $I_a = \gamma(\lambda \to a)$. The edit distance $\delta(\gamma, A, B)$ is the minimum of $\sum_i \gamma(s_i)$ over sequences $s_1, \dots, s_m$ of edit operations taking $A$ to $B$. For fixed strings, $\delta_{i,j} = \delta(\gamma, A^i, B^j)$, where $A^i = A_1 \cdots A_i$; this is the edit matrix. A step is the difference of two horizontally or vertically adjacent entries, $\delta_{i,j} - \delta_{i-1,j}$ or $\delta_{i,j} - \delta_{i,j-1}$, and the possible steps of $\gamma$ are the steps of all edit matrices of all pairs of strings. The cost set $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$ is discrete if some $r > 0$ has every element of $\Omega$ as an integer multiple.

An edit path is a sequence of matrix cells $(p, q)$ in which each cell increases $p$, $q$ or both by one: a deletion of $A_{p+1}$ (cost $D_{A_{p+1}}$), an insertion of $B_{q+1}$ (cost $I_{B_{q+1}}$), or a replacement of $A_{p+1}$ by $B_{q+1}$ (cost $R_{A_{p+1},B_{q+1}}$). The eccentricity of $(i, j)$ is $|i - j|$.

The example. $\Sigma = \{a, b, c\}$ with

$$R_{\sigma,\sigma} = 0,\quad R_{a,b} = R_{b,a} = 1,\quad R_{c,a} = R_{c,b} = R_{a,c} = R_{b,c} = \pi,\quad I_\sigma = D_\sigma = 5.$$

Let $\mu_{2k} = \mu_{2k+1} = \lfloor 2k/(2\pi+1) \rfloor$. The infinite strings $A$ and $B$ are $baba\ldots$ and $abab\ldots$ with a $c$ written into both, at each even position $i$ where $\mu_i > \mu_{i-1}$, so that $A^i$ and $B^i$ each contain exactly $\mu_i$ letters $c$. The first $c$ is at position $8$. $P^*(i, j, k)$ is the minimum cost of an edit path from $(i, j)$ to $(i+k, j+k)$ through points all of eccentricity at least $|i-j|$.

Formalization targets

Goal (Theorem 5, as its proof establishes it)

For the example's $\gamma$, $A$ and $B$,

$$k \mapsto \delta_{k,k+1} - \delta_{k,k} \ \text{ is injective on } \mathbb{N}, \qquad \text{and the set of possible steps of } \gamma \text{ is infinite.}$$

The first part gives at least $n$ distinct steps in the edit matrix of $A^n$ and $B^n$; the second is the negation of the conclusion of the paper's Lemma 4. The goal fixes no constants and no growth rate beyond "at least one new step per diagonal position".

Milestones

1. §2.3: for every nonnegative normalized cost function and all strings, $\delta_{i,j}$ equals the minimum cost of an edit path from $(0,0)$ to $(i,j)$.
2. Lemma 5: $P^*(i,j,k) \ge k - \mu_{i+k} + \mu_i$ if $i - j$ is even, and $P^*(i,j,k) \ge (\mu_{i+k} - \mu_i + \mu_{j+k} - \mu_j)\pi$ if $i - j$ is odd.
3. Lemma 6: for $0 \le k' \le k$, $P^*(0,0,k') + 5 + P^*(k'+1, k', k-k') \ge 5 + (\mu_{k+1} + \mu_k)\pi$.
4. Lemma 7: $\delta_{k,k} = k - \mu_k$ and $\delta_{k,k+1} = \delta_{k+1,k} = 5 + (\mu_{k+1} + \mu_k)\pi$.

A further item records that the example satisfies every other condition of the paper: its costs are nonnegative and normalized ($\gamma(a \to b) = \delta(\gamma, a, b)$), but $\Omega = \{0, 1, \pi, 5\}$ is not discrete.

Significance

The block algorithm precomputes one table entry per block and per pair of initial step vectors, so its preprocessing is polynomial in $n$ only when the number of possible steps is bounded independently of the strings. The example shows that without discreteness the steps can grow with $n$ even over a three-letter alphabet with nonnegative normalized costs, so the table size becomes of order $(kn)^m$ and the method gives no speedup. It explains why the finite-alphabet, non-discrete case is left open in the paper's conclusion.

The paper's result is proved on paper; no machine-checked version is known to exist, and Mathlib has no edit distance at the pinned revision. The formalization produces exact closed forms for three diagonals of a nontrivial edit matrix with irrational entries, a formal link between edit distance over arbitrary edit sequences and minimum-cost paths, and a verified counterexample to the naive generalization of the algorithm. The sibling mission of the series formalizes the algorithm and Lemma 4.

Difficulty

The central difficulty is Lemma 5: a lower bound on the cost of every path confined to a band of eccentricity, not only the straight diagonal. A path may leave its diagonal, pay $10$ for a deletion and an insertion, and travel along another diagonal whose $c$'s may or may not line up. The bound must hold uniformly in $i$, $j$ and $k$, and it depends on the floor function $\mu$ and on precise inequalities between $\mu_{r+s} - \mu_r$ and $s/(2\pi+1)$. Checking that the straight diagonals are optimal for small $k$ does not suffice: the $c$-densities are chosen so that even and odd diagonals cost almost exactly the same per step, and a periodic placement of $c$'s would let one diagonal eventually undercut another.

Formalization scope

Strings are Lists; the infinite strings $A$, $B$ are functions $\mathbb{N} \to \Sigma$ read from index $1$, and $A^n$ is the list of their first $n$ symbols. An edit operation is a pair of Option values other than $(\text{none}, \text{none})$. The edit distance and $P^*$ are real infima (sInf) of nonempty sets of nonnegative reals, so they coincide with the paper's minima. $\delta_{i,j}$ has $i$ indexing $A$ and $j$ indexing $B$ (the paper's Figure 4 prints $A$ across the columns). $\mu_i$ is $\lfloor 2\lfloor i/2 \rfloor/(2\pi+1) \rfloor$. The constraint of $P^*$ applies to every point of the path, endpoints included. Costs use Real.pi itself.

Pinned statements: the paper states Theorem 5 about the running time of Algorithm Y ("Discreteness is a necessary condition for Algorithm Y to run in time $O(k^m)$ on length $m$ strings and step sequences"); its proof establishes that the number of distinct steps grows linearly with the string length, which is what the goal states. Running time is not formalized. The §2.3 milestone is stated, as in the paper, for all strings and every nonnegative cost function satisfying the §1.1 normalization $\gamma(a \to b) = \delta(\gamma, a, b)$; both standing assumptions are hypotheses. The paper's standing assumption $|A| \ge |B|$ is used only for running times and is omitted.

The example must be the paper's: replacing $\pi$ by a rational, or quantifying over "some" cost function or "some" strings, makes the goal false or empty, and the edit distance must be the minimum over edit sequences, not a recurrence.

Needed infrastructure: edit sequences and their costs, the reduction of edit sequences to edit paths, and bounds on $\lfloor \cdot \rfloor$ with $\pi$ (Mathlib's irrational_pi and Real.pi_gt_d2). The edit-distance definitions are shared in shape with the sibling mission and are reusable. Proofs of any milestone are welcome.

Selected references

• W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
• R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
• A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015, 51–58. https://doi.org/10.1145/2746539.2746612

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a function with diminishing returns: the cut of a graph or a directed graph, the value of a facility-location configuration, the entropy of a set of random variables, or a welfare function in combinatorial auctions. These functions are submodular but typically non-monotone: adding elements can decrease the value. Max Cut and Max Directed Cut are the textbook special cases. Unconstrained maximization of a nonnegative non-monotone submodular function is NP-hard, and before Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) no constant-factor approximation was known for general such functions in the value-oracle model.

The paper gives several algorithms. A uniformly random set achieves $1/4$ of the optimum (a separate mission of this series). This mission concerns the paper's first deterministic algorithm: a local search that repeatedly adds or removes a single element while the value improves by a factor larger than $1 + \epsilon/n^2$, and returns the better of the final set and its complement. The key structural fact behind it, that a local optimum of a submodular function dominates all its subsets and supersets, goes back to Cherenin (1962) and Goldengorin, Tijssen and Tso (1999).

Timeline. Cherenin (1962) and Goldengorin–Tijssen–Tso (1999): local optima dominate comparable sets. Schäffer and Yannakakis (SIAM J. Comput. 1991): finding an exact local optimum of Max Cut is PLS-complete, which is why the algorithm here uses an approximate improvement threshold. Feige–Mirrokni–Vondrák (FOCS 2007; SIAM J. Comput. 2011): the $1/3$ and $1/2$ guarantees of this mission, and $2/5$ for a randomized "smooth" local search. Buchbinder, Feldman, Naor and Schwartz (SIAM J. Comput. 2015): a randomized double-greedy $1/2$-approximation, which is optimal in the value-oracle model by the lower bound of the same 2011 paper.

Setting

Let $X$ be a finite ground set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every $S \subseteq X$. It is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

and symmetric if $f(X \setminus S) = f(S)$ for all $S$. Throughout the section of the paper formalized here, $f$ is nonnegative. The algorithm may query $f(S)$ for any $S$ (a value oracle). The optimum is $\mathrm{OPT} = \max_{S \subseteq X} f(S)$.

A set $S$ is a local optimum if $f(S \cup \{a\}) \le f(S)$ for every $a \notin S$ and $f(S \setminus \{a\}) \le f(S)$ for every $a \in S$. It is a $(1+\alpha)$-approximate local optimum (Definition 3.2) if $(1+\alpha)f(S) \ge f(S \setminus \{v\})$ for $v \in S$ and $(1+\alpha)f(S) \ge f(S \cup \{v\})$ for $v \notin S$.

Algorithm LS with parameter $\epsilon > 0$ and $c = 1 + \epsilon/n^2$:

1. Let $S := \{v\}$, where $f(\{v\})$ is the maximum over all singletons.
2. If some $a \in X \setminus S$ has $f(S \cup \{a\}) > c\,f(S)$, let $S := S \cup \{a\}$ and repeat step 2.
3. If some $a \in S$ has $f(S \setminus \{a\}) > c\,f(S)$, let $S := S \setminus \{a\}$ and go back to step 2.
4. Return $\max\{f(S), f(X \setminus S)\}$.

In Lean these are Submodular, SymmetricSetFun, OPT, IsLocalOptimum, IsApproxLocalOptimum, lsStep, IsLSRun, IsLSTerminal and lsOutput in NonmonotoneSubmod.LocalSearch.

Formalization targets

Goal: Theorem 3.4 (p. 1141)

For nonnegative submodular $f$ on a nonempty $X$ and $\epsilon > 0$, every run of Algorithm LS, with any choice of starting singleton and of improving elements, satisfies:

$$\text{at termination at } S:\qquad \max\{f(S), f(X\setminus S)\} \ge \Big(\frac13 - \frac{\epsilon}{n}\Big)\mathrm{OPT};$$ $$\text{if } f \text{ is symmetric, at termination at } S:\qquad f(S) \ge \Big(\frac12 - \frac{\epsilon}{n}\Big)\mathrm{OPT};$$ $$\text{if } n \ge 2, \text{ after any } k \text{ steps}:\qquad \Big(1 + \frac{\epsilon}{n^2}\Big)^k \le n.$$

The last line is the explicit content of the printed bound of $O(\frac1\epsilon n^3 \log n)$ oracle calls: it gives $k = O(\frac1\epsilon n^2 \log n)$ steps of at most $2n$ queries each, and in particular termination.

Milestones, in attack order

1. Lemma 3.1: a local optimum $S$ of a submodular $f$ satisfies $f(T) \le f(S)$ whenever $T \subseteq S$ or $T \supseteq S$.
2. Lemma 3.3: for a $(1+\alpha)$-approximate local optimum, $f(T) \le (1 + n\alpha) f(S)$ for such $T$.
3. Termination bridge (sentence after Algorithm LS): a set at which LS has terminated is a $(1+\epsilon/n^2)$-approximate local optimum.
4. First display of the proof: $2(1+n\alpha)f(S) + f(X\setminus S) \ge f(C)$ for every $C$.
5. Second display, symmetric case: $2(1+n\alpha)f(S) \ge f(C)$ for every $C$.
6. $\mathrm{OPT} \le n f(\{v\})$ for a maximum-value singleton, when $n \ge 2$.
7. Growth along a run: $f(S_k) \ge (1+\epsilon/n^2)^k f(\{v\})$.

Significance

The result. Theorem 3.4 is the deterministic constant-factor approximation of the paper that first gave guaranteed approximation factors for maximizing general nonnegative submodular functions ("Prior to our work, to the best of our knowledge, no guaranteed approximation factor was known", p. 1135), and the $1/2$ bound for symmetric functions matches the value-oracle lower bound proved in the same paper (so it is optimal for symmetric functions among algorithms using polynomially many queries). Local search with a multiplicative acceptance threshold was subsequently used for constrained non-monotone submodular maximization (matroid and knapsack constraints, Lee–Mirrokni–Nagarajan–Sviridenko 2010).

Formalizing it. The result is proved; to our knowledge neither the theorem nor Lemmas 3.1 and 3.3 has a machine-checked proof. The mission produces a reusable finite model of set functions and single-element local search over Finset, with the algorithm stated as a nondeterministic step relation, so that the guarantee is proved for every tie-breaking rule. The same model is the starting point for formalizing other local-search guarantees.

Difficulty

The natural first idea, to argue from an exact local optimum via Lemma 3.1, does not apply: LS stops at an approximate local optimum, and the error $\alpha$ per element must be accumulated along a chain of up to $n$ single-element changes between $S$ and $S \cap C$ or $S \cup C$. This accumulation is where the nonnegativity of $f$ enters (the lemma fails for negative-valued $f$), and where the factor $n\alpha = \epsilon/n$ in the final ratio comes from. The running-time bound requires relating $\mathrm{OPT}$ to the best singleton, which uses submodularity on sets of all sizes and breaks down on a one-element ground set. A further bookkeeping difficulty is the algorithm itself: its steps are ordered (removals only when no addition applies), and the termination bridge must use that order.

Formalization scope

• Ground set: X : Type with [Fintype X] [DecidableEq X]; subsets are Finset X; $f$ is Finset X → ℝ; complements are Sᶜ. $n$ is (Fintype.card X : ℝ).
• Nonnegativity is the hypothesis ∀ S, 0 ≤ f S (standing assumption of §3); Lemma 3.1 and the termination bridge are stated without it, as they need none.
• $\mathrm{OPT}$ is the maximum over all subsets (Finset.sup'), never a supremum with a default value.
• The algorithm is a relation: a run is a sequence S : ℕ → Finset X with S 0 = {v} for any maximum-value singleton v and consecutive sets related by an LS step; the theorems quantify over all runs. Steps use strict inequalities, termination their negation, exactly as printed.
• Added hypotheses, each disclosed in the item statements: $\epsilon > 0$ (implicit in the paper); $X \neq \emptyset$ for the goal; $\alpha \ge 0$ and $f \ge 0$ for Lemma 3.3 and the displays; $n \ge 2$ for $\mathrm{OPT} \le n f(\{v\})$ and the step bound (both false for $n = 1$: $f(\emptyset) = 5$, $f(\{v\}) = 0$). The displays are stated for every set $C$, not only an optimal one.
• The printed $O(\frac1\epsilon n^3 \log n)$ oracle-call bound, an asymptotic statement with an unquantified constant, is replaced by the explicit step bound $(1+\epsilon/n^2)^k \le n$ that its proof establishes.
• Ruling out trivialization: the goal names the algorithm (its start at a maximum singleton, its ordered step rules, termination, and the returned maximum). A statement "for every $(1+\alpha)$-approximate local optimum" is a milestone, not the theorem; an exact local optimum ($\alpha = 0$) is a different algorithm.
• Not in scope: the tight example of pp. 1141–1142, the randomized local search of §3.2, and the hardness results of §4.

Contributions welcome: proofs of the milestones, general lemmas about chains of single-element changes in Finset, and the derivation of the goal from them.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• V. Cherenin, Solving some combinatorial problems of optimal planning by the method of successive calculations, Novosibirsk, 1962 (in Russian).
• B. Goldengorin, G. Tijssen, M. Tso, The Maximization of Submodular Functions: Old and New Proofs for the Correctness of the Dichotomy Algorithm, SOM report, University of Groningen, 1999.
• A. A. Schäffer, M. Yannakakis, Simple local search problems that are hard to solve, SIAM J. Comput. 20(1):56–87, 1991. https://doi.org/10.1137/0220004
• J. Lee, V. S. Mirrokni, V. Nagarajan, M. Sviridenko, Maximizing nonmonotone submodular functions under matroid or knapsack constraints, SIAM J. Discrete Math. 23(4):2053–2078, 2010. https://doi.org/10.1137/090750020
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A tight linear time (1/2)-approximation for unconstrained submodular maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

The k-median problem asks to open $k$ facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.

Local search is the method most used in practice: start from any $k$ facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only $k$ medians. For single swaps they proved a locality gap of $5$ (Theorem 3.2, the subject of the first mission of this series); allowing up to $p$ facilities to be exchanged at once improves the gap to $3 + 2/p$, which the paper notes improves on the $4$-approximation of Charikar and Guha. That $p$-swap bound is the result this mission formalizes.

Timeline (as recounted in §1 of the paper):

• Shmoys, Tardos and Aardal, and Charikar, Guha, Tardos and Shmoys: LP rounding gives a $6\tfrac23$-approximation for k-median.
• Jain and Vazirani: primal–dual schema and Lagrangian relaxation give a $6$-approximation; Charikar and Guha improve it to $4$.
• Korupolu, Plaxton and Rajaraman: local search with add, delete and swap moves gives a solution with $k(1+\epsilon)$ facilities and service cost at most $3 + 5/\epsilon$ times the optimum.
• Arya et al.: locality gap $5$ for single swaps and $3 + 2/p$ for $p$-swaps with exactly $k$ facilities, with a tight example.
• Later work (Li and Svensson, 2013/2016) goes below $3$ with methods other than local search.

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality; $c_{ji} = d(j,i)$ is the cost of serving client $j$ by facility $i$.

For a nonempty set $S \subseteq F$ of open facilities, each client is served by its nearest open facility, and

$$\mathrm{cost}(S) = \sum_{j \in C} \min_{i \in S} c_{ji}.$$

Fix an integer $p \ge 1$. A $p$-swap $\langle A, B\rangle$ deletes a set $A \subseteq S$ of at most $p$ facilities and adds a set $B \subseteq F$ of the same size. The $p$-swap neighbourhood of $S$ is

$$\mathcal B(S) = \{(S \setminus A) \cup B \mid A \subseteq S,\ B \subseteq F,\ |A| = |B| \le p\},$$

and $S$ is locally optimum when $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.

In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.

Formalization targets

Goal: locality gap at most $3 + 2/p$

For every metric instance, every integer $p \ge 1$, every $k \ge 1$, every locally optimum $S$ with $|S| = k$, and every nonempty $O \subseteq F$ with $|O| \le k$,

$$\mathrm{cost}(S) \le \left(3 + \frac{2}{p}\right)\mathrm{cost}(O).$$

This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution $O$ is arbitrary, not only an optimum, which is the strongest form printed.

Milestones

1. §3.4, p. 551: for sets $X, Y \subseteq S$, disjoint sets have disjoint captures, and $X \subseteq Y$ implies $\mathrm{capture}(X) \subseteq \mathrm{capture}(Y)$, where $\mathrm{capture}(A) = \{o \in O \mid |N_S(A) \cap N_O(o)| > |N_O(o)|/2\}$.
2. Claim 3.1, p. 552: when $|S| = |O|$, there are partitions $A_1,\dots,A_r$ of $S$ and $B_1,\dots,B_r$ of $O$ with $|A_i| = |B_i|$, $B_i = \mathrm{capture}(A_i)$ and exactly one bad facility in $A_i$ for $i < r$, and only good facilities in $A_r$.
3. §3.4, pp. 552–553: a family of swaps of size at most $p$ with positive weights, such that each $o \in O$ is swapped in with total weight exactly $1$, each $s \in S$ is swapped out with total weight at most $(p+1)/p$, and $\mathrm{capture}(A) \subseteq B$ for every swap $\langle A, B\rangle$.
4. Property 3.2, p. 553: a bijection $\pi$ of $N_O(o)$ with $\pi(P) \cap P = \emptyset$ for every class $P$ of a partition of $N_O(o)$ with $|P| \le \tfrac12|N_O(o)|$.

Significance

The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to $3$ as the neighbourhood grows; the paper's tight example (§3.5, given for $p = 2$ and stated to generalize to every $p$) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard $\varepsilon$-improvement rule (p. 548), it yields a polynomial-time $(3 + 2/p + \varepsilon)$-approximation. The analysis template (charging each client's reassignment through a bijection of $N_O(o)$, and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.

The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.

Difficulty

For single swaps each facility of $O$ is paired with one facility of $S$ and a direct counting argument suffices. With $p$-swaps, a facility of $S$ may capture several facilities of $O$ at once, and a group of facilities of $S$ may jointly capture a facility of $O$ that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most $p$ members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of $O$ is counted exactly once while no facility of $S$ is counted more than $(p+1)/p$ times. Getting the constant $3 + 2/p$ (rather than a weaker one) depends on this exact accounting.

Formalization scope

• Clients and facilities are types Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).
• The cost is the nearest-facility cost of a nonempty set; the empty set has no cost, so no junk value enters. The bound is stated multiplied out, kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in $\mathbb R$.
• $|S| = k$ is required; $O$ ranges over all nonempty sets with $|O| \le k$. §3.3 introduces multiswaps with $p > 1$; the statement takes $p \ge 1$, where $p = 1$ is Theorem 3.2 (bound $5$).
• Local optimality is over the whole neighbourhood (3), including sets $B$ that meet $S$, not only over the swaps used in the analysis. Restricting it to those swaps would state a theorem with a stronger hypothesis.
• The milestones state Claim 3.1, the swap construction and Property 3.2 in existence form; the procedure of Figure 8 is not formalized. Capture, good and bad are computed against the original $S$ and $O$. The client assignments in the milestones are arbitrary functions; nearest-facility assignments are a special case. Milestone 3 also records that the deleted sets of two swaps are equal or disjoint, which is immediate from the construction and is what makes Property 3.2 applicable.
• The per-swap reassignment inequality is not a milestone: the paper describes it only as "similar to the one presented for the single-swap heuristic" and prints no inequality.
• Out of scope: the tight example (§3.5), the polynomial-time wrapper, and arbitrary client demands.

Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. Charikar, S. Guha, É. Tardos, D. Shmoys, A Constant-Factor Approximation Algorithm for the k-Median Problem, J. Comput. System Sci. 65(1):129–149, 2002. https://doi.org/10.1006/jcss.2002.1882
• K. Jain, V. Vazirani, Approximation Algorithms for Metric Facility Location and k-Median Problems Using the Primal-Dual Schema and Lagrangian Relaxation, J. ACM 48(2):274–296, 2001. https://doi.org/10.1145/375827.375845
• M. Korupolu, C. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• S. Li, O. Svensson, Approximating k-Median via Pseudo-Approximation, SIAM J. Comput. 45(2):530–547, 2016. https://doi.org/10.1137/130938645

Motivation

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

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

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

Timeline:

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

Setting

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

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

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

$$b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.$$

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

The algorithm of §4 is:

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

Formalization targets

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

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

$$\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .$$

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

Milestones

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most $k$ elements its output is never more than the harmonic number $H(k) = \sum_{j=1}^k 1/j$ times the optimum, and that this factor is attained.

Timeline.

• 1974: Johnson proves the $H(k)$ bound for unweighted set cover with sets of size at most $k$, together with a matching family of examples (this mission).
• 1975: Lovász proves the same bound for the fractional relaxation, giving an integrality-gap statement (Lovász 1975).
• 1979: Chvátal extends the bound to weighted set cover, with the greedy rule choosing the set of least cost per newly covered point (Chvátal 1979).
• 1998: Feige shows that no polynomial-time algorithm achieves $(1-\varepsilon)\ln n$ unless NP has slightly superpolynomial deterministic algorithms (Feige 1998), so the greedy guarantee is essentially the best possible.

Setting

An input $F$ of SET COVERING I is a finite family $\{S_1, \dots, S_p\}$ of finite sets. The set to be covered is $T = \bigcup_{S \in F} S$. A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S \in F'} S = T$, and its measure is $|F'|$. The optimum $F^*$ is the minimum measure of a subcover; $F$ itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than $k$ elements.

Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET$[i]$ holding the still-uncovered part of $S_i$. It starts with SUB $= \emptyset$, UNCOV $= T$, SET$[i] = S_i$. While UNCOV is nonempty it chooses an index $j$ with $|\mathrm{SET}[j]|$ maximal, adds $S_j$ to SUB, and removes SET$[j]$ from UNCOV and from every SET$[i]$. When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value $C1(F)$ is the worst choosable output, here the largest, and the ratio is $r(C1, F) = C1(F)/F^*$.

For the proof the paper introduces configurations $K = \langle N_K, \mathrm{UNCOV}_K, \langle \mathrm{SET}_K[1], \dots, \mathrm{SET}_K[N_K]\rangle\rangle$ with $\bigcup_i \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$, runs from a configuration (sequences of admissible choices ending when UNCOV is empty), $\mathrm{Numbers}(R)$, the set of indices chosen in a run $R$, and calls a set $M$ selectable from $K$ if $M = \mathrm{Numbers}(R)$ for some run $R$ from $K$. Write $n(K, i) = |\mathrm{SET}_K[i]|$.

Formalization targets

Goal: Theorem 4

For every $k \ge 1$:

$$\text{for every input } F \in SC(k) \text{ and every choosable } F_1:\quad |F_1| \le H(k)\cdot F^*,$$ $$\text{and some } F \in SC(k) \text{ with } F^* > 0 \text{ has a choosable } F_1 \text{ with } |F_1| = H(k)\cdot F^*.$$

The paper states this as $R[C1, SC(k)](n) \le \sum_{j=1}^k (1/j)$ for all $n > 0$, with equality for all sufficiently large $n$. The two-part form above is the size-free equivalent.

Milestones

1. Lemma 1. For a subcover $F_1$ with index set $M1 = \{i : S_i \in F_1\}$ and $K$ the configuration after Step 1: $F_1$ is choosable by C1 if and only if $M1$ is selectable from $K$.
2. Lemma 2. For any configuration $K$, any $M1$ selectable from $K$ and any $M0$ with $\bigcup_{i \in M0} \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$:

$$|M1| \le \sum_{i \in M0} \sum_{j=1}^{n(K,i)} \frac{1}{j}.$$

3. Fig. 1. For every $k \ge 1$ there is an explicit input of $SC(k)$ on $k \cdot k!$ points with $F^* = k!$ and a choosable output of $k!\,H(k)$ sets.

Significance

The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant $H(k)$ cannot be lowered for any $k$. Since $H(k) \le 1 + \ln k$, it also gives the well-known $1 + \ln n$ bound for general inputs. The $H(k)$ bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.

Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the $\mathrm{opt}\cdot\ln|U|$ form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the $SC(k)$ bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.

Difficulty

The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes $n(K, i)$, and for an arbitrary covering subfamily $M0$. Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.

For the tightness half, the difficulty is bookkeeping: showing that the $k!/j$ blocks of each segment are admissible choices at each stage and that no cover uses fewer than $k!$ sets.

Formalization scope

• An input is an indexed family S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of $1, \dots, N$; two indices may carry the same set, which only widens the input class. The family, subcovers and $F^*$ are taken over the set of sets family S, as on the page. $F^*$ is a Finset.inf' over the nonempty finite set of subcovers; if $T = \emptyset$ then $F^* = 0$.
• C1 is a nondeterministic step relation: a step is allowed for every index maximizing $|\mathrm{SET}[j]|$. An output is choosable if a finite chain of steps from the initial state reaches a halting state with that SUB. No tie-breaking rule is fixed.
• The paper's $R[A, P](n)$ is a maximum over inputs of size at most $n$ in an unspecified notation; it is replaced by the size-free two-part statement above, which is equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$.
• Ratios are stated multiplicatively in $\mathbb{Q}$ ($|F_1| \le H(k)\cdot F^*$), never as a quotient, so an input with $F^* = 0$ does not make the bound vacuous, and the attainment part requires $F^* > 0$. $H(k)$ is Mathlib's harmonic k.
• Configurations carry the covering condition as a field; runs are an inductive predicate on the list of chosen indices; Selectable K M means $M$ is the set of indices of some run.
• Lemma 1 assumes the family's sets are pairwise distinct (the paper's family is a set of sets); without that the index set $\{i : S_i \in F_1\}$ may contain a duplicate index C1 never chose.
• Trivializing formalizations are ruled out: a deterministic tie-break, a ratio written as a division, the original set sizes in place of $n(K, i)$ in Lemma 2, or an attaining input with $F^* = 0$ would each change the theorem.

Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.

Selected references

• David S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• Richard M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• László Lovász, On the ratio of optimal integral and fractional covers, Discrete Mathematics 13 (1975), 383–390. https://doi.org/10.1016/0012-365X(75)90058-8
• Vašek Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233
• Uriel Feige, A threshold of ln n for approximating set cover, Journal of the ACM 45 (1998), 634–652. https://doi.org/10.1145/285055.285059

Motivation

Many problems in scientific computing and statistics ask for a solution of a linear system $Ax\approx b$ that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.

Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.

Setting

Let $A\in\mathbb R^{m\times n}$ have columns $a_1,\dots,a_n$, let $b\in\mathbb R^m$ and $\varepsilon>0$. Write $\|\cdot\|_2$ for the Euclidean norm and $\|x\|_0$ for the number of nonzero entries of $x$. The sparse approximate solution problem asks for $x$ with $\|Ax-b\|_2\le\varepsilon$ and $\|x\|_0$ minimal. Define

$$\operatorname{Opt}(\delta)=\min\{\|x\|_0 : \|Ax-b\|_2\le\delta\}.$$

Let $\mathbf A$ be $A$ with every column divided by its Euclidean norm. Let $\mathbf A^+$ be its Moore–Penrose pseudo-inverse, the unique matrix $P$ with $\mathbf AP\mathbf A=\mathbf A$, $P\mathbf AP=P$ and $\mathbf AP$, $P\mathbf A$ symmetric. Let $\|\mathbf A^+\|_2$ be its spectral norm, the $\ell_2\to\ell_2$ operator norm.

Algorithm Greedy keeps a working matrix $A^{(r)}$ with columns $a^{(r)}_j$, a working vector $b^{(r)}$ and a set $\tau$ of chosen indices. It starts from $A^{(0)}=\mathbf A$, $b^{(0)}=b$, $\tau=\emptyset$. While $\|b^{(r)}\|_2>\varepsilon$, it chooses an index $k\notin\tau$ that maximizes $|a_k^{(r)T}b^{(r)}|$ and replaces $b^{(r)}$ by its projection onto the orthogonal complement of $a^{(r)}_k$. It adds $k$ to $\tau$ and replaces every column outside $\tau$ by its normalized projection onto that complement. If every correlation $a_j^{(r)T}b^{(r)}$ vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system $Bx=b^{(0)}-b^{(r)}$ in the chosen columns $B$ of $A$. The number of nonzero entries of the output is therefore at most the number $t$ of selection iterations.

Formalization targets

Goal: Theorem 2, for $A$ with linearly independent columns

If the columns of $A$ are linearly independent and some $x$ satisfies $\|Ax-b\|_2\le\varepsilon/2$, then every run of the selection phase, with any tie-breaking, performs

$$t\le\Big\lceil 18\,\operatorname{Opt}(\varepsilon/2)\,\|\mathbf A^+\|_2^2\,\ln\frac{\|b\|_2}{\varepsilon}\Big\rceil$$

iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).

Milestones

The proof on pp. 230–233 passes through the following statements, in order:

1. (12): some column satisfies $|a_j^{(r)T}b^{(r)}|\ge\|b^{(r)}\|_2^2/(2\sqrt{N^{(r)}}\|u^{(r)}\|_2)$. Here $u^{(r)}$ is a sparsest vector with $\|A^{(r)}u^{(r)}-b^{(r)}\|_2\le\varepsilon/2$ and $N^{(r)}=\|u^{(r)}\|_0$.
2. (18): $\|b^{(r+1)}\|_2^2\le(1-1/\rho)\|b^{(r)}\|_2^2$ whenever $\rho\ge 4N^{(r)}\|u^{(r)}\|_2^2/\|b^{(r)}\|_2^2$.
3. Lemma 1: $t\le\lceil2\rho\ln(\|b\|_2/\varepsilon)\rceil$ for any such $\rho$ valid at every iteration.
4. Lemma 3: $N^{(r+1)}\le N^{(r)}\le N^{(0)}$.
5. $N^{(0)}=\operatorname{Opt}(\varepsilon/2)$.
6. The columns of $\mathbf A$ indexed by the support $\sigma$ of $u^{(r)}$ and by the chosen set $\tau$ are linearly independent, and $\sigma\cap\tau=\emptyset$.
7. (31): $\|u^{(r)}\|_2\le\frac32\|Z^+\|_2\|b^{(r)}\|_2$ for the matrix $Z$ of those columns.
8. The singular-value comparison $\|Z^+\|_2\le\|M^+\|_2$ for a column submatrix $Z$ of a matrix $M$ with independent columns.
9. Lemma 2: $\|u^{(r)}\|_2\le\frac32\|\mathbf A^+\|_2\|b^{(r)}\|_2$, for $A$ with independent columns.

Items 1–7 hold for every matrix $A$. Items 8, 9 and the goal carry the independence hypothesis.

Significance

Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error $\varepsilon$ with at most a factor $18\|\mathbf A^+\|_2^2\ln(\|b\|_2/\varepsilon)$ more nonzeros than the best solution at error $\varepsilon/2$. The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.

The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of $\mathbf A$, and this comparison holds only when $\mathbf A$ has full column rank. For general $A$, Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.

Difficulty

Each step of the proof is short, but the objects are defined by an iteration. The columns $a^{(r)}_j$ are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration $r$ therefore needs invariants: chosen columns are orthonormal and orthogonal to $b^{(r)}$, and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector $u^{(r)}$ is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.

A naive attempt to bound $\|u^{(r)}\|_2$ directly by $\|\mathbf A^+\|_2\|A^{(r)}u^{(r)}\|_2$ fails: $u^{(r)}$ multiplies the projected columns $A^{(r)}$, not $\mathbf A$, and different sparsest solutions can have different norms.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m), so every $\|\cdot\|_2$ is the Euclidean norm. The only $\|\cdot\|_\infty$ is the maximum of $|a_j^{(r)T}b^{(r)}|$, which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of $t$ iterations (IsGreedyRun) requires, at each $r<t$: the strict while-condition $\|b^{(r)}\|_2>\varepsilon$, an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends $0$ to $0$, so a column lying in the span of the chosen ones stays zero and is never chosen. $\operatorname{Opt}$ is an infimum over ℕ, and the goal assumes that some $x$ has $\|Ax-b\|_2\le\varepsilon/2$, since otherwise the infimum would be $0$. The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then $\|b\|_2>\varepsilon$. The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as $(\mathbf A^T\mathbf A)^{-1}\mathbf A^T$, which would hide the rank assumption.

Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of $A$ are linearly independent, which forces $n\le m$. Without it, Theorem 2 fails. Take $m=2$, $n=200$, columns $(\cos\theta_j,\sin\theta_j)$ and $(\sin\theta_j,\cos\theta_j)$ for 100 distinct $\theta_j\in[0.001,0.01]$, $b=\sqrt2(1,1)$ and $\varepsilon=1$. Then $\operatorname{Opt}(1/2)=2$ and the bound evaluates to $1$, but Greedy selects two columns. Lemma 2 fails for $\mathbf A=[e_1,e_2,(e_1+e_2)/\sqrt2]$ and $b=\beta(-1,1)/\sqrt2$. The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace $\|\mathbf A^+\|_2$ by the largest $\|Z^+\|_2$ over linearly independent column subsets $Z$ of $\mathbf A$, which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.

A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or $\operatorname{Opt}$ is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.

A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM J. Comput. 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• G. H. Golub and C. F. Van Loan, Matrix Computations, Johns Hopkins University Press, 1983.
• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9:256–278, 1974. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51:406–413, 1955. https://doi.org/10.1017/S0305004100030401