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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
A false failure return is a product returned by a consumer as defective although it has no functional or cosmetic defect; managers attribute such returns to installation difficulties, a mismatch with the consumer's preferences, and remorse. Ferguson, Guide and Souza report (pp. 376–377) that false failures account for up to 80% of Hewlett-Packard's inkjet printer returns, roughly 5% of sales, and that the per-unit cost of a false failure return to computer manufacturers is around 25% of the product's price. The manufacturer absorbs most of that cost, while the retailer is the party able to prevent the returns in the short term, by spending time with customers before the sale and supporting them after it. The retailer bears the cost of that effort but captures only part of its benefit, so without an incentive it exerts too little.
The paper (Ferguson, Guide & Souza, MSOM 2006) models this as a single-period manufacturer–retailer problem with non-contractible retailer effort, and asks which contracts restore the supply chain's optimal effort and who gains from them. It belongs to the literature on supply chain coordination with contracts (Cachon 2003) and on channel rebates with sales effort (Taylor 2002); its object is a target rebate, a payment to the retailer for every false failure return below a target.
A manufacturer with unit cost sells to a retailer at wholesale price , who sells at retail price . Avoiding one false failure return is worth
where and are the parties' return-processing costs and , are the unit sale impacts of avoiding the return (p. 381). Both are assumed positive.
The retailer chooses an effort at cost , . At effort the number of false failures is a nonnegative random variable with mean , where is the expected number at the minimum effort . The coordinated supply chain earns
maximized at the coordinated effort . Without a contract the retailer earns and chooses the decentralized effort ; the manufacturer then earns .
Under a target rebate contract the retailer receives for every false failure below the target , so the profits become
The contract coordinates the supply chain when maximizes over . In the uniform case of §3.1, , and the contract must satisfy .
Assume and , and let be uniform. For every coordinating contract with , ,
The milestones follow the paper's §3–§3.1 and the appendix proof, in attack order: concavity of and optimality of (Eqs. (1)–(2)); in the interesting case; optimality of (Eqs. (3)–(4)); ; Proposition 1 (concavity of the retailer's rebate profit when ); its uniform instance; the uniform closed form (8); the first-order condition (9); the coordinating target (10) together with the admissibility condition ; the manufacturer's profit under a coordinating contract (25); the retailer's profit (27); and the retailer's gain in the two cases (30) and (31).
The result divides the effect of the contract between the two parties. The retailer is always at least as well off as without a contract; the manufacturer, who pays the rebate, gains exactly when the supply chain's optimal effort is at least twice what the retailer would exert alone. When this is equivalent to (p. 383), so a target rebate pays for the manufacturer only when its own stake in avoiding a false failure dwarfs the retailer's. The companion result (10) shows that for every rebate exactly one admissible coordinating target exists, and none for : a coordinating rebate is always larger than the manufacturer's own cost of a return.
The results are proved in the paper by calculus and algebra. None of them has a machine-checked proof that we know of, and nothing on Prove2Me models non-contractible effort or target rebates. The mission produces a checked version of the paper's model with the expectation taken as a genuine integral against the uniform law, a formal notion of coordination as the retailer's optimization, and statements that make explicit which hypotheses each step of the appendix uses. The definitions of effort-dependent profits and coordination are reusable for other effort-inducing contracts in the same paper and in the sales-effort literature.
The algebra of the appendix is short once the first-order condition (9) holds at . The substance is getting there. Coordination is defined by optimality of for the retailer's profit, and that profit involves the expectation , which is piecewise in : it equals only while , and beyond. Deriving (9) requires showing that is an interior maximizer, that the expectation is differentiable there with the closed-form derivative, and that the side condition keeps in the closed-form region. The converse direction of (10), that the formula for produces a coordinating contract, needs concavity of the piecewise profit on all of , which is where Proposition 1 enters.
Replacing the expectation by the global formula is the tempting shortcut and it changes the problem: for the formula exceeds the true expectation, and the retailer's maximizer, hence the meaning of "coordinates", changes with it.
All parameters are real numbers, bundled in a structure Params; and are Params.Mm and Params.Rr. Effort ranges over (Set.Ici 1); statements the paper makes for every positive effort (concavity of , the closed form (8)) are stated on . Cube roots are Real.rpow with exponent on positive bases. The uniform law is Lebesgue measure conditioned on , and the expectation is the Bochner integral against it. Coordination is IsMaxOn of the retailer's profit on Set.Ici 1 at .
Three conventions differ from the printed text, each recorded in the item's formalization note:
The side condition of §3.1 is a hypothesis of the goal and of the appendix milestones; without it a coordinating contract with exists and the "if" direction fails. The unused page assertion is not imposed.
The goal is not trivialized by its coordination hypothesis: coordination is the retailer's optimization over the true profit, and milestone (10) shows that coordinating contracts with exist for every , so the hypotheses are satisfiable (Example 1 of the paper, p. 384, is an instance). The retailer half of the goal is comparatively short under this definition of coordination; that is a property of the paper's theorem, not of the encoding. The manufacturer half needs (8), (9) and (25).
The development needs only Mathlib: real calculus (derivatives, concavity, Real.rpow) and Lebesgue integration against a conditioned Lebesgue measure. The model definitions (effort-dependent profits, coordination as the retailer's optimization) are reusable for the paper's other effort-inducing contracts. Contributions welcome: proofs of any milestone, and reusable lemmas on expectations of under uniform laws.
Two optimization problems on weighted networks sit at the base of operations research and algorithm design. The first asks for the cheapest way to connect every node of a network, such as a cable, pipeline or communication network. The answer is a minimum weight spanning tree. The second asks for the shortest route from a depot to every other node of a road or data network, the single-source shortest path problem. Chapter 12 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org, CC BY-SA 4.0) treats both. It proves the structural lemmas behind the greedy spanning tree algorithms of Kruskal (1956) and Prim (1957), and the correctness of the shortest path algorithm of Dijkstra (1959).
The minimum spanning tree problem goes back to Borůvka (1926), who designed an electrical network for Moravia. Kruskal and Prim gave the two greedy algorithms taught today, and Dijkstra's 1959 note treated both problems. Dijkstra's shortest path method, with heap-based refinements such as Fredman and Tarjan (1987), remains the standard solver for non-negative lengths and a building block of routing, scheduling and network flow codes.
A graph has a finite vertex set and a set of 2-element subsets of . A weight is attached to each edge, and a set of edges has weight . A spanning forest of is an acyclic graph with . A spanning tree is a spanning forest that is connected. The weight of a spanning tree is the weight of its edge set. In Lean these are SimpleGraph V with [Fintype V], IsSpanningForest G H ( and acyclic), IsSpanningTree G T ( and a tree), and weight w T for a weight w : Sym2 V → ℕ.
A digraph has with for every directed edge . Each directed edge has a length . The length is extended by for non-edges. A directed path from to is a sequence of distinct vertices in which consecutive pairs are directed edges. Its length is . The distance is the minimum length of a directed path from to , and is when no such path exists. A shortest path is a directed path attaining it. In Lean this is WeightedDigraph V with ext, IsDirPath, pathLength, dist and IsShortestPath.
Dijkstra's algorithm (Algorithm 12.14) with root and keeps a sequence of permanent vertices, a value and a sequence for each vertex. Step 1 sets , , , and , for . Step with scans from the last permanent vertex . For every temporary it sets , and on a strict decrease it replaces by followed by . Each step ends by appending to a temporary vertex of minimum , chosen arbitrarily among ties. The algorithm halts at Step . DijkstraRun G r i s holds when some sequence of admissible choices leads to state s at the start of Step .
For every halted state of every run, and every vertex ,
Milestones 4 and 5 are the two statements the book's proof of the goal rests on. Milestones 1–3 are the spanning tree half of the chapter. Lemma 12.6 is the result from which the book derives the correctness of Kruskal's and Prim's algorithms.
Theorem 12.18 certifies that one pass of steps computes all distances from and a shortest path tree, with no condition on the digraph beyond non-negative lengths. Lemma 12.6 is the cut property. Every greedy minimum spanning tree method (Kruskal, Prim, Borůvka) is an instance of it, and the exchange principle is the matroid basis-exchange axiom specialised to the graphic matroid.
All of these results are classical and proved. None is formalized in this form on the platform. Mathlib has spanning trees of connected graphs, uniqueness of paths in acyclic graphs, and the edge count of a tree. It has no edge–component count for forests, no exchange principle, no weighted spanning trees, and no Dijkstra. On Prove2Me, FamousTheorems.tree_card_edges_6b and ClassicalGaps.isAcyclic_edges_eq_card_sub_one_imp_connected cover only the tree case of Proposition 12.3. KServer.mst_cut_property is a cut property for complete graphs encoded by parent maps, a different statement. The label-correcting algorithm of Dynamic Programming and Optimal Control II (BertsekasDP.label_correcting_*) is a different algorithm: it keeps an open list and scans in arbitrary order, not by minimum label.
The goal is a statement about the final state of a run, but the facts it depends on only become visible across steps: a permanent vertex's and never change again, and is always the length of the current . None of this is recorded in the final state itself. An argument over the steps of the run has to show that each remains a path with distinct vertices, including when edges of length allow ties. It also has to handle the value , where and a comparison between two infinite values never counts as a decrease. Tie-breaking is arbitrary, so no argument may depend on which minimum is chosen. For Lemma 12.6 the difficulty is the exchange step: removing an edge of a tree path and adding a crossing edge must again give a tree that still contains the forest , and this is a statement about cycles and components, not about counts.
SimpleGraph V over a Fintype V. Weights are Sym2 V → ℕ (the book's ; values off are never used). Acyclic, tree and connected components are Mathlib's. In Proposition 12.3, is written and is assumed, which the bound presupposes.ℕ, and and distances are ℕ∞, where is ⊤, never a large finite number. A version with real or ℝ≥0 lengths would be a generalization and is not what is asked.ℕ∞, the invariants of Dijkstra's algorithm, and forest edge counting. Contributions of general lemmas (walks shortcut to paths without increasing length, component counts under edge insertion) are welcome.Network revenue management decides which products to make available to arriving customers when products share scarce resources: an airline sells itineraries (products) that consume seats on flight legs (resources), and each itinerary has a fare. When customers choose among the offered products, rather than asking for one fixed product, the standard planning tool is a deterministic linear program that replaces random choices by their expected values. Gallego, Iyengar, Phillips and Dubey (2004, Columbia CORC technical report TR-2004-01) and Liu and van Ryzin (2008) formulated this choice-based linear program; its solution drives bid-price and offer-set policies used in practice.
The difficulty is size. The choice-based program has one variable for each subset of products, in all, and is solved by column generation, whose pricing subproblem is itself an assortment problem. Feldman and Topaloglu (Oper. Res. 65(5), 2017) show that when customers choose under the Markov chain choice model of Blanchet, Gallego and Goyal (2016), the choice-based program is equivalent to a linear program with only variables and constraints. This mission formalizes that equivalence, Theorem 7 of the paper.
There are products, . Under the Markov chain choice model a customer first visits product with probability . If the product she visits is offered, she buys it. Otherwise she moves from product to product with probability , or leaves without buying with probability . The paper assumes throughout that
For an offer set , is the expected number of visits to product while it is offered, which is its purchase probability, and is the expected number of visits to while it is not offered. The pair is the solution of the (Balance) equations
Dropping the constraints tied to gives the polyhedron
The network has resources, , with capacities ; the selling horizon has periods; product earns and consumes units of resource . With the probability of offering in a period, the (Choice Based) linear program is
and the (Reduced) linear program is
In (Reduced), is the expected number of visits to product while it is available and the expected number of visits while it is not.
Let be an optimal solution of (Reduced). Then there are subsets and positive scalars with such that
and for any such subsets and scalars the vector with and for is optimal for (Choice Based), with objective value equal to that of in (Reduced). In particular the two programs have the same optimal value.
The result. Theorem 7 replaces a program with columns by one with variables and constraints, solvable directly by any LP solver, and it returns an optimal solution of the original program, not only its value. The optimal value is the standard upper bound on the optimal expected revenue of a network revenue management policy, and the dual variables of the capacity constraints are the bid prices used to control sales. The decomposition of part 1 is what turns the small program's solution back into offer-set frequencies that a policy can implement; Section 7 of the paper makes that decomposition algorithmic (a separate mission of this series).
Formalizing it. The theorem is proved in the paper; to the best of available knowledge no machine-checked version exists. A formal proof checks the link between polyhedral geometry (extreme points of and the solutions of (Balance)) and linear-programming optimality, and records exactly which properties of the Markov chain choice model are used: the standing assumptions enter through uniqueness and nonnegativity of and through boundedness of .
The inequality "(Reduced) (Choice Based)" is a direct computation: averaging the (Balance) equations with weights lands in . The reverse direction is where the obvious argument fails. A point of has no offer set attached to it, and a general polyhedron need not be the convex hull of its extreme points: it can contain lines or rays. The argument requires that is bounded, which depends on the substochasticity , and that each extreme point is exactly some , which uses the structure of the balance equations and the uniqueness of their solution. Neither follows from general linear-programming facts. In Lean, the finite vertex representation of a bounded polyhedron is also not a one-line consequence of Mathlib's Krein–Milman theorem, which gives only the closure of the convex hull.
Products are Fin n, offer sets Finset (Fin n), resources Fin m. The model is a structure Model n holding , (rho j i , the transition from to ) and the standing assumptions and ; the nonnegativity , implicit in the paper because the are probabilities, is an added field. is a solution of (Balance) chosen by Classical.epsilon, and milestone 1 is what identifies it with the paper's unique solution. is a subset of (Fin n → ℝ) × (Fin n → ℝ), extreme points are Mathlib's Set.extremePoints ℝ, and boundedness is Bornology.IsBounded. is a natural number entering as a real factor exactly where the paper writes it; , , carry no sign conditions, as in the paper. "Optimal solution" means feasible and at least as good as every feasible point; no supremum is used.
Two conventions are disclosed. The paper defines by ; the formalization sets , which agrees when the are distinct and is the only consistent reading otherwise. Milestone 5 is stated for every feasible of (Choice Based), while the paper applies it to an optimal one; its argument uses only feasibility. No printed statement needed correction.
The goal is not only the decomposition of part 1, which is milestones 2 and 4 combined: it also asserts optimality of and equality of the optimal values, and a formalization that drops part 2 does not state Theorem 7. Part 2 is required for every decomposition, and part 1 guarantees one exists, so part 2 is not vacuous.
A complete development needs the vertex representation of polytopes (reusable beyond this mission; LinearOptimization.polyhedron_resolution on the platform proves the resolution theorem in another encoding), the theory of substochastic matrices behind (Balance) (invertibility of with a nonnegative inverse), and finite-sum manipulations over Finset (Fin n). Contributions to any milestone, and bridges to existing polyhedral results, are welcome.
Airlines, hotels and rental firms sell a fixed stock of capacity (seats on a flight leg, rooms on a night) over a finite selling horizon, and control revenue mainly by deciding which products (fare classes, rate plans) to make available at each moment. When customers substitute between products, the decision in each period is an assortment: a subset of products to offer. Talluri and van Ryzin (Management Science 2004) formulated this single resource revenue management problem as a dynamic program for a general choice model, and showed that structural properties of the optimal policy depend strongly on how customers choose.
The Markov chain choice model of Blanchet, Gallego and Goyal (technical report 2013; Oper. Res. 2016) describes substitution by a Markov chain on the products and approximates a broad class of random-utility models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study assortment and revenue management problems under this model. This mission formalizes their structural result for the single resource problem (Theorem 5): there is an optimal policy whose offer sets are nested in the remaining capacity and in the remaining time, so that it can be implemented by protection levels, one capacity threshold per product and period.
There are products . A customer arrives to purchase product with probability . If is offered she buys it; otherwise she moves to product with probability , and leaves with probability . The paper assumes and for all . For an offer set , the purchase probabilities and the visit counts of unavailable products solve the (Balance) equations
With product revenues , the (Assortment) problem is , and its (Dual) linear program is
In the single resource problem there are periods and units of capacity. In each period at most one customer arrives; a sale of product earns and uses one unit. The optimal expected revenue from period on with units left satisfies the (Single Resource) dynamic program
with and . An optimal subset is a maximizer of the problem on the right side. The marginal value of capacity is .
There exists an optimal policy, i.e. a choice of maximizers for all , , such that
The offer set shrinks as capacity runs down, and it is smaller when more periods remain.
Theorem 5 makes the optimal policy a protection level policy: for each product and period there is a threshold such that is offered exactly when at least units remain. The policy can then be stored as numbers instead of a table of subsets, and each product can be controlled separately, which is how airline inventory systems are organized. The paper also shows (Table 2, p. 1330) that the products need not be closed in revenue order: a higher-fare product can be closed before a lower-fare one, so the result is genuinely about nested sets, not about nested fare classes. Talluri and van Ryzin (2004) show that under the multinomial logit model an optimal assortment consists of a number of products with the largest revenues; the Markov chain choice model does not have this property (Table 1, p. 1328), so their structure of the optimal policy does not carry over directly.
The result is proved in the paper. No part of it is formalized on Prove2Me. The monotonicity of marginal values for an abstract choice model is published and proved as RevenueManagement.choice_marginal_values, stated over the definitions RevenueManagement_singleResource; milestone 5 is the same statement for this paper's dynamic program and can be bridged to it. A complete development here produces machine-checked Theorem 2 and Lemma 3 for the Markov chain choice model, which are reusable for any assortment problem under this model.
The obvious argument chooses, for each , any maximizer of the stage problem. This fails: the stage problems have ties, and an arbitrary choice of maximizers need not be nested, so the theorem is an existence statement about a coordinated choice. The dependence of on is through the solution of a linear system, so the effect of adding or removing a product on the other purchase probabilities has no simple sign, and optimal assortments need not be nested by revenue (Table 1, p. 1328). The link between two stage problems is that their revenues differ by the same constant for all products, and what has to be shown is that such a uniform shift moves an optimal assortment in a controlled direction. Revenues in the stage problems, , can be negative.
Products are Fin n, offer sets Finset (Fin n), the paper's is non-strict inclusion . The model is a structure with fields , and the standing assumptions , ; is added as a field because the are probabilities. is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it is the unique nonnegative one. The value function is defined by recursion on the number of periods to go, and is used only for . Maxima over are taken over the finite family of all subsets, so they are attained; dual optimality is "feasible and no worse than every feasible point".
One hypothesis is added to Theorem 5 and milestone 5, and disclosed: , implied by the paper's description of at most one arrival per period (it makes a probability). No sign condition is placed on the revenues, as on the page. Theorem 2 and Lemma 3 are stated for arbitrary real revenues, as the proof of Theorem 5 applies them to . The first inclusion of Theorem 5 is stated for : with units there is no decision, and the paper reads as . The existential requires every in range to be optimal for its stage problem; a statement without that clause would be satisfied by the empty sets and is ruled out.
Theorem 2 and Lemma 3 need LP duality for (Dual) and the (Balance) system; milestone 5 needs the standard induction on the dynamic program, or a bridge to the published choice_marginal_values (with arrival probabilities and choice model ). Proofs of any milestone, and bridges to published Mathlib or platform LP duality results, are welcome.
A retailer or an airline decides which products to make available, and customers choose among what is offered. When a preferred product is missing, many customers substitute to another product instead of leaving. Assortment optimization asks which subset of products to offer so that the expected revenue from a customer is as large as possible, and its answer depends entirely on the choice model used to describe substitution.
The Markov chain choice model was introduced by Blanchet, Gallego and Goyal (EC 2013; Oper. Res. 64(4), 2016), who showed that it contains the multinomial logit model as a special case and proposed it as an approximation of general random-utility choice models. Feldman and Topaloglu (Oper. Res. 65(5), 2017) study revenue management under this model. Their first result, the subject of this mission, is that the assortment problem, a search over all offer sets, is solved by one linear program with variables. The same paper uses this result for its dynamic single-resource and network results, which are the subjects of the companion missions II–IV of this series.
Timeline:
There are products . A customer arrives to purchase product with probability . If the product she visits is offered, she buys it. Otherwise she transitions to product with probability and checks whether is offered, or leaves without buying with probability . Throughout, , and for all .
For an offer set , let be the expected number of visits to product while it is offered (the probability that is purchased) and the expected number of visits to while it is not offered. The pair is the unique solution of the (Balance) equations
With revenue for product , the (Assortment) problem is . Two linear programs enter: the maximization of over the polyhedron
and its dual
For every optimal solution of (Dual), the set is an optimal assortment:
Theorem 2 reduces a combinatorial problem over offer sets to a linear program, so the assortment problem under the Markov chain choice model is solvable in polynomial time. The same structure drives the rest of the paper: the dual variables are used to show that optimal offer sets shrink when all revenues fall by a common amount, to show that the optimal offer sets of the single-resource dynamic program are nested in the remaining capacity and time, and to reduce the choice-based network linear program to a compact one.
The result is proved in the paper. This mission produces a machine-checked version of it and of its supporting lemmas; to the knowledge of the mission author no formalization of the Markov chain choice model exists. The definition layer (the model, the (Balance) solution, and (Dual)) is the first formal encoding of this choice model and is shared, with the same encoding, by missions II–IV.
The obvious route, comparing across offer sets directly, fails because is defined only implicitly through a linear system whose coefficient matrix changes with ; there is no closed-form expression that can be compared across offer sets, and enumerating the sets is exponential. The connection to linear programming needs an exact correspondence between the vertices of and the (Balance) solutions, which is a statement about polyhedra, not about Markov chains. Even well-posedness is not free: existence, uniqueness and nonnegativity of depend on the row sums being strictly below one. Mathlib has extreme points of convex sets but no ready-made theory of vertices of polyhedra or of linear programming duality in this form.
Products are Fin n (0-based), offer sets are Finset (Fin n) (the paper's is non-strict inclusion, so every subset including and is an offer set), and rho j i is , the transition from to . The model structure carries the paper's standing assumptions and (p. 1325) and the implicit nonnegativity . Revenues are arbitrary reals with no sign assumption. is (Fin n → ℝ) × (Fin n → ℝ), and extreme points are Mathlib's Set.extremePoints ℝ.
The pair is a solution of (Balance) chosen by Classical.epsilon; milestone 1 states that it satisfies (Balance), is nonnegative and equals every solution, so all statements are about the paper's and not about a junk value. Every optimum (of (Assortment), of the linear program over , of (Dual)) is stated as "feasible and at least as good as every feasible point", never through sSup or sInf. The goal is stated for every optimal of (Dual), which is what the proof uses; uniqueness of is neither assumed nor claimed. Replacing the hypothesis " optimal for (Dual)" by " feasible for (Dual)" would make the statement false, and an existential over would weaken it; neither is the target.
No hypothesis beyond the paper's is added. Two printed index slips on pp. 1325–1326 (a garbled sum in the discussion after (Balance), and for in the proof of Lemma 1) are not part of any statement here.
Welcome contributions: the existence and uniqueness of (Balance) solutions via Neumann series for substochastic matrices, a characterization of vertices of polyhedra given by equality constraints and nonnegativity, and a strong duality statement usable for this primal–dual pair. These are reusable well beyond this mission.
Counting the objects that avoid every one of a list of conditions is one of the most frequent tasks in enumerative combinatorics: functions that miss no value, permutations that fix no point, integers that share no prime factor with a given number. The Principle of Inclusion-Exclusion converts such a count into an alternating sum of counts of objects that do satisfy prescribed conditions, which are usually far easier to compute. Chapter 7 of Keller and Trotter's Applied Combinatorics (2017 Edition) develops the principle in the abstract language of properties and applies it to three classical questions: the number of surjections, the number of derangements, and Euler's totient function.
This mission formalizes the first two applications, with the chapter's headline result, the closed formula for the number of surjections from an -element set onto an -element set, as its goal. The surjection count answers distribution questions of the form "in how many ways can distinct objects be handed to distinct recipients so that every recipient receives at least one", which the book illustrates with fifteen lottery tickets shared among four grandchildren ().
Let be a finite set and let be a family of properties: for each and each , either satisfies or it does not. For a subset write
so that .
Two families of properties are used.
In Lean, is a type with [Fintype X], the properties are a decidable predicate family P : Fin m → X → Prop, and is AppliedComb.InclExcl.N P S. The two families are AppliedComb.InclExcl.NotInRange n m on Fin n → Fin m and AppliedComb.InclExcl.FixesPoint n on Equiv.Perm (Fin n).
For all ,
Milestones 1 and 2 are the two ingredients the book names for the goal; milestones 3 and 4 are the parallel derangement application, which shares the definition of and milestone 1.
The result itself. The surjection formula is the standard closed form for , where is the Stirling number of the second kind; it gives for and as special cases, and it underlies counts of ordered set partitions, of onto colourings, and of occupancy problems in which every cell is filled. The derangement formula is the standard answer to the hat-check problem and leads directly to the limit (Theorem 7.12 of the book). The Principle of Inclusion-Exclusion in the book's "none of the properties" form is the common tool behind both and behind Möbius inversion in general.
Formalizing it. All results are classical and fully proved in the book. Mathlib contains inclusion-exclusion for unions and intersections of finsets (Finset.inclusion_exclusion_card_biUnion, Finset.inclusion_exclusion_card_inf_compl), the derangement count via its own recurrence (numDerangements, card_derangements_eq_numDerangements, numDerangements_sum), and Stirling numbers of the second kind (Nat.stirlingSecond) with their recurrence, but no closed formula for the number of surjections. The platform has union-form inclusion-exclusion (FamousTheorems.inclusion_exclusion_card_biUnion) and the limit, neither in the property form used here. This mission produces the property-indexed statement of the principle, the two computations, and the surjection count as a cardinality of surjective functions, in a form that downstream missions of the series (generating functions, Pólya counting) can cite.
The proofs are short on paper, and the work lies in the bookkeeping that the page leaves implicit. Two points stand out. First, the Principle of Inclusion-Exclusion is phrased with properties and rather than with a union of sets; connecting the two forms, or proving the property form directly, requires handling sums over the power set of together with the sign in . Second, the step "the result follows immediately, as there are -element subsets of " requires regrouping a sum over all subsets by cardinality, which needs Lemma 7.8's statement that depends only on and a count of the subsets of each size. The book's one-line arguments for Lemmas 7.8 and 7.10 ("a string of length from an alphabet of letters", "a permutation among the remaining positions") are counting identifications that have to be made precise for subtypes of Fin n → Fin m and of Equiv.Perm (Fin n).
Fin n ; this is an index shift only.Fintype.card {f : Fin n → Fin m // Function.Surjective f} and is Fintype.card {σ : Equiv.Perm (Fin n) // ∀ i, σ i ≠ i}. Defining by the formula, or by the sum, would make the goal hold by rfl; the counts are therefore cardinalities of the sets the book describes. is also not stated through Nat.stirlingSecond, which counts unordered partitions and differs by a factor .A complete development needs only Mathlib's finite-set, power-set and binomial-coefficient API. The property-form inclusion-exclusion (Theorem 7.7) and the two lemmas are reusable for other sieve-type counts, for example Euler's totient function (Theorem 7.14 of the book), which is not part of this mission. Proofs of any milestone independently of the others are welcome, as are alternative proofs of the goal (for instance via exponential generating functions) that do not pass through Theorem 7.7.
List colouring asks for a proper colouring of a graph in which every vertex takes its colour from its own prescribed list. A graph is -choosable if such a colouring exists for every assignment of lists of size . Choosability is harder to guarantee than colourability: planar triangle-free graphs are 3-colourable (Grötzsch) but not all are 3-choosable (Voigt, 1995), and planar graphs are 4-colourable but not all 4-choosable (Voigt, 1993), while every planar graph is 5-choosable (Thomassen, 1994).
A long line of work asks which forbidden cycle lengths make a planar graph 3-colourable or 3-choosable, motivated by Steinberg's conjecture (every planar graph without cycles of lengths 4 and 5 is 3-colourable), which was disproved by Cohen-Addad, Hebdige, Král', Li and Salgado (arXiv:1604.05108).
Timeline.
All graphs are finite and simple. A list assignment gives each vertex a finite set of colours; an -coloring is a map with for all and on every edge . is -choosable if an -coloring exists whenever for all .
Write for a set of colours. A -correspondence assignment assigns to each edge a partial matching between and . A -coloring is a map such that and are not matched in for any edge . Ordinary colouring is the case where every matches equal colours.
For a closed walk (), is inconsistent on if there are colours with for every and ; otherwise it is consistent on . is consistent if it is consistent on every closed walk. An edge is straight if only matches equal colours, and full if is a perfect matching.
A plane graph is a graph with a fixed drawing in the plane without crossings; its faces are the connected components of the complement of the drawing, and a vertex is incident with a face if it lies in the face's closure. A graph is planar if it has such a drawing.
Theorem 8 implies Theorem 6 (), and Theorem 6 with Lemma 5 implies Theorem 1.
The result. Theorem 1 settles Borodin's question and is still the best known forbidden-interval result for 3-choosability of planar graphs with triangles allowed. Theorem 6 is a strengthening in the correspondence setting, and Theorem 8, a precolouring-extension statement, is the form used for induction. The broader contribution is correspondence colouring itself: it allows reductions that identify vertices, which list colouring does not, and it has since been developed by Bernshteyn, Kostochka, Pron and many others as DP-colouring.
Formalizing it. The results are proved in the paper; none has a machine-checked proof. Mathlib has no planarity, no list colouring and no correspondence colouring. This mission produces the first formal definitions of -choosability and correspondence colouring on the platform, the equivalence between list colouring and consistent correspondence colouring (Lemma 5), and a formal statement of the planar result, together with the paper's reduction lemmas as independent targets.
Lemma 5 and Lemma 7 are finite combinatorics. The main obstacle is Theorem 8. The natural list-colouring argument by reducible configurations fails: reductions for ordinary colouring identify two vertices, which is meaningless when their lists differ. Correspondence colouring removes that obstruction only when the identification does not create parallel edges or short cycles, and the main reduction (Lemma 12) needs consistency on triangles, which is why Theorem 6 carries that hypothesis. On the formal side, the proof uses planar topology: faces, the open disk bounded by a cycle, 2-connectedness of a minimal counterexample, and a discharging argument over faces that relies on Euler's formula. None of this exists in Mathlib.
Conventions committed to in the Lean statements:
SimpleGraph V on a Fintype vertex type; the paper's graphs are finite and simple (p. 3).α : Type and lists L : V → Finset α of cardinality exactly .M u c v d on V × Fin k × V × Fin k that lives on edges, is symmetric, and is a partial matching. The paper's is Fin k.G.Walk v v through getVert. The paper's example of Figure 1(a) (p. 5) was checked against this definition by a sorry-free local proof.ℝ × ℝ: injective vertex positions, no vertex on a non-incident edge, and disjoint segments for edges with no common end. These are the clauses of the platform's OPG401.IsPlanar. By Fáry's theorem this is equivalent to planarity for finite simple graphs, and every plane graph has a straight-line drawing with the same faces. Faces are components of the complement of the drawing, incidence is membership in the closure, and the outer face is the unbounded face. Theorem 8 is stated for every drawing and any face, not only the outer one.Type. The measure counts ordered pairs, which gives the same lexicographic order. A minimal counterexample is minimal among all targets of this kind.Formalizations that would trivialize or change the problem are ruled out:
Infrastructure needed and reusable beyond this mission: planar straight-line drawings and their faces (Euler's formula, the Jordan curve theorem for polygons), 2-connectivity and facial cycles, and a DP-colouring library (renaming, consistency, Lemma 5). Contributions to any of these are welcome. So are proofs of Lemma 5 and Lemma 7, which need no topology.
Insertion heuristics build a traveling salesman tour one city at a time: start from a single city, and at each step choose a city not yet on the subtour and splice it into the subtour where it lengthens the subtour least. Local search heuristics start from a tour and repeatedly replace a few of its edges by others while this shortens the tour. Both families are standard in practice, and a natural engineering idea is to combine them: run an insertion heuristic, then polish the result by local search. The question this mission formalizes is whether local optimality of the insertion tour certifies anything about its quality.
Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) answered this for graphs satisfying the triangle inequality. Their §4 proves that nearest and cheapest insertion always return a tour of length at most times the optimal length, and their Theorem 5 shows this bound is attained. Their §7 then shows that the very tour attaining the bound is -optimal for every : no exchange of edges shortens it. So the insertion bound is tight even for tours that local search with -changes cannot improve.
Timeline, as far as this mission is concerned:
A traveling salesman graph on nodes is the node set with a distance that is symmetric and satisfies the triangle inequality . A tour is a Hamiltonian circuit; its length is the sum of its edge lengths; OPTIMAL is the least length of a tour. As in the paper, the identically zero distance is excluded, so OPTIMAL .
A subtour is a circuit on a subset of the nodes (a single node is a subtour without edges). For a subtour and a node , TOUR is obtained by deleting an edge of minimizing and adding and ; COST is the resulting increase in length. An insertion method chooses nodes , starts from and sets ; INSERT is the length of . Nearest insertion chooses minimizing over ; cheapest insertion chooses minimizing COST. Ties are broken arbitrarily.
A -change of a tour deletes of its edges and adds other edges so that another tour is obtained. A tour is -optimal if no -change produces a strictly shorter tour.
The extremal instance is the circle : cities equally spaced on a circular road, with the smallest with or . The insertion run of Theorem 5 inserts the cities in the order and produces the zig-zag tour : city 1, then the even cities in increasing order, then the odd cities in decreasing order.
For and there is a traveling salesman graph with OPTIMAL on which some run of nearest insertion, and some run of cheapest insertion, return a -optimal tour with
The result. The Corollary shows that the worst-case guarantee of nearest and cheapest insertion cannot be improved by requiring that the returned tour survive -change local search, for up to a quarter of the number of cities. Theorem 6 says more generally that -optimality with does not bound the ratio to the optimum below . Together with the paper's upper bound, the insertion guarantee is exact, and it stays exact after local polishing with small neighbourhoods.
Formalizing it. All statements are proved in the paper; none, to our knowledge, has been machine-checked. The platform has an upper bound for nearest insertion (SupplyChainTheory, Theorem 10.7, ratio at most 2) but no tightness example and no notion of -optimality. This mission produces a reusable definition of -changes against arbitrary tours, the circle metric, and the parity-counting argument on a cycle, and it supplies the calculations the paper omits ("We omit these calculations but note that they require the assumption ").
Two steps carry the weight. First, the omitted calculations for the insertion run: at each stage one must show that inserting between and minimizes the insertion increase over every edge of the zig-zag subtour, and that no other outside city can be inserted for less than 2; the claim fails for and , so the verification must use in an essential way. Second, -optimality is a statement about every tour at edge difference , not about 2-opt segment reversals or any specific move family. A search over moves of a special form does not establish it; the argument must bound the length of an arbitrary tour at edge difference from below.
Nodes are Fin n, so the paper's node is index and is index ; subtour indices stay 1-based (, approximation ). A distance is d : Fin n → Fin n → ℝ with the structure IsTSPDist (symmetric, nonnegative, triangle inequality, and ; the last is a normalization absent from the paper that changes no length). A tour is an Equiv.Perm (Fin n), a subtour a list read cyclically; OPTIMAL is Finset.univ.inf' over permutations, the true minimum. TOUR is insertion at a position minimizing the new length; COST is a minimum over positions; the nearest-insertion distance (4.1) takes values in WithTop ℝ, so no junk value arises. -optimality compares the tour with every permutation whose edge set (unordered pairs) misses exactly of the tour's edges. Ratios are multiplied out.
COUNT needs a choice of shortest arc for antipodal pairs when is even; the formalization takes the arc through . The paper's argument does not depend on this choice.
Deviations from the printed text: the Corollary is stated for (the printed statement says only , but its proof uses the example of Theorem 5, which exists for ; for , the printed statement is false). Theorem 6 keeps its printed . In the proof of Theorem 5 the paper writes "(4.2) holds" where the cheapest-insertion condition (4.3) is meant; the formal statement uses (4.3).
The existence statements carry OPTIMAL , the paper's standing assumption (1.1). Without it, the zero distance would make every length zero and every tour -optimal, which would satisfy the ratio equations trivially; that formalization is ruled out.
Contributions welcome: proofs of any milestone, in particular the omitted insertion calculations and the parity lemma, and reusable lemmas on cyclic lists and edge sets of permutations.
In a combinatorial auction a set of items is sold to bidders who value bundles of items rather than single items. Spectrum auctions, procurement of transportation lanes and the allocation of cloud resources all have this form, and the central algorithmic question is how to allocate the items so as to maximize the social welfare, the sum of the bidders' values for what they receive. Even to describe a general valuation takes numbers, so algorithms access the bidders through queries, and the achievable approximation depends on the class of valuations allowed.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) study bidders without complementarities. For the class of XOS valuations, maxima of additive valuations, which strictly contains the submodular valuations, they give LP-based algorithms and, in §3.3, a purely combinatorial algorithm: bidders arrive one at a time, take their demanded bundle at the current item prices, and raise the prices of what they took. Its analysis charges the welfare of any allocation to the item prices the algorithm sets, an argument that uses only the demand and XOS oracles.
The items are and the bidders .
The greedy price-update algorithm. Start with all bundles empty and all prices . For : let be bidder 's demand at the current prices; remove the items of from the bundles of the earlier bidders; let be the maximizing clause for in ; set for . Write for the prices after stage (), , and for the final bundles.
In the Lean development these objects are XOSExpr, XOSExpr.val, IsAllocation, welfare, IsDemandOracle, IsXOSOracle, greedyState, greedyPrices and greedyAlloc in the namespace ComplementFreeCA.XOSGreedy.
For XOS valuations , every demand oracle and every XOS oracle, and every allocation ,
The comparison with every allocation is the paper's comparison with the optimal allocation.
Three further statements are included without being milestones: the output is an allocation (used implicitly by the paper); the first sentence of the proof of Lemma 3.6, that with one has ; and the factor is attained on the paper's two-item, two-bidder example (p. 9).
Theorem 3.3 shows that a factor-2 approximation of the optimal welfare for XOS bidders needs no linear program: one pass over the bidders, one demand query and one XOS query each. The paper's LP-based algorithm of §3.2 attains the better ratio , and Theorem 4.1 of the paper shows that for the larger class of complement-free bidders no -approximation is possible with polynomial communication.
The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. This mission produces a formal model of XOS valuations, demand and XOS oracles and the greedy run that is reusable for other price-based arguments, and a formal proof of the guarantee for every tie-breaking in both oracles.
The argument is elementary, but its bookkeeping is where a formal proof can go wrong. Items move between bidders: an item taken from an earlier bidder in step (b) is re-priced in step (d), and every priced item lies in exactly one final bundle. Lemma 3.4 needs this invariant across all stages, together with the fact that a maximizing clause for the demanded set bounds on every subset, which holds because it is a clause of itself, not merely an additive function agreeing with on . Lemma 3.5 is a contradiction argument using optimality of the demand; Lemma 3.6 telescopes the price increases and needs prices to stay nonnegative. The argument must hold for arbitrary oracle answers, so no canonical demand can be assumed.
Fin n, items Fin m, bundles Finset (Fin m), values in ℝ. An XOS valuation is represented by its expression: a nonempty Finset (Fin m → ℝ) of clauses with nonnegative entries, evaluated with Finset.sup'. The paper's standing assumptions, normalized and monotone valuations (p. 1), hold automatically in this representation.dem : Fin n → (Fin m → ℝ) → Finset (Fin m) and cl : Fin n → Finset (Fin m) → (Fin m → ℝ) with hypotheses IsDemandOracle and IsXOSOracle; every theorem holds for every such pair, so no tie-breaking rule is fixed.Contributions welcome: proofs of the three milestones and of the goal, and reusable lemmas on the invariant that every priced item lies in exactly one final bundle.
In a combinatorial auction a seller offers indivisible items to bidders, each of whom values bundles of items rather than single items. Allocating the items so as to maximize the total value (the social welfare) is the central optimization problem of the area: it models spectrum auctions, procurement and resource allocation, and it is NP-hard and hard to approximate for general valuations. A large literature therefore studies restricted classes of valuations without complementarities. Among them the class XOS (valuations that are a maximum of additive valuations, also called fractionally subadditive) sits strictly between submodular and subadditive valuations and has become a standard benchmark class in algorithmic game theory.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010) gave, among other results, a randomized algorithm that approximates the optimal welfare for XOS bidders within a factor , which is at most . The algorithm rounds the standard LP relaxation and resolves conflicts between bidders using the XOS structure. This mission formalizes that guarantee (Theorem 3.2 of the paper).
A short timeline: Lehmann, Lehmann and Nisan (EC 2001) introduced the XOS terminology and a 2-approximation for submodular bidders; the conference version of the present paper (STOC 2005) gave the bound for XOS with demand and XOS oracles; Feige (STOC 2006) extended the ratio to XOS bidders with demand oracles only and gave a 2-approximation for subadditive bidders.
Items are and bidders are with . Bidder has a valuation assigning a real number to every bundle . An allocation is a tuple of pairwise disjoint bundles; its welfare is .
A clause is an additive valuation given by nonnegative item values , with . A valuation is XOS if there is a nonempty finite set of clauses with
A clause of attaining the maximum for is a maximizing clause for in ; an XOS oracle returns one (arbitrarily, if several attain it).
The LP relaxation has a variable for every bidder and bundle and asks to maximize subject to for each item , for each bidder , and .
Randomized rounding draws a preallocation : independently for each bidder , bundle is chosen with probability and the empty bundle with the remaining probability . The preallocation can give an item to several bidders.
The algorithm of §3.2: (i) draw a preallocation from an optimal LP solution ; (ii) let be the maximizing clause for in ; (iii) give each item to a bidder with for all . Write for the welfare of the resulting allocation.
For every XOS profile, every optimal LP solution , every choice of maximizing clauses, every tie-breaking in step (iii) and every allocation ,
Milestone 5 is stronger than the goal (it compares with the fractional value); the goal is stated against the integral optimum because that is what Theorem 3.2 asserts.
The bound is a constant-factor guarantee for a class that includes every submodular valuation, obtained from nothing more than the LP relaxation and the clause structure of XOS. It shows that the integrality gap of the configuration LP for XOS bidders is at most , a fact reused in later work on welfare maximization, online allocation and posted-price mechanisms. The per-item analysis (Lemma 3.3 and Eq. (1)) is the same "" correlation-gap argument that recurs in submodular maximization and prophet-inequality proofs.
The result is proved in the paper. To our knowledge it has no machine-checked proof. This mission produces a Lean statement and proof of the guarantee with the randomness made explicit, a reusable model of the configuration LP and of randomized rounding over bundles, and a formal version of the inequality in Eq. (1), which is independently useful.
Each piece of the argument is short; the work is in the bookkeeping. The preallocation is infeasible, so welfare cannot be read off from the rounding directly; the proof reduces it to per-item quantities and then lower-bounds by comparing with a different assignment of item that is not the algorithm's. The expectation of that auxiliary assignment involves a product of probabilities over bidders ordered by a conditional expectation, and the final bound needs the calculus inequality of Eq. (1) together with a summation by parts. A naive attempt to bound bidder by bidder fails, because a bidder's received bundle is not contained in its preallocated bundle, and the clause values of other bidders decide what it receives.
Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. XOS is stated through its expression: each comes with a nonempty finite clause set of nonnegative clauses, and is attained by a clause of and bounded by all of them. Normalization and monotonicity, the paper's standing assumptions (p. 1), follow from this.A complete development needs finite product distributions over bundles, the AM–GM inequality, monotonicity of , and a summation-by-parts argument. The LP and rounding model are reusable for the other randomized-rounding results of the paper; proofs of any milestone are welcome.
In a combinatorial auction a seller offers indivisible items to bidders, each of whom values bundles of items rather than single items. Allocating the items to maximize total value is the basic welfare problem of spectrum auctions, procurement and resource allocation, and it is the running example of algorithmic mechanism design. For general valuations no polynomial-time algorithm achieves a ratio polynomially better than under standard assumptions, so positive results require restricting the valuations. The most natural restriction is complement freeness (subadditivity): a bundle is never worth more than the sum of its parts.
Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010; conference version STOC 2005) gave the first polynomial-time algorithms with sub-polynomial approximation ratios for complement-free bidders given demand oracles. This mission formalizes their Section 3.1 algorithm, which rounds the linear-programming relaxation of the auction and splits the resulting infeasible solution into feasible ones.
Timeline. Lehmann, Lehmann and Nisan (2001) introduced the complement-free hierarchy and treated submodular bidders. The original version of the algorithm formalized here claimed an ratio; Feige observed that the same algorithm achieves and that its ratio is at least (Feige, SIAM J. Comput. 39(1), 2009). Feige then obtained a constant ratio () for subadditive bidders by a different rounding.
Items are and bidders . Bidder has a valuation assigning a real value to each bundle . Every valuation is normalized, , and monotone, . A valuation is complement free if for all . An allocation is a tuple of pairwise disjoint bundles; its welfare is , and denotes the largest welfare.
The LP relaxation has a variable for each bidder and bundle, with for each item and for each bidder ; its objective is , with optimum . Randomized rounding lets each bidder independently draw bundle with probability and with the remaining probability. The result, a preallocation, has expected welfare but may give an item to several bidders.
The algorithm takes and:
For all sufficiently large , for normalized, monotone, complement-free valuations and an optimal LP solution with value :
Theorem 3.1 was among the first polynomial-time approximation guarantees for welfare maximization with general subadditive bidders, and its layering argument is the standard way to turn an LP solution that is feasible up to a factor into a feasible allocation losing only a factor for subadditive objectives. The same argument applies to the -duplicates auction and reappears in later rounding schemes. Lemma 3.1 is the standard balls-in-bins tail bound behind every load estimate.
The results are proved in the paper; none of them is formalized, on this platform or in Mathlib, as far as searches show. The mission produces a machine-checked version of the algorithm's guarantee with an explicit constant in place of , a precise statement of the probabilistic step, and reusable statements of two concentration inequalities for sums of independent bounded variables.
The combinatorial part (steps (ii) and (iii)) is short. The difficulty is in step (i). The rounding is a product distribution over bundles, while the count of an item is a sum over bidders of indicators that depend on each bidder's whole bundle; connecting the finite product law to independent Bernoulli variables, and then to Lemma 3.1, requires building the independence structure explicitly. Lemma 3.1 itself does not follow from a Chernoff bound with a fixed relative deviation: the threshold grows with while the mean stays at most , and the bound must hold uniformly in the number of variables, which a fixed-deviation Chernoff statement does not give. Finally, the event- bound needs the preallocation's welfare as a sum of independent variables in , which requires rescaling by and monotonicity.
Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity, the paper's standing assumptions (p. 1), are hypotheses of the goal. is the natural logarithm; the paper does not fix a base. The rounding law is written as explicit finite sums over profiles with product weights, so independence across bidders is literal; Lemmas 3.1 and 3.2 are stated measure-theoretically with Mathlib's iIndepFun.
Explicit constants and conventions that replace the paper's notation:
Printed slips resolved in the statements:
Trivializing formalizations are ruled out: the guarantee assumes the item-count bound (without it the layers do not cover the bundles), the probability statements assume an LP-feasible , neither the layer index nor the step-(iv) bidder is fixed, and the ratio is the explicit rather than an unspecified constant. Running time, the ellipsoid method and oracle complexity are out of scope. Contributions of general concentration lemmas for sums of independent bounded variables are welcome and reusable beyond this mission.
Submodularity — the diminishing-returns property on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.
Let be a finite ground set. A function with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): for all ( componentwise max/min), and (TRF[Z]): there is with for all , where is the all-ones vector. An L-convex function is one whose lift to the extended ground set is L-convex; equivalently (Theorem 7.1), satisfies the translation-submodularity axiom (SBF[Z]): for all and all nonnegative integers . Discrete midpoint convexity asks componentwise. For a positive integer, a point satisfies scaled local optimality if for every .
Assume is a positive integer and . (1) If is L-convex with for all , and satisfies for all , then and there is with the componentwise bound
(2) If is L-convex and satisfies the two-sided version, then there is with . The bound is a genuine vector (lattice-order) inequality, not an -norm bound — the form later chapters' applications need.
Theorem 7.1: L-convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L-APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors , mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition .
The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via . The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.
Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.
A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.
The ground set is a Fintype with DecidableEq; is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and
(SBF[Z]) are stated for all of , not restricted to , so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's
structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same
concern for dom f). L-convexity is represented via an explicit lift to Option V,
matching the book's own primary definition, with the direct axiom (SBF[Z]) kept as a
separate object related to it by Theorem 7.1.
A trivializing formalization of the goal would convert its componentwise vector bound into an
-norm bound (losing the direction-of-approach information the vector form carries)
or drop Part (1)'s periodicity hypothesis ; neither is done here.
Propositions establishing dom g as an L-convex set, the L/L relationship (Theorem
7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure
properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets
for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom
vocabulary, mirroring chunks 06→07.
The heat equation and the free Schrödinger equation are the two model evolution equations of linear PDE on . The first describes diffusion and is the prototype of every parabolic equation; the second describes a free quantum particle and is the prototype of dispersive wave equations. Both are solved explicitly by the Fourier transform and by convolution with a Gaussian-type kernel, and the estimates obtained from these formulas (smoothing, and energy bounds, decay) are the tools later used for nonlinear problems: semilinear heat equations, nonlinear Schrödinger equations, Galerkin constructions for general parabolic PDE, and Strichartz estimates.
This mission formalizes Chapter 5, §§5.1–5.3, of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014, author's copy), which follows the presentation of Taylor's Partial Differential Equations (Taylor, vol. I, Ch. 3). The classical material goes back to Fourier (1822) for the heat kernel and to the analysis of dispersion for the Schrödinger group in the twentieth century; the goal and milestones are textbook results with complete proofs in the literature.
Write for Euclidean space with Lebesgue measure, for the Euclidean norm and for the Laplacian. The heat kernel is
and for data the heat convolution is .
The Schwartz space consists of smooth functions all of whose derivatives decay faster than every power of , with the Fréchet topology of the seminorms . A curve on a time interval has a strong derivative at if the difference quotients converge to in ; and are defined with continuous strong derivatives. A Schwartz solution of the heat problem with data is a curve with and for ; a Schwartz solution of the Schrödinger problem is with and for all .
The Fourier transform is used in the book's normalization,
and, with , the Sobolev norm is for .
Let and . Then the heat convolution converges absolutely for , is on , and
If , every derivative of tends to zero as at each fixed , and
This is the chapter's statement that rough data are instantly smoothed while the initial condition is attained in the sense; it involves no Fourier transform.
A further item, not a milestone, records that for (p. 131).
The result itself. Theorem 5.5 is the statement that the heat semigroup maps into smooth functions decaying with all derivatives, and that it is strongly continuous on for . It is used whenever a parabolic problem with rough data is solved by the Duhamel formula, in particular for the semilinear heat equation in the next part of the chapter. Theorem 5.4 and the energy estimates 5.9–5.10 are the input for generalized solutions (Theorem 5.12) and for Galerkin existence for parabolic PDE in Chapter 6. The Schrödinger estimates 5.16–5.17 are the linear input of the local theory of nonlinear Schrödinger equations and of Strichartz estimates.
Formalizing it. All results are classical and fully proved on paper. Mathlib has Schwartz functions, its own Fourier transform on with Plancherel, Gaussian integrals and Fourier transforms of Gaussians, convolution and approximate identities for compactly supported kernels, and the Laplacian on inner-product spaces. It does not have the heat kernel on as a solution operator, the differentiation of Schwartz-valued curves, the energy estimates, or the dispersive estimates for the Schrödinger group. A platform development of the heat kernel exists only on with a viscosity parameter (the Navier–Stokes mission), and the platform's Plancherel theorem is in Mathlib's normalization. The remaining work is to formalize the known proofs in the book's normalization and dimension.
For the goal, the obvious argument is "differentiate under the integral sign and apply the mollifier theorem". Both steps need care in Lean. Differentiation in requires domination of every derivative of uniformly on neighbourhoods of , paired by Hölder's inequality with an arbitrary . The approximation-of-identity result in Mathlib and in the book (Theorem 1.28) is stated for compactly supported mollifiers, whereas has full support, so the convergence needs the Gaussian version with a tail estimate. The decay of all derivatives as relies on . For the Schwartz-space results the difficulty is the calculus of -valued curves: strong differentiability is convergence of difference quotients in every Schwartz seminorm, and uniqueness requires passing from the strong equation to the pointwise ODE for . The bound (5.16) rests on Riesz–Thorin interpolation, which Mathlib does not have.
EuclideanSpace ℝ (Fin n) with volume; coordinates are 0-based (i : Fin n). is Mathlib's Laplacian: on functions for the goal and (5.9), and for the Schwartz solutions. Smoothness is ContDiff/ContDiffOn ℝ ∞.SchwartzMap with its Fréchet topology, the same as the book's. Real-valued for the heat equation, complex-valued for Schrödinger. Strong derivatives, and the two solution predicates are defined in HunterPDE.HeatFourier.SchwartzCurve. Uniqueness in Theorem 5.4 is agreement for .𝓕 is not used. The norm is -valued and is the norm of the book's inner product, ; the norm formula printed with Definition 5.74 places outside the square root, which differs by the constant and does not affect any statement here, since every inequality and identity has an norm on both sides. norms are eLpNorm in , and the factors in Theorem 5.16 are divisions in , so gives the trivial bound .Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.
Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as . The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).
Timeline:
Fix a positive integer and a prescribed time . Let be the canonical basis of , and let be the -th Jordan block, with . The perturbed chain of integrators is
with state and control . Here is a measurable matched disturbance, and is an uncertain control gain with and no upper bound.
With weights , the dilation is and . An admissible weight is a continuous function on with for . It defines
The parameter blows up at , and maps onto . In the coordinates and the time , the system becomes
The feedback studied is , that is in the original variables, where and .
There is a rate depending only on and such that, for every and admissible , there are and with
for every , every , every disturbance , every closed-loop solution, every and every . Since , every coordinate reaches at the prescribed time .
Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline . The guarantee holds for every control gain , however large, and gives an explicit input-to-state bound for the matched disturbance. The weight is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on from the classical LMI, and is of independent use for high-gain and persistently excited systems.
On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.
The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single and must work for all at once. Second, the transformed system carries the time-varying term , and in the original time the feedback gain is unbounded. Estimates must survive both the rescaling by and the change of time. Constants that look harmless in the new time, such as the condition number of and the value , reappear in the original variables, and dropping them makes the printed estimates false.
Lean representation: vectors of are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every in the interval, the right-hand side is integrable on and the integral identity holds. This matches the paper's measurable and . The standing assumptions are (§3), , continuous and nonnegative on with on , and . No upper bound on is assumed anywhere. is replaced by an arbitrary bound of on the interval.
Corrected statements, with milestone texts kept verbatim:
Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to . Every constant is quantified before the objects it must not depend on: the rate before and , before , and before . No statement weakens the estimates to mere convergence.
Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.
The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.
Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.
Timeline of the thread this mission belongs to:
Let be -dimensional Euclidean space and let be a nonempty, closed, bounded, convex set. Its dimension is the dimension of its affine span , the smallest flat containing .
For let be the point of nearest to ; it exists and is unique. The image of with respect to is
the reflexion of through . The reflexion process starts at and sets as long as (3.2). Either the process terminates with some , or it produces an infinite sequence of points outside .
The family of supporting half-spaces of consists of the closed half-spaces whose bounding hyperplane touches . The paper observes that the half-space through normal to is the member of farthest from , so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family .
A sequence of points outside is Fejér-monotone with respect to if and for all . Two points are symmetric with respect to a flat if their midpoint lies in and is orthogonal to .
For every nonempty closed bounded convex with affine span , every and every run of the reflexion process:
No number of steps is fixed: termination is finite but not uniformly bounded.
The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of , so a solution can be read off.
Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.
The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit lies on the boundary of ; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through , which keeps the iterates on a sphere around . For a convex body there are infinitely many supporting hyperplanes near , and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of at boundary points near are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.
Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of to alone can be expected.
EuclideanSpace ℝ (Fin n). is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension ", "the point of nearest to ").IsImage A p p₁ holds when for a nearest point of ; the nearest point is not chosen by a function. For closed convex nonempty this relation is a function on . A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering are unconstrained. Every statement quantifies over every run from every ; a formalization that only asserts the existence of some terminating run is ruled out.affineSpan ℝ A; is affineSpan ℝ A = ⊤, is affineSpan ℝ A ≠ ⊤. No separate natural number is introduced.IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires and strict alternation for (strict inequality, as printed).frontier A; distances to sets are Metric.infDist.exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.
Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).
Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.
Fix a dimension and an matrix whose transpose is substochastic: all entries of are nonnegative and every column sum of is at most . Assume also as . With Markovian routing, is the routing matrix of an open network of queues.
Vectors carry the norm , and matrices carry the maximum absolute column sum (Eq. (2.5)). is the space of paths that are right-continuous with left limits on . For a path , is the vector of coordinatewise sup norms, , and .
The reflection of is the pair with and
The last condition says that increases only when . In queueing terms, is the vector of queue contents and the cumulative idleness. The operator , where coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write .
For all with reflections ,
The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on .
Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod and topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order in the netput produces an error of at most in the idleness process.
On the formal side, the results are proved in the paper, but neither the reflection map nor has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.
The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of is allowed at a time where even if was positive just before. Existence needs the iterates to converge in and the limit to satisfy (2.1)–(2.3). The explicit constants involve , and . The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from .
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to matters. Membership in is the predicate IsCadlagOn T x: right-continuous on , left limits on , and (redundantly) bounded on . The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure of is zero". For this is equivalent to . is Nat.iterate, is Mathlib's matrix inverse (invertible under the standing assumptions), and is a tsum stated together with its summability.
Corrections and conventions, each disclosed in the item concerned:
A trivializing formalization would read (2.3) through a Bochner integral, which is for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.
Welcome contributions: a general API for càdlàg paths on (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.
MAXIMUM SATISFIABILITY asks for a truth assignment satisfying as many clauses of a given set as possible. It was among the first NP-hard optimization problems for which an approximation algorithm came with a proven worst-case guarantee. In Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 1974, doi:10.1016/S0022-0000(74)80044-9), David S. Johnson set up a framework for measuring such guarantees and analyzed two heuristics for the problem. The second of these, algorithm B2, weights each clause by and repeatedly sets a literal so that the heavier side is satisfied. On inputs whose clauses all have at least literals, it satisfies at least a fraction of the optimum.
B2 is the ancestor of a line of work on MAX-SAT approximation:
A literal is a variable or its negation . A clause is a finite set of literals. A truth assignment is a set of literals containing no pair ; it satisfies a clause when . An input is a finite set of clauses, and is the largest over subsets satisfied by one truth assignment. MS(k) is the restriction to inputs in which every clause contains at least distinct literals.
Algorithm B2 keeps a set SUB of satisfied clauses, a set LEFT of unsettled clauses, the literals LIT still available, and a weight per clause, starting from , , . While some literal of LIT occurs in a clause of LEFT, it picks any such literal . Let YT be the clauses of LEFT containing and YF those containing . If , it makes true, moves YT to SUB and doubles the weight of each clause of YF; otherwise it does the symmetric move with . Finally it removes from LIT. When no literal of LIT remains in LEFT it returns SUB.
The choice of is free, so several outputs may be choosable on one input. Johnson measures the algorithm by its worst choosable output, through the ratio and its maximum over inputs of size at most .
For every , every in MS(k) and every SUB choosable by B2 on ,
and for every there are in MS(k) and a choosable SUB with and
The paper states equality "for all sufficiently large " for every . At this is false: the ratio 2 would require every clause to be a unit clause and all clauses to be jointly satisfiable, and on such inputs B2 satisfies everything. The goal therefore asserts tightness for . A separate item states that at the ratio is never attained.
The bound is exactly the expected fraction of clauses a uniformly random assignment satisfies on MS(k). B2 attains it deterministically, and the proof bounds against rather than against , a feature the paper points out. For the constant was later shown by Håstad (2001) to be optimal among polynomial-time algorithms unless P = NP, so the guarantee of this 1974 algorithm is best possible for MAX-E3-SAT.
Formalizing the result produces a machine-checked potential-function argument for a nondeterministic algorithm: the invariant links each clause's weight to how many of its literals have been removed. The mission also records a correction to the printed statement at . The paper's proof is complete; to our knowledge no machine-checked version exists.
The obvious argument follows the counting proof for algorithm B1 and compares clauses saved with clauses wounded in each step. It fails here: B2 can wound more clauses than it saves in a step, and the bound holds only in the weighted sense. The weight of a clause is not a static quantity. It is times to the number of its literals already discarded, and this invariant must be carried through every step, including clauses that contain both and . Tightness needs an explicit input and an explicit adversarial run that exploits the tie in Step 4, and then a proof that every assignment of the remaining variables kills exactly one clause.
Finsets of literals, and an input is a Finset of clauses, so there are no duplicate clauses. Truth assignments are partial and consistent. is a maximum over the finite, nonempty family of satisfiable subsets.The definitions (the MS layer, the run relation) can be reused by other MAX-SAT approximation results, and an identical MS layer appears in the companion mission on algorithm B1. Contributions welcome: proofs of the milestones, of the tightness family, and of the correction.
An insurance company collects premia and pays claims each period; the difference is a random, signed quantity that can push the company's risk reserve up or down. At the start of every period, before that period's premia and claims are realized, the company's owners may pay themselves a dividend out of the current reserve — but once the reserve goes negative the company is ruined and stops operating for good. How should the owners time and size these payments to maximize the total expected discounted dividend paid out before ruin? This is the classical De Finetti dividend problem, one of risk theory's oldest optimization questions, and Chapter 9 §9.2 of Bäuerle and Rieder's Markov Decision Processes with Applications to Finance (Springer, 2011) solves its fully discrete-time version by identifying the exact combinatorial shape of the optimal policy — not just proving one exists. This mission also covers §9.1, a different application of Chapter 7's contracting theory to a consumption-investment problem whose planning horizon is itself random rather than fixed or infinite.
The dividend model is a stationary Markov Decision Model on the integers: the state is the current risk reserve, the action (for ; only is available once ruined) is the dividend paid, the reward is , and the reserve evolves by i.i.d. increments (premia minus claims) after the dividend is deducted. Because the reward is bounded by an explicit function of the state (Lemma 9.2.2), Chapter 7's general existence theory applies directly, and the value function satisfies a genuine Bellman equation. The chapter's real content begins once existence is established: Theorem 9.2.3 pins down enough analytic structure of and its largest-maximizing policy (monotonicity, a Lipschitz-type inequality, and a self-consistency identity) to drive a purely combinatorial argument that 's shape is a finite alternation of "pay nothing" and "pay down to a fixed level" intervals — a band-policy (Definition 9.2.5). Section 9.1's random-horizon consumption-investment model reuses the same Chapter 7 machinery in a different setting: the usual (consumption, portfolio) decision each period, but where the horizon itself ends after each period with probability , making the effective one-period discount rather than .
The goal, Theorem 9.2.9, states the section's main claim in one sentence: the stationary policy is optimal and is a band-policy. Short as it is stated, its proof assembles every earlier result of the section. The milestones supply that assembly, in order: Lemma 9.2.2 gives the model's bounding function and the resulting integrability/convergence facts; Theorem 9.2.3 gives the value-function bounds and the self-consistency identity ; Corollary 9.2.4 checks the two sign-definite degenerate cases directly from Theorem 9.2.3; Proposition 9.2.6 proves the top threshold is finite (not merely well-defined) and that is a simple barrier above it; Proposition 9.2.8 proves the increment property below that forces each band's shape; and Theorem 9.2.10 (a postscript refinement, stated after the goal) shows the wave lengths are bounded once the reserve's downward jumps are themselves bounded, collapsing to a single barrier-policy in the extreme case. Theorem 9.1.1, the random-horizon consumption-investment verification theorem, is included as a full item but is not a milestone of this goal, since its content and proof belong to a different, disjoint model — see Difficulty.
Band-policies and the discrete-time De Finetti dividend problem have no substrate anywhere in Mathlib or on the platform, and the result is a genuinely deep, classical one: a discrete-time analogue of the continuous-time De Finetti barrier-strategy theory, obtained here by pure dynamic-programming argument rather than the stochastic-calculus techniques the continuous-time theory usually relies on. The mission is explicit that the goal's conclusion is the general band-policy structure, not the strictly weaker barrier-policy special case that Theorem 9.2.10 b) proves only under an extra hypothesis (bounded downward jumps) — stating the goal with a barrier-policy conclusion instead would understate what Theorem 9.2.9 actually proves.
The central formalization challenge is Definition 9.2.5's own combinatorial intricacy: a
band-policy is specified by an alternating chain of thresholds with a positive-width gap condition on every wave, and the policy's four
piecewise branches case-split on which wave (if any) the current state falls into. This mission
renders it existentially over the witnessing rather than as one closed-form function, a
faithful but more verbose transcription that avoids conflating the different branch conditions.
A second difficulty is Proposition 9.2.6's own finiteness claim: is a supremum over a
subset of that could, in principle, be unbounded, and Mathlib's convention for
sSup over the naturals returns a finite junk value () even for an unbounded set — using it
directly would silently trivialize "" into a claim that is true regardless of the
proposition's actual mathematical content. This mission instead states the proposition by
exhibiting the finite value of directly, so that " is finite" survives as genuine
content that the theorem's proof must establish. A third difficulty is scope: Theorem 9.1.1's
random-horizon consumption-investment model shares no state space, action space, or definitions
with the dividend model of the goal, despite both appearing in this chunk's assigned page range;
it is formalized as a genuine application of a locally-restated copy of Chapter 7's contracting
theory, but is excluded from the milestone list proper since it plays no role in the goal's own
proof.
The dividend model's transition law is built from Mathlib's PMF (probability mass function)
type on , which supplies the "probabilities sum to one" fact automatically rather than
as a separate hypothesis. J_\infty, \delta, and every finite-horizon value function throughout
this mission use this whole book series' Filter.limsup-of-truncations convention for
infinite-horizon reward, restated locally (own namespace copy, per this series' file-ownership
boundary) from chunk 07a's identical apparatus rather than imported. The consumption-investment
model of §9.1 is formalized with the number of risky assets as an explicit type parameter and
its admissible-portfolio and domain restrictions as separate, citable fields rather than folded
silently into the reward or transition definitions.
Training a statistical model by empirical risk minimization means minimizing an average of losses over a parameter vector , where both and can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.
Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).
Let be twice continuously differentiable losses and
For a sample of size , the minibatch gradient is . For a sample of size , the subsampled Hessian is .
Assumption 1 requires constants with for every and every Hessian sample. It also requires a bound on the second moment of the stochastic gradient. denotes the minimizer of .
Algorithm 2 turns correction pairs into a matrix . With , it starts from and applies the BFGS update
for .
Algorithm 1 (SQN) runs for . It draws a gradient sample and steps
where for and , , afterwards. Every iterations it forms the block average of the last iterates and a new pair
Samples are drawn independently and uniformly among the subsets of their size. The step length is .
There are , depending only on the problem data, such that every matrix Algorithm 1 applies satisfies . Moreover, for every ,
The constants are not fixed numerically. The goal asserts a rate of order with an explicit constant in terms of them.
The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.
The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.
The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.
On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of that is uniform over all runs and all . The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.
Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices start at as in the paper. In the corollary, is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. and are -measurable, the sample is -measurable, and unbiasedness is a conditional expectation. Integrability of is part of each conclusion, so a junk-zero integral cannot satisfy it.
Two corrections to the paper, each labelled in the item titles and notes:
Smaller conventions:
Trivializing encodings are ruled out: is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all .
Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.
The classical separating hyperplane theorem says that any two disjoint convex sets in can be separated by a hyperplane with an arbitrary real normal vector. When the sets in question are not arbitrary convex sets but the integer points of specially structured discrete sets, one can sometimes ask for much more: not merely that a separator exists, but that it can be chosen from a small, structured, dimension-independent family regardless of the size or shape of the sets being separated. Results of this kind — "discrete separation theorems" — are a recurring and often surprising theme in combinatorial optimization, playing the role that the ordinary separation theorem plays in continuous convex analysis, but with genuinely combinatorial content beyond it.
L-convex sets, introduced by Murota as part of the discrete convex analysis framework, are one of the two dual families of well-behaved discrete convex sets studied in the book (the other being M-convex sets, chunk 04 of this series). They are defined by a lattice-closure axiom together with translation invariance, and they correspond one-to-one to integer-valued distance functions satisfying the triangle inequality — objects long familiar from network flow theory and shortest-path duality, even though the L-convexity terminology is not traditionally used there. This mission formalizes the chapter's central results, culminating in Theorem 5.9: two disjoint L-convex sets can always be separated by a vector with entries in , no matter how large or complicated the sets are.
Let be a finite ground set. A nonempty set is an L-convex set if it satisfies the sublattice axiom (SBS[Z]) — , where are componentwise maximum and minimum — and the translation axiom (TRS[Z]) — , where is the all-ones vector. A distance function satisfies for every ; it satisfies the triangle inequality if for all . The admissible-potential polyhedron of is
The convex hull of a discrete set is written .
If are disjoint L-convex sets, there exists such that
Dropping the restriction and allowing an arbitrary real separator would recover the classical separation theorem for convex sets, which holds regardless of L-convexity and carries no discrete-convexity content; the three-valued restriction is the weakest correct strengthening and is kept in full.
Theorem 5.2: an L-convex set is hole free () — its integer points are exactly the integer points of its own convex hull. Theorem 5.5: is L-convex if and only if for some integer-valued distance function satisfying the triangle inequality — L-convex sets and such distance functions are two descriptions of the same object, the discrete analogue of chunk 04's M-convex-set / submodular- function correspondence. Theorem 5.7 (parts (1), (4)): L-convex sets are closed under intersection in the strongest sense — the convex hulls intersect exactly where the sets do, and a nonempty intersection of L-convex sets is again L-convex.
The result itself. Theorem 5.9 packs two claims into one, as the book itself points out: the separator is forced into (explicit in the statement), and disjoint L-convex sets satisfy "convexity in intersection" — their convex hulls are already disjoint whenever the sets themselves are (implicit, and necessary for the stated inequality to be possible at all). The structure connects directly to combinatorial duality in network flows: L-convex polyhedra are, without the name, a familiar object there, and a -separator corresponds to a signed cut or a negative-cost cycle in an associated graph. Theorem 5.5's correspondence is the L-convex mirror of chunk 04's M-convex/submodular correspondence, and the book explicitly flags that the two will be unified into a single conjugacy relationship in a later chapter (Note 5.6) — this mission's formalization of the L-side is a prerequisite for that later unification.
Formalizing it. No matching item exists on the platform (searches for "L-convex", "distance function", and "negative cycle" return only unrelated results — number-theoretic distance estimates, polytope graph metrics, shortest-path graph structures — none matching the combinatorial L-convexity/discrete-separation content here). This mission gives the first formal statement of L-convex sets and their central separation theorem. Notably, Theorem 5.9's own statement — unlike the analogous M-convex Theorem 4.18 — needs none of the distance-function machinery that its proof uses; only the L-convexity axiom itself appears in the goal, making its formal statement comparatively lean even though the underlying mathematics is just as deep.
The natural first attempt at Theorem 5.9 is to try to construct directly from the structure of — for instance, from a normal vector to a real separating hyperplane, rounded coordinatewise. This does not work: rounding an arbitrary real separator gives no control over its entries, and there is no reason a rounded vector should still separate. The book's actual proof instead represents via distance functions (Theorem 5.5), combines them into , and extracts the separator from a shortest negative cycle in the associated graph: the vertices of the cycle alternate between the two sets' "tight" arcs, and the alternating pattern around the cycle is exactly the vector — with the cycle's negativity translating directly into the required gap of at least . Locating the right combinatorial object (a shortest negative cycle, not an arbitrary one) is what pins the separator down to a vector supported on a single alternating cycle rather than an arbitrary pattern, and is the step a naive rounding or linear-algebra argument has no analogue of.
The ground set is a Fintype with DecidableEq; is a
Set (V → ℤ). Distance functions take values in WithTop ℝ; the goal's infimum and supremum
are taken in EReal (a complete lattice), since L-convex sets are always infinite (translation
invariance along the all-ones direction), so an ℝ-valued supremum/infimum would silently
return a junk value on an unbounded set. The conclusion is stated as
, an addition-based
reformulation of the book's subtraction inequality that avoids EReal's ⊤ - ⊤ ambiguity while
remaining equivalent whenever both sides are finite.
A trivializing formalization of the goal would drop the constraint on
(recovering the classical, L-convexity-independent separation theorem) or fix a single
coordinate pattern rather than asserting existence over the full three-valued family; neither is
done here. Theorem 5.5 is stated existentially rather than via the book's named bijection
(a documented scope reduction, parallel to chunk 04's treatment of Theorem 4.15),
and Theorem 5.7 is drafted with only its two representation-independent clauses (parts (1) and
(4); see MODERATION_NOTES.md). Contributions building the distance-function/admissible-
potential apparatus needed for Theorem 5.7's remaining clauses, or the L-convex/integrally-convex
bridge (Theorem 5.10, needing chunk 03's vocabulary), are welcome.
Matroid intersection is one of the founding results of combinatorial optimization: given two matroids on a common ground set, the largest common independent set can be found in polynomial time, and its size equals the minimum of a natural upper bound ranging over all subsets — a min-max theorem in the spirit of König's theorem and Menger's theorem, but for a strictly richer combinatorial structure. Jack Edmonds proved this in 1970, and Jack Edmonds and Rick Giles's subsequent generalization to submodular flows, together with André Frank's discrete separation theorem for submodular and supermodular set functions (1982), placed matroid intersection inside a single unifying framework: submodular function duality. This framework explains, in one stroke, matroid intersection, the base-exchange structure of matroids, and a family of other combinatorial min-max theorems that had previously seemed unrelated.
Murota's Discrete Convex Analysis develops this framework as the theory of M-convex sets: sets of integer vectors satisfying a lattice-exchange axiom that turns out to be exactly equivalent to being the integer points of a base polyhedron of an integer-valued submodular set function. This mission formalizes the chapter's central results: the equivalence of four variant forms of the exchange axiom (Theorem 4.3), the M-convex set / submodular function correspondence (Theorem 4.15), Frank's discrete separation theorem (Theorem 4.17), and Edmonds's intersection theorem itself (Theorem 4.18) — the deepest duality result in the theory of submodular functions and the historical origin of the M-convexity concept that the rest of the book generalizes to real-valued functions.
Let be a finite ground set. A set function with and is submodular (the class ) if
Its base polyhedron and submodular polyhedron are
where ; a supermodular function is one with submodular. A nonempty set is an M-convex set if it satisfies the exchange axiom (B-EXC[Z]): for and in the positive support of , there is in the negative support of with both and , where is the characteristic vector of . A polyhedron is integral if .
For submodular set functions ,
with both sides attained. If are integer valued, is an integral polyhedron and the maximum is attained at an integer point. Dropping the integrality clause and stating only the real max-min equality would leave ordinary LP duality with no discrete content at all; this mission keeps it in the goal at every strength the book proves it.
Theorem 4.3: the exchange axiom (B-EXC[Z]) is equivalent to three variants that impose the exchange condition asymmetrically or only for distinct vectors — groundwork establishing that M-convexity does not depend on which variant is taken as primitive. Theorem 4.15: is M-convex if and only if for some integer-valued submodular — M-convex sets and integer-valued submodular set functions are two descriptions of the same combinatorial object. Theorem 4.17 (Frank): if a submodular dominates a supermodular pointwise, a single vector separates them ( pointwise on every subset), integrally when are integer valued — derived, in the book, as a direct corollary of the goal theorem.
The result itself. Edmonds's intersection theorem is the min-max theorem underlying polynomial-time matroid intersection (a matroid's rank function is submodular, so the classical matroid intersection theorem is the special case both matroid rank functions), and its generality — arbitrary submodular set functions, not just matroid ranks — is what lets Frank's discrete separation theorem, and through it a wide range of combinatorial duality results in network flows, scheduling, and matroid theory, be derived as corollaries rather than proved from scratch each time. The integrality clause specifically is the fact that makes these duality theorems combinatorial: it guarantees that optimal fractional solutions to the underlying linear program can always be taken integral, without which the connection to discrete optimization would be lost.
Formalizing it. No matching item exists on the platform (searches for "submodular set
function", "base polyhedron", "matroid intersection" return no relevant hits; Mathlib's
Combinatorics/Matroid/ develops matroid rank functions, a special case, but not general
submodular set functions or their polyhedra). This mission gives the first formal statement of
the theorem at its natural generality, together with the M-convex-set viewpoint that motivates
the rest of the book, and Frank's separation theorem as an explicit worked corollary.
The real-valued half of Theorem 4.18 is ordinary LP duality applied to a cleverly chosen primal program (maximize over ) and its dual — routine once the right LP is written down. The integrality half is where the combinatorics enters: an optimal dual solution can always be chosen supported on a chain in each 's effective domain (an extremal argument maximizing a strictly convex potential over the optimal dual face), and the incidence matrix of a chain of subsets is totally unimodular — this is the fact, external to ordinary LP theory, that forces an integral optimal solution to exist whenever the data () are integral. A proof that stops at real-valued LP duality, however carefully done, misses this step entirely and cannot produce the integrality clause; total unimodularity of a chain's incidence matrix is the one piece of combinatorics doing all the discrete work in an otherwise classical convex-duality argument.
The ground set is a Fintype with DecidableEq; subsets are Finset V, vectors are
V → ℝ/V → ℤ. Submodular functions take values in WithTop ℝ (exactly ); supermodular functions in WithBot ℝ; comparisons across the two use an explicit
embedding into EReal. The max/min in the goal are stated via IsGreatest/IsLeast sharing a
common EReal witness, so that "both sides attained, at the same value" — not merely "sup
equals inf" — is what the Lean statement asserts, which is essential since the integrality
clause's whole content is about which point attains the maximum.
A trivializing formalization of the goal would drop the integrality clause (leaving unqualified
LP duality) or replace IsGreatest/IsLeast with a bare supremum/infimum equality (losing the
"is attained" content the second half of the theorem needs); both are avoided. Theorem 4.15 is
stated as the existential "iff" (some integer submodular realizes ) rather than
reifying the book's own named bijection explicitly — a deliberate, documented scope
reduction of that one milestone (see MODERATION_NOTES.md), not of the goal. Contributions
building the explicit map, the Lovász extension (needed for Theorem 4.16, not drafted
here), or M-convex-set infrastructure reusable by chunks 06–07 (M-convex functions, which build
on this chapter's vocabulary) are welcome.
Every model in Chapters 2-4 assumed the controller sees the whole state before acting. Real control problems rarely offer that: a machine's true wear level, a customer's private valuation, a hidden regime driving asset returns — these are exactly the situations a decision-maker must act on despite never observing them directly, learning about them only through their effect on what is observed. This is the subject of Partially Observable Markov Decision Processes (POMDPs), introduced independently in operations research (K. J. Åström, Optimal Control of Markov Processes with Incomplete State Information, 1965) and studied extensively since as the right model for sequential decisions under hidden state. The central difficulty such a process raises is structural, not just computational: the state includes a component the controller never sees, so the very theory built in Chapter 2 — which assumes the controller's policies can depend on the full current state — does not apply. Bäuerle and Rieder's Chapter 5 resolves this by an idea with a long pedigree in stochastic control (Bayesian filtering, going back to R. E. Kalman and R. S. Bucy's filtering theory, and D. Blackwell's 1965 discounted-dynamic-programming treatment of the "state of information"): replace the unobservable state by the controller's own belief about it — a probability distribution, updated at every step by Bayes' rule — and show the resulting belief-state process is once again an ordinary, fully observed Markov Decision Model.
A Partially Observable Markov Decision Model (Definition 5.1.1) has data : state with observable and unobservable; feasible actions depending only on ; a stochastic kernel giving the joint law of the next state; initial law of ; rewards ; discount . A policy (Definition 5.1.3) is a sequence of decision rules , each depending only on the observable history — never on any . The objective
(Equation (5.2)) carries an extra expectation over the unknown that Chapter 2's objective never had.
Assuming has a density against reference measures, the Bayes operator and the filter recursion , (Equations (5.3)-(5.4)) compute the posterior law of given everything observed, purely from the observable history. Theorem 5.2.1 confirms is genuinely this conditional law. The filtered Markov Decision Model (Definition 5.3.1) then treats as an ordinary, fully-observed state, with its own kernel (built from and the marginal ), reward , and terminal reward .
under the Structure Assumption of Theorem 2.3.8; and if maximizes for each , then defines a policy optimal for the original -stage POMDP. This is where the reduction pays off: an ordinary Bellman equation, of exactly the form Chapter 2 already solves, for a problem that had no Bellman equation at all in its original, partially-observed form.
Lemma 5.2.2 (the filter-recursion identity, the technical engine behind everything that follows), Theorem 5.2.1 (the filter is truly the conditional law — without this, would be merely a formula, not a meaningful belief), and Theorem 5.3.2 (the value of the filtered model exactly equals the value of the original POMDP, policy for policy — without this, solving the filtered model would solve a different problem).
Theorem 5.3.3 is the standard justification, made precise, for the single most common technique
in applied sequential decision-making under uncertainty: replace an unknown parameter or hidden
state by a running Bayesian estimate, and optimize as if that estimate were the true state. This
technique underlies applications from inventory control with unknown demand to adaptive clinical
trial design, and Chapter 5's own closing application (two-armed Bernoulli bandits, taken up in
chunk 05b) is a direct instance. The reduction also has real content beyond convenience: it
shows the value is unchanged (Theorem 5.3.2), not merely that a good heuristic policy exists —
the filtered model's optimum is the true POMDP optimum, not an approximation to it.
No result of this chapter has a machine-checked proof on Prove2Me at the time of writing, and no substrate exists for POMDPs, filtering, or Bayes-operator constructions on the platform. Formalizing this mission means building, from Mathlib's general kernel and probability-measure infrastructure, the first POMDP/filtering vocabulary on the platform: a policy class restricted to observable histories, a recursively-computable posterior, and the value-equality between a partially and a fully observed reformulation.
The obstacle is not any single hard inequality but a representational one: an admissible policy for the original problem is a function of a growing observable history, not of a fixed-size state, so the value function cannot be written as a simple recursion over a Markov chain the way every earlier chapter's could. The chapter's insight is that the belief — even though it is a probability-measure-valued object, not a point in a fixed Euclidean space — is itself Markov: depends on the observable history only through , never on more of the past. Recognizing this, and giving the right measurable structure to serve as a genuine Borel state space, is what makes Definition 5.3.1's reformulation a legitimate Markov Decision Model rather than an informal analogy. A formalization that let 's type be an unstructured "distribution object" with no Borel structure, or that quietly assumed the value functions of the filtered model already satisfy the Bellman equation, would miss this content entirely.
are abstract measurable spaces; the transition kernel is a genuine
MeasureTheory.Kernel, not assumed to arise from an i.i.d.-noise-driven transition function (the
form every earlier finance chapter's market used) — the chapter's own examples (Hidden Markov
Models, Bayesian models) do not have that special form in general. Observable histories are
represented as (junk-padded) sequences , rather than
dependent finite tuples, with a decision rule's dependence on only the first /
coordinates stated as an explicit locality condition; this avoids Fin-indexed-tuple bookkeeping
while remaining exactly equivalent to the book's own typing. The belief state
is MeasureTheory.ProbabilityMeasure E_Y, giving a genuine measurable
structure via its standard weak-topology Borel σ-algebra — the formalization scope this chunk's
own pitfall demands, ruling out an ad hoc encoding of "the space of distributions." The Bayes
operator and the filtered kernel are carried as data (functions landing genuinely in
ProbabilityMeasure/Kernel types) characterized by their defining ratio-of-integrals or
pushforward formulas, rather than constructed by normalizing a raw measure inline — proving
that normalization is a routine Fubini calculation the book itself does not spell out, and would
be proof content misplaced in a definition. Theorem 5.2.1's conditional-probability statement is
formalized via the book's own Equation (5.5) test-function identity rather than Mathlib's
conditional-expectation-with-respect-to-a-sub-σ-algebra machinery, since the two are equivalent by
the standard characterization of conditional expectation and the test-function form is what the
book's own proofs actually use. The Structure Assumption of Theorem 2.3.8 is restated locally
(existential value-function and decision-rule classes with its three defining clauses), per this
project's rule against importing another chunk's copy of shared machinery. Reusable beyond this
mission: the kernel-based expectation recursion (Ex/Vpi) is natural substrate for any later
mission needing a Markov Decision Process driven by a genuinely abstract stochastic kernel rather
than an i.i.d.-noise transition function. Contributions completing any milestone's sorry, or the
goal's, are welcome.
Many first-order methods in optimization are fixed-point iterations of a nonexpansive map : proximal gradient descent, projected gradient descent, alternating projections, ISTA and Douglas–Rachford splitting (with the conic solver SCS as an instance) all have this form (Zhang, O'Donoghue, Boyd 2020, §4.2). The averaged (Krasnosel'skiĭ–Mann) iteration converges to a fixed point whenever one exists, but it is often slow in its terminal phase. Anderson acceleration (AA) combines the last few iterates through a quasi-Newton update of an approximate Jacobian; it is used for electronic-structure computations and, in the stabilized form studied here, in the solver SCS 2.1. Its type-I variant (AA-I) is often faster in practice than the more studied type-II variant, but it can be numerically unstable, and no global convergence guarantee existed for it on nonsmooth problems.
Timeline (as recounted in the paper's related-work section):
Let satisfy for all (the Euclidean norm), and assume the solution set is nonempty. The residual is , , and the averaged operator is .
Powell's weight. For , if and otherwise, with .
Window matrices. For vectors and , let be their unnormalized Gram–Schmidt orthogonalization (3.2), , and
The matrix norm is the induced operator norm.
Algorithm 3.1 (AA-I-S-m). With parameters , and max-memory : start from , , , and . At iteration , set and , orthogonalize against the current window, and restart the window (memory back to , replaced by ) if the memory would exceed or . Then apply one Powell-regularized rank-one update to obtain and the trial point . The trial point is accepted if (and increases); otherwise .
The only hypotheses are nonexpansiveness of , and the parameter ranges. The limit is not specified: it depends on and the parameters.
The theorem places a quasi-Newton acceleration scheme under the same hypotheses as the plain averaged iteration: nonexpansiveness and existence of a fixed point. It therefore applies at once to the nonexpansive examples of §4.2 of the paper (proximal gradient, projected gradient, alternating projections, ISTA, Douglas–Rachford splitting and SCS), with no smoothness, strong convexity or local assumption. The matrix bounds of Lemma 3.3 and Corollaries 3.4–3.5 are also of independent use: they give explicit, iteration-independent control of the approximate inverse Jacobians of a limited-memory type-I method, an assumption that other globalization frameworks (for example SuperMann) have to impose.
The result is proved in the paper; to our knowledge none of it is machine-checked. Mathlib has neither the Krasnosel'skiĭ–Mann iteration, nor Fejér monotonicity, nor any Anderson-type method. A formalization provides these pieces, checks the index bookkeeping of the restart and safeguard steps, and makes explicit the one place where the printed algorithm and the analysis disagree (line 9 at a window start; see below).
The accelerated step need not decrease the distance to the solution set, so the Fejér argument for averaged iterations does not apply to it directly. The naive fix, bounding , requires a bound on that holds uniformly along the run; without the Powell regularization can be singular, and without the restart rule can grow without bound as the window becomes nearly linearly dependent. The determinant and norm bounds of Lemmas 3.2–3.3 have to be established for arbitrary windows and then connected to the run of the algorithm, where the window, its orthogonalization and the matrices are defined by an intertwined recursion with resets. The safeguard then turns the uniform bound into a summable perturbation of a Fejér-monotone sequence, and the final step needs an Opial-type argument to pass from convergence of distances to convergence of the iterates.
is EuclideanSpace ℝ (Fin n), so all vector norms are Euclidean; matrices are continuous linear maps with the operator norm; is rankOne ℝ u ŝ; is LinearMap.det; inverses are Ring.inverse (zero on singular maps, excluded by Lemma 3.2). The orthogonalization (3.2) is InnerProductSpace.gramSchmidt. Nonexpansive is LipschitzWith 1 f. The algorithm is the predicate IsAAISRun, a deterministic recursion: every run is determined by , the parameters and , and a sorry-free check that runs exist (for ) was built locally. The reset of in line 8 is local to its iteration. is encoded explicitly. Constants are the paper's explicit expressions; no milestone replaces them with an existential constant.
Line 9. The paper prints , derived from (3.3) through , which fails when the window starts afresh (). The mission uses (3.3) there: when , and the printed formula when .
Milestones of §4.1 and Corollary 3.5 carry the hypothesis for all , as the paper does ("we temporarily assume for simplicity that a solution to (1.1) is not found in finite steps"); the goal does not. A goal proved from an unsatisfiable run predicate, or one that assumes a bound on , contractivity of , or that the accelerated step is never taken, is not this theorem. Division by zero in Lean can only occur once a fixed point has been reached, after which all later iterates coincide.
Useful reusable infrastructure includes the Krasnosel'skiĭ–Mann inequality , quasi-Fejér monotone sequences and their convergence, and determinant and norm identities for rank-one updates (the matrix determinant lemma and Sherman–Morrison). Proofs of the window lemmas, of the run invariants (the window matrices coincide with the algorithm's ) and of the convergence steps are all welcome.
A manufacturer that makes several products must decide, before demand is known, how much capacity to buy. It can buy dedicated capacity, one resource per product, or a single flexible resource that can make every product. Flexible capacity pools demand: a surplus of one product's demand can be served by capacity that would otherwise sit idle. A common intuition in the operations literature holds that a flexible strategy is preferable to a dedicated one when the unit costs are equal, and much of that literature therefore assumes the flexible resource costs more (for example Van Mieghem 1998).
Tomlin and Wang (2005) examine when this intuition is valid for firms that are not risk neutral and whose resources may fail. Their answer has two halves. A risk-neutral firm always values flexibility, whatever the reliability of its resources (their Proposition 1). A firm with perfectly reliable resources also always values flexibility, whatever its attitude to risk, as long as it prefers more wealth to less (their Proposition 4). When neither condition holds, dedicated capacity can be strictly preferred (their Remark 1 and numerical study). This mission formalizes the second half.
There are products with a common contribution margin . The random demand vector is , nonnegative, with an arbitrary joint distribution on a probability space. The firm has initial wealth .
The firm chooses its investment to maximize one of three objectives of terminal wealth , with profit :
SF is (weakly) preferred when its optimal objective value is at least that of SD. The flexibility premium is , where the indifference cost is a flexible cost at which the firm is indifferent between the networks; the firm prefers SF as long as .
With perfectly reliable resources and any demand distribution, for every , for the loss-averse objective and for the CVaR objective. In the formalization: for every ,
for each expected utility with nondecreasing, and the loss-averse objective; for CVaR the same with the threshold quantified jointly with the investment.
Proposition 4 shows that the intuition "flexibility is worth at least as much as dedicated capacity at the same price" survives any monotone risk attitude and any demand distribution, provided supply is reliable. Combined with Proposition 1 it isolates the interaction of risk aversion and unreliable supply as the only source of a negative flexibility premium, which is the paper's Remark 1 and the organizing message of its numerical study. The result requires no concavity, differentiability or distributional assumption, so it applies to the loss-averse and CVaR objectives used throughout the paper.
The result is proved in the paper (Appendix A); no machine-checked version is known. A formalization produces a reusable statement of the model, a pathwise pooling inequality, and the passage from a pathwise comparison of two random variables on one probability space to comparisons of expected utilities and of CVaR, which recurs in capacity-pooling and inventory-pooling arguments.
The pathwise inequality is elementary. The work lies in the passage from it to the objectives. The paper cites Levy (1992) for both the expected-utility and the CVaR comparison; the first holds for every nondecreasing , including discontinuous ones, and the second concerns a maximum over a real threshold that is not a priori attained. A formal proof must also make sure every expectation involved is a genuine integral: the utility is arbitrary, so the expected utility is finite only because, for a fixed nonnegative investment and nonnegative demand, both wealths are confined to a bounded interval. Finally, "" is a statement about optimal values, and the optimal SD investment need not exist; the argument has to be run for every SD investment, not for an optimal one.
All declarations live in the namespace MixFlex.Reliable. The probability space is (Ω, μ) with IsProbabilityMeasure μ; demand is a measurable X : Ω → Fin N → ℝ with each coordinate almost surely nonnegative, and no density, independence or integrability is assumed. Expectations are Bochner integrals. Perfect reliability () is built into the wealths (A-4)–(A-5), so the committed-cost fraction does not appear. Standing parameters: , , , , arbitrary. The requirements and nonnegative, measurable demand are made explicit; the page treats them as part of the model.
The premium and the indifference cost are not defined as real numbers, since the indifference cost need not be unique. "" is encoded as "SF is weakly preferred for every ", and "weakly preferred" as "every nonnegative SD investment is matched or beaten by a nonnegative SF investment", with no real suprema. For CVaR the maximum in (8) over the investment and the threshold is encoded in the same matching form. The milestones compare the objectives at the flexible cost , as (A-5) is printed.
A formalization in which the expected utility of a non-integrable wealth defaults to zero, or in which makes the CVaR bracket , would make the comparisons meaningless; the statements exclude both ( with nonnegative demand bounds the wealths; ). "" is also not trivially true: for a flexible cost above SF can be strictly worse.
Out of scope: Propositions 1–3 and 5–8 (Proposition 1 is the companion mission on the risk-neutral premium), Remark 1's negative-premium claim and the numerical study. Welcome contributions: a general lemma that an almost-sure inequality between bounded random variables transfers to expected utilities of monotone functions, and a proof of the CVaR bracket comparison.
The traveling salesman problem (TSP) asks for a shortest closed route through a finite set of points. It is NP-hard, and in practice tours are built by fast constructive heuristics whose output is then improved or used as is. A central question in the analysis of algorithms, raised in this form by Rosenkrantz, Stearns and Lewis in 1977, is how far such a heuristic can be from optimal in the worst case, as a function of the number of points , when the distances satisfy the triangle inequality.
The paper (SIAM J. Comput. 6(3), 1977) answers this for several heuristics. For the general class of insertion methods it proves a logarithmic bound (Theorem 3); for two specific rules, nearest insertion and cheapest insertion, it proves a bound that does not grow with : the tour is less than twice the optimal (Theorem 4), and more precisely at most times the optimal (Corollary, eq. (4.12)). Theorem 5 of the same paper shows the constant is attained, so this is the exact worst case of both rules. These results, with Christofides' 3/2 bound of 1976, are the classical reference points for approximation ratios of TSP construction heuristics and appear in standard OR and approximation-algorithm texts.
A traveling salesman graph has a finite node set with and a distance that is symmetric, nonnegative and satisfies the triangle inequality . A tour is a circuit visiting every node exactly once; its length is the sum of its edge lengths, and OPTIMAL is the least tour length.
A subtour is a tour on a subset of (a one-node subtour has no edges). For , inserts into where it is cheapest: if has at least two nodes, choose an edge of minimizing and replace it by ; if , form the two-node tour on . is the length of minus the length of .
An insertion method builds subtours with and for some , ; INSERT is the length of . With :
The start node and every tie (between candidate nodes, and between candidate edges) are arbitrary. TREE denotes the length of a minimal spanning tree of .
For every traveling salesman graph on nodes and every run of nearest insertion or of cheapest insertion,
Theorem 4 itself, when is not identically zero, is included as a companion statement.
The bound says that two simple and construction rules are never worse than a factor from optimal on any metric instance, a guarantee independent of , in contrast with nearest neighbor and with arbitrary insertion orders, whose ratios the same paper shows can grow logarithmically. Lemma 3 is reusable on its own: any insertion rule satisfying the local inequality (4.5) inherits the bound , and the paper notes that similar arguments apply to nearest addition and nearest merger.
The result has been proved since 1977. The Prove2Me library has a machine-checked proof of the weaker statement for nearest insertion only with constant (SupplyChainTheory.nearest_insertion_bound, from Snyder–Shen, Theorem 10.7) and of (SupplyChainTheory.mst_lower_bound). This mission asks for the paper's full statement: both rules, the exact constant , and the general Lemma 3 via its correspondence between insertion steps and spanning-tree edges. Paired with the tightness result of the companion mission (Theorem 5), it would give a formally verified exact worst-case ratio for both heuristics.
Lemma 2 and inequality (4.5) are local consequences of the triangle inequality; the difficulty is global. The obvious attempt at Lemma 3 charges step to the tree edge joining to its nearest node of , but distinct steps can then be charged to the same tree edge, and the sum of the charges no longer bounds . Any correct argument must control how the insertion order interacts with the structure of an arbitrary spanning tree, which in Lean means reasoning about paths in SimpleGraph together with the evolving subtours. For cheapest insertion the chosen node need not be a nearest node, so (4.5) is not immediate from the rule. Finally, the goal's constant is sharper than the bound obtained from , so the weaker spanning-tree bound already in the library does not suffice.
Nodes are Fin n with (the paper's nodes shifted to ). The distance satisfies the paper's three axioms plus the normalization , which never affects a tour, subtour or tree length. Tours are permutations; OPTIMAL is a minimum over all of them (Finset.inf'). Subtours are lists of distinct nodes with closed length. is encoded as insertion of at a list position whose resulting length is minimal over all positions, which is the minimization of (3.1) over the edges of ; COST is the corresponding minimum increase. The subtour index is 1-based as printed (, final). The distance is taken in , so no default value enters the nearest rule. Spanning trees are SimpleGraph (Fin n) with IsTree; statements about TREE are phrased over every spanning tree (upper bounds) or some spanning tree (bounds on TREE), which is equivalent. Ratios are multiplied out, so the goal needs no nontriviality hypothesis; Theorem 4's strict form carries the paper's exclusion of the identically zero distance (p. 564).
A formalization in which TOUR inserts at an arbitrary rather than a cheapest position, or in which the run fixes the start node or the tie-breaking, would state a different (and, for arbitrary positions, false) theorem; the statements here quantify over every run.
A complete development needs subtour-length lemmas for List.insertIdx, the telescoping identity (3.7), and a spanning-tree edge-assignment argument on Mathlib's SimpleGraph paths; the last two are reusable for other insertion rules and for the companion missions of this series. Proofs of any milestone are welcome independently.