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?
Data marketplaces buy personal data from many individuals to estimate population statistics. Two features set such pricing apart from an ordinary procurement auction. First, each data owner has a private cost of sharing, so the buyer must design a menu of payments that elicits these costs truthfully. Second, data are correlated across people: an individual who refuses to share still loses privacy when similar people share. Liao, Su, Ziani, Wierman and Huang call the consequence the privacy paradox: privacy-conscious people may join a platform because abstaining does not protect them (arXiv:2105.14262, §1; published in Mathematics of Operations Research, 2024).
The paper asks how an analyst with a fixed budget should design such a mechanism when the goal is statistical: to estimate a population mean while trading off the bias caused by non-participants against the variance caused by sampling only some participants. The answer extends the optimal-auction framework of Myerson (Math. Oper. Res. 1981) and the data-procurement mechanisms of Roth and Schoenebeck (EC 2012) and Chen, Immorlica, Lucier, Syrgkanis and Ziani (EC 2018) to a setting with participation externalities and an adversarial correlation between data and costs.
Agents are split into groups . An agent in group has a cost drawn from a density on the support , with distribution function . At a fixed desired participation profile the privacy cost of a participant is with , a non-participant suffers , the gap is strictly increasing, and participants receive a benefit .
The analyst posts a menu: a selection probability and a payment for a reported cost . A participant with true cost who reports has expected utility
The menu is truthful if reporting maximizes this utility. An agent joins if some report gives utility at least , and the menu induces if the fraction of joining agents of group is for a threshold . The virtual cost is
For the statistical problem, Appendix C of the paper discretizes the costs and sorts all virtual costs of participants as , with cell probabilities summing to . Given agents, a budget , a constant collecting the participation terms, and a weight on the variance, the analyst chooses and an adversary chooses the data probabilities in the min-max program
subject to the budget , under the standing condition .
There are constants , , and a feasible, non-increasing allocation
such that for every feasible . The constants are left existential, as in the printed theorem; the case analysis that identifies them belongs to the milestones.
Theorem 1 is a participation-aware version of Myerson's characterization: it shows that the analyst loses nothing by restricting to monotone allocation rules with one explicit payment, and it pins down the payment that realizes a target participation rate. Theorem 2 then solves the analyst's worst-case bias–variance problem: the optimal selection probability is flat for cheap agents and decays like the inverse square root of the virtual cost for expensive ones. This shape explains when the mechanism can be strictly truthful (a strictly decreasing rule, Corollary 2, in the low-budget regime) and when only weak truthfulness is possible (a flat region, larger budgets).
The paper proves Theorem 2 for discrete costs and passes to continuous costs by letting the number of cells grow without bound, a step it asserts without proof. The mission formalizes the discrete theorem that Appendix C actually proves, together with both directions of Theorem 1. None of these results has a machine-checked proof yet.
The goal is a min-max statement about a program that is convex in the allocation and concave in the adversary's choice, with a coupled budget constraint. The natural first idea, to solve each player's first-order conditions and plug them into each other, does not by itself produce a solution: the analyst's best response clips at 1, the adversary's best response may be interior on some cells and at the boundary on others, and which cells are which depends on the budget. The paper resolves this by a case analysis on the ratio against the values of , with thresholds obtained from intermediate-value arguments, and each case requires its own multiplier and its own adversary strategy.
For Theorem 1 the obstacle is that the paper's envelope argument differentiates the allocation rule, while the theorem quantifies over all monotone rules, which need not be differentiable. The "only if" direction must be recovered from the convexity of the maximal utility as a function of the true cost.
All statements live in the namespace PrivacyParadox.Alloc and use one definitions file. The group layer fixes one desired profile, so , , and are functions of the cost or numbers; their dependence on participation rates and correlation strengths plays no role in Theorems 1–2. The discrete layer indexes cells by as the paper does, with real-valued data and Real.sqrt.
The formalization commits to the following conventions, each disclosed in the item it affects:
Two trivializing readings are excluded: the goal compares with every feasible allocation, so it is not the best-response property of Lemma 3, and it asserts the existence of rather than assuming an optimizer of the stated form.
A complete development needs elementary real analysis (interval integrals of monotone functions, Fubini on a triangle, the intermediate value theorem) and finite-dimensional convex optimization (first-order optimality for a concave quadratic on a box and for a separable convex program with one linear constraint). The latter two are reusable well beyond this mission. Proofs of milestones are welcome in any order. The continuous form of Theorem 2, Lemma 1 (the derivation of the objective from the Horvitz–Thompson estimator), Propositions 1–2 and Properties 1–4 are not part of the mission.
Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is
and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank- PSD matrices is a submanifold of with the Euclidean metric. In the quotient geometry one writes with a full-column-rank factor and optimizes over equivalence classes . Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.
Matrices carry the Frobenius inner product . The objective is twice continuously differentiable and symmetric, (the paper's standing assumptions); and are its Euclidean gradient and Hessian.
Embedded geometry. , viewed as . Its tangent space is the span of the tangent cone. The Riemannian gradient is the orthogonal projection of onto , and the Riemannian Hessian quadratic form is the derivative at along any curve in with , .
Quotient geometry. The total space is , the matrices of full column rank, with the objective (18a). A weight , smooth and symmetric positive definite, defines the metric . The vertical space is tangent to the orbit , and the horizontal space is its -orthogonal complement. Tangent vectors of the quotient are represented by horizontal vectors: is the horizontal part of the total-space gradient , and for horizontal , where is the Levi-Civita connection of (Koszul formula).
Comparison data. ; spans the top eigenspace of , , . For a quadratic form on a -dimensional space with inner product , is its -th largest eigenvalue relative to (). are the extreme singular values of an matrix.
If in addition for all orthogonal , then for every and ,
and if is a Riemannian first-order stationary point of (18a),
both Hessians have eigenvalues, and lies between and .
Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through , so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on and the spectrum of . The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight (flat , right-invariant , or ) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.
The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank- matrices (Theorems 4–7) are natural follow-up missions on the same definitions.
The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection along the manifold, which produces the curvature term ; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying of the tangent cone with the block form (14) needs an explicit chart of the rank- PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.
EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight takes values in in the same form so that is defined.ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension " is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every .Useful contributions include Mathlib-level lemmas on the tangent cone of the rank- PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for .
In bundle size pricing (BSP) a seller of many products offers a menu of bundles in which the price of a bundle depends only on its size, the number of items in it. Customers choose which items to put in a bundle and which size to buy. Season tickets for theatres and sports teams, cable-TV channel packages and streaming plans priced by the number of simultaneous devices are priced this way, and BSP is known to recover much of the profit of full mixed bundling with only a handful of prices (Chu, Leslie and Sorensen 2011).
Choosing the optimal size prices is hard. For given prices, the customer's value for the best bundle of size is a maximal partial sum of order statistics of the item valuations, and the seller's expected profit depends on the joint law of these sums across sizes. Even when that law is known, it is not known whether the resulting pricing problem is tractable.
Li, Sun and Teo (2021) replace the exact choice model by the cross moment model (CMM) of Mishra, Natarajan, Tao and Teo (2012): only the mean vector and the covariance matrix of the bundle valuations are specified, and choice probabilities are those of the extremal distribution, among all laws with these two moments, that maximizes the customer's expected surplus. Their main result (Theorem 2) is that the seller's profit, written as a function of the choice probabilities, is concave, so the pricing problem becomes a concave maximization over a simplex. This mission formalizes that result.
Let be the number of bundle sizes. Let be the mean valuation vector, the vector of bundle costs, and the covariance matrix of the bundle valuations (the outside option, with value , is excluded). Write for the all-ones vector. The simplex and its interior are
A point is a vector of choice probabilities: is the probability that the size- bundle is bought, and the probability of buying nothing.
For a positive semidefinite matrix , denotes its unique positive semidefinite square root, and means that is positive semidefinite. Define
where is the diagonal matrix with diagonal , and below is the vector of diagonal entries of . In the paper, Theorem 1 and Lemmas 1–2 show that for every is the CMM demand at exactly one price vector, namely with
Substituting this price into the profit gives the BSP-CMM profit of Problem (6):
The statement is uniform in , , and in the positive definite ; it fixes no constant.
Concavity of turns bundle size pricing under the cross moment model into a concave program over the simplex: a local maximizer is global, and the problem can be passed to a conic solver through the semidefinite representation of milestone 5. The paper uses this to price bundles directly from two moments of the valuation distribution, and notes that the same reduction approximately solves other bundle pricing problems once they are written as multidimensional pricing problems. Before this result it was known that CMM choice probabilities are computable by convex optimization (Ahipaşaoğlu, Li and Natarajan 2018), but not whether pricing under CMM is tractable.
The result is proved in the paper; it has no machine-checked proof. The mission produces a formal statement of Theorem 2 against the explicit function (6), and the chain of the paper's proof as separately provable milestones. Several of these are reusable beyond the paper: Loewner concavity of , Loewner concavity of the square root composed with it, and the Schur-complement description of a bordered linear matrix inequality over the reals.
The function is not a composition of standard concave functions: it contains the inverse square root of a matrix that depends quadratically on , inside both a diagonal extraction and a quadratic form. The scalar composition rules for concavity do not apply to matrix-valued maps, and the second derivative of has no usable closed form. What is needed is the operator monotonicity and operator concavity of the matrix square root on positive semidefinite matrices (Horn and Johnson 1990). Mathlib has the corresponding results only for elements of C⋆-algebras, through the continuous functional calculus; real symmetric matrices with the Loewner order are a separate instance whose square root, monotonicity and concavity must be connected to that theory or proved directly.
Everything is stated inside BSPConvex.CMM. Vectors are Fin m → ℝ and matrices Matrix (Fin m) (Fin m) ℝ; is named Sig. The objects , , , , , , (defined by the displayed formula), (written literally as (6)), and the bordered matrix are definitions in one file. is CFC.sqrt under open scoped MatrixOrder, and is (A - B).PosSemidef throughout. is (CFC.sqrt (T q))⁻¹, the matrix inverse.
The formalization departs from the page in three disclosed ways:
A formalization that defines through or so that concavity is definitional, or that states the theorem on a set where it is vacuous, does not count: is the literal expression (6), and is nonempty for every (it contains ).
Contributions welcome beyond the milestones: a real-matrix version of operator monotonicity and concavity of the square root, the Schur complement criterion for real block matrices with a positive definite block, and differentiability of on positive definite matrices.
A seller who offers products and sets one price vector for all customers must price for a heterogeneous population. The finite-mixture logit (FML) model describes such a population with a small number of segments. Each segment follows its own multinomial logit (MNL) demand, so this is the simplest heterogeneous extension of the MNL model. It is widely used in empirical demand estimation (Train, 2009). Pricing under it is harder than under a single MNL. The single-segment MNL revenue is not concave in prices (Hanson and Martin, 1996), but it becomes concave once it is written in market shares (Li and Huh, 2011). With two or more segments that change of variables fails, and the revenue can be multimodal (Li et al., 2019). Local search then gives no quality guarantee.
van de Geer and den Boer give an algorithm with a guarantee: for every it returns prices whose revenue is at least times the optimum. This mission formalizes that guarantee, Theorem 1 of the paper (published in Management Science, doi:10.1287/mnsc.2021.4272).
There are segments with shares , , and products . Segment values product at . The price sensitivity depends on the product but not on the segment. At prices , a segment- customer buys product , or nothing, with probability
and the expected revenue is .
All maximizers of lie in a box , where and adds to the largest single-segment revenue. The no-purchase vector is , and is the set of attainable no-purchase vectors. Fix and substitute . The best revenue among prices with is then the value of a concave program with linear constraints , where .
Algorithm 1, , searches the -dimensional set by branch and bound over boxes of sup-norm radius around centers , clipped to . It keeps a lower bound , an upper bound , and an incumbent . In each pass and for each box that meets , it solves a linear program . A map turns the solution into an attainable point in the box. The pass then evaluates , compares an upper bound with , and keeps or discards the box. Kept boxes are split into boxes of half the radius. The loop runs while .
For every , terminates after finitely many passes, and every maximizer of gives prices with
The goal is posed for every bounding rule with two properties, for some constant and all , :
It is also posed for every choice of LP solution and every visiting order of the boxes.
Theorem 1 is an approximation scheme for a non-concave revenue function. The search space has dimension , the number of segments, rather than , the number of products. The reduction behind it (Lemma 1, Equation (5) and Proposition 2) applies to any search over no-purchase probabilities, not only to branch and bound. Proposition 7 and Corollary 1 give an exact LP test for whether a box of no-purchase probabilities contains an attainable point.
The results are proved on paper. None of them has a machine-checked proof, and the platform has no FML model, no no-purchase reparameterization and no pricing branch and bound. A formal proof would also settle two printed defects found in planning. First, Proposition 4 (a Lipschitz bound used inside the paper's bounding rule ) is false as printed: it pairs a sup-norm gradient bound with a sup-norm displacement. Second, the printed constraints (15)–(16) of make Proposition 7 false for centers outside , and Algorithm 1 creates such centers. The mission states the corrected versions.
The obvious argument is the one in the paper: boxes that may contain a maximizer are never discarded, and the gap between the bounds shrinks with the radius. Writing it out runs into two problems.
Proposition 1 is the heaviest analytic milestone. It needs coercivity of in every direction, including negative prices, and a first-order argument for the box.
Segments and products are Fin m and Fin n, and vectors are functions on them. The norm on Fin m → ℝ is the sup norm, as on p. 17. The standing assumptions are , with (the page writes ), and . , and are real suprema, read only where their sets are nonempty and bounded. is an extended real, so line 2 sets it to , line 6 to , and follows extended-real arithmetic.
Algorithm 1 is a definition, not a hypothesis. One pass is a left fold over an enumeration of the finite set of centers. The run is an iterate of the pass, and the state after the first failed loop test is the output. The departures from the page are these:
The counterexample to Proposition 4 has : , , , and . The point then has , which exceeds . Propositions 3, 4, 5 and 8, Theorem 2 (running time) and the competition extension of §5 are not posed.
(U1) and (U2) together say exactly that is -Lipschitz on , and then satisfies both. The goal is therefore not vacuous. It cannot be trivialized either: it concerns the defined algorithm, with every line except the bounding rule kept, and its conclusion compares with a global maximum of over all of .
A complete development needs elementary analysis of logit probabilities, concavity of , compactness on boxes, finite LP attainment, and an invariant proof for an iterated fold. The no-purchase reparameterization (Lemma 1, Equation (5), Proposition 2) is reusable for other FML pricing results. Proofs of the milestones, a Lean proof that is Lipschitz on (which makes (U2) concrete), and a corrected Proposition 4 are all welcome.
Schools, universities and public employers that run affirmative action decide whom to admit from a set of applicants who are ranked by a priority ordering (exam scores, lottery numbers, seniority) and who belong to a minority or a majority group. The procedures used in practice, such as the reserve and quota systems of Boston, Chicago and New York school choice, or the reservation system of India's public sector, are choice rules: functions from the set of applicants, their types and their priorities to the set of admitted students. Market design needs these rules to be substitutable (a chosen student stays chosen when other applicants withdraw), because substitutability is the condition under which centralized clearinghouses produce stable matchings (Hatfield and Milgrom, 2005; Hatfield and Kojima, 2008).
B. Doğan and K. Yıldız, Choice with Affirmative Action (SSRN 3626941; Management Science, doi:10.1287/mnsc.2022.4447), ask which affirmative action rules are substitutable and also respond monotonically to the minority students they are meant to help. Their Theorem 1 says that such rules are exactly reserve rules whose reserve number changes by at most one in response to a type or priority change. This mission formalizes the direction of Theorem 1 that the paper proves correctly: every such rule is a bounded reserve rule.
Fix a nonempty finite set of students and a capacity . A problem is a set of applicants, a type function ( minority, majority) and a strict priority ordering on . The rank of is one plus the number of students with higher priority. The top tier is the set of students of rank at most , the students a pure priority rule would admit; the bottom tier is . Superscripts and select minority and majority students: , , , .
A choice rule picks a subset of at most students. is the set of chosen minorities and the minorities chosen via affirmative action. The axioms are:
An affirmative action rule satisfies these three. Substitutability requires whenever and . MPI (monotonicity in priority improvements) requires that improving the priority of a chosen minority student does not reject any chosen minority student. MTC (monotonicity in type changes) requires that turning a chosen minority student into a majority student does not reject any other chosen minority student.
A reserve function gives each problem a number that depends only on the types of the students of ranks . admits a reserve representation via if chooses all of , then the highest-priority students of (all of them if fewer), then the highest-priority majority students until the seats are filled. The representation is bounded if satisfies Condition B: changing the type of a top-tier minority, improving a top-tier minority's rank, or worsening a top-tier majority's rank changes by or , and worsening the rank of a top-tier majority leaves unchanged when is among the lowest-ranked top-tier majorities.
Milestones 2 and 3 together give the goal, with .
The result describes every substitutable, monotone affirmative action rule by one integer per top-tier type configuration, constrained by local bounds. A designer who wants substitutability, so that the rule can be plugged into a deferred-acceptance clearinghouse, and wants monotonicity in the minority students' favour, therefore only has to choose a reserve schedule. The paper's lexicographic and stepwise-adjusted–reserves rules (§5) are built on this description.
Formalizing it has a second purpose. Theorem 1 is printed as an equivalence, but its (⇐) half is false. Take and the reserve when the top tier has at most one minority, otherwise. This satisfies B1–B3. With priorities and minorities , the rule chooses from but from , so removing the rejected student rejects , and substitutability fails. The same failure occurs in the paper's Example 1 (), and the error sits in Case 3 of the (⇐) proof on p. 23. The mission therefore poses only the (⇒) half, which planning checked by exhaustive search for every capacity and every universe of up to seven students. A machine-checked proof would settle that half for every and every universe. No formalization of this result, or of affirmative action choice rules in this model, exists on the platform or in Mathlib.
The reserve that represents has to be defined from alone. The obvious candidate, the number of affirmative-action admissions at the problem itself, is not a reserve function: it depends on how many minorities happen to sit in the bottom tier, while a reserve function may depend only on the top tier. Showing that a well-defined reserve exists already uses neutrality, substitutability and capacity-filling together (Lemma 1). The bounds of Condition B then compare reserves at problems whose top tiers differ. The monotonicity axioms give only the lower half of each bound, "the reserve does not fall"; the upper half, "the reserve rises by at most one", and the equality of B3 (ii) are not consequences of MPI or MTC and need substitutability. Small universes are a further obstacle: the paper's argument works with problems containing minority students and more than students, which a small does not contain, while the goal makes no assumption on .
Everything lives in the namespace AffirmativeChoice.Reserve, in one definitions file and seven theorems.
Problem holds S : Finset 𝒮, τ : 𝒮 → Bool (true = minority) and pri : 𝒮 → ℕ with s ≻ s' ↔ pri s < pri s', injective on S. Only values on S matter; restriction keeps τ and pri.rank ≤ q; the type of the k-th ranked student is an Option Bool, none beyond |S|.ChoiceRule 𝒮 q carries only C P ⊆ P.S, |C P| ≤ q and nonemptiness for nonempty S; the axioms are separate predicates.reserveChoice, with the majority cap .canonicalReserve, an sSup on ℕ over problems with the same top-tier type configuration. It agrees with the paper's whenever the paper's witness problem exists.Ruled out: problems encoded as type words, which quotients away neutrality; reserve functions defined only on type words; axioms built into the choice-rule structure; an existential that is not required to be a reserve function; or a reserve procedure that may admit bottom-tier majority students. Each of these would make the goal different from, or weaker than, the paper's. The (⇐) half and the full equivalence are not stated in any item.
Contributions welcome: the finite-order combinatorics of ranks, tiers and improvements, which is reusable for other priority-based choice models (reserves, quotas, slot-specific priorities); proofs of the milestones in any order; and a formal proof of the counterexample to the (⇐) half.
Sponsored-search platforms sell ad impressions through auctions in which advertisers submit both per-impression bids and a budget that caps their total spend. The platform then decides which auctions to run, subject to everybody's budget. Most auction theory treats budgets as exogenous constraints. In practice an advertiser chooses the budget, and committing capital has a cost, so budgets and bids are chosen together, strategically.
Ciocan and Iyer (SSRN 3240995; published in Operations Research, doi:10.1287/opre.2020.2052) study this joint choice. Exact equilibria of the resulting game are intractable: when budgets bind, the platform's allocation is the solution of a linear program, and an advertiser's best response depends on everybody else's budget in a complicated way. The paper shows that in large markets a simple, explicit strategy profile is an approximate equilibrium. This mission formalizes that result.
There are bidders and items . Bidder has private valuations , all independent, with . Committing a budget costs her , with . The platform earns an outside value per unit of an unallocated item.
A strategy maps to a budget and bids . Given bids , the price of item to bidder is the next lower bid,
The platform picks an allocation that is optimal for the linear program
Bidder 's spend is , her payoff is , and her modified profit is , the payoff she would get with a budget equal to her spend.
Write and , and assume . Let , let be the second highest on item , and let . The profile has bidder bid with budget
where averages over the other bidders' valuations. A profile is an -equilibrium if no bidder can raise her expected payoff above by a unilateral deviation.
There is a constant such that if and , then for every bidder and every deviation ,
so is an -equilibrium with .
The paper's own lemmas, in the order of its proof: the pathwise slack bound (Lemma 2), the dual-multiplier comparison (Lemma 4), greediness of the equilibrium allocation (Lemma 6), the key no-profitable-deviation lemma on a typical event (Lemma 3, corrected, see below), an order-statistic bound (Lemma 18), the probability of the typical event (Lemma 7), and the expected bounds on modified profit and spend (Lemmas 17, 15, 5, 16).
The theorem shows that a strategy which needs only each bidder's own distribution is an approximate equilibrium: shade each valuation by and declare a budget slightly above the expected unbudgeted spend. The error vanishes as the number of bidders grows, and Theorem 2 of the paper adds that the platform's optimal allocation under is then a per-item second-price auction with high probability. Together these justify analysing budgeted ad markets through a simple, decoupled model.
The result is proved in the paper but not machine-checked. Formalizing it means building an LP-based allocation model with measurable selections, order statistics of independent exponentials, and concentration bounds for sums over items. The formalization also records a correction: Lemma 3 as printed is false (see Formalization scope), and the corrected statement still yields Theorem 1.
The obvious route fails because a deviating bidder can change the allocation of every other bidder. If bidder overbids on an item that bidder would win, she raises 's price, and can run out of budget and leave other items for to buy cheaply. Underbidding creates a similar effect. So the deviation's effect on the market is not small, and mean-field arguments do not apply. The budgets have to absorb these effects on a typical event, while the expected cost of the unspent budget, , has to stay small next to the bidder's profit. Both requirements must hold uniformly over all deviations, including ones whose budget constraint binds, where the optimal allocation is not greedy.
The model is one Lean structure Market (sizes, rates , , the interval , ) with the standing assumptions of p. 18 in Market.Standing. Valuations are a function Fin m → Fin n → ℝ with the product law of independent exponentials. The conventions are:
No allocation rule is fixed by fiat, and none may ignore budgets: the rule must be LP-optimal for all nonnegative budgets, and the sanity check exhibits a market satisfying the standing assumptions, so the goal is neither vacuous nor provable by choosing a convenient allocation.
A complete development needs measurable selections of LP optima, LP duality and complementary slackness (both available on the platform as general theorems), order statistics of independent exponential variables, and a Bernstein-type concentration bound (available as HighDimProb.Concentration.bernstein_unweighted). The order-statistic and concentration layers are reusable beyond this mission. Contributions of the appendix lemmas (Lemmas 9, 23–26) as intermediate results are welcome.
A retail store manager does two kinds of work that the firm cannot observe directly: operational effort, which keeps shelves stocked, and marketing effort, which draws customers. The firm sees only the outcomes, namely how much inventory was available and how much was sold. Sales are the smaller of inventory and demand, so whenever the shelf runs empty the true demand is hidden. This is demand censoring, and it links the two tasks: a sales figure equal to the inventory level says little about how hard the manager worked on marketing.
T. Dai, R. Ke and C. T. Ryan (SSRN 3235866; Management Science, doi:10.1287/mnsc.2020.3651) study the principal–agent problem this creates, with a risk-neutral, limited-liability manager whose pay lies between and a cap . With the bang-bang approach of their §4, they show that an optimal plan pays either nothing or the full bonus , according to whether a weighted likelihood-ratio statistic of the observed pair (inventory, sales) clears a trigger . In the two-effort-level case, the bonus region has a distinctive mast-and-sail shape. Their §6 asks whether such a plan is monotone, meaning that more inventory or more sales never lowers the pay. A non-monotone plan invites ex post moral hazard: the manager would gain by discarding stock. The goal of this mission is the paper's answer, Proposition 5.
Inventory takes values in and demand in , with . Under low and high operational effort, inventory has densities and ; under low and high marketing effort, demand has densities and , with distribution function . Inventory and demand are independent. Each density is continuous, strictly positive on its closed support, and integrates to there. The monotone likelihood ratio property (MLRP) holds: is nonincreasing in , and is nonincreasing in .
Sales are . A compensation plan is defined on the domain . Points with are no-stockout (NSO) outcomes and points with are stockout (SO) outcomes. The firm wants both efforts high. For nonnegative weights summing to , one for each deviation, define
The plan (11) pays on the sail and on the mast , and pays elsewhere. The critical inventories are , the least with , and , the least with ; each equals when no such exists. The sail boundary is the least with .
A plan is monotone in (in ) if raising inventory (sales) within never lowers pay. It is jointly monotone if whenever both points lie in , and .
For every plan of the form (11) with :
By Proposition 3, part (ii) and part (iii) of the goal together cover every plan.
Proposition 5 shows that a mast-and-sail plan fails to be monotone in inventory exactly when the mast starts strictly below the sail. In that case a manager whose sales fall just short of the inventory level would gain by discarding the unsold units. The outcome then becomes a stockout on the mast, which earns the bonus, instead of a no-stockout point below the sail, which earns nothing. This ex post moral hazard is the paper's motivation for studying the cost of imposing monotonicity in its later sections. Propositions 1–3 describe the optimal plan's bonus region completely, and Lemma OA3 records the stochastic-order facts the analysis rests on: MLRP implies a hazard-rate ordering of the demand distributions.
The results are proved in the paper and its online appendix. No machine-checked version of any of them is known. The mission states them under the standing assumptions made explicit, about canonical thresholds rather than existential witnesses, and for every plan of the form (11) rather than only optimal ones. Under this reading Propositions 3 and 5 are slightly stronger than printed. Two printed claims need an added hypothesis to be true, and the mission states these honestly: the continuity of in Proposition 1, and the strict survival-versus-density inequality.
The goal's statement is elementary, but every step depends on joint properties of the two ratio functions on the whole domain. These are monotonicity of in both arguments, monotonicity of , continuity, and the comparison . The last of these is a hazard-rate statement about integrated tails, not a pointwise MLRP fact. The thresholds are infima of level sets, so each part of the goal requires showing that the infimum is attained, and handling the empty cases (an empty sail, an empty mast) where the thresholds default to . Joint monotonicity is strict in both coordinates, so it does not follow from the product order on .
All objects live in MastSail.Monotone. A model bundles , and the four densities as real functions, which are read only on or . Distribution functions are interval integrals from . Pairs are ordered (inventory, sales). The standing assumptions add two things to the printed model: strict positivity of the densities on the closed supports (from §4, p. 9) and (the paper has ). These ensure that every ratio has a positive denominator, so no ratio defaults to division by zero. The paper's "" is read as the least point with . The weights range over the three deviations from the target. Optimality of the plan is never assumed. Proposition 1 additionally takes strict MLRP of and ; Proposition 2 takes . The goal takes only .
The plan and the thresholds are the model's own definitions. A Proposition 5 stated for abstract regions shaped like a mast and a sail, or for thresholds supplied as hypotheses, would be set geometry and does not count. A complete development needs interval integrals, monotone level sets of continuous functions, and product measures with densities (for Lemma 1). The likelihood-ratio-to-hazard-rate comparison for densities on an interval can be reused well beyond this mission. Proofs of any milestone are welcome, as are proofs of the strict variants under weaker hypotheses.
Many sequential decision problems in operations research are learned online while the environment changes: demand responds to prices differently from week to week, click-through rates drift, and the value of an action in a recommendation or auto-loan pricing system decays as conditions move. The stochastic linear bandit is the standard model for such problems when actions are described by feature vectors. The classical algorithms for it (OFUL of Abbasi-Yadkori, Pál and Szepesvári, 2011) assume the unknown parameter is fixed, and they can incur linear regret when it drifts.
Besbes, Gur and Zeevi (2014, 2015) introduced the variation budget , a bound on the total movement of the environment over the horizon, and showed that the right benchmark is then the dynamic regret: the loss against the sequence of per-round optimal actions. Cheung, Simchi-Levi and Zhu, Hedging the Drift: Learning to Optimize under Non-Stationarity (arXiv:1903.01461v4, 2021; Management Science, doi:10.1287/mnsc.2021.4024), study the drifting linear bandit. Their SW-UCB algorithm attains the minimax rate when is known. Their Bandit-over-Bandit (BOB) algorithm needs no knowledge of : it hedges over window sizes with an adversarial bandit learner. This mission formalizes BOB's dynamic regret bound, Theorem 4 of the paper, together with the chain of results that leads to it.
A drifting linear bandit instance consists of a horizon , finite nonempty decision sets , and unknown parameters for , all fixed in advance. In round the learner picks and observes . The noises are i.i.d., centred and -sub-Gaussian: . The constants bound and , and . Assumption 1 asks that every action be a multiple of one vector of a fixed orthonormal basis. The variation constraint is
and the dynamic regret of a policy is with .
SW-UCB with window size and regularisation estimates by ridge regression on the last rounds only:
and plays with .
BOB cuts the horizon into blocks of rounds. Before each block an EXP3 learner draws an index , , and BOB restarts SW-UCB with window . The block's total reward, divided by and shifted by , is EXP3's feedback.
read as: for fixed there are such that the expected regret is at most times the bracket, for every , , , instance and noise.
Theorem 4 shows that a learner ignorant of how fast the environment drifts can still be no-regret against the moving optimum. When it matches, up to logarithmic factors, the rate of SW-UCB tuned with knowledge of , which matches the paper's minimax lower bound (Theorem 1) up to logarithmic factors. The bandit-over-bandit template, in which an adversarial bandit chooses among configurations of a base algorithm run on restarted blocks, is applied in the same paper to generalized linear and combinatorial semi-bandits, and by the same authors to non-stationary reinforcement learning.
The result is proved in the paper; nothing in this chain is machine-checked. The platform has an Exp3 regret bound and an elliptical-potential lemma, but no non-stationary bandit, no sliding-window estimator and no bandit-over-bandit result. A complete development would give a checked proof of the decomposition, of the per-block reduction to SW-UCB, and of the interaction between EXP3 and the high-probability normalisation, which the printed proof treats briefly.
The obvious argument for SW-UCB is to copy OFUL's analysis. It fails at the elliptical-potential step, because the sliding-window Gram matrices are not monotone in (old observations leave the window). Lemma 5 replaces it, and the drift bias of the estimator (Lemma 3) needs Assumption 1. Lemma 3 is false for actions in general position.
For BOB, the obvious idea is to treat each window size as an expert with bounded rewards. Block rewards are not bounded, though: they carry sub-Gaussian noise, and the normalised reward lies in only on a high-probability event (Lemma 1). EXP3's guarantee must be combined with that event. The restarts are also essential: without them a block's reward would depend on earlier EXP3 choices, and EXP3's adversary would no longer be oblivious.
Fin d → ℝ, matrices are Matrix (Fin d) (Fin d) ℝ, and rounds are numbered . The window of round for a run started at round is .A complete development needs:
The self-normalized bound, matrix-inverse monotonicity and the EXP3 bound are reusable well beyond this mission. Contributions to any milestone, and to these general lemmas, are welcome.
Retailers and platforms increasingly set prices and choose which products to display per customer, using observed customer attributes (location, device, purchase history). The decision rule is usually built in two steps: fit a choice model to historical transactions, then optimize prices and assortments as if the fitted model were the truth. Chen, Owen, Pixton and Simchi-Levi (Management Science, 2021; author manuscript SSRN 2579462) ask how much revenue this "estimate, then optimize" procedure loses, as a function of the amount and richness of the historical data. Their answer is a non-asymptotic, high-probability bound on the revenue gap for a feature-dependent multinomial logit model that covers personalized pricing and personalized assortment in one framework.
The estimation side builds on the econometrics of the conditional logit model (McFadden, 1974), whose classical theory is asymptotic. The finite-sample tools come from high-dimensional statistics: concentration of sample covariance matrices of sub-Gaussian vectors (Vershynin, 2012) and strong-convexity arguments for M-estimators.
There are products and a no-purchase option . A customer arrives with a feature vector , scaled so that . The seller offers an assortment and sets a price for each product, ; the price box is . For product the feature–price vector is .
The parameter is . The mean utility of product is . Under the multinomial logit (MNL) model the customer buys with probability
and buys nothing with probability . The expected revenue is .
The data are past transactions , where is the observed choice. The negative log-likelihood is . Given a radius with , the constrained MLE minimizes over .
Two assumptions govern the data. Assumption 1: the outcomes are conditionally independent given features and prices and follow the MNL model at the true parameter , and for each the vectors are independent across (not necessarily identically distributed) and sub-Gaussian with norm at most . Assumption 2: every product was offered in at least transactions, and the averaged second-moment matrix over the transactions offering has smallest eigenvalue at least .
Given a family of feasible assortments, maximizes over (the oracle decision) and maximizes .
For every there is , and for every a constant , such that whenever , with probability at least , for every feature vector ,
The constants are unspecified, as on the page; only their dependence is fixed.
The result. The theorem quantifies the value of historical data for personalized revenue management. The loss shrinks as and degrades with (products rarely offered in the past) and (features and prices that are nearly collinear in the data). This makes precise two practical warnings of the paper: price experimentation must not be correlated with customer features, and every product must have been explored. The bound is uniform over customers, so it is an out-of-sample guarantee. It specializes to customized pricing (Corollary 1) and to personalized assortment with fixed prices (Corollary 2), and the parameter rate of Theorem 1 matches the Cramér–Rao rate up to logarithmic factors.
Formalizing it. The paper's results are proved but none has been machine-checked. A formal development would produce a verified finite-sample theory of the constrained logit MLE: the softmax Hessian bound, strong convexity of the log-likelihood with high probability, the gradient concentration, and the transfer to revenue. Two printed statements need care, and the mission states the corrected forms: Lemma 2 needs an additional sample-size condition (see Formalization scope), and the printed (5) loses a factor relative to what Theorem 1 uses.
The deterministic parts (Lemma EC.1, the constant , the Lipschitz bound, the step (4)–(5)) are finite-dimensional calculus. The main obstacle is Lemma 2. Its proof needs the empirical second-moment matrices to be within of their expectations in operator norm, for independent but non-identically distributed sub-Gaussian vectors, with a sample size depending on only through a constant. The standard references state this for identically distributed vectors. Mathlib has no matrix concentration of this kind, and an -net argument with a Bernstein-type bound must be built. A second obstacle is the randomness of the decision itself: the optimal decisions are argmax selections, so the bad event is controlled through Theorem 1's event and not through measurability of the decision.
A first attempt often tries to bound the gap by the parameter error directly through the optimization problem. That fails: the argmax is not Lipschitz in . The paper's route compares revenues of fixed decisions, which needs the bound of Proposition 1 uniformly over all decisions.
The model is one definitions file in the namespace PersonalizedRM.RevenueGap. The parameter is EuclideanSpace ℝ (Fin J × Fin (d+1)), so ‖θ‖ is the Euclidean norm; is an explicit sum and is a bound on every fderiv partial derivative. Outcomes are Option (Fin J) (none is no purchase). Historical assortments are deterministic. The conventions committed to are:
Theorem 1, Proposition 1 and Theorem 2 are stated exactly as printed.
Constant order. The constants are quantified in the order , before , , , , and the data. A constant chosen after the data could be made large enough that the right-hand side exceeds the trivial bounds (revenue gap , parameter error ), and the statements would be empty.
Infrastructure. A complete development needs:
The concentration bound and the softmax Hessian bound are reusable beyond this mission. Contributions to any milestone are welcome, as are proofs of the generic lemmas as separate theorems.
Not formalized: Corollaries 1–2 (specializations of the goal), Proposition 2 (the mixing-data rate, stated only up to ), and the numerical study of §5.
In a contextual bandit, a decision maker repeatedly observes the features of an individual (a patient, a customer, a user), chooses one of several actions, and sees the reward of the chosen action only. Applications include personalized medicine, dynamic pricing and ad placement. The standard algorithms (upper-confidence-bound and Thompson-sampling methods, or forced-sampling schemes such as the OLS Bandit of Goldenshluger and Zeevi, 2013) deliberately explore: they sometimes take actions that look suboptimal in order to learn. In many of these applications exploration is costly or ethically constrained, and practitioners often run the greedy policy instead, which always takes the action that looks best under current estimates.
Bastani, Bayati and Khosravi (arXiv:1704.09011, Management Science 2021) ask when the greedy policy is nonetheless rate optimal. Their answer is a condition on the context distribution, covariate diversity, under which the natural randomness of the contexts does the exploring. For two arms they prove that the greedy algorithm then has logarithmic cumulative regret, which matches the lower bound of Goldenshluger and Zeevi (2013) for this problem.
There are two arms with unknown parameters . At times a context arrives; the contexts are i.i.d. with law . Pulling arm yields the reward , with independent mean-zero noise satisfying for all real (-sub-Gaussian).
The Greedy Bandit (Algorithm 1) keeps, for each arm, the set of times at which it was pulled, the sample covariance and the ordinary least squares estimate (and while is singular). At time it pulls , breaking ties with a fair coin . Its instantaneous expected regret and cumulative expected regret are
The assumptions are:
With and , for and every ,
The theorem shows that, under covariate diversity, exploration is unnecessary for the two-armed linear contextual bandit: the greedy policy achieves the optimal rate. It explains the good empirical performance of greedy policies reported in practice, and it underlies the paper's Greedy-First algorithm, which runs greedily and switches to exploration only when the data show that covariate diversity fails. The two concentration tools (Lemmas 8 and 9) are standard and reusable well beyond this paper; Lemma 5 is a reusable least-squares bound for adaptively collected data.
The result is proved in the paper. As far as is known, none of it is formalized: the mission produces a machine-checked proof of the regret bound with explicit constants, and of the adapted matrix Chernoff inequality, which is not in Mathlib. Note that the printed display (3) multiplies the constant term by , a factor the proof does not produce; the goal states the bound the proof establishes.
The samples of each arm are chosen by the algorithm from its own past estimates, so they are neither independent nor identically distributed, and classical least-squares consistency results do not apply. The obvious argument, "each arm is chosen with positive probability, hence is sampled linearly often, hence its estimate converges", fails at the second step: being sampled often does not make the sample covariance well conditioned, because the chosen contexts all lie in the half-space where that arm currently looks best. Covariate diversity is exactly what makes the conditional covariance of such a half-space well conditioned, and transferring this to the sample covariance requires a matrix concentration inequality for martingales. The regret bound then needs a peeling argument against the margin condition, with the constants tracked explicitly.
Fin d → ℝ; every norm is the Euclidean norm (Lean's default norm on this type is the sup norm and is not used). and are the infimum and supremum of over unit vectors.Fin 2; times start at . Contexts, noises and tie-breaking coins live on one probability space and are mutually independent; the context law is any probability measure (the paper's Lebesgue density is not used by the proof). Noise sub-Gaussianity is two-sided (Mathlib's HasSubgaussianMGF): the paper's one-sided Definition 1 does not force mean zero, and the theorem would be false without it.A buyer with a fixed budget wants to hire a team from a pool of sellers, each of whom knows privately what participating would cost them. The buyer values teams through a set function and pays each hired seller. The sellers are strategic: they report whatever cost serves them best. A budget-feasible mechanism decides whom to hire and what to pay so that reporting the true cost is optimal for every seller, nobody is paid less than their reported cost, and the total payment never exceeds the budget. The model was introduced by Singer (FOCS 2010). It describes crowdsourcing marketplaces that recruit workers under a fixed task budget, and influence-maximization campaigns that recruit seed users of a social network.
Budget feasibility is what separates the model from classical mechanism design. The truthful VCG mechanism pays far more than any fixed budget. The question is how much value is lost when the payment rule must be truthful and stay within the budget.
Timeline (as surveyed in arXiv:1905.00848v2, pp. 2–5):
For general non-monotone submodular valuations no budget-feasible -approximation mechanism was known before Amanatidis, Kleer and Schäfer (arXiv 2019; Mathematics of Operations Research, 2022). Their offline result is the subject of this mission. The obstacle is that the payments of Singer-style greedy mechanisms can be unbounded once is not monotone.
There is a finite set of agents. Agent has a private cost , where is the budget. The valuation is normalized (), non-negative and submodular: . It need not be monotone. The marginal value of with respect to is . The benchmark is
A deterministic mechanism consists of an outcome rule , which maps declared costs to a set of winners, and a payment rule. Throughout, payments are threshold payments: a winner is paid the largest bid with which it would still win, and a loser is paid nothing. A mechanism is truthful if declaring maximizes each agent's utility (payment minus cost if it wins, otherwise) whatever the others declare. It is individually rational if winners are paid at least their bids, and budget-feasible if the payments sum to at most . A randomized mechanism is universally truthful if it is a probability distribution over deterministic mechanisms that are all truthful.
Simultaneous Greedy grows two candidate solutions with separate budgets . It repeatedly takes the agent–solution pair of largest positive marginal value and offers the take-it-or-leave-it price . If accepts and the price fits into , it joins ; either way it is removed from the pool. The output is the best of and two unconstrained 2-approximate improvements . Sample-then-Greedy splits uniformly at random into , estimates with an -approximation for the knapsack problem on , and runs Simultaneous Greedy on with . GenSm-Main hires the single most valuable agent with probability and runs Sample-then-Greedy otherwise.
GenSm-Main is universally truthful, individually rational and budget-feasible, and for every cost vector the returned set satisfies
The goal is the paper's headline, stated about the mechanism as constructed. Every algorithmic ingredient (the greedy run, the posted prices, the sampling, the threshold payments, the expectation) is defined explicitly. The subroutines , and the tie-breaking rule are left general and enter only through the guarantees the paper uses.
In attack order: Definition 2.1 (three equivalent forms of submodularity); Lemma 2.4 (Myerson: monotone rules with threshold payments are truthful and individually rational); Lemma 3.3 (Simultaneous Greedy is monotone); Lemma 3.4 (Simultaneous Greedy is budget-feasible); Corollary 3.5 (the incentive half of the goal); Lemma 3.6 ( when no agent is worth ); Lemma 3.7 (a random halving keeps a fraction on both sides with probability ); Lemma 3.8 (Sample-then-Greedy's guarantee with probability ); Corollary 3.9 (the approximation half of the goal).
The result. Theorem 3.1 gave the first polynomial-time, constant-factor, budget-feasible mechanism for non-monotone submodular objectives. The posted-price structure of Simultaneous Greedy reduces budget feasibility to a bookkeeping argument and is reused in the paper's online mechanism (Section 4, the secretary model) and its extension to -system constraints (Section 5). Before it, constant-factor guarantees for non-monotone objectives were limited to special classes (cut functions, symmetric submodular functions).
Formalizing it. The result is proved on paper; nothing in it has been machine-checked. The mission produces a checked model of single-parameter procurement mechanisms with threshold payments, a checked form of Myerson's lemma in the procurement convention, and a checked analysis of a greedy algorithm whose two candidate solutions interact through a shared pool. The random-partition lemma (Lemma 3.7), which the paper cites without proof, has to be proved from scratch. The constant 505 is tight to the paper's own arithmetic: with and the chain of bounds gives .
Two steps resist the obvious argument. First, the threshold payment of a winner in Simultaneous Greedy has to be identified with the posted price it accepted. This requires showing that raising one's bid up to that price, or lowering it, changes nothing else in a run whose order of examination depends on marginal values only. Second, the approximation analysis of the case in which some agent is rejected for lack of budget (Lemma 3.6, Case 1) and the case in which every rejection is for price (Case 2) uses three different forms of submodularity together with the non-monotonicity of : adding agents can lower the value, so the usual greedy charging argument fails, and both candidate solutions are needed. Lemma 3.7 is a concentration statement for submodular functions under a uniform random split, cited from earlier work, and must be proved for non-monotone .
Agents form a finite type with decidable equality, sets are Finsets, and values and costs are real numbers (the paper uses ). Submodularity is the published lattice definition NonmonotoneSubmod.Shared.Submodular. The model commits to the following conventions:
Three hypotheses make the paper's implicit assumptions explicit. is deterministic, as in the printed proof (footnote 3 and Remark 3.10 explain that a randomized gives ). is cost-local: it reads only the costs of . The tie-breaking rule sees only the pool and the two partial solutions (Remark 2.6). Exact optimizers satisfy all three, so none is vacuous. The polynomial running time is not formalized.
A trivializing formalization is ruled out by the statement: the goal is about genSmMain as defined, with payments computed from its outcome rule, truthfulness against every misreport in , and the expectation over the explicit randomness. It is not the existence of some mechanism, and not truthfulness against a fixed bid.
Contributions welcome: proofs of Myerson's lemma and Lemma 3.7 are reusable beyond this mission, as is any general library of threshold-payment mechanisms. The online mechanism (Theorem 4.1), the -system result (Theorem 5.2) and the lower bounds of Section 6 are not part of this mission.
Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first positions, with random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position also sees positions ) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.
The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.
There are items. Item has a price and an MNL preference weight ; write and, for an assortment ,
the expected revenue of offering to an MNL customer with a no-purchase option of weight . An assignment is a bijection from positions to items; is the set of items in positions , , and with position weights the objective is
The algorithm fixes an accuracy and a guessed position . A sequence of dynamic-programming actions consists of events and pairs of item sets (a sub-assortment and a super-assortment), starting from , and ending at , . Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness , the accuracy bounds and the same for , a cardinality constraint linking sets to events, and three growth conditions on the proxies
depending on the position of relative to . With the last index whose event is at most , the actions are rounded into blocks of new items (from before , from after), and the rounded assignment lists the blocks in order, each by non-increasing price. The block boundaries are , and are the position intervals between consecutive boundaries, split at .
For every , every feasible action sequence and every rounded assignment ,
with . This is inequality (15) of the paper combined with (16), in the proof of Lemma 5.4.
The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.
The remaining half of the paper's argument is not true as printed. Lemma 5.4, , and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with , , , and , no feasible action sequence can place item 2 first, and every rounded assignment earns at most against an optimum of . A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.
The rounding discards items. Before , block keeps only the part of the sub-assortment that is new with respect to , so the prefix of can carry less -mass than . A loss bounded by the per-step accuracy would accumulate over up to steps; Lemma 5.2's constant is independent of , and holds only because the growth constraint forces to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.
Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position to the item at position . A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention , and . Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by , non-increasing prices within a block, ties in any order.
Conventions and additions relative to the page:
Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance (, ) satisfying all hypotheses at once.
The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.
Random utility models are the standard way to turn utilities into demand in operations management, marketing and economics. A consumer facing products assigns each a random utility and buys the one with the highest realization; the choice probabilities are the market shares that pricing and assortment models optimize. The multinomial logit, built on i.i.d. Gumbel errors, has closed-form choice probabilities, but its errors have the same variance for every product, and this forces the independence-of-irrelevant-alternatives property.
Alptekinoğlu and Semple (SSRN 3232788, forthcoming in Operations Research) replace the Gumbel errors by exponential errors with a product-specific rate. Uncertainty about a product's value can then differ across products, for example between a familiar brand and a new entrant. Their earlier exponomial choice model (Alptekinoğlu & Semple, Operations Research 64(1), 2016) is the special case of equal rates. The paper's first result is that this heteroscedastic model still has choice probabilities in closed form, a finite combination of exponentials of linear functions of the utilities. Its pricing analysis rests on that formula.
There are choices, . Choice gives the random utility
where is the ideal utility of choice and is an exponential random variable with error rate , with density and distribution function for (both for ). The errors are independent, and they are not identically distributed. Since , the ideal utility is the largest utility choice can ever deliver.
The choice probability of choice is
Write and for the choices that are better and strictly better than , and for the strictly worse ones. Let and . The exponomial term of choice is
The proof also uses the distinct values of , and the sets .
For every ,
The statement holds for arbitrary real utilities, ties included, and arbitrary positive rates.
The result. Theorem 1 makes the HEC model usable. Every later result of the paper starts from (3): the continuity and the partial derivatives of (Theorem 2), the expected consumer surplus (Theorem 3), log-concavity (Theorem 5), and the monopoly and oligopoly pricing results. Unlike the multinomial logit, the closed form shows how the rate of each worse product enters through , so substitution patterns are not proportional. With equal utilities it reduces to , and with equal rates it gives the exponomial model of 2016.
Formalizing it. The theorem is proved in the paper. The proof in Appendix C is short and leaves the integration steps to the reader. No machine-checked proof of the theorem or of any step of its proof is known. The mission asks for a complete Lean proof that starts from the probability itself, a product of exponential laws, so that the integral representation (1) is part of what is proved and not assumed. It also produces general facts about the maximum of independent shifted exponential variables, which have uses beyond this paper.
The obvious argument has two steps, and both hide work. Step one conditions on and integrates the product of survival functions. In Lean this is a computation of a product measure of a non-rectangular set, a Fubini argument over with the marginal of one coordinate split off. Step two integrates a function whose exponent is piecewise linear with breakpoints at the gaps . The breakpoints coincide when utilities tie, and the formula is stated through the distinct levels precisely to handle that. Regrouping the telescoping display (16) by level, and identifying each regrouped term with the strictly worse choices at that level, is bookkeeping over a sorted enumeration of a finite set. It is easy on paper and has to be done with care in Lean.
Choices are Fin n. The errors are the coordinates of a point of Fin n → ℝ under Measure.pi (fun j => expMeasure (lam j)), Mathlib's product of exponential laws. is the real value of this measure on the closed event , with the weak inequality as printed. All values are real. Every statement assumes and , the standing assumptions of p. 4. Integrals are Bochner integrals over . is defined for every , with value at a choice of maximal utility, where the paper leaves it undefined; the theorems use it only for , where it is at least . The levels are the increasing enumeration of the set of values of , indexed from in Lean.
is defined as a probability. It is neither the integral (1) nor the closed form (3), either of which would make the goal a computation or a tautology.
A complete development needs the product-measure computation behind (1) and the exponential integral . It also needs facts about sorted enumerations of finite sets of reals. The first two are reusable for any model with independent exponential errors. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 that bypass them.
Not in scope: Corollary 1, Theorems 2–14 and the pricing results, which build on Theorem 1.
Large-scale learning problems, such as empirical risk minimization over millions of samples, are solved in practice by stochastic gradient descent (SGD) run on many processors at once. In a master–worker system, or in a multi-processor system with shared memory, a worker reads the current parameter, computes a stochastic gradient and writes its update back. Other workers update the parameter in the meantime, so by the time a gradient is applied it is stale: it was evaluated at an older iterate. In heterogeneous clusters these delays are not bounded in any useful sense, and they can grow with the run.
The classical analyses of asynchronous gradient methods (Bertsekas and Tsitsiklis, Parallel and Distributed Computation, Prentice Hall 1989, reprinted by Athena Scientific 1997) and of asynchronous SGD for machine learning (Agarwal and Duchi, NeurIPS 2011; Recht et al., Hogwild!, NeurIPS 2011; Lian et al., NeurIPS 2015) assume bounded delays. Zhou, Mertikopoulos, Bambos, Glynn and Ye (arXiv:2107.02919, Mathematics of Operations Research, 2022) show that the delays may grow without bound, polynomially in the iteration count, as long as the step size shrinks to match. This mission formalizes their first main result, Theorem 1, on general nonconvex objectives.
Let be a probability space and a random function. The objective is
to be minimized over . Write for the gradient of in .
Assumption 1 asks that be differentiable for -almost every , that the stochastic gradient have bounded second moment, , and that its mean be -Lipschitz.
Distributed asynchronous SGD (DASGD, Algorithm 3 of the paper) starts at and updates
where are step sizes, is an i.i.d. sequence with law , and is the iteration at which the gradient applied at step was requested. Its delay is .
Assumption 2 couples delays and step sizes. It requires one of four regimes:
If Assumptions 1 and 2 hold and , then
The goal covers all four regimes at once, through the disjunction in Assumption 2. It fixes no constant: , and the regime's parameters are arbitrary.
The result. For a general nonconvex smooth objective, convergence to a minimizer cannot be expected. The standard guarantee is that the gradient vanishes, and Theorem 1 gives it in mean square, which also implies convergence in probability of to zero. The theorem shows that asynchronous SGD stays stable under delays that grow without bound, and it identifies the price: each step up in delay growth costs a logarithmic factor in the step size. A step size of order is, up to a factor, sufficient for every polynomial delay process. The guarantee does not depend on whether the architecture is master–worker or shared-memory, since only enters.
Formalizing it. The paper proves the result, but no machine-checked version of any asynchronous or delayed SGD guarantee exists on Prove2Me or in Mathlib. A formal proof would check the step most prone to error in such analyses: the conditioning that makes a stale stochastic gradient unbiased given the past. The page's own chain before (B.5) has a constant slip ( where belongs), which the printed (B.5) absorbs. The delay-sum estimates (B.8)–(B.10) are asymptotic computations with logarithms, and the paper states them with "". The reusable parts are the differentiation-under-the-integral lemma (Remark 1) and the series lemma A.4.
Without delays, the descent inequality telescopes directly: the cross term has zero conditional mean. With delays, the gradient is unbiased for , not for . The discrepancy has to be paid for out of the step sizes accumulated over the delay window. When the window grows polynomially, it is a sum over polynomially many past steps, and finiteness of the total penalty depends on the precise step-size law. A cruder bound that ignores the logarithmic factors fails in regimes 3 and 4.
A second obstacle is that a finite weighted sum gives only a . The paper's own counterexamples (p. 10) show that it does not imply convergence. The increment bound of Lemma 2 is what closes the gap.
EuclideanSpace ℝ (Fin d), and is Mathlib's gradient. gradient returns at points of non-differentiability, so the goal also asserts that is differentiable.A Lean integral of a non-integrable function is , and gradient is where is not differentiable. Those conjuncts are there so that the goal cannot be proved through either junk value. The goal is also stated for all four regimes, with the delay inside the recursion, so it is not the classical bounded-delay theorem.
A complete development needs:
Contributions of the real-analysis milestones (Lemma A.4, the delay sums) are welcome independently of the probabilistic ones.
Many decision problems in operations research and machine learning ask to minimize an expected cost subject to constraints that also hold only in expectation: a portfolio with a bound on expected shortfall, a resource allocation whose expected load must stay below capacity, a classifier with an expected fairness constraint. The expectations are integrals over a distribution that can only be sampled, so the problem cannot be solved by evaluating it exactly. Stochastic approximation methods process one sample at a time and are judged by how fast their cumulative cost and cumulative constraint violation grow with the number of samples.
For constraints in expectation, the approach that has been analysed most is the primal–dual subgradient method with a drift-plus-penalty multiplier update (Yu, Neely and Wei, NeurIPS 2017, arXiv:1708.03741), which gives expected regret and constraint violation. Zhang, Zhang and Wu (arXiv:1907.12226v3, 2020) replace the gradient step by a proximal method of multipliers in the sense of Rockafellar (Math. Oper. Res. 1976): each iteration minimizes a sampled augmented Lagrangian plus a proximal term over the feasible set. They show that this method, PMMSopt, attains the same rates.
Let be a measurable space, a nonempty closed convex set and an open bounded convex set. Let and be jointly measurable, with and each continuous and convex on . For the law of a random sample , set and . The expectation-constrained problem (1.1) is
with feasible set .
The assumptions are as follows.
Write for the componentwise positive part of . The augmented Lagrangian at the sample is
PMMSopt starts from and . For it sets
The iterates depend only on .
Take and , with and . Then for every and every feasible ,
The constants are and , where is built from the explicit of (3.1). These are the two bounds of the paper's contribution (1). Each half is also a milestone on its own.
The milestones follow the paper's proof chain.
Pathwise lemmas. These hold on every sample path.
Probabilistic lemmas.
The bounds say that, with samples and step parameters tuned to , PMMSopt has average constraint violation and average objective regret against every feasible point, under assumptions that only bound the data and its subgradients. The constraint bound needs Slater's condition; the regret bound does not. The same chain of lemmas feeds the paper's high-probability results in §4, which this mission does not cover.
The paper proves these results; none of them had a machine-checked proof. Formalizing them also fixes several slips in the printed constants. As printed, Lemma 2.4's bound (2.7) is false: a one-step counterexample is recorded on the item. Corollary 2.1 inherits that error. The constant of Theorem 3.1 is not what its proof gives, both because of the inherited factor and because can exceed . The mission states the corrected versions under which the printed proofs go through. The drift lemma (Lemma 2.7) is quoted by the paper without proof, so formalizing it is self-contained new work. It applies to drift analysis well beyond this algorithm.
The pathwise lemmas are convex-analysis inequalities. Their main obstacle is that is not differentiable: the paper's proof of Lemma 2.3 writes , so the three-point inequality has to be derived from convexity and strong convexity alone.
The core difficulty is the expected multiplier bound. An obvious argument would iterate Lemma 2.1 and take expectations. That gives growing linearly in , hence a constraint bound of order rather than . The uniform bound on comes only from the negative drift in Lemma 2.6 combined with the drift lemma, which is an exponential-supermartingale argument in the style of Hajek. Lemma 2.6 itself needs conditional expectations with respect to the sample history, together with the independence of from . An off-by-one in the history σ-algebra breaks it.
and are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p), so norms and inner products are Euclidean. The factors depend on this. is a general measurable space, and and are assumed jointly measurable. Samples are indexed from , and the history is hist ξ t, so the paper's is hist ξ (k+1). Expectations of sums are integrals of the sums.
The run is a predicate IsRun that carries the exact argmin over of Step 1, the exact multiplier update, and the measurability of in the history (asserted on p. 4). It is not a chosen argmin, and it is not an abstraction of the run by its drift properties: a hypothesis of that kind would make Theorem 3.1 a restatement of Lemma 2.7.
The formalization makes the following changes to the paper's statements, each disclosed on its item:
Every hypothesis set is satisfiable: a sorry-free check exhibits a one-dimensional instance with a PMMSopt run. Every statement requires , so the coefficient is never the junk value. The standing hypotheses make every integrand integrable, so no bound holds because an integral defaulted to .
The development needs conditional expectation, independence and filtrations from Mathlib, plus convex-analysis facts about proximal steps. The drift lemma and the three-point inequality are reusable beyond this mission. Contributions to any milestone are welcome, in any order.
A large language model serving a multi-turn conversation re-reads the whole conversation history at every turn. The intermediate attention state of that history, the KV cache, can be stored in GPU memory and reused, so that only the uncached part of the prompt must be recomputed before the first output token appears. GPU memory is scarce, so a server must decide, after every turn, which blocks of which conversations to keep. Production systems such as vLLM (Kwon et al., 2023) use least-recently-used (LRU) eviction for this (vLLM prefix caching).
Service-level objectives for LLM inference are written in terms of tail latency: the fraction of requests whose time-to-first-token exceeds a threshold. Zhang, Li, Moallemi and Peng (arXiv:2510.15152v1, 2025) measure this by the Tail Excess Latency (TEL) of a request: the number of uncached blocks above a threshold. They propose a variant of LRU aimed at the tail and prove that its expected version is optimal in a stochastic model of conversation arrivals. This mission formalizes that optimality theorem, Theorem 2 of the paper, together with the steps of its proof.
The cache holds blocks. A request of conversation whose history has length , whose new prompt has length and of which blocks are cached pays the Tail Excess Latency
where is the latency threshold expressed in blocks.
Conversations are born at rate and die at rate . While active, conversation sends requests as a Poisson process of rate . Each prompt length is drawn from a known, possibly conversation-specific law; each response length from an arbitrary law. Caches are not shared between conversations.
Deaths are never observed, so the decision-maker keeps a belief turn-arrival rate for each conversation. The belief state is : belief rates, conversation lengths and cached blocks of the conversations that have arrived so far. Between arrivals every is multiplied by the decay factor , where is the inter-arrival time. The next request comes from conversation with probability , or from a new conversation with probability . After serving conversation with prompt and response , its rate resets to , its length grows by , and the server chooses a new cache vector subject to
The belief update is the paper's: it decays the return rate with elapsed time and does not otherwise condition on the observed silence.
Expected-Tail-Optimized LRU (ET-LRU, Definition 1) chooses
the cache that minimizes the expected TEL of the next turn under the current beliefs.
For every ET-LRU policy (any tie-break), every policy whose decisions always satisfy (9), (10) and the capacity constraint, every number of requests and every well-formed belief state ,
Milestones 2 and 6 together give the goal.
ET-LRU is myopic: it looks one turn ahead. Theorem 2 says that in this model nothing is lost by myopia over any horizon. Setting with homogeneous rates turns (8) into "keep the blocks of the most recently active conversations", so the theorem yields an optimality statement for LRU for average latency. With deterministic prompt lengths it yields the optimality of the paper's Tail-Optimized LRU. With zero prompt and response lengths after the first turn it reduces to unit-page caching (p. 9), the setting in which Belady (1966) characterized the offline optimum. The paper reports that no such optimality result for LRU under stochastic arrivals had been established before.
The result is proved in the paper; nothing in it is machine-checked. A formalization adds a checked statement of the model (arrival law, belief dynamics, constraints and objective), whose conventions are easy to get wrong in prose, and a checked version of an exchange argument that the paper gives in compressed form. The greedy implementation (Lemma 1) is an instance of separable convex resource allocation and is reusable on its own.
The obvious argument compares ET-LRU's decision with another feasible decision and charges the difference to the next turn alone. That fails: a cache choice changes the state from which every later decision is made, and a cheaper next turn could in principle leave a worse state. The proof must show that the ranking of conversations by is consistent with the optimal cost-to-go at every later stage, under every possible next arrival, including arrivals that refill a conversation's cache and arrivals of new conversations. Ties in the ranking require care: two evictions of equal current score can have different future costs.
The invariant (a belief rate never exceeds the rate a conversation resets to) holds on every reachable state and is needed: exact dynamic-programming computations find states with from which ET-LRU is not optimal.
Everything lives in the namespace TailOptCaching.ETLRU, in one definitions file and eight theorem files.
ℝ≥0∞; is ENNReal.ofReal z; expectations over prompt and response lengths (laws PMF ℕ) are tsums, and the expectation over the decay factor is a lintegral. If a prompt-length law has infinite mean, every value is ; that is the correct reading, not a loophole.The goal must not be trivialized: the horizon is arbitrary (with the claim is the definition of ET-LRU), the competing policy is any admissible policy, not one of index type, the decay factor is not fixed to , and the Bellman optimum is defined independently of ET-LRU.
Not formalized here: Theorem 1 (the hindsight-optimal policy, App. A), the forced-caching variant (App. C) and the experiments. Contributions of proofs of any milestone are welcome. The finite-horizon Bellman machinery and the greedy allocation lemma are the parts most likely to be reused.
Many repeated interactions charge a player not only for what is played at each stage but also for changing what is played: a firm that reconfigures production, a defender that relocates patrols, a server that migrates jobs. Switching costs model this. In a zero-sum repeated game with switching costs, player 2 pays player 1 a stage payoff that depends on the current actions, plus a penalty proportional to a weight whenever player 2 changes action. A natural question is how the value of the game depends on : whether small changes in the cost weight can change the value or the optimal behavior abruptly, and whether an optimal strategy computed for one remains optimal for nearby .
Tsodikovich, Venel and Zseleva (MOR 2022) answer this for the undiscounted average payoff. Earlier work on such games (Liuzzi et al., Rass and Rainer, Schoenmakers et al.) studied static strategies, which repeat one mixed action forever; this mission concerns the value achieved by stationary strategies, which depend on the previous action of player 2.
Let be a real matrix, , and let be a real matrix with nonnegative entries and for every . Fix . At each stage player 1 (the maximizer) chooses a row and player 2 (the minimizer) chooses a column , and player 2 pays player 1
with . Both players observe the whole past history, in particular .
A behavior strategy assigns a mixed action to every finite history. Under a pair of behavior strategies the payoff is the lower limit of the expected average,
A stationary strategy (Definition 1) chooses its mixed action as a function of only, so it is a vector of mixed actions. The game has value in stationary strategies if there are stationary with for all behavior strategies . The game is a stochastic game whose state is the previous column; only player 2 controls the transitions.
The proof of the main theorem also uses a parametric one-shot game: for nonnegative and , is the one-shot zero-sum game with payoff matrix , and is its value.
For every the game has a value in stationary strategies. The function is continuous, increasing, concave, piecewise linear and eventually constant on , and if is linear on then player 2 has one strategy that is optimal for every in that interval:
As an illustration only (a numerical computation, not part of the mission), for and one finds , with a single breakpoint at .
The result. Theorem 1 describes the complete shape of the value as a function of the cost weight: no jumps, diminishing marginal effect of switching costs, finitely many regimes, and saturation at a level below the pure minimax of . The robustness clause says that, inside each linear regime, player 2 can play optimally without knowing exactly, and that optimal strategies need to change only at the finitely many breakpoints. The paper contrasts this with the value in static strategies (its Theorem 2), which is concave and increasing but in general only semialgebraic.
Formalizing it. The result is proved in the paper, but the proof leans on two cited theorems about single-controller stochastic games (Filar's existence theorem for the limiting-average criterion and the Filar–Raghavan matrix-game reduction). A formalization produces machine-checked versions of these classical results for the undiscounted, liminf-average criterion against arbitrary behavior strategies, and a general statement about parametric matrix games (Lemma 1) that is reusable outside this model. None of the statements has a machine-checked proof at present.
The obvious argument writes as a min-max of payoffs that are affine in and concludes concavity and piecewise linearity. This works for the one-shot game on pure stationary strategies, but transferring it to the repeated game is the hard step: the opponent may use any history-dependent behavior strategy, and the payoff is a lower limit of averages that need not converge. Showing that stationary strategies suffice against all behavior strategies, and that the value of the repeated game coincides with the value of the finite one-shot game, is the content of the single-controller theory. A second difficulty is the limiting behavior of the Markov chain induced by a stationary strategy of player 2, which need not be irreducible or aperiodic: its Cesàro averages converge, but the occupation frequencies depend on the initial column. Simply restricting both players to stationary strategies does not prove the theorem.
All objects are defined in SwitchCostGames.Stationary. Rows are Fin m, columns Fin n, with [NeZero m] [NeZero n]; the paper's is column 0. Stages are -based in Lean (stage s : Fin T is the paper's ). Strategies are behavior strategies on finite histories Fin t → Fin m × Fin n; the expectation over the first stages is a finite sum over histories, so no measure theory is needed. The payoff is Filter.liminf of the expected -stage average, which is a bounded sequence, so the liminf is a genuine limit inferior. The structure Game carries and ; the weight is a separate real argument and every statement assumes . Mixed actions and one-shot saddle values use the published finite zero-sum game BlottoLP.Flow.ZeroSum. "Increasing" is nondecreasing (MonotoneOn); "piecewise linear" means affine between finitely many breakpoints.
The value is a property of the repeated game: optimality is against all behavior strategies, not only stationary ones. Defining as the value of the one-shot game on pure stationary strategies, or restricting deviations to stationary strategies, would make the goal a corollary of Lemma 1 and is ruled out. The robust strategy in Theorem 1 is required to be stationary, which the paper's proof provides.
A complete development needs: von Neumann's minimax theorem for finite types, the theory of finite Markov chains (Cesàro limits of transition matrices), the reduction of a fixed-strategy problem to a one-player average-cost decision problem, and Filar's and Filar–Raghavan's single-controller theorems. The Markov-chain and single-controller layers are reusable for other average-payoff stochastic games. Contributions are welcome at every level, including proofs of Lemma 1 alone, which is independent of the repeated game.
The small-step subgradient method is the basic algorithm for minimizing a nonsmooth, nonconvex, locally Lipschitz function . It is also the scheme behind stochastic gradient training of neural networks with nonsmooth activations. From a starting point it iterates
with step sizes and . The basic question is whether a bounded run converges. For smooth , and for continuous-time subgradient flows, convergence follows from a Kurdyka–Łojasiewicz (KŁ) inequality together with tame geometry such as Whitney stratifiability (Bolte, Daniilidis, Lewis, Shiota 2007; Absil, Mahony, Andrews 2005). Whether the same hypotheses suffice for the discrete nonsmooth method was open.
R. Ríos-Zertuche (arXiv:2007.11699, published in Math. Oper. Res. 2022) is a companion to the work of Bolte, Pauwels and Ríos-Zertuche on the long-term dynamics of the subgradient method for path-differentiable functions (arXiv:2006.00098). That work proves positive results, such as slowdown near limit points and convergence of the values under the weak Sard condition. The examples paper shows that these results cannot be improved to convergence of the iterates. Its first example (Section 2) lives on and is the subject of this mission.
For a locally Lipschitz , the Clarke subdifferential is the convex envelope of all limits along sequences of points where is differentiable. The critical set is .
A subgradient sequence (Definition 1) is a sequence obeying the recursion above with positive steps , . The function is path-differentiable (Definition 2) if for every Lipschitz curve and almost every , for all . It satisfies the weak Sard condition (Definition 3) if it is constant on each connected component of . It is Whitney -stratifiable (Definition 5) if its graph in is a locally finite union of disjoint connected submanifolds. These pieces must satisfy the frontier condition and Whitney's condition A: limits of tangent spaces of a stratum contain the tangent spaces of the strata in its boundary.
The example works on . For let
and . Let be the distance to the unit circle . Let be a smooth radial bump with values in , equal to on , vanishing for and non-increasing along rays. Set and . For ,
There are , steps and a sequence such that is a bounded, non-convergent subgradient sequence of , and has all of the following properties:
This is the paper's negative answer to its question Q9, combined with its remarks in Q1 and Q12. The witness is left existential.
The milestones are the properties of the explicit witness (4):
The example is a counterexample: the standard toolbox of tame geometry plus a KŁ inequality does not give convergence of the discrete small-step subgradient method, even with a uniform gradient lower bound away from the critical set and the weak Sard condition. In continuous time the same hypotheses give convergence. The gap therefore comes from discretization. Any convergence proof for nonsmooth subgradient methods needs further structure, such as definability in an o-minimal structure or a stronger KŁ inequality near the critical set. Q12 adds that requiring the iterates to stay in the full-measure set of differentiability points does not help.
The result is proved in the paper; to our knowledge none of it is formalized. Formalizing it gives the first machine-checked Clarke-subdifferential, path-differentiability and Whitney-stratification counterexample. It also gives reusable estimates for an explicit sequence spiralling onto a circle.
Most of the steps are explicit estimates, but three of them are delicate.
Everything lives in EuclideanSpace ℝ (Fin n). The definitions follow these conventions:
ShorNonsmooth.AlmostDiff.almostGradients, which uses cluster points of the gradients rather than limits; the two sets are the same.ProjLikeRetr.Retractor.IsSubmanifold) for every . Tangent spaces are spans of tangent cones, and Grassmannian convergence is convergence of the subspace gap to .BumpProfile with exactly the properties listed on p. 6, and the series in (4) are tsums. The indices , where and in Lean, are never used.Four statements are adjusted, and each adjustment is disclosed in its item:
gradient is at non-differentiable points.The goal cannot be met trivially. Boundedness of the sequence and the conditions , are part of it, and they rule out an affine . Every regularity property is a separate conjunct. Contributions that develop the geometry of Whitney stratifications and path differentiability in Lean are reusable well beyond this example.
Medicare Advantage (MA) is the program in which the U.S. Centers for Medicare & Medicaid Services (CMS) pays private health plans a fixed amount per enrolled beneficiary, a capitation rate, instead of paying providers per service as in Traditional Medicare (TM). Capitation invites risk selection: a plan that receives a fixed payment per patient profits by attracting patients who cost less than their payment and deterring the others. The standard remedy is risk adjustment, which scales each patient's capitation rate by a predicted cost computed from diagnoses and demographics (the CMS-HCC model).
The literature has largely attributed residual risk selection to imperfect risk adjustment: if the predicted cost of a patient type differs from its true expected cost, plans exploit the gap (Glazer & McGuire 2000; Brown et al. 2014). This suggests that better data, "big data", would eventually close the loophole. She, Ayer and Montanera (SSRN 3556992, Manufacturing & Service Operations Management, 2022) ask whether this is true. Their first main result, the goal of this mission, says it is not: even when every patient type is paid exactly its expected cost under Traditional Medicare, the health plan's profit-maximizing quality differs from the quality CMS targets.
There is a finite set of services and a finite set of patient types. A quality vector is , with restricted to the feasible interval , where is a regulatory minimum.
and CMS pays , where is the targeted quality, with .
the expected TM payment for a type- enrollee at the target.
over the box . The program meets its Targeted Quality Benchmark (11) if the maximizer is .
Under the standing assumptions, with at least one patient type and a nonempty black-swan set, problem (9) with the rates (7) has a unique solution , and
The theorem separates two causes of risk selection. Informationally perfect risk adjustment removes mispricing of patient types, yet the plan still under-provides black-swan services: the plan's revenue is tied to enrollment, which responds to the quality of an expensive service less than the demand for that service does (assumption (6)), while the cost of quality is the same as in TM. The paper builds on this in Theorem 2 (two distinct causes of risk selection) and Theorem 3 (indirectly contracting on quality through a constraint restores the target under informationally perfect risk adjustment); both rest on the equilibrium characterization formalized here. The model is a smooth concave program over a box, so the result is an exact statement about a well-defined optimization problem rather than a heuristic.
The result is proved in the paper, in an appendix proof of about one page. It has not been formalized. This mission produces a machine-checked version of the model, of the first-order characterization of the plan's optimum (Proposition 1), and of the kernel argument, with every hypothesis the printed proofs use made explicit.
The argument has two delicate points. First, the equilibrium is defined by a constrained maximization, so the first-order condition at the target is an equality only for interior coordinates; at it is an inequality, and the "only if" direction of Proposition 1 needs , while Theorem 1 does not. Second, the comparison requires both the sum bound and the nonnegativity of the kernel entries and of the rates; the printed proof states a strict inequality where only a weak one holds, and the strict conclusion comes from the black-swan condition instead. Uniqueness of the equilibrium needs strict concavity of the profit, which in turn needs nonnegative rates.
Services and patient types are finite types (Fintype), with Nonempty I assumed where the maximum over types appears. All quantities are real numbers. A model is a structure carrying , , , the slope , and ; a predicate Standing collects the standing assumptions. Functions are on all of (resp. ); monotonicity, concavity and convexity hold on the feasible box. Partial derivatives are Fréchet derivatives applied to unit vectors. "Nondecreasing in each " is monotonicity for the product order on the box. Equilibrium means a maximizer of (10) on the box.
Added relative to the page: on the box; and (divisions in (7), (3) and ); in Proposition 1 and in the large-rate milestone; in the characterization only. Lemma 1's lower-boundary case (4) is stated with in the "if" direction and in its converse (at the multiplier is ).
The prices and rates are computed by (3) and (7) from the model; they are never free parameters, since with free rates the goal is false (take rates satisfying (12)). The goal asserts existence and uniqueness of the equilibrium, so it cannot hold vacuously; a verified instance with two services and two patient types satisfies every hypothesis.
Needed infrastructure: existence of maximizers of continuous functions on compact boxes, uniqueness under strict concavity, and first-order conditions for differentiable concave functions on a box. These are general facts about optimization over boxes and are reusable well beyond this mission. Proofs of the milestones, and of general box-constrained optimality lemmas, are welcome.
Ride-pooling platforms receive trip requests one at a time and must decide, within a short waiting window, which requests to group into a shared vehicle. A request that is not grouped before its window closes is served alone or lost. Online hypergraph matching with delays is the combinatorial core of this decision: requests are vertices that arrive over time, feasible groups of up to riders are weighted hyperedges, and the platform must commit irrevocably to disjoint groups while every member of a group is still waiting. Pavone, Saberi, Schiffer and Tsao (arXiv:2009.12022, 2020; journal version Technical Note — Online Hypergraph Matching with Delays, Operations Research, 2022) determine the optimal competitive ratio of this problem in the utility-maximization setting. For no online algorithm beats ratio , where is the waiting time (their Theorem 1, via the adversarial secretary problem), and their Theorem 3 achieves with a polynomial-time algorithm for every fixed . This mission formalizes the achievability half.
Requests arrive one per time step; request arrives at time and disappears at time . A hyperedge is a non-empty set of requests, its diameter is , and each hyperedge carries a weight . A shareability hypergraph with parameters is a finite edge set of subsets of with and for all (Definition 1, p. 2). A matching is a set of pairwise disjoint hyperedges, of weight . In Online-(k, d)-Max-Matching (Definition 2, p. 3) a hyperedge may be chosen only after all its vertices have arrived and before any of them disappears, and choices are irrevocable.
Greedy (Algorithm 5, p. 15) scans a finite edge set in non-increasing order of weight, ties broken arbitrarily, and keeps every edge disjoint from those already kept.
Randomized-Batching (Algorithm 1, p. 5) draws a shift uniformly from and cuts time into windows
with batch edges and . At the end of each window it runs an offline subroutine on the batch and commits the result ; the output is .
Depth-k Greedy (Algorithm 2, p. 7) is the subroutine. With and the first and last vertices of the batch, it enumerates the restricted matchings (Definition 18, p. 19), the matchings whose every edge meets both and ; it extends each by Greedy on the edges avoiding the vertices of , and it returns the heaviest extension.
For every shift , is a matching of whose edges each lie inside one window, and for every matching of
The statement holds for every weight-sorted tie-breaking of Greedy.
With and :
Theorem 3 closes the gap left by the general guarantee of Theorem 2 and Lemma 2 (p. 6), under which any -competitive offline subroutine yields ratio . With plain Greedy this gives only (Corollary 1, p. 7), and an exact subroutine gives but is NP-hard for . Together with the upper bound of Theorem 1, Theorem 3 settles the optimal competitive ratio of Online-(k, d)-Max-Matching for and shows that it is attained in polynomial time for each fixed . The batching-plus-restricted-enumeration pattern applies to other online problems in which items have a bounded lifetime.
The result is proved in the paper. To our knowledge none of it is machine-checked: no hypergraph matching model, no Greedy guarantee for weighted -set packing, and no batching argument exists on the platform. Lemma 4, the classical guarantee of Greedy for weighted rank- hypergraph matching, is cited in the paper without proof ([6, 8]); its formalization is reusable on its own.
The natural attempt is to run Greedy inside each batch. It loses the factor on every edge, and the random shift recovers that factor only for edges that survive batching for at least of the shifts, that is, edges of diameter at most . A long edge, with diameter above , lies in for fewer than shifts, so its loss is never compensated and the bound degrades to . Long edges therefore have to be recovered exactly in every batch. The exact optimum is intractable, so a different handle on long edges is needed. The formal work also has to deal with windows truncated at the ends of , with the first partial window, and with arbitrary tie-breaking inside Greedy.
Vertices are natural numbers and ; hyperedges are Finset ℕ, edge sets are Finset (Finset ℕ), and weights are a function Finset ℕ → ℝ, read only on . The definitions file HyperMatchDelay.Batching.Model fixes these conventions:
The running-time clauses of Theorem 3 and Lemma 4 are not formalized, since there is no cost model. The goal does not assume condition (3) as a hypothesis, and its subroutine is Depth-k Greedy as defined, with Greedy inside it. A single batch containing all of , or an exact offline subroutine, would make the statement a different and easier claim, and the formalization rules both out.
Contributions are welcome on every milestone. Lemma 4 and Observation 1 are independent of the rest. Lemma 4 is the most reusable item: a general Greedy guarantee for weighted set packing.
Double auctions match buy and sell orders at a common price. Stock exchanges, commodity markets and electricity markets use them at their opening and closing auctions and to trade multi-asset portfolios. Economists have long asked how efficient the resulting allocations are. Laboratory work starting with Smith (1962) found that repeated double auctions with few traders reach competitive outcomes quickly (Smith 1962). Since then the phenomenon has been documented in many experimental studies, but it had remained largely unexplained by theory (Pennanen, §1).
Pennanen (arXiv:2001.02071v2, Mathematics of Operations Research 2022) takes agents who bid their indifference prices in a multi-asset double auction, and shows that repeating the auction drives the economy to an efficient allocation. The total surplus left on the table decays like .
A finite nonempty set of agents trades a finite set of assets. Agent holds a portfolio , and an allocation is . Short positions are allowed and there is no free disposal. Agent has a utility with effective domain . All prices are quoted in a numeraire portfolio , for example cash.
Assumption 1 holds throughout: each is upper semicontinuous and concave (its hypograph is convex), and for and .
At the endowment , agent bids the indifference price
the most the agent would pay for without losing utility. The auctioneer solves the market clearing problem
whose optimum value is the total consumer surplus available at . A market clearing price is a vector that is a supergradient of every at a solution . Agent then receives and pays units of . An allocation with is a double auction equilibrium.
In the repeated auction the agents re-bid from their new positions:
where and clear the -th auction, whose indifference prices are built from .
Two further conditions are used. Assumption 3: no nonzero with has every a direction of recession of . Assumption 5: for every there is with on the ball . Assumption 4, which is needed only for Pareto efficiency, says that an agent who is not at the lowest possible utility can give away a little of and stay in .
Under Assumptions 1, 3 and 5:
The constants are those of Assumption 5 at one radius that is large enough for the whole sequence. The statement holds for every admissible choice of them.
The milestones are the results that the proof of Theorem 16 uses, in attack order:
Theorem 16 is a welfare theorem for a mechanism that is actually used. Agents bid myopically, nobody computes a Walrasian equilibrium, and the allocation still becomes efficient. The result also gives a convergence rate. Together with Theorem 11 it identifies the limits of the mechanism with the Pareto allocations, so studying where repeated auctions end up comes down to studying Pareto efficiency.
The theorem is proved in the paper. No part of it, and none of its model, has a machine-checked proof. The formalization would check an argument that runs entirely in extended-real convex analysis, with utilities that may take the value , such as Cobb–Douglas utilities on the positive orthant. It would also settle points the printed proof leaves implicit. One is the radius at which Assumption 5 is applied. Another is that the endowments must lie in the utility domains, which some lemmas need explicitly.
The obvious route bounds each agent's gain per auction by times the agent's surplus and then telescopes. That route needs a single constant valid along the whole sequence, which in turn needs the iterates and the surpluses to be bounded in advance. Boundedness is the step a newcomer cannot get from compactness or from Lipschitz estimates. It comes from recession analysis of the superlevel sets of upper semicontinuous concave extended-real functions, through Rockafellar's characterization of bounded closed convex sets. Mathlib has none of this.
A second difficulty is attainment. Several steps use , so the supremum defining must be attained. Attainment comes from upper semicontinuity, not from the definition. The cluster-point claims also need upper semicontinuity, in order to pass the monotone utilities to the limit.
Utilities are functions (J → ℝ) → EReal, with I, J finite types and I nonempty. Concavity is convexity of the real hypograph, which is Rockafellar's definition. Mathlib's ConcaveOn does not apply because EReal is not a module. The indifference price and are EReal suprema. A supergradient requires to be finite, which is Rockafellar's convention. Without that requirement a bid of would satisfy (4) vacuously and the goal would be trivial.
is encoded as the property that is nondecreasing for every , which the paper quotes from Rockafellar's Theorem 8.6. is the closed sup-norm ball. The paper fixes no norm, and Assumptions 2 and 5 are unaffected by the choice.
The sequence in Theorem 16 is any sequence the mechanism generates: purchases and prices satisfying the market clearing conditions at the current allocation. Existence of solutions and prices is not part of the goal. The rate is stated with the real values of and . Proving these values finite is part of the proof, and nothing in the statement assumes it.
The goal must not be trivialized. Bounded iterates, finite utilities along the sequence and are conclusions, not hypotheses. The constants are universally quantified at a radius whose existence is claimed, not chosen existentially.
The following additions are disclosed on the items concerned. Lemma 2, the boundedness milestone and the first half of Theorem 11 assume , without which they fail. Lemma 9's solution correspondence assumes a finite optimum value.
The development needs extended-real concave analysis: upper semicontinuous concave functions, their recession cones, and attainment of suprema. This layer is reusable beyond this mission. Contributions are welcome on any milestone. The recession-cone boundedness and Lemma 9 are good entry points.
A trader who quotes an exotic option written on several underlying assets (a basket call, a spread option, a best-of option) needs a price range that does not rest on a particular stochastic model. What is observed in the market is a finite set of liquid derivatives (vanilla calls and puts on each asset, and possibly some traded basket options), each with a bid price and an ask price. A model-free price bound for the exotic payoff is the range of prices consistent with these quotes and with the absence of arbitrage. Its upper end can be computed in two ways: as the cheapest static portfolio in the traded derivatives that dominates the payoff in every state of the world, or as the largest expected payoff over all probability measures that price the traded derivatives inside their bid–ask spreads.
The equality of these two numbers is a superhedging duality. For a single asset with exact (zero-spread) prices it goes back to the model-independent pricing literature of Hobson and others; Bouchard and Nutz (2015) proved a one-period duality and a fundamental theorem in a nondominated framework without spreads. Neufeld, Papapantoleon and Xiang (arXiv:2006.14288, Management Science 2023) extend the one-period result to a market where the derivatives are traded with bid–ask spreads and the payoffs are arbitrary Borel functions on a Polish state space, and then use the minimisation side to compute bounds exactly by cutting-plane algorithms.
Let be a Polish space with its Borel -algebra, and let be the set of all Borel probability measures on ; there is no reference measure. Fix traded derivatives with Borel payoffs , collected in , with bid prices and ask prices , .
A static position pays and costs
since long positions are bought at the ask and short positions sold at the bid. The cost is sublinear, not linear.
No-arbitrage (Assumption 2.1): for every , if for every , then for every .
For a Borel payoff , the superhedging price is
and the set of pricing measures is
The proofs also use the box and the set of payoffs super-replicable at zero cost, where is the set of nonnegative Borel functions.
Under Assumption 2.1, for every Borel ,
The identity is stated in and covers the case of payoffs that no static portfolio dominates.
In the order of the proof in Appendix EC.4:
The duality turns a maximisation over an infinite-dimensional set of probability measures into a minimisation over , a finite-dimensional problem with infinitely many constraints. This is what makes the exact computation of model-free bounds in the paper possible: for continuous piecewise affine payoffs, the minimisation side is solved by cutting-plane algorithms whose subproblems are linear and mixed-integer programs. Parts (i) and (ii) say that the upper bound is never under no-arbitrage and that it is realised by an actual static hedge. Lemma EC.4.2 also yields the paper's fundamental theorem (Theorem 2.3), which characterises no-arbitrage by the existence of pricing measures dominating any given probability measure.
The result is proved in the paper; it has no machine-checked proof. A formalization would also give a checked version of the closedness lemma for cones of super-replicable payoffs, which is the step most often adapted from Bouchard–Nutz in later work on one-period robust pricing, and a reusable statement of the extended-valued duality with an explicit convention for non-integrable payoffs.
The obvious route is finite-dimensional linear programming duality. It fails because the constraint is indexed by every in an uncountable Polish space and the dual variables are measures; the paper uses a semi-infinite Fenchel duality theorem (Borwein–Lewis), whose constraint qualification is exactly the relative-interior condition of Lemma EC.4.2. Proving that condition requires constructing, from any , an equivalent-type measure with finite moments, and separating a polyhedron from a convex set properly. A second difficulty is the passage to unbounded : it rests on the closedness of under pointwise limits (Lemma EC.4.1), proved by an induction on the number of coordinates along which the hedge positions diverge; compactness of the unit sphere alone does not suffice because the bid–ask cost is not linear.
The Lean development lives in the namespace ModelFreeBounds.Duality, with one definition file Market. Conventions:
[TopologicalSpace Ω] [PolishSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]. Indices are Fin m and vectors in are functions Fin m → ℝ; is intrinsicInterior ℝ.Market.Standing.EReal with ; the right-hand side of (2.3) is a supremum in EReal over the subset of measures, equal to when .The following formalizations would trivialise the statement and are excluded: a real-valued (where an unbounded infimum becomes ), the Bochner integral for (which is on non-integrable ), without the integrability of the , no-arbitrage stated almost surely under a fixed measure, over sub-probability or arbitrary measures, and a finite .
A complete development needs: semi-infinite or infinite-dimensional Fenchel duality for linear maps into (Mathlib has finite-dimensional separation theorems but not this duality), proper separation of a polyhedron from a convex set in , and the measure-theoretic construction of measures with prescribed null sets and finite moments on a Polish space. The closedness lemma and the support-function identity are independent of the duality and are natural first contributions. Contributions of any milestone, of alternative proofs of the goal, or of reusable infrastructure (extended-valued integrals, relative-interior constraint qualifications) are welcome.
Remanufacturing restores used products (cores) to a sellable condition. Its economics depend on which cores are acquired: a core's condition is unknown until it has been collected, disassembled and inspected, and condition determines what remanufacturing costs. A remanufacturer who decides when to acquire cores therefore commits money before learning what it has bought, while carrying inventory of cores of mixed quality and facing random demand. Nadar, Akan, Debo and Scheller-Wolf (Oper. Res. 71(5), 2023) model this as an infinite-horizon Markov decision process and characterize the optimal acquisition and remanufacturing policy for an arbitrary number of quality types.
Earlier work either assumed that all cores have a single quality level, in which case the model reduces to a single-item inventory problem with an acquire-up-to policy (Ha, 1997), or treated condition uncertainty in one- or two-period models. The paper's contribution is the infinite-horizon structure with quality types.
A collected core is inspected and falls into one of types , type 1 being the highest quality, with probability . Remanufacturing a type core costs , with ; holding one costs per unit time, with . At most one acquisition is in progress at a time; it takes an exponential time with rate and costs . Demand arrives as a Poisson process with rate ; a demand that is not met costs . Costs are discounted with parameter , and time is scaled so that .
The state lists the available cores of each type; is the -th unit vector and . For a function on the paper defines
and . is the acquisition decision, the decision whether to fulfil an arriving demand and with which core type. The optimal cost function satisfies the optimality equation , equation (1).
The acquisition gap in state is ; acquiring is optimal when . The acquire-up-to level is the least value of at which acquiring stops being optimal, the other coordinates being fixed ( if there is none). The paper's analysis runs through a set of functions defined by six inequalities (A.1)–(A.6) on differences of along unit vectors.
The optimal stationary policy is a state-dependent noncongestive-acquisition policy:
and (i) weakly decreases when a core of another type is added; (ii) weakly decreases when a core of another type is replaced by a higher-quality one; (iii) whenever cores are available it is optimal to satisfy a demand; (iv) it is optimal to remanufacture a core of the highest available quality.
Theorem 1 says that the acquisition decision, a priori a function of a -dimensional state, is described by thresholds, each depending on the other inventories in a monotone way. The thresholds fall both when the system holds more cores and when it holds better ones, which is the paper's notion of congestion: an acquired core waits behind the cores already in stock. The policy reduces to Ha's acquire-up-to policy when . The remanufacturing side, points (iii) and (iv), says demand is always met when possible and always with the best core.
The proofs of Theorem 1 and Lemma 1 are in the paper's online appendix; as far as is known, none of these results has been machine-checked. A complete formalization produces a verified threshold-policy theorem for a multi-type inventory MDP with unbounded holding cost, and a verified propagation result for a new event operator, , which averages over inspection outcomes.
The standard route to threshold policies in inventory problems is discrete convexity and supermodularity of the value function. The paper notes that it could not verify these properties in the presence of condition uncertainty: mixes the values at with weights , and the known propagation results for event operators do not cover it. The structure must instead be carried by the custom property set , whose properties (A.3)–(A.6) are coupled across types; showing that preserves all six simultaneously, in particular under the minimum in over the available types, is the central step. A second difficulty is analytic: the holding cost is unbounded, so the operator is not a contraction in the sup norm and the optimal cost must be obtained by monotone value iteration rather than by a fixed-point argument on bounded functions.
States are Fin K → ℕ; index 0 of Fin K is the paper's type 1, so "higher quality" is "smaller index". All costs and rates are real numbers collected in a structure Params K; the demand rate is the field lam. A predicate Standing holds the assumptions of §2 (monotone , antitone positive , , , ) and the disclosed additions implicit in the model: , a probability vector, , , , .
is a fold of min in which unavailable types contribute the rejection value, so the inner minimum over an empty set is handled exactly. is defined as the pointwise limit of value iteration from the zero function, and milestone 1 shows the limit exists and solves (1). Acquiring is optimal in when , ties counting as acquiring. is the canonical level, valued in ℕ∞, defined from as an infimum; it is not a threshold chosen to fit. Point (ii) is formalized as moving one core from type to type with .
Theorem 1 is about this and this : a statement about an arbitrary function , about thresholds chosen after the fact, or with optimality redefined through the thresholds would be a different and weaker theorem.
A complete development needs monotone convergence of value iteration for a concrete operator on with an unbounded holding cost, and the case analysis of Lemma 1 for each of , and . The value-iteration argument is reusable for other uniformized inventory MDPs with nonnegative costs. Proofs of any milestone, and of intermediate lemmas such as the preservation of individual properties by or , are welcome.
Dynamic games with many players, such as dynamic oligopolies with investment, industry dynamics models, and heterogeneous-agent macroeconomic models of Bewley–Aiyagari type, are rarely tractable through Markov perfect equilibrium: the number of population states a player must track grows too fast with the number of players. Mean field equilibrium (MFE) replaces the evolving population by a fixed distribution of states that each player takes as given and that is reproduced by the players' own optimal behaviour. The concept is used throughout operations research and economics to approximate equilibria of large games (Weintraub, Benkard and Van Roy 2008; Adlakha, Johari and Weintraub 2015).
Existence of an MFE is comparatively well understood. Uniqueness is what makes the concept usable for prediction and for comparative statics, and general uniqueness conditions for models with individual states and dynamic optimization were missing. Light and Weintraub (arXiv:1903.02273v3) give such a condition, in the form of monotonicity properties of a single player's optimally controlled Markov kernel, and apply it to capacity competition, quality ladders, advertising, reputation and Bewley–Aiyagari models.
Time is discrete. A player has a state in a compact metric space carrying a closed partial order , and chooses an action from a non-empty compact set . The population state is a Borel probability measure on ; the set of such measures carries the weak topology. A player in state who takes action when the population state is receives the payoff and moves to the state , where the idiosyncratic shock takes the value with probability () independently in each period. Payoffs are discounted by . Assumption 1 requires bounded and jointly continuous, jointly continuous, and compact-valued and continuous.
Holding fixed, a player maximizes the expected discounted payoff over measurable strategies; is the resulting value function and
is the optimal strategy correspondence. A stationary strategy with induces the kernel and, for each , the operator . A pair is an MFE if is optimal given and .
The kernel is -ergodic if each has a unique fixed point in and weakly for every . With the usual stochastic order, is increasing in if implies . The model also carries a binary relation on such that forces and ; is decreasing in if implies , and agrees with if implies .
Suppose is -ergodic, increasing in and decreasing in , agrees with , and is single-valued (Assumption 2). If is complete, then for any two MFEs and ,
Existence is not part of the statement.
In the order the paper's proof uses them:
Theorem 1 turns uniqueness of a stationary equilibrium of a large dynamic game into monotonicity conditions on one player's optimally controlled Markov kernel, which in applications follow from monotonicity of the policy function in the population state. The paper's comparative statics result (Theorem 4) depends on it: directional changes of the unique MFE in the discount factor or the investment cost are only meaningful once the equilibrium is unique. The applications in §§4–5 are each a verification of its hypotheses.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal model of a discounted anonymous stochastic game on a compact metric state space with population states in under the weak topology, a formal statement of the uniqueness theorem in it, and statements of the order-theoretic and dynamic-programming facts its proof cites. Two of these, the upper-set characterization of the stochastic order and its closedness under weak limits, are general results of Kamae, Krengel and O'Brien (1977) that are not yet on the platform in this form.
The order-theoretic core of the proof is short. Two cited facts carry the weight. Closedness of under weak convergence is not a consequence of the definition: weak convergence controls integrals of bounded continuous functions only, while the stochastic order quantifies over all bounded measurable increasing functions, and increasing functions need not be continuous; this is where the closedness of the partial order and the compactness of enter. Second, the steps that use single-valuedness of and the equivalence go through the value function, which is a supremum over history-dependent measurable strategies, so its dependence on the population state, its continuity, and the measurability of the optimal strategy have to be established from the dynamic program rather than read off the definitions.
Model. is a compact metric space with a partial order whose graph is closed, with its Borel -algebra. is Mathlib's ProbabilityMeasure X, whose topology is the weak topology. Actions are elements of a set (a subtype of EuclideanSpace ℝ (Fin q)). The shock takes values (the paper's ) and is i.i.d. over time.
Value function. Strategies are history-dependent and measurable. The expected discounted payoff is a series in 0-based time with weight , and its period- term is a finite sum over shock histories. is the supremum over feasible strategies, and is the Bellman argmax.
Orders. is the published platform order StochIneqPO.Comparison.StochLE, which tests against bounded measurable increasing functions. Its arguments are swapped relative to the paper's notation: StochLE P₁ P₂ means . The relation is an arbitrary predicate on with no order axioms.
Equilibrium. acts on measures, and MFE consistency is an equality of measures.
Added hypotheses, all disclosed:
Ruled out. The kernel is never a free family of measures. It is always built from , and the value function, so equality of strategies under equivalent population states is a theorem, not a hypothesis. MFE existence is neither assumed nor concluded.
Infrastructure. A complete development needs:
The last two are reusable well beyond this mission. Contributions to any of these layers are welcome.
Banking and insurance regulation measures capital requirements with risk measures that look only at the tail of a loss distribution. The Basel framework moved from Value-at-Risk (VaR) to Expected Shortfall (ES) for market risk (BCBS, Minimum capital requirements for market risk, 2016), and both VaR and ES at level depend on a loss only through its distribution beyond the -quantile. Liu and Wang (SSRN 2841909; Mathematics of Operations Research 46(3), 2021, doi:10.1287/moor.2020.1072) isolate this feature as a definition. A tail risk measure is any risk measure that depends only on the tail, and every such measure is generated by an ordinary law-invariant risk measure applied to the tail. The paper then asks which of the classical properties of risk measures (Artzner et al. 1999; Föllmer and Schied 2002) survive this construction.
The answer to that question is a practical design rule. A regulator or risk manager who wants a coherent tail risk measure can choose any coherent law-invariant risk measure and apply it to the tail. The theorem guarantees that the result is again coherent, and that nothing is lost by working only with generators.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a loss when positive and a profit when negative. Its distribution function is . The space of risks is , the measurable, essentially bounded random variables. A risk measure is a real-valued functional on .
For , the -tail of is a random variable with distribution function
the conditional law of beyond its -quantile. A risk measure is a -tail risk measure if whenever and have the same law. A pair is a -tail pair if is law-invariant and
in which case is a -generator of . For example, is generated by the expectation. The mixture has distribution function : it adds mass at the essential infimum of .
The classical properties are those of Appendix A of the paper:
A monetary risk measure satisfies (A1)–(A2), a convex one (A1)–(A3), and a coherent one (A1)–(A4) (Definition A.1).
For and a -tail pair on ,
All three equivalences are part of the goal. No normalization such as is assumed.
where is the set of sums with (resp. , the law of the -tail).
The result. Theorem 1 (iii) makes the generator a complete parametrization of coherent and convex tail risk measures. Coherent tail risk measures are exactly with coherent and law-invariant, so representation results for law-invariant coherent risk measures (Kusuoka 2001) transfer to tail risk measures. The paper uses this for dual representations (Appendix G) and for the bound of Theorem 2. Theorem 3 reduces worst-case risk aggregation for a tail risk measure to the same problem for its generator on tail marginals. It contains classical results on worst-case VaR (Bernard et al. 2014, Lemma 4.3) and the subadditivity of ES as special cases.
Formalizing it. The results are proved in the paper; none of them is machine-checked. The mission produces a Lean statement of tail risk measures and their generators that later missions on tail risk can import. It also produces formal versions of the distributional identities (Lemma B.1, eq. (14)) on which the paper's proofs rest, and a statement of worst-case aggregation in extended-real suprema. A complete development would also be the first formal proof that ES-type constructions preserve coherence through a general generator, rather than for one specific measure.
Several directions are routine. Monotonicity, translation invariance and positive homogeneity pass from to because commutes with shifts and positive scalings and preserves . The converse directions go through .
Convexity is the obstruction. The obvious argument would compare with , but the tail of a sum is not the sum of the tails. The event "beyond the -quantile" for the sum differs from the corresponding events for and , so no pointwise or comonotone coupling identifies them. Example 1 makes this concrete: the tail standard deviation is generated by a convex measure and is not convex. Convexity of therefore needs monotonicity of together with the worst-case aggregation identity of Theorem 3. That identity is a statement about all dependence structures with given marginals, and it requires constructing, on an atomless space, couplings whose tails dominate a given sum.
TailRiskSharing.TailConv.Linf), as the paper suggests on p. 5. Then , every risk measure is a real-valued function on , and every property quantifies over only. The general cone with -valued risk measures is not stated.TailRiskSharing.VaRConv.IsAtomless), not Mathlib's NoAtoms, which only says that singletons are null.A formalization in which is a fixed Classical.choose of the tail, in which coherence omits monotonicity, or in which atomlessness is replaced by NoAtoms is not this theorem.
A complete development needs the quantile transform on an atomless space, couplings with a prescribed joint law, the elementary identities of Lemma B.1 and eq. (14), and the worst-case aggregation argument of Appendix C. The distributional lemmas, quantile couplings and aggregation sets can be reused in any later mission on law-invariant risk measures. Contributions to any milestone, and to general infrastructure for quantile couplings on atomless spaces, are welcome.