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?
Comparing uncertain outcomes is the basic problem of decision making under risk. Second-degree stochastic dominance (SSD) is the comparison that every risk-averse decision maker who prefers larger outcomes agrees with: dominates in this sense exactly when for every nondecreasing concave utility for which the expectations are finite. The relation grew out of majorization theory for finite distributions (Hardy, Littlewood and Pólya) and was extended to general distributions by Rothschild and Stiglitz and by Hadar and Russell around 1970; it is the standard consistency requirement for portfolio models and for risk measures in operations research and finance.
SSD is defined through the distribution function, which is awkward in optimization: portfolio returns are linear in the decision variables, but their distribution functions are not. Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) showed that SSD has an equivalent dual description through the integrated quantile function, the absolute Lorenz curve, and that the two descriptions are related by Fenchel conjugation. That dual description underlies the later theory of SSD-constrained optimization (Dentcheva and Ruszczyński, SIAM J. Optim. 14 (2003)) and the use of conditional value-at-risk as an SSD-consistent risk measure.
Fix a probability space and real random variables with , .
distFun P X).secondPerformance P X, eq. (2.1)).SSD P X Y, eq. (2.2)). The dominating variable has the smaller curve.leftQuantile P X). A number is a -quantile if (IsPQuantile P X p q).secondQuantile P X, eq. (3.2)).conj F), and is the subdifferential of a real function at (subdiff f η).Both directions are required, and the range of includes both endpoints (at the right-hand side contains ).
A companion item, Corollary 3.3, states the four equivalent characterizations of a -quantile (quantile condition, attainment in either conjugate, and the Fenchel–Young equality ).
Theorem 3.2 converts a condition on distribution functions into a condition on integrated quantiles. Its consequences in the paper include the SSD consistency of the mean–risk models built on tail means (conditional value-at-risk), on the Gini mean difference and on the mean absolute deviation from a quantile, and the linear-programming representations of those models for finitely many scenarios; the companion mission Dual Stochastic Dominance and Related Mean-Risk Models 2 builds on the same objects. Theorem 3.1 is the precise statement that and form a conjugate pair; Corollary 3.3 identifies the subgradients of each with the quantiles of .
All results here are proved in the paper, and the quantile characterization of the increasing concave order also appears in the stochastic-orders literature. None of them is formalized: Mathlib at the pinned revision has ProbabilityTheory.cdf but no convex conjugate on the extended reals, no subdifferential of a real function, no quantile function and no stochastic dominance. The mission produces a machine-checked account of the quantile side of SSD, with the conjugacy stated exactly, including the value off .
The naive route to Theorem 3.2 compares and through the quantile functions directly, but the first quantiles need not be ordered when (the paper notes this on p. 65), so no pointwise argument on quantiles works. The equivalence rests on Theorem 3.1, and there the hard part is computing the conjugate of for a general distribution: atoms of make nondifferentiable and flat pieces of make the maximizer non-unique, so the subdifferential (3.3) and the interval of -quantiles must be handled as sets, and the endpoints (where the supremum need not be attained) and (where it is ) must be treated separately. Part (ii) is a biconjugation statement for a closed convex function, whose general form is not in Mathlib.
(Ω, P) with [IsProbabilityMeasure P] carries both and ; nothing depends on anything but the laws, and no independence is assumed.P.real {ω | X ω ≤ η}; is a Bochner integral over Set.Iic η; is an interval integral over , placed in EReal, with ⊤ off .⨆ ξ, ((p * ξ : ℝ) : EReal) - F ξ in the complete lattice EReal, so terms where contribute , exactly the paper's convention.Integrable X P (and Integrable Y P in the goal). This is the paper's own hypothesis (p. 65, and the hypothesis of Theorem 3.1), not a repair. The -quantile milestone assumes only AEMeasurable X P.sInf. It is the true infimum for ; at the paper's value can be while sInf ∅ = 0. This one point does not affect (3.2), and no item states anything about .VectorSpaceOpt.fenchel_biconjugate_on and ConvexOptimization.fenchelConjugate concern real-valued conjugates on other spaces and are related but not reused.A stochastic processing network (SPN) is the general model behind manufacturing lines, call centers, computer systems, communication networks and hospital wards: a collection of buffers holding waiting work, a collection of activities (servers) that consume items from buffers and produce items into others, and stochastic primitives — arrival processes and service requirements — that drive the whole system forward in continuous time. Before any control policy can be designed, evaluated, or proved to work, the modeler needs a single, unambiguous, checkable notion of what it means for such a system to be stable: to settle into statistical equilibrium rather than pile up work without bound.
The difficulty is that "stability" has several natural, superficially different candidate definitions — positive recurrence of the underlying Markov chain, existence of a unique stationary distribution, convergence in distribution of queue lengths — each convenient for a different purpose (positive recurrence for verifying via drift criteria, a stationary distribution for computing long-run averages, distributional convergence for interpreting simulation output). J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' own pre-publication draft, 2020-4-2, http://spnbook.org) opens its technical development by proving these candidates coincide, so that the rest of the book — and, in practice, most stability results for queueing networks published since Rybko and Stolyar's and Dai's foundational work in the 1990s — can speak of "SPN stability" as one well-posed property.
An SPN has buffers, indexed , and activities (service types), indexed . External work arrives into buffer according to a counting process ; activity , whenever engaged, requires a service time and produces an output vector into the buffers on completion. The baseline stochastic assumptions (Assumption 2.1) specify these primitives precisely: the external arrival processes are independent Poisson processes with rates (no arrivals into a buffer with rate ); for each activity , the matched pairs of processing variables — service time and output vector, — form an i.i.d. sequence with finite means and ; each such pair has a joint phase-type distribution (realized as the absorption time and terminal mark of a finite-state continuous-time Markov chain, per Appendix D.9); and the initial processing variables, the arrival process, and the processing-variable sequences are, collectively, mutually independent.
Under a fixed control policy, the SPN generates two continuous-time processes: the service-count process and the buffer-contents process . Assumption 3.1 (Markov representation) requires these to be embeddable in a richer, irreducible Markov chain on a countable state space : a function with on every sample path, whose level sets are finite for every buffer-content vector , and which has at least one empty state with .
and, when these hold, for every bounded and every initial distribution of ,
Definition 3.6 then names an SPN stable exactly when these equivalent conditions hold — the weakest possible target, since it commits to no particular one of the three characterizations, only to their joint truth or falsity.
Two strong laws of large numbers for the primitive stochastic elements (Propositions 2.2 and 2.3) — the arrival counts and the processing-variable sample means , — and two structural results about the ambient chain: Lemma 3.7, a drift-type sufficient condition for positive recurrence that foreshadows the fluid-model methodology of later chapters, and Proposition 3.9, a sufficient condition (reachability of the empty state) for the irreducibility that Assumption 3.1 itself demands.
The result itself. Proposition 3.5 is what turns "is this queueing network stable?" into a single question rather than three potentially different ones, and it licenses every later chapter of the book (and a large fraction of the queueing-theory literature going back to the 1990s fluid-limit program of Rybko–Stolyar, Dai, and others) to prove stability via whichever characterization is most convenient — typically positive recurrence via a Lyapunov drift argument — while concluding all three, including the practically important long-run-average SLLN. Every one of the thirteen other missions in this series builds directly on Definition 3.6: their goal theorems all conclude "the SPN is stable," meaning exactly the three-way equivalence established here.
Formalizing it. No result in this mission or its milestones has a prior formal counterpart on
Prove2Me: a search for "positive recurrent," "stationary distribution Markov chain," and
"irreducible Markov chain" surfaced only MarkovMixing's PositiveRecurrent predicate, defined
for a countable-state discrete-time chain — a different object from Assumption 3.1's
continuous-time ambient chain, reused here only conceptually (as the pattern for a mean-return-time
definition), not as a Lean dependency. This mission is a from-scratch formalization of the
model (baseline stochastic assumptions, Markov representation) and of positive recurrence,
stationary-distribution uniqueness, and distributional convergence for it.
The obvious first attempt — define as an arbitrary countable-state Markov chain and directly
import a Mathlib theorem relating its recurrence, its stationary distribution, and long-run
convergence — fails because Mathlib currently has no general countable-state continuous-time
Markov chain theory of the kind Appendix D of the book develops (its own finite-state CTMC
stationary-distribution result is unproven substrate, not applicable to a countably infinite
state space). The formalization instead works at the level of the chain's embedded discrete-time
jump chain, which is where Lean's PMF-based machinery is available, and states the three
equivalent conditions and the SLLN conclusion directly as hypotheses to be discharged, rather than
inheriting them from a pre-existing continuous-time framework. A second difficulty is Assumption
2.1(d)'s independence clause, which is a genuine three-way mutual independence of -algebras
(initial processing variables, arrival process, and the collection of all processing-variable
sequences), not the pairwise independence a careless reading might substitute — a weaker
hypothesis here would silently make later derivations in the series unsound.
The ambient chain's state space Xstate is an arbitrary countable type ([Countable Xstate],
not Fintype) — no result may assume finiteness anywhere. The chain itself is represented by its
one-step jump kernel jump : Xstate → PMF Xstate (stepIter gives -step iteration,
Irreducible requires every state to reach every other in finitely many jump-chain steps);
positive recurrence is mean return time under jump, defined via the standard first-return-time
renewal decomposition. IsStable is defined as positive recurrence of the jump chain — one of
the three equivalent conditions — with the goal theorem itself certifying the equivalence, so the
choice carries no loss of faithfulness. Buffer contents and service counts are Fin I → ℕ and
Fin J → ℕ-valued, matching the book's , . A formalization that
took IsStable to mean, say, only distributional convergence of (dropping the chain-level
characterizations) would be a strictly weaker, trivializing shortcut — ruled out here by proving
all three equivalent and stating the SLLN as part of the same goal theorem. The definitions in
this mission (BaselineAssumptions, MarkovRepresentation, IsStable) are the shared substrate
every other mission of the series is built on, and are the primary reusable contribution;
contributions completing the by sorry proofs, particularly of the goal theorem (which the book
proves via appeal to general CTMC theory in its Appendix D, not reproduced here), are welcome.
A decision problem with several conflicting objectives, such as cost, risk and service level, has no single optimum. What it has is a set of nondominated outcomes: those that cannot be improved in one objective without being worsened in another. Interactive methods of multiple objective programming search this set with a decision-maker, and at each step they need a computational device that returns nondominated outcomes and can return any of them.
The classical device, maximizing a weighted sum of the objectives, fails the second requirement. On a nonconvex or discrete outcome set it only reaches the supported nondominated points, those on the boundary of the convex hull, and misses the rest (see, e.g., Boyd and Vandenberghe, Convex Optimization, §4.7.4, where the weighted-sum approach is shown to be sufficient but not necessary for Pareto optimality). Steuer and Choo (Math. Programming 26 (1983) 326–344) replaced the weighted sum by a weighted Tchebycheff distance to an ideal point, augmented by a small linear term. Their procedure became one of the standard interactive methods of the field, and the augmented Tchebycheff scalarization is now a standard tool in multiobjective integer programming and in the generation of nondominated sets.
Timeline, as recorded in the paper's own references. Dinkelbach and Dürr (1972) showed, in the linear case, that among the minimizers of a weighted Tchebycheff program there is always a nondominated one (the paper's Theorem 3.1 extends this to the discrete case). Bowman (Lecture Notes in Economics and Mathematical Systems, as cited by the paper) related the Tchebycheff norm to the efficient frontier of multiple-criteria problems. Choo and Atkins (Computers and Operations Research 7, 1980) and Choo's dissertation (1980) developed interactive weighted Tchebycheff algorithms. Steuer and Choo (1983) added the augmentation term , gave an explicit choice of the weights and of in the discrete case, and proved that the resulting program characterizes the nondominated set exactly (Theorem 3.7).
There are objectives to be maximized. The set of attainable criterion vectors is a finite set (in the paper, is the image of a discrete feasible set under the objectives ). A vector dominates if for all and for at least one . The nondominated set consists of the that no dominates.
An ideal criterion vector has coordinates with , where must be strictly positive if (i) more than one nondominated vector maximizes objective , or (ii) the only nondominated vector maximizing objective also maximizes another objective.
Weights range over the simplex . For a scalar the augmented weighted Tchebycheff program is
where is the vector of ones; at a fixed its value is .
For the paper defines weights by (b): , normalized to sum to one, when for all ; otherwise puts weight on the coordinates where and elsewhere. With it sets
For every ,
with from (3.8). One coefficient , computed from and alone, works for the whole nondominated set.
Printed Lemmas 3.2 and 3.3 are false. For and , which is ideal with , the nondominated vector has and , while the dominated vector lies in and has . The proof's second case assumes that only reaches in coordinate , but the -rule constrains nondominated vectors only. The mission states both lemmas with the added hypothesis , under which they hold; the milestone texts are the printed ones. Theorems 3.4, 3.7 and Corollary 3.9 are unaffected, since for , the augmentation term separates from on its own. Hypothesis (a) of the paper also contains the misprint "" for .
Theorem 3.7 says that the augmented weighted Tchebycheff program, with a computable , is an exact scalarization of the discrete multiple objective program. It returns only nondominated vectors (unlike the plain Tchebycheff program, whose optima can be weakly dominated) and it can return every nondominated vector, including unsupported ones (unlike weighted sums). Corollary 3.9 adds that each nondominated vector is the unique optimum for a suitable weight, so it is found even by a solver that stops at the first optimum. These facts underlie the interactive Tchebycheff procedure of the paper's §5 and a large body of later work on generating nondominated sets of multiobjective integer programs.
The results are proved in the paper; to our knowledge none has been machine-checked. The mission produces a checked version with the two lemmas of the paper's proof chain corrected, a precise treatment of the ideal-vector rule, and an explicit . Alternative proofs, for instance one for the goal that avoids the explicit of (3.8), are welcome.
The ⇐ direction is short. The work is in ⇒: the explicit weights must be shown to lie in and to make strictly better than every competitor that is not below it. Both depend on the -rule for , whose role is subtle: it forbids two coordinates of a nondominated vector from reaching , and forbids two nondominated vectors from sharing a coordinate equal to , but it says nothing about dominated vectors. The paper's own argument overlooks exactly those dominated vectors, so a proof that follows the printed Lemma 3.2 literally will fail; the gap is closed only by combining the corrected lemma with the augmentation term. Choosing a single for all of also requires that every quotient in (3.8) be strictly positive.
Criterion vectors are Fin k → ℝ (objective indices ), is a Finset, and is imposed as [NeZero k]. The decision set , the objectives and the program variable are eliminated: the programs are stated over , and is replaced by its minimal value . The programs use without absolute values, as printed; on this equals the metric's when is ideal. " minimizes the program" means that minimizes the value over , and "uniquely minimizes" means that every other element of has a strictly larger value. is Mathlib's stdSimplex ℝ (Fin k).
The ideal vector is encoded with its full -rule, not as " for all "; the latter would exclude the paper's case where touches in one coordinate. The minima in (3.6) and (3.8) can range over empty sets (e.g. ); the paper assigns them no value, and the formalization sets , to then. A value of would make the goal's ⇒ direction false, so no formalization may rely on Lean's default for an empty minimum. Theorem 3.1 is stated for an arbitrary reference vector , since it needs no ideal-vector hypothesis. The paper's "Let be finite" in Theorem 3.7 is taken as " finite", which is what (3.8) and the proof require.
A trivializing formalization would take or leave unconstrained; both are excluded, since is the specific value (3.8) and ranges over .
The definitions (dominance, , ideal vector, Tchebycheff values, , the weights and coefficients of §3) are reusable for the continuous and polyhedral cases of the paper's §4 and for other scalarization results. Contributions of proofs of any milestone are welcome.
A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.
Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).
Let be the feature space with an arbitrary norm , and let labels take the values . The feature-label space is with points . A weight vector acts on features by ; its dual norm is .
Metric (Definition 2). For a weight ,
Changing a label costs ; moving a feature costs its norm distance.
Wasserstein distance (Definition 1). For distributions on , is the infimum of over all couplings of and . The Wasserstein ball of radius is .
Data. Training samples , , define the empirical distribution .
Classifier and risk. Logistic regression models (eq. (1)). The classifier is if and otherwise, and its risk under the data-generating distribution is .
Worst- and best-case risks.
The worst case counts a nonpositive margin, the best case a strictly negative one.
The linear programs. For data , a weight vector and variables , , program (10a) minimizes subject to, for every ,
Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.
For every , , , all samples and every weight vector , both programs attain their minima and , and
The identities hold for each fixed , so they apply to any computed from the data.
equals the minimum of (10a).
If the training samples are i.i.d. from and the radius is such that , then for any sample-dependent
The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with variables and constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.
Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.
The objective is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane or by flipping its label, and the two options interact through the shared budget . Distances to the hyperplane are measured in the given norm and produce the dual norm . The degenerate weight (every point on the hyperplane) must come out correctly without any division by .
The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for ; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding , ; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in , and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with .
The following choices differ from a literal reading of the page:
Swapping the strict and non-strict inequalities in and , restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.
Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.
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.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.
Classifiers trained by standard methods reach high accuracy on image benchmarks and yet change their prediction under perturbations of each pixel that are invisible to a human. Training against such perturbations (adversarial training) improves robustness, but on CIFAR10 and SVHN the robust test accuracy stays far below the robust training accuracy: robust models overfit. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285, 2018) asked whether this gap is a failure of current methods or an information-theoretic fact about the number of samples needed. They introduced two simple data models in which a single sample suffices for standard accuracy and proved that robust accuracy needs many more samples.
This mission formalizes their lower bound for the second model, the Bernoulli model on the hypercube, which was designed to resemble MNIST (whose images are close to binary). In this model the lower bound holds for linear classifiers, and the paper shows separately that a non-linear classifier (thresholding followed by a linear rule) escapes it. The result therefore isolates a concrete way in which the model class, not only the amount of data, governs robust generalization.
Let and . Points are , labels . For a parameter , the -Bernoulli model draws uniformly from and then, independently for every coordinate , sets with probability and with probability (Definition 7). The two classes are noisy copies of the opposite vertices .
The adversary may move a test point anywhere in the ball
leaving the hypercube. The -robust classification error of a classifier is (Definition 3)
A linear classifier is for . A linear-classifier learning algorithm is any function from labelled samples to a weight vector .
The lower bound is Bayesian: is drawn uniformly from , the learner receives independent samples from the -model, outputs , and is charged the robust error of on a fresh sample, averaged over and . The posterior mean measures how much the learner can know about coordinate .
For , , and every linear learner : if
then
The goal keeps the paper's explicit constants (, , ) because Theorem 31 is itself the explicit form of the paper's asymptotic Theorem 9.
With a single sample already yields a linear classifier with small standard error (Theorem 8 of the paper), while Theorem 31 shows that for of order every linear learner needs on the order of samples to get expected robust error below against an adversary (the paper's Theorem 9 states this as for ). The companion upper bound (Theorem 10) shows that thresholding the input first makes one sample enough for any . Together these give a rigorous example in which robust generalization is polynomially harder than standard generalization for a model class, and in which a change of model class removes the gap.
The theorem and its proof are published and not in doubt. The platform holds no statement of this lower bound, of Lemma 29, or of the ℓ∞/ℓ1 robustness criterion for linear classifiers (searched 2026-09-26). The mission produces a checked statement of the result with every hypothesis explicit, including the tie convention and the domain of that the printed statement leaves implicit, and a finite, measure-free encoding of a Bayesian learning lower bound that other hypercube models can reuse.
The obvious attempt bounds the robust error of the best classifier the learner could output, but the learner is arbitrary: it may output any , including ones that use the samples in unusual ways. The argument must therefore hold for every function of the samples, which is why is random and why the error is averaged over it; for a fixed the learner is robust and the statement is false. The technical difficulty is to pass from "the posterior of every coordinate is nearly uniform" (a statement about separate one-dimensional problems) to a bound on the margin relative to that holds for every at once, uniformly in how spreads its weight across coordinates. Concentration of is not available for a general (a single heavy coordinate defeats it), so only a weak, constant-probability tail bound survives, which is why the final error is rather than close to .
Everything is finite. Hypercube points are sign vectors Fin d → Bool, labels are Bool with true ↦ , and every probability is an explicit finite sum of weights; no measure theory is involved. is EuclideanSpace ℝ (Fin d). Committed conventions:
The learner is any function of the samples to ; restricting to a specific learner, fixing , letting the learner output an arbitrary classifier (for which the theorem is false), or bounding only the standard error () would each trivialize or falsify the target and are excluded. Useful infrastructure: Hoeffding's inequality for sums of independent variables, Markov's inequality over finite sums, and the ℓ∞/ℓ1 duality on EuclideanSpace. Related platform work: the other three missions of this series (the Gaussian lower bound, the Gaussian robust upper bound, and the Bernoulli thresholding upper bound). Contributions of general lemmas on finite product measures over the hypercube are welcome.
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.
Many 0–1 optimization problems can be written as linear programs over the convex hull of the 0–1 points of a polytope, but that hull usually has no manageable description by inequalities. Lift-and-project methods approximate it by a sequence of convex sets. Each set comes from a linear or semidefinite system in more variables, followed by a projection. Lovász and Schrijver introduced the operator in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim. 1(2), 1991). For any polytope in the unit cube, rounds of reach the 0–1 hull (their Theorem 1.4), and each round keeps linear optimization tractable.
The stable set problem is the paper's main test case, and the question is quantitative: how many rounds does a given valid inequality need? Section 2.c answers it with a single number read off a linear program. Later work on the rank of lift-and-project hierarchies uses this measure: Balas, Ceria and Cornuéjols's lift-and-project cuts (1993), the Sherali–Adams and Lasserre comparisons of Laurent (2003), and the rank lower bounds for stable set relaxations in the decades since.
Let be a finite graph with no isolated nodes, which is the paper's standing assumption for Section 2. For let be its incidence vector.
Homogenize with a new coordinate . Let be the cone spanned by the 0–1 vectors with , and let be the cone given by and . For a convex cone with polar cone , the matrix cone is the set of symmetric matrices that satisfy two conditions:
The operator is . Its iterates are and . On the graph side, , so and for every .
Let be valid for , with and . Two numbers are attached to it:
For a node with neighbourhood , the deletion of zeroes . The contraction of zeroes on and lowers the right-hand side to .
For every such inequality with defect and N-index ,
formalized as and . The goal holds for every graph without isolated nodes and every valid inequality with nonnegative integer coefficients and nonnegative defect.
Corollary 2.8. Let have nodes, stability number and graph N-index . Then
Theorem 2.13 turns the N-index, which is defined through an infinite family of matrix-cone projections, into a quantity computable by one linear program over . Some consequences:
The result is proved in the paper; the mission's work is to formalize it. Nothing on Prove2Me or in Mathlib covers stable set polytopes, the Lovász–Schrijver operator or its index, and no machine-checked version of Theorem 2.13 is known. A formal proof would give the first verified rank bound for a lift-and-project hierarchy. It would also build a reusable library for , , half-integrality of vertices, and the operator.
The upper bound is an induction on the defect, and it needs several facts about :
The last is the heart of Lemmas 2.11 and 2.12. The induction also climbs through for every , so Lemma 2.2 must hold for an arbitrary closed convex cone inside , not only for polytopes given by inequalities.
The lower bound is where the obvious argument fails. The printed proof tests at and obtains . That equals only when , which Lemma 2.10 gives for facets alone. For a general valid inequality can exceed , so the uniform vector does not suffice. The theorem is stated, as printed, for every valid inequality, and a complete proof must supply the missing step.
Option V, with none as . Graphs are finite SimpleGraphs with the hypothesis that every node has a neighbour.IsGreatest and IsLeast hypotheses, so no default value such as can make a statement vacuous.The work needs half-integrality of , Lemma 1.3 of the paper () and monotonicity of . Each of these is reusable and welcome as a separate contribution.
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 jobshop is a factory in which each job visits a sequence of machine groups, the sequence differing from job to job. J. R. Jackson's 1963 paper Jobshop-Like Queueing Systems (Management Science 10(1), 131–142) models such a shop as a network of queues and computes its long-run distribution of queue lengths in closed form. It generalizes his 1957 paper Networks of Waiting Lines (Operations Research 5(4)), which treated Poisson arrivals and multi-server centers, to arrival rates that depend on the total number of customers present and service rates that depend arbitrarily on the local queue length. The resulting product-form equilibrium is the starting point of queueing-network theory, which is used in performance analysis of manufacturing systems, computer systems and communication networks.
Timeline:
There are service centers, Center . A state vector has non-negative integer components, being the number of customers at Center , and . The system is given by:
The paper's standing Assumptions (2.1)–(2.4): (2.1) either all , or exactly for ; (2.2) and for ; (2.3) each row is a probability distribution; (2.4) the traffic equations
have a unique solution, and it is non-negative.
The process is defined by its transition probabilities over a short interval (p. 134), from which the paper derives the balance equations (3.1) for . An equilibrium state probability distribution is a probability distribution on state vectors such that solves (3.1). With
the constant is when the series converges and otherwise.
If , then
is an equilibrium state probability distribution; and if the arrival rates are bounded, it is the only one. The goal fixes no constants; the condition is the paper's.
Theorem (6.3) in its case , : with constant arrival rate and for every , the equilibrium is , being the normalized .
Theorem (4.5) states that the queue lengths of a whole network have an explicit stationary law, determined by the routing only through the visit ratios , and that conditionally on the total it does not depend on the arrival process. With constant arrival rate it factorizes into independent one-center laws (Theorem (6.3)), each that of a single queue fed at rate ; this is the form in which Jackson networks enter textbooks. State-dependent arrivals cover systems with balking or finite capacity: taking for caps the population.
The result is classical and proved; it has no machine-checked proof on this platform. The platform has Kelly–Yudovina's open migration process (KellyStochasticNetworks.open_migration_equilibrium): constant external arrivals, no self-loops, a full-balance conclusion without uniqueness. It is the companion (6.3) in substance but not the general theorem: arrival rates depending on the total population are not in it. This mission contributes the state-dependent model, a stationary form of Jackson's own equations (3.1), and a uniqueness statement.
The balance equations are an infinite system in . Substituting (4.6) gives terms with shifted states, guarded by non-negativity of components, a double sum over ordered pairs of distinct centers, self-loops appearing only in the outflow factor , and centers with , where vanishes. Checking each state term by term against the traffic equations requires the diagonal of (2.5), excluded in (3.1), to be handled exactly. Summing (4.6) to one requires regrouping a series over by the finite fibres of .
Uniqueness is the hard part. The paper gives no proof: footnote 5 refers to a limit theorem for Markov processes and to the communication structure of non-transient states. A solution of the algebraic balance equations need not be the stationary law of the process when the process can explode, and the model allows explosion with (e.g. , , ). Uniqueness therefore depends on non-explosion as well as on the communication structure of the states, and neither is addressed on the page.
Centers are Fin N with ; states are Fin N → ℕ; rates are real. The routing is one function r : Option (Fin N) → Option (Fin N) → ℝ, where none is the index in the first argument and in the second. A structure JobshopSystem N bundles with Assumptions (2.1)–(2.4) as fields; is a parameter satisfying (2.5), uniqueness and non-negativity, not a formula. Balance sys q k is the stationary equation (3.1) at k for an arbitrary q, and IsEquilibrium sys q is , HasSum q 1, and Balance at every state. is defined with an explicit if Summable … then … else 0.
Explicit choices, each stated in the item where it applies:
Correction of (3.1). The paper prints the arrival outflow as :
Its transition probabilities (p. 134) give , since an arrival with an empty routing leaves the state unchanged. The two agree only when , and with the printed coefficient Theorem (4.5) is false (, , , constant rates, at ). The formalization uses the coefficient the transition probabilities give. It does not assume : the paper allows empty routings.
Uniqueness under bounded arrival rates. Uniqueness (milestone 4 and the goal's second conjunct) assumes . The paper asserts uniqueness without proof, citing a limit theorem for regular processes; bounded arrival rates make the process regular and hold for every example in the paper. Existence and the formula carry no added hypothesis.
Companion (6.3). System of §5 is not formalized in the paper and not here; only its case , is stated.
A trivializing formalization is ruled out: Balance and IsEquilibrium are stated for an arbitrary function on states and never mention , or , and equilibrium is neither defined as (4.6) nor as detailed or partial balance.
Useful infrastructure: summation over Fin N → ℕ grouped by total (Finset.Nat.antidiagonalTuple), and a non-explosion and uniqueness theory for countable-state continuous-time chains, which is reusable beyond this mission. Not included: the limit , which needs a construction of the process; the equivalence of (2.4) with finiteness of routings; Theorem (5.5) and (5.7)–(5.9).
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.
Let be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can be?
The answer is .
Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.
The hypothesis is a graph condition in disguise. Join to when ; then "among any three some two are orthogonal" says that graph is triangle-free.
The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of that the argument uses.
State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.
google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.
The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need at all.
Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.
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.Pattern search methods minimize a function by comparing values of at points of a structured set of trial points, without evaluating or approximating derivatives. Coordinate search and the method of Hooke and Jeeves (Hooke–Jeeves 1961) are the classical members of the family. Such methods remain in use when derivatives are unavailable, unreliable or expensive, for instance when is the output of a simulation, and practical problems of this kind usually carry simple bounds on the variables.
Torczon (SIAM J. Optim. 1997) gave a global convergence theory for pattern search on unconstrained problems: under compactness of the level set and continuous differentiability of , , and under stronger hypotheses . Lewis and Torczon extended this theory to bound constrained problems (ICASE Report 96-20, 1996; SIAM J. Optim. 1999). The extension is not automatic: the paper exhibits a pattern search method for unconstrained problems (Box's evolutionary operation with factorial designs) that fails on bound constrained ones, and identifies the structural condition on the pattern that restores convergence.
Timeline.
The problem is
with vectors of extended reals and for every ; or is allowed. The feasible region is , is the coordinatewise projection onto , , and is the feasible level set. A stationary point is an with for all . The stationarity measure is
which vanishes exactly at stationary points.
A generalized pattern search method is fixed by a nonsingular basis matrix , a finite set of nonsingular integer matrices, a rational , an integer and nonnegative integers . At iteration the generating matrix is with , an integer matrix containing a zero column, and diagonal. A trial step is for a column of . The step is a trial step with , and it must decrease whenever some feasible trial step from the core does. The iterate moves, , exactly when . The step length is multiplied by after an unsuccessful iteration and by some after a successful one. The Strong Hypotheses additionally require to be no larger than the best feasible core trial value whenever that value is below .
If is compact, is continuously differentiable, the columns of the are uniformly bounded, , and the Strong Hypotheses hold, then
Theorem 3.2 shows that a method which never computes a gradient still has a subsequence approaching first-order stationarity for the bound constrained problem, even though it cannot enforce a sufficient decrease condition measured by the projected gradient. Theorem 3.3 upgrades this to the whole sequence, so every limit point of the iterates is a KKT point. These results justify the bound constrained variants of coordinate search and Hooke–Jeeves discussed in §5 of the paper, and they are the template for the later theory of pattern search under linear constraints and generating set search.
The results are proved in the paper, and three of the milestones are proved in Torczon (1997). None of them has a machine-checked proof. Formalizing them produces a Lean model of generalized pattern search (patterns, exploratory moves, step-length updates) that later missions on direct search, mesh adaptive direct search or linearly constrained pattern search can reuse, and checks the details the paper handles briefly: the lattice argument, the feasibility of the chosen coordinate step, and uniform constants.
The obvious argument copies the unconstrained proof with replaced by . The step that fails is the existence of a good trial step: in the unconstrained case some pattern direction makes an acute angle with , but near the boundary of that direction may leave the feasible region, and a feasible direction may not be a descent direction. For a general pattern no uniform choice exists, and the paper's counterexample in §5.2 shows convergence can fail. The diagonality of is what makes the pattern contain coordinate directions, one of which is both feasible and a descent direction of quality (Proposition 4.2). The second difficulty is Theorem 4.5, which uses no derivatives: it rests on the rationality of and the integrality of the , which confine the iterates to a lattice that meets the compact set in finitely many points.
Points are EuclideanSpace ℝ (Fin n) with the Euclidean norm; the bounds are Fin n → EReal with the hypothesis for all , so infinite bounds are allowed as in the paper. Paper coordinates are Lean's Fin n. The gradient is Mathlib's gradient f. A run of the method is a structure of sequences together with a predicate IsGPSRun that encodes §2.1–§2.4 clause by clause; the parameter is the number of columns of (the paper's ). is rational and the are integer matrices, as the lattice argument requires. "" over the finite set of feasible core trial points is encoded as "some feasible core trial step strictly decreases ". statements are encoded with ∃ᶠ, not Filter.liminf. The modulus of continuity is not formed as a real supremum; Proposition 4.1 takes an explicit radius .
Standing assumptions and every departure from the page:
The run predicate is not vacuous: an explicit run of coordinate search on over satisfies IsGPSRun, the Strong Hypotheses, bounded columns, and compactness of . That check is proved in Lean without sorry, so the goal cannot be closed by exhibiting an unsatisfiable hypothesis.
A complete development needs the mean value theorem along segments, uniform continuity of near the compact set , finiteness of a discrete lattice inside a compact set, and elementary facts about the coordinatewise projection. The projection and lattice lemmas are reusable beyond this mission. Proofs of any milestone, alternative proofs, and a general statement of Proposition 3.1 for closed convex are welcome.
Large combinatorial structures are often best understood through their limits. For dense graphs, Lovász and Szegedy (2006) showed that every sequence of graphs whose subgraph densities converge has a limit object, a graphon, and that every graphon arises this way. Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) related this convergence to the cut distance. These results turned questions of extremal combinatorics and property testing into analysis on a compact space.
Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) carried this programme over to permutations. Their limit objects, called limit permutations here and now usually called permutons (as a probability measure on the square), underlie later work on quasirandom permutations, pattern densities, and property testing of permutations (Hoppen et al., 2011). This mission formalizes the paper's main result, Theorem 1.6: convergent permutation sequences have limits, and every limit is attained.
Timeline:
For , is the set of permutations of , and for . For and , the number of occurrences counts the increasing -tuples in with . The subpermutation density is for and for . A permutation sequence is convergent if converges for every fixed .
A function is a cdf if it is non-decreasing and right-continuous with and . A limit permutation is a Lebesgue measurable such that is a cdf for every , and for every . The set of limit permutations is .
With one associates a random point : , and given , has cdf . Draw independent copies . The -random permutation records the relative order of the read in increasing order of the . The density of in is . A sequence with converges to , written , if for every .
For , the step limit permutation spreads the permutation matrix of uniformly over its grid cells. The rectangular distance is the largest difference, over axis-parallel rectangles, between the probabilities the two associated random points assign to the rectangle.
The two parts together identify with the set of limits of permutation sequences.
In the order the proof uses them:
Theorem 1.6 makes , modulo null sets, the completion of the set of finite permutations under density convergence. Asymptotic statements about pattern densities, such as quasirandomness criteria, extremal pattern-density problems and the testability of permutation properties, can then be stated and proved on a compact space of measures rather than along sequences. Lemma 4.2 is the quantitative sampling statement behind testability, and Theorem 1.7 says that a limit, viewed as a measure on the square, is unique.
The results are proved in the paper and have been used for over a decade. To the best of current knowledge they are not formalized in any proof assistant. The mission produces a machine-checked account of the permuton correspondence: the definitions of subpermutation density, limit permutation and -random permutation, and the equivalences between the three natural convergences on . Alternative proofs are welcome, for instance of (ii) through Lemma 4.2 and the Borel–Cantelli lemma rather than the paper's strong law for U-statistics.
The obvious route to (i) is compactness: the laws of the random points attached to have a weakly convergent subsequence. The weak limit is only a measure, however. Turning it into a function that is a cdf in for every , with exact uniform integrals for every , requires a regular conditional distribution (Lemma 2.2). One then has to show that weak convergence carries the pattern densities along. That fails for general measures on the square, because the events defining have boundaries on which ties occur. Uniform marginals are what rule the ties out. The limit must also be independent of the subsequence, which needs the uniqueness statement Lemma 5.1. For (ii), the natural random sequence converges only almost surely, so an almost-sure limit theorem or a quantitative concentration bound is unavoidable.
unitInterval with Lebesgue measure. A limit permutation is a curried real function Z : I → I → ℝ. Measurability is almost-everywhere measurability for the product measure, which is Lebesgue measurability. The cdf and integral conditions hold for every and every .Equiv.Perm (Fin n) (0-based), and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n). Patterns of every length, including the trivial length , are quantified over; the length- clause always holds.Needed infrastructure includes Prokhorov compactness of probability measures on a compact space, the Portmanteau theorem, conditional cdfs (ProbabilityTheory.condCDF), Hoeffding's inequality and Borel–Cantelli, all largely in Mathlib. The permutation-density and permuton layer is reusable for quasirandomness and testing results. Mission II of this series, on the rectangular-distance characterization, uses the same model.
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 fitting is a standard tool in estimation, identification and data analysis, and its data , are rarely known exactly. El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl. 18(4), 1997) proposed to choose to minimize the worst-case residual over a set of admissible data perturbations. Earlier missions of this series treat unstructured perturbations of and perturbations affine in a parameter vector. §5 of the paper covers a more general model, taken from robust identification (Doyle et al.): the perturbed data depend on an uncertain matrix through a linear-fractional transformation. This form covers rational dependence of the data on uncertain parameters, max-norm bounds on independent parameters, and data matrices with some columns known exactly (pp. 1046–1047).
In this generality, deciding whether the worst-case residual is finite is NP-complete, and computing it is NP-hard even when the dependence is affine (§5.3, Lemma 5.1). Theorem 5.2 gives the tractable replacement: a semidefinite program whose value bounds the worst-case residual from above, and equals it when the perturbation is unstructured. The main tool is a structured form of the S-procedure. Robust control uses the same tool, with the scalings and below, to bound the real structured singular value (Fan, Tits and Doyle, 1991).
Vectors carry the Euclidean norm . For a matrix , is its largest singular value (operator norm between Euclidean spaces). Let be a linear subspace of (the perturbation structure), and fix , , , , , . For with the perturbed data are
With the normalization (the paper's, with no loss of generality), the worst-case residual of is
if for every such , and otherwise (35). The commutant scalings are and (37). The SDP constraint is
For all and :
Part (a) says the value of the SDP (40) is an upper bound on . Part (b) says this upper bound is exact for full perturbations, including the case , where (40) is infeasible.
The worst-case residual under linear-fractional uncertainty cannot be computed efficiently unless P = NP. Theorem 5.2 gives an SDP-computable upper bound with an explicit certificate . Since enters (38) linearly, the same constraint can also be optimized over (Theorem 5.3, not part of this mission). For the bound is exact, which covers the model and, as a special case, the unstructured problem of §3.
The results are proved in the paper (the proof of Theorem 5.2 is only indicated, through Appendix C). No machine-checked version of these statements, of Lemma 2.2 or of the structured S-procedure with commutant scalings is known. The formalization also fixes the statements. As printed, Lemma 2.2's "only if", Lemma 2.3 and the upper bound of Theorem 5.2 are each false in a boundary or structural case (see Formalization scope). The corrected forms stated here are the ones the paper's proofs support.
Part (a) reduces to robust positivity of a linear-fractional matrix function, and the difficulty is the inverse . The certificate is one LMI in which does not appear, while the conclusion is about a rational function of over a whole structured ball. The certificate also has to guarantee that is invertible everywhere on that ball, and not only that the residual is small where it is defined. Evaluating at a single point does not show this. Part (b) needs a lossless S-procedure in its strict form. The standard (non-strict) S-lemma gives only , and the gap between strict and non-strict inequalities is exactly where the printed statements fail. The degenerate case is not covered by the S-lemma's regularity condition and has to be handled separately.
Fin n, Fin m, Fin N; is a Submodule ℝ (Matrix (Fin N) (Fin N) ℝ), with as ⊤. The Euclidean norm is written out, because ‖·‖ on Fin n → ℝ is the sup norm. is the operator norm of Matrix.toEuclideanLin Δ, the largest singular value.ResidualBelow: every with has and residual . It is false for every when . No real-valued supremum is used, so the branch of (35) cannot turn into a default . Matrix inverses are Mathlib's Matrix.inv, and every use carries the determinant condition.ConvexOptimization.s_procedure, in a different sign convention), square roots of positive definite matrices that commute with , and compactness of the structured unit ball. The S-procedure lemmas are reusable in robust control and trust-region analysis. Proofs of the milestones in any order are welcome.