Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).
Two firms, a retailer and a supplier , each use a base stock policy: firm keeps its inventory position equal to its base stock level . A negative supplier base stock means planned backorders. Let and be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means , , and their distribution functions , are continuous, zero at , strictly increasing on and differentiable on . Holding costs are and , with . Each backorder at the retailer costs the retailer and the supplier per unit time. Write .
At retailer inventory level the expected on-hand stock is and the expected backorders are . The retail-level cost rates are , and . Because the supplier may stock out, the retailer's actual inventory level is , and every retail-level quantity is averaged accordingly:
With the supplier's inventory and backorders , the firms' costs and the chain's cost are
A pair minimizing is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.
Under a linear transfer the supplier pays the retailer (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter are
If is optimal with and , then under the contracts
is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every in the range.
The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter splits the retail-level costs between the firms in any proportion up to . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers and are those of the single-location model (§6.7), even though the retailer's target fractile changes from to .
The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.
The firms' costs are compositions: a convex single-location cost evaluated at the random level , which is concave in . The supplier's cost is therefore not obviously convex in ; its convexity at depends on the value of and on . Uniqueness is the hard part. Under the contracts the retailer's best response decreases, but the supplier's marginal cost along that best response, , is not monotone in general when is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.
Demand laws are probability measures on with no mass below , finite means, and continuous distribution functions, zero at , strictly increasing on and differentiable on . These are the section's standing assumptions, together with and (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: , , and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against are written against the law of , so no density hypothesis is made. Base stocks range over all of , and "optimal" means minimizing over ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of and , implicit on the page, enters only through the convolution of their laws in (38).
The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.
Corrected slips: (42) is stated with where the page prints (the difference does not depend on ). The retailer's single-location fractile on p. 79 is stated as , not the printed . The garbled display after (43) and the / slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.
In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.
The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor . When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio .
Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on . Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio , but not by a polynomial algorithm for varying ; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.
Work in with the Euclidean length , and write for the closed ball. For points , the simplex volume is
where has column vectors .
Let be convex, and let with linearly independent. Choose linear functions with
Thus measures the height above the facet opposite . The stopping condition of the second stage is
The ratio is the factor by which the volume changes when is replaced by , so (16) says that no such swap enlarges the simplex by more than .
Let be a nonsingular linear map of such that span a regular simplex, meaning that all distances , , are equal. Let be its centroid and its convex hull. For , the paper defines
The proof of the LEMMA works in model coordinates. There is the hyperplane of , the are the standard basis vectors, , and .
Under (15) and (16), with making the simplex regular and its centroid, there are positive reals with
These are conditions (3)–(4) of §1 with .
The paper's own proof derives the goal from milestone 1 and the LEMMA at . At the constant cannot be improved by this argument.
The result. The theorem is the only place in the paper where the roundness constant is computed, and enters the bound on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of to obtain ( even) and ( odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume- neighbourhood" of a regular simplex extends.
The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor , by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.
There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map . The second is the transfer to the model. The paper's "similarity transformation" identifies with a hyperplane of and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and must all be carried across this isometry up to scaling. The LEMMA is stated in , not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.
EuclideanSpace ℝ (Fin n) and the model is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching .A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.
This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.
Fix . Industry demand is low or high, each with probability . If the retailers hold a total stock , the market clearing price is
Leftover inventory has no salvage value, and the supplier's production cost is zero.
Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the with and on . The supplier earns .
The page's notation , , and is kept in Lean under the names q1, q2, supplierProfit, wStar.
With
the goal states four things:
The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever . It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at . Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.
The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.
Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.
All quantities are real numbers and throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor ) are written into the contract definitions, as the page describes them in words. The theorems use only .
The formulas , , and are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside . Uniqueness of is not asserted at .
The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.
A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.
The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.
One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity and an effort level . Effort costs him , where , and . Demand given effort has distribution function on , with and strictly increasing. Demand is stochastically increasing in effort: for . Units sell at the retail price and cost to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are
Let maximize . A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back , quantity flexibility , revenue sharing , the sales rebate and the quantity discount . Under each, the retailer's profit is his revenue less the transfer and .
The goal combines the section's negative and positive results.
the following hold for every . The retailer earns and the supplier earns . The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If maximizes , both firms' profits at effort are maximized by .
The milestones follow the section's own claims: the integral form of (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility () and revenue sharing (), and the reverse inequality for the sales rebate (, ); the two displays of under the quantity discount; and the fact that decreases in .
The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because with free in , any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).
The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.
Most of the algebra is short. The substance is in the derivatives. is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs to be integrable and negative on a set of positive length, which is why (and for the sales rebate) matters.
The natural reading "the quantity discount makes the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed the retailer's effort incentive is the chain's, and at his best order is . Since , the retailer can gain by moving and together when is small. The goal states exactly the two partial claims.
The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: and with ; a family of demand laws indexed by effort (probability measures on with finite mean, no atom at , strictly increasing distribution function); the effort derivative , negative for , ; and with and positive first and second derivatives for . is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts . The inequalities assert that both derivatives exist.
The following hypotheses are standing assumptions or disclosed additions:
Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less .
The page prints the last term of as . With that sign the page's own displays and fail by . The formalization uses , under which both hold. is the explicit printed schedule with this correction. It is not defined as "a schedule with ", which would make the goal empty.
Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue ) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.
Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.
D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.
Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.
Fix , a vector , a symmetric positive definite matrix , an matrix with columns , and . The quadratic program (1.1) is
The gradient is . For , the subproblem keeps only the constraints indexed by ; is solved by . A set is linearly independent if the normals , , are.
For an independent , let be the matrix with columns , , and define
The multipliers are ; for a constraint with normal the infeasibility multipliers are ; a superscript denotes the same objects for .
An S-pair is an independent active set with for and optimal for . A V-triple has , independent, , for , and .
The dual algorithm starts from . In Step 1 it stops if is feasible; otherwise it picks any violated constraint . In Step 2 it moves along the primal direction and the dual direction with step , where is the largest step that keeps the multipliers nonnegative and makes constraint active. If both are infinite it reports infeasibility. A full step () adds and returns to Step 1. A partial step (), or a dual step (), drops a constraint attaining and repeats Step 2.
For every choice of the violated constraint and of the dropped constraint :
Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for and , a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.
The obvious termination argument is that increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave unchanged (the dual steps of Step 2(c)(ii)), so is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move . Any such argument relies on invariants (independence of , nonnegativity of the multipliers, along partial steps) that hold only on reachable states, and the operators and are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.
Vectors are Fin n → ℝ, is Matrix (Fin n) (Fin n) ℝ with G.PosDef, is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in . Lean's matrix inverse returns for singular matrices, so every statement about and assumes and an independent active set (directly, or through an S-pair or V-triple).
The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of and . Infinite step lengths are separate transitions; a tie takes the full step, as the paper tests first. The running value of and the factorizations of Section 4 are not part of the state.
Explicit readings of the paper's words:
Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);Property (2.10), printed , is false unless and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.
A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.
Needed infrastructure: Schur-complement and projector identities for and ; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about and , are welcome.
Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.
The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.
A circulation network has a finite vertex set and a symmetric set of directed arcs: whenever is an arc, so is . Let and , counting both orientations. Each arc has a real capacity and cost , with . A pseudoflow respects capacities and the paired-arc relation . Its excess is the sum of flow entering . A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity . An arc is residual when this capacity is positive.
A price function changes an arc's reduced cost to . A pseudoflow is -optimal with respect to when every residual arc has reduced cost at least . A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is -optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by -optimality. These rules are Figures 4 and 5, printed pages 18–19.
The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a -optimal circulation, Lemma 5.8 bounds each vertex's price increase by . Lemmas 5.9–5.11 bound the numbers of relabelings, saturating pushes, and nonsaturating pushes:
The goal combines the resulting bound on the number of updates with progress and correctness:
If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is -optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.
The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.
This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.
A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being -optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.
Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new is positive, so the entry circulation is -optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index . Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.
The reduced-cost sign is , and relabel raises . This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's , , , and ; the goal sums the last three. The report's RAM-model running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.
A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.
Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.
Timeline:
The products form a finite set . A system of choice probabilities gives, for every offer set and product , the probability that a customer buys . The no-purchase probability is . The model is regular if
Each product has a revenue . Offering earns , and .
Let be the distinct revenues, with , and . The heuristic earns
For an optimal let , , and the largest index with . Section 3 of the paper proves
For every and every there are a finite nonempty product set, a regular , revenues with exactly distinct values, and an optimal with , such that
So none of the bounds (A), (B), (C) stays true when multiplied by , for any number of distinct revenues.
The paper's witness has products with and . Product has revenue , and when and , and otherwise, for . The milestones follow the proof on pp. 10–11:
With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters , and , revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.
On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.
The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:
The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly revenues on which all three bounds are nearly attained, for every .
C. The no-purchase option is not a product: is the derived quantity noPurchase P S. Offer sets are Finset C.IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at is essential: without it the guarantees fail.Finset.sup' over all subsets, including . is Finset.sup' over the threshold sets only, and needs Nonempty C.r, indexed by Fin k from : the Lean index is the paper's , and is a separate case. lives in WithBot (Fin k).𝓝[>] 0.Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.Ruled out:
Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of , and general lemmas on sorted distinct values of a finite function.
A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).
The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).
Let be a finite nonempty set of products. A system of choice probabilities gives, for every offer set and product , the probability that a customer offered buys . Buying nothing is the option , with . The model is regular when
Axiom 4 at says that enlarging the offer set never makes buying nothing more likely.
Prices are a function . Offering earns , and . Let be the distinct values of , and let for . The revenue-ordered strategy earns
For an assortment , the purchase profile is
the probability that a customer offered buys something priced at least . It is non-increasing in .
Let be optimal, , suppose , and let be maximum with . Then
The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form .
Theorem 3.3 gives a guarantee that is independent of prices. The bound of Theorem 3.2 grows when prices are spread out. The bound is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.
The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.
Each step is elementary. The difficulty is bookkeeping. The revenue of has to be regrouped by distinct price levels rather than by products: several products may share a price, and counts values. The regrouping uses an Abel-type rearrangement with the boundary convention . Comparing with the purchase probability of needs regularity twice. First, axiom 4 for products passes from to . Then the no-purchase case passes from to . A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.
C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's . Offer sets are Finset C, and is P : C → Finset C → ℝ. The no-purchase option is not a product: is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.Finset.sup' over all subsets. is Finset.sup' over the indices of the threshold sets only.level r i is for . purchaseProfile P r S i is for and otherwise, which builds in .Real.log, applied to .The following statements are trivial or false and are not this mission: a maximum over all subsets in place of ; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular .
A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that is non-increasing.
Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?
Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.
A finite MDP consists of finite sets of states and of actions ( nonempty), a transition kernel , rewards and a discount factor . A policy assigns to each state a probability vector on . Its value is the expected discounted sum of rewards when actions are drawn from ; its state–action value is and its advantage is . For a distribution on states, , and the discounted state visitation distribution is . A policy is optimal if for every policy and every state ; .
The softmax policy with parameters is
Softmax policy gradient ascent with step size produces, from an arbitrary , the iterates
The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ , and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.
If for every state and , then for every state
The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.
The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to at every state, not only on average under . It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether can be dropped.
The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.
The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from , but under softmax , so a vanishing -gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.
Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in , ); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are and Mathlib's gradient is ; the coordinate of the gradient is . Logarithms do not appear. Conventions committed to:
PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.Tendsto … atTop atTop / atBot; "strictly increasing for " is StrictMonoOn on Set.Ici T1, with existentially quantified.The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets ; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.
A full development needs: differentiability of and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for -smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.
Consensus asks processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, fail-stop faults can be tolerated for any . With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).
Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound , but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates faults once .
Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.
There are processors . Each processor holds an initial value . Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either , which puts message in 's buffer, or , which removes a set of messages from 's buffer and delivers it. The next state depends on the current state and, for a Receive, on . A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.
Real time is the ticks . A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.
A protocol is a -resilient consensus protocol achieving weak unanimity if the following holds for every set of at least processors and every allowed run in which the processors of are correct and the others fail-stop. No two processors of decide differently (consistency). Every processor of decides (termination). If all initial values are and no processor is faulty, every decision is (weak unanimity).
For integers with
there is no -resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive when holds eventually, and when delta is unknown.
Split the processors into groups and with .
The result. Theorem 4.3 shows that the resiliency of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.
The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.
The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.
First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past . With delta unknown, this needs a larger than that delay. When holds eventually, is fixed before the protocol, and the protocol fixes and . So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after . Read literally, "every message between the groups takes more than steps" is not an allowed run in this model.
Second, "the processors of act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to . With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.
All declarations live in the namespace DLSConsensus.LowerBound. Processor is the index of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick . A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.
Explicit readings and conventions:
Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.
Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension and the number of facets is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in , with a constant exponential in (Larman 1970).
Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."
The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.
Let and write for the family of its -element subsets. A graph in the base abstraction has a nonempty vertex set : every vertex is a -element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each there exists a path connecting and whose intermediate vertices all contain . Condition i) makes connected. The class of all such graphs is ; is called the dimension and the number of facets of the abstraction, and denotes the largest diameter of a graph in (p. 2).
The distance is the least number of edges of a path from to . The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly facets), each vertex labelled by its facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class is not restricted to such graphs.
The abstract prints the bound as and states that it continues to hold in the base abstraction. The target is the pointwise form of :
In Lean this is the existence, for every pair , of a walk from to with at most edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.
For fixed the bound is linear in , and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in for fixed dimension, but not a linear bound uniform in and . Since the graph of every non-degenerate polyhedron lies in (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant .
Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant for nonempty bounded -polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an -polytope, and are credited as prior work; none states the bound for every graph of . The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.
The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on -subsets of gives only the trivial bound , which is far from linear in . A linear bound in has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.
Fin n, labels ; only the number of labels matters.V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality , and CondI V G.CondI asks for a walk all of whose vertices contain . This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain automatically.Hirsch.larman_bound is not claimed here.Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).
This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.
Let , and let be the family of its -element subsets. A graph in the paper's base abstraction has a nonempty vertex set . Thus each graph vertex is labelled by a distinct -element subset. The edges can be chosen freely subject to condition i): for every pair , there is a path from to u\cap v\mathcal B_{d,n}dn$ the number of facets of the abstraction (definition and footnote, p. 2).
The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and is the largest diameter among graphs in . Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly facets, its tight facets provide a -element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict to a realizable polyhedron graph.
For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:
Equivalently, every pair has a connecting path with at most edges. Consequently . The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for , its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).
The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once and are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in (p. 3).
A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded -polytope, with a different exponent , and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all .
The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of -sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).
Lean represents by Fin n, with labels instead of ; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires to be nonempty, every label to have cardinality , and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain . Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.
The theorem takes , so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to for comparison with . No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining through a supremum with an artificial value for an empty class. At with , InB has no instance, as there are no -element labels; at , the bound is , consistent with a connected graph on at most labels.
The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.
Consensus asks processors, each starting with a value, to agree on one value although some of them may be faulty. It underlies replicated databases, atomic commitment and state-machine replication. Two classical models bracket the problem. In a fully synchronous system, with known bounds on message delay and processor speed, consensus is solvable for many fault types. In a fully asynchronous system, Fischer, Lynch and Paterson showed in 1985 that no deterministic protocol tolerates even one fail-stop fault (FLP, J. ACM 1985).
Dwork, Lynch and Stockmeyer (J. ACM 35(2), 1988, 288–323) introduced partial synchrony between these extremes: message delays are bounded, but either the bound is unknown, or it holds only from an unknown global stabilization time (GST) on. This model, and the GST abstraction in particular, became the standard assumption under which practical consensus protocols (Paxos-style and Byzantine fault-tolerant replication) are proved live. The paper determines, for each fault type, the largest number of faults that consensus can tolerate under partial synchrony. This mission formalizes its first positive result: for fail-stop and omission faults, processors suffice.
There are processors , an integer , and an arbitrary set of values; processor starts with .
In the basic round model (Section 3.1 of the paper), computation proceeds in rounds . In each round every processor sends messages, each message is either delivered in that round or lost, and every processor then performs a state transition on the messages it received. Losses are described by a predicate . A set of processors (the correct ones) and a round constrain it: every message sent at a round from a processor of to a processor of is delivered. Before GST any message may be lost, and messages from or to processors outside may be lost at any time. Processors outside follow the protocol but lose sends and receptions (omission faults, which include fail-stop faults).
Algorithm 1 (Section 3.2.1) works as follows. Every processor keeps a set , initially , attaches it to every message, and merges in every PROPER set it receives. A processor may hold locks, each a value with an associated phase number; is acceptable to if has no lock on a value other than . Phase belongs to when . Trying phase occupies rounds , , :
Lock-release phase is round : every processor broadcasts its locks , and a lock on with phase is released on receipt of some with and .
The correctness conditions (Section 2.4) for the set are consistency (no two decisions of processors in differ), termination (every processor in decides), and strong unanimity (if all initial values equal , every decision in is ).
For all with , every value type , all initial values, every with , every , every delivery pattern allowed for and , and every admissible choice of proposals,
This is the theorem as printed; it fixes no constants.
Theorem 3.1 shows that, against omission and fail-stop faults, partially synchronous communication costs nothing in resilience compared with a majority bound: suffices, and Section 4 of the paper shows that does not. The lock-and-release structure of Algorithm 1 (a value is decided only after a quorum locks it, and locks are released only on evidence of a later competing lock) recurs in later partially synchronous protocols, where safety must hold regardless of timing and liveness is obtained only after stabilization. The result separates the two concerns cleanly: consistency and strong unanimity hold in every run, while termination uses GST.
The result is proved in the paper; to the best of the available information it has not been formalized in Lean, and no distributed-computing model exists on Prove2Me. The mission produces a machine-checked model of the basic round model with a GST delivery guarantee, a full executable specification of Algorithm 1, and proofs of its safety and liveness. The paper's own proof of Lemma 3.3 is one line and the termination argument relies on "sufficient communication"; a formal proof must make these steps explicit.
The safety argument is an invariant over an unbounded number of phases with an arbitrary loss pattern: a lock on the decided value must be shown never to be released without being replaced by a higher lock on the same value, while competing locks on other values may exist at faulty or slow processors. The obvious argument ("after a decision, every later proposal must equal the decided value") is circular without a persistence statement for locks such as Lemma 3.2. Liveness requires reasoning about what every correct processor knows after GST (its PROPER set and the locks of the others), and it depends on processors sending lock-release and list messages even when these carry no locks or no acceptable values. Quorum counting with and must be carried out over distinct senders.
Fin N; the paper's is the processor of index . Rounds start at ; exec … 0 is the initial state and exec … r the state after round . Phases start at .pick : ℕ → Set V → V, required only to pick an element of every nonempty candidate set, and universally quantified in every theorem.DecidesAt p k v (owner of phase , proposed , at least acknowledgements in round ); consistency requires all such events of processors in to agree.A formalization in which a run cannot exist, the delivery constraint is unsatisfiable, the choice of proposals is fixed, or faulty processors are absent ( = all processors) would trivialize the theorem; the model here admits runs in which processors decide, and ranges over all sets of at least processors.
Reusable beyond this mission: the round-based message-passing model with a GST delivery guarantee and omission faults. Contributions of general lemmas about runs (monotonicity of PROPER sets, persistence of locks, quorum intersection over Finset) are welcome.
Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)
The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses -configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4
Fix a finite index set , positive rational coefficients for , and a rational right-hand side . A zero–one solution is a vector with each satisfying the single row
The model uses the support set for such a vector. A set is a minimal cover when its total coefficient exceeds , but removing any one member makes the total at most :
It yields the cover inequality for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when is empty.
A -configuration consists of , and an integer . The set itself fits the row, while is a minimal cover for every -element subset of . For any and -element , its inequality is . Crowder, Johnson and Padberg (1983), pp. 810–811
For a point , the separation problem asks for a cover minimizing , subject to the strict condition . This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value is therefore asserted only when a least attainable value exists.
The goal is the paper's Section 2.3 equivalence:
where is the attained optimum of (2.12). A cover inequality cuts off precisely when its left-hand side exceeds . If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813
The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, is the maximum integer objective value in (2.10), is the maximum in its linear relaxation, and . The claims are and validity after adding variable with coefficient . They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814
The equivalence turns a geometric question about which cover inequality excludes into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4
The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.
Checking all subsets of directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when . The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814
Lean uses an arbitrary finite index type for , replacing the paper's indices . A zero–one vector is a finite support set. Row coefficients and are rational, as on p. 810; the point and separation values are real. The target asks only that lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on .
The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions and are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.
Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set . After adding , it ranges over support in . The final inequality covers the whole row when that set is . The development must preserve the full quantifier over every -subset in (2.8) and every and in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.
Many feasibility problems ask for a point satisfying several constraints at once. When each constraint set admits a manageable Euclidean projection, a parallel method can project onto all sets independently and combine the results. Chapter 5 of Boyd, Parikh, Chu, Peleato and Eckstein (2011) places this construction inside the alternating direction method of multipliers (ADMM). That connection matters when a single projection onto the intersection is difficult but projections onto its individual factors are available.
The chapter first rewrites constrained convex optimization as a split problem. It then treats feasibility for two sets and finally an arbitrary finite collection of sets. For the latter, the product of the sets captures the separate constraints, while a consensus set forces all copies of the variable to agree. These are ordinary finite dimensional convex sets, so the account applies to geometric feasibility and to constrained optimization subproblems in which projection is the computational primitive. The mission isolates the identities that let the product-space algorithm run through parallel individual projections and one average.
A Euclidean projection of a vector onto a set is a point closest to in Euclidean distance. Each set , for , is assumed nonempty, closed and convex, and . These properties give a unique projection for every input. They do not require the common intersection to be nonempty: the iteration and the algebraic identities still make sense when the feasibility problem has no solution.
A block vector belongs to the product set exactly when for all . The consensus set consists of constant block vectors . The block average is . Distances in the stacked space use the ordinary Euclidean metric, whose square is . A block vector need not carry a function-space norm in the formalization for this metric to be stated precisely.
Starting with arbitrary and , the parallel projection ADMM run has three updates: each is the projection of onto ; is the average of ; and . The are scaled dual variables, formed using a penalty parameter . The source presents these equations as the specialization of scaled ADMM for the indicator functions of and §5.1.2, pp. 35–36.
The first targets identify the projections that make the iteration parallel:
The goal is the full reduction of a run. Its dual average is zero after every update, and its common vector equals the primal average from the following update onward:
Consequently, for every and every , the same iterates obey the simpler two-line algorithm
If , those last identities hold already for . The index qualification is necessary because is arbitrary, and still contains the initial dual average unless that average was zero. This is the precise reading of the source's “after the first step” statement §5.1.2, p. 36. The milestone list also records the indicator-function projection update on p. 33 and the averaged identities on p. 36.
The result identifies what information must pass between the parallel projection steps: each local step needs the shared average and its own dual displacement. It also fixes the relationship between the displayed three-variable ADMM iteration and the shorter project-and-average rule. Without the dual-average identity, replacing by is not justified at the initial indices. The product and consensus projection identities explain why the update can be decomposed into independent local projections followed by a mean §5.1.2, p. 35.
The chapter's identities are known mathematical results; this mission asks for machine-checked proofs of their stated finite dimensional version. A completed development supplies reusable statements about nearest-point projection onto products and diagonal sets, and a precise run predicate for later analysis of parallel ADMM. The goal is a statement about every valid run rather than a claim of convergence or existence of a feasible common point. Neither convergence nor feasibility of the intersection is concluded on these pages. Those distinctions keep the mission aligned with the actual scope of Chapter 5.
The product projection uses a sum of squared component distances. Treating a block vector as an arbitrary function and applying its default norm would change the metric, so a projection theorem stated that way would describe a different algorithm. The consensus projection likewise depends on the Euclidean sum and the finite average, including the condition . The run reduction has a separate indexing difficulty: the vanishing average follows after one dual update, but the first simplified projection step can occur later because it uses the previous common vector. An argument that silently assumes would erase the arbitrary initialization on the source page.
Lean represents each as EuclideanSpace ℝ (Fin n) and the blocks as a function on Fin N; the latter is the source's -based indexing shifted to -based indices. Squared stacked distance is defined as the sum of squared component norms. The average uses the real factor only under . Individual projections reuse the published nearest-point relation RandomGradFree.Nonsmooth.IsMetricProjection. A run records the three updates as conditions on sequences, with arbitrary and unused . The source's scaled dual variable appears directly; cancels from these projection updates once it is positive.
The source assumes closed convex sets; nonemptiness is stated explicitly here because a projection onto an empty set does not exist. The book prints in its averaged dual update on p. 36, while its defining update on p. 35 and the next line on p. 36 require . The formal statement uses the corrected index. The book also calls the individual sets in its closing sentence; the sets defined for this subsection are . The milestone quote preserves the printed intermediate index. The goal includes the simplified primal and dual updates, since asserting only that the dual average vanishes would omit the chapter's advertised reduction.
The development needs finite sums in Euclidean spaces, convex-set projection, and elementary properties of product and diagonal sets. Product and consensus projection results are useful beyond ADMM. Contributions proving the four milestones, the full run theorem, or equivalent projection lemmas at the same generality are within scope.
In distributionally robust modelling, a baseline probability model on a space is distrusted, and the analyst reports the largest expected loss over every model within a budget of . Blanchet and Murthy (arXiv:1604.01446; Math. Oper. Res. 44(2), 2019, doi:10.1287/moor.2018.0936) measure the budget with an optimal transport cost and prove strong duality for the resulting worst-case expectation on an arbitrary Polish space, with a lower semicontinuous cost and an upper semicontinuous performance function. Duality computes the worst-case value. A risk manager also wants the worst-case model: a distribution that attains the value, whose structure explains which perturbation of is most harmful.
Such a model need not exist. Unlike the Kantorovich problem, where the set of couplings with two fixed marginals is weakly compact, the feasible set here fixes only one marginal and is not compact in general. Section 5 of the paper gives an example on where the supremum is not attained, then gives abstract conditions under which it is (Proposition 9), and growth conditions on a locally compact normed space that imply them (Corollary 1). Related existence results in were obtained by Gao and Kleywegt (arXiv:1604.02199, 2016) and, for empirical baselines and norm costs, by Mohajerin Esfahani and Kuhn (arXiv:1505.05116, 2018).
Let be a Polish space with its Borel -algebra, a probability measure on , a budget, a cost and a performance function. The standing assumptions are:
The primal feasible set consists of the probability measures on with first marginal and (transport plans out of of cost at most ). The primal objective is and the primal value is . The dual feasible set consists of pairs with , universally measurable and for all . The dual objective is and the dual value is . For put .
Section 5 assumes throughout that is a dual optimal pair with . Write for the plans in concentrated on .
(P-Compactness): for every there are a compact with and such that has compact closure. (P-USC): whenever converge weakly to .
On a normed space : (A3) for , with nondecreasing and . (A4) for an increasing with ; and for every , once .
Let be a real normed space that is locally compact, and let satisfy (A1)–(A4). Under the standing assumption, if there is with
The result. An attained worst case turns duality into a structural statement. By Theorem 1(b) of the paper, an optimizer moves mass from only to maximizers of and, when , uses the full budget. When those maximizers are unique (Remark 8: convex in , concave) the worst-case model is unique and is the image of under a transport map. That map is what stress tests and robust estimators are built from. Without existence, these statements describe an object that may not be there.
Formalizing it. The paper's proofs are complete; nothing here is open. No machine-checked version of this result is known: the worst-case optimal transport literature, including the strong duality of this paper, is unformalized. The mission produces the transport objects of §2 in a form that keeps the paper's generality (Polish space, lower semicontinuous real cost, universally measurable dual variables, the convention), a tightness argument for nearly optimal one-marginal plans, and an upper semicontinuity argument for unbounded upper semicontinuous integrands under uniform integrability.
The obvious argument takes a maximizing sequence and extracts a weak limit. Both steps fail without more structure. First, is not tight: only the first marginal is fixed, and a sequence may push mass to infinity at bounded cost. That is exactly what happens in Example 2 (p. 26), where and the value is approached but never reached. Tightness has to come from the dual: nearly optimal plans concentrate near maximizers of , and (A3)–(A4) with confine those maximizers. Second, is only upper semicontinuous and unbounded, so weak convergence alone does not give . A uniform integrability bound is needed, and it uses the restriction to in an essential way. A third, Lean-specific difficulty is measure-theoretic: is only universally measurable, and the gaps of Remark 4 are integrals against completions.
All declarations sit in the namespace ModelRiskOT.PrimalOpt. Values of , , , and are in EReal. is with lower integrals, and Mathlib's realises the paper's reading of the supremum (footnote 2, p. 5). Integrals of nonnegative or extended-real functions are lower integrals (lintegral), never Bochner integrals. Universal measurability is the published BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable. Weak convergence is the topology of ProbabilityMeasure (S × S). Measures on use the product -algebra.
The following readings are fixed:
EReal convention.LocallyCompactSpace. It also carries PolishSpace, which is redundant, since a locally compact real normed space is finite-dimensional.The goal cannot be satisfied by a junk value: and are EReal suprema and infima, not real sSup, and the hypothesis is kept because Example 2 shows the conclusion fails without it. A sorry-free check that , on satisfy (A1), (A3) and (A4) accompanies the drafts.
A complete development needs Prokhorov's theorem (in Mathlib), a Fatou lemma for weakly converging measures with a lower semicontinuous integrand, an upper semicontinuity theorem for uniformly integrable upper semicontinuous integrands, and the change of variables for universally measurable . The last three are reusable well beyond this mission. Proofs of any milestone, and these general lemmas as separate contributions, are welcome.
A probability model for a risk quantity, such as the reserve process of an insurer or the path of a queue, is usually chosen for tractability or fitted to limited data, and the true law of the system is unknown. Distributional model risk asks how large a probability of interest could be if the true law were any model "close" to . When closeness is measured by an optimal transport cost rather than a likelihood ratio, the competing models may put mass where puts none, which is the situation for rare events such as ruin or buffer overflow: the event of interest often lies outside the support of the baseline.
Blanchet and Murthy (arXiv:1604.01446, Mathematics of Operations Research 44(2), 2019) prove strong duality for worst-case expectations over an optimal-transport ball on a general Polish space, with a lower semicontinuous cost. Their §2.4 specializes the duality to worst-case probabilities of a closed set and obtains a closed-form answer: the worst-case probability of is the baseline probability of an inflated version of . This mission formalizes that result, Theorem 3 of the paper, together with the numbered statements its proof uses.
Let be a Polish space with its Borel -algebra, its probability measures, and the baseline. A cost satisfies Assumption (A1): it is nonnegative, lower semicontinuous, and if and only if .
For , a coupling of and is a probability measure on with marginals and ; is the set of couplings, and the optimal transport cost is
For a budget , the primal feasible set consists of the probability measures on with first marginal and .
Fix a nonempty closed set and let be the cheapest cost of moving unit mass from into . The worst-case probability is
Its dual is the univariate problem
and for a minimizer of (13) the paper defines
If attains the infimum in (13) and , then
Theorem 3 converts a supremum over an infinite-dimensional ball of probability measures into a single probability under the baseline: of the set of points that can reach at cost at most , where is determined by through the one-dimensional function . For the cost of a metric this is the baseline probability of the -neighbourhood of . The paper uses it to compute worst-case ruin probabilities for the Cramér–Lundberg model around a Brownian approximation (§3, §6.1), where is a path space; the result applies there because nothing in it uses local compactness of .
The result is proved in the paper. As far as the platform's corpus shows, neither it nor the strong duality behind it has been formalized. A formal development produces, beyond Theorem 3: a reusable definition of optimal transport costs with lower semicontinuous costs on Polish spaces; the coupling reformulation of the transport ball, which rests on the existence of optimal transport plans (Villani, Optimal Transport, Theorem 4.1), not in Mathlib; and an -optimal-plan argument that avoids assuming a primal optimizer exists.
The heuristic derivation on pp. 9–10 constructs an optimal transport plan that moves each with to a nearest point of and leaves the others in place. It needs a nearest point to exist and to be selectable measurably, which fails for general closed in a non-locally-compact space, and it needs a primal optimizer, which need not exist. Theorem 3 assumes neither, so the construction is not a proof. A second point is the boundary level : when charges it, as for atomic baselines, the identity (15) can fail (for a point mass at distance from and , the worst case is , not ), and the hypothesis is exactly what excludes this. Measurability is a second obstacle: is an infimum of a lower semicontinuous function over and in general only universally measurable, so integrals of it are taken against the completion of .
All objects live in the namespace ModelRiskOT.WorstProb. carries [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]; is a Measure S with IsProbabilityMeasure; the cost is a real-valued c : S → S → ℝ with (A1) bundled as a structure (nonnegativity, lower semicontinuity on , and ). Committed conventions:
ℝ≥0∞; integrals are lower Lebesgue integrals and the positive part is ENNReal.ofReal. For the universally measurable functions and sets that occur, lower integrals and outer measures agree with the completion of , which is the paper's reading (p. 4). No Bochner integral is used.A formalization in which the transport ball fixes only the first marginal would contain every probability measure and give for every nonempty ; the definitions here fix both marginals of the couplings in , and the hypothesis is kept as stated rather than replaced by continuity of .
A complete development needs the existence of optimal couplings for lower semicontinuous costs (tightness and Prokhorov's theorem, available in Mathlib), the strong duality of the paper's Theorem 1 specialized to indicators (milestone 3; a separate mission in this series formalizes Theorem 1 in general), and universal measurability of through projections of Borel sets. The transport-cost definitions and the coupling reformulation are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs that derive (13) from the general strong duality once that is published.
In classical single-machine stochastic scheduling, jobs with independent random processing requirements are processed one after another, and the makespan (the completion time of the last job) is the same for every schedule that never idles: it is . Research therefore concentrated on weighted flow times and rewards. Browne and Yechiali (Operations Research 38(3), 1990, 495–498) studied jobs that deteriorate while they wait: the longer a job is delayed, the more processing it needs. Such models arose in the control of queueing and communication systems (Browne 1988; Browne and Yechiali 1989) and in inventory issuing, where stored items lose quality at item-specific rates. Under deterioration the actual processing times depend on the order, so the makespan, and its expectation, become functions of the schedule, and the basic question is which order minimizes the expected makespan.
There are jobs, all available at time , and a single processor. Job has an initial processing requirement , a random variable on a probability space : the time needed to complete job if it is processed first. Under linear deterioration, a job whose processing is delayed until time needs
where is its deterministic growth rate. A job stops deteriorating once it is put on the processor.
Only nonpreemptive strategies without idling are allowed, so a policy is a permutation of , with meaning that job is the -th processed. The completion times follow the model: , and the job in position starts at and takes , so
The makespan is and the expected makespan is . In Lean these are completionTime X α π k ω, makespan X α π ω and expectedMakespan P X α π in the namespace DeterioratingJobs.Makespan.
The paper's Lemma 1 concerns, for real numbers and , the sum (1)
the Lean lemma1Sum μ γ π (empty product ).
If the are integrable, , and schedules the jobs by increasing values of , then
The result is an index rule: each job receives a number computed from its own data, , and sorting by that number is optimal. It needs only the means of the initial requirements, not their distributions, and it holds without independence. The same reduction to Lemma 1 gives the paper's other index rules: the variance of the makespan under independent requirements, the Poisson-shock model (5), Lévy-type growth (6) and setup/detach times (7). In inventory issuing, it says which stored item to issue first when items lose value at item-specific linear rates. Lemma 1 itself, which the paper attributes to Rau (1971) and relates to optimal search, is a general statement about ordering products of factors along a sequence.
The result is proved in the paper by an appeal to Lemma 1, whose proof is given there as one sentence ("direct upon an interchange argument"). None of these statements has a machine-checked proof on Prove2Me or in Mathlib. This mission produces a formal model of linear deterioration on a single machine, a formal proof of the interchange lemma with ties handled, and the formal index rule.
The algebra of one adjacent interchange is short. The work is in passing from that local comparison to optimality over all permutations, with ties allowed: the paper speaks of "the permutation ordered by increasing values", but with equal indices several permutations qualify, and each of them must be shown optimal. The natural route, "an optimal permutation exists and must be sorted", needs care, because a sorted permutation is not unique and the swap that improves an unsorted permutation may only weakly improve it. On the probabilistic side, the expectation of the makespan must be reduced to the expectations of the ; the makespan is a polynomial in the with deterministic coefficients, so this is linearity of the integral, but integrability has to be carried through the recursion.
Fin N (0-based: Lean job i is the paper's job ); a policy is π : Equiv.Perm (Fin N) with π k the job in position k, as in the paper's . is allowed.(Ω, P) with [IsProbabilityMeasure P]; is Ω → ℝ; expectations are Bochner integrals, and every theorem about them assumes each integrable. The growth rates are deterministic reals.Monotone), and "decreasing" means Antitone; "is minimized" means against every permutation; "expected" means the integral of an integrable random variable.PalmQueueing.Ordering.interchange_permutations (interchange permutations of a GI/GI/1 queue) and the additive, non-deteriorating completion-time models MooreLateJobs.Shared.completionTime and NumStochOpt.ListScheduling.Makespan.Contributions welcome: proofs of the milestones, a reusable "sorted permutation minimizes a sum of products" lemma, and the variance index (3) as an extension.
The alternating direction method of multipliers (ADMM) is one of the most widely used algorithms for large-scale convex optimization in statistics, machine learning and signal processing. Its appeal is decomposition: a problem whose objective splits into two parts, coupled only by a linear constraint, is solved by alternately minimizing over each part and updating a dual variable. Each subproblem is often a proximity operator, a projection or a small linear system, so ADMM turns problems such as the lasso, sparse inverse covariance selection and consensus fitting across many machines into sequences of simple steps. The survey of Boyd, Parikh, Chu, Peleato and Eckstein (DOI 10.1561/2200000016) made the method standard, and every algorithm in its later chapters is justified by one convergence result, stated in §3.2.1 and proved in Appendix A. This mission formalizes that result and the inequalities behind it.
The method goes back to Gabay and Mercier (1976). Eckstein and Bertsekas (1992) proved convergence through the theory of maximal monotone operators, by identifying ADMM with Douglas–Rachford splitting applied to the dual problem. The proof in Appendix A of the survey is different: it is a direct Lyapunov argument in finite dimensions that uses only convexity and elementary algebra.
Let and , let , and . The problem is
with optimal value . The augmented Lagrangian with parameter is
and is the ordinary Lagrangian. For , ADMM generates iterates by
The state is ; plays no role. The primal residual is , the dual residual is , and .
Two assumptions are made. Assumption 1: and are closed, proper and convex. Assumption 2: has a saddle point , i.e. for all . Nothing is assumed about the ranks of and . The convergence proof uses the Lyapunov function
Under Assumptions 1 and 2 and for , every ADMM run satisfies
The statement fixes no rate and no constant. It does not claim convergence of or , which fails in general (p. 17).
In the order of Appendix A:
The theorem is what licenses every specialized ADMM of the survey (lasso, basis pursuit, covariance selection, consensus and sharing, distributed model fitting): each of these chapters only computes the subproblem solutions, and correctness of the overall method is inherited from §3.2.1. Inequality (3.11) and its corollary in §3.3.1 justify the primal/dual residual stopping criterion (3.12) used in practice: small residuals certify small suboptimality.
The result itself is classical and proved; it is not open. To our knowledge no machine-checked proof of convex two-block ADMM convergence exists in Lean's Mathlib. Formalizing it produces a reusable development of the augmented Lagrangian method with explicit domain handling for extended-valued convex functions, and checks a proof whose index bookkeeping the printed text leaves loose (the monotonicity step and (A.1) need , see below).
The obvious argument, "the subproblem optimality conditions plus the saddle point give a decreasing quantity", works only once the right Lyapunov function is found and the cross term is controlled. That term has no sign from the optimality conditions of a single iteration, and at the first iteration, where is an arbitrary starting point, the decrease (A.1) can genuinely fail. A second obstacle is that and need not converge or even be bounded when or is rank deficient, so objective convergence cannot pass through limits of the primal iterates; it has to come from the two-sided bounds (A.2) and (A.3). Finally, the subdifferential sum rule used to linearize each subproblem must be handled for functions taking the value .
EuclideanSpace ℝ (Fin n); matrices act through Matrix.toEuclideanLin; the problem data are bundled in a structure Problem n m p.ShorNonsmooth.Subdiff.subdifferential relative to the domain.A complete development needs the subdifferential of a convex function plus a differentiable quadratic, the first-order characterization of a constrained minimizer, and elementary limits; all of this is reusable for the later missions of the series, which take ADMM runs as given. Proofs of individual milestones are welcome independently.
Two-stage optimization separates a decision made before uncertainty is observed from one made after a scenario is known. A fully adaptive policy can choose a different second-stage decision in each scenario, while a static robust solution commits to a single second-stage decision that works in every scenario. Static solutions can be simpler to implement, but their worst-case cost may be higher. Bertsimas and Goyal ask how large this cost difference can be when both the right-hand sides of the constraints and the second-stage prices vary. Their Theorem 5.1 gives a factor of four when the paired uncertainty set is symmetric and nonnegative, even when both stages contain integer variables.
The distinction matters in planning problems where one policy is fixed in advance and another could respond to realized demand or prices. A uniform bound lets a planner assess the cost of the static restriction without solving every adaptive policy exactly. The source is the authors' manuscript; all page and result numbers in this mission refer to that manuscript, not to the journal pagination.
Fix matrices and . A scenario supplies a right-hand side and a second-stage cost vector . The first-stage cost vector is . For a set of designated integer coordinates, write for the nonnegative real vectors whose coordinates in are integers. After relabelling, this is the paper's .
In the robust problem , one first-stage decision and one second-stage decision must satisfy for every scenario. Their cost is . In the adaptive problem , is still chosen once, but may depend on the scenario. Its constraints are for every , and its cost is . The optimal values and are infima over feasible decisions in these respective problems; these are models (1.5)–(1.6).
The paired uncertainty set is . It is symmetric when it contains a point such that belongs to the set exactly when does, for every displacement . The point is itself a scenario realization. The smallest coordinatewise bounding hypercube has lower and upper corners and ; its center is . These are Definition 1.2 and displays (2.5)–(2.7).
The goal is Theorem 5.1:
The factor applies to every nonnegative symmetric paired uncertainty set and to both continuous and mixed-integer decisions. The theorem does not require an optimal adaptive policy to attain its infimum. The milestones record the source's geometric Lemma 2.3 and the estimates labelled (5.1)–(5.4), which supply the center-scenario cost and feasibility statements with the explicit factor four. They are stated for arbitrary feasible adaptive policies so the conclusion also covers nonattained infima.
The result bounds the price of committing to a single second-stage decision, despite uncertainty in both the constraints and the objective. In this setting the comparison is independent of the number of scenarios and of the dimensions . The paper also considers right-hand-side-only uncertainty, positive sets, and hypercubes; this mission isolates its symmetric paired-uncertainty result §5.1.
The theorem is proved in the paper. The remaining formalization work is a machine-checked development of the model, the bounding-hypercube geometry, the cost inequalities, and the passage from arbitrary feasible policies to the optimal values. The resulting definitions of mixed-integer domains, robust and adaptive feasibility, and extended-real optimal values can also support the other results in this paper's mission series. The theorem statements here are open proof targets, with no machine-checked proofs claimed.
The worst-case maximizer of can vary with , and an adaptive policy can choose a different integer vector in every scenario. Selecting one of those vectors as a static decision therefore gives no immediate cost or feasibility guarantee. The point of symmetry is a realizable scenario, but it must control both components of every other paired scenario. Without nonnegative data, doubling the center-scenario decision may fail to cover a positive right-hand side, and the cost comparison can fail as well. Integer coordinates also constrain which scalings preserve the decision domain; the exact factor in the theorem is compatible with doubling, unlike arbitrary fractional rescalings.
Vectors are real functions on finite index types, matrices use Mathlib's matrix-vector product, and inequalities are componentwise. The scenario set is the range of , with a product-space symmetry predicate. No probability measure or measurability structure is used in these worst-case problems. Both stages may have integer coordinates designated by sets ; no continuous-only second-stage restriction is imposed.
Optimal values and worst-case costs use extended real numbers. An infeasible problem has value ; a real infimum over an empty feasible set would incorrectly return a default zero. Symmetry includes a center belonging to the scenario range, so the scenario set is nonempty. Combined with nonnegative coordinates, symmetry bounds every scenario coordinate and makes the bounding-hypercube endpoints meaningful. The hypotheses retain , , and , which the source uses in its factor-four estimate. A statement restricted to continuous recourse, an assumed optimal adaptive policy, or a zero-valued infeasible problem would not express this target.
The source prints in (1.5)–(1.6), although the model's second-stage integer count is ; the domain here follows the surrounding convention. Lemma 2.3 is stated here for nonnegative sets, the regime needed for its second inequality. Its coordinatewise suprema and infima agree with the printed maxima and minima in this bounded symmetric setting. Contributions to the shared domain and geometry lemmas, the mixed-integer scaling fact, and the optimal-value comparison are all useful to the goal.
Many operations problems are decided in two stages: a first-stage decision is fixed before an uncertain quantity is revealed, and a second-stage (recourse) decision is chosen afterwards. Two classical ways to optimize such a problem differ in how they treat the uncertainty. Two-stage stochastic optimization minimizes the expected cost under a probability distribution over scenarios, with a recourse decision adapted to each scenario. Robust optimization fixes a single solution that must be feasible for every scenario in an uncertainty set, and minimizes the worst-case cost. The robust problem is usually far easier to solve, but it is conservative; the question is how much it can lose.
Bertsimas and Goyal (Math. Oper. Res. 35(2), 2010) answer this for uncertain right-hand sides. Their main positive result (Theorem 2.1) bounds the stochasticity gap: if the uncertainty set and the probability measure are both symmetric, the robust optimum is at most twice the stochastic optimum. This mission formalizes the companion negative result, Theorem 2.6: once the uncertainty set is not symmetric, the gap is not bounded by any constant. The example is the simplest non-symmetric set in practice, the corner of the unit simplex, with the uniform distribution on it. It shows that the symmetry hypothesis in the positive result is not an artefact of the proof.
Fix matrices , and costs , . Let be a set of scenarios, the right-hand side realized in each scenario, and the uncertainty set. Let be a probability measure on .
In general some coordinates of and are required to be integers; in this mission's instance there are none. A set is symmetric (Definition 1.2) if some satisfies for every .
The instance of Theorem 2.6 has no first stage (, so , ), , , and . The uncertainty set is the corner simplex (2.29)
and is the uniform probability measure on it: .
On this instance,
The constant is the paper's, and it is exact: the robust optimum is and the stochastic optimum is at most .
The result. Together with Theorem 2.1, Theorem 2.6 locates the boundary of the paper's positive theory. Theorem 2.1 says a static robust solution loses at most a factor of against the fully adaptive stochastic optimum under symmetry; Theorem 2.6 says that without symmetry the factor can be , hence arbitrarily large as the dimension grows. The paper's later results (the bound for "positive" uncertainty sets, Theorem 2.7) are motivated by this example: some structural condition replacing symmetry is necessary. The same instance also separates the adaptive problem from the stochastic one (p. 21), which shows that the gap comes from comparing a worst case with an expectation, not from the lack of adaptivity.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The formalization adds two things beyond the paper. First, it pins down the problems as optimization problems over integrable policies with values in the extended reals, so that the inequality cannot hold for a degenerate reason. Second, it requires the volume of the corner simplex and the first moment of a coordinate on it, which the paper calls "standard computation". Neither is in Mathlib at the time of writing: Mathlib has the standard simplex as a convex set but no volume formula for it.
The optimization part is short: one feasible stochastic policy and the vertices of the simplex give both bounds. The work is in the measure theory. The volume and the moment are iterated integrals with variable upper limits, and the paper calls them "standard computation"; as statements about Lebesgue measure on they are dimension-dependent identities that Mathlib does not contain, for the simplex or for the convex hull of points. The other technical point is the scenario model: the uniform measure lives on , while the integrals live on , so the expectation must be moved through the push-forward of by .
Fin k → ℝ with the componentwise order; products are A *ᵥ x and c ⬝ᵥ x. The paper's -th coordinate is index of Fin n, and is lastUnit n.EReal infima over the feasible set, equal to when the problem is infeasible. No optimal solution is assumed to exist.Needed infrastructure: the volume of the corner simplex in and the integral of a coordinate over it (reusable well beyond this mission, for example for Dirichlet distributions and order statistics), and the change of variables from to through the push-forward. Contributions of either simplex integral, in any form that implies the stated milestones, are welcome.
This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.
The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.
The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.
The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.
For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.
The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryAssortment optimization asks a retailer which products to offer when customers substitute among them. The nested logit model groups products into nests and is one of the most used choice models in revenue management, because it relaxes the independence of irrelevant alternatives of the plain multinomial logit model while keeping choice probabilities in closed form. Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) study how the tractability of the assortment problem under this model depends on two features: whether the dissimilarity parameters of the nests are at most one, and whether a customer who selects a nest always buys there (fully-captured nests).
When the dissimilarity parameters are at most one and the nests are fully captured, offering the highest-revenue products in every nest is optimal (Theorem 4 of the paper). This mission concerns what survives when a dissimilarity parameter exceeds one, the regime the paper calls possibly synergistic products. Then the problem is NP-hard (Theorem 5), and the paper shows that the same nested-by-revenue assortments still achieve an explicit, data-dependent fraction of the optimal expected revenue.
There are nests and products in every nest. Product of nest has a revenue and a preference weight , ordered so that . Nest has a dissimilarity parameter , and is the weight of leaving without choosing a nest. Throughout this mission the nests are fully captured: the within-nest no-purchase weights are zero. For an assortment in nest ,
and the expected revenue of is
Problem (2) maximizes ; its optimal value is . The nested-by-revenue assortment collects the highest-revenue products of nest , with and .
Problem (2) is equivalent to the linear program (3): minimize subject to and for every nest and every . Problem (4) keeps the second family of constraints only for candidate assortments; here the candidates are , which gives a linear program with variables and constraints. The performance factor of the nested-by-revenue assortments is
Assume for every nest, for some nest, positive revenues and . If is an optimal solution of (4) over the nested-by-revenue assortments, then
Combined with Theorem 1 of the paper this yields for the assortment read off the small linear program; that consequence is a companion item.
Two companion statements follow the goal: the bounds and when revenues, respectively preference weights, within each nest differ by at most the factors , ; and the guarantee .
Because problem (2) is NP-hard once a dissimilarity parameter exceeds one (Theorem 5 of the paper), an exact polynomial algorithm is not expected, and a guarantee for a polynomial-size candidate family is the natural substitute. Theorem 7 gives one with an explicit factor computed from the data: when revenues within each nest are balanced, when preference weights within each nest are balanced, and the nests may differ arbitrarily from one another. The same linear-programming argument (Theorem 1) is reused for partially-captured nests in §6 of the paper.
The result is proved in the paper (Appendix A.1); no machine-checked version is known. A formalization verifies an appendix argument that is stated with little detail, and fixes the conventions that the page leaves implicit, such as the value of the objective of (8) at and the role of the standing assumption that some exceeds one.
Theorem 7 is a feasibility statement for the exponentially many constraints of (3), one per subset of every nest, while optimality of only controls the nested-by-revenue constraints per nest. The obvious approach, comparing each subset directly with a nested-by-revenue assortment, fails: when the nested-by-revenue assortments are not optimal within a nest, and the example of §4.1 shows that they can lose an unbounded factor. The constant must absorb the gap between a fractional assortment and its two neighbouring nested-by-revenue assortments, which the dual-style solution of the small program does not see.
Lean 4 with Mathlib. Nests form a finite type ι; products are Fin n, indexed from , so is nbr n j = {k | k < j} and product of the page is ⟨k - 1, _⟩. Powers are real powers (Real.rpow), and division is total (), which gives and value for the objective of (8) at .
Standing assumptions in every statement: , , , , , revenues ordered within each nest (§1); for every nest and for some nest (§4, p. 16). Added and disclosed: wherever (6) appears, so that no denominator of (6) vanishes; , the nonempty range of (6); only in the guarantee , inherited from Theorem 1. The factor enters as a real number with the hypothesis that it is the greatest element of the set of terms of (6). An optimal solution of (4) is a feasible pair whose is minimal among feasible pairs.
A trivializing formalization is ruled out: is the maximum of (6), not an arbitrary upper bound, and the goal states feasibility for the full program (3) over every subset of every nest, not for (7) or for the candidate collection.
Needed infrastructure: maximization of a continuous function on , the greedy solution of a continuous knapsack, monotonicity of weighted averages and elementary real-power calculus. These are reusable beyond this mission. Proofs of any milestone, of the companions, and of the §4.1 example are welcome.
A portfolio manager who maximizes expected utility needs the distribution of asset returns, but in practice only estimates of its first two moments are available, and these estimates are themselves noisy. Distributionally robust optimization handles this by optimizing against the worst distribution in a set of plausible ones. Delage and Ye (Operations Research 58(3), 2010) proposed a set of distributions defined by confidence bounds on the mean and on the second-moment matrix, showed that the resulting problems are solvable in polynomial time for a large class of costs, and applied the framework to portfolio selection.
The set contains an upper bound on the covariance but no lower bound. Remark 1 of the paper says a lower bound "leads to important computational difficulties" and argues it should be unnecessary: for a concave utility, a less predictable market can only reduce expected utility, so the worst distribution should already have the largest covariance allowed. Proposition 3 in §5.2 turns this argument into a theorem for piecewise-linear concave utilities and unconstrained support. This mission formalizes Proposition 3 and the steps of its proof.
Let assets have a random return vector , and let be a portfolio, so the return is . A distribution of is a Borel probability measure on with finite second moments. For symmetric matrices, (the Loewner order) means is positive semidefinite.
Given a support set , a centre , a positive definite matrix and , , the distributional set of Assumption 3 is
The second constraint, (1b), is the covariance constraint.
The utility is piecewise linear concave, with pieces, and the cost of a return is :
With estimates , of the mean and covariance, the inner problem of the robust portfolio problem with unconstrained support and an exactly known mean () is
The proof relates (18) to a semidefinite program in variables , , :
For every (the mean-uncertainty radius of the robust portfolio problem (16); (18) is the case ),
The worst-case expectation is attained, and at a distribution for which the covariance constraint holds with equality. The statement holds for every portfolio , every , every , every , every , every and every .
The proposition justifies a modelling decision of the whole paper: for portfolio problems with piecewise-linear concave utility, adding a lower bound (display (2)) to the distributional set cannot change the robust decision, so the computational difficulty that lower bound would cause is avoided at no loss. It also shows that, under these assumptions and with , the paper's semidefinite formulation solves the known-moment portfolio problem of Popescu (2007) in polynomial time (Remark 4). The worst case is explicit: a finite mixture of distributions with prescribed first and second moments, read off an optimal solution of (19).
The result is proved in the paper; no machine-checked version is known. Formalizing it requires a moment-problem argument (from a distribution to a feasible point of an SDP) and its converse (from an SDP solution to a distribution), both of which are reusable for other moment-based distributionally robust results. The proposition concerns the robust portfolio problem with ; the paper's proof writes out only "for simplicity of our derivations". The goal states the proposition for every ; the milestones follow the written proof and are stated for .
The obvious argument, "a concave utility prefers less spread, so the adversary maximizes spread", does not prove anything by itself: increasing the second-moment matrix of a given distribution in the Loewner order does not determine its law, and the expected cost depends on the whole law, not on the moments. The proof goes through the semidefinite program (19). Two steps carry the weight. First, every distribution in must be mapped to a feasible point of (19) with no smaller value, although the cost is only piecewise affine in . Second, an optimal point of (19) must be turned back into a distribution in ; this needs the existence of random vectors with prescribed first and second moments, and care with blocks where , which the paper sets aside "without loss of generality" although such a block can carry a nonzero that the mixture would lose.
Fin n → ℝ; all Euclidean quantities are dot products, never the sup norm. Matrices are Matrix (Fin n) (Fin n) ℝ; is (B - A).PosSemidef; is Mathlib's matrix inverse, used only with .Measure (Fin n → ℝ) that is a probability measure and whose coordinates are in (MemLp _ 2). This makes every mean, second moment and expected cost a genuine integral; without it a non-integrable expectation would evaluate to .[NeZero K]).The source is the authors' draft of 20 February 2008 of the Operations Research paper; every page, display and label in this mission refers to that draft.