Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Retailers sell seasonal and perishable goods under markdown pricing: the posted price may fall over the selling season but never rise. Fashion, consumer electronics and grocery chains use markdowns because customers and regulators react badly to price increases and because markdown schedules are easy to communicate. The revenue management literature measures a pricing policy by its revenue loss against the fluid (deterministic) benchmark as inventory and horizon grow together.
Timeline:
A seller holds units and sells over . Customers arrive as a Poisson process with rate ; each buys one unit iff her valuation, which lies in , is at least the posted price. At price a customer buys with probability , the purchase rate. Since is a decreasing bijection of onto , a purchase rate determines the price , and the revenue rate is . The model assumes (A2) that is strictly concave with a maximizer and (A3) that .
The fluid rate is and the fluid value is .
The policy updates the price at times , , with , (equation (14)). On it posts until stock-out, where and
with the projection onto , the deviation of the realized sales from their mean, and shift terms given by equation (15) with a parameter . The maximum makes non-decreasing, so prices only fall. is the expected revenue of this policy. In the asymptotic setting the -th problem has inventory and horizon .
For large and every with ,
with the constant depending only on the model, , and , and uniform in .
The milestones follow Appendix B of the paper: Lemma 7 (the schedules satisfy and ); the coupling bound (EC.2) with an uncapped process that ignores inventory; the second-order Taylor bound after (EC.2) with error terms ; the closed form (EC.3) of on a good event ; Lemma EC.1 (bounds on ); Lemma EC.2 (inventory balancing, corrected); Lemma EC.3 (expected overselling); Lemma EC.5 (a Poisson tail bound with random rate); Lemma EC.4 ().
Theorem 4 shows that the monotonicity constraint costs little: with the loss is , already below the of any fixed price, and letting grow like brings it to a polylogarithmic order. The policy is explicit (two closed-form schedules and a one-line update), so the bound is a guarantee for an implementable markdown rule; the same construction is used in the paper for pricing with strategic customers.
The result is proved on paper. To our knowledge none of it is formalized; the platform has Gallego–van Ryzin's fluid bound and fixed-price results, which this mission does not need (it compares against the explicit value ). The mission adds a machine-checked version of the full Appendix B argument and corrects Lemma EC.2, whose printed identity holds only when .
The policy is a nonlinear feedback rule: the projection and the running maximum make a non-smooth function of all past sales, and the sales are themselves capped by the inventory. A direct Taylor expansion of the revenue around fails because is not a linear function of the sales deviations. The argument controls this by passing to the uncapped process (paying for overselling separately), proving that on the good event the projection and the maximum are inactive, and showing that the good event fails with superpolynomially small probability. The last step needs a concentration bound for Poisson counts whose rate is itself random, uniformly over a number of updates that grows with ; this uniformity is where the condition on enters.
The model is a structure Model with the survival function as primitive (continuous, strictly decreasing on , , ), as the inverse on , and A2 for on and A3's derivative bounds on the open interval (nothing is asked at the endpoints); continuity of is not assumed. The continuous-time process is not built: the demand counts of the intervals have, given the past, Poisson laws with mean (thinning and independent increments), and seqPoissonLaw is that exact joint law on . The actual policy sells in interval ; the uncapped process sells . The constant of the goal is chosen before and , and the condition on is evaluated at ; a fixed admissible is a special case. Upper bounds on unbounded nonnegative quantities use the lower Lebesgue integral, so a non-integrable variable cannot make them vacuous. The lemmas of Appendix B are stated for every instance satisfying the setting (, , the condition on ), which includes the -th problems for large .
Reusable parts: the sequential Poisson law with history-dependent rates and the mixed-Poisson tail bound (Lemma EC.5) apply to any policy that sets a constant price on each of finitely many intervals. Welcome contributions: proofs of the milestones, in particular Lemma EC.5 and the coupling bound (EC.2), and a general lemma identifying expectations under seqPoissonLaw with iterated Poisson expectations.
Two literatures study how to split a resource among agents who report private information. Fair division of divisible goods asks for allocations that are proportional, efficient and resistant to misreporting (Steinhaus 1948; Cole, Gkatzelis and Goel 2013). Wagering mechanisms let bettors with subjective beliefs about a future event bet against each other, and ask for individual rationality, incentive compatibility and budget balance (Lambert et al. 2008; journal version, 2015). Freeman, Pennock and Vaughan observe that, once a wagering mechanism is read as a sale of Arrow–Debreu securities (Freeman, Lahaie and Pennock 2017), the two problems are the same problem: a bet is a share of the securities, and the securities are divisible goods.
The paper (AAAI'19; extended preprint, 2018, which is the basis here; journal version in Management Science, 2024) makes this precise as a correspondence between the two classes of mechanisms, and uses it to move mechanisms and impossibility results from one side to the other. This mission formalizes the correspondence itself (§3).
There are agents and goods (fair division) or outcomes of a random variable (wagering). Each agent reports a point (or ) of the probability simplex : normalized additive values of the goods, or subjective probabilities of the outcomes. Each agent also has a weight (entitlement) or wager , with and . The value of a bundle for values is .
An allocation mechanism maps to a feasible allocation: and for every good . A wagering mechanism , in security form, maps to numbers of type- securities, each paying if . and are corresponding mechanisms (Definition 10) if
The properties compared are: proportionality (), Pareto optimality over feasible allocations, and weak / strict incentive compatibility (truthful reporting maximizes true value) on the allocation side; individual rationality (some report guarantees expected payoff at least ), weak / strict budget balance (, resp. ), weak / strict incentive compatibility, and side-bet Pareto optimality (no zero-sum re-trade of securities, keeping holdings nonnegative, weakly helps every agent and strictly helps one) on the wagering side.
For all , the conjunction of four clauses:
The two validity claims of p.4; the two halves of the proof of Theorem 1 (A.1) and Theorem 1; the two halves of the proof of Theorem 2 (A.2, the direction "proportional ⇒ individually rational" without IC) and Theorem 2; the three steps of the proof of Theorem 3 (A.3) and the corrected Theorem 3.
The correspondence lets every wagering mechanism be used as an allocation rule for divisible goods with no money, and every allocation rule be run as a bet. The paper's Table 1 and §4 use it to read off, for example, that weighted score wagering mechanisms give proportional, strictly incentive-compatible, envy-free allocations, and that no-arbitrage wagering mechanisms are not envy-free. Impossibility results transfer the same way (§6): Schummer's theorem that the only incentive-compatible, Pareto-optimal allocation mechanisms are dictatorial carries over to wagering, and the welfare bound of Han et al. (2011) for incentive-compatible allocation carries over too.
The results are proved in the paper; none is formalized. The formalization adds two things. First, a reusable model layer for mechanisms on profiles of simplex points, which fixes the quantifier structure of IC, IR, proportionality and both Pareto notions, where informal statements are loose (which report the IR guarantee may depend on; over which alternatives Pareto optimality ranges). Second, a check of the printed statements. The "only if" direction of Theorem 3 is false as printed: a Pareto-optimal allocation mechanism may leave a good unallocated when every agent reports zero value for it, so its corresponding wagering mechanism need not be strictly budget balanced. The goal states the minimal corrected equivalence.
Each proof is a short calculation, and the obstacle is getting the definitions to line up. Two steps need care. In Theorem 2 proportionality is about reported values and individual rationality about true beliefs, so the transfer needs weak incentive compatibility to replace the IR report by the truthful one. In Theorem 3 the "if" direction is printed as "a Pareto-improving allocation consists of agents swapping goods", which is only true when the improving allocation wastes nothing; an improving allocation may itself waste goods, and must first be completed before its difference from becomes a side bet. The "only if" direction relies on "some agent who values it positively", who need not exist, and that is where the printed statement fails.
Agents are Fin n, goods / outcomes Fin m, both 0-based. Reports, true values and beliefs are points of Mathlib's stdSimplex ℝ (Fin m); weights and wagers are strictly positive vectors (PosVec n), whose sum is both and . Allocation and wagering mechanisms share one type, total functions of (profile, positive vector); validity is a predicate (IsAllocMech, IsWagerMech). Unilateral deviations are Function.update. Pareto alternatives are feasible allocations. Strict IC is weak IC plus strictness on every misreport. The side-bet nonnegativity condition is entrywise. Corresponding A B is the form . Theorems 1 and 2 and the inverse identities are stated for arbitrary elements of Mech, without the validity predicates, which their arguments do not use.
Positivity of weights is essential: with the inverse map is meaningless, and unnormalized reports would change what proportionality means. No hypothesis is needed for or .
Everything is finite sums over Fin; no measure theory or analysis is needed. The model definitions are reusable for later formalizations of §4 (weighted score wagering mechanisms, envy-freeness). Proofs of the milestones, and of the goal from the milestones, are welcome.
A seller offers a service to a set of buyers, each with a private value, and a feasibility constraint limits which sets of buyers can be served together. This is the basic single-parameter problem of mechanism design. Milgrom and Segal proposed clock auctions for it, and designed one for reallocating radio frequency licenses (Milgrom and Segal 2020). In a clock auction each bidder faces a personal price that only rises, and may leave at any time. The format is transparent, a buyer needs to answer only price offers, and the winners never reveal their values.
The cost of the format is the question. Dütting, Gkatzelis and Roughgarden showed that a deterministic clock auction with no information about the values attains no bounded approximation to the optimal welfare, even with two maximal feasible sets (Dütting et al. 2014). Feldman, Gkatzelis, Gravin and Schoepflin (arXiv:2202.09291v1) show that information about the values removes this obstacle, for every downward-closed constraint. This mission formalizes the version with full knowledge of the distributions.
Let be a finite set of buyers, with values , . A feasibility constraint is downward-closed if every subset of a member is a member. Its maximal feasible sets form the collection , and is the parameter of the result.
In the Bayesian setting each is drawn independently from a distribution , and the seller knows . The benchmark is the expected optimal welfare
A single-price clock auction (Mechanism 1) computes a vector of prices from public information, which here includes , and offers once to each buyer. A buyer stays exactly when . Among those who stayed the auction selects a feasible subset , serves , and charges each member . It is deterministic when the prices and the selection rule involve no randomness. The selected set depends on the values only through the set of buyers who stayed.
There is an absolute constant such that every downward-closed constraint with maximal sets and every product distribution admit a deterministic single-price clock auction with
The constant is not fixed in the statement, so the goal survives any improvement.
For let , and let be the least with .
The theorem shows that the impossibility for deterministic clock auctions is a statement about missing information, not about the clock format, and that a very restricted member of the class already beats a logarithmic barrier. Sequential posted-price mechanisms, which must serve every buyer who accepts, cannot do better than even when the maximal sets are disjoint (Rubinstein 2016). The single-price auction differs from them only by deferring the choice of whom to serve until all buyers have answered, and that gains an exponential factor. The same benchmark decomposition is reused in the paper's limited-information and prior-free results.
The result is proved in the paper, and no machine-checked proof of it is known. Formalizing it adds a definition of Bayesian single-price clock auctions and a machine-checked core-tail decomposition of an expected maximum over feasible sets. Formalized clock auctions so far concern budget-feasible procurement with descending prices, which is a different model. Two printed steps of the proofs do not hold as written, while the lemmas do: the display on p.20 in the proof of Lemma 3, and the exact doubling in the proof of Lemma 2, which needs repair for distributions with atoms. A complete formalization must supply these arguments.
The maximum over sets defeats the two obvious estimates. Replacing the maximum by a sum loses a factor . Bounding it by the largest expected set value fails, because with heavy-tailed values the realized maximum can far exceed every set's mean. The natural single-threshold approach of posted pricing fails too, since it must commit to each acceptance as it happens.
Independence is needed twice, and in the second use a bidder's own value is correlated with the event that the bidder's set has many high values, so the expectation does not factor as written. A further obstacle is that the distributions are arbitrary: atoms mean that the expected count above a threshold can jump, so an exact solution of need not exist.
Lean conventions:
Fintype N, and 𝓕 : Finset (Finset N) with ∅ ∈ 𝓕, which excludes only the empty family.ℝ≥0. The laws ν i are arbitrary probability measures: atoms, unbounded supports and infinite means are all allowed.ℝ≥0∞-valued lower integrals, so no integrability hypothesis appears and the benchmark cannot collapse to a junk 0.log is base 2 (it writes for the natural logarithm), and the thresholds and the cutoff use Real.logb 2. In the goal and in Lemma 3 the base is absorbed by the existential constant, and Real.log is used there. The factor is , because is at and negative at . In Lemma 3 the factor is , because the literal fails at .tS is an infimum, footnote 2's reading. Statements using it assume .A trivializing formalization is ruled out by the auction structure: price does not see the values and select reads only the set of acceptors, so the auction cannot be VCG, which would have factor .
The development needs the product measure on N → ℝ≥0, a multiplicative Chernoff bound for sums of independent non-identical indicators, and layer-cake integration. Those parts, and the decomposition itself, are reusable beyond this mission. Contributions welcome are the milestones above and the general Chernoff bound. Theorems 4, 6 and 9 of the paper are outside this mission.
In bilateral trade a seller and a buyer each hold a private valuation for one good, and an intermediary (a platform or broker) decides at which price the good changes hands. Myerson and Satterthwaite showed that no mechanism can be at once efficient, incentive compatible, individually rational and budget balanced (Myerson–Satterthwaite 1983). Among mechanisms that are dominant-strategy incentive compatible, individually rational and exactly budget balanced, only posted fixed prices survive. A platform facing a stream of seller/buyer pairs therefore has to learn a good fixed price from experience.
Cesa-Bianchi, Cesari, Colomboni, Fusco and Leonardi (arXiv:2109.12974v1, 2021; later in Mathematics of Operations Research, 2024) study this as a regret-minimization problem and map out the attainable rates under full and realistic feedback and under stochastic and adversarial valuations. This mission formalizes their positive result for realistic feedback, the setting of an actual posted-price mechanism, where the learner only sees whether each side accepted the price.
Valuations, prices and gains live in . The gain from trade of price for a seller with valuation and a buyer with valuation is
In each round a fresh pair arrives, the learner posts , and under realistic feedback it observes only the two bits and ; the gain stays hidden. In the stochastic i.i.d. setting with independent valuations the pairs are i.i.d. with law . The bounded-density assumption asks and for every Borel set . The learner randomizes through i.i.d. uniform draws on that are independent of the valuations.
The regret of a pricing strategy is
A -armed bandit strategy chooses, in each round, an arm in as a measurable function of its own uniform draws and of the rewards it has observed. Its regret after rounds is taken against i.i.d. reward vectors with law on , and a distribution-free bound bounds for every such .
Scouting Bandits (SB, Algorithm 3) uses a grid , . For rounds it posts uniform prices and forms and , both computable from the feedback. It then runs on the grid, posting and feeding the surrogate reward .
For every ,
and, for every , there is depending only on such that if for all and , then SB with , and has
Theorem 3 gives an regret for posted-price bilateral trade under realistic feedback, and Theorem 4 of the paper shows that cannot be improved in this setting. Theorems 5 and 6 show that dropping independence or bounded densities makes linear regret unavoidable, so the hypotheses of Theorem 3 are where learning becomes possible. The reduction itself is reusable: any minimax-optimal bandit algorithm plugged into SB inherits the rate.
The result is proved in the paper. No machine-checked proof of it, of the Decomposition lemma, or of the bandit reduction exists on the platform. Formalizing it adds a checked version of a regret bound whose proof combines a measure-theoretic identity, a discretization argument, a conditioning argument for a randomized learner, and a uniform deviation bound.
Posting a price reveals only and in the long run, while the expected gain also depends on integrals over prices away from . A standard bandit algorithm run directly on prices therefore does not see its own reward, and the obvious approach of treating each grid price as an arm fails.
In the formal proof, the steps that need the most care are probabilistic. Term (III) needs that, conditionally on the scouting estimates , the bandit phase is a genuine run of on i.i.d. reward vectors in . This uses almost surely, the independence of from the bandit-phase data, and a disintegration of the product measure. Term (IV) conditions on the history before round . Terms (V) and (VI) need the univariate Dvoretzky–Kiefer–Wolfowitz inequality with Massart's constant, which is open on the platform as OfflineCensoredPricing.Identifiability.lemma_A_2 and is not posed again here.
Rounds are indices of Fin T. The sample space is with the law , so i.i.d. sampling, independent valuations and independence of the learner's randomization are built into the measure. Valuation laws are probability measures on concentrated on . The density bound is imposed on each marginal law, which every joint density bounded by implies. The regret is the real supremum over , and all its expectations lie in . The grid is grid K k = (k+1)/(K+1) for k : Fin K.
A bandit strategy is a sequence of measurable maps from (uniforms, past real rewards) to Fin K. Admissible reward laws are probability measures on concentrated on , with correlated arms allowed. SB uses one uniform sequence for both its scouting prices and 's randomization. Its prices depend on the valuations only through the realistic feedback bits. , , and are hypotheses.
Measurability of is part of the strategy, so the expectations are not junk. In (b) the constant is quantified before the bandit family, the laws, and . The family is indexed by , because there is no strategy over zero arms, and by the horizon it is tuned to, because MOSS takes the horizon as an input; one strategy for each is the case that does not depend on the horizon.
The development needs product measures, conditional independence on finite products, and a DKW bound. The definitions of the bandit game and its regret apply to any i.i.d. bandit problem with correlated arms. Contributions are welcome on any milestone, especially Lemma 1 (Fubini on ) and the conditioning steps (III) and (IV).
A two-sided market has sellers who hold goods and buyers who want them, each with a private value. A mechanism that reallocates the goods should be truthful (no agent gains by misreporting her value), individually rational (no agent is worse off for participating) and budget-balanced (the mechanism neither injects nor keeps money). Myerson and Satterthwaite showed that already for one buyer and one seller no mechanism has all three properties and always trades efficiently (Myerson–Satterthwaite 1983). The question is therefore how much of the optimal social welfare such a mechanism can guarantee.
Braun and Kesselheim (arXiv:2105.15032v1, 2021; Mathematics of Operations Research, 2022) answer it for matroid double auctions by transferring the balanced-threshold technique of one-sided prophet inequalities (Kleinberg–Weinberg 2012) to two-sided markets.
Timeline.
There is a finite set of buyers and a finite set of sellers, disjoint. Each seller holds one item, all items are identical, and each buyer wants at most one item. A matroid on the buyers restricts which sets of buyers may be served. Agent 's value for an item is drawn independently from a known law ; is the profile.
An allocation serves a set of buyers and lets a set of sellers keep their own item, with ; its welfare is . The benchmark is .
For served buyers and items left for buyers, is the best set with and . Buyer 's threshold is
or if cannot be feasibly added. Seller 's threshold is . The price of a trade is .
Mechanism 1 (Algorithm 1, p.9) repeatedly pairs the remaining buyer with the largest threshold and the remaining seller with the smallest one. Infeasible buyers are discarded. Otherwise the seller is asked first: if her value exceeds the price she keeps her item and drops by one. If not, the buyer is asked, buys if her value exceeds the price, and leaves either way.
Mechanism 1 is DSBB, DSIC and IR for all buyers and sellers, and
It is stated for every finite market (empty sides allowed), every matroid, every family of independent laws on with finite means, and every fixed tie-breaking order.
Lemmas 5–7 and inequality (2) carry the minimal correction "the buyer is not already served"; without it the printed statements fail on one-buyer instances.
The theorem gives a mechanism that satisfies all of the properties Myerson–Satterthwaite forces a trade-off between, except exact efficiency, and loses at most a factor 3. Every trade is a bilateral exchange at a single price. The prices are posted and depend only on the distributions, so the mechanism is simple to run and to explain. The proof splits the welfare into a base value covered by prices and a surplus above them. This turns one-sided balanced-price arguments into two-sided ones, and the paper reuses the template for knapsack and combinatorial double auctions.
The result is proved on paper. The platform has the one-sided matroid prophet inequality of Kleinberg and Weinberg, but nothing for two-sided markets: no budget-balance notion, no seller incentives, no double-auction mechanism. A complete development adds the first machine-checked two-sided result and checks the corrections to Lemmas 5–7.
Buyer incentives are routine: a buyer is asked at most once, at a price independent of her report. The difficulty sits elsewhere:
Agents are B ⊕ S with Fintype. The matroid is a Mathlib Matroid B with M.E = univ. Values are real, each is a probability measure with and an integrable identity, and the profile law is Measure.pi D. Thresholds and prices live in WithTop ℝ (). Ties are broken by injective ranks rkB, rkS, quantified over. The comparisons are strict, as printed. Algorithm 1 is a step function iterated times, with a log of offers. An outcome records served buyers, keeping sellers, buyer payments and seller receipts. IsDSBB asks for a set of trades with distinct buyers and sellers that explains the allocation and makes each buyer's payment equal to the seller's receipt. IsDSIC and IsIR quantify over all report profiles in . Ghost samples are integrals over the product of two copies of Measure.pi D.
The approximation clause compares against the maximum over feasible allocations, not against . Because non-integrable integrands integrate to , the integrability hypotheses must stay: without them the clause could hold for the wrong reason.
Useful infrastructure beyond this mission: maximum-weight independent sets in truncated matroids (greedy optimality, exchange), submodularity of , and measurability of finite iterated decision procedures. Proofs of any milestone, and of the monotonicity lemmas as stand-alone matroid facts, are welcome.
A seller who allocates resources that appear and expire over time (machine slots in a cloud, rooms on given nights, edges of a matching market that change from round to round) often cannot run an auction for every user. A posted price mechanism announces prices before the user arrives and lets the user buy her preferred bundle; it is truthful for myopic users because the prices do not depend on what the user reports. Emek, Lavi, Niazadeh and Shi (arXiv:2005.01869v2, later in Mathematics of Operations Research, 2024) ask how well such a mechanism can learn prices online when valuations are chosen by an adversary and inventory is limited. The difficulty is that the natural benchmark is stateful: a good pricing rule reacts to how much of each resource is left, and inventory couples the rounds. The paper's answer, Theorem 3.10, is a mechanism whose regret against the best inventory-dependent pricing policy in a finite class is sublinear in the number of rounds.
A DRACC instance (dynamic resource allocation with capacity constraints) has rounds and finitely many resources. Resource arrives at round , departs after round (with ) and carries units. The active set consists of the resources with , and . User has a valuation with , otherwise arbitrary. Facing prices , she buys one unit of each resource in her demand set
with ties broken by a fixed order, and pays . The inventory vector records the remaining units; a price vector is feasible for if every price lies in and every exhausted active resource is priced at , which no user buys since valuations are below .
A pricing policy maps the active set and an inventory vector to a feasible price vector. Played on its own, it generates its own inventory trajectory and revenue . A randomized mechanism posts using only , the capacities of arrived resources and the valuations . Its regret with respect to a finite class of policies is
There is an absolute constant such that for all and every finite nonempty some non-anticipating, always feasible randomized mechanism satisfies, on every DRACC instance,
The proof passes through an abstract model, the dynamic deterministic MDP (Dd-MDP), in which an adversary picks a transition function and a reward function each round. The milestones, in proof order, are:
The theorem gives the first vanishing-regret guarantee for posted pricing against a stateful benchmark with arbitrary (not even monotone) valuations, and the paper derives from it learning guarantees for online job scheduling and matching over dynamic bipartite graphs (Corollaries 4.1–4.4). The bound degrades as grows, and Theorem 3.11 shows that some dependence on and is unavoidable: if , every posted price mechanism has regret . The abstract part, Theorem 3.8, applies to any Dd-MDP satisfying chasability, beyond pricing.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them requires a precise account of what an online randomized mechanism may know, of policy regret along the policy's own trajectory, and of an online-learning algorithm with switching cost. The Theorem 3.7 statement here corrects the printed one (it needs ), and the Theorem 3.8 statement corrects the printed one by and ; the first episode of C&S costs up to , which the paper's switch count misses.
The obvious approach, running an experts algorithm over the policies in , fails because the reward of a policy depends on the inventory state it has built up; switching to a policy in the middle of the horizon does not recover that policy's reward, since the mechanism's inventory differs from the policy's. Proposition 3.1 of the paper shows that general Dd-MDPs force regret , and Proposition 3.3 that no deterministic chasing strategy has chasing regret on DRACC. The central difficulty is to follow a target policy whose inventory differs from the mechanism's own, from an arbitrary starting inventory, at a cost sublinear in $; with arbitrary valuations, raising the price of one resource can change which other resources the buyer takes, so the comparison between the two inventory trajectories cannot be done resource by resource.
Resources are natural numbers and an instance's resources are a finite set; the number of resources is not bounded. Inventory vectors are functions that vanish off the active set, price vectors are functions with values in , and a policy takes the active set as an explicit argument. Ties are broken by an arbitrary injective rank on bundles (every lexicographic order is one). The instance is fixed before the coins (an oblivious adversary); the expectation is over the mechanism's coins only, and the benchmark is each policy's revenue along its own trajectory. The constant is absolute, chosen before , , and , and is natural.
A mechanism that reads before posting , or one chosen after the instance, could play the best policy in hindsight and trivialize the goal; the non-anticipation predicate and the quantifier order mechanism instance rule this out, as the same order oracle instance does in Theorem 3.6.
The development needs a randomized-online-algorithm vocabulary for Dd-MDPs, chasing oracles, online learning with switching cost (the experts setting of Kalai and Vempala), product measures of i.i.d. coins, and the DRACC model. The Dd-MDP, chasing and OLSC definitions are independent of pricing and reusable. Contributions to any milestone, including a formal proof of the Kalai–Vempala switching-cost bound, are welcome.
In many recommendation and promotion settings the reward of showing an item depends on how long it has been since the item was last shown: a promoted product in a live-streaming session, a notification, a piece of content whose appeal recovers while it rests. Bandits with recovering rewards model this. Kleinberg and Immorlica (FOCS 2018) studied recharging bandits with concave recovery, Basu, Sen, Sanghavi and Shakkottai (NeurIPS 2019) blocking bandits, and Pike-Burke and Grünewälder (NeurIPS 2019) recovering bandits with parametric recovery. Simchi-Levi, Zheng and Zhu (arXiv:2106.14813) drop every shape assumption except monotonicity and boundedness, and ask how well a simple class of schedules can do when all recovery functions are known. This mission formalizes their offline guarantee.
Timeline:
There are arms. Pulling arm after it has been idle for periods pays the mean reward , where , and is non-decreasing in (no concavity). Every arm was last pulled at time . In each period at most arms may be pulled.
For one arm, is the best average reward over when the arm is pulled at most times (problem (2)), and is its long-run value. The upper bound is
and bounds the offline optimum over horizon . The supporting points are the points where meets its upper concave envelope .
A purely periodic policy gives each arm a period and an offset and pulls it at , ; it is a -PPP if at most arms are pulled in any period. Algorithm 2 takes an optimal solution of the upper-bound program, lifts each coordinate to a frequency , rounds every period up to the set , packs the arms with periods in each into at most groups that can each be served one arm per period, and keeps the groups of largest long-run reward. The Lean names follow the paper: F, FT, UB, supp, Rcc, roundUp, PPP, IsKPPP, IsRSRun (Algorithm 1), IsAlg2Run (Algorithm 2), gamma.
There is an absolute constant such that for every admissible instance and every , Algorithm 2 has a run, every output of every run is a -PPP, and for every
The constant is not fixed in the statement; the paper's proof gives .
Theorem 1 says that, with no assumption on the shape of recovery beyond monotonicity, a schedule that pulls every chosen arm at a fixed period loses only a factor against an upper bound on the optimum, and . The offline problem is NP-hard even within purely periodic policies, so a constant-factor guarantee for a simple, polynomial-time policy is the relevant benchmark. The paper's online results (an regret against ) are measured against exactly this quantity.
Formalizing it produces a checked statement of what "the policy returned by Algorithm 2" guarantees for every admissible run, including the boundary effects behind the term. The result is proved in the paper; it has no machine-checked proof that we know of. The developments of the long-run value of a single arm (a limsup of a finite optimization), of dyadic period packing, and of top- averaging are reusable for other periodic-scheduling and recharging-bandit statements.
The obvious first idea is to schedule each arm at its optimal frequency directly. It fails twice: need not be an integer, and arbitrary periods cannot be interleaved (periods and always collide). The rounding to makes the periods in each class divide one another, at a loss of , and the packing step then costs a factor ; balancing the two gives . The single hardest piece is Lemma 1: is defined as a limsup of a finite combinatorial optimization, and identifying it with the piecewise-linear interpolation needs the exchange argument of Claim 1 and an asymptotic construction in Claim 2. Lemma 2's "all but one coordinate" uses the piecewise linearity of every .
Arms are Fin N, recovery functions ℕ → ℝ with the four admissibility conditions; the paper's is not assumed. A schedule is a finite set of pull times in , and every first gap is measured from time . and are suprema of the optimization problems themselves, and is the real Filter.limsup over of a sequence bounded in ; is never defined by the closed form of Lemma 1. Periods live in WithTop ℕ with . Concavity on means non-increasing increments. Algorithm 1 and Algorithm 2 are relations on runs: every choice the paper leaves open (the optimal , the maximizer , the grouping, the offsets, ties in the top- selection) is free, and the goal quantifies over all of them while also asserting that a run exists. That existence clause, and the requirement that groups number at most and that the selection be of maximal reward, rule out a vacuous relation or a trivially weak selection. The term is with chosen before the instance, so it cannot absorb the growth in .
Not part of this mission: Theorem 2 (tightness), the online learning results (Theorem 3, Corollary 1, Proposition 2), the refined ratio of §6, and the running-time clauses of Lemma 4.
Contributions welcome: proofs of the milestones in any order; a general library for the upper concave envelope of a function on and its supporting points; the 1-PPP construction for periods with a common odd part.
In adversarial online learning a learner chooses one of actions (arms) in each of rounds and suffers a loss in . Classical regret bounds grow with the horizon, . A small-loss bound replaces by the loss of the best arm, which matters whenever good actions exist: routing traffic, choosing treatments, recommending items. With full information (all losses revealed each round) such bounds are standard. With partial information, where only some losses are observed, they were known only for pseudo-regret in special cases, as discussed in Lykouris, Sridharan and Tardos (arXiv:1711.03639v5), §1.2.
That paper gives a black-box reduction: any full-information learner with a small-loss guarantee becomes a learner for graph feedback with a high-probability small-loss guarantee. The bound depends on the independence number of the feedback graphs instead of the number of arms. This mission formalizes the reduction's central high-probability statement, Theorem 3.6, together with the chain of claims its proof rests on.
Timeline:
There are arms. In round the adversary fixes an undirected feedback graph on the arms, which the learner sees before acting, and a loss vector . Both may depend on everything that happened in earlier rounds. The learner picks a distribution , an arm is drawn, and the learner observes for every in the closed neighbourhood (the arm and its neighbours). A natural number bounds the independent sets if no has more than pairwise non-adjacent arms.
The -approximate regret against an arm is
A full-information algorithm maps past loss vectors to a probability vector . It has the guarantee at parameter and range if for every loss sequence in and every arm .
The Double-Threshold Freezing Algorithm (Algorithm 1) takes , and and sets and . In each round it does the following.
Let and . Suppose every has independent sets of at most vertices and has the guarantee at on the range . Then Algorithm 1 satisfies
The milestones follow the order of the proof:
The theorem turns approximate-regret guarantees of full-information learners into high-probability guarantees under graph feedback. The bound scales with rather than and has no dependence on . With the doubling trick of Lemma 3.8 it gives the paper's high-probability small-loss regret (Theorem 3.9). The same framework yields the paper's results for semi-bandits, contextual bandits and shifting comparators (§5).
Status. The paper states the bound with constant , and that constant is false. A counterexample has , complete graphs, , and losses in every round. The learner has : it spends its regret budget on arm 1 first and then runs Hedge. Algorithm 1 then plays arm 1 for rounds with certainty, so , above the printed bound of about . The proof bounds the estimated losses by , but only holds (proof of Theorem 3.4). Carried through with , the proof gives , and the same family of instances shows that no smaller constant of this form works. No part of this chain has a machine-checked proof that this mission knows of. A complete formalization would check the corrected constant and the high-probability reduction.
The obvious approach uses importance weighting with uniform exploration, as in Exp3. It bounds the variance of the estimates through the loss of the worst arm, so it gives uniform rather than small-loss bounds. Freezing avoids this, but freezing one arm lowers the observation probability of its neighbours and can cascade. The central combinatorial step, Claim 3.3, bounds the cascade by a charging argument along the freezing order. The probabilistic difficulty is that the estimated losses fed to depend on the arms drawn, so the three concentration steps need a martingale (adapted) Chernoff bound with multiplicative error (Lemma 3.7) rather than Hoeffding's inequality. The final chain also has to track the estimator range correctly, which is exactly where the printed proof slips.
Arms are Fin d and graphs are SimpleGraph (Fin d); closed neighbourhoods include the arm itself. Rounds are -based and arm paths are Fin T → Fin d. The adversary is a deterministic map from the earlier arms to ; randomized adversaries are mixtures of deterministic ones. is a deterministic map from the list of past (estimated) loss vectors to a probability vector, and its guarantee is assumed only at , and horizon . Probabilities are sums of path probabilities , which sum to one. The bound is stated for all comparator arms at once, inside one event. The logarithm is natural. When every arm carrying probability is frozen (possible only for , i.e. ), the algorithm plays ; the goal is trivial there.
The goal is not vacuous. A learner with the guarantee and an adversary with nonempty graphs satisfying the bound exist; the path probabilities sum to ; and the event is not empty in general (the counterexample makes it certain for the constant ). Lemma 3.7 is stated for an arbitrary filtration in Mathlib's measure-theoretic language and is reusable on its own. Contributions are welcome on each claim separately, on Lemma 3.7, and on a bridge from the path-sum model to Lemma 3.7.
Two-player zero-sum extensive-form games (poker, negotiation, security games) are solved at scale by first-order methods. Writing each player's strategy in sequence form turns the computation of a Nash equilibrium into a bilinear saddle-point problem over two polytopes, and methods such as Nesterov's excessive gap technique (EGT) and Nemirovski's mirror prox solve it at rate . Both need a distance-generating function (DGF) on each polytope, and their convergence bounds scale with the DGF's range divided by its strong-convexity modulus.
Hoda, Gilpin, Peña and Sandholm (2010) introduced dilated DGFs, which keep the proximal step computable in linear time. Kroer, Waugh, Kılınç-Karzan and Sandholm (2020) gave the dilated entropy explicit weights with modulus in , but their weights double at every level of the decision tree, so the range of the DGF grows like in the depth . Farina, Kroer and Sandholm (arXiv:2105.12954v2, 2021; Operations Research, 2025) remove this exponential factor with the dilatable global entropy.
A sequential decision problem has a finite set of decision points; at each a finite nonempty set of actions ; and for each a parent sequence , the last decision point–action pair before , or the empty sequence if the player has not acted yet. The decision points form a tree. The sequences are , and is the set of decision points that follow .
The sequence-form polytope is
and . The weights are defined from the leaves up by
with . The dilatable global entropy (Definition 4) is
and the dilated entropy with the same weights is . In Lean these are seqFormPolytope, MQ, gamma, gammaRoot, weight, dge and dilatedEntropy over a SeqDecisionProblem.
For every sequential decision problem:
In proof order: the weights satisfy and (Definition 4); on (Theorem 3); ; on , with the uniform strategy as its unique zero; Theorem 4; Theorem 5; is largest at root decision points and ; and on .
The range bound, divided by the modulus, is the constant in the rates of EGT and mirror prox. The Kroer et al. dilated entropy achieves range at the same modulus. The dilatable global entropy improves it by the factor , and because it coincides with a dilated entropy on (Theorem 3), its proximal step keeps the linear-time closed form. In deep but narrow trees, where the number of decision points is linear in the depth, this replaces an exponential constant by a polynomial one.
The results are proved in the paper. No machine-checked version exists. The mission adds to the platform sequence-form strategies, tree-form decision problems and distance-generating functions on polytopes with boundary, none of which it has yet. Theorem 6 is formalized in corrected form: as printed it bounds the Bregman diameter , which is infinite, while its proof bounds , which is the quantity the convergence theorems use.
The ingredients are elementary, but none is a one-line unfolding. Theorem 3 telescopes logarithms across the tree using the flow constraints of , so it needs an induction over the tree. The minimum and its uniqueness are statements about every decision point at once, through entropy bounds on conditional distributions. For Theorems 4 and 5, the Hessian bound on must be turned into the gradient-monotonicity form of Definition 1 on , where is not twice differentiable at the boundary. The relative interior must first be identified: the open cube of the printed proof contains no point of , because . The bound relates a recursively defined weight to a maximum over the whole polytope.
A decision problem is a structure with a finite type of decision points, finite nonempty action types, a parent map into Option (Σ j, A j) (none is ) and a well-founded child relation. There may be several roots, and may be empty. The weights are defined by WellFounded.fix. is the formula of Definition 4 on all of with Mathlib's Real.log (), and is fderiv ℝ (dge P) x v. Because is tangent to , the extension off does not affect the inequalities. The relative interior is intrinsicInterior ℝ. The and norms are explicit sums, since Mathlib's norm on Seq P → ℝ is the sup norm. is an sSup over counting . is the logarithm of the largest , which is when is empty.
The DGF clause keeps differentiability on as a separate conjunct, so the strong-convexity clauses cannot hold through a junk derivative. The platform's existing DGF definitions require differentiability on all of , which the entropy lacks at the boundary, and are not used. A sanity file checks on the one-decision-point, two-action problem that , that the uniform strategy lies in , and that the range clause is not trivial.
Contributions of general use are welcome: induction principles for tree-form decision problems, the bound , and a lemma turning a Hessian lower bound on a relatively open convex set into gradient monotonicity.
Rank-based rewards are the standard incentive in sales tournaments, research prizes and promotion contests. Seel and Strack (Gambling in contests, J. Econ. Theory 2013) showed that such contests can be analysed as games of risk taking, in which each player chooses when to stop a privately observed diffusion. Nutz and Zhang (Reward design in risk-taking contests, SIAM J. Financial Math. 2022) solve the finite-player version with players. The mean field limit was treated by Nutz and Zhang in the source of this mission (arXiv:2103.04219, published in Math. Oper. Res. 2023, doi:10.1287/moor.2022.1297). The reward is an arbitrary decreasing function of rank, which may have jumps and flat stretches. Such rewards are the ones used in practice (a prize for the top decile, say), and they make the equilibrium singular: it has atoms and gaps.
A reward function is a decreasing, right-continuous with . Write and .
A continuum of players each observes an independent copy of , absorbed at , with and . Each player chooses a possibly randomized stopping time . The set of feasible laws consists of the laws of under the absorbed dynamics.
If the other players stop with law , a player who stops at has rank and receives when has no atom at , and otherwise averaged over , which splits ties uniformly. Call this payoff . A mean field equilibrium is an with for all . The value function is the supremum of over the laws reachable from a start at .
Let be the scale function of , normalized by , , and let and
For there is exactly one mean field equilibrium. Its cdf and value function are
It is carried by , with and in its support, where . Its atoms are in bijection with the level sets of having more than one point. The value identity is stated at every starting level .
Lemma 2.1 characterizes by if and if . The existence half of Theorem 2.2 follows. Lemmas 3.1, 3.2, 3.6 and Remark 3.3 relate flat stretches of the reward to atoms and jumps of the reward to gaps. The §3.2 identity
and display (3.4), , recast equilibrium as a minimization. Lemmas 3.7, 3.8 and 3.9 analyse the minimizer, and the uniqueness half closes the argument.
The theorem gives one equilibrium for every rank-based reward with , in closed form, which is what the optimal reward design of the paper's Section 4 and the comparison with the -player game in its Section 5 rest on. Discontinuous rewards are the case in which the mean field model separates from the finite game: the equilibrium is -Nash in the -player game exactly when is continuous.
All of these results are proved in the source, apart from Lemma 2.1, which the source cites. None of them is proved in Mathlib or on the platform (searched 2026-10-31). This mission states them in Lean. A completed development would add stopped Brownian motion with drift and absorption, a law-level Skorokhod embedding for it (Hall, Embedding submartingales in Wiener processes with drift, J. Appl. Probab. 1969), and a worked equilibrium analysis through concave envelopes.
The obvious argument is to verify the candidate and then compare any other equilibrium with it through first-order conditions, as a density-based mean field analysis would. That fails here: an equilibrium may have atoms and gaps at arbitrary locations, so it has no density, and is not invertible. Uniqueness instead needs perturbations of a measure that keep it inside and strictly improve a deviation, together with a minimization over of a concave envelope, carried out with ties present. Lemma 2.1 is itself substantial: the paper cites it, and a proof needs embedding and optional sampling for , with the three regimes of behaving differently at infinity and at the absorbing boundary.
The Lean development fixes the following conventions.
feasibleLaws: laws of with the first time , over all Type carrying a filtration , a -Brownian motion (EllsbergLearning.IsBrownianWrt) and a finite -stopping time. A randomized stopping time is a stopping time of a larger filtration. Stopping positions are required a.e.-measurable, so the zero measure is not feasible.EReal; ; conc is TractableComposite.concOn.The formalization has no shortcut definitions: is not defined by Lemma 2.1's condition, is not defined by the envelope, and equilibrium is not defined by (2.3), so none of these results is definitional.
The source's statements are corrected or read as follows.
Needed infrastructure: optional stopping and embedding for drifted Brownian motion, generalized inverses of monotone functions, Stieltjes measures from cdfs, and concave envelopes of bounded monotone functions on an interval. The reusable parts are Lemma 2.1 and this inverse and envelope layer. Proofs of Lemma 2.1 stated as a general result on absorbed diffusions, or proofs that bypass the paper's perturbations, are welcome.
During online shopping holidays an e-commerce seller depends on a third-party carrier to deliver every unit it sells. Peak demand is far above normal and hard to forecast, and carriers have responded with surcharges for sellers whose shipping volume exceeds the capacity they reserved (the paper cites UPS's 2017 plan, p. 9). Song and Zhao (SSRN 3129499; version of record MSOM 2021, doi:10.1287/msom.2021.1008) model this as a Stackelberg game between a shipper and a seller and ask which shipping contract can make the decentralized pair act like one integrated firm. The classical supplier–retailer theory (Cachon, Supply Chain Coordination with Contracts, 2003) says that a single wholesale price coordinates only if the supplier earns nothing. This mission formalizes the paper's flat-rate half of the answer: a single per-unit shipping rate does coordinate the seller–shipper chain, and it leaves the shipper a positive expected profit whenever emergency capacity costs more than regular capacity, and the seller one whenever its margin exceeds the regular shipping cost.
A seller sells one product in one season at price , buys at cost and salvages leftovers at , with . Its overage and underage costs are and . The demand is random with finite mean and c.d.f. , continuous and strictly increasing on .
A contract charges a base rate per unit shipped, a penalty per unit of over-reservation and per unit of under-reservation. The flat rate is ; the paper's coordination results use " or ". A contract is feasible when , and .
The shipper announces . The seller chooses a reservation and inventory . The shipper then builds regular capacity at unit cost , and in season covers any excess shipment with emergency capacity at unit cost . With shipment and , the profits are
and an integrated chain would earn , assuming . A best response is a maximizer over nonnegative decisions. A first best is a maximizer of . A contract coordinates the chain when best responses exist and every pair of best responses is a first best.
The switch condition is (case a); case b is its negation. The coordinating flat rate is in case a and in case b.
The flat rate is feasible and coordinates the chain. For every feasible coordinating contract with or and all best responses and ,
The paper says that both profits "can be greater than zero". Its proof derives a strict inequality in every instance, but the strict step fails when the relevant fractile is . The goal states the exact conditions.
Theorem 8 is the flat-rate half of the paper's main comparison. A carrier can align a seller's inventory and its own capacity with first-best decisions using one per-unit rate that depends only on the cost parameters, and still keep a positive margin. In case b the rate sits strictly between and , so part of the emergency-capacity risk stays with the shipper.
The other half of the comparison is out of scope here. The paper also claims that "the risk penalty coordinates only if the shipper makes zero profit" (Theorem 5's "only if"). At fixed parameters this is false. With , , , , , the contract satisfies every assumption, coordinates the chain for every demand law of the model, and earns the shipper under Uniform demand. The flat-rate result does not depend on that claim.
The results are proved on paper only. None of them has a machine-checked proof yet. A formal proof would check the case analysis and make explicit the edge cases the paper's argument misses: , , and demand laws with bounded support.
The chain's cost is not convex in , because couples inventory and capacity. A first-order condition in both variables at once gives a stationary point that need not be optimal. The first best is found by minimizing over on each side of and gluing two convex one-dimensional problems. Lemma 2 makes that possible, and its printed third bullet is false in . Best responses are characterized here from the c.d.f. alone, with no density, so the Leibniz-rule derivatives of the paper are not available as stated. The strict sign of each profit needs , which needs to be strictly increasing on an interval below .
The demand is a probability measure μ on ℝ, and is ProbabilityTheory.cdf μ. The standing assumptions are a.s., Integrable identity, continuous, and strictly increasing on . No density is assumed. Each is written as a point with ; the assumptions make that point unique for . The procurement cost is cProc, the capacity cap, and is uE. The switch condition is used multiplied out, . Expectations are Bochner integrals, and finite mean makes them honest. Decisions range over the nonnegative reals.
The seller's, the shipper's and the chain's optimal decisions are argmax predicates over the profits (3.2), (4.5), (5.7), never closed forms, so the theorems are not algebra about . Coordinates contains an existence clause, so a contract without best responses cannot coordinate vacuously.
A complete development needs newsvendor-type arguments from a c.d.f. without densities, the layer-cake identity , and convexity of expectations of piecewise-linear integrands. These pieces are reusable in other newsvendor and capacity models. Proofs of any milestone are welcome, and so are alternative routes to Theorem 7 that avoid the case analysis.
Banks, insurers and asset managers evaluate portfolios with risk measures such as Value-at-Risk (VaR) and Expected Shortfall (ES), which regulators prescribe (BCBS 2019). A recurring question is how much a portfolio benefits from pooling its components. The indices in use, the diversification ratio and the diversification benefit, can be negative, change when a risk-free asset is added, and are not quasi-convex in portfolio weights. Han, Lin and Wang (arXiv:2206.13679, Management Science 2025) propose seven axioms for a diversification index and prove that, for a non-linear coherent risk measure, they characterize a new index, the diversification quotient (DQ). This mission formalizes that characterization.
is a probability space and the space of essentially bounded random variables, almost surely equal ones identified; is a loss. A risk measure is a map . It is monotone [M] if , constant additive [CA] if , positively homogeneous [PH] if for , and subadditive [SA] if . It is MCP under [M], [CA], [PH], coherent under all four, and linear if for all real .
A diversification index for assets is a map . Write and when for all . The axioms are: [+] ; [LI] for ; [SI] for ; [R] if and ; [N] , , and whenever some has for all and ; [C] if and then ; [PC] is convex for every and .
Given , , a decreasing class ( for ) and , the diversification quotient is
For the ES family, measures how far the confidence level can be relaxed before the pooled risk exceeds the sum of the individual risks at level .
For and a non-linear coherent ,
It is stated as printed, with the printed [C] and real-valued risk measures, except that the probability space need not be atomless (no step of the proof uses that).
Theorem 1 is corrected. (C1) The constructed can be identically , so the class of the "only if" direction must allow values in : with , and , no real-valued class with represents . (C2) With a DQ can take the value , and the printed [C] then fails (take ); Theorem 1 uses the semi-continuous form , which the page names ("a special form of semi-continuity", p.8). Neither correction affects Theorem 2, whose indices satisfy .
Theorem 2 identifies DQ as the index of diversification consistent with coherent risk measurement: it is non-negative, location and scale invariant, monotone in the aggregate loss, normalized at duplicate portfolios, and quasi-convex in weights. For ES, DQ has closed forms and portfolio optimization reduces to linear programs (§§4–6 of the paper), so the axioms lead to a computable index.
The result is proved on paper. As far as this mission's search found, no part of it, nor any theory of diversification indices, is machine-checked. A formal proof would check the two corrections to Theorem 1 and the steps the printed proofs pass over: the case in claim (e), the bound needed to apply the convex-hull identity at levels , and the common scaling that requires .
The "if" direction is a computation, except for continuity at the boundary of . The "only if" direction must produce a family of risk measures from alone. The natural candidate, a sublevel set of , lives on , while a risk measure acts on ; the bridge is , and showing that the induced reproduce exactly needs claim (e), a one-sided continuity obtained from [C]. In Theorem 2, [PC] only speaks about portfolios over a single vector , while coherence of compares arbitrary pairs of positions; the step that writes two acceptable positions as portfolios of one four-asset vector needs non-linearity of .
is MeasureTheory.Lp ℝ ⊤ P with IsProbabilityMeasure P, ordered almost surely; constants are Lp.const ⊤ P c; the convergence in [C] is that of ‖Lp.posPart (S X - S (Y k))‖. Portfolios are Fin n → Lp ℝ ⊤ P. Indices and the extended values of Theorem 1 are EReal. In the infimum is the EReal infimum capped by , never the real sInf (which is on the empty set); a proved sanity check exercises the empty case. The right-hand side of the goal is shown to be inhabited by a non-trivial class on a two-point space with and . Classes are maps ℝ → Lp ℝ ⊤ P → ℝ of which only the members indexed by matter.
A complete development needs basic facts about classes (order, norm, positive part), acceptance sets of MCP risk measures, and quasi-convexity on the standard simplex. The risk-measure predicates and the acceptance-set construction are reusable for other work on law-based risk measures. Proofs of any milestone, alternative arguments, and reusable lemmas on risk measures are welcome.
Hotels, airlines and car-rental firms routinely give a customer a better product than the one requested, at the price of the requested one. The classical practice is the reactive upgrade: the upgrade is offered only once the requested product is sold out. Chen, Tang, Wang, Wang and Yu (SSRN 3777846; published in Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2022.1084) study the proactive upgrade, in which the seller may offer the upgrade even while the requested product is still in stock. Giving away a more expensive unit early can pay off when the cheaper product is scarce relative to its future demand, and the paper characterizes exactly when it does.
The structural tool is anti-multimodularity of the value function, a lattice property related to the multimodularity of Hajek (1985), which Altman, Gaujal and Hordijk (2000), Koole (2004) and Li and Yu (2014) used for queueing and inventory control. Koole (2004) records that multimodularity is preserved by some controlled operators but not by uncontrolled ones alone, and the paper's operator conditions on two coordinates at once.
A seller holds a fixed stock of products with prices over periods. In each period one customer arrives with probability . A customer requests product with the multinomial-logit probability
where is the probability of no request and is the price sensitivity. A customer who requests and is offered a free upgrade to accepts with probability , given by formula (3) of the paper, and pays in either case. Write for the -th unit vector and .
The optimal profit function is defined by and the optimality equation
Here the operator sells product if it is in stock. When , it takes the larger of the no-offer value and the offer value . The thresholds are
Both are functions of the inventories of the products other than . A function is anti-multimodular if for distinct , where .
For every , , period and inventory :
and the policy that offers exactly in these cases is optimal among all proactive upgrade policies, with revenue . No constant is fixed. The thresholds are defined from , and the content is that the sets defining them are upward closed in .
Theorem 3 reduces the seller's decision from a function of the whole inventory vector to a comparison of one coordinate with two numbers. Proposition 5 of the paper and its numerical study (§5, §6.2) build on this structure. For two products the paper also shows that the optimal proactive policy earns at least as much as the optimal reactive one (Corollary 1, p.19). The result for two products is Theorem 2, and Theorem 3 generalizes it to products.
The paper proves the results; none of them is formalized. A formalization would supply the preservation argument for a two-variable controlled operator, which the paper's Remark 2 says existing results do not cover, and a library of multimodularity facts for variables. The paper omits the proof for and states several subcases of the nine-case proof with index slips. A checked proof would settle both.
The obvious approach is induction over periods: show that each operator in (14) maps anti-multimodular functions to anti-multimodular functions. This fails as stated, because a maximum of anti-multimodular functions is not anti-multimodular in general. The operator also switches form at the boundaries and . Anti-multimodularity at is therefore not enough. The induction must also carry Lemma A.5, which fixes which branch of the maximum is taken near the boundary, and the anti-multimodularity of both parts of the split at an empty coordinate. The resulting case analysis has nine cases with further subcases at and . Every second-difference inequality must also be routed through points of the quadrant, since is defined only there.
Fin m (0-based) and inventories Fin m → ℕ. is used only under , and successor indices carry the proof i.val + 1 < m.ℕ∞, with on an empty set, so no junk value can make every offer optimal.A formalization in which is an arbitrary function, a maximum is replaced by one branch, or the sale of product is read as forced, would make the goal empty. Here the recursion is fixed, and clause (d) proves optimality over policies.
Contributions welcome: the Lemma A-series for general on the quadrant (reusable for any multimodular control problem), Lemma 3 as a statement about recursions on product chains, and the case analysis of the preservation claims.
Many welfare-maximization problems in mechanism design are NP-hard: combinatorial auctions, packing integer programs, unsplittable flow, maximum traveling salesman. The standard algorithmic answer is relax-and-round: solve a fractional relaxation exactly, then round the fractional solution to a feasible one. Turning such an algorithm into a mechanism is the difficulty. Truthful or truthful-in-expectation mechanisms built from approximation algorithms either apply only to special (monotone, maximal-in-range, convex) rounding procedures or sacrifice solution quality on every instance (Dütting, Kesselheim, Tardos 2015, §1.2).
The alternative studied here is to keep the algorithm and charge pay-your-bid prices, then bound the welfare of every equilibrium through the smoothness framework of Roughgarden and of Syrgkanis and Tardos (STOC 2013). The paper shows that a rounding scheme which does not look at the objective preserves smoothness up to a factor depending only on its approximation ratio. Applications in the paper give Price of Anarchy bounds for sparse packing integer programs, single-source unsplittable flow, maximum traveling salesman and XOS combinatorial auctions.
There is a finite set of agents. The relaxed outcome space is a measurable space and the original outcomes form a subset . Each agent has a class (Val i) of nonnegative weight functions ; its valuation and its bid both come from . The classes are closed under halving (HalfClosed).
A mechanism (Mechanism) maps a bid profile to the law of a random outcome and to expected payments . Agent 's utility (utility) is . The mechanism is pay-your-bid (IsPayYourBid) if . It is an exact declared welfare maximizer over a feasible set (IsExactMaximizer) if almost surely maximizes over .
A mechanism is -smooth (IsSmooth), , if for every valuation profile each agent has a possibly randomized deviation , depending only on and , such that for every bid profile
It is smooth for deviations to half the value (IsSmoothHalf) when works.
An -approximate oblivious rounding scheme (IsObliviousRounding) is a Markov kernel from to itself, with , whose output lies in almost surely and which satisfies, for every relaxed solution , every agent and every ,
A mechanism is obtained from by rounding (IsRounded) if its outcome is the outcome of followed by .
If is pay-your-bid, -smooth over , and an exact declared welfare maximizer over , and is a pay-your-bid mechanism obtained from through an -approximate oblivious rounding scheme, then
The goal follows from Lemma 1, Theorem 3′ at , and the semi-smoothness step.
Combined with the theorem of Syrgkanis and Tardos (Theorem 2 of the paper, which also needs agents to be able to withdraw), Theorem 3 turns a Price of Anarchy bound proved by smoothness for the relaxed mechanism into a bound for the rounded mechanism, valid for mixed Nash, Bayes–Nash and coarse correlated equilibria (Corollary 1). Every application section of the paper is an instance: it supplies a smooth relaxation and an oblivious rounding, and reads off a Price of Anarchy bound. The theorem is the only mechanism-design component of those applications; the rest is the cited rounding schemes.
The result is proved in the paper; no machine-checked proof of it or of its lemmas is known. The mission produces a formal account of -smooth mechanisms with randomized outcome rules and randomized deviations, of oblivious rounding schemes as Markov kernels, and of the VCG mechanism for a randomized exact maximizer on an arbitrary measurable outcome space. These objects are reusable for the paper's applications and for other smoothness results.
Rounding preserves the value an agent gets at a fixed relaxed solution. Smoothness instead compares the equilibrium with an unknown, possibly randomized deviation chosen by the smoothness proof of , and the relaxed solution changes with that deviation. So the arbitrary deviation cannot be pushed through the rounding directly. It first has to be replaced by the fixed deviation , and that step (Lemma 1) needs exactness of and a comparison with a truthful VCG mechanism on the same randomized outcome rule. The rounding guarantee is then used twice, in opposite directions, at two different relaxed solutions: once on the deviating profile and once on the original one. Both uses need the guarantee for each agent's weight separately; a guarantee on the total weight alone does not suffice.
In Lean the work is measure-theoretic: utilities are Bochner integrals, the rounding guarantee is a lower Lebesgue integral, and the two meet through Measure.bind with only almost-everywhere measurability available.
Agents form any finite type N; the relaxed outcome space Ω' is any measurable space and Ω : Set Ω'. Weights are Ω' → ℝ≥0; a profile is a plain function N → Ω' → ℝ≥0, and IsProfile Val b says each b i ∈ Val i. Mechanisms are total on all profiles; every property constrains them on profiles only. Outcome laws are probability measures, so a deterministic rule is a Dirac law. Payments are recorded as real expected payments. ExpFinite makes every weight integrable under every outcome law, so no Bochner integral is a junk 0. A randomized deviation (RandomBid) is a random variable into Val i on an arbitrary probability space. The maximum over feasible outcomes is replaced by "for every feasible x". The relaxation's feasible set is Set.univ, the original problem's is Ω.
The weight classes are a parameter on purpose. With Val i equal to all functions, no oblivious rounding exists when (take the indicator of a point outside ), and the goal would be vacuous. The feasibility clause of the rounding excludes the identity kernel as a trivial 1-approximation, and the kernel sees only the relaxed solution. A sanity instance (one item, two agents, fractional allocations, linear valuations, first-price relaxation, independent rounding) satisfies every hypothesis of the goal with , , and .
Contributions welcome: proofs of the milestones in any order, general lemmas on Measure.bind with almost-everywhere measurable integrands, and the VCG facts for randomized exact maximizers, which are reusable on their own.
Additive convexity is the structural property behind the tractability of serial inventory theory. Clark and Scarf (1960) showed that the multi-variate value functions of a serial inventory system are sums of univariate convex functions of the echelon inventory levels. This gives the optimality of echelon base-stock policies and replaces a high-dimensional dynamic program by univariate ones. Later work found the same structure in assembly systems, in systems with expediting, and in systems with advance demand information.
Gong and Wang (doi:10.1287/opre.2020.2064; SSRN 3217007) isolate one reason why this structure persists. It is a statement about real functions: a class of minimizations, with no stochastic model attached, under which additive convexity passes from the objective to the value function. They use it to give short proofs of results of Zhou, Tao and Chao (2011) and Bao, Liu, Yu and Zhang (2018), and to analyse a serial system with expediting and dynamic capacity management with upgrading. This mission formalizes the first of its two preservation results. The second, for disposal problems, is derived in the paper from the first.
Throughout, "increasing" means non-decreasing, and is a convex subset of . For the chain domain is
A function on is additively convex if on for functions , each convex on the projection of on coordinate .
Fix . The transformation problem moves amounts into the low coordinates. Its feasible set is
and its value is
At the bound is absent. The serial problem has the larger feasible set , which replaces the ordering of the differences by for each .
If is additively convex and increasing in , and is the minimum above, then:
and for and real , every slope bound passes from to :
over pairs in that agree off coordinate with .
Under the monotonicity of alone, the transformation problem and the serial problem have the same minimum.
For convex on , with right ends in a set above :
with convex increasing on and convex decreasing on , for every pair at which the minimum exists (no attainment is assumed: a convex function on with a jump at can lack one), and the explicit form of and at a minimizer of , where the minimum always exists.
The decomposition , with no term at .
The third clause of the goal, stated on its own and without additive convexity of .
The result. Theorem 1 gives a model-free test: to show that a value function with prioritized decisions is additively convex, recognize the minimization as problem (1). Lemma 1 explains why the test works, since a transformation problem with prioritized decisions is a serial inventory problem with zero lead times. The sensitivity clause is what the paper adds to the classical preservation of additive convexity.
Formalizing it. The result is proved in the paper, with Lemma EC.1 quoted without proof from Karush (1959). A prior-art search of the platform found no statement of additive convexity or of Karush's lemma. This mission produces a statement of Theorem 1 that makes its implicit conventions explicit, and a form of Karush's lemma that is reusable in inventory theory.
Moving a resource couples two adjacent coordinates, so separability of does not pass through the minimization on its face. The feasible set ties each to and on both sides. The obvious elimination of in turn through minimizers does not go through as written: a convex need not have a minimizer, it may jump at an end of its domain, and the have different domains, for and the upward closure of otherwise. The right end of a stage's interval can lie outside the domain of that stage's function, and at no coordinate pins it.
Points of are Fin (n + 1) → ℝ, with indices as in the paper. Coordinates are free above ; in particular gives them no upper bound. A feasible is stored together with the tail as one vector , which handles uniformly.
means an attained minimum. The goal assumes IsLeast (f '' transformSet I k x) (g x) for every . It is not sInf. The minimum can fail to exist under every printed hypothesis: with , , , the feasible points , , give . Attainment is the only such hypothesis: no continuity, closedness or compactness is assumed, because the can jump at the ends of their domains.
The sensitivity clause is stated without differentiability. The theorem assumes convexity only, and need not be differentiable, so "" is the slope bound above, for real of any sign. It specializes to the printed clause: a derivative bound gives the slope bound on a section of , and a slope bound gives every existing derivative at most . The case is not claimed.
Univariate convexity is on coordinate projections, not on , because the paper's applications use functions that are convex only on a half-line. "Increasing in " compares only points of agreeing off coordinate .
The statement has trivializing readings, which the definitions exclude. Dropping the chain or the ordering of differences in would separate the problem, and additive convexity without convexity of the would be free.
The needed library is one-variable convex analysis on subsets of , including non-closed intervals and functions discontinuous at endpoints. Karush's lemma with a general right-end set is reusable beyond this mission. Proofs of the milestones in any order are welcome, as are alternative proofs of Lemma EC.1.
Many firms let their salespeople set prices. A salesperson who spends effort talking to a customer can learn what that customer is willing to pay and quote a price close to it; a salesperson who skips that effort can only quote a price that works on average. The firm sees neither the effort nor the customer's value, only the revenue of each sale, and it can only pay the salesperson as a function of that revenue. Atasu, Ciocan and Désir (SSRN 3931055, INSEAD Working Paper 2022/06/TOM; published in Management Science, 2023, doi:10.1287/mnsc.2023.4939) ask how the firm should pay a salesperson for whom learning is costly, when payments cannot be negative (limited liability) and when the firm has fewer units than customers.
Without limited liability the answer is classical: with risk-neutral parties, "selling the firm" to the agent through a linear contract achieves the first-best payoff (Laffont and Martimort 2009, cited by the paper on p.11). Limited liability rules this out, and a firm with scarce inventory must in addition stop the agent from selling to low-value customers. The paper's answer for one customer (Corollary 3) and for many customers with limited inventory (Corollary 5) is that simple contracts get arbitrarily close to first best. This mission formalizes the multiple-customer result.
A customer's willingness-to-pay is a continuous random variable on with density , survival function , and finite mean. Learning costs the agent . Two standing assumptions are made: Assumption 1, (learning is worth inducing for a single customer), and Assumption 2, the failure rate is non-decreasing.
There are customers with independent values drawn from this law and units, , with . The paper studies a fluid model: inventory need only hold in expectation, and the theorem is about this deterministic relaxation, not about the stochastic dynamic problem. A policy learns customer 's value with probability , then quotes the price ; otherwise it quotes the uninformed price . Prices lie in , where means no sale. The expected inventory use , revenue and learning cost are finite sums of one-customer expectations, and (inventory) is .
A static separable contract pays for each sale revenue , where is non-decreasing, , and . Its expected cost under is , the agent's utility is , (IC-multi) says that maximizes over all inventory-feasible policies, and (participation-multi) says . The first-best payoff is the supremum of over inventory-feasible policies: the payoff when effort is observable.
Dualizing (inventory) with a multiplier gives
The multiplier acts as a reservation price. Its zero-crossing value and the uninformed price split into three regimes: full learning , partial learning (learn with probability ), and no learning (Proposition 4).
For the first-best policy of Proposition 4 and every there is a static separable contract with
such that satisfies (IC-multi) and (participation-multi). The goal keeps every regime, the paper's monotone contract class and (IC-multi) over all inventory-feasible policies.
The result says that under limited liability and limited inventory the firm needs neither dynamic nor history-dependent contracts to approach first best. A per-sale commission schedule that pays nothing below the shadow price of inventory, then rises like , and is capped at is enough. It also shows that the shadow price of the firm's inventory problem is the reservation price that makes the agent's own problem respect inventory.
The paper's proofs leave several gaps that a formalization closes. Lemma 8's limit is printed as ; it is the learning cost , which is under full learning. The claim that is unique fails when the failure rate jumps, so the mission works with any minimizer. The identity needs . The printed no-learning contract is not monotone and so lies outside the paper's own class. The goal keeps the class, which the contract satisfies. The results are proved on paper; none is formalized elsewhere to our knowledge.
The obvious idea, giving the agent a share of revenue, fails: limited liability forbids the fixed fee that makes a linear contract first best, and a pure revenue share leaves a rent bounded away from zero (Table 1 of the paper). The contract has to make the agent indifferent among all uninformed prices, which forces and an infinite expected payment unless it is capped. Every part of the proof is one-variable real analysis, but it needs care. must be handled as a convex function of without assuming that is differentiable, which the paper's first-order conditions take for granted. (IC-multi) must be checked against every inventory-feasible deviation, including randomized learning and arbitrary measurable informed price policies. The single-customer problem of Lemma 6 is an infinite-dimensional linear program, solved in the paper by an omitted primal–dual argument.
Lean represents the law by a measurable density vanishing on , with total mass , finite mean, and positive mass on every interval of . Expectations are integrals over against . Customers are indexed by Fin N. Prices are elements of (ℝ≥0∞), with the no-sale price. Informed price policies are measurable, so all expectations exist. and are real suprema, shown attained in the milestones. uses , which gives the larger value and so the stronger goal. The contract takes the value for every , as the reservation constraint requires. The incentive constraint of Lemma 6 is a bound at every .
A trivializing encoding is ruled out. Expectations of non-measurable deviations would be junk values, which measurability forbids. A first-best value taken over a set that is unbounded or empty would default to ; it is shown to be attained. The goal is about the policy of Proposition 4 and asks for a contract in the paper's class, not about some policy or an arbitrary transfer.
The development needs elementary facts about survival functions (continuity, strict monotonicity, ), log-concavity of under a monotone failure rate, convexity of suprema of affine functions, and the change of variables for . These are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Lemma 6 that avoid the infinite linear program.
The simplex method moves between bases of a linear program, and its running time is governed by the pivot rule that picks the next basis. Whether some pivot rule needs only polynomially many pivots is a central open question in linear optimization. It is open even for 0/1-LPs, where the feasible region is a polytope whose vertices lie in , although the graph of such a polytope has diameter at most its dimension (Naddef 1989).
The obstacle is degeneracy. 0/1 polytopes are highly degenerate, perturbing one destroys the 0/1 structure, and a basis exchange need not move the current vertex. A first step, posed as Question 1 of the source and attributed there to Kortenkamp, Richter-Gebert, Sarangarajan and Ziegler 1997, is a rule that guarantees polynomially many non-degenerate pivots. Black, De Loera, Kafer and Sanità give an affirmative answer. This mission formalizes their strongest result, Theorem 3: the Ordered Shadow pivot rule reaches an optimum in at most non-degenerate pivots, where is the dimension of the polytope and not the number of variables.
An LP of form (1) has variables, equalities and further inequalities:
with feasible region . It is a 0/1-LP when and is a nonempty bounded set whose extreme points lie in . has full row rank.
Adding one slack per inequality gives the standard form , , with . A basis is a set of linearly independent columns of . It is feasible when its basic solution is nonnegative, and the original part of that solution is the vertex of .
For a nonbasic column , the pivot direction is the unique with , and for all other nonbasic . Its original part is , and is the reduced cost. is optimal when all reduced costs are . A pivot on removes a column that attains the ratio test, and it is non-degenerate exactly when the vertex changes.
The basic cone is
From a starting vertex , let and for . A run from a feasible basis with vertex has two phases:
A lexicographic run also keeps every Phase 2 basis feasible for a perturbed right-hand side, which is the lexicographic leaving rule.
For every 0/1-LP with of full row rank and every feasible basis , the goal has three clauses:
The milestones follow the proof:
The result itself. The bound is tight on the cube and matches Naddef's diameter bound, so it yields monotone paths of the best possible length on every 0/1 polytope, reached by an actual pivot rule. It uses no perturbation of the polytope, no randomization and no special constraint format. It does not bound total pivots: the number of degenerate pivots remains open (Question 2 of the source).
Formalizing it. These results are proved on paper and, as far as the platform shows, not machine-checked; Naddef's undirected diameter bound is the nearest formalized result. Two proof steps of the source need repair. The printed proof of Lemma 6 stops at a test on pivot directions, which is weaker than the slope condition on the whole cone that its statement asserts, and the convexity step in the proof of Theorem 7 does not follow from the facts it cites. Both statements stand, by other arguments. A formal proof would settle these points and give the platform a reusable vocabulary of bases, pivot directions, basic cones, shadows and coherent paths.
An edge rule does not give a pivot rule. Non-degenerate pivots trace an edge path, but a pivot rule sees only the generators of , and at a degenerate vertex this cone can strictly contain the feasible cone. So the improving direction of largest slope among the generators need not be the Shadow rule's edge. The central step is the invariant that keeps the simplex method on the Shadow path. If satisfies the slope condition and is chosen with slope , then is optimal for and has reduced cost for it, so any pivot on keeps that optimality, whichever column leaves.
The natural length argument also fails. Corollary 1 is useless for this , because can take up to values on vertices. The length is controlled instead by a chain of faces of strictly increasing dimension, with the slope comparison reduced to the leading coefficient of a polynomial in . That step needs integral and the exact constant .
Coordinates are Fin n, so exponents of , the index function and are 1-based. Columns are Fin n ⊕ Fin p and rows are Fin m ⊕ Fin p. The inequalities are kept apart from , and only the other inequalities receive slacks. All data are real, and integrality of is a clause of IsZeroOneLP, so Theorem 7 and Lemmas 6 and 7 hold for a general LP. The pivot direction is defined by , which fixes the sign that the printed formula gets wrong. The dimension is Module.finrank ℝ (vectorSpan ℝ P). An edge is a pair with IsExtreme ℝ Q (segment ℝ x y). The upper path is the upper boundary of . The lexicographic rule is encoded by right-hand-side perturbation, for all sufficiently small , starting from the Phase 2 basis.
The count alone would hold for an empty run, and it is clause 1 that excludes this: runs exist for every feasible basis, including an optimal basis without the slope condition. Replacing the slope condition by a test on pivot directions is not allowed.
A complete development needs the correspondence between feasible bases and vertices, simplicial basic cones, adjacency under non-degenerate pivots, anti-cycling, and faces of 0/1 polytopes. Most of this is reusable for other pivot rules. Proofs of any milestone are welcome, as are alternative proofs of Lemma 6 and Theorem 7.
About 30 million tons of plastic waste reach the oceans every year (Baron et al.), and over 80% of it is estimated to enter from low- and middle-income coastal countries (Jambeck et al. 2015). Firms such as Plastic Bank and rePurpose Global try to prevent this by working with local recycling supply chains and financing the work through plastic offsets: a customer pays for a unit of ocean-bound plastic to be collected and recycled, as in the carbon market. Practitioners and certifiers ask that offsets satisfy additionality: an offset may only be sold on plastic that would not have been recycled without the firm.
Baron, Romero, Zhang and Zhou ask whether this requirement actually raises the firm's environmental and social impacts. For a profit-maximizing firm that sells only offsets, their answer is no in general. This mission formalizes that result, Proposition 5 of the paper, together with the chain of equilibrium results it rests on.
Let collectors each choose a volume at effort cost , and let a processor buy their plastic at unit price and sell it at the local price . Without a firm (the Benchmark Case) a collector picks , the total volume is , and the processor sets , giving
In Case O a firm pays a bonus per unit to the supply chain and sells offsets. Customers value an offset at plus a social value with , and the market has potential size . The volume and the supply chain's incomes become, by eq. (3) of the paper,
and the firm's profit is
The social impact is with , and the environmental impact is . With weights the objective is , and the firm solves problem (4):
The first constraint is additionality. The no-additionality variant replaces it by .
The goal is about the optimal solutions of problem (4) and of its no-additionality variant, for a profit maximizer (, ) with . It asserts that both problems have optimal solutions. Then, for every optimal of (4) and every optimal of the variant, with and :
The environmental inequality in the second line is strict when .
The milestones lead to this statement: Proposition 1 (benchmark equilibrium), eq. (2)–(3) (lower stages of Case O), Proposition 2(a) (reduction of (4) to a concave univariate problem for general weights), Corollary 1(a) (the for-profit optimum with additionality) and Corollary 3 (the for-profit optimum without it).
Proposition 5 is the paper's analytical answer to its question about additionality: the requirement is not uniformly good. When the offset market is large relative to , a for-profit firm subject to additionality offers a smaller bonus and recycles less than one free of it. The threshold shows that this is more likely when there are few collectors, when collection is costly, and when customers respond strongly to the bonus. That is a direct warning to firms and regulators who promote additionality.
The result is proved on paper; no machine-checked proof is known to exist. Formalization adds two things. The printed statement needs a correction, recorded below. The argument is also a complete, checkable equilibrium analysis of a three-stage model, and it fixes which domain each closed form holds on.
Neither optimum is the obvious one. The firm's objective is a concave quadratic in two variables, jointly concave only under Assumption 1(2), and it degenerates at equality. Corollary 3 has three regimes, in which the volume constraint binds, the bonus vanishes, or both, and each must be matched to the printed / expression.
The tempting one-line argument, subtracting the two closed forms, gives . It fails at both ends of the price range. At the two bonuses coincide, and for the positive part clips to while is also whenever .
For that reason the paper's "if and only if", stated for all parameters, is false, and the goal corrects its "only if". At , , one has , yet both at and at .
All parameters are real fields of the structure Params, which also carries the ranges , , , , . The collectors' income is the gross payment, not their net utility. An optimal solution is a feasible pair that no feasible pair beats. is written , which is meaningful at .
Eq. (3) holds only for : for larger the processor's constraint binds, and the milestone on eq. (2)–(3) carries this correction. The goal nevertheless follows problem (4) as the paper poses it, in the total bonus with the closed forms (3). It does not repose the firm's problem on the pair .
The optima in the goal are arbitrary maximizers of the two problems, never defined by the closed forms. Defining , by those formulas would reduce the goal to algebra and is ruled out. Because existence is part of the goal, the universally quantified clauses cannot hold vacuously.
Only Mathlib is needed, with no new infrastructure. Lemmas on maximizing a concave quadratic in two variables over a polyhedron would be reusable beyond this mission, and contributions of auxiliary lemmas on the impacts and on the candidate optima are welcome.
In Bayesian persuasion a sender who observes a random state commits to a rule that maps states to recommendations, and a receiver who knows the state distribution follows a recommendation only when it is optimal given what it reveals (Kamenica and Gentzkow 2011; Bergemann and Morris 2019). When the distribution is known, the sender's best rule solves a linear program (Dughmi and Xu 2016). Online platforms that recommend products, routes or content to a stream of users are in the same position, except that the state distribution is not known to anyone: it has to be learned from the states the platform observes over time.
Zu, Iyer and Xu study this repeated problem. Recommendations based on an estimate of the distribution may fail to be persuasive under the true one, and a receiver has no reason to follow such a recommendation. The paper therefore asks for robust persuasiveness: the mechanism used at each round must be persuasive for every distribution in a confidence set that contains the truth with high probability. The question is how much sender utility this robustness costs over a horizon of rounds. This mission formalizes the paper's answer for its algorithm Rai: the regret is of order with high probability.
A persuasion instance consists of finite sets of states and actions , with , a receiver utility , a sender utility , and a set known to contain the unknown state distribution . At each time a state is drawn independently from . The sender sees it and recommends an action .
A signaling mechanism gives, for each state , a distribution over actions. It is persuasive under a prior , written , if
The sender's expected utility is , and the known-prior benchmark is . For a set of priors, , and the cost of robust persuasion is
A signaling algorithm chooses a mechanism after each history . It is -robustly persuasive if there are history-dependent sets with and . Its regret along a realized path is .
The Rai algorithm (Robustness Against Ignorance) keeps the empirical distribution of the past states and the -ball . At each round it plays any maximizer of over , with radii
The regularity conditions (Assumption 1) require that each region of beliefs under which is optimal contains an -ball of radius , and that for every .
For regular instances, every and every run of Rai, with probability at least ,
and, with a constant depending only on , on an event of the same probability.
In the order of the proof:
Theorem 2, together with the paper's lower bound (Theorem 3, not part of this mission), shows that robust persuasiveness costs a sender order regret and no more, up to a logarithm. In this sense learning to persuade is no harder than a standard stochastic online learning problem, provided the instance is regular. Without regularity the cost of robust persuasion can be a constant (Appendix A.1 of the paper), and the regret is then linear. Proposition 2 is a static statement of independent interest: under regularity, persuasion that is robust to an -misspecified prior loses only in sender utility.
As far as we know, none of these results is machine-checked. A complete development would add to the platform a finite model of repeated persuasion with history-dependent mechanisms and its path law, the cost of robust persuasion, an concentration bound for empirical distributions, and a worked use of the Azuma–Hoeffding inequality on an adaptively generated sequence. The printed proof of Proposition 2 contains a step that fails as written (see Difficulty), so a formal proof also confirms a corrected argument.
The obvious argument compares each round's linear program with the one at and bounds the difference by . It fails because the feasible set moves with the prior, and the value of the robust program at a ball has no a priori Lipschitz dependence on the radius. Everything rests on Proposition 2. Its proof constructs a mechanism persuasive on the whole ball by splitting into fully revealing posteriors and posteriors pushed toward the interior balls . The printed step (p.35) uses convexity of , but the balls are taken inside the simplex. A point it needs can then have negative coordinates, and on a three-state instance the inclusion is false. The statement and its constant survive with a different choice of , but a solver must supply that argument.
The probabilistic steps have their own care points. The recommendations depend on the whole history, so the martingale term must be handled under the algorithm's own path law, with the conditional range of given equal to . Lemma 1's proof cites a Talagrand-type inequality (Foucart and Rauhut, Corollary 8.46) that is not in Mathlib. McDiarmid's inequality with bounded differences suffices for the stated bound.
States and actions are finite types with at least two elements. is Mathlib's stdSimplex ℝ Ω, mechanisms are real functions with each row in the simplex, and is a finite sum. and are real suprema over sets of mechanisms only. These sets are nonempty and bounded, since the full-information mechanism is persuasive under every prior. Rounds are , a history is a function Fin t → Ω × A, and the path law is the explicit product . Probabilities are finite sums of it. is written . is natural, and is the real power.
Some conventions are fixed where the paper is silent or ambiguous:
The ball in Assumption 1 lies inside the simplex, as printed. Assuming instead that it is a full ball would weaken the goal, and is not done.
Contributions welcome: proofs of the milestones in any order. The concentration and martingale steps (Lemma 1 and the Azuma step) are reusable beyond this mission, as is the corrected proof of Proposition 2.
A Markov decision process (MDP) with the average-cost criterion asks for a policy that minimizes the long-run expected cost per stage. A classical way to solve it is linear programming: the optimal average cost is the value of a linear program over occupation measures (probability measures on state–action pairs that are invariant under the dynamics), and its dual is a relaxed form of the average-cost optimality equation. On Borel state spaces the LP formulation and its duality theory are developed in Hernández-Lerma and Lasserre ([20, Ch. 12] of the paper). Duality between the two programs is what justifies computing the optimal cost from either side and what connects the LP to the optimality equation.
Timeline.
The state space is a Borel space and the action space is countable with the discrete topology. Each state has a nonempty set of admissible actions, and the graph is Borel. Transitions follow a stochastic kernel ; the one-stage cost is Borel, finite on and off .
A policy chooses from a kernel with ; it may randomize and depend on the history. A stationary policy is a single kernel . For an initial distribution , the average cost is
A stationary pair is a stationary policy with an invariant probability measure of the chain it induces.
The primal program (P) minimizes over probability measures on with whose marginal on satisfies . The dual program (P*) maximizes over and bounded Borel with
Assumption 2.1 has three parts: (G) some pair has finite average cost; (SU) there are compact sets with ; (M) for each there are an open , a closed and a finite measure with on , while on the kernel is continuous and the cost lower semicontinuous in for each action.
Under Assumption 2.1, (P) is consistent and solvable, (P*) is consistent, and
The Lean statement asserts , that is the least primal objective value, and that the nonempty set of dual objective values has least upper bound .
The theorem establishes LP duality for average-cost MDPs whose costs need not be lower semicontinuous and whose kernels need not be weakly continuous, which covers models with discontinuous dynamics where the transition laws have densities bounded above. It makes the dual program (P*), over bounded functions, a valid route to , and it is the base case of the paper's constrained result (Theorem 4.2), where Lagrange multipliers enter. The abstract duality theorem (Theorem 2.2) applies to any infinite-dimensional LP in dual pairs.
The result is proved in the paper; no part of it is machine-checked. The mission adds a formal model of history-dependent policies on Borel spaces with an initial distribution, the average-cost criterion over all policies, occupation measures, both programs, and the dual-pair LP layer.
The obvious argument shows that every point of the closure of the cone of the primal program lies in it; this needs a compactness and lower semicontinuity argument for and continuity of , which fail when is not lower semicontinuous and is not weakly continuous. Weak limits of occupation measures need not be invariant, and the cost of the limit can jump above the limit of the costs. The proof replaces continuity by Lusin's theorem on sets of large majorizing measure, and controls the remainder through (M). A second difficulty is measure-theoretic: the limit measure must still live on , which is not assumed closed, and the disintegrated kernel must obey the control constraint at every state.
IsLeast/IsLUB/IsGLB, never with real sInf/sSup, which return on empty or unbounded sets.Regulators and large buyers must discover violations that firms prefer to hide: an emissions defeat device, a supplier's noncompliance, an environmental spill. They can audit, which is costly, or pay for voluntary disclosure through reduced penalties or remediation assistance, as in the U.S. EPA's audit policy. The question is how to combine the two when the firm can also invest in evasion, making audits less effective without fixing anything; the Volkswagen emissions case is the motivating example.
Wang, de Véricourt and Sun (Oper. Res. 72(5), 2024) model this as a dynamic principal–agent problem with adverse selection (the agent privately learns that an issue has occurred), moral hazard (hidden evasion) and costly state verification. Without evasion, the earlier model of Wang, Sun and de Véricourt (Oper. Res. 64(2):371–389, 2016) has deterministic periodic audits as the optimum. With evasion the optimum changes qualitatively, and this mission formalizes that change.
An issue occurs at a random time , exponential with rate , and only the agent observes it. Costs are discounted at rate . Remediation costs . The principal can audit at cost . An audit of an agent who has not evaded reveals the issue, and the agent pays a fine, at most . The agent can evade at cost , after which an audit detects the issue only with probability . The paper assumes and .
The principal commits to a policy adapted to the public history, the list of past audit epochs (with ). After each history the policy specifies, until the next audit:
After the issue occurs, the agent chooses when to act. At that moment it either discloses (cost ), evades (cost , where the threat utility is the expected discounted fine after evading) or self-corrects (cost ). If an audit comes first, the agent pays the fine .
Theorem 1 of the paper reduces the problem to policies under which the agent discloses at once. Such a policy must satisfy the obedience constraint (6) and the IC constraint: prompt disclosure costs the agent no more than any other strategy. Among these policies the principal minimizes
where counts audits. With perfect evasion, , the threat utility vanishes and obedience reads .
Let , , , . The equation
has a unique positive root . The cyclic policy is feasible and minimizes (11) over all feasible policies. In each cycle it charges with no audits for time units, then audits at rate with . Under it the gaps are i.i.d. exponential with rate .
with and .
The result says that evasion forces randomization. Without evasion, deterministic audits are optimal, because the disclosure payment may rise all the way to . With evasion the payment is capped at . Once it reaches , only an audit threat with constant hazard keeps the agent from delaying, and a constant hazard means exponential waiting times. The audit rate depends neither on nor on . Corollary 1 shows that the agent's expected payment exceeds the principal's auditing expense, so audits are self-financing. The paper later uses Theorem 2 to analyze imperfect evasion and the social-welfare extensions.
The theorem is proved in the paper, through a quasi-variational-inequality verification argument in its Online Appendix B. No machine-checked version exists. This mission produces a Lean model of continuous-time, history-dependent audit policies and a statement of optimality over all of them. Proving it requires the verification argument and a renewal analysis of the cyclic policy.
The cost of the cyclic policy is a renewal computation, and the indifference of the agent is a direct calculation. The hard part is the optimality lower bound. It must hold against every history-dependent mixture of impulsive and intensive audits, with every payment path, measurable but neither monotone, nor continuous, nor bounded below. It cannot be checked against stationary policies alone, or against the policies of the form of (13)–(14) alone. The IC constraint is global: prompt disclosure must beat every delay, including never acting. Its local form (9)–(10) holds only along paths. A proof must turn the global constraint into pathwise inequalities, or verify a value-function candidate against it, inside a measure-theoretic model of the audit process.
Correction. The printed theorem allows , where is undefined. The statements assume .
Ruled-out trivializations. None of the following is allowed:
The verification file checks the first two: the no-audit policy with is feasible, with it is not, and the first audit of the cyclic policy is computed from the policy.
The model definitions are reusable for the paper's Theorems 3–5 (imperfect evasion). Contributions are welcome on:
During the COVID-19 closures, restaurants, cafés and other small service businesses asked their regular customers to pay now for service later: gift cards, prepaid meals, "buy now, eat later" campaigns, discount coupons sold for a modest fee, and crowdfunding pages with all-or-nothing targets. Papanastasiou, Xiao and Yang (Management Science 71(4), 2025) ask when such advance selling actually helps a firm in financial distress, compared with a bank loan. The difficulty is that two incentive problems interact. A firm that has already been paid has less reason to work hard afterwards (moral hazard). Consumers who can wait and pay later will free-ride on the others (strategic consumers).
The bank side is the fixed-investment model of credit rationing with moral hazard in Tirole, The Theory of Corporate Finance (Princeton University Press), Chapter 3, as the paper states on p. 5. The paper's last finding concerns a hybrid scheme: discount coupons sold under an all-or-nothing clause, used together with a reduced bank loan. Group-buying platforms used the same design under the name "threshold discounting". This mission formalizes the paper's exact characterization of the hybrid scheme, Proposition 10.
A firm needs funding to survive a financing period. In the repayment period it operates with probability . If it operates, it chooses an effort at cost , which succeeds with probability . An inner segment of loyal customers (mass ) values the service at , and an outer market (mass ) values it at . After success every consumer values the service. After no success only a fraction does. Write for the largest achievable revenue, and
Two standing assumptions hold throughout: (Assumption 1) and (Assumption 2).
Bank financing. For revenues (success) and (no success) and a debt with face value , the firm's effort maximizes on . The firm has limited liability. A competitive bank lends at the least face value for which its expected repayment equals . Proposition 1 solves this game for a pure bank loan . In the first-best region the face value is . For (moderate distress) the loan is risky and effort drops to . For the firm is credit-rationed.
Scheme H. The firm sells each inner consumer a coupon at price now, and service at the spot price later. The campaign is cancelled and refunded unless all inner consumers buy. If they all buy, the firm borrows only , with revenues and . Consumers buy iff the conditions of the paper's Lemma A.1 hold. Because of the all-or-nothing clause, any deviation sends the game back to pure bank financing, where a waiting consumer earns . A feasible plan is a pair with whose financing is secured and which consumers buy. The firm picks the most profitable feasible plan or pure bank financing.
Let , and . Put , and . Then:
is feasible with effort and profit . No feasible plan earns more, every optimal plan has effort , and the bank-only profit satisfies , strictly iff ;
Three readings are part of the goal. First, the optimal prices are not unique: a risky-loan plan at other prices earns the same profit. The goal therefore states an optimal plan, with effort and profit unique. Second, is a tie, where hybrid selling and bank financing earn the same. Third, the purchasing equilibrium uses Lemma A.1's weak inequalities, which the optimum binds.
The paper proves Proposition 10 by substituting into Proposition A.7. Milestones M3–M6 are the steps of the proof of Proposition A.7 at , as that proof of Proposition 10 uses them.
Proposition 10 is the main-text form of the paper's headline claim. Under moderate distress, classic advance selling and coupons alone do not help, and an all-or-nothing clause alone helps only in a limited range of scenarios (Propositions 7 and 8). Their combination succeeds. It succeeds exactly when the financing need exceeds and the loyal customers' valuation exceeds an explicit threshold, and its profit is then given in closed form. The comparison between and is what makes the coupon design work: the discount keeps the firm's stake in success while the clause stops free-riding.
The result is proved in the paper but has no machine-checked proof. The formal development adds a complete check of a multi-regime constrained optimization in which the paper's own displays need care. Its "maximum" (146) is attained only on the boundary of the low-price region. The general- claim in the proof of Proposition A.7 fails for . Proposition 1 prints a tie-break at . Each of these is resolved in the statements and recorded in the items' difference lists.
The obvious approach is to plug Lemma A.5's closed forms into the profit and maximize over . The constraint set is not given in closed form, though. It comes from the consumers' best response to the firm's effort, which comes in turn from the bank's least root, and it splits into a safe-loan region (profit linear in ) and a risky-loan region (profit , with the larger root of a quadratic). The consumer constraint binds at the optimum. In the risky-loan region the profit's supremum is approached only along a curve, and the region below must be shown to be dominated by bank financing. Nothing in the statement needs derivatives, but every step needs exact monotonicity of explicit square-root expressions. Each radicand must be shown nonnegative from , not by Lean's convention for .
All objects are real numbers; lam denotes . Effort is a best response on Set.Icc 0 1, and the bank's face value is the least break-even one (IsLeast). The consumers' decision is Lemma A.1's condition with the all-or-nothing deviation utilities, and the firm's choice is optimality over the feasible plans (HPlan). None of these is defined by a closed form. The closed forms (, , , , , , , ) appear only as statement values. Plans range over and . The inner segment is a continuum, which is the limit of the paper's footnote 3. The financing subgame takes the revenues at the revenue-maximizing regular price, and clause (0) of the goal and Proposition 1's price clause prove that this price is revenue-maximizing.
A statement that defined effort or the interest rate by Lemma A.5's formulas would turn M2 and most of the goal into identities. Defining the consumers' choice by a closed-form outside option would skip M3. Both are ruled out by the relational definitions.
The development needs only Mathlib's reals, Real.sqrt, max/min, IsLeast, IsGreatest, IsLUB and Set.Icc. The financing subgame (best-response effort, least break-even face value) is a reusable model of credit rationing under moral hazard. Proofs of the milestones, alternative decompositions through sketches, and proofs of the general- steps where they hold are all welcome.
A risk manager who has fitted a loss distribution does not trust it completely. Robust risk assessment asks how bad the expected loss could be under every alternative model close to the fitted one, with closeness measured by an -divergence, the classical notion of Csiszár (1963), Morimoto (1963) and Ali and Silvey (1966). Breuer and Csiszár (2016) give a general worst-case theory for such divergences. Kruse, Schneider and Schweizer (2019) show that there is a wide class of models for which neither Kullback–Leibler nor polynomial divergence has certain desirable properties for robustness analysis, and for heavy-tailed reference models those two divergences have considerable limitations.
The paper of Kruse, Schneider and Schweizer responds by building the divergence around the reference model. This mission formalizes its Weibull case: the three components of the toolkit, and the lemma that applies all three.
Let be a distribution on with density , support , and . An alternative model has density . For a convex with ,
with , and if is not absolutely continuous with respect to .
The paper specifies through a generating function: continuous, strictly increasing, with as and . Then for , and . The choice is Kullback–Leibler. The worst case at radius is
The Weibull case assumes and for some . For the tailored generating function is
For , , this , and every reference density with and :
for all and ; condition (7) holds; and the conclusions of Propositions 1, 2 and 3 hold, written out in the statement.
The Weibull function: Lemma 3 and the inverse (11). The worst case: Lemma 2, Lemma 1, the conjugate formula, finiteness of , the Fenchel identity and Proposition 1, which gives, under
the worst-case density . The contents of balls: display (30), Proposition 2 (a finite -th moment gives finite divergence), the lower bound on , and Proposition 3 (a power tail with an infinite moment of order gives infinite divergence).
Lemma 4 shows that one divergence simultaneously gives finite worst cases, an explicit worst-case density and a sharp moment cut-off for reference models with Weibull-type tails, including the heavy-tailed range . The modeller chooses and thereby decides which moment an alternative model must have to enter the ball. The hypothesis needs only tail asymptotics, so no closed form of is required.
Formalizing it adds a checked account of a result that rests on a citation. All results here are proved in the paper, except that its proof of Proposition 1 quotes Breuer and Csiszár (2016), Theorem 4.2 and Corollary 4.6, and Csiszár and Matúš (2012), Corollary 3.8, for attainment and for . A complete formalization therefore needs either those results or a direct variational argument. No machine-checked proof of these results is known.
The obvious route to Proposition 1 is pointwise Lagrangian maximization: maximize in and read off the density. That gives only the form of a candidate. The real content is existence of multipliers solving two coupled nonlinear equations in , for every below , and showing that when is unbounded above. Here must be shown essentially smooth, and controlled, on an unbounded domain where grows quickly. For the moment cut-off, the delicate point is that the bounds on must be sharp up to a constant in both directions and interact with the tail of only through . For the Weibull case, the analysis must work for fractional exponents and for .
Models are represented by densities: IsRefModel f, IsDensity g, with the closed support refSupport f, which is Mathlib's Measure.support. Divergences take values in ℝ≥0∞, the integrand tests first, and non-absolutely-continuous models get ⊤. The worst case is never a real sSup, which would be for an unbounded set: finiteness is integrability of every ball member together with BddAbove of the set of means, and attainment is IsGreatest. The ball is not restricted to integrable models, so a statement cannot gain anything by dropping heavy-tailed alternatives. Since Real.log 0 = 0 and , conditions on and on quotients are written with the case explicit. L enters through Set.range H, and is cocompact ℝ.
A complete development needs: calculus for through interval integrals, convex conjugates of one-variable functions, the Fenchel–Young equality case, the two-multiplier existence argument, and rpow asymptotics. The divergence layer and the conjugate formula are reusable for other -divergence missions. Contributions are welcome on any milestone, on direct proofs replacing the quoted results, and on the lognormal analogue.
A retailer choosing which products to offer (an assortment) must predict how customers substitute between products. Discrete choice models make this prediction, and the paired combinatorial logit (PCL) model is a generalization of the multinomial and nested logit models in which every pair of products forms a nest, so that the correlation between the utilities of any two products can be set separately. Assortment optimization under the PCL model is NP-hard even without constraints, and practical instances carry constraints on the number of products displayed.
R. Ghuge, J. Kwon, V. Nagarajan and A. Sharma (Oper. Res. 70(2):786–804, 2022) reduce PCL assortment optimization to the maximum directed cut problem and obtain constant-factor approximation algorithms under cardinality, knapsack and matroid constraints.
Timeline.
There are products . Product has revenue and preference weight , and is the weight of not buying. Each ordered pair , , is a nest with dissimilarity parameter . An assortment is (in Lean, a Finset (Fin n)). With and , the expected revenue is
and is the optimal revenue under the cardinality constraint .
The ratio is linearized by : if and only if . The reduction graph has a vertex for each product and a dummy vertex , edges and , and explicit weights , affine in , such that is the weight of the edges leaving (pclWeight, pclEdges). keeps the edges of nonnegative weight.
For a digraph with weights , sizes and capacity , the LP (9) is
and LP is this LP on with ; its value is an upper bound on . Algorithm 1 takes an optimal basic solution of (9), possibly shifts it along the coordinates equal to and , applies pipage rounding (repeatedly moving mass between two fractional coordinates in the direction that does not decrease ), and outputs the better of the rounded set and that set plus the last fractional vertex.
For every finite loopless digraph with , every and unit sizes, and every optimal basic solution of LP (9) with value , Algorithm 1 has an output, and every output satisfies
For every PCL instance and , has a fixed point ; Algorithm 1 run on has an output; and for every output the assortment satisfies
The theorem doubles the best previous factor (0.25) for cardinality-constrained PCL assortment optimization and carries the factor 0.5 of Ageev et al. (2001) for cardinality-constrained max-dicut over to assortment optimization (Table 1 of the paper). The reduction of Lemma 1 is reusable: any LP-based approximation for constrained max-dicut with nonnegative weights becomes an approximation for PCL assortment optimization through the framework of Theorem 2. Theorem 5 extends the half-integrality of Ageev et al. from cardinality to general knapsack constraints, and is also the basis of the paper's knapsack results (Theorem 7 and the -approximation of §5).
The proofs of most of these statements are in the online appendices of the paper. None of the results has a machine-checked proof; this mission produces the first, together with Lean statements of the PCL model, the max-dicut LP and pipage rounding.
The ratio objective is neither submodular nor linear, and the reduction graph has negative edge weights, so max-dicut algorithms do not apply directly; Lemmas 2, 6 and 7 are what allow deleting the negative edges. The main obstacle is Theorem 5: the knapsack constraint destroys the half-integrality of the max-dicut polytope, and the proof must show that a single extra value (and ) suffices for every extreme point. Pipage rounding alone does not give the 0.5 bound at such points; the shift of equation (10) and the case analysis of Lemma 11 are needed, and the bound is tight there.
Products are Fin n; the vertices of are Option (Fin n) with none the dummy. Real powers are Real.rpow, and is part of PCLInstance, so that empty nests contribute (Lean's ). Optimal values over finite families are suprema over finite nonempty sets; is an sSup over a nonempty polytope. "Basic feasible solution" is Set.extremePoints of the feasible set of (9) in the joint space, with fixed to off . Algorithm 1 and pipage rounding are relations: every nondeterministic choice is quantified, the goal asserts that an output exists and that every output satisfies the bound, and running time is not formalized. For the PCL part, Algorithm 1 runs on with all vertices of size , and the output is intersected with .
The statement "some assortment with at most products earns at least " is trivially true (take the optimum) and is not the theorem; the goal is about the outputs of Algorithm 1. Lemma 2 is corrected: its first clause holds with "nonpositive", not "negative".
A complete development needs LP duality and the existence of optimal extreme points for bounded polyhedra, the extreme-point analysis of Theorem 5, and the termination of pipage rounding. The max-dicut LP and pipage rounding definitions do not depend on the PCL model and can be reused for other rounding results. Proofs of any milestone, and alternative routes to the goal, are welcome.
When several agents repeatedly choose actions and pay costs that depend on everyone's choices, each agent faces an online learning problem whose environment is the other agents. Online gradient descent (OGD) is the standard learner in this setting. It is doubly optimal under strong convexity: a single agent facing arbitrary strongly convex costs has regret, and when every agent of a strongly monotone game runs it, the joint action converges in the last iterate to the Nash equilibrium at rate (Zhou et al. 2021, as summarized in Jordan, Lin and Zhou, Theorem 3.5). Both guarantees need the strong monotonicity modulus to set the step size , and in a game no agent knows .
Jordan, Lin and Zhou remove this requirement with a randomized step size. Each agent draws independent geometric variables , , and uses . Their Theorem 2.5 treats one agent and their Theorem 3.7, the target of this mission, treats the game.
A continuous game has agents , nonempty convex compact action sets , the joint set with the Euclidean norm , and costs that are continuous and differentiable in the agent's own action. The gradient profile is , continuous on . The game is -strongly monotone if on . A Nash equilibrium is a profile from which no agent can lower its cost by a unilateral deviation. The diameter of is at most .
At round every agent observes a noisy gradient with and , the conditioning being on the current joint action and all step sizes. MA-AdaOGD (Algorithm 3) then sets, for each agent independently,
with i.i.d. Geometric() on .
The game has a unique Nash equilibrium , and
for every , . The constant is the paper's, stated in full; the rate is its consequence.
The theorem gives a learning rule for games that is feasible: each agent uses only its own gradient feedback, the horizon and its own random draws, with no knowledge of , , , or the other agents. Its last iterate converges to the Nash equilibrium at rate , within logarithmic factors of the lower bound for strongly convex optimization. With Theorem 2.5 it makes the same rule doubly optimal. The proof never uses that is a gradient profile, so the bound also covers stochastic strongly monotone variational inequalities (Corollary 3.11).
Nothing in this mission is formalized elsewhere: the platform has no continuous-game, strong-monotonicity-on-a-set or Nash-equilibrium layer of this kind, and no result on maxima of geometric variables. The game layer (Definitions 3.1–3.3, Proposition 3.4, existence and uniqueness of equilibria) is reusable by any mission on monotone games or variational inequalities.
The deterministic parts are short: the descent inequality follows from the optimality condition of the projection step, strong monotonicity and the variational inequality at . The difficulty is the expectation of the random step sizes. The paper bounds the third term III of (3.4) in display (3.7) by . That step is not valid as printed: it replaces a conditional expectation given the argmax agent by an unconditional one, uses a ratio bound that fails when one agent holds the overall maximum, and relies on (A.1), whose printed bound is false. A Monte Carlo estimate of III exceeds the printed (3.7) for . The paper's proof of Theorem 3.7 is therefore incomplete. No counterexample to Theorem 3.7 itself is known, and the goal is posed as printed. A proof needs a different bound on III, or a different route from Lemma 3.10 to the goal; (3.7) is deliberately not a milestone.
Existence of the Nash equilibrium needs a fixed-point or variational-inequality existence argument on a compact convex set, which Mathlib does not provide.
Agents are Fin N, agent 's space is EuclideanSpace ℝ (Fin (d i)), and the joint space is PiLp 2, so every norm and inner product is the Euclidean one of the product. Costs and gradients are total functions constrained on only, and is a gradient within (HasGradientWithinAt). The goal and the existence of equilibria take compact action sets, as on the paper's p.1; Definition 3.1 says "bounded", under which neither the argmin nor the equilibrium need exist. Lemma 3.10 and (3.4) assume a run and an equilibrium, so they need no compactness. The conditional moments of are taken given and all step sizes , the conditioning written in the paper's Appendix D (p.40); the paper's p.13 writes alone. Geometric variables live on , and . Expectations are Bochner integrals, and every bounded expectation comes with an integrability clause, so no bound holds because an integrand fails to be integrable.
Proposition A.1 (A.1) is posed with the bound that the printed proof derives, in place of the false . Contributions are welcome at every level: the game layer, the probabilistic lemmas on geometric maxima, the descent lemma, and above all a valid bound on III.