Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Hirsch conjecture, stated by Warren M. Hirsch in a 1957 letter to George Dantzig, asserts that the combinatorial diameter of a -dimensional polytope with facets is at most . The diameter is the largest number of edge steps needed to walk between two vertices of the polytope. The question matters to linear optimization: every edge-following pivot rule of the simplex method, starting at a vertex of the feasible region, needs at least as many pivots as the graph distance to an optimal vertex. A polynomial bound on polytope diameters is a necessary condition for a strongly polynomial simplex method, which is still unknown.
Timeline of the conjecture before the counterexample:
The polynomial Hirsch conjecture, which asks only for a bound polynomial in and , remains open.
A polytope in is written as . A facet presentation is one in which has nonempty interior and no inequality is redundant. For a bounded polytope it then has dimension , and its inequalities correspond one to one to its facets. A step between two vertices crosses an edge (a one-dimensional face). The polytope is non-Hirsch when its diameter exceeds .
A spindle (Santos, Definition 1.4) is a polytope with two distinguished vertices such that every facet contains exactly one of them. Its length is the graph distance from to . The polar objects are prismatoids: polytopes with two parallel facets containing all vertices, whose width is the dual-graph distance between and .
Santos's explicit object is the 5-prismatoid whose vertices are the 48 rows of Table 1 of the paper: with and with . Its polar is a spindle with apices and . Table 2 of the paper lists the 322 facets of , which are the 322 vertices of : and the points of twenty types with sixteen sign patterns each. The symmetry group of has order 64; its index-two subgroup preserves and .
The goal fixes the dimension (43) and the number of facets (86), as the paper does. It does not assert the exact diameter (44, remarked on p. 24).
Corollary 1.7 settles the Hirsch conjecture in the negative. Theorem 1.5 is the reusable part: it turns any spindle whose length exceeds its dimension into a counterexample. That made the later search for small spindles (Matschke–Santos–Weibel) a finite, low-dimensional problem. Theorem 1.6 is the concrete certificate. Its claims about Tables 1 and 2 are finite statements about explicit rational data.
The result is proved, and several pieces are already formalized on Prove2Me. Hirsch.santos_counterexample (Proved) states that some polytope violates the bound , with no dimension or facet count. Hirsch.strong_dstep_spindle (Proved) is the "in particular" clause of Theorem 1.5, counting inequalities rather than facets. Lemmas 2.2 and 2.4 of the paper are Proved in polar form (Hirsch.spindle_inward_row_push_graph, Hirsch.spindle_wedge_vertex_graph_projection), as is the bound for spindles (Hirsch.spindle_n_ge_two_d). This mission adds the dimension-43, 86-facet statement with facets counted exactly, the general length bound with the spindle structure preserved, and a machine-checkable account of Santos's specific spindle.
The obvious first idea for the 5-dimensional milestones is brute computation. This is feasible in principle but heavy in Lean. Showing that 322 given points are extreme requires exhibiting, for each, five linearly independent tight rows among 48. Showing that no other vertex exists requires a complete enumeration argument rather than a membership check. Exact distance 6 requires the full adjacency structure between the 322 vertices, not only a path.
For the general theorems, the difficulty is that the construction is a one-point suspension followed by a perturbation. Edges and facets of the new polytope must be controlled, with the face lattice changing only in a prescribed way. Diameter is not monotone under arbitrary perturbations, and in particular a walk can become shorter. Keeping the facet count exact (not merely the inequality count) adds an irredundancy argument at each step.
Polytopes are H-presentations Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d), from the platform definition Hirsch_model. "A -polytope with facets" is boundedness plus IsFacetPresentation: nonempty interior and every row irredundant. Without this predicate, padding with redundant rows would change the bound , and the statement would collapse to the platform's dimension-free Hirsch.santos_counterexample. Diameter and length use the platform's padded walks (Hirsch.DiamLE, Hirsch.Reach). "Length at least " means no walk of fewer than steps, and "length exactly " adds a walk of steps. The junk-valued Hirsch.gdist is never used.
All prismatoid statements of the paper (§3, Theorems 2.6, 3.1, 4.1) are stated for the polar spindle, which the paper licenses (pp. 6, 8, 9). Vertices of become rows, facets of become vertices, the width becomes the apex distance, and become . Natural-number expressions , , are faithful because spindles have . Theorem 1.5's "length " is read as "length at least ", which is equivalent by monotonicity. Tables 1 and 2 are written entry by entry in Lean in the page's order.
Useful contributions include proofs of the finite Table 1/Table 2 facts by certified computation, reusable lemmas on one-point suspensions and on facet presentations under perturbation, and a proof of Corollary 1.7 from milestones 5 and 7.
Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.
Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy , whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of affinely independent points of . Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.
Let , , , and let be an uncertainty set. The problem is
Here is the first-stage decision and is the second-stage policy; all inequalities between vectors are componentwise. The value is the same minimum restricted to affine policies with and ; an affine policy must still satisfy for every . Always .
The instance of (6) is defined for and an even integer . It has , , , , and
where , is the -th unit vector for , has entries in its first coordinates and in the others, and has in its first coordinates and in the others. Thus is generated by nonzero points. The last two are also extreme points when ; for or they lie in the convex hull of .
For a permutation of , write . A set is permutation-invariant with respect to if (Definition 2), and is the set (10) of permutations with .
Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach . The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to for sets with polynomially many extreme points and prove a matching upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.
The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values and , and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.
The upper bound requires a feasible policy, which can be written down. The lower bound on is a statement about all affine policies, an dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most yields only , not the strict inequality.
Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, is B *ᵥ x and is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate is index , so "" is (i : ℕ) < m / 2, with natural-number division (exact since is even). is x ∘ τ for τ : Equiv.Perm (Fin m).
and are the infima of the sets of real numbers for which some feasible (respectively feasible affine) solution satisfies for all . This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value , which is why Lemma 1 also asserts the existence of the feasible solution of cost . Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on , as in (1).
The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional , feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: , even and . For the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most , which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis . Definition 2 prints ""; the formalization reads as the set .
Replacing by the cost of one particular affine policy, stating the goal with , or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.
A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in with infinitely many constraints indexed by , reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with . Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.
Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage decision is chosen after the parameter is observed, so that the second stage may depend on arbitrarily. The objective is the worst case over an uncertainty set of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.
Optimizing over all functions is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) ; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.
Timeline of the relevant results:
Let , , and . The problem of model (1) is
where inequalities between vectors are componentwise. A pair satisfying the constraints is feasible; its worst-case cost is . A feasible pair is optimal when its worst-case cost equals , and an affine policy is a second stage of the form with , , still required to be nonnegative on . The value is the same minimum restricted to affine policies.
A simplex in is the convex hull
of affinely independent points, that is, points for which are linearly independent. The proof works with the matrix , the matrix of display (2), and the affine rule . In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.
If with affinely independent and is feasible, then there exist , and such that
is an optimal solution of , optimal among all (not only affine) two-stage solutions. In particular .
The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:
The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix and and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with extreme points the best affine policy can already be worse by a factor , and that on sets with exponentially many extreme points the gap can be ; Section 6 uses a dominating simplex, on which affine policies are exact, to build an -approximation for general . The theorem also says that on a simplex the whole adaptive problem reduces to scenario copies of a linear program.
Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.
Two steps are not routine to formalize. First, the paper starts from "an optimal solution ", that is, it assumes the minimum in (1) is attained. Over arbitrary functions this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of points to invertibility of the matrix , and the identity requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing and as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.
Vectors in are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at , Lean's at : is v (j-1) and is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of is the hypothesis that all vertices are nonnegative (the page writes , a slip for ). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values and are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.
The goal must not be replaced by , by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention , or the interpolant.
A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.
Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a -regular graph is governed by the Alon–Boppana bound , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( with prime) and special numbers of vertices (orders of or ). Applications often need a graph of a prescribed size .
N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on vertices can be enlarged to vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.
Let be a finite set of vertices. A -graph is a -regular graph on vertices whose adjacency matrix satisfies for every nontrivial eigenvalue , that is, every eigenvalue other than the top eigenvalue of the constant vector . For a symmetric with , the nontrivial eigenvalues are those with an eigenvector satisfying . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry of .
Fix an integer and let be an -graph on , a -regular Ramanujan graph. Let be new vertices and let be pairwise disjoint sets of vertices each. Put and . The graph on is obtained from by joining each to every vertex of and adding one loop at each vertex of . Its adjacency matrix is
where is the adjacency matrix of (zero on ), that of the stars joining to , and the diagonal matrix of the loops. Every vertex of has degree .
The paper states for ; its proof gives , which is stronger, and the error term it produces is . The goal is parametrised by , and the sets , so it does not depend on how and are chosen.
With the Lubotzky–Phillips–Sarnak graph on vertices for the largest suitable prime with , and , the distribution of primes in arithmetic progressions gives , and the goal yields an explicit -graph with for every sufficiently large . This is within a factor of about of the Ramanujan bound , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.
The result is proved in the paper. No formalization of it, of the notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.
The vertices of and lie in the old graph , whose spectrum is controlled, but the new vertices of are not; and a vector orthogonal to on need not be orthogonal to the constant vector on . Bounding by applying the Ramanujan bound for to restricted to therefore fails: the restriction has a component along the trivial eigenvector of , whose eigenvalue is large. The argument must show that this component is small, of order , and must balance the star edges between and against the loops on so that every vertex class gets the same coefficient. The naive bound added to for and for gives a constant larger than ; the stated constant needs the weighted estimate.
On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace , while Mathlib states the spectral theorem for the whole space.
SimpleGraph with adjMatrix.Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy after iterations, where and are measured in the Euclidean norm; on the simplex this hides a factor of order in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to .
Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance . This viewpoint gives a short convergence proof, and with the entropy as it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.
Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the potential , , whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same rate with a closed-form update.
Let be with an arbitrary norm , and the dual norm. The problem is under Assumption A: is closed and convex; is convex on and Lipschitz there, ; has a minimiser ; and a subgradient can be computed at every .
Let be strongly convex with parameter and differentiable. The distance-like function (3.10) is
The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from and sets, with step sizes ,
With this is the projected subgradient method.
On the unit simplex take the entropy (5.27), with . SANP becomes the entropic descent algorithm (EDA):
If is convex and -Lipschitz on for , with subgradients satisfying , and the EDA is started at with step for a horizon , then
For any norm, any -strongly convex and any SANP run,
and with the optimal constant step this gives .
The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound , the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on ; then for the simplex, the 1-strong convexity of for (Proposition 5.1(a), Remark 5.1), the bound (Proposition 5.1(c)), and the identification of the EDA with SANP.
The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy in iterations, with measured in the dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.
Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.
The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in ). The bound must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over , which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from to and the strong convexity constant of the entropy, and loses the rate.
Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, is its value at , and is the operator norm. is the Fréchet derivative. Iterates are indexed from . A SANP run is a predicate on sequences: each step size is positive, each iterate lies in , is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces " has nonempty interior" and "". Section 5 works on as functions with explicit and sums; is the relative interior, and the entropy formula is evaluated on only. "" is stated as the existence of with .
Added hypotheses, each disclosed in the item: a bound on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to ); in Proposition 4.1, without which the proposition as printed is false; in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon , which is what the proof chooses; Theorem 5.1 is stated with , since the free index in the printed bound (5.28) cannot be bound, and is what the proof yields.
Trivializing formalizations are ruled out: is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of over the run, and the step is not an anytime schedule .
A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.
The newsvendor problem is the basic model of inventory under uncertain demand. A decision maker orders units before demand is observed, and pays a unit backordering cost for each unit of unmet demand and a unit holding cost for each unit left over. When the demand distribution is known, the optimal order is a quantile of it. In practice the distribution is unknown and the decision maker holds historical data, often including features: observable covariates such as the day of the week, the weather or a recent sales trend, recorded alongside each past demand.
Rudin and Vahn (MIT Sloan Working Paper 5036-13, version of February 6, 2014, from MIT DSpace; published as Ban and Rudin, Operations Research 67(1), 2019, doi:10.1287/opre.2018.1757) propose to learn the order quantity directly as a linear function of the features, by minimizing the empirical newsvendor cost over the training data, with or without a regularization penalty. Their question is the one any data-driven decision rule must answer: how much worse can the learned rule do on new data than it did on the data it was fitted to? When the number of features is comparable to the sample size ("big data"), a bound that grows with says nothing, and the paper's Theorem 2 gives one for the regularized rule that does not depend on .
This mission formalizes that bound, Theorem 2 of the working paper, together with the results its proof is assembled from. All page and result numbers refer to the 2014 working paper, not to the published article.
Cost. For an order and a demand , the newsvendor cost is
Write .
Data. A data point is a pair of a feature vector and a demand . Features lie in a domain inside the ball , and demands lie in . A sample consists of independent draws from an unknown probability distribution concentrated on .
Rules and risks. A vector defines the linear decision rule . Its true risk and empirical risk are
The regularized algorithm (NV-reg). For a parameter , the rule minimizes
The objective is strictly convex, so the minimizer is unique. Following Appendix B of the paper, the rules the algorithm outputs on samples from are assumed to map into (the paper's ): the learned order quantity is never negative and never exceeds the demand cap.
Uniform stability. An algorithm is uniformly stable with parameter if removing one observation from any sample changes the loss of its output at any test point by at most (Bousquet and Elisseeff's Definition 6, the paper's Definition 1).
For every and , with probability at least over ,
The dimension appears nowhere in the bound.
The result. Theorem 2 bounds the generalization gap of the regularized feature-based newsvendor rule at rate with constants that depend on the costs, the demand cap, the feature radius and , but not on the number of features. It gives a theoretical basis for regularizing when is not small, and it indicates how to scale with the feature radius. The companion bound for the unregularized rule (Theorem 1) grows linearly in .
Formalizing it. The theorem is proved in the paper, but its proof is short and relies on cited results: Theorem 5 and Theorem 6 are stated with references to Bousquet and Elisseeff and no proof of their own, and the paper's Theorem 6 is a two-sided variant of Bousquet and Elisseeff's Theorem 12 that is only sketched. None of these results has a machine-checked proof. A formalization produces a checked two-sided stability-to-generalization theorem for general algorithms (reusable for any stable learner), a checked stability bound for a regularized piecewise-linear loss, and the newsvendor bound itself, with the constants the proof actually supports.
The bound is not a uniform-convergence argument: the class of linear rules on has complexity growing with , so any bound that holds simultaneously for all rules in the class depends on . The bound must exploit the specific rule produced by the algorithm. The two analytic steps that carry this are the stability of the regularized minimizer, which needs a strong-convexity comparison between the full and the leave-one-out objective, and a concentration inequality of bounded-differences type for a function of the whole sample whose differences are controlled only through stability.
The leave-one-out comparison is a known pitfall. If the leave-one-out problem is run literally on points it carries the weight , and the comparison argument then gives twice the constant of Theorem 4. The stated constant holds for the leave-one-out objective that keeps the weight , which is the form of Theorem 5.
Representation. Features are EuclideanSpace ℝ (Fin p), rules are vectors acting by the inner product, and data points live in EuclideanSpace ℝ (Fin p) × ℝ. The cost is the published newsboy loss with overage cost and underage cost ; the empirical and true risks are the published empirical and generalization errors, and the (NV-reg) objective and its -weighted leave-one-out version are the published regularized objectives of Bousquet and Elisseeff. The regularizer is (the display prints both and ; the text calls the problem a quadratic program). "With probability at least " is stated as: the event on which the gap exceeds the bound has measure at most under the product measure .
Standing assumptions and pinned hypotheses.
Trivializing formalization ruled out. The range assumption is quantified only over feature vectors in and over samples drawn from ; stated over the whole ball , it would force (both and would lie in ) and the goal would be nearly empty.
What is needed and reusable. McDiarmid's two-sided bounded-differences inequality under product measures; integrability of bounded measurable losses; existence and properties of minimizers of strongly convex objectives on ; the comparison argument behind Theorem 5. Theorem 6 is stated for an arbitrary data space and hypothesis space and is reusable for any uniformly stable algorithm. Contributions to the Theorem 5 reference and to McDiarmid's inequality benefit other missions as well.
Prove that -SAT is NP-complete for every fixed , with at most literal occurrences per clause.
Construct the reductions and certificate verifier using the existing WordRAM definitions. We reuse proved polynomial backend and Cook–Levin SAT completeness.
Many systems consist of units that form themselves into clusters: individuals at a gathering forming conversational groups, monomers forming polymers, particles coagulating and fragmenting. Chapter 8 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) treats such clustering processes as Markov processes whose state counts the clusters of each type, and shows that when the process is reversible its equilibrium distribution has an explicit product form. The chapter opens with a model of social grouping (§8.1), develops a general basic model (§8.2) and later applies it to polymerization (§8.4).
The basic model sits in the same family as the migration processes and queueing networks of the earlier chapters: the method is to guess reversibility, solve the detailed balance equations, and normalize. Its specific feature is that the transitions are unions and break-ups of clusters, with rates quadratic in the cluster counts, rather than movements of single individuals.
There is a countable collection of cluster types . A state is a vector of non-negative integers, being the number of -clusters present, with only finitely many non-zero. For cluster types let be the -th unit vector and
the union of an -cluster with an -cluster into a -cluster, and the break-up of a -cluster into an -cluster and an -cluster. Given non-negative parameters and , the clustering process has transition rates
A closed clustering process lives on a finite irreducible state space . The open clustering process additionally lets one-clusters enter at rate and leave at rate ,
and its state space is the countable set of all with finite, every state being reachable from every other.
An equilibrium distribution is a collection of positive numbers summing to one that satisfies the equilibrium equations ; the process is reversible in equilibrium exactly when satisfies the detailed balance conditions .
If there are positive numbers with
then the open clustering process has equilibrium distribution
it is reversible, and the counts are independent, being Poisson with mean .
Theorem 8.2 gives the equilibrium of a whole class of coagulation–fragmentation dynamics in closed form: the cluster counts are independent Poisson variables, and the equation system (8.8) is the only thing to solve. Quantities such as the expected number of clusters of each type, or the proportion of units in clusters of a given size, are then read off directly. Theorem 8.1 gives the corresponding result for a closed system, where the normalizing constant couples the types; opening the system removes that coupling. The results are the base of the polymerization models of §8.4 and of the later literature on reversible coagulation–fragmentation processes.
The results are proved in the book, with short proofs that state the detailed balance computation is "readily verified". To our knowledge they have no machine-checked proof. The work this mission asks for is the formal verification of that computation for the aggregated rate function, including unions in which two clusters of the same type meet, and the normalization of an infinite product over a countable set of types, which the book takes for granted.
The book calls the detailed balance computation readily verified; the bookkeeping is where a formal check can fail. Two different unions, or a break-up and the entry of a one-cluster, can lead from the same state to the same state when a cluster type is reproduced by the transition, so the rate between two states is a sum over transitions, and the identity has to be checked for the sums, not for single transitions. The same-type case carries the falling factorial rather than .
The normalization is the second difficulty. The state space of the open process is countably infinite, the product (8.10) runs over infinitely many types, and the interchange that makes it sum to one requires (8.9). Without (8.9) the weights are not summable; this is the content of the book's remark that (8.9) is necessary.
Cluster types are an arbitrary countable type R carrying a linear order, used only to count each unordered pair of types once. States are finitely supported vectors R →₀ ℕ. The rate is the sum of the rates (8.3) of all unions and break-ups taking to , plus, for the open process, the rates (8.7); a transition is present only when the clusters it consumes exist, and holds because every transition changes the number of clusters. The one-cluster type is a distinguished element one. The closed state space is a finite non-empty set closed under positive-rate transitions and irreducible. The open process carries the book's assumptions that every state is reachable from every other and that the total rate out of each state is finite.
The statements are at the level of rates: reversibility is detailed balance for a positive, normalized , the equivalence with reversibility of the stationary process being Kelly's Theorem 1.3. That is the law of a stationary Markov process with these rates is not formalized. Independence and the Poisson laws are stated as the joint law of every finite set of counts. A formalization in which may vanish, in which detailed balance is imposed only for a degenerate choice of rates, or in which (8.10) is not normalized does not meet the goal: the are positive, the rates are arbitrary non-negative symmetric parameters, and both detailed balance and total mass one are required.
The development uses the published definitions KellyStochasticNetworks_Balance (detailed balance and the equilibrium equations) and the proved implication from detailed balance to the equilibrium equations. Lemmas on summing products over finitely supported vectors, and on infinite products of exponentials, are reusable beyond this mission. Lemma 8.3, a partial converse to Theorem 8.1, is not part of this mission; a faithful statement of it, with the units structure of the clusters, is a welcome addition.
A migration process is a continuous-time Markov model of a population spread over sites, called colonies, in which individuals move one at a time: between colonies, out of the system, or into it from outside. The model was introduced by Whittle (1967) and Kingman (1969) and is the framework of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979). It covers closed and open networks of queues (Jackson networks), linear population models and the movement of particles between cells. Its central fact is that the equilibrium distribution is a product form: the joint law of the colony sizes factorizes into one term per colony, and for open processes the colony sizes are independent in equilibrium.
In the migration processes of Chapter 2 the rate at which an individual leaves colony depends on the number there, but not on the number already present in the colony it joins. Chapter 6 (§6.1) lifts this restriction. The rate of a move into colony is multiplied by a function of the receiving colony's occupancy, which can model blocking (a crowded colony slows arrivals) or attraction (as in the models of social grouping of §6.2). The price is that product form survives only under a reversibility condition on the routing parameters. This mission formalizes the two theorems of §6.1 on top of the already-formalized results of Chapter 2.
Timeline. Whittle (1967) and Kingman (1969) introduced migration processes and their product-form equilibria; Kelly (1976) treated networks of queues with general routes; Kelly (1979, Ch. 2) states the closed and open product forms (Theorems 2.3, 2.4) and the time reversal of an open process (Theorem 2.5); Kelly (1979, §6.1) states the reversible versions with receiving-colony dependence (Theorems 6.1, 6.2).
There are colonies. The state is , with the number of individuals in colony . Three operators change the state by one individual: moves one individual from colony to colony , removes one from colony , and adds one to colony .
The model is given by non-negative constants (with ), , , and functions with , for , and for all . A closed reversible migration process with individuals has state space and transition rates
An open reversible migration process has state space and, in addition to (6.2), the rates
The parameters are required to make the process irreducible: in the closed case an individual can pass between any two colonies along pairs with ; in the open case it can reach every colony from outside and leave from every colony. Setting recovers the migration processes of Chapter 2.
Given positive constants , the candidate equilibrium is
with chosen so that sums to one over the state space.
If positive satisfy
and every colony series converges, then (6.3) with is in detailed balance with the rates (6.2), (6.5), (6.6), satisfies the equilibrium equations, is positive and sums to one, and under it are independent with marginals .
Theorems 2.3–2.5 are already proved on the platform and enter as references.
The result. Theorem 6.2 shows that product form and independence of colony sizes are not tied to routing that ignores the destination's occupancy. Any positive is allowed, provided the routing is reversible in the sense of (6.4) and (6.7). This is what makes the social-grouping models of §6.2 and the clustering models of Chapter 8 tractable, and it identifies (6.4) as the structural condition: Exercise 6.1.1 shows that without it the process cannot be reversible. Through Theorem 1.3 of the book, detailed balance also gives that the stationary process looks the same run backwards in time.
Formalization. The Chapter 2 results (Theorems 2.3–2.5) are formalized and proved on the platform, at the level of transition rates, in the KellyStochasticNetworks series. Theorems 6.1 and 6.2 are not formalized anywhere to our knowledge. The new work is the detailed-balance verification with the receiving-colony factor, the normalization over the finite set in the closed case, and the summation over the countable space with the marginal computation that expresses independence in the open case.
The equilibrium equations of a migration process with blocking have no simple solution in general (p. 135); a direct attack on the full balance equations does not close. Detailed balance is a local condition, but the formal statement has to be careful with transitions that do not exist: a move out of an empty colony, a departure that would make a count negative, and the coincidences between operators at the boundary ( when ). In the open case the bookkeeping is in infinite sums: positivity and normalization need convergence of each colony series, and independence needs the marginal of on one colony to be computed as a sum over the remaining coordinates.
Colonies are Fin J; states are Fin J → ℕ; rates are real-valued functions of two states, assembled as sums of indicator terms over the possible transitions, reusing the operators Tjk, Tout, Tin and the predicates DetailedBalance, FullBalance of the published definitions KellyStochasticNetworks_Migration and KellyStochasticNetworks_Balance. Transitions out of an empty colony carry the factor and so vanish. The hypotheses , non-negativity of the rates, positivity of (), () and , and the book's irreducibility requirements are binders of each theorem.
The statements are at the level of transition rates: "reversible" is read as detailed balance of the equilibrium distribution, and "equilibrium distribution" as positive, summing to one, and satisfying the equilibrium equations. The stochastic process itself is not constructed. In the closed case the distribution lives on and vanishes off , which is equivalent because every transition preserves ; is assumed so that is nonempty. In the open case stationarity is the convergence of each colony series, carried as HasSum hypotheses with sums .
The normalizing constant is never free: satisfies detailed balance, so a statement that leaves unconstrained, or omits the factor from (6.2), (6.6) and (6.3), is not this theorem. Contributions welcome: proofs of Theorem 6.1 and 6.2, reusable lemmas on detailed balance for indicator-sum rates, and on products of summable families over Fin J → ℕ.
Linear programming asks for the best value of a linear objective under linear constraints. In the form studied by George B. Dantzig in 1951, all variables are nonnegative and the constraints are equalities. The simplex technique moves between small sets of columns, seeking a feasible vector first and then improving its objective. Its basic promise is operational: a run should end with a valid answer, whether that answer is a maximum, infeasibility, or an objective that can grow without bound. Dantzig's chapter sets out both phases and the tests that distinguish these outcomes.
The formulation matters to readers of optimization because it separates the algebraic claim about a linear program from a particular rule for selecting the next column. The chapter permits any entering column satisfying the stated improvement test. This mission captures the correctness claim for every sequence of admissible choices under the chapter's nondegeneracy assumption, with one additional general-position condition needed for the Phase I argument.
Fix integers . Let be a right-hand side, be columns, and be objective coefficients. A feasible solution is a weight vector with and . Its objective value is . It is maximum feasible when for every feasible . Unboundedness means that feasible objective values exceed every real threshold.
Dantzig assumes nondegeneracy: every indexed selection of points among is linearly independent. A Phase II state uses exactly basic columns , each with a positive weight, and represents with them. Every column has unique coordinates , and is the corresponding objective value. A column with can improve the objective. When some , the step uses the smallest ratio over those positive coordinates and replaces a minimizing basic column.
A Phase I state begins from basic columns and a fixed reference point . Positive weights and satisfy . Write . A column with either gives a new Phase I basis through the positive-ratio test or supplies the nonnegative weights in equation (39), which start Phase II.
The goal is the correctness of the complete two-phase transition system. There is no infinite admissible run. Every state with no outgoing transition has one of three outcomes:
The five milestones follow the chapter's own statements: Theorem 3's infeasibility certificate, Section 2's termination and hand-off, Theorem 1's improving family and two cases, Section 1's termination alternatives, and Theorem 2's optimality test. The goal includes the hand-off from the first phase to the second; the milestones make each outcome separately auditable.
The result gives a complete outcome guarantee for the chapter's procedure under its stated nondegeneracy regime. A terminal basis satisfying is certified optimal against every feasible solution, not just against nearby bases. The other terminal tests certify properties of the original problem: nonexistence of feasible weights or arbitrarily large feasible objective values. This is the distinction needed to use the procedure as an algorithm for an LP rather than merely a local improvement rule.
The chapter's Theorems A and B assert existence of a basic feasible solution, and existence of a basic optimal one when the objective is bounded above. A proved platform theorem on basic optimal solutions covers these structural results after changing minimization cost to ; it is included by reference. Existing simplex results in the platform's minimization convention do not state Dantzig's Phase I reference-point process or his and tests. Formalizing this mission adds that two-phase interface and a machine-checkable statement of its outcomes.
An improving column alone does not say whether another basis exists. In Phase II, the signs of its basis coordinates determine whether the positive weights meet a finite ratio limit or instead continue along an unbounded feasible family. In Phase I, the analogous limit must preserve strictly positive weights on exactly columns. The printed argument says that a coefficient vanishes at the limit, but does not exclude two coefficients vanishing together. That gap matters because the next state in the paper's recurrence must again have strictly positive basic weights. The mission states a general-position condition on that rules out this simultaneous-vanishing case. It is an explicit addition to the printed assumptions and should be reviewed as such.
Lean uses Fin n → (Fin m → ℝ) for the columns, Fin m → ℝ for and , Fin n → ℝ for weights and costs, and finite sets for bases. Its zero-based Fin n labels correspond to the paper's . Each state carries its basis cardinality, independence, coordinate equations, and strictly positive basic weights. This keeps the coordinate functions defined on genuine bases and prevents a zero-weight intermediate state from counting as a valid pivot. The transition relation records every admissible entering column and minimizing leaving index; the pivot-selection heuristics (20) and (21) are outside the claim.
The phrases “upper bound of is infinite” and “process terminates” are read as, respectively, objective values above every real threshold on the original feasible set and absence of an infinite sequence of admissible steps. “A feasible solution has been obtained” is the explicit vector of equation (39), not an unnamed existence assertion. Maximum feasible means feasible plus comparison with every feasible vector, avoiding a real supremum's empty-set default. The dimensions make both kinds of basis possible and prevent a vacuous nondegeneracy condition. General position asks every family containing , , and distinct to be independent. The paper does not write this condition, so its inclusion is a substantive qualification of the target.
The printed indices in (30), (45), and a sentence following (18) do not match their defining ranges. The Lean statements use all columns for and the current Phase I columns for . The indices in (17) and (45) also carry the entering conditions and , respectively. These corrections preserve the paper's described procedure and prevent a terminal test from becoming trivial through a basic column. Contributions may address the finite-state termination argument, the ratio-test lemmas, coordinate uniqueness, and the translation from terminal signs to the three global LP outcomes. The operation counts and geometric interpretation on the last pages are outside the formalization.
In statistical learning, one picks a function from a class to make the population risk small, with access only to an i.i.d. sample from an unknown distribution . Empirical risk minimization replaces by the empirical mean , and its classical guarantees decay like regardless of how concentrated is. Bernstein-type inequalities show that the deviation of from scales with the standard deviation of , so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every is convex in its parameters, which makes it hard to optimize.
J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a -divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order . This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.
Let be a probability measure on a measurable space and , , an i.i.d. sample from with empirical distribution . Let and let be a collection of measurable functions (losses).
with sub-root, and is a point with .
Let and let satisfy (21): . With probability at least , every robust minimizer satisfies
In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,
and the uniform bound (22): with probability at least , for all ,
The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point of a localized complexity bound. For bounded VC classes is of order (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order , faster than the of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).
The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).
The obvious route applies a uniform concentration inequality to and then a Bernstein bound to each . Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity , which yields only rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as . The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling , which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.
Lean conventions. The sample is the coordinate map of the product measure on Fin n → X. Distributions on the sample are weight vectors in the ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for , ). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded ; empirical means and variances are normalized by . The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on . Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is , (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition is part of the page's "root" (and the proof divides by ); with allowed, would remove the complexity term from (21). The condition makes defined.
Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):
UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.
The complexity of computing a Nash equilibrium is usually studied for an approximate equilibrium, because an exact equilibrium of a game with three or more players can require irrational probabilities. Two approximation notions are in use, and results proved for one do not automatically transfer to the other. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) prove their PPAD-hardness results for the stronger notion, the ε-approximately well-supported Nash equilibrium, and then show in their §4.7 (Lemma 4.28, announced as Lemma 2.1) that any ε-approximate Nash equilibrium can be turned, by an explicit and cheap transformation, into an approximately well-supported one with a polynomially worse accuracy. This is what lets their hardness results hold for both notions. A weaker version of the relation had been pointed out by Chen, Deng and Teng (FOCS 2006, reference [9] of the paper).
This mission formalizes Lemma 4.28 together with the steps of its proof: the best-response inequality (28), Claims 5 and 6, and the Lipschitz estimate of Lemma 4.26 (used in the proof as Lemma 4.29).
A game in normal form has players. Player has a finite set of pure strategies; is the set of pure strategy profiles and the set of profiles of the players other than . For each player and profile there is a payoff ; for and the payoff to at the profile is written . The number is the largest entry over all players and all profiles.
A mixed profile assigns to each player a probability distribution on ; the players randomize independently, and for we write . The expected payoff of player for playing the pure strategy against the others is
The trimmed profile of with parameter deletes the strategies whose expected payoff is more than below and renormalizes:
In the Lean development these are purePayoff u x p j, maxPurePayoff u x p, maxPayoff u, IsEpsApproxNash u x ε, IsEpsWellSupportedNash u x ε, trimMass u x ε k p and trim u x ε k, all in the namespace DGPNash.WellSupported.
For and an -approximate Nash equilibrium , the trimmed profile with is a mixed profile and a
The constant is the paper's. The statement is about the specific profile built from , not about the existence of some well-supported equilibrium.
The result. Lemma 4.28 makes the two approximation notions polynomially equivalent for computation: every well-supported equilibrium is approximate with the same , and conversely an approximate equilibrium yields a well-supported one at accuracy for fixed and payoff range. Hardness results proved for well-supported equilibria, including the PPAD-completeness of 3-player Nash in the paper and the two-player result of Chen, Deng and Teng, therefore apply to approximate equilibria as well, and algorithms for one notion give algorithms for the other. Lemma 4.26, the Lipschitz dependence of expected payoffs on the opponents' strategies in , is a general tool for perturbation and rounding arguments in finite games.
Formalizing it. The result is proved in the paper; as far as we know there is no machine-checked version, and the platform has neither approximation notion. The mission produces both definitions, on top of the published game vocabulary agt_games, and the quantitative chain from an approximate equilibrium to a well-supported one. These definitions are what any later formalization of approximate-equilibrium algorithms or hardness results would need.
The obvious attempt, to show that itself is approximately well-supported, fails: an approximate equilibrium may put small positive probability on a strategy that is far from optimal, which a well-supported equilibrium forbids for any accuracy. Removing those strategies changes the opponents' expected payoffs, so the well-supported condition must be checked for , computed from , not for . The accuracy of the result therefore depends on how far all opponents' strategies move, which is why the bound carries the factor . Lemma 4.26 is a statement about product distributions: the change in a multilinear expected payoff is controlled by the sum of the per-player distances, not by their product.
ι with decidable equality; player p has a finite strategy type S p; payoffs are u : ι → (∀ i, S i) → ℝ with the standing hypothesis ∀ p s, 0 ≤ u p s of §2.1. The number of players is Fintype.card ι, and 2 ≤ Fintype.card ι is assumed in every statement, as in §2.1. Strategy sets may differ between players.AGT.IsMixedProfile and AGT.IsLottery from agt_games; both equilibrium notions include the requirement that the profile be mixed. is AGT.expectedPayoff after player alone switches to the pure strategy , and the approximate-Nash condition compares AGT.expectedPayoff before and after player alone switches to a lottery , which is the paper's inequality (27).AGT.nash_existence) a δ-well-supported equilibrium exists for every δ ≥ 0, so the goal is stated for , defined from , and not as an existence claim.Contributions welcome: proofs of the milestones, in particular the decomposition of the expected payoff, which Eq. (28) and the goal both need, and Lemma 4.26, which is reusable in any perturbation argument for finite games.
When many self-interested users share resources whose cost grows with use (links of a network, servers, machines), each user picks the option that is cheapest for them given what the others do, and the resulting equilibrium can be worse for the group than a centrally planned allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures this loss as the worst ratio between the social cost of an equilibrium and the optimal social cost. Congestion games (Rosenthal 1973) are the standard finite model of such resource sharing: they always have pure Nash equilibria, and they cover atomic routing, load balancing and many network design questions.
Timeline of the linear-latency case:
A congestion game consists of a finite set of players, a finite set of facilities, for each player a collection of pure strategies, each a subset of , and for each facility a latency function . In a pure profile , , the load is the number of players whose set contains , and player pays
The social cost of a pure profile is ( times the average cost). Latencies are linear: with .
A mixed strategy of player is a probability distribution on . The players randomize independently, so the pure profile occurs with probability . Player 's expected cost is , and the expected load of is . A mixed profile is a mixed Nash equilibrium if no player can lower their expected cost by switching unilaterally to another distribution on their strategies. The social cost of a mixed profile is the sum of the expected costs, .
In Lean: CongestionGame ι E with fields strategies and latency, load, cost, IsProfile, sumCost, IsLinear, expCost, expLoad, mixedSumCost and IsMixedNash, all in the namespace CongestionPoA.Mixed; lotteries and independent randomization come from the platform definition agt_games (AGT.IsLottery, AGT.profileProb, AGT.IsMixedNash).
For every congestion game with linear latencies, every mixed Nash equilibrium and every pure profile with ,
Taking optimal, the mixed price of anarchy of the average social cost is at most .
The bound says that randomization by the players cannot make linear congestion games much worse than pure play: the loss stays within a constant factor independent of the number of players and facilities. Mixed equilibria matter because they always exist in every finite game and because they model populations of users whose individual choices are not known in advance. The same authors report (PDF p. 2) extending these bounds to correlated equilibria with the same values, which places the mixed bound in a hierarchy of equilibrium notions whose worst cases coincide.
The result is proved in the paper, in one sentence that defers to the proof of Theorem 1. The work here is a complete machine-checked version: the expected-cost layer for congestion games on top of agt_games, the deviation and summing inequalities under product distributions, and the corrected Lemma 3. The paper prints Lemma 3 for all nonnegative reals , where it is false (at , the left side is and the right side about ); the formal statement keeps an integer, which is how the lemma is used. No formalization of congestion-game price-of-anarchy bounds was on the platform when this mission was drafted.
The pure proof compares with and through an integer inequality (Lemma 1). Under a mixed equilibrium the equilibrium side is an expectation, so the cost of a facility is no longer a function of one integer load, and Lemma 1's constant is not available for real arguments: a real-variable version is needed, and the constant degrades from to . A second obstacle is bookkeeping: the deviating player's load changes only on their own deviation, while the other players' randomization stays independent, and the expected cost of a player has to be related to expected facility loads, which uses linearity of the latencies in an essential way. The naive idea of applying Theorem 1 to each pure profile in the support of the equilibrium fails, because those profiles are not themselves Nash equilibria.
Players and facilities are finite types ι and E; profiles are functions ι → Finset E, with feasibility IsProfile a separate predicate. Latencies are real-valued on natural-number loads, and "linear" means affine with nonnegative coefficients, ; the paper displays only the identity latency and states that its proofs extend. Mixed strategies are real weight functions on the finite strategy type ; independence is built into AGT.profileProb; Nash deviations range over all lotteries, which is equivalent to pure deviations. agt_games maximizes payoffs, so the game is passed to it with payoff . The goal is stated against every feasible pure profile rather than as a ratio, so no division by an optimum that may be occurs. The social cost is the expected sum of the players' costs; the paper's second option, , is not part of this mission. A version with correlated distributions on profiles, or one that bounds the cost of an "averaged" profile instead of the expected cost, is a different statement and does not discharge the goal.
A complete development needs elementary finite-sum manipulation of product distributions (marginals of AGT.profileProb, expectations of loads), and a Jensen-type inequality for finite distributions. The expectation lemmas for congestion games are reusable for the other mixed results of the literature (weighted games, polynomial latencies). Proofs of the milestones, of the expectation layer, and alternative arguments are all welcome.
Thompson Sampling is the oldest heuristic for the multi-armed bandit problem: proposed by Thompson in 1933, it plays each arm with the posterior probability that the arm is the best one. It is simple to implement, performs well empirically (Chapelle and Li, NIPS 2011), and has been used in production systems such as click-through-rate prediction for search advertising. For a long time, however, no finite-time regret guarantee was known for it: the analyses available before 2012 gave only regret.
Agrawal and Goyal (arXiv:1111.1797, COLT 2012) gave the first logarithmic bounds on the expected regret of Thompson Sampling. This mission formalizes their bound for the general case of arms (their Theorem 2). A companion mission of the same series formalizes their two-armed bound (Theorem 1), whose proof is independent.
Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least of order . Auer, Cesa-Bianchi and Fischer (2002) showed that UCB1 achieves in finite time. Agrawal and Goyal (2012) proved for Thompson Sampling with arms; Kaufmann, Korda and Munos (2012) and Agrawal and Goyal (2013) later proved the asymptotically optimal constant for Bernoulli rewards.
A stochastic -armed bandit has arms . Arm , when played, yields a random reward drawn from a fixed distribution supported in , with mean ; rewards of an arm are i.i.d. and independent of the other arms. Arm is assumed to be the unique optimal arm, for , and is the gap of arm .
Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm , a count of successes and of failures, both starting at . In each round it draws independently for every arm, plays , observes a reward , performs a Bernoulli trial with success probability , and increments on success and on failure.
The expected regret in time is
the expectation being over the rewards, the Bernoulli trials and the posterior samples.
The proof works with the reward stacks : the outcome of the -th Bernoulli trial of arm , all independent. Then , the number of successes in the first plays of arm , is a random variable. The other objects of the proof are the threshold , the saturated set of suboptimal arms with at least plays before round , the intervals between the -th and -th plays of arm , and the counts and defined in §4.
There is an absolute constant such that for every , every instance as above and every horizon ,
does not depend on , on the reward distributions or on .
The result. Theorem 2 shows that Thompson Sampling, a randomized Bayesian heuristic, achieves regret logarithmic in the horizon for any number of arms with bounded rewards, matching the order in of the Lai–Robbins lower bound. Its dependence on the gaps, , is worse than UCB1's; the paper's own Remark 1 and later work improve it. The proof introduced the device of bounding the waiting time between plays of the optimal arm through geometric variables with Beta-cdf parameters (Lemmas 1 and 3), which reappears in later analyses of Thompson Sampling.
Formalizing it. The theorem is proved on paper; it has not been machine-checked. Bandit theory in Lean (bandit environments, regret, UCB-type analyses) is still young, and no Beta–Bernoulli Thompson Sampling result is formalized. The mission produces a Lean model of Algorithm 2 for general rewards with the paper's stack coupling, the §4 bookkeeping of saturated arms and intervals, and the paper's lemmas as separate targets.
Two difficulties are specific to the -armed analysis. First, the arm that competes with arm changes over time: the set of saturated arms grows, and which saturated arm is "best" depends on the history, so the waiting time between plays of arm cannot be compared with a single geometric variable as in the two-armed case. Second, the number of rounds at which arm 's sample is large but arm is not played is not independent of the counts : both depend on the same posterior samples, and Lemma 5 needs a careful conditioning on the history to separate them. The obvious union bound over arms, treating each suboptimal arm as in the two-armed proof, fails because it ignores the interruptions by unsaturated arms, whose number is the source of the squared sum in the bound.
Fin N, and Lean arm 0 is the paper's arm . Rounds are ; Lean round is the paper's round . Sums over are sums over .Off-policy learning estimates the value function of a target policy from data generated by a different behavior policy . It is how an agent learns about a greedy policy while exploring, and how many policies can be evaluated from one stream of experience. Combined with linear function approximation and bootstrapping (updating an estimate toward other estimates, as temporal-difference methods do), off-policy learning can be unstable: the weights can diverge even when every quantity involved is well defined. Sutton and Barto call this combination the deadly triad (Chapter 11 of Reinforcement Learning: An Introduction, 2nd ed., 2018).
Chapter 11 does two things. It exhibits the instability with small, fully computable examples, and it identifies an objective that can be minimized stably from off-policy data: the mean square projected Bellman error (PBE), whose gradient the Gradient-TD methods (GTD2, TDC) follow in expectation. This mission formalizes the chapter's exact, finite-dimensional claims.
A short history, following the book's bibliographical remarks (pp. 285–286): Baird (1995) gave the seven-state counterexample for off-policy semi-gradient TD; Tsitsiklis and Van Roy (1996) gave the earliest w-to-2w example and the counterexample of Example 11.1, showing that even a least-squares fit at every step can diverge; Gradient-TD methods, which follow the gradient of the PBE, were introduced by Sutton, Szepesvári and Maei and by Sutton et al. (2009); Sutton, Mahmood and White (2016) introduced Emphatic-TD. The learnability discussion of §11.6 is the book's own.
A finite Markov decision process has states , actions , a finite reward set and dynamics . A policy induces the transition matrix and expected reward . For the true value function is the expected discounted return .
A state weighting is a probability distribution on , with and norm . The matrix has the feature vectors as rows, and a weight vector gives the linear value function . The Bellman operator is
The Bellman error vector is , the projection is , and the two objectives are
Off-policy samples are reweighted by the importance-sampling ratio .
If is invertible, then for every
With the state distribution under this is (11.27), .
The results. The divergence examples show that no step-size choice rescues semi-gradient TD off-policy, and that exact least-squares fitting does not either. The learnability results separate objectives that can be estimated from observed features and rewards (RE, PBE) from one that cannot (BE), and (11.24) shows that the unobservable VE has the same minimizer as the observable RE. The gradient formula (11.27) is the expected update of the Gradient-TD family; its factorization into three expectations is what makes an stochastic-gradient method possible.
Formalizing them. All of these are proved or computed in the book, in informal notation that leaves hypotheses implicit (invertibility, coverage, the distribution , the domain of ). A machine-checked version fixes them, and gives a reusable layer of linear value-function geometry (Bellman operator, -norm, projection, BE, PBE, behavior-policy expectations) for later work on Gradient-TD convergence and on the TD fixed point. No formalization of this chapter is known to exist.
The individual steps are finite linear algebra, but they are easy to get wrong. The gradient of a quadratic form in an affine produces , and collapsing it to uses the symmetry of . The Jacobian of has to be identified through the Bellman operator's affine form , which is a theorem about the four-argument dynamics, not a definition. Passing from matrix to expectation form needs coverage, since otherwise fails. The divergence examples need the conclusion , not merely "the multiplier exceeds one".
States are a finite type; values are functions ; weights are as Fin d → ℝ; matrices are Mathlib Matrix. The dynamics are the book's with a finite reward set, and one action type serves all states. is a probability distribution (nonnegative, summing to one). is defined from expected returns, not as a Bellman solution. The gradient is a Fréchet derivative whose linear map is .
Explicit hypotheses the book leaves implicit:
Readings and corrections:
A trivializing formalization is ruled out: is not defined as a fixed point of , the PBE is not stated without the invertibility hypothesis, and the gradient is a derivative of the defined PBE, not a restated formula.
Welcome contributions: proofs of the milestones, and a general lemma on the gradient of for affine and symmetric invertible , which is reusable well beyond this mission.
The irrationality measure is the supremum of the for which has infinitely many rational solutions . Every irrational number has (Dirichlet), almost every real number has , and it is conjectured that . Known upper bounds:
The campaign's first proved value is Mahler's . This entry records Rhin–Viola's bound.
The campaign template with the value filled in: PiIrrationality.UpperBound (14.797074 : ℝ), i.e. .
Value. The paper's Theorem states exactly that is an effective irrationality measure of , "whence is an effective irrationality measure of ". The value is used as stated, with no rounding.
Rhin and Viola prove that is an effective irrationality measure of , using a birational transformation acting on Beukers' double integrals and semi-infinite linear programming to optimise the arithmetic. A measure for gives for (if is small then is small with denominator ), hence their .
Each step down the list replaces Mahler's approximations with a sharper family. Formalizing would build reusable explicit machinery: integral constructions of rational approximations to , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.
The question behind this mission was posed by T. E. Harris to L. R. Ford, Jr. and D. R. Fulkerson at RAND, in the setting of rail transport: given a rail network linking two cities, with a capacity on every link, find the largest steady flow from one city to the other. Ford and Fulkerson's answer, the minimal cut theorem, published in the Canadian Journal of Mathematics in 1956 (DOI 10.4153/CJM-1956-045-5), says that the obvious upper bound, the total capacity of a set of links whose removal separates the two cities, is always achieved by some flow.
The theorem became the starting point of network flow theory, and through it of a large part of combinatorial optimization and operations research: transportation, assignment, scheduling and network reliability problems are routinely reduced to it.
Timeline.
A network consists of a finite set of vertices , a finite set of arcs , two distinct vertices, the source and the sink , and a positive capacity on every arc. Each arc has two distinct end vertices; arcs are undirected, and several arcs may join the same pair of vertices.
A chain joining and is a set of distinct arcs that can be arranged as with , and the vertices pairwise distinct; each arc may be traversed in either direction. The null chain () joins to itself.
A flow assigns a number to each chain joining and (and to every other set of arcs) such that the load satisfies for every arc. Its value is . An arc is saturated by if . A maximal flow is a flow of largest value.
A set of arcs is a disconnecting set if every chain joining and contains an arc of ; its value is . A cut is a disconnecting set no proper subset of which is disconnecting.
The proof introduces two further objects: the set of arcs saturated by every maximal flow, and the set of left arcs, those arcs of whose left vertex (the end vertex met first by a positive chain flow of a maximal flow, travelling from ) can be reached from by a chain with no arc saturated by some maximal flow.
with both the maximum and the minimum attained. The statement mentions only flows and disconnecting sets, not the proof objects and .
Two further statements of the paper are included as items without being milestones: the remark that a disconnecting set of minimal value is a cut (p. 400), and the Corollary (p. 402): if a set of arcs meets every cut in exactly one arc, adding to the capacity of each arc of raises the maximal flow value by .
The minimal cut theorem turns a maximization over flows into a minimization over finite sets of arcs, so an optimal flow comes with a short certificate of optimality. It implies Menger's theorem (unit capacities), and through it König's theorem on bipartite matchings and Hall's marriage theorem. The Corollary is the tool behind the paper's own computing procedure for source–sink planar networks (§2, formalized in a companion mission).
The theorem is classical and proved. What this mission adds is a machine-checked proof of the paper's own formulation: undirected arcs, parallel arcs, flows decomposed along chains (path flows, with no circulations), and the minimum taken over arc sets meeting every chain, together with the proof's intermediate claims. Max-flow min-cut theorems already on the platform (Applied Combinatorics VIII, AppliedComb.Flows.max_flow_min_cut; Introduction to Linear Optimization X, LinearOptimization.max_flow_min_cut) concern directed networks with edge flows obeying conservation and cuts given by vertex sets. They are related results, not this statement, and connecting the two models is itself welcome work.
Weak duality (milestone 6) is immediate; the content is the reverse inequality. The obvious first step, taking a maximal flow and observing that its saturated arcs separate from , does not finish the proof: a positive chain flow may pass through several saturated arcs, so the total capacity of the saturated arcs can exceed the flow value. One has to single out a disconnecting subset that every positive chain flow crosses exactly once, and there is no canonical choice from a single flow. The paper's sets and are defined from all maximal flows at once, and the work consists in showing that these sets are well behaved. The orientation claim in particular needs an exchange argument on two chains that cross at an arc, where the recombined arc sequences may revisit vertices and must be reduced to chains. In a formal development this "a walk contains a chain" step and the averaging of maximal flows over finitely many chains are the main bookkeeping costs.
V and an arc type E, both Fintype with decidable equality, with end-vertex maps tail, head (labels only, no direction), tail e ≠ head e, a source and a sink with source ≠ sink, and capacities cap : E → ℝ with 0 < cap e. These are the paper's standing assumptions; there are no others in §1. In particular, no planarity is assumed and an arc may join and directly.Finset E that is the arc set of some arrangement (list of arcs, list of pairwise distinct vertices, each arc joining consecutive vertices in either order).f : Finset E → ℝ, non-negative, zero off the chains joining source and sink, with every arc load at most the capacity. A collection of chain flows that lists a chain twice merges into this form without changing the value or any load.IsGreatest and IsLeast on the sets of flow values and of values of disconnecting sets, so no supremum of a real set appears and both extrema must be attained.Finset (Finset E), convexity in Finset E → ℝ, compactness of the flow polytope (for existence), and lemmas on lists (extracting a chain from a walk). The walk-to-chain lemma and weak duality are reusable for the companion mission and for any path-flow model.A forecaster announces, each day, a probability that it will rain; afterwards nature reveals whether it did. The forecaster is calibrated if, on the days on which it announced roughly 30%, it rained roughly 30% of the time, and likewise for every other announced value. Calibration is a minimal consistency requirement for probabilistic forecasts, used in meteorology, in the evaluation of probabilistic classifiers, and in game theory, where calibrated forecasts of the opponents' play lead to correlated equilibrium (Foster and Vohra, 1997).
Calibration is achievable even against an adversary who chooses the outcomes, provided the forecaster randomizes. Timeline:
This mission formalizes the last result, Theorem 22 of the 2011 paper, in the explicit form given by its proof.
Fix a positive integer and the grid width . Each round the forecaster chooses a probability vector in the simplex over the grid indices , draws and announces . Nature then reveals .
Vectors live in with the Euclidean norm . The ℓ₁ norm is , the ℓ₁ ball is , and the unit cube is .
The calibration game (11) has payoff
The -calibration rate (Definition 19) of the announced forecasts is . Replacing each indicator by its expectation gives the rate of the forecast distributions,
which is for the average payoff .
The forecaster is Algorithm 5. It keeps a point in the cube, starting from with arbitrary. After round it takes a projected gradient step (Algorithm 4, online gradient descent) against the loss vector :
where is the Euclidean projection. It then sets to the output of the oracle Algorithm 3 on , which puts weight on at most two adjacent grid points where changes sign.
For , , every outcome sequence and every run of Algorithm 5 with ,
This is the bound of display (14) with the paper's constant .
The bound shows that a forecaster with logarithmic per-round cost has calibration error vanishing at rate against every outcome sequence. Earlier calibrated forecasters required solving a linear program or computing a fixed point each round. The construction is also the paper's worked instance of its general equivalence: a calibration problem, posed as approachability of an ℓ₁ ball, is solved by a no-regret learner on the dual unit cube together with a halfspace oracle.
The result is proved in the paper; no machine-checked version is known to exist. The formalization makes explicit three points the paper leaves informal: the step size, the sign of the gradient step, and the gap between the forecast distributions and the sampled forecasts. The milestones are reusable on their own: the ℓ₁/ℓ∞ duality, and the regret bound of online gradient descent for linear losses on a general closed convex set.
The chain (12)–(14) looks like a direct composition, but each link has content. The oracle guarantee needs a case analysis over the sign pattern of , including the degenerate case . The reduction (12) needs the duality (13) with attained minima, and it holds only outside the ball . The regret bound of online gradient descent needs the non-expansiveness of the Euclidean projection and a telescoping argument. The tempting shortcut of quoting "OGD has regret " does not give the stated constant without fixing the step size.
Vectors are EuclideanSpace ℝ (Fin (m+1)), with grid index as Fin (m+1) and as a real quotient; the ℓ₁ norm and the cube are written out coordinatewise. Rounds are . Minima over sets are stated through IsLeast or as the infimum of the image of a nonempty bounded set. Algorithm 3 is a relation that allows every sign-change index the binary search might return. The projection is any Euclidean minimizer onto the cube.
Conventions and corrections, each disclosed in the item's Formalization Note:
A trivializing formalization is ruled out. The rate is defined from Definition 19's formula, not as a distance, and the step size is pinned. A free step size would make the bound false, and an empty oracle relation would make it vacuous; milestone 3's existence clause excludes the latter.
Contributions are welcome on each milestone. The online gradient descent bound and the ℓ₁/ℓ∞ duality are independent of calibration. The published one-step inequality LogRegretOCO.OGD.one_step_inequality is included as a reference item for the regret bound.
A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.
For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.
Timeline:
Let be a finite graph with node set and edge set ; each edge meets two different nodes, its ends. Real variables correspond to the edges . The polyhedron is the set of vectors satisfying
The matching vectors are the vectors with every component or that satisfy (2); they are the incidence vectors of matchings. For edge weights , the linear form (4) is .
The dual program has a variable for each node and for each odd set (, ). Its objective is (5) , subject to (6) and (7) for every edge with ends . For a matching , conditions (8)–(10) are the complementary slackness conditions: at nodes not covered by , equality in (7) on , and every odd set with contains exactly edges of .
A blossom sequence (Theorem (M)) starts from with matching and repeatedly shrinks an odd circuit (a blossom, edges of which are matched) to a single node, carrying node weights and edge weights that obey conditions (a)–(k) of p. 127.
In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron (), matchingVectors (), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.
The vertices (extreme points) of are exactly the matching vectors of . Hence the maximum weight of a matching equals for every .
The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.
Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).
The inclusion and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to must be verified through the whole shrinking history.
V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.|V|.z is a function on all node sets of which only odd sets are read.Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy , and the goal is the value function of a target policy . Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under is reweighted by the relative probability of its trajectory under and . Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for -step, gradient-TD and eligibility-trace methods.
This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).
A finite Markov decision process has finite sets of states (terminal states included), actions and rewards , and dynamics : for each a probability distribution over next state and reward. The state-transition probability is . A policy gives a distribution over actions in every state.
An episode from a start state is a sequence in which are nonterminal and is terminal. Under it has probability . The return is with discount rate , and the value is the expected return of an episode generated by from .
The behaviour policy covers the target policy if implies . The importance-sampling ratio of decisions is
and the per-decision return weights each reward only by the ratio of the decisions that precede it:
The book writes these objects at a general time and conditions on ; by the Markov property this is the same as starting the episode at , which is what the formal statements do.
For episodes generated by from ,
The first equality is Eq. (5.4) (p. 104); the second is the statement of §5.9 (p. 114).
Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.
The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on -step off-policy returns and off-policy traces can reuse.
Eq. (5.4) itself is a termwise identity: for every episode, under coverage. The per-decision identity is not termwise. The later factors of multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode and differ.
In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.
Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values (Exercise 5.6).
A Markov decision problem asks how to control a system that moves at random between finitely many states, where each decision changes the probabilities of the next move and incurs a cost. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) treats two criteria: the long-run average cost per period, and the total cost of driving the system into an absorbing state. Its Theorem 2 shows that, once attention is restricted to stationary procedures, each problem can be solved as a linear program over the state-action frequencies of the procedure. This mission formalizes that theorem, its supporting displays (3)–(10) and its Lemma on linear-fractional programs.
The linear programming formulation is now the standard computational and theoretical tool for constrained Markov decision processes, and its variables, the occupation measures, are the objects of most later work on that topic. Derman's paper is among the first to state it for the average-cost criterion. Manne (Linear Programming and Sequential Decisions, Management Science, 1960) gave an earlier average-cost formulation for an inventory model. The reduction of a ratio of linear functions to a linear program in Derman's Lemma is the transformation published in the same year by Charnes and Cooper (Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly, 1962).
There are finitely many states and decisions , all available in every state. Making decision in state sends the system to state with probability , where , and costs .
A procedure of class is stationary randomized: in state it makes decision with probability , where and , independently of the past and of the time. Under such a procedure the states form a Markov chain with transition probabilities . Write for the expected cost at time when .
The state-action frequencies of a procedure with stationary distribution are . They satisfy the linear constraints
For Problem 2, Derman adjoins a state that restarts the chain uniformly on and is entered from . The expected total cost then becomes a ratio of two linear functions of the frequencies of this augmented chain, (9).
The printed statement, "If Assumption A (B) holds, then problem 1 (2) can be formulated as a linear programming problem", is not a mathematical statement as it stands. The goal is the reading established by its proof (pp. 20–23).
Under Assumption A with , the program
has an optimal solution. For every optimal , every row sum is positive, and satisfies for all and all .
Under Assumption B with the Problem 2 costs, the linear program obtained from (9) by the Lemma's transformation, subject to (12), has an optimal solution. For every optimal one has , and the procedure decoded from satisfies for all and all .
In the order the proof uses them: the Cesàro limit and the unique positive stationary distribution of a one-class chain ((3), (5)); the taboo-probability identity (4); the formula (6) for ; the cycle formula (7) for the averaged total cost; the remark that minimizing the average of the minimizes each one; the correspondence between and the solutions of (10); and the Lemma reducing a linear-fractional program under conditions (i) and (ii) to the linear program (12).
The theorem replaces a search over infinitely many randomized procedures by a single finite linear program. It also yields the structural fact that an optimal stationary procedure can be read off from any optimal solution. The variables make constraints on long-run frequencies of actions expressible as linear constraints. That is the origin of the theory of constrained Markov decision processes, and of the dual linear programs whose variables are value functions. The Lemma is the classical linear-fractional reduction, used well beyond this setting.
All of these results are proved in the paper and in later textbooks (for example Puterman, Markov Decision Processes, 1994, §8.8 and §9.5). None of them has been formalized: Mathlib has Perron–Frobenius-type facts for irreducible matrices but no linear programming theory, no taboo probabilities and no Markov decision model. The mission produces machine-checked versions of the proof's chain of equalities and of the decoding step, written so that they can be reused for occupation-measure arguments.
Several steps fail in the naive argument. The correspondence between procedures and solutions of (10) needs every row sum to be positive. That uses Assumption A for a procedure obtained by completing the decoded rows arbitrarily, together with the uniqueness and positivity of the stationary distribution. Positivity of the stationary vector of an irreducible but possibly periodic chain, and the Cesàro (not ordinary) convergence of , have no ready-made form in Mathlib. The total-cost identity (7) needs the regenerative identity (4), whose sums must first be shown to converge, and needs the augmented chain to be irreducible, which follows from Assumption B but is not assumed. Problem 2 needs one more step: a minimizer of the averaged total cost is optimal from every starting state, which uses the finiteness of all .
States and decisions are finite Lean types S and Act. Probabilities and costs are real numbers, a procedure of is a nonnegative real matrix with unit row sums, and the chain is chainMatrix q D. Assumption A is irreducibility (Matrix.IsIrreducible) of every such chain matrix. Assumption B is reachability of from every state; for a finite chain in which is absorbing, this is equivalent to absorption with probability one. is a real limsup of a bounded sequence, with the paper's sum over . takes values in . The paper requires on p. 17 and in Problem 2. The formalization uses for in Problem 2, and keeps the two problems as separate implications. The adjoined state is none : Option S, with the transition law that produces Derman's , for every procedure. The published JewellMRP.InfiniteStep definitions of an ergodic matrix and of a stationary vector are reused.
The goal states optimality of the decoded procedure against every competitor in , for every optimal solution of the linear program, with existence of an optimal solution as a separate clause. A statement that only identifies feasible sets, or that only asserts that some optimal procedure exists, does not count as Theorem 2. Optimality over all history-dependent procedures is Theorem 1, a separate mission of this series.
Welcome contributions: the stationary-distribution facts for irreducible finite stochastic matrices (reusable across Markov chain work), a small linear-programming existence lemma (a linear function attains its minimum on a nonempty compact polytope), and the Lemma's transformation, which is self-contained.
A Markov decision process with finitely many states and decisions is the basic model of sequential decision making under uncertainty: inventory replacement, machine maintenance, queue control and pursuit problems all fit it. Its computational methods (Howard's policy iteration, 1960; Manne's linear programming formulation, 1960) search only over stationary procedures, which use the same decision every time the system is in the same state. A controller, however, may also remember the whole past and randomize. Whether such procedures can do better is a genuine question: as Derman puts it, "a proof is required before a procedure optimal over can be considered as the optimal procedure."
Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) answers it for two criteria, the long-run average cost and the total cost until absorption, by showing that a deterministic stationary procedure is optimal against all procedures. This mission formalizes that theorem, Theorem 1, together with the steps of its proof.
Timeline. Karlin (1955) gives the existence of a discount-optimal procedure used here; Howard (1960) and Manne (1960) solve the average-cost problem over stationary procedures; Wagner (1960) shows by linear programming that an optimal average-cost procedure can be taken deterministic and stationary; Derman (1962) proves the reduction for both criteria by the functional equation approach; Blackwell (1962) strengthens the discounted side to procedures optimal for all discount factors close to .
The system is observed at times in one of finitely many states . After each observation one of decisions is made; every decision is available in every state. If the system is in state and decision is made, it moves to state with probability , where , and a cost is incurred.
A procedure chooses decision at time with probability , which may depend on the whole history of states and decisions . The class of all procedures is . The class consists of the stationary randomized procedures, for which this probability is a number depending only on the current state . The class consists of the deterministic stationary procedures, those of with , that is, maps from states to decisions; is finite.
Started from , a procedure incurs the expected cost at time . The criteria are
and, for a discount factor , the auxiliary discounted cost . Problem 1 assumes . Problem 2 assumes that state is absorbing under every decision and that , so is the expected cost of driving the system from into .
There are procedures such that, for every state ,
One procedure serves every initial state, and the minimum is over all of .
Theorem 1 is what makes finite optimization possible for these problems: once is known to contain an optimal procedure, the search runs over finitely many maps, and the linear programs of the paper's §3 (the next mission of this series) and of Manne describe the whole problem rather than a restriction of it. Part (2) is a total-cost result without any assumption that the absorbing state is reached; it holds even when every procedure has infinite cost from some state, which separates it from the stochastic shortest path theory that assumes properness.
Part (1) is available on the platform as part of Sennott's Proposition 6.2.3 (stated there, not yet proved), and it is referenced here rather than restated. Part (2), the functional equation for history-dependent procedures and the Abel-limit identity for the total cost have no statement on the platform; to our knowledge none has a machine-checked proof.
The obvious argument compares an arbitrary procedure with stationary ones state by state, but a history-dependent randomized procedure does not induce a Markov chain, so no transition matrix is available for it. The comparison has to pass through the discounted problem, where an optimal stationary procedure exists for each , and then let . Two limit exchanges are needed: for the average cost, an Abelian inequality valid for every procedure plus a Markov chain limit theorem for the stationary one; for the total cost, monotone convergence in , which must work when the limit is infinite. The discount-optimal procedure depends on , and the finiteness of is what yields a single procedure along a sequence .
The model is the published SennottDP.AvgFinite.Model (a Markov decision chain with finite action sets, nonnegative costs in and transition probabilities in ) with finite nonempty types of states and decisions and every action set equal to the whole decision type. Derman's class is its Policy (history-dependent, randomized); is StationaryPolicy. is expCost, is discCost, and is avgCost , which has the same value as Derman's normalization because is bounded. is a new definition, a sum in . Every discount factor is restricted to explicitly. "Minimum over " is stated as an inequality against every policy, with the optimal procedure chosen before the initial state.
Problems 1 and 2 enter as separate implications with their own cost hypotheses; the page's "" is read as for in Problem 2, since there. A formalization that compares only against stationary procedures, or that states the total cost as a real series (whose divergent values default to ), is ruled out: the competitors are all policies and lives in .
A complete development needs the discounted Bellman equation for history-dependent policies, the selection of a deterministic minimizer, and Abelian theorems for nonnegative series. These are reusable across the platform's dynamic programming missions, and proofs of the referenced Sennott propositions are welcome contributions in their own right.
A finite game describes several decision makers whose payoffs depend on everyone's choices. A Nash equilibrium is a collection of choices at which no single player can improve their expected payoff by changing strategy alone. Equilibrium existence is a classical result, but a computational argument needs to connect an object that can be approximated numerically to a strategically meaningful outcome. Daskalakis, Goldberg and Papadimitriou make that connection using Nash's map on mixed-strategy profiles in their study of equilibrium computation (Daskalakis, Goldberg and Papadimitriou 2009, §3.2). This mission isolates their quantitative connection: a profile close to a fixed point of that particular map is close to a Nash equilibrium, with the paper's explicit error bound.
The result is a known lemma from the published paper, not an open conjecture. It belongs to the paper's route from finite games to approximate equilibrium computation. The present mission treats the analytic statements about the map and finite payoffs; it does not state the paper's PPAD completeness theorem or encode computational reductions.
A normal-form game has players. In the Nash-map section each player has the same nonempty set of pure strategies. A pure profile chooses one strategy for each player, and player receives a nonnegative real payoff . The largest entry among all these payoff tables is . A mixed profile assigns each player probabilities that sum to one over ; different players randomize independently. The expected payoff when everyone uses is . If player instead uses the pure strategy while the others keep their mixed strategies, the expected payoff is .
Write for the positive part of this unilateral payoff gain. Nash's map assigns to each coordinate of a mixed profile the normalized value
The numerator raises the weight of a strategy whose pure payoff exceeds the current expected payoff. The common denominator ensures that the new weights for a player sum to one. These are exactly the quantities and normalization displayed on page 205 of the paper (Daskalakis, Goldberg and Papadimitriou 2009).
An -approximate Nash equilibrium here means a mixed profile at which no player can increase expected payoff by more than through any mixed-strategy deviation. This is the alternative approximation notion identified on page 199 and written as Eq. (27) on page 243. It is weaker than the paper's -approximately well-supported condition; the two notions must remain distinct.
The goal is Lemma 3.8 (p. 207). For any mixed profile with , where , its approximate-equilibrium error is bounded by the paper's exact quantity:
No numerical constant is left free or replaced by an unspecified asymptotic bound. The goal is universal over games and profiles satisfying the stated conditions; it does not merely assert the existence of one favorable profile.
The milestone list also includes Lemma 3.5, bounding the variation of a pure-strategy payoff when opponents change their distributions; Lemma 3.6, an inequality for normalized nonnegative sums; and Lemma 3.4, the explicit Lipschitz bound
Equation (3) on page 208 is a further milestone: it bounds each coordinate's share of the total positive gain under approximate fixedness. Lemma 3.4 has a separate role in the paper's grid analysis; it is not claimed as a prerequisite of Lemma 3.8.
The goal gives a quantitative translation between two kinds of approximation. An error measured in the coordinates of a fixed-point map becomes an upper bound on a player's incentive to deviate. The dependence on , and matters because the later computational construction chooses its grid scale using an explicit threshold, not simply a convergence claim. Lemma 3.4 provides the separate sensitivity estimate for that map, also with its exact constant (Daskalakis, Goldberg and Papadimitriou 2009, pp. 205–207).
Formalizing these known statements supplies a reusable bridge between finite-game payoffs, mixed profiles and a concrete fixed-point map. The shared finite-game representation already exists in the published agt_games definition bundle. What remains here is a machine-checked proof of each quantitative statement and of the payoff identities needed to relate pure and mixed deviations. The local Lean statements compile as open theorem targets; the mission does not claim that their proofs are already formalized.
A coordinatewise small value of does not by itself bound the largest payoff advantage by the same number. The map normalizes by a sum of all positive advantages, and a strategy with a large advantage might have little probability under . Conversely, controlling a player's current expected payoff requires information about the entire probability vector, including strategies that are worse than the current mix. The explicit square-root dependence in Lemma 3.8 captures this mismatch. A direct substitution of the fixed-point error for the equilibrium error would lose both the dimension and payoff-scale factors in the published bound.
Lean represents players by Fin r, strategies by Fin n, payoffs by a real function on pure profiles, and mixed strategies by real-valued weight functions satisfying AGT.IsMixedProfile. The paper numbers players and strategies from one; Fin uses zero-based indices without changing the mathematical sets. AGT.expectedPayoff and AGT.profileProb implement the independent product distribution. Pure-strategy expected payoff is the same expectation after replacing just one player's lottery by a point mass. The maximum payoff is computed from the game's actual finite table; the statements require and , so this maximum exists. Nonnegative payoff entries, the standing convention from §2.1, are hypotheses.
The formula for is defined on all real coordinate arrays, exactly as an algebraic expression. Every theorem about an equilibrium supplies mixed-profile membership. This explicit condition rules out interpreting Lemma 3.8 on arbitrary vectors, for which “approximate Nash equilibrium” has no strategic meaning and the paper's argument does not apply. The infinity norm is written as a bound for every player-strategy pair, avoiding any dependence on a chosen norm instance. All error parameters appearing in the statements are nonnegative, and the denominator of is positive on mixed profiles because each is nonnegative.
The development needs finite products and sums, real inequalities, the game bundle, and elementary facts about lotteries and unilateral deviations. Results about how expectations vary under a changed product distribution are reusable for other finite-game formalizations. Contributions proving the milestone inequalities, the payoff identities, and the goal's exact bound are welcome.
A single server shared by several classes of jobs must decide, at every moment, which class to serve. Different scheduling rules give different mean response times to the classes, and a system designer often starts from the other end: a target vector of mean response times, one per class, and the question whether any rule can meet it. Coffman and Mitrani answered this question for the multiclass M/M/1 queue in A Characterization of Waiting Time Performance Realizable by Single-Server Queues (Operations Research 28 (1980), 810–821). Their answer is a polytope with an explicit description: the response-time vectors that can be realized are exactly the convex combinations of the vectors of the preemptive priority rules, and these are exactly the vectors satisfying one equation and inequalities.
The starting point is Kleinrock's conservation law (Kleinrock, Naval Res. Logist. Quart. 12 (1965)): a weighted sum of the response times does not depend on the rule. The characterization is the first instance of what was later called the achievable region method, developed for general multiclass systems by Federgruen and Groenevelt (Oper. Res. 36 (1988)), Shanthikumar and Yao (Oper. Res. 40 (1992)) and Bertsimas and Niño-Mora (Math. Oper. Res. 21 (1996)), and used to derive priority-index policies such as the rule and Gittins indices.
There are job classes. Jobs of class arrive in a Poisson stream at rate and have exponential service times with parameter . The traffic intensity of class is , and the system is stable: . A performance vector lists the mean response times of the classes. Write , , and for a set of classes
In Lean the data are a structure Params M carrying and the three standing assumptions; Params.f, Params.Hss (), Params.prioVec, topSet and Params.H are the objects above.
The paper's Theorem 2 says a vector is achievable by a scheduling strategy iff it lies in ; its proof is the chain , where is the achievable set. The goal is the part of the chain that involves no strategies.
A further item states the paper's final remark (§4): every linear cost is minimized over at some preemptive priority vector.
The theorem turns a question about all scheduling rules into a finite check: a target vector is realizable iff it satisfies (1) and the inequalities (4), and every realizable vector is realized by randomly mixing at most priority rules. Linear costs over the realizable vectors are minimized by a priority rule, the fact behind the optimality of priority-index rules in multiclass queues. The paper also gives a linear program for finding the mixture.
The result has been proved since 1980. No machine-checked proof of it is known. The Prove2Me library holds the abstract generalized conservation law theorem of Gittins, Glazebrook and Weber (AllocationIndices.achievable_region_theorem, included as a reference item), which assumes the inequalities (4) for every policy and whose polytope also imposes nonnegativity; it does not compute the right-hand sides for the M/M/1 queue, does not prove that the priority vectors satisfy (4), and uses equality on the lowest-priority sets rather than the highest. This mission supplies the concrete polytope, the closed form of the priority vectors and the strict supermodularity of .
That the priority vectors lie in is a family of inequalities between ratios , one for each pair of a priority order and a set , and the order and need not interact in any simple way. The reverse inclusion is a statement about vertices: a vertex is determined by tight constraints, and one has to show that they form a chain. This needs strict inequalities with the right direction for every crossing pair of sets, which is where the positivity of every is used. If some , then appears in no constraint, is unbounded and the goal is false. Finally, uses only points, not all , so the goal contains a Carathéodory-type bound for the hyperplane of (1).
Classes are Fin M, numbered from . A priority order is π : Equiv.Perm (Fin M) with π r the class of rank r, rank highest. "Vertex" is an element of Set.extremePoints ℝ. The points of (3) are prioVec (σ k) for an arbitrary σ : Fin M → Equiv.Perm (Fin M), so repetitions are allowed. The priority vectors are given by their closed form, not as solutions of a system. The goal assumes ; for the set is empty.
The paper's notion "achievable by some scheduling strategy" is replaced by its analytical characterization : the strategy class of the paper (Assumptions 1–3, p. 812) is described only in prose and the steady-state means are assumed to exist, so the queueing half of the proof (Theorem 1, Lemma 1 for arbitrary strategies, the conservation law itself) is not stated. The goal is not to be stated on an abstract set satisfying hypotheses that encode Lemma 1 and (1); that form is already proved and drops the content of milestone 4. The conservation law is an equality, never the inequality (4) at the full set.
A complete development needs finite-set sums, the extreme points of a polyhedron and a Carathéodory argument in an affine hyperplane; the inequalities of milestones 2 and 3 and the vertex-chain argument are reusable for any strictly supermodular set function. Proofs of any milestone, and alternative proofs of the goal through polymatroid theory, are welcome.
An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.
Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.
A single flight leg has capacity . Class 1 has fare , class 2 has fare , with . The numbers of requests for the two classes are random variables with values in , defined on a probability space and independent. There are no cancellations, no no-shows, and a refused request is lost.
The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level is the number of seats reserved for class 1; it sets the class-2 booking limit . All class-2 requests arrive before any class-1 request. Class 2 therefore books seats and class 1 books , and the realised revenue is
The expected revenue is .
The tail probability of class 1 is , the probability of receiving or more class-1 requests, and the expected marginal seat revenue of the -th class-1 seat is
For a single class with seats the expected revenue is , and is its increment from to seats. The EMSR protection level is the largest integer with
In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.
The goal fixes no distribution: it holds for every pair of independent -valued demands, and depends only on and the law of .
RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.
The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of against and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.
The expected revenue couples the two demands through the capacity left by class 2, so is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment : it is not , as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of and is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with in place of the rule is off by one seat and the claim fails.
Conventions the Lean statements commit to:
r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.μ.real; seat counts use truncated subtraction only where .A trivializing formalization is ruled out: is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.
The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.