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?
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 .
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.
Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.
Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor over a -approximate one-machine schedule, which is when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio . In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.
Timeline of the relevant results:
There are jobs and identical machines. Job has a processing time and a weight ; every job is available at time (there are no release dates).
The precedence constraints form an in-tree (more generally, an in-forest): every job has at most one immediate successor , and following successors never returns to the start. Write if is reached from by following successors one or more times.
A feasible schedule on machines gives each job a start time and a machine; a job runs without interruption for time units; two jobs on the same machine do not overlap; and implies that starts no earlier than completes. The completion time is and the value of the schedule is .
The critical-path length (Definition 4.1 with no release dates) is if has no predecessors and otherwise.
A list is an ordering of the jobs that obeys the precedence constraints. It defines the one-machine schedule that runs the jobs in list order without idle time; its completion times are , the total processing time of the jobs up to and including in the list. An optimal one-machine schedule is a list minimizing .
List scheduling (Graham's rule, footnote 3 of the paper) on machines with list : whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.
Let be an optimal one-machine schedule and the list schedule on machines with list . Then for every feasible -machine schedule ,
Lemma 4.16 (any precedence-respecting list , with its idle-free one-machine schedule ): for every job ,
Lemma 4.10: , i.e. for an optimal list and every feasible .
Lemma 4.11: , i.e. for every feasible on any number of machines, and the value is attained by a feasible schedule on machines.
The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor for a strongly NP-hard problem, halving the factor that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a share of its one-machine completion time, so the same bound applies to other objectives built from completion times.
Formalizing it. The paper's proof is complete and short, but it argues about events at a time (jobs that finish exactly at , jobs that become ready at , machines freed at ) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.
List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form holds only if such idle time can be accounted for by 's own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.
Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits only in lower-bound instances elsewhere; the bounds here assume .succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.
Minimizing the sum of weighted completion times is one of the standard objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. With release dates or precedence constraints the problem is NP-hard already on one machine, and on identical parallel machines it is harder still, so the literature of the 1990s concentrated on approximation algorithms. Many of these, including LP-based ones, are naturally designed for a single machine, where an order of the jobs determines the schedule.
Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) gave a generic way to move from one machine to many. Their §4 describes an algorithm, Delay List, that takes any one-machine schedule as a priority list and produces an -machine schedule, and proves that a -approximate one-machine schedule yields a -approximate -machine schedule for every . The guarantee holds with release dates and arbitrary precedence constraints simultaneously, which at the time gave the best bounds known for several special cases, for example a factor 4 for series-parallel precedence without release dates.
An instance has jobs . Job has processing time , release date and weight . Precedence constraints form a strict partial order : means that may start only after completes.
A feasible nonpreemptive schedule on machines assigns each job a start time and a machine; each job runs uninterrupted for time units on its machine, two jobs on one machine do not overlap, , and whenever . The completion time is and the value of the schedule is . A one-machine schedule is the case .
The critical-path length (Definition 4.1) is for a job without predecessors and otherwise; it is the earliest time could complete with unlimited machines.
A list is an ordering of the jobs. Delay List with parameter processes time continuously. A job is ready once it is released and all its predecessors have completed; is the time it becomes ready. The head is the first unscheduled job of the list. Idle machine-time is recorded as charged to jobs. Whenever a machine is idle:
For a job , is the set of jobs up to and including in the list, the set after it, the set of jobs of started before , and . Definition 4.4 builds from the schedule a backward path ending at , whose length is .
Let be a feasible one-machine schedule of the instance with for every feasible one-machine schedule . Let and . Every Delay List schedule built on the completion order of satisfies, for every feasible -machine schedule ,
A further item states that a Delay List schedule exists for every instance and every list, so that the goal does not hold vacuously.
The result. Theorem 4.13 turns every one-machine approximation algorithm for weighted completion time with release dates and precedence into an -machine algorithm at a bounded loss. With an optimal one-machine schedule and the factor is (Corollary 4.14, for series-parallel orders), and the bounds are job-by-job (Theorem 4.9, Corollary 4.12), which the paper uses in Remark 4.15 to extend the method to other metrics and to one-machine schedules that ignore release dates. The same algorithm is the engine of the paper's -approximation for parallel machines with release dates (§4.5).
Formalizing it. The theorem has been proved since 1997 (SODA) and 2001 (journal). There is no machine-checked version of it or of any of its lemmas, and the platform currently has no model of scheduling with release dates and precedence constraints. A formalization produces a precise specification of Delay List, whose informal description is given in discrete time and repaired in a remark; a checked proof of the charging argument; and reusable lower bounds (Lemmas 4.10 and 4.11) for any later work on parallel-machine scheduling with precedence.
The obvious attempt, list scheduling (start the first available job of the list whenever a machine is free), fails with non-identical processing times: a long job taken out of order can occupy a machine and delay a more valuable job that becomes ready shortly afterwards. Delay List allows out-of-order jobs only against accumulated idle time, and the analysis rests on a charging invariant. Stating it needs care about time (the paper's discrete-time exposition can over-charge by a time unit), about which idle time a charge consumes, and about many jobs being scheduled at one instant. The bound must hold simultaneously for release dates and arbitrary precedence constraints, where idle machines can be forced both by jobs that are not yet released and by chains of predecessors, and it must hold for every tie-breaking choice of the algorithm.
Jobs are Fin n, machines Fin m, and times are real numbers. Processing times are positive, release dates nonnegative and weights positive, as in §1. Precedence is a strict partial order, the transitive closure of the paper's DAG; , readiness and feasibility are unchanged by taking the closure. The optimum is never a real infimum: "within a factor of an optimal one-machine schedule" and "within a factor of an optimal -machine schedule" are inequalities against every feasible schedule of the same instance, with the same release dates and precedence constraints.
Delay List is formalized in the continuous-time version described in the proof of Fact 4.6, as a predicate on runs that records start times, machines, the order in which jobs are scheduled at equal times, and charge windows. A case-2 charge takes the most recent uncharged idle time, and idle time is charged by whole time slices. Every guarantee is claimed for every run satisfying the predicate. The ties in Definition 4.4 are broken arbitrarily, so statements involving hold for every admissible path. Lemma 4.10 uses nonpreemptive one-machine schedules. Lemma 4.11's is modelled by machines.
It would be trivializing to assume the conclusions of Fact 4.6 or Lemma 4.7 as properties of the run, or to measure against a relaxation without release dates or precedence; both are ruled out. The algorithm's rules are the only hypotheses on the run.
Not stated: the running time of Delay List; the discrete-time algorithm; Corollary 4.14 (it needs a formal class of series-parallel orders and the external one-machine algorithm of Adolphson for them); Remark 4.15 (release-date-free one-machine schedules), whose hypotheses the paper does not pin down; and the extension to delays between jobs. Contributions of general infrastructure, such as idle-time accounting for step functions and lemmas about list schedules under precedence, are welcome and reusable beyond this mission.
Minimizing the average completion time of jobs that arrive over time is a basic objective in machine scheduling. It measures how long a job spends in the system on average. With several identical machines, release dates and no preemption (written ), the problem is strongly NP-hard already on one machine. Research has therefore looked for approximation algorithms: polynomial-time rules whose total completion time is provably within a constant factor of every feasible schedule.
A common approach solves a relaxation that is easy to optimize and converts its solution into a feasible schedule. Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1), 2001) use a relaxation that needs neither linear programming nor dynamic programming: pretend that the machines are one machine that is times as fast, and allow preemption.
Timeline:
An instance has jobs and identical machines. Job has a processing time and a release date .
A feasible schedule gives each job a start time and a machine. Job runs without interruption on its machine during , and two jobs on the same machine never overlap. The completion times are and the objective is . denotes the completion times of an arbitrary feasible schedule, against which every bound is stated.
The one-machine relaxation has the same jobs and a single machine. Job has processing time and release date in , and may be preempted. A preemptive schedule of gives each job a processing rate . The rates sum to at most at each time, and no job is processed before its release date. Each job receives units in total. Its completion time is the first time by which all of it has been processed. is optimal if is minimal among all such schedules.
A list is an ordering of the jobs, and the completion order of lists the jobs by nondecreasing . Two ways of turning a list into an -machine schedule are compared.
With optimal, its completion order, the strict-order list schedule of and a Delay List schedule of with , every feasible schedule satisfies
The printed lemma says . Its proof gives , which is stated here.
In the order the proof uses them:
Two existence statements accompany them. One says an optimal exists. The other says a Delay List schedule exists for every list and every .
The result gives a -approximation for that is simple to state and runs in time. It improves the bound of Chakrabarti et al. Neither of its two algorithms achieves the ratio alone. It comes from an analysis in which each algorithm is good exactly when the other is bad. List scheduling is good when processing times are small relative to the optimum. Delay List is good when release dates are small. The inequality (4.2) connects the two cases.
The component results are reusable beyond this paper. The one-machine relaxation lower bound (Lemma 3.1) and the bound for list scheduling from it (Lemma 3.2) apply to any conversion from a fast single machine. The per-job bound of Theorem 4.9 is the core of the Delay List technique. Its general form, with precedence constraints, drives the paper's results for precedence-constrained scheduling.
All results are proved in the paper. None of them has a machine-checked proof that this mission knows of. A formalization would check the Delay List charging argument, which the paper states only in discrete time and adapts to continuous time in one sentence. It would also produce reusable Lean definitions of parallel-machine schedules with release dates and of list scheduling.
The arithmetic of the goal is routine once the milestones are in place. The substance lies in two places.
The first is Lemma 3.1 together with the "standard makespan argument" behind (3.2). The one-machine relaxation must be related to the -machine schedule, and to the list schedule, with care about release dates. In particular, in the list schedule every machine is busy between the last release among the first jobs of the list and the start of the -th job. Proving this needs the strict order.
The second, and harder, is Theorem 4.9. The obvious argument bounds the waiting time of job by the work of the jobs ahead of it, but Delay List lets later jobs jump ahead. The idle time before starts and the work of the jobs that jump ahead of it must both be controlled, and the paper's charging argument for this depends on where charged idle time lies on the time axis and on which jobs charged it. Making that bookkeeping precise for a continuous-time algorithm is the main formalization cost.
Jobs are Fin n and machines Fin m with . Times are real, processing times are positive and release dates nonnegative. There are no weights and no precedence constraints. "Optimal" is never an infimum. Every bound is stated against every feasible nonpreemptive schedule, and 's optimality is the hypothesis that its total completion time is at most that of every preemptive schedule of .
Committed conventions:
Fin n ≃ Fin n. A list of may break ties in completion time in any way, and every such list is covered.The statement cannot be made easy by the hypotheses. Two existence items show that an optimal and a Delay List schedule always exist, so no statement is vacuous. The bound is against every feasible schedule, not against the relaxation's value.
Not stated: the running time, the on-line version of §3's algorithm, and Delay List with precedence constraints (Theorem 4.9 in general, which is the subject of mission III of this series). Contributions welcome: proofs of the milestones, and reusable lemmas on list scheduling with release dates.
A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.
In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.
Demand for the season has law on , distribution function and density . As in §3 of the paper, , is strictly increasing on , on , and the generalized failure rate is strictly increasing (IGFR). The expected sales from available units are
The retail price is , the unit production cost , the salvage value , with .
A contract is a pair of wholesale prices . Before production the retailer submits a prebook order of units at . The supplier then produces . During the season, after running out of prebooked stock, the retailer places at-once orders at , filled from the supplier's remaining stock. Pull is ; an advance-purchase discount is . In §5.1 the supplier pays an extra shipping and handling cost per at-once unit. The profits are
A supplier best response to maximizes over . An outcome of is a pair with a best response to and maximizing when every alternative prebook is followed by a best response to it.
Fix and , and suppose the retailer does not prebook under the pull contract : is his unique best reply, followed by the supplier's best response . Then there is with
such that has an outcome, and every outcome of it satisfies
Without shipping costs, advance-purchase discounts with coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.
The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.
The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as . That limit involves , which the model does not provide: is differentiable only on , and for gamma demand with shape above the density vanishes at , so the paper's limit is . A proof of the goal must therefore not rest on the limit display alone.
The second obstacle is the retailer's global choice. The calculus concerns prebooks below the supplier's production . Once , the retailer might instead prefer a prebook at least , turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for close to requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at .
Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on only, so the exponential law is admitted. Quantities range over . Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for , and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue . The prebook function in milestones 5 and 6 is a function pinned on by Eq. (22), which determines it uniquely.
Readings of the paper's words:
A version of the goal that assumed , assumed , compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with , would be weaker than Theorem 8 and is not the target.
A complete development needs the concavity and first-order conditions for , the inverse-function derivative for , and the regime comparison between prebooks below and above . The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.
A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.
The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.
Demand is a random variable with distribution function and density . The paper assumes , strictly increasing, and an increasing generalized failure rate (IGFR): has . Production costs per unit, the retail price is , and leftover units are salvaged for , with . Expected sales with units available are
and the integrated supply chain's expected profit is . It is maximized at with ; write . The efficiency of a contract is , where is the quantity produced.
A contract is a pair of wholesale prices with . The retailer first prebooks units at each. The supplier, seeing , produces . During the season the retailer sells the prebook and, once it runs out, places at-once orders at per unit from the supplier's remaining stock, provided . The supplier's and retailer's expected profits are
with the at-once terms absent when . An outcome of a contract is a pair where maximizes the supplier's profit given , and maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push (), pull () and advance-purchase discount (). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).
For every with , the contract has an outcome and is Pareto; every outcome of every Pareto contract satisfies
and for every some contract with has an outcome with payoffs
A further draft theorem states the step of the proof in which the retailer's outcome profit along falls strictly from to as rises from to .
The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces ; the prebook price then acts as a pure transfer. Every division of is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.
The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.
The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when . Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook always being available and on . Third, the division claim is surjectivity of the retailer's equilibrium payoff over , which needs the solution of to vary continuously with , including at both ends ( at , at ).
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The standing assumptions are a structure: , strictly increasing on , on , and on . Differentiability is required only on , so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over . is a parameter with the hypothesis ; its existence is part of milestone 1.
Readings of informal words: "includes all" means every contract with has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the family; "any division is achievable" is surjectivity onto ; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is " is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when (p. 226, "with push , so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires (p. 228 sets aside as Pareto inferior); pull includes (the paper's remark in the proof) and advance-purchase discounts include (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.
Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of as would turn the goal into algebra, and is ruled out.
Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of , and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.
A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.
Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.
Demand has distribution function and density . The paper's standing assumptions (§3, p. 225) are: , strictly increasing, and the generalized failure rate strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost to produce, sell at the retail price , and are salvaged at .
Expected sales with units available are , and the integrated chain earns . It is maximized at the newsvendor quantity , , with ; the efficiency of a contract is .
A contract is described by the quantity it induces.
Write and (the hazard rate). The retailer's preferred pull contract is and the supplier's preferred push contract is .
A contract Pareto dominates if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.
A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks and the supplier then chooses her production to maximize . A pull contract survives the push challenge if the retailer's profit is strictly highest at .
There is a quantity , , the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that
and every pull contract with survives the push challenge.
The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ( for the supplier, for the retailer) is Pareto, and the least efficient Pareto contract, , is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself.
The results are proved in the paper, with the calculus informal, the unimodality of cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).
The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of (Lemma 1), and that fails to be routine at , where need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records , strictly increasing on , on , and for . Differentiability is not required at : the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy ; no sign is imposed on . Quantities range over . The paper's is a parameter characterized by , and the first milestone proves it exists and is unique.
Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.
Readings of informal words, each named in the item concerned:
The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. , , and are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.
Welcome contributions: basic facts about , and under the demand assumptions, reusable across the series' other two missions.
In the predict-then-optimize framework, a machine-learning model predicts the cost vector of a linear optimization problem , and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by when the true cost is . El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.
The SPO loss is discontinuous in : its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and balls with .
Let be a finite-dimensional real vector space with a norm (the paper's with a generic norm). A cost vector is a linear functional on ; its value at is written , and its dual norm is . The closed ball of radius around is .
The feasible region is nonempty, compact and convex. An optimization oracle is any map with and for all ; no tie-breaking rule is fixed.
If is compact, not a singleton, and -strongly convex for some , then for every oracle ,
The strength parameter equals the strong convexity constant.
Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with , so the Lipschitz constants in the margin analysis are explicit; and , so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).
The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.
Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant . Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of over a ball to be attained and equal to , a fact about dual norms whose attainment depends on finite dimensionality.
For , comparing with gives only the inequality ; equality needs every nonzero cost vector to have a unique minimizer over . The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.
StrongDual ℝ E), so is c w and the operator norm is the dual norm; balls are Metric.closedBall.S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.Metric.infDist to the degenerate set; the parameter conditions and are hypotheses of the theorems, not parts of the predicates.