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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix that is never formed explicitly: may be an inverse, a matrix function , or a product of large operators, and the only affordable access is a routine that returns for a given vector . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors , and average the quadratic forms , each of which costs one matrix–vector product.
Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples guarantee relative error with probability . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).
Let be symmetric positive semi-definite, with eigenvalues and rank . Write for the largest eigenvalue and
defined for ; it is the condition number of on its range.
A normalized Rayleigh-quotient trace estimator of with samples is
where are independent random vectors in with and for each (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( entries, i.i.d. uniform) and the vectors with uniform are instances.
A random variable is an -approximator of if
(Definition 4.1).
For every nonzero symmetric positive semi-definite , every , , and every normalized Rayleigh-quotient estimator of ,
The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is , independent of . For ill-conditioned matrices the bound degrades with , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).
The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.
Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event must be rescaled to a statement about the sum . A naive attempt that fixes a particular distribution for the (Rademacher, say) proves a different, narrower theorem and does not settle the goal.
Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. is lambdaMax (the maximum eigenvalue) and is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. is a placeholder, and every statement assumes .z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each measurable, the family mutually independent (iIndepFun), almost surely, and . The estimator is universally quantified over this class. Unbiasedness is required for the given only, as on the page. Probabilities are P.real of events; is a natural number and is (M : ℝ)⁻¹.IsNormalizedRayleighSample.Cost and benefit allocation problems arise whenever several parties share a joint undertaking: towns building a common water supply, divisions of a firm sharing overhead, users of a multi-purpose reservoir. They are modelled as cooperative games, and a rule that divides the joint value among the players is an allocation procedure. The standard such rule, the Shapley value, was characterized by Shapley (1953) through efficiency, symmetry, a dummy axiom and additivity. Additivity (the allocation of a sum of two games is the sum of the allocations) is a mathematical convenience with little direct appeal in applications, and it has been the most criticized of the four axioms.
H. P. Young's paper Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985) studies allocation procedures through monotonicity: how a player's allocation should respond when the game changes. Its Theorem 1 shows that the core is incompatible with coalitional monotonicity for five or more players (the subject of the sister mission of this series). Its Theorem 2, the subject of this mission, shows that efficiency, symmetry and a single monotonicity axiom — strong monotonicity — determine the Shapley value, with no additivity axiom at all. The result is widely cited as Young's axiomatization of the Shapley value, usually in the form with the marginality condition (7) that the paper states in its remarks.
Timeline:
Fix and the player set . A game is a function on the coalitions with ; superadditivity is not assumed. An allocation procedure is a map assigning to each game a vector with (efficiency).
The marginal contribution of player to coalition (Eq. (3)) is
defined for every . The Shapley value is
The axioms:
A primitive game () takes the value on coalitions containing and elsewhere.
For every map from games on to ,
Both directions are part of the goal: the Shapley value has the three properties, and it is the only map that has them.
Efficiency and symmetry of the Shapley value are supporting theorems of the existence half; the paper uses them without separate statement.
The result. Theorem 2 shows that additivity is not needed to single out the Shapley value: a player's payoff is pinned down by symmetry, efficiency, and the requirement that it respond monotonically to that player's own marginal contributions. This gives the Shapley value a justification that can be checked directly in applications — a division that improves its marginal contributions to every coalition is never penalized — and the marginality form (7) is the standard starting point for characterizations on restricted classes of games and for extensions to games with a variable player set.
The formalization. The theorem is proved and classical; no machine-checked proof of it is known to exist. The mission produces a checked proof of Young's characterization together with reusable infrastructure: marginal contributions, the unanimity-game basis of the space of games (a Möbius-inversion statement on the subset lattice), the Shapley value on unanimity games, and the Shapley value's efficiency, symmetry and monotonicity for the published ShapleyValue definition. These are the ingredients of most other axiomatizations of the Shapley value (Shapley 1953, Hart–Mas-Colell's potential) and are useful beyond this mission.
The existence half is a direct computation. The uniqueness half cannot proceed by linearity, since is not assumed additive: knowing on each primitive game says nothing directly about on their sum. The obvious idea — decompose into primitive games and add up — therefore fails. What must be controlled instead is how much of a game each player "sees" through the marginal-contribution vector alone, and how symmetry and efficiency distribute what remains. The formal proof also has to manage the dependence of the argument on a minimal-length expression (9) while keeping all comparisons inside the class of games with .
Fin n: the paper's player is the Lean index . The player set is fixed, and is a single map Game n → Fin n → ℝ, as in the paper; no lower bound on is needed (at both sides of the goal hold).Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. The normalisation is essential: on arbitrary set functions a constant game would receive per player from every efficient symmetric procedure, but from the Shapley formula, and Theorem 2 would be false.Supermodularity.Cooperative.ShapleyValue, written as a sum over with weight ; it agrees term by term with the formula above.Contributions welcome: proofs of the milestones in any order, general lemmas on unanimity-game expansions over Finset powersets, and alternative proofs of the uniqueness half.
Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.
A packet network with fixed routing (Section 12.6) has I packet classes; each class i
routes, after one hop of processing, deterministically to a single successor class or exits the
network — encoded here as a function . The K
links are indexed by , and a matrix assigns each class to the single link its next
transfer uses; denotes the classes belonging to link . At the start of a
timeslot, is the vector of class-level packet counts and the
corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book):
(a) solve the concave program (Eq. 12.57), where is the finite set of feasible link configurations
and its convex hull; (b) randomize a link configuration with mean ;
(c) transfer packets over link ; (d) select which packets to transfer uniformly
at random from each link's queue. This makes a discrete-time
Markov chain. The function is exactly the proportionally fair (PF) allocation function
of Section 10.1, applied here with the link-level demand vector in place of the PF model's
job-class demand vector.
Here is the vector of external arrival rates, the resulting vector of total (external plus internally routed) arrival rates into each class, and the input-output matrix determined by . The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.
Lemma 12.23 is an almost-sure convergence result for a residual process tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to . Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of .
The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.
Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no
relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction:
rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the
RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so
that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b)
a direct instance of this mission's own Theorem 12.27. This is the payoff the whole
proportional-fairness apparatus (missions IX-X) was built for.
The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a
class-indexed process , while the chapter's own general fluid-equation machinery
(Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that
matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own
fixed-routing model, however, the book's remark that " ... is an I-vector of actual
packet transfers by class" (page 245) collapses this distinction: each class has a single
associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid
model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4)
already uses. Missing this identification is the natural way to get stuck restating Proposition
12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty
is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference
sequences as an external fact rather than deriving it, so a faithful statement must commit to an
explicit representation of "martingale difference sequence" (a filtration and Mathlib's
Martingale predicate) even though no full measure-theoretic construction of the underlying
probability space is attempted.
Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's
deterministic routing successor (none meaning exit), and the resulting input-output matrix
and routing matrix are derived from it rather than taken as independent data (this chunk
verifies , the identity Proposition 12.26's reduction to the PF model relies on).
The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated
verbatim from mission IX, and the general packet-network fluid equations restated from mission
XII, since concurrently-drafted chunks in this series never import one another's Lean files even
within a shared sub-namespace. The formalization does not admit a trivializing reading: the load
condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible
configurations (not weakened to or to a single configuration), RPSFluidStable quantifies
over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is
stated as a two-sided equivalence, not a one-directional inclusion that would understate "special
case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's
martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit
argument (mirroring mission XII's own Theorem 12.13 proof).
Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.
This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.
The season is . Customers arrive as a Poisson process with rate , so is the expected number of arrivals in the season. Every customer has base valuation , and a customer's valuation at time is for a fixed decline parameter (equivalently with ; is the fraction of the valuation left at the end of the season). In the paper's notation this is the case , , of a family of Gamma-distributed base valuations with mean and coefficient of variation ; the tail of the base valuation is for and otherwise.
The seller posts a premium price on and a discount price from the discount time on, and has unlimited inventory. A myopic customer arriving at buys at once iff ; otherwise the customer waits and buys at iff . A customer arriving after buys iff the current valuation is at least . The expected numbers of buyers in the three groups are the segment rates , and , and the expected revenue is
For a price let , the time at which the valuation has fallen to , and write , . The reduced objective is
every maximizer of together with every with attains , and, if , the maximizer is unique,
and every with is optimal.
For :
Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on at all. The paper uses it as the benchmark against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.
The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.
The revenue is defined through integrals of a step function of time, and the reduction to needs these integrals evaluated in every configuration of , and , including prices above (nobody buys) and below (everyone buys, at a needlessly low price). The paper's proof covers only and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when , and boundary points of the region must be excluded.
Everything is over . Logarithms are Real.log, powers are real powers, the segment rates are interval integrals ∫ t in a..b of the tail , and with . The model definitions (, , and the revenue) are stated for a general tail , decline factor, season length and discount time and then specialized.
The following readings of the paper's words are fixed:
IsGreatest of the set of attainable revenues.The decimals and are not stated. A formalization that restricted prices to in the revenue maximization, or that fixed in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside .
Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision and a parameter with objective to be maximized, the robust problem around a nominal parameter with a deviation set is
When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix and solve the same problem over the shrunken set . The heuristic is easy to implement, but the meaning of the set is unclear, and it has lacked a justification.
Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.
Let carry the Euclidean norm and its Borel -algebra, and let be the set of Borel probability measures on . Let be any set of decisions and . Fix , a deviation set , and . Write .
The two-scenario set is
A distribution in describes a system that is, with probability at least , in a normal state where the parameter equals , and otherwise in an abnormal state where the parameter deviates by an element of . The DRSP value of a decision is .
Two further quantities enter. The radius of the deviation set is . The curvature bound is a constant with
where is the Hessian of at and is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.
If is twice differentiable with for all , then for all
Corollary 4.2 (p. 104): if every is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if is star shaped, every is convex with and has Hessian bounded by , then the shrunken value lies between the DRSP values over and , where requires only .
The result gives a physical meaning to the parameter of the shrinkage heuristic: is a lower bound on the probability that the system is in its nominal state. The error vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.
Two points need care. First, the step from the Hessian bound , a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of .
is EuclideanSpace ℝ (Fin m) with its Borel -algebra. Measures are Measures, and membership in includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.
The formalization makes the following readings explicit:
The Lean functions drspValue and devRadius return on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped would make the inequalities hold or fail for the wrong reason and is ruled out.
Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.
Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).
In data-driven problems the situation is different: the parameters are samples, and all of them lie in the same space . Robustifying each sample by its own uncertainty set gives the objective , and the sets typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on itself rather than on . This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.
Let and write . Let be the set of Borel probability measures on . The data are:
For write and . The distribution set is
Each must give every union of uncertainty sets at least the total weight of its indices. For the expectation is the extended integral .
as an identity in , with no boundedness assumption on and no disjointness assumption on the .
The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space . This is what allows distributions in to be compared with the true data-generating distribution as grows: in §3 of the paper a kernel density estimator is shown to lie in for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.
Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.
The inequality from the left side is the easy half: point masses with belong to . The substance is the reverse bound, that no can do better than . For disjoint sets this is immediate, since . For overlapping sets a measure may place mass in intersections, and a single point of can serve several indices at once; the constraint family over all subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded , infinite integrals, infima equal to ) must also be handled rather than assumed away.
Fin m → ℝ with its Borel -algebra; no norm is used. Indices are Fin n, subsets are Finset (Fin n), and is Finset.Iic i.Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, and included.expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, . The Bochner integral is not used, because its value on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set .Model): the set , the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.Statistical learning theory asks when the empirical frequencies of a whole class of events converge to their probabilities uniformly over the class. Vapnik and Chervonenkis answered this question in 1971 (Theory Probab. Appl. 16 (1971) 264–280) by attaching to every class of sets a single combinatorial quantity, the growth function, and bounding the probability of a large uniform deviation in terms of it. For that bound to be useful, the growth function must grow more slowly than an exponential. The first result of the paper, Theorem 1, shows that the growth function of any class is either exactly or bounded by a polynomial. This dichotomy is the reason finite VC dimension (the size of the largest fully shattered sample) became the central complexity measure of learning theory.
Timeline of the combinatorial core:
Let be a set and a collection of subsets of . A sample of size is a finite sequence of elements of ; repetitions are allowed. Each induces in the sample the subsample of the terms that lie in , which is determined by the set of positions .
The index is the number of different subsamples induced by the sets of , i.e. the number of distinct sets of positions with . It is at most . The growth function is
the maximum over all samples of size . For the rays on the line ; for the open subsets of , .
The function on pairs of natural numbers is defined by the recurrence (1) of the paper,
In the Lean development these are index S x for x : Fin r → X, growthFunction S r, and Phi n r in the namespace VapnikChervonenkis.GrowthFunction.
For a nonempty class , either for every , or, with the first value of at which fails,
The exponent is pinned down by minimality: and for every .
Theorem 1 converts the distribution-free bound of Theorem 2 of the same paper into a convergence statement: whenever the growth function is not identically , the right-hand side is a polynomial times a decaying exponential, so relative frequencies converge to probabilities uniformly over . The same dichotomy underlies sample-complexity bounds for PAC learning, covering-number bounds for VC classes, and the notion of VC dimension itself; the exponent is the VC dimension plus one.
The results are classical and proved. Mathlib contains the Sauer–Shelah lemma for finite set families (Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean). The platform has several open formal statements of Sauer's lemma for growth functions over finite point sets (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah) and a closed form for Kearns–Vazirani's (ComputationalLearning.phi_closed_form, the same recurrence). No statement of Theorem 1, and none over the paper's sequence model of samples, is formalized. This mission formalizes the paper's own route: Lemma 1 in the paper's form, the polynomial bound on , and the dichotomy with the minimal exponent. It also provides the growth function over sequences that the companion missions (Theorem 2, and the entropy criterion Theorem 4) are stated with.
The obvious argument has two steps: bound by whenever no subsample of size is fully split, then bound by . The first step is the Sauer–Shelah lemma, and it does not follow from counting alone. A class can induce many subsamples on points without inducing all on any fixed of them, and no counting of subsamples one position at a time rules this out. The second step is elementary but must hold uniformly for all , including , where and the bound uses .
Samples are sequences, not sets. With repeated points, two positions carrying the same point can never be separated, so Lemma 1 must be applied to position sets rather than point sets. Transferring Mathlib's set-family lemma to this setting is a bookkeeping step that does not reduce to a citation.
x : Fin r → X with positions ; repetitions are allowed. A subsample of size is x ∘ e with e : Fin n → Fin i strictly increasing.index S x counts distinct Finset (Fin r) of positions {i | x i ∈ A} with A ∈ S. Counting point sets A ∩ {x_1, …, x_r} instead would be a different object when points repeat; the growth function over finite sets of points (as in ComputationalLearning_VC) differs from when has fewer than elements.growthFunction S r is the supremum in ℕ of index S x over all samples; the family is bounded by , so it is a maximum. When is empty and its value is ; exactly when is nonempty.Phi is defined by the recurrence (1). The paper introduces as the maximal number of components into which hyperplanes cut -space; that geometric identity (Example 3) is not part of this mission.No measure, σ-algebra or probability appears: the class is an arbitrary collection of subsets of a bare type. Needed infrastructure: basic API for index (monotonicity in the sample, behaviour under restriction to a subsample) and a bridge between samples and Mathlib's set families (Finset.Shatters, Finset.vcDim). Both are reusable by the two companion missions of this paper, and contributions of either are welcome.
Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping rows for basic integer variables , dropping the nonnegativity of (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of with . Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.
Fix , a point and a linear subspace , and assume that the affine space contains an integral point. Products such as are standard inner products.
A function is sublinear if for and .
with on and a maximal lattice-free convex set in with in its interior.
The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on or .
In the order in which the proof on pp. 15–21 uses them:
Theorem 3 says that the minimal valid inequalities of are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull . It also says that for irrational , where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.
The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.
For rational data every valid inequality can be written with right-hand side and nonnegative coefficients, and is then the gauge of . For irrational this fails. Since , adding to changes nothing on , so coefficients can be negative, and may have a full-dimensional recession cone. A maximal lattice-free set containing then yields a that need not lie below (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within . This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.
EuclideanSpace ℝ (Fin q), is a Submodule, and is W →₀ ℝ. The printed phrase "the set has finite cardinality" is read as ordinary finite support.The paper is imprecise in three places, and the formalization departs from the page in each:
Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.
Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).
A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, ), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.
The two-station, five-class re-entrant network's fluid model is globally stable if and only if
The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.
Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.
The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.
Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station"
(q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to
this material; this mission is a from-scratch formalization of global stability at both the
Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class
re-entrant line, and the assembly-with-side-business network.
Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible pairs with a wedge region, then separately solves an analogous system for — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.
Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload
operator are restated locally (drafts in this series do not import one another), as is mission
VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable,
even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly
over an uninterpreted policy type and two predicates, since the concrete "simply structured
non-idling policy" and "positive recurrence under a policy" notions belong to mission I's
apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a
structural property of an ordinary flat-indexed queueing network (a partial successor function
encoding the deterministic route) rather than by re-introducing the book's own two-index
type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is
representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2
serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not
read off Figure 8.3 directly, though the two are cross-checked as consistent. The
assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter
2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations
(8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare
↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's
instability construction — a formalization that dropped either direction of the iff, or that
conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing
graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable,
IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/
reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the
six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery
this mission does not otherwise build — are welcome.
Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.
A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator (Eq. 8.24) gives, for any buffer-contents vector , the total service effort each pool would need to drain to emptiness with no further arrivals; the load vector of the standard load condition is (Eq. 8.25), and the total arrival rate vector (including internally routed traffic) is the unique solution of the traffic equations . A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.
For any queueing network under HLSPS control with proportion vector , if
the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.
Lemma 8.15 isolates the workload derivative identity at a busy
station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma
8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a
feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov
function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the
book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct
structural engine behind the goal theorem: a uniform excess departure rate over the total arrival
rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to
generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.
The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.
Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network,
q=workload) return no relevant results (per triage.json); this mission is a from-scratch
formalization of feedforward networks, the workload operator, HLSPS control, and their stability
theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.
Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights , chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.
Mission IV's queueing-network model data and fluid-equation specialization are restated locally
(drafts in this series do not import one another). The workload operator's matrix inverse
is supplied as external data with its defining two-sided-inverse property, rather
than derived from substochasticity/transience hypotheses on (Chapter 2 material, out of
series scope) — the same convention mission III used for its process-family apparatus. The
non-idling and HLSPS fluid models are each packaged as their own predicate plus a
Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the
non-idling stability object (not a separately restated "FCFS fluid model") since the book's own
remark identifies the two exactly for generalized Jackson networks. A formalization that stated
Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's
actual proof architecture (see Difficulty); this mission keeps them as independent milestones/
goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range
but absent from the planning brief's disposition table, is added as a milestone rather than
silently dropped, since it is the structural step the goal theorem's own proof cites by name.
QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model
predicates are the primary reusable contributions; contributions completing the five by sorry
proofs are welcome.
Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.
The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.
There are commodities; a commodity vector is an element of , compared componentwise ( means for all ; means for all ). The inner product is .
Assumptions I–IV are: (I.a) each is closed, convex and contains ; (I.b) with ; (I.c) ; (II) each is closed, convex and bounded from below; (III.a) is continuous on ; (III.b) no is a satiation point; (III.c) if and then ; (IV.a) some satisfies ; (IV.b) and .
A competitive equilibrium is a tuple such that
An abstract economy (§2) is a game in which each player's feasible set depends on the other players' actions ; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy with the consumers, the producers and a fictitious market participant who chooses and receives , and a truncated version in which all choices are restricted to a large cube .
The statement fixes no constants; its only added hypothesis is .
In the order of the paper's argument:
Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.
The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.
The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.
A second difficulty is non-compactness. The economy has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from back to (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.
Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.
Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume (for the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking to contain , by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.
A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of ; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.
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.
The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator , is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.
For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of already implies four of the classical families of facets of the stable set polytope.
Timeline:
Vectors live in with coordinates . The polar cone of is . Let be the cone spanned by the 0–1 vectors with . For a convex cone , the matrix cone consists of the symmetric positive semidefinite matrices with for and for all , . The operator is
and , .
Let be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). is the convex hull of incidence vectors of stable sets . is the polytope given by and for . is the cone , . The relaxations are
so . The -index of an inequality valid for is the least with valid for .
The four constraint families are:
The contraction of a node turns into the inequality with the coefficients of and its neighbours removed and right-hand side .
For every graph without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has -index exactly 1:
Corollary 2.19 (first sentence): the -index of a -valid inequality is at most the independence number of the subgraph induced by the nodes with positive coefficient.
Corollary 2.15 shows that a single round of , a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently for every -perfect graph, in particular for perfect and -perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding -ranks.
The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver operator, its iterates, and the stable set relaxations , , in Lean.
The lower bound (each constraint fails on ) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix alone, cannot succeed: those conditions define the linear operator , and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in , including closedness of the iterates , which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.
Option ι, with none the special coordinate . For graphs, ι := V.IsLeast, never with an infimum that would default to 0 on an empty set.A formalization asserting only validity on , or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.
Not formalized: the linear operator and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.
Reusable infrastructure includes the polar cone, the matrix cone and the operator (usable for any 0–1 program), the polytopes and , and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of for bipartite graphs, or the -cone reformulations (iii′)–(iii″) are welcome.
Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.
David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most elements its output is never more than the harmonic number times the optimum, and that this factor is attained.
Timeline.
An input of SET COVERING I is a finite family of finite sets. The set to be covered is . A subcover is a subfamily with , and its measure is . The optimum is the minimum measure of a subcover; itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than elements.
Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET holding the still-uncovered part of . It starts with SUB , UNCOV , SET. While UNCOV is nonempty it chooses an index with maximal, adds to SUB, and removes SET from UNCOV and from every SET. When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value is the worst choosable output, here the largest, and the ratio is .
For the proof the paper introduces configurations with , runs from a configuration (sequences of admissible choices ending when UNCOV is empty), , the set of indices chosen in a run , and calls a set selectable from if for some run from . Write .
For every :
The paper states this as for all , with equality for all sufficiently large . The two-part form above is the size-free equivalent.
The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant cannot be lowered for any . Since , it also gives the well-known bound for general inputs. The bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.
Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.
The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes , and for an arbitrary covering subfamily . Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.
For the tightness half, the difficulty is bookkeeping: showing that the blocks of each segment are admissible choices at each stage and that no cover uses fewer than sets.
S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of ; two indices may carry the same set, which only widens the input class. The family, subcovers and are taken over the set of sets family S, as on the page. is a Finset.inf' over the nonempty finite set of subcovers; if then .harmonic k.Selectable K M means is the set of indices of some run.Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.
Many problems in scientific computing and statistics ask for a solution of a linear system that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.
Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.
Let have columns , let and . Write for the Euclidean norm and for the number of nonzero entries of . The sparse approximate solution problem asks for with and minimal. Define
Let be with every column divided by its Euclidean norm. Let be its Moore–Penrose pseudo-inverse, the unique matrix with , and , symmetric. Let be its spectral norm, the operator norm.
Algorithm Greedy keeps a working matrix with columns , a working vector and a set of chosen indices. It starts from , , . While , it chooses an index that maximizes and replaces by its projection onto the orthogonal complement of . It adds to and replaces every column outside by its normalized projection onto that complement. If every correlation vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system in the chosen columns of . The number of nonzero entries of the output is therefore at most the number of selection iterations.
If the columns of are linearly independent and some satisfies , then every run of the selection phase, with any tie-breaking, performs
iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).
The proof on pp. 230–233 passes through the following statements, in order:
Items 1–7 hold for every matrix . Items 8, 9 and the goal carry the independence hypothesis.
Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error with at most a factor more nonzeros than the best solution at error . The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.
The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of , and this comparison holds only when has full column rank. For general , Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.
Each step of the proof is short, but the objects are defined by an iteration. The columns are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration therefore needs invariants: chosen columns are orthonormal and orthogonal to , and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.
A naive attempt to bound directly by fails: multiplies the projected columns , not , and different sparsest solutions can have different norms.
Vectors live in EuclideanSpace ℝ (Fin m), so every is the Euclidean norm. The only is the maximum of , which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of iterations (IsGreedyRun) requires, at each : the strict while-condition , an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends to , so a column lying in the span of the chosen ones stays zero and is never chosen. is an infimum over ℕ, and the goal assumes that some has , since otherwise the infimum would be . The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then . The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as , which would hide the rank assumption.
Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of are linearly independent, which forces . Without it, Theorem 2 fails. Take , , columns and for 100 distinct , and . Then and the bound evaluates to , but Greedy selects two columns. Lemma 2 fails for and . The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace by the largest over linearly independent column subsets of , which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.
A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.
A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.
Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction , in which every clause has at least literals, is polynomial complete for every , so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.
Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).
Timeline, for orientation:
Let be the set of literals; the complement of is and conversely. A clause is a finite set . A truth assignment is a set containing no complementary pair ; it may leave variables unassigned. satisfies if .
An input is a finite set of clauses. Its feasible solutions are the subsets satisfied by a single truth assignment, measured by , and the optimum is
The subproblem admits only inputs whose clauses each contain at least distinct literals.
Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB TRUE , LEFT , LIT . While some literal of LIT occurs in a clause of LEFT, it picks a literal LIT contained in the most clauses of LEFT, moves those clauses from LEFT to SUB, adds to TRUE, and removes and from LIT. When no literal of LIT occurs in LEFT it returns SUB.
The choice of is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on is the smallest over choosable outputs . The worst-case ratio on inputs of size at most is
For all ,
with equality for all sufficiently large . In the size-free form used here: every choosable output on every satisfies , and for every some has a choosable with and .
The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio . The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.
The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every . The paper spells out only and states that "similar examples can be constructed for any other "; the formal goal requires them for all .
The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both and are allowed and have to be handled.
The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at the paper's pattern degenerates and needs adjusting.
Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.Set of literals without a complementary pair (partial, as in the paper). is the maximum of over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition ; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general . The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.
David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.
Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity so as to fill it as much as possible. For this problem the paper gives a family of algorithms , one for each , whose guaranteed ratio tends to . It is one of the first examples of what is now called a polynomial-time approximation scheme: for every there is a polynomial-time algorithm within a factor of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.
This mission formalizes Theorem 1 of the paper, the performance guarantee of together with its tightness.
An input of SUBSET-SUM is a finite set , a positive rational size for every , and a positive rational bound . An approximate solution is a subset with , where the measure is . The problem is a maximization problem with optimal measure
Fix and call big if and small otherwise. Algorithm keeps a set , its measure , and the remaining elements :
Steps 1 and 3 may have ties. Following the paper, a set is choosable by if some resolution of all ties produces it, and the performance on input is the smallest measure of a choosable output. The ratio is , and is its maximum over inputs of size at most .
For and ,
Formally, for every : every choosable output of every input satisfies ; and for every some input has a choosable output with and .
Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above , in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of itself cannot be sharpened.
The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly . The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.
The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as always equalling or which elements can enter after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general : exactly unit elements are added after , and this must be shown for every choosable run, not only for one.
ℚ), as in the paper; sizes are required to be positive on and . The index is a natural number with as a hypothesis; is rational division, and "big" is the strict inequality .opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains ; it is when no element fits.Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning . Every "closest to, without exceeding" is an existential choice among all maximizers.def on Fin (k + 2) exactly as on the page, with (the page leaves the range implicit; keeps the only big element that fits when ).Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ( for step 1) and Sahni's knapsack extension are not part of the mission.
A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem , and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.
J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.
Timeline:
A finite set of jobs is given. Job has a processing time and a due-date , and the paper assumes for every job (a job that cannot finish on time even if started at time is removed beforehand). The machine starts at time and processes the jobs one after another, without idle time or preemption.
A schedule of is an ordering of all jobs of . The job in position completes at . The late set is and the early set is . A schedule is optimal if no schedule of has fewer late jobs. and denote the early and late jobs of , each kept in their order in .
Moore's algorithm works on a current sequence and a list of rejected jobs.
The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.
In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, and are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.
Let be a shortest-processing-time schedule of , and let a run of MooreStep from reach a state in which has no late job. Then for every due-date ordering of and every ordering of ,
All tie-breaks in both sorts are covered.
In attack order:
A companion item states the p. 104 remark that the final current sequence need not be re-sorted: is already optimal.
The theorem shows that the minimum number of late jobs on one machine can be found in time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.
The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.
Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job , the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as .
ι with decidable equality; is a Finset ι; .List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.MooreStep. The re-ordered prefix is any due-date sorted permutation of the first jobs, and case 2) rejects the first late job itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.The goal must concern runs of this step relation from a shortest-processing-time schedule of . Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.
Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.
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.