Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
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:
A set system is a finite set of elements together with a family of subsets of . Given a weight for each element , the weight of is , and has a unique minimum weight set if one member of is strictly lighter than every other member.
A graph has vertices (in Lean, Fin n, in their natural order) and edge set , with . A perfect matching is a set such that every vertex lies in exactly one edge of . The edges and the perfect matchings of form a set system.
Given edge weights , the integer matrix is obtained from the Tutte matrix by substituting for its indeterminates:
is its determinant, the submatrix with row and column removed, and its adjugate, whose entry is .
The algorithm of §4 is:
For every graph that has a perfect matching, with edge weights drawn uniformly and independently from ,
This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the weight functions.
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.
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.
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 , 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 , which is where "since 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: divides every term, and every term other than the one of is divisible by .
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 ; the weight range is exactly (resp. in Lemma 1). " is odd" means and is an odd integer. The minor is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's is .
Added hypotheses: Lemma 1 and its maximum version assume nonempty (the printed lemma omits it and is false for ); the goal and the isolation milestone assume 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 , , , 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², 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.
Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).
Let be the feature space with an arbitrary norm , and let be the dual norm of a weight vector . Labels are , and the feature-label space is . The logloss of at is
For a label weight , the metric of Definition 2 on is
so that changing a label costs . The Wasserstein distance between probability distributions on (Definition 1) is the infimum of over all couplings of and , and . Given training samples , the empirical distribution is , and the distributionally robust logistic regression problem (6) is
Program (7) has variables , , , objective , and constraints , for all , and .
For every , , and every norm on the feature space,
and for the infimum of (7) is attained.
Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in ; with the , or norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value a certificate on the out-of-sample logloss whenever the ball contains the true distribution.
The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the reduction, and the implication in Theorem 2).
The worst-case expectation ranges over every Borel probability distribution within transport distance of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.
V standing for with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as ; the label is Boolean negation. The metric of Definition 2 is written literally.Many polytopes that arise from combinatorial optimization problems have no small facet description in their natural variable space, yet become describable by a compact linear system once lifted to a higher-dimensional space of auxiliary variables and projected back down — Chapter 2's own extended formulation of the convex hull of a disjunctive set is one instance of this phenomenon. This chapter turns the idea around: rather than using projection to build a compact formulation, it uses projection to prove integrality of a formulation that is already compact but whose integrality is not obvious from any standard sufficient condition (total unimodularity, balancedness, etc.). The technique is illustrated on three closely related combinatorial polytopes built from perfectly matchable, assignable, and path-decomposable vertex subsets of a graph or digraph — each proved integral by lifting to an edge- or arc-variable space where total unimodularity is easy to check, then projecting.
For a finite vertex set , the incidence vector of is on , elsewhere, and . A graph has a perfect matching if there is a fixed-point-free involution on respecting adjacency. The PMS (Perfectly Matchable Subgraph) polytope of is where is the set of incidence vectors of such ; .
For a digraph : is assignable if it admits a cycle decomposition (a permutation of respecting arcs), giving the Assignable Subgraph Polytope. For an acyclic digraph with distinguished nodes : admits an - path decomposition if a collection of interior-node-disjoint - paths covers it, giving the - Path Decomposable Subgraph Polytope over . and are the corresponding out-neighborhood operators. For an arbitrary graph, counts the connected components of the induced subgraph .
for every all of whose components are single nodes or nonbipartite with odd order — the weakest faithful statement, since dropping the side condition would assert the inequality for subsets it does not hold for.
The results themselves. Each theorem gives an explicit, checkable linear system defining a polytope that arises naturally from a combinatorial covering/decomposition property, turning "does have property " into a linear-programming feasibility question. Theorem 5.1 is the one the book proves in full and the template for the other three: bipartite matching, digraph assignment, and acyclic-digraph path decomposition are structurally parallel problems (all reduce to checking a König–Hall-type combinatorial condition), and the same lift-and-project technique handles all three uniformly. Theorem 5.4 extends the idea to arbitrary (non-bipartite) graphs at the cost of a sharper right-hand side and a component-based side condition, connecting to Edmonds' classical matching-polytope theory while remaining a genuinely different object (a polytope of coverable vertex sets, not of matchings themselves).
Formalizing it. No object in this mission — the PMS, Assignable, or Path Decomposable Subgraph
polytopes, or their defining neighbor operators — exists on the platform prior to this mission.
The closest platform result, MetricTSP.pm_polytope_decomposition (Edmonds' perfect matching
polytope theorem, in edge-variable space over a fixed vertex set requiring every vertex
matched), is a genuinely different object from Theorem 5.4's PMS polytope (vertex-variable space,
vertices may be left unmatched by design) and is not reused as a kind: reference item; it is
noted here as related, not equivalent.
The natural first attempt tries to verify each polytope's integrality directly, by checking a known sufficient condition (total unimodularity, balancedness) on the displayed vertex-space system itself. This fails: the book states explicitly that (5.5)'s coefficient matrix is not totally unimodular, which is exactly why the lift-to-edge-variables step is necessary at all. The real content of each theorem is the two-part argument: (1) the lifted system in edge/arc variables is totally unimodular (checkable directly), so its polyhedron is integral; and (2) the vertex- space system is exactly the projection of the lifted one — a nontrivial fact requiring Chapter 2's projection machinery, not merely an unfolding of definitions. Theorem 5.4's extra difficulty, flagged explicitly in the text, is that its projection cone is not pointed, so the proof must work with a finite generating set rather than extreme rays, and it suffices to find a subset of generators producing every facet rather than a complete generating set — a genuinely harder argument the book itself outsources to a citation.
Undirected graphs use Mathlib's SimpleGraph; digraphs use a bare relation A : V → V → Prop
(not required symmetric or irreflexive, matching the book's unrestricted notion). Bipartition is
recorded via part : V → Bool (decidable by construction) rather than two Set V halves, keeping
the sums x(V_1), x(V_2) computable over Finsets throughout. IsAssignable uses Equiv.Perm
on the vertex-set subtype, since a cycle decomposition is exactly a permutation. IsComponentOf
and IsBipartiteOn (Theorem 5.4) are built directly from reachability and 2-colorability rather
than Mathlib's induced-subgraph/ConnectedComponent API, matching the "maximal connected subset"
reading of "component" the book's own prose intends.
IsPathDecomposable (Theorem 5.3) encodes "admits an - path decomposition" via a
degree-constrained arc set (every interior node has exactly one incoming and one outgoing chosen
arc, none entering or leaving , at least one leaving ) rather than an explicit list of
vertex-disjoint paths — provably equivalent by the standard fact that an acyclic arc set with this
degree pattern always decomposes into such a path family, and considerably lighter to state and
reason about than constructing Path objects directly.
A trivializing formalization is ruled out explicitly: every theorem keeps the fractional box
constraint rather than the integral (per BRIEF.md's own
warning, dropping the relaxation collapses the claim to a restatement of the combinatorial
definition), and Theorem 5.1 is stated only for bipartite graphs — never generalized to subsume
Theorem 5.4's genuinely different inequality system and side condition.
Classifiers trained by standard methods can be fooled by small, carefully chosen perturbations of their inputs. Adversarial training reduces this vulnerability on the training set, but on image benchmarks such as CIFAR10 the robust accuracy on held-out data remains far below the training accuracy. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) asked whether this gap is a failure of current algorithms or an intrinsic statistical phenomenon, and answered it in two simple data models: learning a classifier that is robust to -bounded perturbations can require provably more samples than learning a classifier with small standard error.
The paper's separation has two halves in its Gaussian model. The lower half (every learner needs many samples) is the subject of the companion mission Adversarially Robust Generalization Requires More Data 1. This mission formalizes the upper half: a concrete, simple estimator reaches small robust error once the number of samples is of order , so the lower bound is tight up to logarithmic factors.
Write and for the Euclidean inner product and norm on , and . Labels are .
The -Gaussian model (Definition 1) is the distribution of a pair obtained by drawing the label uniformly at random and then the point from the spherical Gaussian , where is the per-class mean and the standard deviation of each coordinate. The paper works in the regime , which every statement of this mission assumes explicitly.
A classifier is a map . Its classification error (Definition 2) under a distribution is . Given the perturbation set , its -robust classification error (Definition 3) is
The -robust error is defined the same way with the ball, and is the dual norm.
For the linear classifier is . The estimator studied here is built from i.i.d. samples of the model: the class-weighted sample mean
and the classifier is .
If and , then with probability at least over the sample, has -robust classification error at most provided
For every and every , with the same probability the -robust error of is at most .
The milestones follow the paper's Appendix A.1: Fact 12 (Gaussian norm tail); Lemmas 13 and 14 (norm of a Gaussian sample mean); Lemma 15 (inner product of the sample mean with the mean); Lemma 16 (alignment with high probability); Lemma 17 (Gaussian margin tail for a fixed unit vector); Lemma 20 (the -robust error of a fixed linear classifier, for every ); and Theorem 21. The mission also contains Theorem 18, the corresponding standard-generalization bound, as a companion item.
The result. Corollary 22 shows that the lower bound of the paper is essentially attained by an elementary estimator: in the regime a single sample gives small standard error, while -robustness at level is obtained with samples, matching the lower bound up to a logarithm. The separation between standard and robust sample complexity is therefore a property of the data distribution and not of a weak learning procedure. Lemma 20 is of independent use: it gives the exact form of the robust error of any linear classifier in a Gaussian model for every adversary.
Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. A formalization produces a checked instance of a statistical-versus-robust separation, and along the way checked versions of dimension-explicit Gaussian tail bounds (norm and inner-product tails of sample means) that Mathlib states only in partial form.
The estimator is explicit, so the difficulty is analytic and quantitative. Two obstacles stand out. First, the robust error involves a supremum over an uncountable perturbation set for every test point, so it is not a margin probability until the worst case over the ball has been identified exactly; any slack there changes the constants. Second, the estimator is random, and its alignment with depends on two concentration events at once, a norm upper bound and an inner-product lower bound, with dimension-explicit constants. Generic sub-Gaussian bounds with unspecified constants, the usual first attempt, do not yield the stated , and : the constants have to be tracked through the final numerical case analysis. Gaussian norm concentration in the dimension-free form of Fact 12 is not available in Mathlib.
Everything is stated in the namespace RobustGeneralization.GaussUpper. The data space is EuclideanSpace ℝ (Fin d); labels are Bool with true . is the push-forward of Mathlib's stdGaussian under , with the standard deviation (Definition 1 calls the "variance parameter" but samples from ). The model is a measure on and the errors are literally the measures of the events of Definitions 2–3; since the robust event need not be Borel, the measure of it is its outer measure, i.e. its probability under the completed measure. The ball is written coordinatewise. The linear classifier labels the tie as ; no statement depends on this. is , equal to on the null event . The samples are a product measure on Fin n → ℝ^d × Bool.
"With probability at least the error is at most " is stated as an upper bound on the probability of the failure set, which is the strong form under outer measures.
Added hypotheses, each disclosed in its item: (Fact 12), (Lemmas 13, 15 and Theorem 18), (Lemma 15, false as printed at ), and (Theorem 21). The constants , , , , and are kept exactly.
A formalization that states the robust error bound for a fixed unit vector instead of the estimator , that replaces the robust error by its closed-form margin expression, or that uses the ball instead of the ball, proves a different and weaker statement and is excluded.
A complete development needs: Gaussian concentration for Lipschitz functions (or a direct -type tail for ), the law of a sample mean of Gaussian vectors and of a one-dimensional projection of a spherical Gaussian, and the dual-norm identity for linear functionals over balls. These pieces are reusable beyond this mission. Proofs of any milestone, and reusable lemmas on spherical Gaussians under stdGaussian, are welcome. Related platform work: the other missions of this series, Adversarially Robust Generalization Requires More Data 1, 2 and 4.
Convexity is what makes optimization tractable: a linear program's feasible region is convex, and this single fact underwrites the simplex method, LP duality, and everything built on top of them. Integer and disjunctive programs have no such luck — their feasible regions are unions of polyhedra, and a union of convex sets is generally not convex. If the convex hull of such a union could always be described compactly, integer programming would reduce to linear programming: optimize the same linear objective over the hull instead of the union, and any optimal vertex of the hull is automatically integral. The obstacle has always been that the convex hull of a union of polyhedra in , described directly by its facets in , typically needs exponentially many inequalities.
Balas's Theorem 2.1, proved in the 1970s and presented here as Chapter 2 of Disjunctive Programming (Balas, Springer 2018), breaks this exponential barrier by changing where the description lives. Rather than writing down the hull's facets in , Theorem 2.1 lifts the problem to a higher-dimensional space — one auxiliary copy of per polyhedron in the union — where the hull becomes the projection of a single, explicitly given polyhedron whose size grows only linearly with the number of polyhedra. This "extended formulation" technique, born here, became one of the central tools of modern integer programming and combinatorial optimization: representing a hard polytope as the projection of an easy one in higher dimension underlies, for instance, the polynomial-size extended formulations known for many combinatorial polytopes.
Fix a finite index set . For , let be a real matrix and a vector of matching row dimension, and set . The union is the disjunctive set. Write for the feasible disjuncts.
The recession cone of a nonempty polyhedron is : the set of directions along which one can travel indefinitely from any point of while remaining in . For a subset and sets (), the (finite) Minkowski sum is . The maximal indices are the feasible disjuncts whose polyhedron is not contained in any other feasible disjunct's polyhedron.
Given a set , its projection onto is .
This is the weakest correct statement: it claims only that the closed convex hull equals the projection of this specific lifted polyhedron , not any stronger uniqueness or minimality claim about lifted representations in general (that refinement is Theorem 2.1's own follow-up discussion, not part of the theorem itself).
Extreme points of correspond bijectively to the extreme points of that place all of their mass on a single disjunct's coordinates.
where is the variant of indexed by all of rather than only .
Under two recession-cone conditions on , restricting 's variables to makes its -projection recover itself, not merely .
The result itself. Theorem 2.1 is the founding extended-formulation result of integer programming: it shows that every union of finitely many polyhedra — hence every mixed-integer program's feasible region, once expressed in disjunctive normal form — has a lifted description of size linear in the number of disjuncts, in stark contrast to the union's own facet description, which is generally exponential. Corollary 2.2 shows this lifting is not merely an upper bound with extraneous points: its extreme points correspond exactly, one-to-one, with the extreme points of the object it represents. Theorems 2.3 and 2.4 sharpen the picture: 2.3 tells you exactly when you can avoid knowing in advance which disjuncts are nonempty, and 2.4 tells you exactly when the same family of lifted systems, restricted to integral , describes the union exactly rather than only its convex hull — this is Jeroslow and Lowe's characterization of when a disjunctive set is representable as the feasible region of an integer program at all.
Formalizing it. No object in this mission — the disjunctive set , its lifted polyhedron
, recession cones of a union's components, or the extreme-point correspondence between a
polytope and its lift — exists on the platform prior to this mission or anywhere in Mathlib
(substrate.md records zero LP/polyhedron modules in Mathlib as of this writing). This mission is
a from-scratch formalization of the book's central construction, restating (rather than importing)
the disjunctive-set vocabulary introduced by the companion IntroDuality mission, per the series'
convention that a draft mission cannot import another draft mission's definitions.
The natural first attempt at Theorem 2.1 tries to prove the two inclusions and by a direct facet-by-facet or vertex-by-vertex argument in — exactly the exponential-size approach the theorem exists to avoid. The book's own first proof instead works entirely with convex combinations: an arbitrary point of is a combination of at most points, one from each polyhedron in the union (Carathéodory-style), which converts directly into a point of by splitting the combination's weight across the lifted coordinates — and conversely, a point of decomposes, disjunct by disjunct, into a convex combination of that disjunct's own vertices and extreme rays. Neither direction ever needs to enumerate facets of in . The second proof (via projection and the polar cone of the lifted system) shows the projected inequalities coincide with exactly the valid-inequality characterization of Theorem 1.2 (disjunctive Farkas), which is a different, complementary way of seeing why no facet of is missed.
All theorems are stated over a finite index set Q : Type* with [Fintype Q], matrices
Matrix (Fin (m h)) (Fin n) ℝ with m : Q → ℕ allowed to depend on h, and vectors in
Fin n → ℝ. DisjunctiveSet, FeasibleIndices, MaximalIndices, RecessionCone, and
MinkowskiSumOver fix the chapter's vocabulary; ProjX, LiftedPolyhedron, and
IntegerRestricted fix the lifted system and its variants. cl conv F is Mathlib's
closure (convexHull ℝ ·); extreme points use Mathlib's Set.extremePoints.
LiftedPolyhedron ranges its auxiliary vectors , over all of rather
than only the index subset Qidx the book restricts to, forcing the components outside Qidx to
zero. This is an equivalent, Finset/decidability-free encoding — appending zero terms changes
neither the defining sums nor the constraints — documented as a convention, not a weakening, in
MODERATION_NOTES.md; the same definition instantiates both the system (Qidx = Q^*) and
the variant (Qidx = Q) that Theorem 2.3 compares.
A trivializing formalization is ruled out explicitly: taking collapses the lifted
system to , , a vacuous restatement of that proves nothing about
unions. Every theorem here is stated for a generic finite Q, never specialized to a fixed small
size. Contributions beyond this mission's statements would need genuine polyhedral machinery
(vertex/extreme-ray decomposition of a polyhedron, Carathéodory's theorem for cones) that is itself
absent from Mathlib and would be welcome as a separate, reusable definitions layer.
Linear programming duality is one of the load-bearing facts of optimization: every feasible linear program has a dual whose value matches the primal's, and this correspondence drives the simplex method's stopping criterion, sensitivity analysis, and most complexity results for polyhedral problems. Integer and mixed-integer programs have no such duality theorem in general — the feasible region of a mixed-integer program is not convex, and the entire apparatus of linear programming duality is built on convexity.
Disjunctive programming, introduced by Egon Balas in the early 1970s, closes part of this gap. A disjunctive set is a union of finitely many polyhedra rather than a single polyhedron — the natural convex-analytic shadow of the "either/or" logical structure that integer variables encode (an integer variable's feasible region is a finite union of half-open pieces, hence a disjunction of the linear constraints that pin it to each value). Balas's insight was that disjunctive programs — linear programs whose feasible region is such a union — admit a strong duality theorem of their own, generalizing the linear-programming case rather than replacing it. This mission formalizes that theorem (Theorem 1.5 of Balas, Disjunctive Programming, Springer 2018) together with the two results the same chapter builds around it: the founding construction of the field, the intersection cut (Theorem 1.1, circa 1970), and the disjunctive generalization of Farkas' Lemma (Theorem 1.2), which characterizes every valid inequality — hence every cutting plane — for a disjunctive set.
Fix a finite index set . For each , let be a real matrix and , and set . The union is a disjunctive set: any (linear) system of inequalities combined with the logical connectives "and", "or", "not" reduces, via its disjunctive normal form, to a set of exactly this shape. Because a union of convex sets need not be convex, is generally nonconvex even though each is a polyhedron.
A disjunctive program minimizes a linear objective over such a union:
Its dual pairs a scalar with one dual multiplier vector per disjunct, requiring and , , simultaneously for every , and maximizes . Write for the disjuncts whose primal system is feasible, and (with ) for those whose dual system is feasible.
The theorems below also use two objects from the origin of the subject (§1.2): given a basic solution of a linear program's optimal simplex tableau, with basic index set and nonbasic index set , the tableau's coefficients (, ) determine, for each nonbasic , an extreme ray direction of the associated LP cone. A convex set is -free at if lies in the interior of and that interior contains no point of the mixed-integer feasible set .
The displayed inequality cuts off but excludes no point of , for any -free convex set containing in its interior.
Under the Regularity Condition — and — exactly one of:
This is the weakest faithful statement of the theorem: it asserts only the shape of the dichotomy established by Balas, not any strengthened or specialized form of it.
If the Regularity Condition fails, is feasible, and is infeasible, then still has a finite minimum — exhibiting the duality gap that opens up once the condition is dropped.
The results themselves. Theorem 1.5 is the mission-critical fact that makes disjunctive programming a genuine extension of linear programming rather than an unrelated combinatorial device: every LP-duality-based algorithmic tool (bounding, sensitivity, complementary-slackness optimality certificates) has a disjunctive-programming counterpart because of this theorem. Theorem 1.1's intersection cut is the historical seed of an entire branch of integer-programming algorithms — lift-and-project cuts, mixed-integer Gomory cuts, and the split closure (later missions of this series) all specialize or generalize it. Theorem 1.2 is the structural fact that makes cutting-plane generation for disjunctive sets tractable at all: every valid inequality decomposes into per-disjunct Farkas certificates.
Formalizing it. None of these results, nor the union-of-polyhedra machinery they are stated
over, exist on the platform prior to this mission: the platform's existing Farkas' Lemma and
linear-programming strong duality theorems (SmaleNinth.farkas_lemma,
SmaleNinth.lp_strong_duality) are the ordinary single-polyhedron statements, which is exactly the
special case of the theorems formalized here — genuinely different statements, not
restatements. This mission is a from-scratch formalization of the disjunctive generalization,
including the vocabulary (disjunctive sets, the paired primal/dual index sets , the
Regularity Condition) that the rest of the fifteen-mission Balas series builds on.
The obvious first attempt collapses the disjunctive dual to separate ordinary LP duals, one per disjunct, and tries to combine their individual strong-duality statements. This fails: couples all disjuncts through the single shared scalar , which must simultaneously satisfy for every at once, not disjunct-by-disjunct. The Regularity Condition exists precisely because this coupling can break down — Balas's own example (a two-term disjunctive program with an infeasible dual but a feasible, bounded primal) shows that without the condition, situation (2) of the dichotomy can fail: the primal can have a finite optimum with no matching dual optimum. Any formalization that omits the Regularity Condition, or weakens it to an informal restriction like "nondegenerate", either proves a false statement or proves nothing (a vacuous hypothesis), which Corollary 1.6 exists specifically to rule out.
All three theorems are stated over a finite index set Q : Type* with [Fintype Q], real
matrices Matrix (Fin (m h)) (Fin n) ℝ with row-dimension m : Q → ℕ allowed to depend on h
(the book never assumes a common row count across disjuncts), and vectors in Fin n → ℝ. Poly,
PolyNonneg, and DualPoly are the plain, nonnegative-orthant, and dual polyhedral systems
respectively; FeasibleIndices and RegularityCondition pin / and the Regularity
Condition exactly as stated on p. 13. "No finite optimum" is formalized via UnboundedBelowOn /
UnboundedAboveOn: nonempty (feasible) together with no finite bound on the objective, matching
Balas's case (2), which explicitly distinguishes infeasibility from unboundedness.
A trivializing formalization is ruled out explicitly: fixing collapses Theorem 1.5 to
ordinary LP duality (already on the platform) and Theorem 1.2 to ordinary Farkas' Lemma, so both
theorems are stated for a generic finite Q, never specialized. Theorem 1.5's "exactly one of"
dichotomy is formalized as a logical Xor of the two situations, not a weaker Or, since the book
asserts mutual exclusivity, not merely that one holds.
The intersection-cut theorem (1.1) is formalized over a generic finite index type ι standing for
the full set of structural and surplus variables, with I J : Finset ι the basic/nonbasic
partition; a complete development would additionally need the simplex-tableau apparatus connecting
ι, I, J, and abar to an actual linear program, which lies outside this mission and belongs
instead to the tableau-focused later missions of the series (SimplexTableau, RayCGLP). The
extremeRay and PIFree definitions introduced here are local to this mission and are restated,
not imported, by later missions that need related vocabulary — per the series' convention that a
draft mission cannot import another draft mission's definitions.
The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator , is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.
For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of already implies four of the classical families of facets of the stable set polytope.
Timeline:
Vectors live in with coordinates . The polar cone of is . Let be the cone spanned by the 0–1 vectors with . For a convex cone , the matrix cone consists of the symmetric positive semidefinite matrices with for and for all , . The operator is
and , .
Let be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). is the convex hull of incidence vectors of stable sets . is the polytope given by and for . is the cone , . The relaxations are
so . The -index of an inequality valid for is the least with valid for .
The four constraint families are:
The contraction of a node turns into the inequality with the coefficients of and its neighbours removed and right-hand side .
For every graph without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has -index exactly 1:
Corollary 2.19 (first sentence): the -index of a -valid inequality is at most the independence number of the subgraph induced by the nodes with positive coefficient.
Corollary 2.15 shows that a single round of , a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently for every -perfect graph, in particular for perfect and -perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding -ranks.
The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver operator, its iterates, and the stable set relaxations , , in Lean.
The lower bound (each constraint fails on ) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix alone, cannot succeed: those conditions define the linear operator , and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in , including closedness of the iterates , which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.
Option ι, with none the special coordinate . For graphs, ι := V.IsLeast, never with an infimum that would default to 0 on an empty set.A formalization asserting only validity on , or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.
Not formalized: the linear operator and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.
Reusable infrastructure includes the polar cone, the matrix cone and the operator (usable for any 0–1 program), the polytopes and , and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of for bipartite graphs, or the -cone reformulations (iii′)–(iii″) are welcome.
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 elements its output is never more than the harmonic number times the optimum, and that this factor is attained.
Timeline.
An input of SET COVERING I is a finite family of finite sets. The set to be covered is . A subcover is a subfamily with , and its measure is . The optimum is the minimum measure of a subcover; itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than elements.
Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET holding the still-uncovered part of . It starts with SUB , UNCOV , SET. While UNCOV is nonempty it chooses an index with maximal, adds to SUB, and removes SET from UNCOV and from every SET. 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 is the worst choosable output, here the largest, and the ratio is .
For the proof the paper introduces configurations with , runs from a configuration (sequences of admissible choices ending when UNCOV is empty), , the set of indices chosen in a run , and calls a set selectable from if for some run from . Write .
For every :
The paper states this as for all , with equality for all sufficiently large . The two-part form above is the size-free equivalent.
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 cannot be lowered for any . Since , it also gives the well-known bound for general inputs. The 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 form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the 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.
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 , and for an arbitrary covering subfamily . 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 blocks of each segment are admissible choices at each stage and that no cover uses fewer than sets.
S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of ; two indices may carry the same set, which only widens the input class. The family, subcovers and are taken over the set of sets family S, as on the page. is a Finset.inf' over the nonempty finite set of subcovers; if then .harmonic k.Selectable K M means is the set of indices of some run.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.
Many problems in scientific computing and statistics ask for a solution of a linear system 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.
Let have columns , let and . Write for the Euclidean norm and for the number of nonzero entries of . The sparse approximate solution problem asks for with and minimal. Define
Let be with every column divided by its Euclidean norm. Let be its Moore–Penrose pseudo-inverse, the unique matrix with , and , symmetric. Let be its spectral norm, the operator norm.
Algorithm Greedy keeps a working matrix with columns , a working vector and a set of chosen indices. It starts from , , . While , it chooses an index that maximizes and replaces by its projection onto the orthogonal complement of . It adds to and replaces every column outside by its normalized projection onto that complement. If every correlation vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system in the chosen columns of . The number of nonzero entries of the output is therefore at most the number of selection iterations.
If the columns of are linearly independent and some satisfies , then every run of the selection phase, with any tie-breaking, performs
iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).
The proof on pp. 230–233 passes through the following statements, in order:
Items 1–7 hold for every matrix . Items 8, 9 and the goal carry the independence hypothesis.
Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error with at most a factor more nonzeros than the best solution at error . 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 , and this comparison holds only when has full column rank. For general , 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.
Each step of the proof is short, but the objects are defined by an iteration. The columns are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration therefore needs invariants: chosen columns are orthonormal and orthogonal to , 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 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 directly by fails: multiplies the projected columns , not , and different sparsest solutions can have different norms.
Vectors live in EuclideanSpace ℝ (Fin m), so every is the Euclidean norm. The only is the maximum of , 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 iterations (IsGreedyRun) requires, at each : the strict while-condition , an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends to , so a column lying in the span of the chosen ones stays zero and is never chosen. is an infimum over ℕ, and the goal assumes that some has , since otherwise the infimum would be . The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then . The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as , which would hide the rank assumption.
Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of are linearly independent, which forces . Without it, Theorem 2 fails. Take , , columns and for 100 distinct , and . Then and the bound evaluates to , but Greedy selects two columns. Lemma 2 fails for and . The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace by the largest over linearly independent column subsets of , 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 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.
Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction , in which every clause has at least literals, is polynomial complete for every , so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.
Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).
Timeline, for orientation:
Let be the set of literals; the complement of is and conversely. A clause is a finite set . A truth assignment is a set containing no complementary pair ; it may leave variables unassigned. satisfies if .
An input is a finite set of clauses. Its feasible solutions are the subsets satisfied by a single truth assignment, measured by , and the optimum is
The subproblem admits only inputs whose clauses each contain at least distinct literals.
Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB TRUE , LEFT , LIT . While some literal of LIT occurs in a clause of LEFT, it picks a literal LIT contained in the most clauses of LEFT, moves those clauses from LEFT to SUB, adds to TRUE, and removes and from LIT. When no literal of LIT occurs in LEFT it returns SUB.
The choice of is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on is the smallest over choosable outputs . The worst-case ratio on inputs of size at most is
For all ,
with equality for all sufficiently large . In the size-free form used here: every choosable output on every satisfies , and for every some has a choosable with and .
The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio . The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.
The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every . The paper spells out only and states that "similar examples can be constructed for any other "; the formal goal requires them for all .
The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both and are allowed and have to be handled.
The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at the paper's pattern degenerates and needs adjusting.
Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.Set of literals without a complementary pair (partial, as in the paper). is the maximum of over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition ; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general . The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.
David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.
Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity so as to fill it as much as possible. For this problem the paper gives a family of algorithms , one for each , whose guaranteed ratio tends to . It is one of the first examples of what is now called a polynomial-time approximation scheme: for every there is a polynomial-time algorithm within a factor of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.
This mission formalizes Theorem 1 of the paper, the performance guarantee of together with its tightness.
An input of SUBSET-SUM is a finite set , a positive rational size for every , and a positive rational bound . An approximate solution is a subset with , where the measure is . The problem is a maximization problem with optimal measure
Fix and call big if and small otherwise. Algorithm keeps a set , its measure , and the remaining elements :
Steps 1 and 3 may have ties. Following the paper, a set is choosable by if some resolution of all ties produces it, and the performance on input is the smallest measure of a choosable output. The ratio is , and is its maximum over inputs of size at most .
For and ,
Formally, for every : every choosable output of every input satisfies ; and for every some input has a choosable output with and .
Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above , in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of itself cannot be sharpened.
The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly . The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.
The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as always equalling or which elements can enter after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general : exactly unit elements are added after , and this must be shown for every choosable run, not only for one.
ℚ), as in the paper; sizes are required to be positive on and . The index is a natural number with as a hypothesis; is rational division, and "big" is the strict inequality .opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains ; it is when no element fits.Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning . Every "closest to, without exceeding" is an existential choice among all maximizers.def on Fin (k + 2) exactly as on the page, with (the page leaves the range implicit; keeps the only big element that fits when ).Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ( for step 1) and Sahni's knapsack extension are not part of the mission.
A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem , and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.
J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.
Timeline:
A finite set of jobs is given. Job has a processing time and a due-date , and the paper assumes for every job (a job that cannot finish on time even if started at time is removed beforehand). The machine starts at time and processes the jobs one after another, without idle time or preemption.
A schedule of is an ordering of all jobs of . The job in position completes at . The late set is and the early set is . A schedule is optimal if no schedule of has fewer late jobs. and denote the early and late jobs of , each kept in their order in .
Moore's algorithm works on a current sequence and a list of rejected jobs.
The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.
In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, and are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.
Let be a shortest-processing-time schedule of , and let a run of MooreStep from reach a state in which has no late job. Then for every due-date ordering of and every ordering of ,
All tie-breaks in both sorts are covered.
In attack order:
A companion item states the p. 104 remark that the final current sequence need not be re-sorted: is already optimal.
The theorem shows that the minimum number of late jobs on one machine can be found in time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.
The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.
Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job , the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as .
ι with decidable equality; is a Finset ι; .List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.MooreStep. The re-ordered prefix is any due-date sorted permutation of the first jobs, and case 2) rejects the first late job itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.The goal must concern runs of this step relation from a shortest-processing-time schedule of . Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.
Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.
A processor, a machine shop or a single server must work through a set of jobs one at a time, and each job is costly when it is late. Deciding the order is the single-machine sequencing problem, the simplest and most studied model of scheduling theory. Robert McNaughton's 1959 article Scheduling with Deadlines and Loss Functions (Management Science 6(1):1–12) treats it for a computer that must run several tasks, each with a deadline and a loss that grows linearly with the lateness. Its §2 gives the first sufficient condition under which a simple ratio rule is optimal in the presence of deadlines, and shows that interrupting and resuming tasks ("splitting", now called preemption) never helps on one processor.
Timeline.
There are tasks for a single processor, and the present is time . Task takes units of processing time, has a deadline and a penalty rate . If is finished at time there is no loss; otherwise the loss on is , where is the time from the deadline to the completion. Thus the loss on a task completed at time is
The ratio of task is .
A task may be split: part of it may run between times 4 and 6 and the remainder between times 8 and 11, and similarly in any finite number of parts. A schedule is therefore a finite list of pieces, each a task together with a start and a stop time. It is feasible when every piece lies in with start stop, no two pieces overlap in time, and the pieces of each task have total length exactly . The completion time is the latest stop time of a piece of , and the total loss is
For an order of the tasks ( in position ), the sequenced schedule runs the tasks without splits and without unused time: occupies . The order is in decreasing when implies . Finally denotes the total loss of computed as if .
If is in decreasing and no task finishes before its deadline in , i.e. for every , then is feasible and
The competitors may split tasks and leave the processor idle. The condition is sufficient but not necessary.
The result. Theorem 2.3 is the ratio rule for total weighted completion time, in its strongest single-machine form: it holds against preemptive schedules and schedules with idle time, not only against permutations. Theorem 2.4 carries the rule over to deadlines and linear tardiness penalties under a checkable condition on one schedule. Since weighted tardiness is strongly NP-hard in general, a condition of this kind is what one can hope for, and the paper's two-step heuristic for general deadlines (p. 6) is built on it. Theorem 2.2, as the paper remarks (p. 6), "does not depend on the linear loss function": it makes non-preemptive scheduling without loss of generality for single-machine objectives of this kind.
Formalizing it. All results of §2 are proved in the paper and are textbook material; none has a machine-checked proof on the platform. The platform's Scheduling Algorithms V mission formalizes the multi-processor results of §§3–4 (via Brucker's textbook), and nothing there states a single-processor ratio rule with deadlines. This mission supplies a single-processor schedule model with splitting, the interchange lemma, the non-preemption theorem and the ratio rule, each over all feasible schedules.
The interchange argument of Theorem 2.1 compares only two schedules that differ in the order of two adjacent tasks. Turning it into optimality against every feasible schedule requires two further steps, and each fails if done naively. First, a competitor may split tasks and leave gaps; the interchange argument does not apply to such schedules, so a separate argument must remove splits without raising any completion time. Second, with deadlines the loss is not linear in the completion time, so the ratio order is in general not optimal; the obvious attempt to repeat the interchange argument fails as soon as a task can finish before its deadline, since moving such a task later costs nothing. This is why Theorem 2.4 needs its hypothesis that no task finishes early, and why the paper leaves the general case to a heuristic.
Tasks and positions are the zero-based indices of Fin m; times, lengths, deadlines and penalties are real numbers. A schedule is a List of pieces (task, start, stop), mirroring the public definition SchedulingAlgorithms_ParallelMachines with one processor. Feasibility requires start stop, pairwise disjoint pieces, and exact total length per task; zero-length pieces and unsorted lists are allowed. The completion time is the maximum stop time of the task's pieces ( for a task with no pieces, which feasibility excludes). "No split" means exactly one piece per task, so two abutting pieces count as a split. "Decreasing " is non-increasing, with ties in any order. "Minimal" and "optimal" are stated as against every feasible schedule, never as an infimum.
Standing assumptions, stated in every item: (tasks take time, and needs ), and for Theorems 2.2–2.4 and the proof steps (penalties are non-negative; with a negative penalty and idle time allowed the loss is unbounded below). Theorem 2.1 carries no sign condition. No condition is placed on the deadlines.
A formalization that restricts the competitors of Theorems 2.2–2.4 to unsplit schedules, or to sequenced schedules of other orders, states a weaker theorem and is ruled out: every statement quantifies over all feasible schedules.
A complete development needs: sums over sublists of pieces, rearrangements of pieces of a schedule and their effect on completion times, and optimality over permutations of a finite set of tasks. The schedule model and the non-preemption argument are reusable for any single-machine regular objective. Contributions of intermediate lemmas on these points are welcome.
The nearest common ancestor problem asks, for a rooted tree and two of its vertices and , for the deepest vertex that is an ancestor of both, written . It is a subroutine in string and graph algorithms.
Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree whose sizes double along every edge, and is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about and Lemma 9.
Timeline.
A rooted tree (Appendix, p. 354) consists of a finite vertex set with , a root and a parent map , defined for , such that every vertex reaches by iterating . The edges of are the pairs for . If for some , then is a descendant of and an ancestor of . Every vertex is its own ancestor and descendant. The depth of is the number of edges from to . is the number of descendants of , including .
An edge is light if and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and denotes the apex of the heavy path containing .
The compressed tree has the same vertices and root as , and its edges are
Write , and let be the number of descendants of in . The rank of is , where . Let denote the -fold iterate of . Ply three is the set of vertices of rank at least . Ply two is the set of vertices whose rank lies between and , inclusive. Ply one is the set of vertices of rank below .
For every rooted tree on vertices:
and for every vertex in ply one, every -descendant of lies in ply one and .
The paper states the first two bounds as and . The constants and are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of containing at most vertices", read vertex by vertex. Ply one is closed under -descendants, so the component of a ply-one vertex is the -subtree of its shallowest ply-one ancestor.
A further item states Lemma 7 (p. 344): has depth at most . The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.
Lemma 9 is the counting step of the linear-time preprocessing. Ply three has vertices, each with ancestors in by Lemma 7, so storing every vertex's ply-three ancestors takes space. Ply two has vertices, each with ply-two ancestors, which again gives . Ply one splits into subtrees of at most vertices, and these are small enough to be embedded in complete binary trees and answered by the bit arithmetic of §3.
Lemmas 5–8 and the proof of Lemma 9 are proved or cited in the paper, and none of them is open. As far as a search of the platform shows, none has a machine-checked proof, and Mathlib has no parent-map rooted trees, subtree sizes or heavy-path decompositions. The mission produces a reusable formal account of heavy paths and of the size-doubling compressed tree, with the paper's explicit constants.
The paper states Lemmas 5–7 without proof, citing Tarjan (1979). Lemma 5 requires identifying the -descendants of an apex with its -descendants. That identification needs a clean description of heavy paths: at most one heavy edge enters each vertex, a vertex's heavy path runs up to its apex, and the heavy paths do not overlap. Lemma 8 needs the observation that two vertices of equal rank are unrelated in , so that their descendant sets are disjoint and the sizes add up to at most . Lemma 9 turns floors of iterated real logarithms into bounds on powers of two. The step loses a factor , and this is where the constant comes from; a proof that expects the constant fails at this step.
Fintype vertex type with a root, a total parent map and the axiom that every vertex reaches the root. The paper's partial map is made total by . Every statement about an edge assumes , since for Lemma 6 would read . The Appendix's printed "" is read as .Nat.log 2 of , which is exactly . The ply thresholds are iterated Nat.log 2, which equal the real floors and for . The bounds of the goal use Real.logb 2.Nat.log thresholds agree with the real ones. It is reusable for heavy-light decompositions generally.A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality . In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.
When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.
Fix natural numbers . The decision variable is . The nominal data are affine maps
with every symmetric, and fixed matrices , . A perturbation is a matrix , and the perturbed constraint matrix is the linear-fractional representation (LFR)
which is defined when . The perturbation ranges over a linear subspace , which encodes the structure, and is bounded by a level in the spectral norm (the largest singular value). The robust feasible set is
and the robust SDP (RSDP) is to minimize over .
The scaling set of is the linear subspace
For every : if some has , and
then , and in fact for every with . A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.
then every integer vector closest to in the maximum norm satisfies .
The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable . Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size in each coordinate of turns an SDP-feasible point into an integer solution by rounding.
Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).
The inequality to be proved is a statement about infinitely many perturbations, and depends on through a matrix inverse. The natural first step, eliminating by an exact S-procedure as in the full case, is not available: with a structured the set of pairs of vectors linked by some is not described by one quadratic inequality, and losslessness fails. The scalings in give several valid quadratic inequalities instead, and one must show that their combination controls every in the norm ball, including the well-posedness claim , which is part of the conclusion rather than an assumption. The commutation condition must be turned into an inequality for , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between and the stated matrix must be matched to the general lemma.
Matrices are Matrix (Fin a) (Fin b) ℝ; and are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is at a singular matrix, so every statement pairs the LFR with . The standing assumption of Section 3 is a hypothesis.
Readings and corrections of the printed statements:
Trivializing formalizations are ruled out: always, so the hypotheses and are kept outside ; is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.
A complete development needs the square root of a positive definite matrix and its commutation with and , the spectral-norm characterization , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.
Many firms learn about demand before it has to be served: customers place orders days or weeks ahead of the date they want delivery. Gallego and Özer (Management Science 47(10), 2001) model this advance demand information in a periodic-review inventory system and ask how the optimal replenishment policy should use it. Classical inventory theory (Arrow, Harris and Marschak 1951; Scarf 1959; Veinott 1965, 1966; Iglehart 1963) assumes that nothing about future demand is known when an order is placed. With advance orders the state of the system is no longer a single number, and it is not a priori clear whether the familiar policy structures survive.
This mission covers the paper's zero set-up cost case (Section 5). The companion mission Integrating Replenishment Decisions with Advance Demand Information I covers the positive set-up cost case and its policies.
Time is divided into periods . The supply lead time is an integer , and the information horizon is . In period customers place orders , where is demand placed in period for delivery in period . Throughout, ; write .
At the start of period the decision maker knows two things. The first is the modified inventory position : on-hand stock plus outstanding orders minus backorders, net of the demand already observed for the protection period . The second is the vector
of demands already observed for periods beyond the protection period. The decision maker raises the position to at zero fixed cost, the demand vector is realised, and the state moves to
with .
Costs enter through a single-period cost (holding, backorder and linear ordering cost, charged against the demand over the protection period) and one-period discount factors . The optimal cost-to-go and the cost of ordering up to satisfy
where the expectation is over . The base-stock level in period is the smallest minimizer
and the myopic level is the smallest minimizer of the single-period cost,
A function has decreasing differences if whenever and componentwise.
If is nondecreasing on , then for every period and every observed-demand vector ,
The optimal order-up-to level then ignores all advance information beyond the protection period. A second item states the paper's stationary special case: if for all , the smallest minimizer of is the optimal base-stock level in every period.
For every period and every fixed :
Parts 1–3 are what the goal's proof uses. Parts 4–6 are the paper's second zero set-up result, monotonicity of the base-stock level in observed demand.
The theorem identifies when advance demand information beyond the protection period can be ignored. When the myopic levels do not decrease over time, which includes stationary costs and ramping-up demand, the -dimensional dynamic program collapses to a sequence of one-dimensional newsvendor-type problems. That is both a computational simplification and a managerial statement: information about demand after the protection period does not change the order. Theorem 4, Part 5 gives the complementary monotone comparative statics. When the myopic condition fails, more observed demand never lowers the order-up-to level.
The results are proved in the paper, with the proofs in Appendix B. No machine-checked version exists. This mission produces a formal account of the finite-horizon recursion with a multi-dimensional information state, and checks the base-stock and myopic-optimality arguments against it.
The obvious induction carries convexity of backward, but here the future cost is evaluated at a random next state whose first coordinate depends on the current observed demand . Showing that the base-stock level does not depend on therefore needs more than convexity. It needs to know where is flat, uniformly in the random , and that the next position cannot exceed the current order-up-to level. The latter holds only on the reachable states, where observed demands are nonnegative. For a sufficiently negative the next period starts above its myopic level whatever is ordered now, and the conclusion fails. On the analytic side, every infimum and expectation in the recursion must be shown to be finite and attained before the order-theoretic argument can start.
The model is parametrised by and , with . The demand vector is a function on and a function on , ordered componentwise. is defined by backward recursion with for . The minimum over is a real infimum and the expectation a Bochner integral against the law of . Attainment and finiteness are consequences proved in the theorems, not assumptions. Base-stock and myopic levels are characterised as smallest minimizers (IsLeast), never through sInf.
The single-period cost is a primitive rather than being assembled from , and the lead-time demand; the paper's has the assumed properties, so the theorems cover the paper's model. Hypotheses the paper uses without stating, all placed on primitives and labelled in the statements:
The goal cannot be trivialised: the hypotheses are satisfied by concrete instances (for example with any finite-mean nonnegative demand), and the conclusion identifies the base-stock level exactly rather than asserting that some minimizer exists.
Out of scope: the reduction of the control problem to the functional equation (Appendix A, Özer 2000), the infinite-horizon Theorem 6, and Lemma 5, whose proof argues on the integers and whose real-valued form with a unit forward difference is unverified. Contributions of general lemmas are welcome: convexity and attainment for of a convex coercive function, and preservation of convexity and decreasing differences under expectation. All of them are reusable in other inventory models.
Subgradient optimization maximizes a concave function that is not differentiable by stepping along an arbitrary subgradient with a prescribed sequence of step sizes. It became a standard tool of integer programming after Held and Karp used it to compute the Lagrangian 1-tree bound for the traveling-salesman problem (Held & Karp 1971). Held, Wolfe and Crowder then tested it on the assignment problem, a traveling-salesman relaxation and a multicommodity flow problem (Held, Wolfe & Crowder 1974).
The method has one practical defect that the paper names at the start of its Section 6: it contains no test of optimality. The value approaches the maximum, but at no finite step does the method say that the maximum has been reached, or what the maximum is. Section 6 of the paper supplies such a test for the case where is a minimum of finitely many affine functions. The finitely many subgradients produced by the iterates define a small linear program, the core problem, and from some iteration on this linear program already solves the full dual linear program. Its optimal value is therefore the exact maximum of , obtained from quantities the method computes anyway. This is how the authors certified the optimal values reported in their experiments.
Timeline:
Fix and write with the Euclidean inner product . The data are scalars and vectors , and
The function is assumed bounded above, the paper's standing assumption. An index attains the minimum at if .
A run of the subgradient algorithm consists of a starting point , step sizes and indices such that attains the minimum at , and
No rule for choosing among several minimizing indices is imposed. Write and . The step-size conditions are
The dual linear program of is
For integers the core problem has one variable for each iteration :
An index chosen at several iterations contributes several identical columns. A point of is sent to the point of (6.1). This aggregation preserves feasibility and objective value.
Assume is bounded above, is a run satisfying (2.7), and is bounded. Then
The goal states existence of , which is what the paper claims. The paper's argument in fact gives the conclusion for every sufficiently large . That stronger form is not the goal. Feasibility of (Lemma 6.2) or the inequality , which holds for every feasible , is not a formalization of the goal. The content is optimality in (6.1).
Theorem 6.3 turns an asymptotic method into one that returns an exact answer. Solving for growing produces a linear program of bounded size whose optimum is eventually the optimum of (6.1), and hence . In the Lagrangian applications, where (6.1) is the linear relaxation of a combinatorial problem, this yields both the bound and a primal solution of the relaxation. The theorem is the ancestor of the primal-recovery results listed in the timeline.
The mission produces a machine-checked version of the paper's Section 6, together with the input the paper takes on citation: Poljak's convergence theorem for divergent-series step sizes, specialized to piecewise-linear concave functions. Neither Poljak's theorem nor Theorem 6.3 is in Mathlib. The pieces are reusable: the convergence theorem applies to every Lagrangian dual solved by subgradient steps, and the duality between and (6.1) is linear-programming duality for a minimum of affine functions.
The inequality is immediate, since aggregation maps feasible points to feasible points with the same objective. All of the content lies in the reverse inequality. That inequality ties a finite linear program to the limit of an infinite sequence, and it must hold for an arbitrary choice among tied minimizing indices. The iterates themselves need not converge, and under (2.7) the values are not monotone. So an argument that inspects a single iterate, or assumes that the method settles on one face of , fails. The convergence statement of milestone 2 is not proved in the paper and is the heaviest single step. Feasibility of also needs its own argument, and it fails without the boundedness hypothesis.
is EuclideanSpace ℝ (Fin n), the index set is a finite nonempty type ι, and is the finite minimum Finset.univ.inf'. A run is the predicate IsSubgradientRun c v t π k: positive steps, a minimizing index at every step, and update (2.6). It is not a function of , so every tie-breaking rule is covered. (2.7) is StepSizeCond t: t → 0, and the partial sums tend to . Iterates are indexed from . Boundedness is Bornology.IsBounded (Set.range π). The variables of are a function on of which only the values at enter. Optimality of in either linear program means feasibility plus an objective no larger than that of every feasible point. Suprema are never taken over unbounded sets: every maximum of is stated as attained at an explicit .
A statement that only asserts feasibility of , or only , is not the theorem. The goal requires that the solutions of be optimal for (6.1).
Theorem 6.1 is printed for the step rule (2.8), but its proof uses , the consequence of (2.7). The mission states it for (2.7), and its milestone title says so.
A complete development needs:
The first three are reusable well beyond this mission. Contributions of any of them, as standalone theorems, are welcome.
Least squares fits a linear model by minimizing , and its solution can be extremely sensitive to errors in the data when is ill-conditioned. The standard remedy is Tikhonov regularization (ridge regression): minimize , whose solution is stable but depends on a parameter that must be chosen by some external rule.
El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed instead to take the uncertainty in seriously: the robust least-squares (RLS) solution minimizes the worst-case residual over all perturbations of Frobenius norm at most . Their Theorem 3.1 shows that for this worst-case residual equals and that its minimization is the second-order cone program (15). Theorem 3.2, the subject of this mission, reads off the optimal solution: it is a Tikhonov-regularized solution, and the regularization parameter is not a free choice but is fixed by the data. This gives a principled answer to the question of how to choose , and it is the reason the paper describes RLS as "a Tikhonov regularization procedure" with "a rigorous way to compute the regularization parameter" (abstract, p. 1035).
A closely related model for least squares with bounded data uncertainty was developed at the same time by Chandrasekaran, Golub, Gu and Sayed; the paper notes that their preliminary draft (its reference [5]) gives a solution to the unstructured RLS problem similar to that of §3.2 (pp. 1036–1037).
Throughout, , , , and every vector norm is Euclidean, . For , is with a coordinate appended, so .
The SOCP (15) is the problem, in the variables and ,
A triple is optimal for (15) if it is feasible and for every feasible . Its dual, derived in the paper from the general second-order cone duality of §2.1, is the problem in , ,
The minimum-norm solution of is a solution with for every other solution ; when is consistent it is , with the Moore–Penrose pseudoinverse.
In the Lean development these objects are IsSOCPFeasible, IsSOCPOptimal, IsDualFeasible, dualObjective, IsDualOptimal and IsMinNormSolution, in the namespace RobustLS.Tikhonov, with the Euclidean norm eucNorm.
Let be optimal for (15) and set . Then
By Theorem 3.1 (the subject of the companion mission I of this series), the -part of an optimal point of (15) is the RLS solution for , so this is formula (17) of the paper. The identity for is the final display of the paper's proof and is the claim in the mission's title.
A further item states Remark 3.1: for , is the unique minimizer of the weighted residual with and .
The result. Theorem 3.2 turns a robust optimization problem into a familiar linear-algebra object. It says that the robust solution always lies on the Tikhonov path or at its endpoint , and it identifies the point on the path through a fixed-point equation relating to the residual and the size of the solution. The paper builds on this in §3.3 (a one-dimensional search for via the SVD) and in §6 (continuity of the RLS solution in the data), and Remark 3.1 is the template for the weighted least-squares interpretation of the structured and linear-fractional problems in §5.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal account of second-order cone duality for a concrete program, the characterization of the optimal dual point by equality in the Cauchy–Schwarz inequality, and the minimum-norm characterization of , all in terms of explicit Euclidean norms on Fin k → ℝ.
The paper's proof rests on strong duality for (15) ("both primal and dual problems are strictly feasible"), which it cites from the SOCP literature rather than proving; Mathlib has no second-order cone duality, so this step is the main gap. The degenerate case also needs care: there , the residual term is not differentiable at the optimum, and the conclusion changes from a regularized inverse to a pseudoinverse. A statement that only handles the case , or that assumes the matrix invertible without deriving it from , misses part of the theorem.
Fin k → ℝ; the Euclidean norm is the explicit eucNorm v = √(∑ vᵢ²) (Mathlib's ‖·‖ on Fin k → ℝ is the sup norm). Stacked vectors and are indexed by Fin m ⊕ Unit.Matrix.inv; it is used only where , where the matrix is positive definite. at every feasible point, so is well defined without an extra hypothesis.Contributions welcome: second-order cone (or general conic) weak and strong duality for finite-dimensional programs, the equality case of Cauchy–Schwarz in the explicit-norm form used here, and a Moore–Penrose pseudoinverse for real matrices with its minimum-norm property. The platform's ConvexOptimization.conic_slater_strong_duality may help with the duality step.
Nuclear norm minimization is the standard convex surrogate for rank minimization: to recover a low-rank matrix from a few linear measurements, or from a subset of its entries, one minimizes the sum of the singular values subject to the data constraints. For matrix completion, Candès and Recht (Found. Comput. Math. 2009) showed that this convex program recovers a low-rank matrix exactly from sufficiently many random entries. Solving it at scale is another matter: interior-point methods for the equivalent semidefinite program become impractical beyond matrices of a few hundred rows and columns.
Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm, whose iterates are cheap and typically of low rank. SVT does not solve the nuclear norm problem itself. It solves a proximal problem, in which the nuclear norm is replaced by for a fixed parameter . Section 3.4 of the paper justifies this substitution: as , the solutions of the proximal problem converge to a specific solution of the nuclear norm problem, the one of least Frobenius norm. This mission formalizes that result, Theorem 3.1 of the paper, under general convex constraints.
Let be natural numbers and the space of real matrices, with the inner product . Three functions of a matrix are used:
Let be constraint functions and the feasible set. The nuclear norm problem is
and, for , the proximal problem is
When the are convex and is nonempty, (3.4) has exactly one solution, written , because is strongly convex. Problem (1.6) may have many solutions. Among them, the paper singles out the minimum Frobenius norm solution
Linear equality constraints, and in particular the matrix completion constraints for sampled entries , are covered by taking pairs of affine functionals.
Assume that the are convex and lower semicontinuous. Then
In the order in which the paper's proof uses them (all on p. 1967):
The result itself. Theorem 3.1 is the link between the problem SVT actually solves and the problem one wants solved. The companion missions of this series prove that the SVT iteration, and its variant for general convex constraints, converges to . Theorem 3.1 says what is worth: for large it is close to a nuclear norm minimizer, and the minimizer it approaches is identified exactly, namely the one of least Frobenius norm. The statement is not specific to matrix completion. It covers every finite family of convex, lower semicontinuous constraints, and hence noisy variants such as the inequality-constrained problems of §3.3 of the paper.
Formalizing it. The theorem is proved in the paper, in about half a page. It has not, to our knowledge, been machine-checked. A formal proof pins down the hypotheses: the argument needs the minimizers to exist, and it uses continuity and convexity of the nuclear norm, closedness of the feasible set, and uniqueness of . It also produces a reusable fact about the nuclear norm in Lean, namely that the sum of singular values is a continuous convex function of the matrix.
The first steps are elementary consequences of the definitions of and : (3.16) compares objective values, and (3.17) and the convergence of the nuclear norms follow by algebra and a squeeze. The difficulty lies elsewhere.
A tempting shortcut, reading the family as a sequence indexed by integers, proves a weaker statement: the limit in (3.15) is over real .
Matrix (Fin n₁) (Fin n₂) ℝ, abbreviated Mat n₁ n₂, over the reals as in the paper. and .LinearMap.singularValues of Matrix.toEuclideanLin X. It is the genuine sum of singular values, not an abstract norm or the Frobenius norm.f : Fin m → Mat n₁ n₂ → ℝ of real-valued functions. (no constraints) is allowed.ConvexOn ℝ Set.univ (f i) and LowerSemicontinuous (f i) for every . Lower semicontinuity is redundant for real-valued convex functions on a finite-dimensional space, but it is kept because the theorem states it.Xτ : ℝ → Mat n₁ n₂ assumed to solve (3.4) for every , and its values at play no role. is a matrix assumed to satisfy the defining property (3.14): it solves (1.6) and has the least among its solutions. Uniqueness of is a milestone to prove, not an assumption.Filter.atTop on . Convergence of matrices uses Mathlib's entrywise topology, which is the topology of . The goal states (3.15) literally, with the Frobenius norm of the difference tending to .Infrastructure. The needed facts, all reusable beyond this mission:
Contributions of these general lemmas as separate theorems are welcome.
Singular value thresholding (SVT) is a first-order method introduced by Cai, Candès and Shen (SIAM J. Optim. 20 (2010)) for recovering a low-rank matrix from incomplete or indirect information. Its basic form, for matrix completion, alternates a soft-thresholding of singular values with a gradient step on a dual variable, and needs only one sparse singular value decomposition per iteration. That is what made nuclear-norm heuristics usable on matrices with tens of thousands of rows and columns, where interior-point methods for the equivalent semidefinite program do not fit in memory.
Matrix completion is only one constraint set. In applications the data are noisy linear measurements , and the constraint takes the form of componentwise error bounds or norm balls around the data (§3.3 of the paper). Section 3.2 of the paper extends the method to a general finite family of convex constraints, and §4.2 proves that the extended iteration converges. This mission formalizes that extension and its convergence theorem, Theorem 4.4.
Let be natural numbers and the real matrices, with the Frobenius inner product and norm . The nuclear norm is the sum of the singular values of . For a fixed the objective is
A matrix is a subgradient of a function at , written , if for all .
Let be convex and put . On , and is the Euclidean norm. The constrained problem is
with Lagrangian for . A pair with is primal-dual optimal if it is a saddle point:
The paper's standing assumption "strong duality holds" is the existence of such a pair.
The iteration (3.5) starts from and, for step sizes , sets for
where has entries . It is Uzawa's method for (3.4): an exact minimization in the primal variable followed by a projected ascent step on the dual. When is affine, the minimization is a singular value thresholding step, which gives the algorithm its name.
The analysis of §4.2 assumes is Lipschitz in the sense
for a constant .
If and strong duality holds, then the sequence of (3.5) converges to the unique solution of (3.4):
The result. Theorem 4.4 is the convergence guarantee for SVT beyond matrix completion. The componentwise error bounds of (3.8), whose SVT iteration is (3.9), are finitely many affine constraints and fall under it directly, as does any finite family of Lipschitz convex constraints, for instance a Frobenius-norm ball around the data. The conic variants of §3.3 ((3.11)–(3.13)) project the dual variable onto a cone rather than onto the nonnegative orthant and are not covered by the theorem as stated. Together with Theorem 3.1 of the same paper, which says that the solution of (3.4) tends to the minimum-nuclear-norm solution as , it justifies using SVT as a solver for nuclear-norm minimization under general convex constraints.
Formalizing it. The theorem is proved in the paper, with two steps delegated to the literature: Lemma 4.3 cites [31], and the concluding step reads "the conclusion is as before". Its proof is short but relies on convex-analytic facts that are standard on paper and missing, in this form, from Mathlib: subgradients of the nuclear norm, the subdifferential sum rule for finite convex functions, and nonexpansiveness of the projection onto the nonnegative orthant. No machine-checked proof of this theorem or of Uzawa-type convergence for nuclear-norm objectives is known to exist. The mission produces a complete, checked version of the argument, including the omitted closing step.
The obvious approach is to view (3.5) as projected gradient ascent on the dual function and quote the standard convergence theorem for gradient methods with Lipschitz gradients. That does not apply directly: for general convex the dual function need not be differentiable, is only a supergradient, and the Lipschitz hypothesis (4.2) is on , not on a dual gradient. The proof instead works with the primal-dual pair: it needs first-order optimality conditions (4.4), which require a subdifferential sum rule for with nonsmooth , and it needs the strong monotonicity of (Lemma 4.1), which depends on the description of subgradients of the nuclear norm. A second subtlety is that the theorem asserts convergence of the whole primal sequence to the unique solution, not to some solution along a subsequence, while nothing is claimed about convergence of the dual sequence.
Matrices are Matrix (Fin n₁) (Fin n₂) ℝ, vectors in are Fin m → ℝ, and convergence of matrices is in Mathlib's product topology, which coincides with the Frobenius topology. The nuclear norm is the sum of Mathlib's LinearMap.singularValues of the matrix viewed as a map between Euclidean spaces. Each is a real-valued function with ConvexOn ℝ Set.univ. The iteration is a predicate on sequences indexed by ℕ: the paper's step produces X (k+1) and y (k+1) from y k with step size δ (k+1), and y 0 = 0. is required to minimize ; for and convex this minimizer exists and is unique, so the predicate is satisfiable and determines the sequence. The step-size condition is stated as for with and , which avoids the division (evaluated as in Lean when ); for it requires only bounded steps, matching the convention . Strong duality is the hypothesis that a saddle point exists; Slater's condition is not assumed. The paper's standing assumptions (, convex , and (4.2) where enters) appear as explicit hypotheses in every statement.
A formalization that assumes convergence or boundedness of the dual iterates, replaces the primal minimization by a closed-form thresholding step (valid only for affine ), or states only subsequential convergence would not be this theorem; each of these is excluded by the statements above.
A complete development needs: subgradients of the nuclear norm and strong monotonicity of ; existence and characterization of minimizers of strongly convex continuous functions on a finite-dimensional space; the subdifferential sum rule for finite convex functions; complementary slackness from the saddle-point inequalities; and nonexpansiveness of the entrywise positive part. These are reusable beyond this mission, especially for other Uzawa and augmented Lagrangian analyses. Contributions of any of these pieces as separate lemmas are welcome.
Matrix completion asks to recover an matrix from a subset of its entries. When has low rank, a standard convex surrogate is to minimize the nuclear norm (the sum of the singular values) subject to agreeing with on ; Candès and Recht showed that this recovers exactly under incoherence and sampling conditions (Candès–Recht 2009). Generic interior-point solvers for this semidefinite program do not scale beyond matrices of a few hundred rows.
Cai, Candès and Shen (SIAM J. Optim. 2010) proposed the singular value thresholding (SVT) algorithm: a first-order iteration whose only nonlinear step is a soft-thresholding of singular values, and whose other iterate is a sparse matrix supported on . The algorithm has become a standard baseline in low-rank matrix recovery and a model example of dual (Uzawa-type) methods for nuclear-norm problems. This mission formalizes its convergence theorem.
All matrices are real. For write and . The nuclear norm is the sum of the singular values of .
For an index set , the sampling projector keeps the entries with indices in and sets the others to zero.
A reduced singular value decomposition of a matrix of rank is with () and () having orthonormal columns and with . For the singular value shrinkage operator is
Fix , a sequence of step sizes and data . The SVT iteration (2.7) starts from and sets, for ,
The proximal problem (2.8) is
More generally, for a linear map with adjoint and spectral norm , and , problem (3.1) is to minimize subject to , and Uzawa's iteration (3.3) starts from and sets , .
If , then (2.8) has a unique solution and the SVT iterates satisfy
If (3.1) is feasible and , then (3.1) has a unique solution and the iterates of (3.3) converge to it.
The theorem certifies that SVT, run with any step sizes in a fixed interval , computes the unique minimizer of the strongly convex surrogate (2.8). Together with the separate fact that the solution of (2.8) tends to the minimum nuclear norm completion as (the paper's Theorem 3.1, a companion mission), this is what justifies using SVT as a solver for nuclear-norm matrix completion. Theorem 2.1, the proximal characterization of singular value soft-thresholding, is used throughout the literature on proximal methods for low-rank problems.
The paper's proof of Theorem 4.2 consists of the reduction to Uzawa's method and a citation of a general convergence theorem for projected gradient methods on the dual. The formalization produces a self-contained, machine-checked chain: the proximal characterization of , the Lagrangian identity, strong monotonicity of , and the convergence argument itself. To our knowledge none of these results has a machine-checked proof; Mathlib at the pinned revision has singular values of linear maps but no SVD structure, no nuclear norm and no subgradient calculus.
Nothing in the iteration is a gradient step of a smooth function in : the -update is a nonsmooth proximal map, and the convergence of is not visible from the recursion itself. The paper's argument cites a general theorem on projected gradient methods ([25, Theorem 2.1]) and takes for granted that "strong duality holds" for (2.8) (p. 1963), so the existence of a Lagrange multiplier is part of what must be formalized. Theorem 2.1 depends on the subdifferential of the nuclear norm, which Mathlib does not provide, and therefore on the singular value decomposition and the duality between the nuclear and spectral norms. Convergence of objective values or of a subsequence would not suffice: the target is convergence of the whole sequence to the unique solution.
Matrices are Matrix (Fin n₁) (Fin n₂) ℝ; convergence is Mathlib's topology on matrices, which coincides with the Frobenius-norm topology. and are defined entrywise; is the sum of Mathlib's LinearMap.singularValues of viewed as a map . The shrinkage operator is a relation IsShrink τ Y X defined, as in (2.1)–(2.2), through some reduced SVD of ; well-definedness is a milestone. It is not defined as the minimizer of (2.3), which would make Theorem 2.1 definitional. Linear maps are given by matrices with , and a sampling operator by an injective enumeration of . Subgradients are those of (2.4).
Sequences are indexed by : Lean's step is the paper's step , so and are unused. Committed conventions:
A small unprinted helper, for sampling operators, is included to pass from the first sentence of Theorem 4.2 to the second; it is not a milestone. The subdifferential formula (2.6) of the nuclear norm and the Fejér-type condition of §5.1.2 are not stated. Reusable infrastructure welcome from solvers: existence and uniqueness properties of the reduced SVD, the nuclear/spectral norm duality, the subdifferential of the nuclear norm, and a general convergence theorem for Uzawa's method with a strongly convex objective.
The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It is a basic model in operations research, underlies bipartite matching, transportation and scheduling problems, and is a standard subroutine inside larger combinatorial algorithms.
The classical method for it is the labeling method of Ford and Fulkerson: starting from some flow, repeatedly find an augmenting path from source to sink along which flow can be increased, push as much as the path allows, and stop when no such path exists. When all capacities are integers, each augmentation raises the flow value by at least one, so the method terminates, but the number of augmentations can be as large as the final flow value, which is exponential in the size of the input. Edmonds and Karp give a four-node example in which the method alternates between two paths and needs augmentations for capacities (Edmonds–Karp 1972, p. 250). With irrational capacities, Ford and Fulkerson showed that the method need not terminate at all and may converge to a non-maximum flow.
Timeline.
A network consists of a finite set of nodes, a source and a sink , and a set of arcs, which are ordered pairs with ; there is at most one arc from a node to another. One arc is the special return arc , and denotes the set of all other arcs. Each has a real capacity .
A flow is a nonnegative function on the arcs of with on and with inflow equal to outflow at every node, the return arc included. The value is the amount sent from to ; a maximum flow maximizes it.
Given a flow , the residual network has the same nodes, and is an arc of when with , or with . An augmenting path is a sequence of distinct nodes whose consecutive pairs are arcs of . Each step carries a number (residual capacity forward, flow backward, or their sum when both and lie in ); , and a step with is a bottleneck arc. Augmenting raises by and shifts the flow on the path's arcs accordingly, using the paper's own rule for opposite arcs, which never exceeds a capacity.
A run with fewest-arc augmentations is a sequence where is a flow and each arises from by augmenting along a path with fewest arcs. The distance is the least number of arcs of a directed path from to in , or .
For every network on nodes and every run of length with fewest-arc augmentations,
and if no augmenting path exists relative to , then is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.
The theorem shows that one simple rule for choosing augmenting paths, which a breadth-first labeling process implements, makes the number of augmentations depend on the number of nodes alone, independent of the capacities and of their arithmetic nature. It removes both pathologies of the unrestricted labeling method at once: exponential running time for integer capacities, and non-termination for irrational ones. Together with Dinic's work it is the starting point of the theory of strongly polynomial network-flow algorithms, and the distance-monotonicity argument (Proposition 3, Lemma 2) reappears in blocking-flow and push-relabel analyses.
The result is classical and fully proved in the paper. What this mission adds is a machine-checked version of the complete argument in the paper's own model: return arc, arbitrary real capacities, and the paper's augmentation rule for pairs of opposite arcs, which differs from Ford and Fulkerson's (footnote 1, p. 249). The platform has a max-flow min-cut theorem and an integer termination theorem for the Ford–Fulkerson method in the Bertsimas–Tsitsiklis model (Introduction to Linear Optimization, missions IX–X), but no bound on the number of augmentations. No machine-checked proof of Theorem 1 in Lean is known to exist.
The obvious argument, "each augmentation saturates a bottleneck arc, which then disappears", fails because a saturated arc can reappear after later augmentations push flow back along its reverse. Counting augmentations therefore requires control over how often the same pair of nodes can supply a bottleneck again, and no property of a single augmentation provides it; the bound has to come from an invariant of the whole run that holds for real capacities, where no integrality argument is available. A second trap is that the converse direction of milestone 2 (no augmenting path implies maximality) is a max-flow min-cut statement that the paper cites without proof; it must be proved in the paper's model with the return arc.
Nodes form a finite type V with decidable equality and = Fintype.card V counts all nodes, and included. The arc set A is a Finset (V × V) with no loops and without ; capacities are real and positive on A. A flow is a function V → V → ℝ whose values off the arcs are ignored. A maximum flow is the predicate " for every flow ", never a real supremum. Paths are lists of distinct nodes with every consecutive pair a residual arc, so the return arc is never on a path. Distances take values in ℕ∞. A run is a pair of ℕ-indexed sequences constrained on indices up to . The explicit constants are stated as printed: in ℕ (the truncated subtraction is harmless since ) and for the per-pair count.
Case (b) of the paper's definition of augmenting paths is misprinted (its hypothesis repeats that of Case (c)); the formalization uses the reading , , which the paper's own description of on p. 251 confirms.
A trivializing formalization is ruled out: a run predicate that no sequence satisfies (for instance, one that requires paths through the return arc, or computes ) would make the bound vacuous; the step predicate here is satisfiable, and a concrete four-node run has been checked. Replacing the paper's augmentation rule by "increase the forward arc by " would also change the theorem, because that rule can violate capacities.
A complete development needs basic facts on simple paths in finite digraphs, shortest paths and their subpaths, and a max-flow min-cut theorem in the paper's model. These are reusable well beyond this mission, as are the network, residual-network and augmentation definitions. Contributions proving any milestone independently are welcome.
Many problems in signal processing, statistics and machine learning minimise a sum of three convex terms: a smooth data-fit term and two nonsmooth regularisers or constraints, each of which is easy to handle on its own (through its proximal map) but not in combination. Examples are constrained sparse regression, matrix completion with a nuclear-norm penalty and box constraints, and support-vector machines with a norm penalty. Davis and Yin (Set-Valued Var. Anal. 25 (2017)) introduced a three-operator splitting scheme that evaluates each proximal map and the gradient of the smooth term once per iteration and reduces to Douglas–Rachford splitting (Lions and Mercier 1979) and forward–backward splitting as special cases. Section 3 of that paper gives the objective-error rates of the scheme on convex problems. This mission formalizes those rates for general convex problems.
Let be a real Hilbert space. The problem is
where are closed, proper, convex functions (lower semicontinuous, never , finite somewhere, with convex epigraph) and is convex and differentiable with -Lipschitz gradient , .
For the proximal map is the unique minimiser of . Algorithm 2 of the paper picks and and iterates, with relaxation ,
Equivalently for the three-operator map
If is a fixed point of , then minimises (3.1). The weighted ergodic iterate is
and is defined the same way from .
Let be a fixed point of , , and suppose is -Lipschitz continuous on the closed ball . Then there is a constant , independent of , with
The goal asserts the order and leaves the constant free, so it is not invalidated by a sharper constant.
The result. Theorem 3.1 gives the last iterate an objective error of . Theorem 3.2 shows that averaging with linearly increasing weights improves this to , the rate of the standard uniform ergodic average, while putting more weight on recent iterates. The paper notes that this matters when the iterates are sparse vectors or low-rank matrices and the average should stay close to them. The rates hold under a local Lipschitz condition on one of the two nonsmooth terms only, so may be the indicator function of a constraint set. They therefore cover the constrained applications of Section 4 of the paper.
Formalizing it. The results are proved in the paper. No machine-checked version of this scheme or its rates exists on the platform or, as far as is known, in Mathlib. A formalization produces a checked proof in an arbitrary real Hilbert space with extended-valued . It also produces infrastructure that Mathlib lacks: proximal maps characterised by minimisation, the prox-subgradient inclusion, Fejér monotonicity of an averaged-operator iteration, and a weighted Jensen inequality for extended-valued convex functions. All of these can be reused by other splitting and proximal-gradient missions. The formalization also checks the constants: the last display of the published proof of Theorem 3.2 drops a factor in front of the Lipschitz term, and the printed ball in both theorems is centred at where the proof needs .
The obvious argument sums the one-step inequality (3.2). That controls the objective at the two different points and , and only appears, never . Moving from one point to the other needs the Lipschitz hypothesis on , and so it needs every iterate, and every weighted average, to stay in the ball on which that hypothesis holds. For the weighted average there is a further obstacle: the cross term does not telescope under the weights . Controlling it requires the summability of the gradient differences (2.7), which is inherited from the averagedness analysis of Section 2 and not from convexity alone. Uniform averaging with the same argument does not give the weighted statement, and the weights must not be replaced.
InnerProductSpace ℝ H, CompleteSpace H), not .EReal. They are proper (never , somewhere ), lower semicontinuous, and have a convex epigraph in . is convex and differentiable, and Mathlib's gradient h is -Lipschitz.Welcome contributions: the prox–subgradient inclusion for EReal-valued convex functions, averagedness and Fejér monotonicity of (the companion mission on Section 2 treats the general operator case), a weighted Jensen inequality in EReal, and proofs of the milestones in the listed order.
Many problems in convex optimization, variational inequalities and signal processing reduce to a monotone inclusion: find a point at which the sum of several monotone operators contains . When the sum has two terms, the classical operator-splitting methods (Douglas–Rachford, forward–backward, forward–backward–forward) solve it by iterating a fixed-point map that uses each operator separately, through its resolvent or through a forward (explicit) step. Problems with three terms, for instance a smooth loss plus two nonsmooth regularizers or constraints, are common in practice, and before 2015 no fixed-point map was known that handled three operators one at a time without a product-space reformulation.
Davis and Yin (Set-Valued Var. Anal. 25 (2017) 829–858; preprint arXiv:1504.01032) introduced such a map, now called Davis–Yin three-operator splitting. It contains Douglas–Rachford splitting () and forward–backward splitting () as special cases, and it has become a standard building block of first-order methods for composite optimization. This mission formalizes Section 2 of the paper: the fixed-point encoding, the averagedness of the map, and the weak and strong convergence of the resulting iteration.
Let be a real Hilbert space. A set-valued operator is monotone if for all , , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. Its domain is and the zero set of an operator is . A single-valued is -cocoercive () if for all .
Problem (1.1) is: given maximal monotone and -cocoercive , find
For the resolvent is the map with . The Davis–Yin operator (Eq. (1.2)) is
Algorithm 1 starts from and, for relaxation parameters , iterates
so that . A sequence converges weakly, , if for every .
Fix , , and with , where , and . If , there is with and
and if or is uniformly monotone on every nonempty bounded subset of its domain, or is demiregular at every zero of , then and converge strongly to a common point of .
In the order the proof uses them: Lemma 2.1 (the identities for one application of ), Lemma 2.2 (), Lemma 2.3 (inequality (2.1)), Proposition 2.1 ( is -averaged, inequality (2.2)), Remark 2.1 (the strengthened inequality (2.4)), Corollary 2.1 Parts 1–3 (Fejér monotonicity, vanishing residual, weak convergence of ), Corollary 2.1 Part 4 (the residual rates and ), and Eqs. (2.6)–(2.7) (the per-step descent inequality and its summed form).
Theorem 2.1 is the basic convergence guarantee for three-operator splitting: it certifies that the computable sequences , , not only the auxiliary sequence , approach a solution of (1.1). In infinite dimensions this is the delicate part: for Douglas–Rachford splitting () weak convergence of the shadow sequence was only established by Svaiter in 2011. The result underlies the convergence of the many algorithms obtained from it by specialization (Douglas–Rachford, forward–backward, and the three-block methods of Section 4 of the paper), and the averagedness coefficient of Proposition 2.1 reduces, for , to the best known one for forward–backward splitting.
All statements of this mission are proved in the paper, partly by appeal to Bauschke and Combettes' monograph (Krasnosel'skiĭ–Mann convergence, the demiclosedness of maximal monotone graphs). None of them has a machine-checked proof: Mathlib has no maximal monotone operators, resolvents, averaged maps or Krasnosel'skiĭ–Mann theorem. The mission therefore produces both a formal proof of the Davis–Yin theorem and a first body of monotone-operator theory in Lean.
The fixed-point part is standard once is known to be averaged: Krasnosel'skiĭ–Mann theory and Opial's argument give . The obstacle is transferring this to . Resolvents are nonexpansive but not weakly continuous, so does not imply ; the naive argument fails at exactly this step. Identifying the weak cluster points of requires a closedness property of sums of maximal monotone operators under mixed weak and strong convergence, fed by the strong convergence of , which in turn needs the extra term of (2.4) that (2.2) discards. Strong convergence in Part 2 needs yet another argument for each of the three alternative hypotheses.
NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); a finite-dimensional space would identify weak and strong convergence and change the theorems.H → Set H; is single-valued H → H. The resolvents are not constructed: are maps satisfying the resolvent inclusion , which for maximal monotone operators determines them uniquely and exists by Minty's theorem.A complete development needs the basic theory of monotone operators (monotonicity of resolvents' graphs, firm nonexpansiveness of resolvents, weak-to-strong closedness of maximal monotone graphs), Krasnosel'skiĭ–Mann iteration with Opial's lemma, and weak sequential compactness of bounded sets in Hilbert space. All of this is reusable far beyond this mission, and contributions of any of these pieces as separate theorems are welcome.
In 1955 E. M. L. Beale showed how Dantzig's simplex method, which was built for linear objectives, can be carried over to certain nonlinear convex objectives that are minimized subject to linear inequalities (Beale 1955). Section 4 of that paper treats one such objective: the sum of the largest of a set of linear forms. Beale's motivation comes from the theory of games: "if the enemy has to choose out of a set of possible actions, and represents his average gain through using the th", then the defender wants to minimize the sum of the largest .
The same objective can be written as a linear program. One introduces a bound and requires every sum of forms to be at most . That formulation has constraints, which is unwieldy once and is large. Beale's alternative works with the nonlinear objective directly, and he needs a test that tells him when the current basic solution is already optimal. This mission formalizes that test, Theorem 1 of the paper.
The objective reappears in later work under other names: the sum of the largest components of a vector, the "top- sum", and times the conditional value-at-risk of an empirical distribution. Beale's paper is an early source for its optimality conditions.
There are real variables , indexed by in a finite set (possibly empty), and . Two linear forms in these variables are given,
together with further forms
For an integer the objective is
The sum of the largest of numbers is the largest total of any of them. Ties do not make it ambiguous.
The feasible region is fixed by a set of indices. The variables with and all the are free, and every other is restricted to . At the origin , all forms are equal to , so the origin is where fails to be differentiable. In Beale's algorithm the origin is the current basic solution: the measure how far the "borderline" forms sit from a chosen critical form, and collects the forms that are certainly among the largest.
Write and .
For , is minimized over the feasible region when all the and vanish if and only if
"Minimized" means a global minimum: at every feasible point.
Theorem 1 is the optimality test of Beale's simplex method for the sum-of-largest objective. The algorithm on pp. 178–179 changes nonbasic variables one at a time. When no single change is profitable it applies Theorem 1: either (4.5) holds and the current solution is optimal, or one of the six descent rules names the variable to change next. The test is exact even though the objective is not differentiable at the current point. It is a closed-form description of the subdifferential of a top- sum at a point where all the forms tie. The theorem is also the base case of the multi-group generalization that Beale mentions on p. 181.
The paper proves Theorem 1 by hand. To our knowledge neither the theorem nor the rearrangement identity behind it has been formalized in any proof assistant. The mission produces:
Necessity, the "only if" direction, is the part the paper calls obvious: each descent rule changes linearly for small steps. Two features still have to be handled explicitly. The step must be small only in rule-dependent ways, and the ordering of the forms changes along the moves of rules 4 and 6.
Sufficiency is where the work lies. The naive argument, "the directional derivative in every coordinate direction is non-negative, so the origin is a minimum", fails because is not differentiable at the origin. Nonnegative derivatives along the coordinate axes do not control mixed directions in which several move by different amounts, which reorders the forms. Which forms are the largest then depends on the point, and the paper settles the configurations in which is among the largest by an informal appeal to the "essential symmetry" between and the other forms. A formal proof cannot leave that appeal informal: the forms are parametrised relative to (each is ), so the symmetry is a change of variables that has to be written down and shown to preserve (4.5).
z : Fin r → ℝ (any r, including ) and u : Fin s → ℝ. The paper's for is Lean's u f for . The coefficients form a structure Forms r s.Fin (s+1) → ℝ, with index for and index f.succ for . The free set is a Finset (Fin r), and is a natural number cast to wherever it multiplies a coefficient.sumLargest τ v is the maximum over -element subsets of (Finset.sup' over powersetCard). It is the junk for larger than the number of entries, a case no statement uses.Needed infrastructure:
sumLargest: its value at a constant family, at a family sorted by a monotone shift, and under adding a common constant;These lemmas are reusable for any top--sum or empirical-CVaR objective. Contributions are welcome at any level: lemmas about sumLargest, any of the milestones, or an alternative sufficiency proof through convexity and one-sided directional derivatives.
Not in scope: the pivoting rules (4.2)–(4.4), the degeneracy discussion on pp. 180–181, and the multi-group generalization, which the paper says is "cumbersome to state" and does not state.