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?
The continuous-review policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point , an order of fixed size is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.
Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity of the stochastic model compare with the EOQ quantity computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the bound on the cost of using the EOQ quantity (Theorem 5).
Demand arrives at rate and replenishment orders arrive after a fixed leadtime . Shortages are backordered. Holding costs accrue at rate per unit held, backorder penalties at rate per unit short, and every order costs . The leadtime demand is a nonnegative random variable with law and mean . The expected inventory cost rate at inventory position is the newsvendor cost
assumed, as in the paper, to attain its minimum at a unique point . The long-run average cost of the policy is
For each , let be an optimal reorder point, i.e. a minimizer of . The analysis runs through the curves
and through the cost of order quantity with the reorder point set optimally. The optimal order quantity is the minimizer of over .
The EOQ model is the case of a constant leadtime demand . Its cost rate is , and the same construction gives , , and the optimal quantity
For , let , , be the positive solutions of
Each has exactly one positive solution, and
Moreover, with and the demand law fixed, is nondecreasing on and converges to a finite constant as .
The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:
The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by , a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as grows. The first inequality, , is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most ). The explicit bounds , , bracket and give a search interval for it.
Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.
The obvious route to compares the two cost curves and directly. It fails because pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve is defined only implicitly, as evaluated at a minimizer of a parametric integral, so its growth relative to the linear has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ( also has a vanishing derivative), so the printed proof of the limit does not go through as written.
Without a density, need not be differentiable. Every derivative in the paper's proofs (of , and ) must be replaced by monotonicity or chord arguments.
The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:
Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:
Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).
Firms that can buy the same item from two suppliers, a cheap slow one and a fast expensive one, face the dual-sourcing inventory problem: how much to order from each source in every period when demand is random and unmet demand is backlogged. Global sourcing (offshore regular supply plus a near-shore express supply) is the standard example (Allon and Van Mieghem 2010). When the two lead times differ by more than one period, the optimal policy depends on the whole pipeline of outstanding orders. No simple optimal policy is known, and dynamic programming is intractable for long lead times.
The tailored base-surge (TBS) policy orders a constant amount from the slow source and uses the fast source to bring the expedited inventory position up to a fixed level. It is simple, and it is used in practice. Janakiraman, Seshadri and Sheopuri (JSS, Management Science 2015) showed that its best parameters solve a convex program that does not depend on the regular lead time, and they conjectured, with numerical support, that TBS is near-optimal when that lead time is long.
Timeline:
Let be a nonnegative random variable with finite mean that is not almost surely constant. Demands are i.i.d. copies of . The regular source has lead time , the express source has lead time , and . In period the controller orders and ; then arrives and is realized, so the on-hand inventory evolves as and may be negative. Initially nothing is on order and , where the are further i.i.d. copies of and , .
The per-period cost is with , where and is the express premium (the regular unit cost is normalized to ). An admissible policy chooses the two orders in period as deterministic measurable functions of . Its long-run average cost is
With the expedited inventory position , the TBS policy orders and . A best TBS pair minimizes over and (first in through , then in ).
The constants and are explicit functionals of the law of and of . They are built from , , , the mean absolute deviation , and the large-deviation quantities of (p. 441).
For all , and ,
The threshold does not depend on , so the statement gives an explicit, inverse-polynomial rate. Its limit form is Corollary 1 of the paper.
In the order the proof uses them:
The theorem shows that one of the simplest dual-sourcing heuristics is asymptotically optimal as the regular lead time grows. This is the regime where exact dynamic programming is hopeless. The best TBS parameters come from a convex program independent of , so the result yields an algorithm whose running time does not grow with and whose optimality gap is bounded explicitly for every finite . It extends the lower-bounding technique of Xin and Goldberg's lost-sales work (Operations Research 2016) from a static to a dynamic relaxation.
Formalization adds the following. To the best of available knowledge, none of the objects involved (average-cost inventory control with backlog, TBS policies, Lindley-type maxima of random walks with their Spitzer identity) exists in Mathlib or on the platform. The paper's proof defers several ingredients to the literature or omits them: Lemma 1, Eq. (3), Lemma 3, and the details of Lemmas 5 and 7. A complete formal proof must supply them. The result is proved on paper but not formalized anywhere.
An optimal dual-sourcing policy need not be stationary, its induced Markov chain need not have a stationary distribution, and the inventory is unbounded below. The natural argument would compare the optimal policy's steady state with the TBS steady state, and it fails at its first step. Theorem 2 replaces the steady state by a vector with a few distributional properties, built from time averages. That construction, and the independence structure it must carry, is the central technical step. The conditional Jensen step then leads to a single-source problem with possibly negative demand, where textbook interchange-of-limits theorems do not apply directly. Finally, bounding away from requires a quantitative lower bound on the growth of random-walk maxima under only a first-moment assumption.
Conventions of the Lean development (namespace XinGoldbergTBS.Asymptotic):
Lemma 1, Eq. (3) and Lemma 3 are results the paper quotes from Sheopuri et al. (2010), JSS and Scarf (1960). Proposition 1 (conditional-expectation form of the bound) is not included.
A trivializing formalization is ruled out: ranges over the full admissible class, the constants are definitions rather than hypotheses, and the goal includes an existence clause.
Reusable beyond this mission: average-cost inventory models with lead times, discounted single-source backlog value functions, and Spitzer-type identities for random-walk maxima. Contributions to any milestone are welcome.
A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.
The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.
There are states and, in state , a finite nonempty set of decisions. A transition under decision earns and rewards are discounted by , . The row of transition probabilities is unknown; it is known to lie in a closed convex nonempty set of probability vectors, and .
A prior is a probability distribution on matrices whose rows are all probability vectors. Its means are . After a transition under decision the prior is replaced by the Bayes transformation (Eq. (8)), with the normalizing constant. The Bayesian optimal return solves the recursion
The max-max and max-min values , solve
with max for and min for . Finally , the prior probability that the true matrix lies in .
The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.
For every bounded solution of (10), all solutions , , every prior and every state ,
together with the existence of , and . Both halves are the paper's printed statements.
The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability . When the prior concentrates on () the bounds become : the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.
Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.
The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to , which cannot represent a prior with mass outside ; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of is not automatic, since is only characterized by a functional equation.
Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel -algebra.bayes then returns . That posterior is always multiplied by in (10), so the choice is immaterial.⨆/⨅ over a nonempty bounded set. "Obviously " is stated for every pure stationary policy , not only a max-min optimal one. The policy return is the componentwise series .Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known- optimal value in ; a general Jensen inequality for functions convex along mixtures of probability measures.
Many problems in optimization and equilibrium modelling reduce to a system of equations whose map is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, , is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.
Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.
Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of , with order under -order semismoothness.
Let be locally Lipschitz. By Rademacher's theorem is differentiable on a set of full measure; write for the Jacobian at . The generalized Jacobian is
the convex hull of all limits of Jacobians along sequences of differentiability points converging to . The one-sided directional derivative is .
is semismooth at if it is Lipschitz near and, for every , the limit of over , , exists. For , is -order semismooth at if in addition for , .
For , the nonsmooth Newton method is
where any element of may be chosen at each step. A run is a pair of sequences , with and for all . A root () is regular when every is nonsingular.
Let be locally Lipschitz, , semismooth at , and every nonsingular. Then there is such that every with is nonsingular, a Newton step from such a stays within of , and every run with satisfies
The goal asserts only the shape of the convergence (superlinear) and fixes no constants.
If moreover is -order semismooth at , , there are and with
for every run started within of .
The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of and its realisation by an element of ), Theorem 2.3 (semismoothness is equivalent to and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order- sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).
The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order- variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.
The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.
The classical Newton proof compares with its linearization and uses continuity of the Jacobian at . Here neither is available: need not be differentiable at or at any iterate, the element is chosen arbitrarily from a set, and need not be close to any fixed linear map. The comparison has to go through the directional derivative , which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls uniformly in the direction, and that is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of , none of which is in Mathlib. The superlinear rate also requires a uniform bound on in a whole neighbourhood, not just at .
Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces (the paper's is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:
fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences of differentiability points.lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.IsUnit in the ring of continuous linear endomorphisms; is a two-sided inverse of operator norm at most .IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order " is pinned as with and uniform over runs. Every in (2.8), (2.9) and (2.17) is its – form with a non-strict inequality , and every is an explicit constant and radius.HasStrictFDerivAt, which corrects the misprint for in the paper's display (2.16).A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.
A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about , are welcome.
Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.
Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.
Let be a finite set of terminals and a simple graph on , the labelled graph whose edges are the possible links. Each edge carries a real length ; lengths may be negative, zero, or tie. For a finite set of links, denotes the graph on whose edges are the links of .
Only edges of are possible links; in Prim's distance table a missing edge has length .
For every finite connected graph and every ,
This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.
The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.
The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.
The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.
Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:
Fintype with decidable equality; is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of matter.Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.linkGraph F; the P2 condition is a single inequality against every -edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty ).sInf of the lengths of spanning subtrees; continuity is in the product topology.Implicit hypotheses made explicit: connected (hence ) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; nonempty and for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.
The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.
Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.
Quasi-Newton methods minimize a smooth function on by moving along , where is the gradient and is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building , but it stores a dense matrix, which is prohibitive for large .
Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last correction pairs and rebuilding the matrix from a simple initial matrix at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.
Timeline:
Let be a symmetric positive definite matrix and , and let , a strictly convex quadratic with gradient and unique minimizer .
Exact line search. Along a direction from , the step minimizes .
BFGS update. For a pair with and , the BFGS update of is
Special BFGS matrices. Fix symmetric positive definite and a number of stored corrections. Given pairs , the special matrix is updated by the pairs , oldest first (the paper's (4)–(5)). Only the most recent pairs enter, and the matrix is rebuilt from .
SQN. Starting from , with :
with the exact step and the special matrix built from the last pairs.
PCG with fixed preconditioner . , , with .
For every , every symmetric positive definite and , every , and every ,
where are the SQN iterates. The statement fixes no constant beyond the dimension bound .
The result shows that storing only correction pairs costs nothing on quadratics: for any , SQN terminates in at most steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with : the matrix satisfies the secant equation on the most recent directions.
The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.
The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, is dotProduct, and is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step . The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's ). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: , , and exact line searches. need not be diagonal.
Two misprints are corrected and flagged in the items: the denominator of in (13) is (as in (12) and p. 778), and the second relation of (16) is stated for (as used on p. 778), since it fails for .
Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from and the last pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns . The standing assumption is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With SQN is steepest descent and the goal is false, so is required.
Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that mutually -orthogonal vectors in include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.
Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.
Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, for the gradient norm, is better than the of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.
This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.
Let be a closed convex set with nonempty interior, and let be twice differentiable on with gradient and Hessian . A starting point is fixed, and is assumed to contain the level set in its interior. Assumption 1: the Hessian is Lipschitz continuous on in the spectral norm, for all , with .
For a parameter the cubic model of at is
The cubic-regularized Newton step is any global minimizer of over ; it exists because the model is continuous and coercive. Write and .
The cubic regularization of Newton method (3.3) fixes , starts at and, for , chooses such that , then sets . The choice always passes the test.
Write for the smallest eigenvalue of a symmetric matrix . The measure of local optimality is
It is nonnegative and vanishes exactly when and .
If for all , then every run of method (3.3) satisfies, for every ,
The constant and the exponent are the paper's; the statement holds for every admissible choice of the parameters and of the global minimizers .
Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, , and the most negative curvature, , along the best iterate, from a single scalar potential . The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.
The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.
Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only , which is weaker. The natural first attempt, "take the second-order optimality condition of the model at ", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.
The second is Lemma 2's second claim, used for (2.12): showing that stays in requires a boundary argument along the segment from to , since the Taylor bounds are only available inside . The remaining work is calculus in : the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of .
The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of this asks for two-sided derivatives, a mild strengthening of "twice differentiable on ". The Lipschitz condition uses the operator norm, which is the spectral norm. is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes as plus the model value at , which is the minimum because attains it. is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound is required on only. The minimum over is written as the existence of an index attaining the bound.
A stationary point of the cubic model is not an admissible step, and the run must keep the test and the acceptance test. Replacing the step by any point with makes the goal false, and dropping the square root in makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis , which its printed proof uses and which holds at every iterate.
A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.
A maximal independent set (MIS) of a graph is a set of pairwise non-adjacent vertices to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be computed by a fast parallel algorithm was a central question of parallel complexity in the early 1980s: Karp and Wigderson gave the first NC algorithm (STOC 1984), and Luby's paper, SIAM J. Comput. 15(4):1036–1053, 1986, gave a much simpler one. MIS is a subroutine of many parallel and distributed graph algorithms (colouring, matching, symmetry breaking), and Luby's randomized algorithm remains the standard one in distributed computing.
The paper's second contribution, the subject of this mission, is a general method for removing randomness: analyse the randomized algorithm under pairwise independence only, then realize pairwise independent random variables on a sample space of polynomial size and try every sample point in parallel. The same method, often attributed jointly to Luby (1986) and to Alon, Babai and Itai (J. Algorithms 7, 1986), became a standard tool of derandomization.
Let be a finite simple graph with vertices labelled . The algorithm keeps a set (initially empty) and the current graph , the subgraph of induced on (initially ). For the neighbourhood is . Each execution of the loop body selects an independent set , adds it to , and deletes from ; the loop runs while . Write for the degree of in , for the number of edges of before the -th execution, and .
Algorithm B's select step draws a coin for each vertex, with , puts , and removes from the endpoint of smaller degree of every edge inside (both endpoints on a tie).
The sample space. Fix a prime with . The sample points are the pairs with , each of probability . With , the coin of vertex at is iff , so , and distinct coins are pairwise independent.
Algorithm D. Each execution of the loop body first moves the isolated vertices of into . Then:
No random bits are used.
For every graph on vertices, every prime with , and every run of Algorithm D (every tie-break among maximum-degree vertices and every maximizing sample point), the loop body is executed exactly times, with
and the output is a maximal independent set of .
The goal is the deterministic half of Luby's result: an MIS is computed in parallel rounds with no randomness, which places MIS in deterministic NC. The pairwise-independent analysis (Lemmas C, D, Theorems 2, 3) is the reusable part: it shows that the Monte Carlo algorithm's progress guarantee survives when mutual independence is weakened to pairwise independence, which is what makes a sample space of size sufficient. Lemmas 1 and 2 are the standard construction of pairwise independent variables with prescribed rational marginals.
All of these results are proved in the paper. None is formalized on the platform. A related but different object is the platform's dot-product hash family (AlmostLossless.pairwiseIndependent_dotHash), which has uniform marginals over a field and is not the -point matrix space with prescribed marginals . The companion mission A Simple Parallel Algorithm for the Maximal Independent Set Problem I formalizes Theorem 1, the mutually independent analysis of Algorithms A and B.
The obvious route to Theorem 2 repeats the proof of Lemma B, which lower-bounds by a product over independent events. Under pairwise independence the probability of an intersection of three or more coin events is not determined by the marginals, so that product argument fails, and the constant degrades from to .
The round bound needs a separate argument for high-degree vertices. The rounded probabilities are close to only when is large, which is why vertices of degree at least are handled by Case 1. Counting the Case 1 rounds uses the vertex count of the original graph, not of the current one. Correctness at termination requires an invariant linking , and across both kinds of rounds and the deletion of isolated vertices.
Vertices are Fin n with labels , which is §4.2's indexing of ; the label enters as a residue, and labels are distinct mod because . The current graph is the induced subgraph kept on the full vertex type, with deleted vertices isolated. One execution of the loop body is a relation between states that leaves the maximizing vertex (Case 1) and the maximizing sample point (Case 2) free, as the page does, and a run is any sequence of states starting at that follows the relation while . The goal asks for the first index with , so a statement about a later state or a bound on without termination does not meet it.
The conditions and are encoded exactly as and in . is natural-number division. The printed code tests , which puts residues in and contradicts stated on the same page; the formalization uses the strict test.
Lemmas C, D and Theorems 2, 3 quantify over every probability space carrying measurable, pairwise independent (IndepFun for each pair of distinct vertices) coins with the stated marginals at vertices of positive degree. Replacing pairwise by mutual independence, or fixing the probability space, would weaken them. They are stated for a fixed current graph, that is, as the expectation conditional on the state before the round, which is what their proofs establish. Expectations are Bochner integrals of a function with finitely many values and are therefore genuine. Lemma 2 carries the hypothesis , implicit on the page.
The development needs the induced subgraph and degree bookkeeping from Mathlib's SimpleGraph, pairwise independence from ProbabilityTheory.IndepFun, finite counting in ZMod q, and real logarithms. The pairwise-independent analysis (Lemma C to Theorem 3) and the sample-space lemmas are reusable beyond this mission. Contributions to any milestone are welcome.
A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with colours, and many other symmetry-breaking tasks.
Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.
All algorithms in the paper run the same loop on a finite simple undirected input graph with vertices. The current graph is , initially . For the neighbourhood is . One execution of the loop body selects a set independent in , adds it to the output, and replaces by the subgraph induced on . The loop stops when is empty.
For write for its neighbours and for its degree. The two Monte Carlo select steps are:
Let be the number of edges of before the -th execution of the loop body. The number of edges eliminated by that execution is : exactly the edges of with at least one endpoint in . For the paper uses the weight .
For the current graph and ,
The constants are those printed in the paper. No connectivity, degree or size condition on is assumed.
Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is , and hence that MIS has a Monte Carlo algorithm running in expected time on a CRCW P-RAM and on an EREW P-RAM with processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.
The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.
The obvious argument tries to show that a fixed vertex enters with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in . This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when is large, which is why the conclusion involves a minimum with a constant.
A second obstacle is the passage from vertices to edges: vertices of small can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from can collide, so the argument about a uniformly random order holds only on the event that is injective. That event appears as the factor .
SimpleGraph V on a finite type with decidable adjacency, and . The degree is SimpleGraph.degree, is neighborFinset, and is edgeFinset.card.Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces by does not state the paper's theorem.
A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.
The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.
The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.
A project network has events labelled with : event is the origin and event the terminus. A job is an arrow from an event to an event , written job ; the jobs form a finite set of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:
Each job has a real duration . The earliest event times are given by display (1) of the paper,
and, for a project completion time , the latest event times by display (2),
The maximum time available for job is . The job is critical if this equals its duration, , and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events with every a critical job of .
In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.
For every project network, durations and completion time ,
This is the paper's "A project will contain critical jobs only when . If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.
The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify and with extreme solutions of the system of difference constraints , which the paper's own §3 uses to build the project cost curve.
Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.
The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.
Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.
The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real ; the paper's assumption is a hypothesis of every theorem that uses them.
Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of in for .
A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking and as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.
Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints , which are reusable for the companion mission on the project cost curve.
Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.
This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most of the optimum, plus an additive constant, is ever used, and that the factor cannot be improved.
Timeline.
A list is a finite sequence of real numbers in ; values may repeat. A bin has capacity ; its level is the sum of the numbers placed in it. The optimum is the least number of bins into which the elements of can be distributed so that no bin has level exceeding .
The bins start empty and the elements are placed one at a time, in list order.
and are the numbers of bins that receive at least one element.
Two auxiliary notions from the paper's proof also appear among the milestones. The position of an element in a packing means that it is the -th element placed into bin . The weight of a collection of elements is defined through -pieces, the elements in . Each element has the weight . A pair with a -piece and has the discounted weight , and any other pair has . is the least total weight over all ways of grouping into singletons and pairs.
For every list ,
The constants are the paper's. Both halves are part of the goal.
The bound makes FFD and BFD, which run in time, the reference heuristics for off-line bin packing. The bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines , where is the largest ratio over lists with .
The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the bound is present in Mathlib or on the platform.
The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio . Summing over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total -weight well above . The paper's remedy is a weight defined on pairs, , which discounts elements that could share a bin with a larger one. Even with , the bins of FFD whose largest element exceeds do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.
The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with . Theorem 3.4 works only because Lemma 3.3 first removes all elements below .
Lists are L : List ℝ with the predicate IsList L ( for every element), assumed by every statement. is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most . A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least " over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted . Positions are -based pairs (bin, place in bin) read off the run.
sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: is closed in Theorem 3.4, is open at , and Lemma 4.2 has .
A weakened goal, such as with a larger , a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities , of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps , .
A complete development needs basic lemmas about FF and BF runs (levels stay at most , a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of under deletion, and . These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.
Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.
Timeline:
A Markov-renewal program has a finite set of states (the paper's ) and a finite, nonempty set of alternatives (the paper's ), each available in every state. For each alternative and states it specifies:
The Laplace–Stieltjes transform is the expected discount over one interval. The average one-step return is , and for a vector of returns the test quantity is
A stationary policy is a map ; a nonstationary policy is a sequence of such maps, being used at the -th transition. The -step return of a policy, with boundary rewards , is the test quantity of applied to the -step return of the shifted policy; the optimal -step return of equation (6) replaces by a maximum over . The value-determination equations (15) of a stationary policy are .
The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.
For every : (15) has a unique solution for every stationary policy, and every run of Fig. 1 reaches with , where
for every state and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".
The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers , so the same algorithm serves any sojourn-time law. For fixed the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).
The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.
The discount over one transition, , varies with , and , so the problem is not a constant- contraction of textbook form; the relevant bound is that every row of sums to less than one, which rests on . Entries in alone, the paper's stated justification of Claim (a), do not make invertible: the matrix with every entry has entries in , yet minus it is singular.
Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.
Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.
The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems with a symmetric positive definite matrix . It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most steps, and a method of successive approximations whose intermediate estimates are useful in their own right.
The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the -weighted error , and the residual need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.
Timeline:
Let be a real matrix that is symmetric and positive definite, let , and let be the solution of . Write and . From an arbitrary starting point , the cg-method (5:1) computes estimates , residuals and direction vectors by
The error vector of is . The error function (4:5) is , which is nonnegative and vanishes only at . The Rayleigh quotient (4:12) of a vector is . The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for , errorFun A h x and rayleigh A z.
For every step that the method performs, that is, every with ,
The paper writes the step from to ; the Lean statement shifts the index by one. The goal holds for every dimension , every symmetric positive definite , every and every .
The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the -norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.
The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.
The obvious argument does not reach the conclusion. The method decreases at every step, but a decrease in this -weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.
A second difficulty is bookkeeping at the end of the run. The recursion divides by and by , which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis exactly because the strict inequality fails once .
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention makes it stay at with once . Lengths appear squared, as . The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries .
Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination () or any bound on : it quantifies over every cg run and every step that takes place. And it is about the Euclidean length , not the error function (that is Theorem 6:1, a different and weaker statement) and not the residual.
A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of for . These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.
Solving a linear system with a large symmetric positive definite matrix is a basic task of scientific computing: it arises from discretized elliptic equations, least-squares problems and the Newton steps of optimization methods. In 1952 Magnus Hestenes and Eduard Stiefel published the conjugate gradient method (cg-method) (J. Res. Natl. Bur. Stand. 49 (1952) 409–436). The method uses only through matrix–vector products and stores a few vectors. The paper's abstract states its central property in one sentence: "The solution is given in steps."
The paper obtains this property from a more general scheme, the method of conjugate directions (cd-method), which also contains Gaussian elimination as a special case. Its argument has two parts. Every cd-method with nonzero directions reaches the solution within steps (Theorem 4:2). The cg-method is a cd-method (Theorem 5:2), which follows from the orthogonality and conjugacy relations of Theorem 5:1. This mission formalizes that chain.
Vectors are real -tuples, with scalar product and squared length . The matrix is real, , symmetric and positive definite, which is the paper's standing assumption (p. 410). The solution satisfies . The residual of an estimate is . Two vectors are conjugate when .
The cg-method (eq. (3:1), p. 411) starts from an arbitrary estimate and sets . Given , , , it computes
In Lean the iterates are cgIter A k x₀ i, a structure with fields x, r, p. The step length is cgA.
The cd-method (Section 4, p. 412) chooses an arbitrary first direction and then sets with and . Each new direction may be any vector conjugate to . Because the directions are free, a cd-run is a property of sequences: IsCDRun A k x r p.
For every , every symmetric positive definite , every and with , and every initial estimate ,
where is the -th cg iterate. This is the statement of the abstract and of Section 3 (p. 410): "one will reach an estimate () at which . This estimate is the desired solution ."
IsCDRun.Finite termination is the property that distinguishes the conjugate gradient method from stationary iterations such as Jacobi or Gauss–Seidel. It explains why the method can be used as a direct solver in exact arithmetic. It is the starting point for the later theory of Krylov subspace methods. The relations of Theorem 5:1 are the checks the paper recommends for monitoring a computation (eq. (3:3)). They are also the input to the paper's further results on the monotone decrease of the error (Section 6) and on the connection with orthogonal polynomials (Sections 14–18).
The result has been proved since 1952 and appears in every numerical linear algebra textbook. As far as a search of the Prove2Me catalog shows (September 2026), it has no machine-checked proof there. The only conjugate gradient material on the platform is a Hilbert-space convergence result for a different recurrence. This mission adds a faithful formal version of the original recursion (3:1) and of the cd-method. It also adds the complete termination argument, organized as in the paper. The definitions and the Theorem 5:1 relations are reusable by any later formalization of Krylov methods, including the second mission of this series on the decrease of the error .
The obvious argument says that the residuals are mutually orthogonal, so at most of them are nonzero. That argument is only as good as the orthogonality, and Theorem 5:1 must be established by a simultaneous induction over four families of relations. The recursion defines by an update, not as , so even needs a proof. Orthogonality of to the earlier residuals needs the conjugacy of the earlier directions, and conjugacy of needs the orthogonality of the earlier residuals. Neither family can be proved first.
A second obstacle is the passage from orthogonality to termination. A cd-run with a zero direction stalls, so Theorem 4:2 needs the directions to be nonzero. The cg directions become zero exactly when the solution is reached, so applying Theorem 4:2 to cg needs a case split at the first vanishing residual.
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), and is Matrix.mulVec (*ᵥ). The hypothesis on is Mathlib's Matrix.PosDef, which includes symmetry. The solution enters only through the hypothesis A *ᵥ h = k. Indices are 0-based, as in the paper.
The cg iteration is total and has no stopping test. Once , Lean's convention gives and . From then on the iteration stays at , with zero residuals and directions. For this reason the relations of Theorem 5:1 are stated for all indices without guards: after termination they hold trivially.
Two formulations would make the goal trivial, and neither is used. One is a stopping test or step that refers to or to . The other replaces (3:1b), (3:1d) or (3:1e) by the equivalent formulas (3:2a), (3:2b) or , which would move Theorem 5:5 and part of Theorem 5:2 into the definition. The iteration is (3:1) literally.
The cd-method's implicit hypothesis, that the directions are nonzero, is an explicit binder of Theorem 4:2. Without it the statement fails (take ). The hypothesis is satisfiable: the cg run with nonzero residuals is one example.
A complete development needs the standard facts that mutually conjugate nonzero vectors are linearly independent and that independent vectors span . It also needs the induction behind Theorem 5:1. Contributions welcome beyond the milestones include the converse half of Theorem 5:2, the relation (5:2) expressing through , and Theorem 4:5 (the cd-method computes ).
In online convex optimization a player repeatedly chooses a point from a convex set , after which an adversary reveals a convex cost function and the player pays . The player's regret after rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).
For general convex costs the best achievable regret is of order . Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, -exp-concavity, brings the regret down to order , and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of .
Timeline.
Fix and a set that is nonempty, closed, bounded and convex, with positive Lebesgue volume . Fix . The cost functions are , each continuous on and -exp-concave on : the function is concave on (LogRegretOCO.EWOO.IsExpConcave).
EWOO keeps the weights
and on round plays the -weighted mean of ,
(LogRegretOCO.EWOO.ewooPoint). In particular is the centroid of , and each depends only on . The regret against a comparator is .
For every and every ,
This is the paper's printed constant. The paper's proof yields the slightly sharper ; the printed form is the goal.
The proof in §3.4 (p. 187) passes through five displays, each a milestone:
The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant that does not depend on the size of or on the gradients of the costs. Specialised to the log-loss on the simplex, where , it recovers the regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound and diameter and pay a factor .
Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, , appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in , the change of volume under homothety, and the elementary inequality . A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.
The pieces are classical, but they have to be assembled in measure-theoretic form. The point is a Bochner integral of a vector-valued function over , and its membership in and the Jensen inequality both require the normalised weight to be a genuine probability measure on , with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that be closed and have positive volume.
The second obstacle is that Eq. (18) compares the algorithm with an average of the product over all of , while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in destroys the logarithmic rate. Controlling this loss in dimensions, with a constant independent of the shape and size of , is the heart of the argument.
Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from : the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of ; only their values on enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.
Conventions and corrections relative to the printed text:
⨅ or sInf over , which in Lean would return a junk value off its intended domain and trivialize the statement.volume P ≠ 0 is added: the algorithm divides by , which the paper leaves implicit. Without it Lean's convention would set .Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound . Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.
Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret over rounds is optimal; for costs with curvature it can be logarithmic.
Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with regret for -exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.
Timeline. Zinkevich (2003) proved regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with regret for exp-concave costs.
The decision set is nonempty, convex, closed and bounded, and bounds its diameter: for . In rounds the player picks and then pays , where is a cost function differentiable at the points of with gradient norm on . The cost is -exp-concave () if is concave on . The regret over rounds against a comparator is .
Follow the Leader plays (any point of in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter plays FTL on the approximate costs
In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory .
With , every FTAL run on -exp-concave costs satisfies, for every and ,
This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.
Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.
On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.
The obvious attempt, bounding each term by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like , with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small , so the constants must be tracked exactly rather than asymptotically.
Points are in EuclideanSpace ℝ (Fin n) so that is the Euclidean norm; cost functions are functions on all of , differentiable at the points of , with Mathlib's gradient. Rounds are -based; and are unused. is any upper bound on pairwise distances in . Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.
Regret is always stated against every comparator . A formalization with a real-valued ⨅/sInf over , or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's , would be trivial or false, and is excluded: the goal carries IsFTALRun with .
Corrections and conventions relative to the printed paper:
deriv with explicit differentiability at the points , .Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality . Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.
Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round a player picks a point of a convex set , and only then learns a convex cost function and pays . Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.
Many costs met in practice have more curvature than bare convexity. The log-loss of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.
Timeline:
The decision set is nonempty, closed, bounded and convex, and bounds its diameter: for all , with the Euclidean norm. The costs are real functions, differentiable at every point of , with gradient bound on . A cost is -exp-concave () if is concave on .
For a matrix , the generalized projection is a point of minimising over .
The Online Newton Step fixes
writes and , plays an arbitrary , and then
The regret after rounds against a comparator is ; the paper's regret is its maximum over .
In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.
For every run of ONS, every horizon with , and every ,
The added condition is what makes the printed constant correct (see Formalization scope).
Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in , at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.
The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with and a , a different statement) and the Euclidean case of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with and bound ) is an open private draft with different parameters.
The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes , needs a uniform lower bound on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential and a projection in the norm of rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.
Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index is unused. Cost functions are ambient functions , differentiable at the points of , with given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. enters only as an upper bound on distances in . The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.
Corrections and added hypotheses:
Regret is stated against every comparator , never as a real infimum ⨅ over , which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's , and . A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with , , , is a model.
A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, and ); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of .
The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).
For a class of Vapnik–Chervonenkis (VC) dimension the answer was known up to a logarithmic factor for about 25 years:
Let be a set with a -algebra and . A classifier is a measurable map ; the concept space is a set of classifiers with . A finite sequence is shattered by if every labelling is realized by some ; the VC dimension is the largest such , assumed finite (then ).
A data set is a finite sequence of pairs in , and is the set of with for all . For a probability measure and a target , the error of is , where . A learning algorithm maps data sets to classifiers.
For , the sample complexity (Definition 1) is the least such that some algorithm satisfies, for every probability measure on and every , with independent with law ,
and if there is no such .
The learner of the paper uses three ingredients. A sample-consistent learner returns an element of whenever that set is nonempty. The majority vote is . The subsample algorithm returns if ; otherwise it splits into a head of points and three blocks of points, and returns the concatenation of , and . The learned classifier is .
The paper states Theorem 2 as with a numerical constant; its proof establishes the bound above with , and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.
Together with the classical lower bound, Theorem 2 gives : the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.
The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.
The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth . In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set that varies with the level, and the numerical constants, which are tight (the key comparison is ).
Bool (true for ); data sets are lists and is concatenation; is a set of measurable functions with ; the VC dimension is a supremum in , assumed equal to a natural number . The i.i.d. sample is the product measure on . "With probability at least " is stated as a bound on the outer measure of the failure event. takes values in , so the goal is stated as , which is equivalent. Ties in the majority vote go to , as printed.Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.
The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.
A serial supply chain has stages. Stage is the demand node and stage supplies stage for . Time is discrete, with periods . Stage has a deterministic lead time and a base stock . It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.
The end-item demand in period is . The window demand is , which is when . The demand bound gives , the maximum possible end-item demand over periods, with .
The backlog is the amount the customer of stage has ordered but not yet received. It satisfies the recursion (A1):
Unrolling it gives the closed max-form (A2). The external customer receives 100% service when for all . When demand never exceeds its bound, this is ensured by the service constraints
Let be the holding cost at stage and the echelon holding cost. After constant terms are dropped, the expected holding cost gives program :
Demand is random, and is the expected backlog at stage in a period .
If the echelon holding costs are nonnegative and is nondecreasing, then an optimal solution of is
Formally, (A6) is feasible, and for every period its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible . The weaker claim that "some optimal solution binds all of (A3)" would not be enough.
The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.
The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.
The objective is not linear in . Each is a convex, nonsmooth function of through the maximum in (A2), and the objective subtracts these terms, so minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on , and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.
Stages are natural numbers read on the range . Lead times are natural numbers cast to . Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function , and only indices are read. The backlog is defined by the recursion (A1), computed in steps, with for . The closed form (A2) is a theorem. Randomness is a probability space with a demand path whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.
The page's informal words are read as follows:
Monotone D on .A non-integrable backlog would make its Bochner integral and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.
Useful contributions include a proof of (A2) by downward induction on stages, the integrability of , the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.
A retailer who sells several products from shared, non-replenishable inventory over a finite season must set prices without knowing how demand responds to them. Every price posted is both a sale and an experiment. This is the network revenue management problem with demand learning, and it sits between two literatures: dynamic pricing with inventory, where demand is known and the fluid linear program of Gallego and van Ryzin (1997) is the standard benchmark, and multi-armed bandits, where learning is the whole problem but there are no resource constraints.
Ferreira, Simchi-Levi and Wang (Oper. Res. 2018) combine Thompson sampling with a linear-programming step: sample a demand model from the posterior, solve the fluid LP for that model, and randomize prices according to its solution. The same paper extends the scheme to continuous price sets, contextual pricing and bandits with knapsacks.
Timeline of the relevant results:
There are products and resources. One unit of product consumes units of resource , and resource starts with inventory that is never replenished. The season has periods. In each period the retailer posts one of price vectors or a shut-off price under which demand is zero.
Given the posted price , the demand vector has law , where is unknown and drawn from a known, arbitrary prior . Demand is independent of the past given the posted price and , and is bounded: . Write for the mean demand of product under and parameter , and .
When inventory covers all demand, all demand is sold. Otherwise the satisfied demand satisfies , leaves every inventory nonnegative, and leaves at least one resource at zero; no other rule is imposed. Revenue is .
For a mean-demand matrix and capacities , the linear program is
with optimal value .
TS-fixed (Algorithm 1): in each period, sample from the posterior of given the history of posted prices and observed demands; let be an optimal solution of ; post with probability and with the remaining probability; observe demand and update the posterior.
Finally and .
For , , every prior, every bounded demand family, every admissible fulfilment rule and every run of TS-fixed,
The paper prints this bound for , where is the revenue of the optimal policy that knows ; see Formalization scope for why the LP benchmark is stated instead.
The article states Theorem 1 and says that its proof is in the online appendix (Supplemental Material at the DOI). The article itself contains no numbered lemma. The milestone list is therefore empty; the appendix's lemmas will be added as milestones once the appendix is held.
The bound is prior-free and has explicit constants that depend only on prices, consumption rates and demand bounds. Its dependence on matches the lower bound for Bayesian regret in unconstrained bandits with rewards in , a special case of the model with no inventory constraints (Bubeck and Cesa-Bianchi 2012, Theorem 3.5). It shows that the posterior-sampling principle survives the addition of resource constraints, lost sales and randomized LP-based pricing, and it is the template for the paper's later results (TS-update, contextual pricing, bandits with knapsacks).
The theorem is proved on paper but, as far as a platform search shows, not formalized anywhere. The platform has a formal proof of the unconstrained Bayesian Thompson sampling bound (BanditAlgorithm.thompson_sampling_bayesian_regret, Lattimore–Szepesvári Theorem 36.5) and an open single-product deterministic upper bound in revenue management (RevenueManagement.deterministic_upper_bound). Neither has inventory, an LP subroutine, or lost sales. A formal proof here would supply the first machine-checked analysis of Thompson sampling under resource constraints and would check the paper's constants.
In an unconstrained bandit, Thompson sampling's regret reduces to a sum of per-period gaps between an upper confidence bound and the sampled reward, because the sampled optimal arm and the true optimal arm are identically distributed given the history. Here the action is a randomized mixture from an LP, the reward is not additive in the prices chosen, and revenue is lost when inventory runs out. Two quantities must be controlled: the revenue the algorithm would collect if all demand could be served, and the revenue lost to stock-outs. The second depends on the random time at which each resource is exhausted under a pricing rule that was optimized for a sampled, not the true, demand, and on an arbitrary fulfilment rule once some resource is empty. Standard bandit arguments do not bound such lost sales, which are a nonlinear function of the whole trajectory.
Lean representation. Products, resources and price vectors are indexed by Fin N, Fin M, Fin K; the posted price is an Option (Fin K) with none the shut-off price. Periods are 0-based ( stands for the paper's ). is a standard Borel space with a probability measure ; demand is a Markov kernel from Fin K to , bounded in for every parameter. A run of TS-fixed is a family of random variables on a probability space satisfying, almost surely and via conditional expectations: ; the posterior-sampling property of given everything before period ; the price draw with probabilities for a measurable optimal LP selection ; the demand law given the past, and the posted price; and fulfilment rules (a)/(b). The logarithm is natural. Prices, consumption and inventory are nonnegative (implicit in the paper). is a supremum over a nonempty bounded feasible set, so it has no junk value.
Corrections to the printed statement.
Ruled out. A bound for the "ideal" revenue instead of the satisfied revenue, or for an arbitrary policy whose prices are merely close to the LP solution, is not Theorem 1; the goal carries the full TS-fixed run and the lost-sales accounting.
Infrastructure needed. Posterior-sampling identities for general (standard Borel) priors, a Hoeffding/Azuma-type concentration for bounded demand along the price-selection process, LP sensitivity with respect to the mean-demand matrix, and a pathwise bound on lost sales under an arbitrary fulfilment rule. The LP and fluid-benchmark definitions are reusable for later missions on TS-update (Theorem 2), contextual pricing (Theorem 4) and bandits with knapsacks (Theorem 5). Contributions welcome: proofs of the goal, and formal statements of the online appendix's lemmas.
Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.
For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.
Let be a finite set with elements. A set function assigns a real number to every subset . It is submodular if
equivalently if the marginal value of an element does not increase as the set grows. It is symmetric if for every ; the cut function of an undirected graph is the standard example. The optimum is
For , denotes the random subset of containing each element independently with probability ; similarly is the random subset of a fixed . The Random Set Algorithm (RS) returns , a uniformly random subset of , without querying . Its expected value is the average of over all subsets,
where is the multilinear extension of , the expectation of on a random set that includes element independently with probability .
For every nonnegative submodular ,
and if is in addition symmetric,
Both parts form the goal, stated as one theorem. The constants and are exact, not asymptotic, and they are tight: the directed cut of a single arc attains , and the cut of a single edge attains .
The milestones need no sign on the function; nonnegativity enters only in the goal.
The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive -algorithm and its local search algorithms with factors and , followed by later work culminating in the tight -approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that is optimal among nonadaptive algorithms required to return one of the queried sets, and that is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.
Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.
The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.
Lemma 2.2 is not a pointwise statement: the random set can be any subset of , and can be smaller on it than both and . The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets and may overlap, and on the union contains an element with probability , so it is not the product distribution with probability on and on . Finally, the third milestone requires identifying the uniform random subset with the union of independent half-samples of and of its complement, as a statement about finite sums.
The obvious attempt at the goal, comparing with for an optimal set by set, fails: is not monotone, so a random set that contains most of may still have small value, and a random set can pick up elements that hurt.
The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption , is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.
Expectations are written as exact finite sums, not as integrals. is the multilinear extension F f (fun _ => 1/2). is , and is the double sum over independent samples , with the product of the two weights. The ranges and , implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.
Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all subsets, is the true maximum rather than the value at one fixed set, and is required to be both nonnegative and submodular.
Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.
A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.
J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.
Timeline:
A graph consists of a finite set of nodes and a finite set of edges. Each edge is directed toward a node , its front end, and away from a different node , its rear end. Parallel edges are allowed; loops are not.
For , a node meets edges of if . A set is a forest if it contains no polygon, i.e. no nonempty in which every node meets zero or two edges of ; it is a branching if in addition distinct edges of have distinct front ends. The incidence vector of has for and otherwise.
The branching polyhedron is the set of with
A vertex of a set is a point of that is the unique maximizer over of some linear function .
For weights , the dual variables are for each node and for each with ; write and . Edmonds' conditions are (15) , (16) , (17) for every edge, and, for a branching , (18) some edge of enters , (19) exactly edges of lie inside , (20) for .
Both inclusions, for every finite loopless directed multigraph.
Theorem 2 says that the linear program always has an optimal solution that is a branching, and that every vertex of is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.
The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of , linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.
The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of ; the difficulty is the dual. The natural attempt, taking for all sets and the largest positive weight entering , violates (20) as soon as the greedy choice closes a circuit: the duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form on edges entering a shrunk circuit.
A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and is the solution set of –, never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of is the real number .
Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop , the vector of is a vertex of but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.
Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for ; contributions of either are welcome.
Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with , and for multistage models it grows very fast, so is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.
Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional (an optimal transport cost). Scenario reduction then becomes: find a measure supported on a subset of the scenarios with small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.
Let be a set and a cost function with if and only if , and (conditions (C1)–(C2), p. 498). The original distribution has scenarios with weights and . Write .
A set of scenarios is deleted. The reduced measure is with reduced weights , . A transport plan from to is a nonnegative matrix with row sums and column sums . The Kantorovich functional (10) is the value of this transportation problem,
and is the best distance achievable once is fixed. The optimal deletion problem (13) asks for for a given .
In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue (), optWeightsValue () and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.
For every ,
and the minimum is attained at the optimal redistribution rule , where and , for every such choice of .
Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of , which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.
The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.
The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all , not over the kept scenarios.
Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: , (C1), (C2), and . Measurability of and conditions (C3) and (C4) concern and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis , implicit in Theorem 2, is stated explicitly; in Theorem 4, plays this role.
and are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. is defined as the transportation problem and is not defined by the closed form ; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force .
Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).
Nash's equilibrium existence theorem assumes that each player's set of available strategies is fixed. Many social and economic systems do not work that way: a consumer's budget set depends on prices, which are the choices of another agent, and a firm's feasible production may depend on what other firms do. Gerard Debreu's A Social Equilibrium Existence Theorem (PNAS 38(10), 1952) proves that an equilibrium exists in such a system, called a social system or abstract economy (today also a generalized game). Here each agent's feasible actions depend on the actions of all the others.
Arrow and Debreu used this theorem to prove the existence of a competitive equilibrium (Econometrica 22(3), 1954). It is the standard existence result for generalized Nash equilibrium problems in operations research, where the feasible sets are coupled by shared constraints.
Timeline.
There are finitely many agents . Agent chooses an action in a set , a subset of a finite-dimensional real space. A profile lies in . For each agent, denotes the actions of the others, ranging over .
Given , agent may only choose from a nonempty set , a multi-valued function of the others' actions. Its graph is . The payoff takes values in the completed real line . The best value available to agent and the set of constrained best responses are
An equilibrium point is a profile such that, for every , and .
The topological vocabulary is Debreu's §1:
A multi-valued function is semicontinuous if its graph is closed.
Assume that for every , is a contractible polyhedron, is closed, is continuous on , is continuous on , and is contractible for every . Then
The result. The theorem gives an equilibrium for games in which one agent's choices constrain another's. This is the step that makes competitive equilibrium an equilibrium of a game: the market participant's price choice constrains the consumers' budget sets. The same result gives existence for generalized Nash equilibrium problems, including games with shared constraints. Replacing convexity by contractibility also admits non-convex best-response sets: a contractible set such as a star-shaped region or an arc qualifies. Nash's theorem for finite games and von Neumann's minimax theorem are special cases. With values in , payoffs may take infinite values.
The formalization. The theorem was proved in 1952. None of it is formalized on the platform: neither the theorem itself, nor the LEMMA, nor the topological vocabulary of polyhedra and contractible sets used here. Brouwer's theorem is available on the platform as AGT.brouwer_fixed_point. Nash's existence theorem for finite games (AGT.nash_existence) and Sion's minimax theorem are also formalized. All of these assume convexity. The mission produces a machine-checked existence theorem for generalized games, together with a fixed-point theorem for set-valued maps with contractible values on polyhedra.
Most of the argument reduces to the LEMMA, which is a particular case of the Eilenberg–Montgomery fixed-point theorem. The usual route to Kakutani's theorem does not carry over: it approximates a convex-valued map by continuous selections and applies Brouwer's theorem on a convex set. Contractible values do not admit convex combinations of nearby values, and a contractible polyhedron need not be convex, so neither the selection step nor Brouwer on a simplex applies directly. Debreu cites the LEMMA without proof, and Mathlib has no fixed-point theorem for set-valued maps and none of the algebraic topology of polyhedra that the classical results rest on.
The remaining steps are point-set topology. The product milestones require building homeomorphisms and deformations on products of subspaces, and the closed-graph steps require care with continuity on as opposed to continuity everywhere.
Fintype. Profiles live in . The others' actions range over the product over the subtype , so cannot depend on agent 's own action. With a single agent this product is a point, and the theorem becomes the one-agent statement.EReal with its order topology. is a supremum (sSup) in EReal; under the hypotheses it is attained, so it is Debreu's Max. No arithmetic in EReal is used anywhere.Three formalizations would be easier but are not this theorem: one that replaces contractible by convex (that is the Kakutani–Nash setting), one that maximizes over all of instead of , and one that assumes a fixed point of or states only the closed-graph step. None of these is acceptable, and the LEMMA may not be weakened to convex domains or convex values.
The work needed includes a small library of polyhedra and contractible subsets, and closed-graph correspondences on products. The largest piece is a proof of the LEMMA, a fixed-point theorem that is reusable well beyond this mission. Proofs of any milestone, alternative routes to the LEMMA, and supporting lemmas on polyhedra, such as compactness, triangulation or being absolute neighbourhood retracts, are all welcome.
The stable set problem asks for a largest set of pairwise non-adjacent vertices in a graph; its size is the stability number . It is NP-hard in general, and a standard way to attack it in integer programming is to write down linear inequalities valid for all stable sets and solve the resulting linear program. The weakest such relaxation uses only the edge inequalities ; its optimum can be as large as on graphs with small . Adding, for every odd circuit , the inequality gives the odd-cycle relaxation, the first strengthening that cuts off the fractional point on odd cycles.
Section 7 of V. Chvátal, On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154, doi:10.1016/0095-8956(75)90041-6) identifies a graph class on which this relaxation is exact for the all-ones objective, with an integral certificate on the dual side: the series-parallel networks. The paper conjectures (Conjecture 7.3) that for these graphs the odd-cycle inequalities describe the whole stable set polytope; graphs with that property were later called t-perfect.
Timeline:
All graphs are finite, undirected and loopless, with no parallel edges. A stable set is a set of vertices no two of which are adjacent. We write for the degree of .
A set induces an odd circuit if the induced subgraph is a cycle of length with ; triangles count, and such a cycle has no chords. is the set of all such . The odd-cycle system of is
Its linear programming dual for the objective , with read as sign constraints, has variables , , and reads
A homeomorph of is a graph obtained from by subdividing its edges into paths through new vertices of degree two. is a series-parallel network if no subgraph of is a homeomorph of .
For every series-parallel network ,
and there is a zero–one dual feasible whose dual objective equals the minimum over all real dual feasible points. Both optimality claims are against real points. Chvátal's statement has no constants to improve; the formal goal is his theorem as printed.
The result. Theorem 7.1 says that on series-parallel networks the odd-cycle relaxation computes exactly, and that the optimum is certified by a covering of the vertex set by single vertices, edges and chordless odd circuits whose total weight equals . This is a min–max theorem of König type for a non-bipartite, non-perfect class: odd cycles of length at least five are series-parallel and not perfect, so the clique inequalities of the perfect-graph theory (mission I of this series) do not suffice here. The statement is the unweighted case of the later polyhedral results of Boulala–Uhry and Gerards–Schrijver, and the combinatorial core (milestone 3) is the basis of a polynomial algorithm for on this class, as the paper remarks.
Formalizing it. The theorem has been proved since 1975; neither Mathlib nor the Prove2Me library contains a formal proof of it. A formal proof needs a working notion of graph subdivision (topological minor), which Mathlib does not have, Dirac's degree theorem, the induction of the paper with its four cases, and the passage from the combinatorial core to a pair of LP optima through weak duality. Each of these is reusable: topological minors and the -subdivision-free class appear throughout structural graph theory.
The combinatorial core is proved by induction on removing a vertex of degree at most two, and three of the four cases are routine. The obstacle is Case 4 (, neighbours non-adjacent): deleting alone loses the information needed to recover and , so the proof identifies the two neighbours. That requires the class to be closed under this identification, a statement about subdivisions that is not a local edge count, and a lifting of from the reduced graph with a case split on the component of containing the merged vertex. A second gap is between and the dual: an odd-circuit component of may have chords in and so need not lie in , and the zero–one dual solution must be extracted from it. Finally, Dirac's theorem itself is the one place where the absence of subdivisions is used positively, and it is not a consequence of a degree-counting argument.
Graphs are SimpleGraph V on a Fintype V with decidable equality and decidable adjacency. is a Finset (Finset V) whose members induce a subgraph isomorphic to Mathlib's cycleGraph (2k+1), . The dual variables are indexed by V, by the edge set G.edgeSet, and by the subtype of ; is a sign constraint with no dual variable. "Contains a homeomorph of " is encoded by four distinct branch vertices and six paths (Walk.IsPath) that avoid other branch vertices and meet only at common endpoints; it is not the -minor notion and not the series–parallel composition notion, whose equivalence with it is not part of the paper.
Conventions and implicit hypotheses made explicit:
Corollary 7.2 (stated without proof) and Conjecture 7.3 are not part of this mission. Contributions welcome: a general topological-minor library, Dirac's theorem, and a proof of the combinatorial core.