Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Many sellers accept returns of standard goods but restrict returns of customized goods. A customized item is more likely to fit its buyer, yet it may be harder for the seller to recover value when it comes back. Choosing a return policy therefore changes both what customers buy and how many units they return. Esenduran, Letizia, and Ovchinnikov study this tradeoff in a two-product market and show that permitting customized-product returns can, for some parameters, raise the firm's profit while reducing its total return volume (accepted manuscript, Proposition 2, p. 11). The result is an existence statement about a firm's optimal policy, not a claim that permissive returns always have this effect.
A unit mass of consumers has taste uniformly distributed over . The standard product is located at and has baseline willingness to pay . The customized product changes both a direct-value attribute and a taste-related attribute; its baseline willingness to pay is . Here may have either sign, while measures the taste improvement. These are the paper's normalized expressions, with the reservation value set to one (§2.2, pp. 5–6).
Product matches a consumer's needs with probability ; after a mismatch, the consumer values it at only , where . The firm chooses a nonnegative price and a nonnegative return fee for each product. A buyer learns whether the product matches after buying and keeps it exactly when keeping gives at least the payoff from returning it. Before purchase, the consumer compares the two expected utilities, including this return option, and buys only if the best one is positive. A tie between products goes to the standard product. These rules determine the buyer volumes , the mismatch-return segments , and the keep segments . The expected number of returns is (§2.3, p. 7; problem (3), p. 10).
With production cost and recovered value on a returned unit, the firm's expected profit and total return volume are
An optimal policy maximizes this profit over all nonnegative prices and fees. In the paper's disallow counterfactual, the standard product's price and fee remain at the original optimal policy's values, while the customized price and fee are chosen to maximize profit subject to . The proof writes this as problem (5) in the Solution 2 region (Online Appendix pp. 14–15).
The goal is Proposition 2. There exist admissible parameters and an original optimum such that customized returns occur, and for every original optimum and every associated disallow-counterfactual optimum,
Both optimization problems must attain their maxima. The quantified claim is what “can increase profits and reduce total returns” means in this model; it does not replace an optimum by a preselected formula.
Three milestones trace the part of the paper used for this existence result. Solution 2 characterizes an original optimum with positive customized-return and standard-return segments, a positive standard-keep segment, and no customized-keep segment. Solution 2b characterizes the corresponding optimum when customized returns are disallowed and the standard terms stay fixed. Their returns identity expresses the difference in total return volumes as a factor containing ; away from the boundary , that difference is negative exactly when (Online Appendix pp. 4–5, 15).
The paper's claim separates the total number of returns from the permissiveness of one product's return policy. A permissive customized policy may induce some consumers to switch away from standard goods. Since customized goods match preferences more often, those switches can outweigh returns from newly served buyers; profit can rise at the same time. Thus a firm cannot infer total return volume by looking only at the customized product's own returns (§3.2, p. 11).
The paper proves the result analytically. This mission records its model, optimization comparison, and three central statements in Lean; the theorem proofs are open formalization work. A completed development would certify the global optimum comparison, including existence and all admissible nonnegative policies, as well as the algebraic segment identity. The definitions of consumer choice, return volumes, and the constrained counterfactual can also support formalizations of the paper's other solution regions and robustness results.
The return option makes each consumer's expected utility piecewise linear in taste. Which product a consumer buys depends on the upper envelope of two such functions and zero, so the volumes change formula when thresholds cross. The firm's objective is consequently piecewise rather than one differentiable expression on the full policy space. A stationary formula for one segment ordering is insufficient to establish a global optimum; the proof must account for policies on other orderings and their boundaries. The paper's displayed Solution 2 region also includes parameter points where a fee becomes negative or a segment leaves , so those expressions alone do not characterize the intended interior policy (Online Appendix A.2, pp. 3–5).
Lean represents every parameter, price, fee, threshold, profit, and segment size as a real number. Consumer volumes are Lebesgue measures of subsets of ; a consumer purchases only when expected utility is strictly positive. The latter convention follows the proof of Proposition B1 and Table 2, which exclude a buyer with nonpositive expected utility. The paper's p. 7 prose uses a weak inequality; at a zero fee that choice could create a positive-volume tie incompatible with its return accounting. The standard product wins ties between products. The standard product has in the definitions (Table 1, p. 7; Online Appendix p. 11).
The standing assumptions include Table 1's parameter ranges, the ordering condition , , and . The lower bounds and are made explicit. Milestone formulas that divide by or assume and . The Solution 2 and 2b milestones additionally require an interior feasible region: positive return segments, a positive standard-keep segment, nonnegative standard fee, and less than full market coverage. These added conditions select the solution described in the appendix. The displayed customized price of Solution 2 is not used: at the rational consistency witness it conflicts with the displayed segment sizes. The statements retain those segment sizes and the standard terms, which are the quantities needed for Proposition 2.
The goal quantifies over the firm's actual feasible policies and asserts that both optima exist. Defining “optimal” through a closed-form candidate, omitting the disallow maximum, or using a zero-volume population would erase the comparison. Contributions may address global optimality, the consumer threshold and measure calculations, the counterfactual optimum, or the returns identity. The measure and piecewise optimization results would be reusable for other product-line models.
A seller choosing a simple way to sell several items faces a problem when one buyer values both individual items and combinations. Pricing each item or offering the entire set as one bundle is easy to describe; an optimal lottery menu can use many more options. The question is how much revenue this simplicity can cost. Eden, Feldman, Friedler, Talgam-Cohen and Weinberg give a guarantee controlled by how many potentially valuable combinations contain any one item. Their result applies to valuations with complements and feasibility constraints that also create substitutes. The preprint used here is arXiv:1612.04746v2; its theorem and page numbers are the source for this mission.
The paper's lower-bound examples show that dependence on the complementarity degree is needed, up to constants, for the mechanisms under study (§6, pp. 13–15). The mission targets the upper bound, including its stated constant. It does not claim that the stronger lower-bound examples have already been formalized.
Let be a finite set of items. A hyperedge represents a combination with a nonnegative bonus . A fixed feasible family is downward closed and contains the empty set. A buyer receiving bundle can obtain the bonuses of a feasible subset , so the induced valuation is
Each weight is sampled independently from a distribution with finite support; together they induce a population of valuations. As in §2, pp. 4–5, weights outside are zero, and normalizes the empty bundle's value. The population has complementarity degree at most when every item belongs to at most hyperedges for which a positive weight is possible.
A mechanism gives each reported valuation in the finite type space a lottery over bundles and a payment. The buyer evaluates a lottery by expected value. The mission uses incentive compatibility and individual rationality for truthful mechanisms: a buyer prefers their own report, and participating gives nonnegative utility. Let be such a mechanism's expected payment.
BREV is the best expected revenue from a single price for the grand bundle, namely . SREV* is a conservative separate-price benchmark. At item prices , item contributes its price only when some bundle containing has strictly positive surplus and every bundle omitting has nonpositive surplus. The supremum is over all real price vectors; it is the paper's , rather than a favorable tie-breaking convention for an ordinary item-pricing menu (§2, p. 5).
The goal is Theorem 3.2, p. 6. For every population of degree at most and every truthful mechanism ,
The milestones follow the paper's two benchmark terms. Corollary 3.1, p. 6 bounds revenue by NON-FAVORITE plus SINGLE. Theorem 4.6, pp. 9–10 specifies a partition of hyperedges returned by Partition-Edges, and Proposition 4.1, p. 7 bounds SINGLE by . For NON-FAVORITE, Lemma 5.1, p. 10 introduces the CORE and TAIL terms at a cutoff ; Propositions 5.5 and 5.7, pp. 12–13 bound those terms; and Proposition 5.10, p. 13 gives . These seven statements are the mission's intermediate targets.
The theorem gives a concrete revenue guarantee for two simple selling formats even though the valuation can contain overlapping complementary bonuses and feasibility constraints. It says that, within the stated finite-support model, the better simple benchmark captures at least a fraction of the revenue of any truthful, individually rational lottery mechanism. The paper also establishes lower bounds showing that a factor growing with is inherent for its simple-mechanism comparison (§6).
The mathematical result is proved in the paper. The Lean goal and milestones here are statements awaiting proofs; compilation checks their types and definitions, not their truth. Completing them would create a reusable finite product model for mechanism-design arguments, an explicit version of the strict separate-sale benchmark, and a machine-checked combinatorial partition theorem. Those pieces can support later work on revenue bounds with constrained bundles.
The first apparent shortcut is to compare revenue directly with the best bundle price. It cannot account for instances where value is spread among item prices, while item pricing alone cannot account for large complementary bonuses. The paper therefore has to control two different contributions to its revenue benchmark. In the favorite-hyperedge contribution, overlapping edges make independently chosen bundle prices interact. In the nonfavorite contribution, large weights require a different estimate from bounded weights. The duality benchmark also uses ironed virtual values for discrete distributions; replacing them by un-ironed slopes can change SINGLE. These are specific obstacles to closing the Lean goal, beyond the routine finite-sum bookkeeping (§§3–5).
The Lean model uses Finset bundles, a downward-closed finite family , and positive masses on finite supports for each hyperedge law. A finite product support gives the expectation and probability operators. The valuation is computed from a realized hypergraph; mechanisms operate on the resulting finite valuation type space. The goal quantifies over each valid mechanism. It does not use a real supremum over mechanism revenues, whose default value on an unbounded set would make the statement misleading. BREV and SREV* do use real suprema over all real prices, matching the paper's price domains.
Favorite regions compare nonempty hyperedges, with an injective rank resolving ties. The paper specifies a lexicographic tie rule; quantifying over ranks includes that choice. SINGLE uses the slope of the least concave majorant of the finite revenue curve, the discrete ironed virtual value implicit in the paper. Figure 1 is represented by its actual sweep and loop, and Theorem 4.6 excludes the empty hyperedge because that input prevents the stated procedure from terminating. Proposition 5.5 specifies , the domain on which its printed inequality holds. These conventions and the explicit individual-rationality requirement prevent zero-valued or arbitrary-payment cases from trivializing the target.
Contributions toward the published milestones are welcome, including the duality and ironing argument behind Corollary 3.1, the combinatorial theorem for Figure 1, and the finite-support estimates for CORE and TAIL. The listed milestones do not include every supporting lemma from the paper; the remaining posted-price, concentration, and independent-event results may be developed as reusable lemmas where needed. No milestone is weakened to make its proof fit the current library.
Optimal stopping asks when to halt a stochastic process so as to maximize an expected reward. Examples are exercising an American option, selling an asset, or ending a clinical trial. The optimal policy is the solution of a dynamic program over the whole state space. In high dimension it cannot be computed exactly, and the usual approximations (regression on basis functions, as in Longstaff–Schwartz) produce policies that are hard to read: a decision maker cannot see why the policy stops in a given state.
Ciocan and Mišić (Interpretable Optimal Stopping, Management Science 2022; arXiv:1812.07211) propose to restrict the search to tree policies. These are binary decision trees whose split nodes compare one state variable with a threshold and whose leaves say stop or go. The tree is fitted by maximizing the average reward over a finite set of simulated trajectories, which is a sample average approximation (SAA) of the true problem. This mission formalizes the consistency guarantee that justifies the method: as the number of trajectories grows, the optimal SAA value over trees of bounded depth converges almost surely to the optimal true value over the same trees.
The state of the system is a vector . The process runs for periods and starts at a fixed state . Stopping in period in state pays , and rewards are discounted by a factor per period.
A stationary policy is a map . Its stopping time on a path is , and if the policy never stops. Its value is
where a path on which never stops earns . Given trajectories for , the sample-average value is the average of the same discounted reward over the trajectories.
A tree policy is given by four things:
A state descends to the left child of when and to the right child otherwise, and receives the action of the leaf it reaches. is the class of tree policies of depth at most . Once is fixed, the skeletons form a finite set, but the split points range over a continuum.
The paper's standing assumptions are:
Fix a depth and . With probability one there is a finite such that for all ,
This is the paper's headline consistency result: the optimal SAA value converges almost surely to the optimal tree-policy value.
Corollary 1 is what makes the SAA tree-fitting procedure a consistent estimator of the best interpretable policy. A decision maker who optimizes a depth- tree on enough simulated trajectories obtains an in-sample value that approximates, to any precision, the true value achievable by depth- trees. The paper also shows (Section EC.1.2) that the conclusion fails when the depth is unbounded, so the depth restriction is part of the result and not a convenience. Theorem 1, the uniform law behind it, has its own uses: it also controls the out-of-sample value of the SAA-optimal tree.
The results are proved in the paper's electronic companion. To our knowledge they have no machine-checked proof. Formalizing them yields a reusable model of finite-horizon stopping with stationary policies and decision-tree policies, and a uniform strong law for a class of indicator-type functionals that is discontinuous in its parameters. The latter is a pattern that recurs in empirical-risk results for trees and threshold rules.
The strong law gives convergence for one policy at a time, outside a null set that depends on the policy. Uncountably many split points mean uncountably many null sets, so the pointwise law does not yield Theorem 1. The usual fix, a Lipschitz or continuity argument in the parameter, fails because is a step function of : moving one threshold past a sampled state changes a decision and the sample value jumps. The jumps of the true value must instead be controlled by the probability that the process visits the thin slab between two thresholds, which is where Assumption 3 enters. The jumps of the sample value must be controlled by the empirical frequency of such visits, uniformly in the thresholds. The first period is excluded throughout, because is deterministic and Assumption 3 does not apply to it.
Fin n → ℝ, whose Mathlib norm is the sup norm . Paths are Fin T → (Fin n → ℝ), and periods are 0-indexed (k : Fin T is period , so is β ^ k).μ, a probability measure, with and almost surely.g k are measurable. Both are readings of "discounted" and of the expectation on the page.μ, measurable and mutually independent (iIndepFun). The page says only "trajectories of the process" and its proofs use the strong law. averages the first m samples, and "with probability one" is ∀ᵐ.Fin n and leaf actions. Split points are a function of the node address. A split sends ties left (). A leaf has depth . is the type of (skeleton of depth , split points), and the suprema in Corollary 1 are real suprema over it. They are genuine suprema because the type is nonempty and the values are bounded in (for , almost surely).The statements cannot be met by a degenerate policy class or a junk value. is the expectation under the true law, the average over i.i.d. trajectories, and the suprema range over every tree of depth at most with arbitrary real split points. The hypotheses are jointly satisfiable with a nonconstant reward and a split that changes the action. One example is , , , uniform, and .
A complete development needs:
strong_law_ae.Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 through Glivenko–Cantelli or VC-type arguments.
When a bank or firm in a network of mutual obligations cannot meet its liabilities, some rule must decide how much each debtor pays each creditor. The rule used almost universally in the systemic-risk literature is the proportional rule of Eisenberg and Noe (2001): every agent pays its liabilities in full if it can, and otherwise distributes its whole asset value over its creditors in proportion to their claims. Central banks and regulators use it to measure contagion in interbank markets; Elsinger, Lehar and Summer (2006) apply it to the 881 banks reporting to the Austrian Central Bank, and Upper (2011) surveys fifteen such studies.
The rule is usually taken as given. Csóka and Herings (2021) ask which properties of a bankruptcy rule single it out, without assuming in advance that payments depend only on an agent's asset value and liabilities. Their answer is an axiomatization: five basic axioms together with one axiom on splitting an agent into identical copies.
For claims problems (one estate, several claimants) the proportional rule has classical characterizations through nonmanipulability by merging and splitting claims (O'Neill 1982, de Frutos 1999, Moreno-Ternero 2006, Ju, Miyagawa and Sakai 2007). Csóka and Herings show that the network analogue of nonmanipulability is too strong (no rule satisfies it together with the basic axioms) and replace it by invariance to mitosis.
Agents are natural numbers. A financial network consists of a nonempty finite set of agents, endowments for , and a nonnegative liability matrix on with ; is what owes . The class of all financial networks is . The relative liability matrix is if and otherwise.
A payment matrix is an element of , the nonnegative matrices with zero diagonal; is the amount pays . Agent 's asset value is and its equity is . For rows, means for all with strict inequality for some .
A bankruptcy rule assigns to each a payment matrix (Definition 2.1). The proportional rule assigns the solution of
The axioms, in the order of the paper:
Part (a) makes a well-defined bankruptcy rule; part (b) says that satisfies the axioms and that every rule satisfying them is .
The theorem justifies the proportional rule by properties rather than by convention. Because the axioms make no assumption on the form of the rule, consequences such as the absence of pairwise netting are derived, not assumed. Together with the paper's Theorem 5.3 (no rule satisfies the basic axioms and full nonmanipulability), it shows that invariance to mitosis is the strongest splitting requirement compatible with the basic axioms.
The result is proved on paper; no part of it, and no part of the Eisenberg–Noe clearing theory, has a machine-checked proof on this platform. A formalization contributes a reusable layer for clearing payments in financial networks: the system (2.1), its existence and uniqueness under strictly positive endowments, nonnegativity and zero-equity properties of clearing vectors, and their continuity in the data. These are the objects every stress-testing model on top of Eisenberg–Noe starts from.
Existence and uniqueness of a solution of (2.1) is a fixed-point statement about a nonlinear, non-contracting map; uniqueness holds only because every endowment is strictly positive, and fails without it (two agents owing each other one unit with no endowments admit both and ).
In the characterization direction, impartiality only equalizes payments to equal claims, and invariance to mitosis only relates networks that differ by splitting one agent into identical copies. Neither axiom speaks directly about payments to unequal claims, and splitting reaches only ratios of positive integers. Passing from rational to real liabilities needs continuity of the rule and continuity of , and the latter rests on uniqueness of the clearing vector, so the two halves of the theorem are not independent.
Finset ℕ; a fixed finite type cannot express mitosis, which creates fresh agents. Endowments, liabilities and payment matrices are functions on (resp. ) that vanish outside the population, as part of the network structure and of . All quantities are real.OrderHom.lfp, the uniqueness argument under positive endowments, and lemmas on the split network (sums over the copies, the relative liabilities of copies) that serve both Part (I) and Lemma A.1.Emergency departments (EDs) are crowded in part by patients whose condition could have been treated by a primary care provider (PCP), while other patients first visit a PCP, are found to be critical, and are sent on to the ED, paying for two visits. Teletriage — a nurse telephone line that assesses symptoms and recommends where to seek care — is widely offered by health systems and insurers as a remedy for both. It is not error-free: a nurse can undertriage a critical patient (advise primary care) or overtriage a sick one (advise the ED). Whether such an imperfect advisor reduces ED usage, or merely sends more worried-but-well patients to the ED, is the question this mission formalizes.
Çakıcı and Mills (M&SOM, 2020; accepted manuscript at SSRN 2849635) model a patient who does not know whether she is merely sick or critical, chooses between the PCP, the ED and a teletriage call, and updates her belief after the call. Their Proposition 3 answers the question in closed form when every patient calls: teletriage reduces ED usage exactly when the overtriage rate is below an explicit threshold, and reduces double-dipping exactly when the undertriage rate is below another.
A patient is in one of two states, sick () or critical (), and holds a belief , the probability that she is critical. Three actions are available.
Without teletriage the patient's cost is , minimized by the ED exactly when . With teletriage it is
Teletriage is informative when . Proposition 2 of the paper identifies an interval where calling is strictly optimal, bounded by two thresholds
Write and for the probabilities that a patient with belief who acts optimally ends up at the ED, resp. double-dips, without teletriage, and , with it. When beliefs are uniform on , the population rates are the averages , and likewise for the others.
Assume informative teletriage, beliefs uniform on , and : with teletriage everyone calls, and without it some patients go to the PCP and some to the ED. Then
The result separates the two failure modes of a triage line. Overtriage alone governs whether ED visits fall, and undertriage alone governs whether double-dipping falls, with thresholds that depend only on the copays (through ) and the belief range. A health system can therefore read off, for a given patient population, the overtriage rate a teletriage service must achieve before it relieves the ED. In the paper's example (, beliefs uniform on ), : with an overtriage rate of 2.5% or more, teletriage does not reduce ED usage even though every patient calls.
The result is proved in the paper; no machine-checked version exists. Formalizing it means checking the full chain from the patient's optimization to the population averages: that the argmin of produces the threshold structure of Proposition 2 with the stated thresholds, that the per-belief probabilities on p. 11 follow from the optimal actions (including the boundary cases the page leaves implicit), and that the integrals evaluate as claimed. Two printing slips in the proofs (a right-hand side for , and a denominator for ) are corrected in the milestone statements.
The final integrals are elementary once the integrands are known. The work is in the integrands. is not given; it comes from which of three costs is smallest at , and, for a caller, which provider is chosen at each of two posteriors that are rational functions of . On the calling range the patient must go to the PCP after the prediction sick and to the ED after critical, i.e. , and this is what makes . That in turn needs the inequalities and , which use and informativeness, and the linearization of the teletriage cost in the middle range. Reading off the display on p. 11 skips exactly this argument.
Everything lives in the namespace Teletriage.OneShot and in ℝ. A single definition file holds the parameters , the standing assumptions, the posteriors, the costs, the optimal actions, the probabilities, the uniform average and all thresholds.
Conventions:
Not in scope: the traditional-access model (Propositions 4–5), the open- vs traditional-access comparisons (Propositions 6–7, Corollaries 1–2), the sequential POMDP (Lemma 1, Propositions 8–9), and the uninformative cases of Proposition 1.
Welcome contributions: proofs of the milestones in any order. The algebra of milestones 3–4 is self-contained and reusable for the traditional-access analogue (Proposition 4).
Loot boxes are a selling format for virtual items in video games and digital collectibles: the customer pays a fixed price for a box whose content is a random item from a catalog. They generate a large share of revenue in the game industry and have drawn regulatory attention because the customer does not know what they are buying. From the seller's side they are a form of probabilistic selling, close to bundling: a box is a lottery over the catalog, and repeated purchases let a customer assemble a collection.
Chen, Elmachtoub, Hamilton and Lei (Loot Box Pricing and Design, Management Science 2021; the mission follows the authors' manuscript submitted in August 2019) compare two designs. A unique box never repeats an item the customer owns; a traditional box draws uniformly from the whole catalog, so duplicates occur. Their headline asymptotic results are that, as the catalog grows, the optimal unique box earns the mean valuation per item, as much as the grand bundle (Theorem 2), while the optimal traditional box earns exactly a fraction of it (Theorem 3). This mission formalizes the traditional-box result.
A monopolist sells distinct virtual items. A customer's valuations are i.i.d. with a law on with mean and finite variance . A second copy of an item is worth nothing.
The seller offers a traditional box at a fixed price in every period. Each box contains an item drawn uniformly at random from , independently of the valuations and of earlier draws. Let be the set of distinct items owned before the -th box, so . The expected utility of the -th box is
The customer is myopic: they buy the -th box if and only if , and the first time they leave for good. The normalized revenue at price and the optimal normalized revenue are
The milestones use a random walk. For i.i.d. with law , the first passage above a level is ; the paper's is . Also , where is the Euler–Mascheroni constant.
It holds for every valuation law in the model, with no condition on the shape of beyond non-negativity and a finite variance.
whose right-hand side tends to when .
The result. Theorem 3 quantifies the price of duplicates. A traditional box loses a factor against the unique box, the grand bundle and the upper bound of the paper's Proposition 1, for every valuation distribution, so in large catalogs the unique box earns about more per item. The constant comes from the interplay between the coupon-collector waiting times and the price at which the myopic customer stops; the identity and the bounds expose that interplay as a statement about the first passage of a random walk.
Formalizing it. The result is proved on paper, not formalized. Two of the printed steps of the proof need repair: the harmonic-number rewriting in (16) drops one term, and the per-price upper bound (25) derived from it is false at small prices (for , , the revenue is while (25) gives ); its maximization also ignores prices above . The milestones state the corrected claims, and the limit survives. A machine-checked proof therefore settles the headline result independently of the printed argument.
The number of boxes a myopic customer buys depends on all valuations and on the random order in which distinct items arrive, and the index at which the customer stops is not a stopping time of the forward purchase process: whether the customer continues depends on valuations of items not yet collected. Applying Wald-type identities directly to the purchase sequence therefore fails. The revenue identity (16) also mixes two sources of randomness, the coupon-collector waiting times and the values in order of collection, whose independence must be established rather than assumed. On the upper side, the expected first-passage index needs an overshoot bound for renewal processes (Lorden's inequality), which Mathlib does not contain, and the limit needs an upper bound that is uniform over all prices, including prices far above where the per-price estimate of the paper breaks down.
All declarations live in the namespace LootBox.TB. The valuation law is a probability measure F : Measure ℝ with F (Set.Iio 0) = 0 and MemLp id 2 F; is ∫ x, x ∂F and the centred second moment. The sample space for items is valuations × draws, (Fin N → ℝ) × (ℕ → Fin N), with the product of Measure.pi of and Measure.infinitePi of the uniform law on Fin N; draw is the item of the -th box. The purchase count is the first with , valued in ℕ∞; expectations are lower Lebesgue integrals and revenues live in ℝ≥0∞, so no expectation is truncated by toReal. The paper's is a supremum over . The goal is indexed by so that the uniform law is defined. The page's backward walk , extended by virtual i.i.d. variables, is represented by the partial sums of an i.i.d. sequence under walkLaw F = Measure.infinitePi (fun _ => F).
The hypothesis appears in the milestones that divide by , not in the goal: when nothing is bought and both sides of the limit are . A formalization in which revenue is a real number obtained by toReal, or in which prices may be (where a customer with zero valuations buys forever), could make bounds vacuous; neither is used here.
A complete development needs the coupon-collector decomposition of the purchase count, the exchangeability of the values in order of collection, Wald's identity and Lorden's overshoot bound for i.i.d. non-negative walks, Chebyshev's inequality (meas_ge_le_variance_div_sq), Jensen's inequality for , and the bounds and (Mathlib's NumberTheory/Harmonic). Wald's identity and Lorden's bound are reusable well beyond this mission. Proofs of individual milestones, and of the renewal-theoretic lemmas they need, are welcome.
Convex optimization often minimizes a function obtained by applying one convex function to the output of another map. The inner map may be vector valued, and its components need not be linear. To understand sensitivity, optimality conditions, and dual formulations for such a convex composite, one needs its Fenchel conjugate. Standard formulas for an affine inner map do not directly describe a nonlinear, partially defined map. Burke, Hoheisel, and Nguyen treat this setting in finite-dimensional Euclidean spaces and identify conditions under which the conjugate has an exact, attained representation over a polar cone (Burke–Hoheisel–Nguyen, pp. 3, 10).
The paper distinguishes monotonicity of the outer function along the particular epigraph of the inner map from monotonicity throughout the entire cone order. This matters when the outer function behaves well on the points the inner map can reach but does not satisfy a stronger global condition. Its Theorem 12 gives a conjugacy formula under a point-based condition on relative interiors; subsequent results use it to describe subgradients and additive composites (Burke–Hoheisel–Nguyen, pp. 8, 10–13). The mission isolates the conjugacy theorem and the source results that support it.
Let and be finite-dimensional real inner-product spaces. A closed convex cone defines the relation when . Its polar cone is . A possibly partial map , where adjoins one formal value , has an effective domain on which its values lie in . Its -epigraph is
The map is -convex when this set is convex. The paper assumes throughout §4 that is nonempty (Burke–Hoheisel–Nguyen, pp. 6, 10).
The outer function belongs to : it is proper and convex but need not be lower semicontinuous. The composite equals on and outside . The key monotonicity condition, numbered (7), is whenever . It is restricted to the epigraph of , unlike global -increasingness (Burke–Hoheisel–Nguyen, pp. 6, 8).
For an extended-real function , the Fenchel conjugate is . The scalarization takes value on and elsewhere. Its conjugate and the conjugate are combined in the dual function
Here means interior relative to the affine hull, and means the set where is finite (Burke–Hoheisel–Nguyen, pp. 4, 6, 10).
The goal is Theorem 12(c). Suppose is a closed convex cone, is proper and -convex, satisfies (7), and the Slater-type condition (10) holds:
Then the formula has an actual minimizer at every and the effective domain has an exact description:
The milestones follow results stated in the paper: Theorem 2 on conjugacy and infimal convolution; Lemma 6 on support functions; Lemma 4 on the relative interior of a -epigraph; and parts (a) and (b) of Theorem 12, which establish a closure bound and properness with attainment for (Burke–Hoheisel–Nguyen, pp. 5–7, 10).
The theorem turns the conjugate of a nonlinear composite into a minimization over the negative polar cone. It also identifies exactly which dual arguments give a finite value. Attainment matters because later subgradient formulas can use a specific minimizing multiplier rather than only an approximating sequence. In this paper, Theorem 12 is followed by a subdifferential formula for and a formula for the additive composite (Burke–Hoheisel–Nguyen, pp. 10–13).
The mathematical theorem is proved in the source paper. The formalization task is to give its statement a machine-checkable meaning and then prove that statement from a reusable collection of facts about extended-real conjugacy, support functions, cones, and relative interiors. The imported definitions of conjugacy and closed convex cones already have published formal interfaces; the paper-specific definitions and theorems in this mission are draft statements and do not yet have machine-checked proofs.
The main obstruction is the interaction between closure and conjugacy of a sum. A direct interchange of a supremum over primal points and an infimum over cone multipliers does not itself establish equality or the existence of a minimizing multiplier. Theorem 2 supplies a finite-dimensional conjugacy rule under a relative-interior qualification, while Lemma 4 identifies the relative interior of the relevant epigraph. The source then needs to account for the extended-real values of a partial map and for an outer function that is convex but may not be lower semicontinuous (Burke–Hoheisel–Nguyen, pp. 5–6, 10–11).
The Lean model uses finite-dimensional real inner-product spaces and EReal for extended-real values. The partial map is a pair : is its domain, and values of the total representative outside are ignored. Properness of is the explicit hypothesis . The effective domain of an extended-real function excludes ; this corrects a printed in the paper's definition. Conjugacy, epigraph convexity, , closed convex cones, and polar cones reuse published definitions. The lower semicontinuous hull follows the paper's sequential-limit definition, and is Mathlib's intrinsic interior. Pairings on are sums of the two component inner products.
The theorem keeps the infimum and minimizer inside , uses relative rather than ordinary interior in (10), and retains the properness and finite-dimensional hypotheses. These conventions prevent a vacuous or weaker encoding. Attainment is a separate existential statement, including the case where the minimum is . The printed in Theorem 12(a)'s scalarization clause is read as because each scalarization has domain ; the paper's Lemma 10 uses that same space. Theorem 2's closure identity is stated under the added hypothesis . With the paper's definition of as the lower semicontinuous hull, the unconditional identity fails when . The cited source theorem uses a closure that is identically for improper functions.
The mission develops the definitions of effective domain, closure, infimal convolution, indicators and support functions, -epigraphs, scalarizations, condition (7), and . Contributions proving the listed milestones or building general lemmas for those definitions are in scope. Corollaries 14 and 16, the other corollaries of §4, and the applications of §5 are outside this mission (Burke–Hoheisel–Nguyen, pp. 11–27).
Allocating divisible resources among agents with money-like budgets is the setting of Fisher markets. When agents report their preferences, a central planner can compute a market equilibrium, and by the Eisenberg–Gale convex program that equilibrium maximizes the Nash social welfare, the budget-weighted geometric mean of utilities. This objective is a standard compromise between efficiency and fairness, and is scale-free in each agent's utility.
The catch is that agents may misreport. Brânzei, Gkatzelis and Mehta (arXiv:1607.01569v3, published in Operations Research, 2022) ask how much Nash social welfare is lost when agents act strategically in simple market mechanisms, measured by the price of anarchy: the worst ratio between the optimal Nash social welfare and the welfare at a pure Nash equilibrium. One of the mechanisms they study is the Trading Post game of Shapley and Shubik (Shapley–Shubik 1977), in which each agent splits its budget into bids on the goods, and each good is shared in proportion to the bids it receives.
For agents with Leontief (perfect-complements) utilities, the plain Trading Post game may have no pure equilibrium at all (Example 4.4 of the paper). The paper repairs this with a small entrance fee : a bid below buys nothing. This mission formalizes the main result of §4.2: with a small enough fee, every pure Nash equilibrium has Nash social welfare within a factor of the optimum.
There are agents and divisible goods, one unit of each. Agent has a valuation vector , a budget , and a demand set , assumed nonempty. Its Leontief utility for a bundle is
so the agent wants the goods in the fixed ratio . An allocation is feasible if and for every good. With , the Nash social welfare is
In the Trading Post game with entrance fee , , agent chooses bids with . A bid is effective, , if , and otherwise. Agent receives of good when , and nothing otherwise. A profile is a pure Nash equilibrium if no agent can raise its utility by switching unilaterally to another bid vector.
Throughout §4 the paper assumes perfect competition: each good is demanded by at least two distinct agents.
The proof passes through Fisher-market prices. Given prices , let be the cost of one unit of utility for agent . A pair is an -market equilibrium (Definition 4.6) if goods with positive price are sold out, every agent spends exactly its budget, and no bundle that agent can afford gives it more than .
For every and every entrance fee , every pure Nash equilibrium of satisfies
for arbitrary budgets .
The proof has two halves, and the milestones follow them.
The result shows that a decentralized, prior-free mechanism, in which agents only place bids, implements the Nash social welfare objective for perfect complements up to an arbitrarily small loss. By contrast, the paper shows that the centralized Fisher market mechanism with strategic Leontief agents has price of anarchy (Theorem 3.9), so the bound here is a strong guarantee for a simple mechanism. Theorem 4.8, which the authors flag as of independent interest, says that approximate Leontief market equilibria are approximately optimal for Nash social welfare. That is a robustness statement about the Eisenberg–Gale optimum, useful independently of any game.
The result is proved on paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A complete development produces a reusable formal model of Fisher markets with Leontief utilities, -market equilibria and the Trading Post game, the first such model on the platform, and checks two printed slips that the formalization repairs (see the scope section).
Without the fee, equilibria need not exist, and the natural argument "an equilibrium is a market equilibrium" fails: agents can leave tiny bids on goods they barely need, and the induced prices then misrepresent demand. With the fee, an equilibrium is only an approximate market equilibrium. Each agent is forced to leave a bid of exactly on its non-tight goods, and the money spent there must be shown to cost at most a factor in utility. That accounting is where the bound and the normalization enter.
The second half needs a welfare comparison between an approximate equilibrium and the unknown optimum. The paper uses duality for the Eisenberg–Gale program, in the dual form due to Devanur (2009, manuscript). An exact-equilibrium argument does not transfer directly, because approximate optimality of each agent's bundle must be converted into a product bound over all agents with budget weights.
Agents and goods are Fin n and Fin m; all quantities are real numbers. The standing assumptions are bundled in Standing: , , , and for every agent. Perfect competition is a separate predicate. It is a hypothesis of every Trading Post statement and not of the Fisher-market statements. The utility is a finite minimum over . The Nash social welfare uses real powers of nonnegative bases. Prices are , as in the proof. Deviations in the game range over the whole strategy set, including bids below the fee.
Three encoding choices are disclosed in the statements:
The goal is not trivialized by an empty equilibrium set. A sorry-free sanity check exhibits, for two agents and two goods with and , a pure Nash equilibrium of for every , and an -market equilibrium for every .
A complete proof needs weighted AM–GM, which is in Mathlib as Real.geom_mean_le_arith_mean_weighted. It also needs elementary but careful reasoning about best responses in the Trading Post game. The Fisher-market milestones and Theorem 4.8 are reusable for any later work on Leontief markets. Contributions to either half are welcome independently.
An online display impression often reaches an advertiser through a chain of ad exchanges and networks instead of through a direct sale. Each intermediary runs its own auction among its downstream bidders and decides what to report to the auction above it. Its profit depends on whether it wins upstream and on what it can charge downstream. Even when every local auction is a second-price auction, the sale becomes a sequential game in which agents choose mechanisms. Balseiro, Candogan and Gurkan study this game on a symmetric tree. They characterize a subgame perfect equilibrium in which every intermediary applies a projected virtual value to its highest downstream report (SSRN 2661459; journal version in Manufacturing & Service Operations Management, 2020, doi:10.1287/msom.2019.0854). The single-auctioneer case is Myerson's optimal auction (Myerson 1981). In it, a seller facing i.i.d. bidders with increasing virtual values sets the reserve at the zero of the virtual value.
The seller occupies tier of a symmetric -tree, intermediaries occupy tiers , and buyers are the leaves at tier . Every tier- node has downstream agents. Buyers' values are i.i.d. draws from a law on with lower support end , a continuous strictly positive density on its support, and a finite mean. Buyers report their values.
An intermediary's mechanism is a reserve and a nondecreasing reporting function . If its highest downstream report satisfies , it reports upstream. If it wins upstream, it allocates to that downstream agent. The seller runs a second-price auction with a reserve . A winning agent pays the minimum report that would still have won (Definition A.1). An intermediary's profit is what its winning child pays minus what it pays upstream.
For a law with cdf and density , the virtual value is and its inverse is . The projection point is . The projected virtual value equals below , equals from up to , and equals beyond. If has an atom at , these objects use the positive part (Definitions 3.1–3.2).
The anticipated reports are laws defined by recursion: and , the projected virtual value of the maximum of i.i.d. copies of (Definition 3.3). Assumption 3.1 asks that, for , has finite mean and its positive part has a continuous positive density and a strictly increasing virtual value.
form a subgame perfect equilibrium. Fix any tier and any history: arbitrary mechanisms in for tiers and any seller reserve. Then no tier- node gains by switching to any mechanism in . The seller gains nothing from any reserve instead of .
The theorem identifies optimal mechanisms at every tier from the distribution of the reports directly below that tier alone. It also gives the seller's reserve after the network has transformed the buyers' values. Every later result of the paper is stated at this equilibrium. Examples are the profit ratios along chains with generalized Pareto values, the effect of market size, and the comparison of network shapes. Without the characterization each of these would need its own strategic analysis.
The paper proves the result on paper; none of these statements has a machine-checked proof yet. Formalizing it means building a finite tree auction with threshold payments and laws of maximum reports. It also needs virtual values for laws on unbounded supports and with an atom at zero, and Myerson-type reserve optimality for such laws. The last two are standard tools of auction theory that are absent from Mathlib in this generality.
In a single second-price auction, truthful bidding is dominant and the reserve is the only choice. An intermediary is different. Its report changes its chance of winning upstream, while its reserve and reporting function change what it can charge downstream. So the local second-price argument does not settle its choice. In a tree, a deviation must also be evaluated after arbitrary upstream histories, including reporting functions that are flat on intervals or jump. There, ties and payment thresholds matter. The paper's closed payment formula (2) can disagree with the minimum report that actually wins under a fixed tie rule. With that formula, a deviation with a jump beats , so the theorem would be false. The anticipated reports also carry an atom at zero from tier on, so the one-stage lemma is needed in its atom version.
Laws are probability measures on ; is the pushforward of a product measure under . The density is the derivative of the cdf, read only at , where it also gives the virtual value of the positive part. The support of a positive part is the interval , and "" means . The general objects (virtual value, projection, regularity, reserve objectives) are a separate definition module, reusable beyond this mission.
The tree has buyers with a product law. A report below the reserve is no report, which is never allocated. Ties go to the lowest index, and a report equal to a reserve wins. Payments are minimum winning reports. Buyers report truthfully (Lemma 2.1(B)). The seller's reserves range over , and in Lemma 3.1 the competing bid is independent of the buyers. Strict increase of is an explicit hypothesis: Assumption 3.1 starts at tier , but and Lemma 3.1 need it at tier .
Expected profits are single integrals of realized profits. The equilibrium profit is nonnegative pointwise, so a non-integrable deviation never violates the inequality. Deviations range over all of , and histories over all upstream mechanisms and reserves, so the equilibrium cannot hold for want of competitors. With rate-one exponential values and one intermediary with one buyer, the intermediary earns . Proofs of any milestone, and the measure-theoretic groundwork (measurability of , laws of maxima, Myerson's reserve on unbounded supports), are welcome.
The Hospital Readmissions Reduction Program (HRRP), created by the US Affordable Care Act and run by the Centers for Medicare & Medicaid Services since 2012, cuts the Medicare payments of hospitals whose 30-day readmission rates exceed a benchmark computed from other hospitals. It is a form of yardstick competition in the sense of Shleifer (1985): a regulator that cannot observe a provider's costs pays it according to what comparable providers achieve. The penalty differs from Shleifer's scheme in three ways: it is scaled by a multiplier that grows as the benchmark readmission rate falls, it is capped, and no bonus is paid for beating the benchmark.
Arifoğlu, Ren and Tezcan (2021) build a game-theoretic model to separate the effect of each feature. Their Proposition 1 isolates the multiplier: with the cap and the no-bonus rule removed (the scheme they call HRRP-I), hospitals still choose readmission rates below the social optimum and treatment costs above it. Medical and policy researchers had argued informally that the multiplier distorts incentives; Proposition 1 is the paper's precise version of that argument.
There are identical hospitals. Patients arrive at each hospital at rate . Hospital chooses a readmission rate and a marginal treatment cost in the action box
and pays an investment cost to reach them. Each admitted patient is readmitted with probability , so the hospital treats patients per unit time at cost each.
Standing assumptions on (p. 10 of the paper): is twice differentiable, decreasing in each variable, and jointly convex; on ,
where subscripts denote partial derivatives.
The regulator's objective is the social welfare
where is a fixed total patient utility. A maximizer of over is the first best (Lemma 1 of the paper: it exists, is unique and is interior).
The regulator observes every hospital's cost, readmission rate and investment, and computes the yardsticks
Under HRRP-I hospital receives
and earns the profit . The factor multiplying the excess readmission rate is the multiplier. An equilibrium is a pure-strategy Nash equilibrium: a profile of actions in from which no hospital can raise its profit by changing its own action within . A symmetric equilibrium is an equilibrium in which every hospital plays the same action.
For every :
and for every equilibrium is symmetric.
The goal is the conjunction of milestones 2–4; Lemma 1 supplies the comparison point.
Proposition 1 is the paper's first main result and the base for its later analysis: the capped scheme HRRP-II and the actual HRRP (Propositions 2 and 3) are studied relative to the HRRP-I symmetric equilibrium, and the remedy the paper proposes (m-HRRP, Proposition 4) removes the multiplier precisely because Proposition 1 identifies it as a source of distortion. The ordering says that hospitals over-invest in readmission reduction; says that, as a consequence, they under-invest in reducing treatment costs.
The paper's proofs are in its online appendix, which is not part of the source this mission cites (the authors' accepted manuscript, LBS Research Online eprint 1402). No machine-checked proof of any statement of the paper is known. The mission produces a checked version of the model and of all three claims of Proposition 1; the two-hospital claim in particular has no published argument in the cited source.
Lemma 1 is the routine part. The ordering claim is harder: a symmetric equilibrium need not be interior (in simple examples ), so the first-order conditions of the hospital's problem hold only as variational inequalities on , and the comparison with must work from those inequalities and the curvature hypotheses alone. The existence claim needs a fixed-point theorem for the best-response map of a hospital facing yardsticks , and therefore continuity of the best response, which rests on strict concavity of the hospital's profit; Brouwer's theorem is not in Mathlib. The two-hospital claim is a uniqueness-type statement about a two-player game with non-separable payoffs; the obvious route through contraction of the best-response map does not follow from the stated assumptions without further estimates.
The Lean development lives in the namespace ReadmissionsHRRP.HRRPI. A Model carries lam (, a Lean keyword), V, the box bounds and the curried cost R r c. Partial derivatives are deriv of the sections of R. Profiles are maps Fin N → ℝ × ℝ (first coordinate , second ); the averages divide by the real number . The equilibrium notion is the published pure-Nash relation CarbonDoubleCount.Planner.IsPureNash, with every hospital's feasible set equal to ; deviations keep the other hospitals' actions, so the yardsticks of the deviating hospital do not move.
The standing assumptions are one predicate, Model.Standing: the inequalities on the box bounds, (implicit in the paper), of class on an open set containing , non-increasing in each variable on , jointly convex on , and the two pointwise curvature conditions on . The paper's Appendix A, which imposes boundary conditions "to ensure that optimal actions are interior", is not in the cited manuscript; it is replaced by the separate hypothesis Model.FirstBestInterior, that every maximizer of over is interior. Every theorem assumes .
The first best is a maximizer of over , never a solution of the first-order conditions; the ordering claim quantifies over every such maximizer, and the existence claim is part of the goal so that the ordering claim is not vacuous. A sorry-free sanity file checks that the hypotheses are jointly satisfiable for , , .
Useful infrastructure: strict concavity on a box from a Hessian condition, variational inequalities at constrained maxima, continuity of argmax maps, and Brouwer's theorem on a planar box (proved on the platform as AGT.brouwer_fixed_point). Contributions to any of these, or to the hand proofs of the separate claims, are welcome.
The apparel industry produces far more garments than it sells. A large part of its environmental footprint comes from overproduction: inventory made against uncertain demand and then burned, landfilled or downcycled. Mass customization (MC), where a garment is made to order after the customer specifies it, is often promoted as a remedy. Under MC, supply matches demand exactly for the products it makes.
Alptekinoğlu and Örsdemir (MSOM, 2022; SSRN 3685235) ask whether this intuition survives once the firm's profit motive is taken into account. A firm that adopts MC does not abandon mass production (MP). It runs a hybrid system and re-optimizes its mass-produced line around the new option. The paper characterizes exactly when adopting MC is a win-win, meaning more profitable and better for the environment, and when the hybrid firm ends up overproducing more than the pure MP firm would.
Consumers' ideal products are spread uniformly on the Hotelling line . A consumer at distance from a mass-produced product priced gets utility . The total market size is random: with probability , otherwise, where , , and . Units cost , and offering variants costs .
The MP firm chooses the number of variants , the market share of each variant (which fixes the price ) and the stock of each variant before is known. Its expected profit is
The hybrid firm can also make any consumer's ideal product to order, at price , but the consumer then bears a waiting cost . It adds MC share , with , and earns an additional .
The environmental impact counts per sold unit (production, use, disposal) and per leftover unit (production, overproduction):
MC is made to order and leaves no leftovers.
The standing assumptions are , , and . Products are classified by the cost-adjusted value as high-value (), moderate-value () or low-value (). The paper's thresholds are closed-form functions of the parameters (Table 2 of the paper).
Adopting MC is a win-win if and only if
Here "win-win" means that both firms' problems have optimal decisions and that every optimal hybrid decision is strictly more profitable and has strictly lower expected impact than every optimal MP decision.
The result separates the two ways MC changes the footprint. It adds sales, because the gaps between mass-produced variants are now served, and each such sale carries the impact . It also reshapes the mass-produced line: the market served by MP shrinks, each variant captures a smaller share at a higher price, and stocking for the high market size can become profitable (§4.2, pp. 16–17). That raises overproduction even though the MC part produces none. Proposition 3 states exactly when the net effect, together with the profit gain, is a win-win. The paper's policy section (§6) builds on this characterization to study how promoting MC, a disposal fee for overproduction, and recycling move the win-win region.
The paper proves the result by hand, with case analyses across nine orderings of thresholds. No part of the model or its proofs has been machine-checked. A complete development gives a checked solution of a newsvendor-type stocking problem embedded in a Hotelling variety model, which is a common pattern in operations-management research.
Both optimization problems are non-concave. Profit is piecewise in (Lemma 1), and after substituting the optimal stock it is piecewise in , with a kink at and a corner at full coverage . The global optimum therefore switches between four solution types, and the switching thresholds include , a root of a non-polynomial equation. A comparison of first-order conditions alone does not settle which type is optimal. The goal compares two such case analyses, MP and hybrid, at once, so the threshold orderings ( versus , versus , versus ) have to be established across all three product-value classes.
Contributions are welcome on any milestone. The stocking lemmas and Lemma 2 are elementary. The root lemmas need monotonicity analysis of . Propositions 1 and 2 are the bulk of the work.
New brand-name drugs, in particular biologics, are expensive. Their benefit is also uncertain: a given patient cannot know in advance whether the treatment will work for her. Outcome-based pricing (also called performance-based or risk-sharing agreements) responds to this. The manufacturer is paid only when the treatment reaches a pre-specified goal and rebates the price otherwise. Agreements of this kind between manufacturers and payers have been signed for cholesterol, diabetes and oncology drugs. Carlson et al. (2010) give a taxonomy. Whether such a contract actually helps the parties that must agree to it is a question about incentives. It cannot be settled by noting that the patient bears less risk.
E. Adida (Management Science, 2021; accepted manuscript at eScholarship) studies it in a three-stage game between a monopolist firm, a payer and risk-sensitive patients. The patients follow prospect theory (Kahneman and Tversky 1979; Tversky and Kahneman 1992). The paper's headline result is that, in the region where the payer covers the drug under both systems, the firm and the payer typically disagree about outcome-based pricing. A side payment from the firm to the payer can make both strictly better off, but only for high-risk drugs. This mission formalizes that result and the chain of equilibrium computations that leads to it.
There are patients with values , , a unit cost , a co-insurance rate and a success probability . On success the payer gains a fixed surplus . The game has three stages.
Under uniform pricing the price is paid on every purchase, and the buyer's welfare is . Under outcome-based pricing it is paid only on success, and the welfare is . Demand is times the measure of buyers in . The firm earns per buyer under uniform pricing and under outcome-based pricing. The payer's objective is its own expected payoff plus the patients' total expected (risk-neutral) payoff. It covers iff its objective with coverage is at least its objective without. An equilibrium price maximizes the firm's realized profit, with the payer's coverage response, over all .
Let
A drug is high-risk if and low-risk if ; the risk premium is positive exactly for high-risk drugs. Assumption 1 is . Assumption 2 is
with , , and the solution of . It is the region of large payer benefit, in which both systems end in coverage. Finally,
Under Assumptions 1 and 2, let and be equilibrium prices, and write and . Then
and, if and , : every transfer strictly between the two amounts, which runs from the firm to the payer, works.
In attack order:
Proposition 4 says that for a high-risk drug outcome-based pricing raises total firm-plus-payer surplus, even where it hurts the payer. A negotiated side payment therefore always exists that makes both parties prefer it. For a low-risk drug no such payment exists, because the payer's gain is smaller than the firm's loss. The result locates where outcome-based contracts can be self-enforcing and identifies the risk premium as the quantity that decides it. In this model the patients' loss aversion and risk sensitivity act on the comparison only through and .
The paper proves the result with explicit algebra once the equilibrium is pinned down. The formalization adds two things. First, the equilibrium layer is checked, not assumed: the statements quantify over the backward-induction equilibrium prices, with an explicit payer coverage rule and an integral model of demand. The closed forms and the unique optima , become theorems. Second, the formalization makes the small hypotheses explicit (positivity of , non-negativity of , strict versus weak improvement), which the published proof uses without listing. As far as is known, none of these results has a machine-checked proof.
The algebra of Propositions 3 and 4 is short once and with coverage are established. The work is in establishing them. The firm's realized profit is a discontinuous function of the price, because the payer's coverage decision switches at the thresholds , , , , which depend on the regime of . Showing that is the unique global maximizer requires comparing the covered and uncovered profit curves on every piece. It uses Assumption 1, the bound (which places above and above ), and the monotonicity of through the root of . Reading the closed forms off the paper's formulas is not enough: they must be derived from the purchase rule, which itself rests on the prospect-theory inequality . A natural shortcut is to state Proposition 4 at and directly. That deletes the equilibrium content and is not the goal.
All quantities are real numbers in one structure Params with a Standing predicate: , , , , , . Two of these are added to the page's assumptions: ( divides by ) and (used in the proof of Theorem 1).
Powers are Real.rpow on non-negative bases only. The roots (of ), (of ) and (of ) are passed as numbers together with their defining equation on ; uniqueness is a milestone. Demand and patient payoff are a Lebesgue measure and a set integral over the buyers in . Ties follow the paper: an indifferent patient buys, and an indifferent payer covers. "The firm prices at " is read as " is the unique equilibrium price". "Better for both parties" is read as strict improvement, and the paper's closed range of transfers is replaced by the open range, because at its endpoints one party is only indifferent. The payer's side of every comparison is its objective .
A formalization that fixes and by hypothesis, or takes the closed forms as definitions, would make the goal an algebraic identity. The goal here quantifies over all equilibrium prices of the integral model.
A complete development needs elementary real analysis (convexity and monotonicity of , rpow manipulations), Lebesgue measure and integrals over intervals, and piecewise maximization of concave quadratics. The prospect-theory value function and the threshold purchase rule are reusable for other behavioral pricing models. Proofs of any milestone are welcome, as are proofs of the omitted parts of Theorems 1 and 2 (the constrained prices , , , ).
The circular economy movement argues that manufacturers should keep control of their products after use (by leasing instead of selling) and design them so that worn parts can be replaced individually (a modular architecture). Each of the two levers has a long literature in operations management and economics. Leasing versus selling durable goods is studied in models of durable goods with secondary markets (Desai & Purohit 1998; Agrawal, Ferguson, Toktay & Thomas 2012), and modularity in the product-design literature, where its value lies in replacing modules independently. Agrawal, Atasu and Ülkü (Management Science) ask whether the two levers reinforce each other: when is leasing a modular product strictly the most profitable of the four combinations of business model and architecture? Their answer (Proposition 3) is a closed-form partition of the parameter space by cost thresholds, and it shows that the combination is optimal only under limited conditions.
A monopolist offers a durable product made of two modules, each with a useful life of two periods; module 1 is the more durable one. A customer of type , uniform on , values a new product at per period. Under selling, a used module retains a fraction of its value; under leasing, off-lease modules retain , where is the relative return condition (: off-lease products are in worse shape than previously sold ones; : in better shape). Each module costs to produce. The standing assumptions are
In steady state the firm solves one of four quadratic problems, each written in quantities through inverse demand functions derived from customer self-selection and secondary-market clearing:
The optimal profits are the attained maxima of these problems. The paper's thresholds are explicit functions of :
together with , , and the square-root expressions , of the Appendix.
With ties between architectures broken towards the integral one (footnote 13 of the paper):
In each region the chosen option's optimal profit strictly exceeds the others, except at exact ties of the model. These are for , for , , and at further ties between leasing and selling. The goal states these as equalities or weak inequalities and restores strictness for .
The result gives a complete description of the firm's joint choice in a standard durable-goods model with a secondary market, and it qualifies a common claim. Leasing a modular product is strictly optimal only at low production cost. For modularity can even push a leasing firm to selling (Proposition 2), and for the firm never sells. The thresholds feed the paper's later environmental and consumer-surplus comparisons.
The paper's proofs are pencil-and-paper KKT computations reported in compressed form, and nothing in the paper is machine-checked. A formalization would certify the four closed-form optima, every threshold comparison, and the case split of Proposition 3. It would also settle two printing errors found while preparing this mission (see below), one of which changes the statement of Lemma 2 and Proposition 3.
Each firm problem is a strictly concave quadratic program over a polyhedral cone, so existence of the optimum is routine. The difficulty is everything after that. The optimum changes face as moves: LM alone has four KKT cases, and each must be shown to be optimal exactly on its cost interval. The profit comparisons then reduce to sign conditions on rational functions of four parameters. Some involve the square roots in and , which are only meaningful for and are defined as roots of quadratics in , so the comparisons must be placed relative to them. The ordering is an inequality between such expressions on the whole parameter region. It is not a symbolic identity, and checking it at sample points proves nothing.
IsGreatest (profit '' feasible) v, never a supremum without attainment. Statements about the optimizer ("the UN segment exists", "") quantify over every optimal decision.Real.sqrt for , , , . and are used only for , where their radicands are nonnegative.Online platforms show a reader many short signals about the same question (posts, headlines, tweets), more than the reader can absorb. The reader screens the menu and consumes only a few items. Allon, Drakopoulos and Manshadi (Information Inundation on Platforms and Implications, SSRN 3385627; Operations Research, 2021, doi:10.1287/opre.2021.2119) ask what a purely information-seeking reader picks when the accuracy of each post is unknown. Their answer, Proposition 1, is that she picks the post closest to her current belief, the effect the paper calls screening bias. It is the mechanism behind the paper's later results on slow learning and polarization, and it explains a pattern resembling confirmation bias without assuming any bias in how beliefs are updated. Confirmation bias was documented empirically by Lord, Ross and Lepper (1979) and modelled through source reputation by Gentzkow and Shapiro (2006) and Suen (2004). In those models the bias comes from repeated interaction with strategic sources; here it comes from a single screening decision by a Bayesian reader.
An unknown fact is a real number . A post is a noisy observation
where and the accuracy (a standard deviation) is drawn independently from a publicly known law . The paper assumes throughout (§3, p. 8) that is a probability law whose support lies in an interval with .
A consumer holds a normal belief about , with . From her point of view, a post of accuracy is distributed , so its likelihood is
By Bayes rule (4), her posterior on the accuracy after seeing the post value has density proportional to with respect to ; write for the posterior expectation.
If she reads a post and learns its accuracy (ex-post known accuracy), her belief becomes normal with standard deviation (Belief Updating Equations). Before reading, she scores each post by the expected reduction of her uncertainty. The Screening Equation prints the score as
while the text calls it the expected decrease in posterior variance, . A menu is a finite list of post values, and she picks a post in the argmax of the score.
In Lean the model lives in InfoInundation.Screening.Model: AccuracyLaw G (the standing assumption), psi, likelihood, postExp (the Bayes ratio), nextSd, sdScore, varScore, argmaxMenu, closestPosts, and the auxiliary moments auxMoment/auxExp used in the proof.
For every accuracy law satisfying the standing assumption, every belief with and every menu :
(a) if is not a point mass,
(b) if with , the argmax of both scores is the whole menu.
The proof on pp. 10–11 has no numbered lemmas; the milestones are its labelled steps:
Proposition 1 turns a modelling choice (each reader maximizes expected information) into a behavioural prediction (each reader consumes the post nearest her belief). Every later result of the paper is built on it: the slow-learning theorem, in which the speed of learning decreases with menu size, and the multimodal belief distribution, both come from feeding the closest post back into the belief dynamics. Part (b) is the benchmark: with known equal accuracy there is no screening bias, and learning is fast.
The result is proved in the paper; it has no machine-checked proof. The mission produces one, and with it a small reusable library on posteriors over a Gaussian scale mixture: the predictive density of a normal belief under a known noise scale (milestone 1), a measure-theoretic Bayes rule for the noise scale given one observation (milestone 2), and moment inequalities under exponentially tilted mixing laws (milestones 5–6). The formalization also settles two points that the printed proof leaves open (see Difficulty): which of the two scores the conclusion holds for, and why the conclusion is an equality of sets rather than an inclusion.
The proof covers the variance score. Reducing it to the monotonicity of in is algebra. The monotonicity itself requires differentiating a ratio of -integrals under the integral sign, for an arbitrary law , which in turn needs the boundedness of the support to dominate the integrands.
Three places need more than the printed argument:
Measure ℝ with AccuracyLaw G: a probability measure with for some . "Supp() includes at least two distinct values" is ∀ σ, G ≠ Measure.dirac σ; "Supp() = {σ}" is G = Measure.dirac σ with .Z : Fin K → ℝ; argmax and argmin are Finset (Fin K), so posts of equal value are distinct posts, and "" is Finset.univ.Needed infrastructure: dominated differentiation of parameter-dependent integrals against a finite measure on a bounded set (Mathlib's hasDerivAt_integral_of_dominated_loc_of_deriv_le), the equality case of Cauchy–Schwarz in , Gaussian convolution (gaussianReal_add_gaussianReal_of_indepFun) and conditional expectation via densities for milestone 2. Contributions of a covariance or likelihood-ratio ordering lemma for the standard-deviation conjunct are welcome as supporting theorems.
A new venture rarely knows two things at once: whether its core idea is worth anything, and whether the particular way it has chosen to bring the idea to market — its strategy — will work. A failed pilot, a disappointing A/B test or a lukewarm customer experiment can mean either, and the founder cannot tell which. Work on entrepreneurial experimentation (Kerr, Nanda and Rhodes-Kropf, Journal of Economic Perspectives, 2014, doi:10.1257/jep.28.3.25; Gans, Stern and Wu, Strategic Management Journal, 2019, doi:10.1002/smj.3010) treats testing as the main tool founders have to resolve uncertainty before they commit resources.
Agrawal, Gans and Stern (NBER Working Paper 27379, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3920) give a two-period model in which a single test produces a conflated signal about the idea and the strategy together. Two consequences come out of it. A signal that the strategy is good can still lead the entrepreneur to abandon the venture. And when a mentor can sharpen a test, the better direction to sharpen it depends on the founder's prior beliefs. This mission formalizes the model and its two propositions.
The idea is worth (state ) with prior probability , or (state ). Value is realized only if the strategy used is effective (state , against ineffective ). Every strategy is effective with prior probability , independently of every other strategy and of the idea, and there are several strategies to choose from. Implementing a strategy costs and testing one costs . The standing assumptions are
where means that launching a randomly chosen strategy without testing exactly breaks even.
A test of the selected strategy has precisions and emits one of four signals, , , or :
| w.p. | w.p. , w.p. | |
| w.p. , w.p. | w.p. |
Write and for the posterior probabilities that the idea is high-value and that the tested strategy is effective, given signal . Assumption (A1), that tests are weakly informative, requires
After the signal the entrepreneur picks one of three period-1 actions:
is the best of these three conditional values. The value of testing is
The strategy-biased test is and the idea-biased test is , where is the baseline test.
For baseline precisions , if both precise tests satisfy (A1) and
then
The statement leaves and the baseline precisions free, subject only to the standing assumptions.
Proposition 2 answers the question a mentor faces when it can make a test more precise in one direction only. A test with high makes abandoning a poor idea more efficient. A test with high makes it more efficient to continue the idea with a different strategy. The condition weighs these two benefits, and it shows that the choice is driven by the prior . Proposition 1 shows why: the idea is the same in every test while the strategy can change, so switching strategies after an ambiguous signal is how the entrepreneur learns about the idea. The paper's later sections (differing priors between mentor and entrepreneur, §5.2) start from these two results.
The results are proved in the paper by hand-calculation, and Proposition 2 has no printed proof. No part of the model has been machine-checked before. The formalization produces an explicit, reusable encoding of a two-dimensional Bayesian test with a conflated signal, together with machine-checked versions of the case analysis that Proposition 1 summarizes. It also gives a checked replacement for the printed display: the second line of that display does not follow from the first.
The obvious argument reads the paper's prose, takes and as given, and subtracts. In the formal model these values are optima over three actions, computed from the signal table, and each one needs an argument.
The model lives in the namespace EntrepChoice.TestChoice. Params holds . Standing collects the standing assumptions, with kept as the hypothesis rather than substituted. Test holds , and Test.Valid bounds both in . The states, signals and actions are small inductive types, and sums over them are written out explicitly.
Action values are unnormalized: times the conditional expected payoff. With this choice (testValue) needs no division. (A1) is stated cross-multiplied by . It agrees with the posterior form whenever and is harmless when . The posteriors p1 and e1 are real quotients, equal to on a probability-zero signal.
Several conventions are disclosed readings of the paper:
testValue is the maximum over the three period-1 actions, built from the signal table. It is never defined by the closed form of milestone 6, and neither Standing nor A1 mentions it, so the goal cannot be closed by unfolding a definition.
Contributions are welcome on every milestone. Further results of the paper — testing order under irreversibility (§4.1), heterogeneous strategy priors (§4.2) and the mentor–entrepreneur game with differing priors (§5.2) — are natural follow-on missions on the same definitions.
Farmers who sell the same crop can benefit from better forecasts of the market price, but their production decisions also affect one another through the price. A forecast sent to one farmer may improve that farmer’s decision; a forecast sent to many farmers can make their output responses move together. A planner choosing who receives a common forecast therefore faces a question that differs from asking whether the forecast is accurate. Zhou, Fan, Chen and Tang study this question for a public signal about the uncertain intercept of a Cournot market’s inverse demand curve in Information Provision and Farmer Welfare in Developing Economies (SSRN preprint dated June 27, 2019, §§3–4).
The paper’s base model concerns a publicly funded information service. The planner can send the same signal to any number of farmers without charging them, and its objective is the sum of farmers’ expected profits. The target here is the paper’s Proposition 2, which says that the planner should inform either exactly one farmer or none, according to the sign of an explicit polynomial in the model’s signal precisions and number of farmers. The statement is about equilibrium production choices and the resulting profits, rather than about forecast quality alone (Zhou et al., pp. 11, 14).
There are farmers producing the same good with deterministic yield. Farmer chooses a quantity and pays . The total harvest is , and the inverse demand at sale is , where is market potential, measures price sensitivity, and is a centered Gaussian demand shock. Farmer earns . The quantities in this formalization are real valued, as required by the paper’s affine equilibrium formula; this interpretation is explained below (Zhou et al., p. 8, (1); p. 10, (2)–(3)).
Each farmer sees a private signal . The are independent centered Gaussian noises of common precision ; the shock has precision . Thus their variances are and . A planner also observes a public signal , where the independent Gaussian noise has precision and variance . The planner chooses an informed set of farmers who may see ; every farmer sees only its own , and an uninformed farmer cannot use . Write , so is an integer from zero through (Zhou et al., pp. 8–9).
A farmer’s strategy is a measurable function of the information available to that farmer. The realized quantity must be square-integrable under the joint Gaussian law. A Bayesian Nash equilibrium is a profile of such strategies in which no farmer can increase ex-ante expected profit by changing only its own admissible strategy. Write for the sum of the expected profits of all farmers at a profile . Proposition 1 gives a linear equilibrium and its almost-sure uniqueness. Lemma 2 gives the ex-ante profit of each informed and uninformed farmer at that equilibrium (Zhou et al., pp. 12, 14, 34).
The goal is the equilibrium welfare conclusion of Proposition 2. Let be the explicit polynomial displayed in that proposition, with also fixed by the model. For every informed set, an equilibrium exists. When , every one-farmer informed set strictly outperforms all sets of another size. When , the empty informed set is optimal; for it strictly outperforms every nonempty set:
At , informing zero and one farmer gives the same welfare, so the second case asserts that zero is an optimal choice rather than the unique choice. The goal compares for every Bayesian Nash equilibrium of each informed set, allowing any subset of the prescribed size (Zhou et al., p. 14, Proposition 2; p. 36).
The milestone statements follow the claims used for that result: Lemma 1’s two Gaussian posterior identities; Proposition 1’s equilibrium existence and almost-sure uniqueness; Lemma 2’s profit formulas and advantage for informed farmers; and the Appendix A claims that welfare declines after two recipients, one recipient beats two, and the sign of is controlled by (Zhou et al., pp. 10, 12, 14, 35–36). Here is the paper’s closed-form welfare expression for the linear equilibrium, extended from integer to real only for the paper’s continuous analysis.
The result identifies the welfare-optimal reach of a common forecast in a competitive production market. Under the stated model, informing more farmers does not necessarily raise their aggregate expected profit. The threshold decides whether the planner should send the signal to one farmer or withhold it. Proposition 1 and Lemma 2 are needed to connect that policy claim to farmers’ actual equilibrium decisions, rather than to a free-standing polynomial comparison (Zhou et al., pp. 12–14).
The paper proves the result mathematically. This mission asks for a machine-checked development of the Gaussian signal model, the equilibrium result, the profit identities, and the final optimization statement. The Gaussian posterior and square-integrable game infrastructure can be reused in other information provision models. The proposal statements compile, but their proofs are open; no machine-checked proof of these mission claims is asserted here.
The planner can compare policies only after accounting for how all farmers change production when the public signal is shared. Informed farmers use both their private observation and the common signal, while uninformed farmers use only their private observation; the same signal changes both the informed farmers’ expected profit and the Cournot price faced by everyone. The linear equilibrium formula alone does not justify restricting all possible strategies to linear ones. The proof must establish that it is an equilibrium against every admissible deviation and that any equilibrium gives the same realized quantities almost surely. The integer policy choice must then be related to the paper’s real extension without allowing noninteger informed sets (Zhou et al., pp. 32–36).
Lean represents the uncertainty by a product of independent Gaussian measures for , the private noises, and the public noise. The variances are the reciprocals of the positive precisions , , and . Informed sets are finite subsets of Fin n, including the empty and full sets. The observation map gives to a member of and to a farmer outside , so neither type sees another farmer’s private signal. Strategies are measurable functions with square-integrable realized quantities, and both equilibria and deviations satisfy that condition. Welfare is the sum of integrals of realized Cournot profit. The goal quantifies over all equilibria and does not replace their welfare by the closed-form function .
The base game assumes , , , and positive ; no sign condition is imposed on . The paper mentions as an unavailable-private-signal limiting case, but a Gaussian noise with variance is undefined there, so that separate regime is outside this mission. The positive public precision likewise excludes the degenerate case. Equations (2)–(3) print , but the claimed affine equilibrium takes negative values with positive Gaussian probability; the formalization uses unrestricted real quantities, which is the game solved by the paper’s displayed first-order calculations. All of these choices are explicit in the statements and should be checked against the source’s intended reading (Zhou et al., pp. 8–10, 12).
The coefficient definitions , the linear profile, the two type-specific expected profits, and are fixed to the source displays. The useful contributions are proofs of the posterior identities, unrestricted equilibrium existence and uniqueness, expected-profit identities, and the welfare inequalities. Neither an arbitrarily chosen equilibrium nor an affine-only strategy class would establish the target.
A buyer may be liable for social responsibility violations among suppliers that remain in its production network. Auditing can prevent a later penalty, but the buyer must pay for each audit and then choose what to do with a supplier that fails. Dropping a supplier can also remove other firms that depend on it, changing the buyer's eventual production profit. Zhang, Aydin, and Parker study this decision in a three-tier supply network and establish a structural rule for an optimal auditing policy in Theorem 3. The rule tells the buyer how dropping and rectification can be ordered without specifying which supplier to audit first.
There is one buyer in tier 0 and two possible tier-1 firms, and . The tier-2 suppliers are divided into three disjoint sets: , whose members supply only ; , whose members supply only ; and , whose members supply both. A network is , where is the set of tier-1 firms still present. Its supplier set contains those tier-1 firms and the members of the three tier-2 sets. The set of dependents of supplier includes itself. For a tier-1 firm, it includes its exclusive tier-2 suppliers. For a tier-2 supplier, it also includes a tier-1 firm if that supplier is the firm's sole remaining tier-2 source.
An auditing state records the current network and its finite set of unaudited suppliers, . The state is terminal when . The operator vets an unaudited supplier without changing the network. The operator drops and . If a tier-1 firm is dropped, its formerly shared tier-2 suppliers become exclusive to the other tier-1 firm. These transitions are the paper's footnotes 3 and 4 on page 10.
At a state, the buyer can proceed to production (), audit and rectify an unaudited supplier (), or audit and drop one if it fails (). An auditing policy chooses an admissible action at every state. Let be the audit cost, the rectification cost, the chance that a supplier is noncompliant, the chance that an uncorrected violation is exposed, and the penalty for an exposed violation. If the buyer proceeds to production, it receives production profit less the expected penalty .
The optimal value is the maximum of the values of the admissible actions at , using the finite recursion (1)–(5) of §3.2. An optimal policy chooses a maximizing action at every state. The appendix also defines the value of a fixed policy and the restricted value when only and are available.
The main target is Theorem 3, page 19: some optimal policy first audits and drops any number of suppliers, perhaps none, and then enters a second subphase. In that second subphase it either rectifies all remaining unaudited suppliers, in any order, or proceeds directly to production. The choice is governed by the comparison
The inequalities are non-strict: both choices are permitted at equality. The statement applies at every state of the auditing process. Once the policy rectifies a supplier, it rectifies another at the successor state whenever unaudited suppliers remain; no later audit-and-drop action follows. Every available rectification action is optimal during this subphase.
Two appendix results are the milestones. Proposition D.1, OA-11 says that, for each starting state, a buyer can postpone rectification actions until after dropping actions without lowering its value at that state. Proposition D.2, OA-13 identifies the optimal value and actions in the restricted rectify-or-produce problem. With , its value formula is
Theorem 3 reduces the form of policies that need consideration: rectification need not be interleaved with later dropping, and the final choice between rectification and accepting exposure risk depends on one comparison of per-supplier costs. It does not resolve which suppliers to audit and drop, or when to leave that first subphase. Those decisions can still depend on the network and audit outcomes, as §5.1 explains.
The paper proves the structural result and its two appendix propositions. This mission asks for machine-checked proofs of those known statements, together with a reusable finite representation of network dependents, transitions, and Bellman values. The present draft statements compile with proof placeholders; they are not machine-checked proofs of the claims. The definitions also permit later work on other auditing rules over the same state space.
An audit-and-drop action can change the network and therefore production profit. Comparing it with an audit-and-rectify action is more involved than comparing their immediate costs: a dropped supplier can remove its dependents, and those losses affect all later decisions. The obvious choice of rectifying whenever ignores the possibility that a later drop removes the rectified supplier anyway. The structural theorem must account for both successor states of an audit and still produce one policy that is optimal at every state.
Tier-2 suppliers carry labels in an arbitrary type, while every individual network and unaudited set is finite. The tier-2 components of a network are pairwise disjoint. The Lean parameters explicitly require , , and . The paper derives from independent supplier outcomes; the formalization uses that derived formula, and its Bellman recursions already take the audit outcomes' expectations. The profit is any real-valued function of the current network. This is a disclosed generalization of the Cournot profit used earlier in the paper: §6.1 says the two-subphase result does not depend on the mode of competition, and (D.27) uses only that vetting leaves the network unchanged.
The value functions are defined by recursion on the number of unaudited suppliers. Their maxima are taken over exactly the admissible finite action set, and optimality is checked at every state. Transition functions are total, but the theorems use them only for unaudited suppliers. The action-value functions return zero for inadmissible supplier actions; the fixed-policy recursion returns the production value there. These values have no role for admissible policies. The formulation excludes an unattained policy supremum, a policy that is optimal only at a chosen initial state, or a special production-profit function. Contributions that establish the appendix propositions, the main structural theorem, or useful lemmas about the finite transitions and recursions fit this scope.
Online and omni-channel retailers promise delivery within a fixed number of days, and carriers charge less for slower service. A retailer that receives orders over time can therefore wait, collect several orders into one package, and send it by a slower and cheaper service, as long as no order misses its promised date. Waiting saves the fixed cost of a shipment but uses up the slack of the orders already waiting. This trade-off between shipment consolidation and expedited delivery is the subject of L. Wei, R. Kapuscinski and S. Jasin, Shipping Consolidation across Two Warehouses with Delivery Deadline and Expedited Options for E-commerce and Omni-channel Retailers (Manufacturing & Service Operations Management, 2020; author's manuscript SSRN 2920899).
The paper treats one and two warehouses, with fixed and with volume-dependent shipping costs. Its first structural result concerns the simplest case, one warehouse and a fixed cost per package: the optimal policy waits while the most urgent order has enough slack and ships everything once the slack falls to a period-dependent threshold. This mission formalizes that result and the lemmas its proof rests on.
Time is discrete and counted backward: is the number of periods to go and period is the last. Each order must be delivered at most periods after it arrives. The slack time of a pending order is the number of periods left until its deadline; slack means the order must leave now.
Shipping a package that must arrive within periods costs , the fixed shipping cost, which does not depend on the number of orders in the package. The paper assumes is non-increasing and convex (slower delivery is cheaper, with diminishing savings), and specifies it on . In each period new orders arrive with probability .
With one warehouse and fixed costs, the paper's Lemma 1 shows that it is optimal either to ship all pending orders together in one package or to ship none, at a cost depending only on the smallest slack among pending orders. The state is therefore , or when nothing is pending. The cost-to-go functions and satisfy the recursion (2)–(3): for and ,
with and . Holding is infeasible at . Shipping is optimal at when the ship branch attains the minimum; holding is optimal when it is feasible and the do-not-ship branch attains the minimum. With ties both are optimal.
For every period there is an integer such that, for every slack ,
The threshold may depend on , and no formula for it is asserted.
Theorem 1 reduces the policy of a -period stochastic control problem to one integer per period. The paper builds on it: Theorem 2 computes the long-run average cost of a constant threshold, Proposition 2 and Lemma 3 describe the best constant threshold, and the two-warehouse analysis of §5 and the heuristics of §7 start from this one-warehouse structure. Lemma 2 states that the cost-to-go reacts to a loss of slack at least as strongly as the current shipping cost does, which the paper calls counter-intuitive (p. 13); it is the property that makes the threshold exist.
The results are proved in the paper, with one gap: the proof of Lemma 2 is written out only for , and the case is described as similar and omitted. A formal proof closes that case. To the best of our knowledge none of these results has a machine-checked proof.
The natural first idea is to argue that the cost-to-go inherits convexity in from and then read off a threshold. That is not what is needed: the threshold needs a comparison between the slope of and the slope of (Lemma 2), and the paper notes (p. 13) that, without further structure, the difference can a priori be larger or smaller than , because the optimal shipping periods for slacks and may differ. The recursion couples two indices, period and slack, through the no-order value , and its boundary cases (, where shipping is forced, and , the last period) behave differently from the interior. The paper's own argument covers only ; the regime , in which the horizon ends before the most urgent order's deadline, is left to the reader.
valuePair F α d t returning . The reduction from the general dynamic program (1) over all slack vectors to (2)–(3) (Lemma 1) is not formalized; stands for the smallest slack among pending orders. All objects are deterministic; enters only through (3).Finset.inf', ConvexOn and natural-number arithmetic are needed. Lemma E1 is a self-contained fact about finite minima and may be reusable. Alternative proofs of Lemma 2 that avoid the unrolled form are welcome.Autonomous vehicles (AVs) can drive closer to one another than human drivers, because they react faster and can coordinate in platoons. Transport agencies and industry groups have therefore proposed reserving a designated lane for AVs on highways, so that AVs can exploit short headways without mixing with human-driven vehicles (HVs). Whether such a lane helps depends on a trade-off that is familiar from queueing theory: splitting a highway into two separate lanes loses the efficiency of pooled capacity, while a lane reserved for AVs moves faster when it is busy.
Mirzaeian, Cho and Scheller-Wolf (Management Science, 2021; manuscript SSRN 3278330) model a highway segment as a state-dependent loss queue and compare a no-AV benchmark with the designated-lane policy (the D policy). Their headline finding is that the D policy reduces mean travel time only when the highway is heavily loaded and AVs make up a large enough share of traffic. This mission formalizes that finding.
The queueing model is the state-dependent queue of Cheah and Smith (1994), developed for pedestrian flows, which Jain and Smith (1997) applied to vehicular traffic; its stationary law, display (12) below, is due to Cheah and Smith.
A highway segment has length and lanes, each holding at most vehicles. Vehicles arrive as a Poisson process of rate ; a vehicle that finds the segment full is turned away. When vehicles are on a segment of capacity , each travels at mean speed , for , with . This is the queue. Its stationary law is (display (12) of the paper)
its throughput is , and its mean travel time is, by Little's law, (display (13)).
The benchmark pools all lanes into one queue of capacity with speeds ; its mean travel time is . Under the D policy, a fraction of arrivals are AVs and must use the designated lane, so there are two independent queues: the AV queue (capacity , speeds , arrival rate ) and the HV queue (capacity , speeds , arrival rate ). The overall mean travel time is
The jam speeds , , are the speeds of full queues. The paper assumes throughout, and the AV lane is faster when full than the HV lanes, . The threshold is
For every with there is such that
The goal makes precise the paper's main policy conclusion: under heavy load a designated AV lane lowers mean travel time relative to the benchmark exactly when the AV share exceeds a threshold that depends only on the three jam speeds. Below the threshold, the loss of pooling dominates. This is the basis for the paper's caution against designating lanes for AVs while AV penetration is low, and the same heavy-traffic argument underlies its comparisons with the integrated policy (Propositions 2 and 3).
The printed Proposition 1(a) is not correct as stated, and the formal statement records the repair. Its heavy-load clause asserts a single valid for every ; the travel-time gap behaves like with affine and vanishing at , so no single threshold works for AV shares arbitrarily close to , and at the equivalence can fail for all . Its light-load clause (" for when is small") fails at whenever the AV lane is as fast as the benchmark at low occupancy and faster at higher occupancy, which includes the paper's calibrated model. The mission therefore poses the heavy-load clause pointwise in , excluding , which is what the paper's proof establishes. None of these results has a machine-checked proof; the queueing layer (the stationary law, travel time and their heavy-traffic limits) is new on the platform.
The heavy-traffic limits are the core. The obvious route, letting in the definition , gives the indeterminate form : the blocking probability and tends to the jam throughput. The limit has to be read off a rearranged expression, the closed form (16), whose leading terms in cancel to . Lemma 1 is a genuine monotonicity statement about a ratio of polynomials in whose coefficients depend on an arbitrary nonincreasing speed sequence; it cannot be checked degree by degree. The goal then needs strict separation of the two limits away from , together with an eventually-in- argument, and care at , where one of the two D-policy queues receives no traffic.
The queue is represented by its closed-form stationary law (12), exactly as in the paper; no continuous-time Markov chain is constructed. Speeds are arbitrary real sequences , read at ; the platooning model of §3.1.2 (a Markovian arrival process that generates the speeds) is out of scope, and Proposition 1 is stated in terms of the speeds only. "Decreasing" speeds are read as nonincreasing (AntitoneOn on ), and "increasing" in Lemma 1 as weakly increasing. Capacity is per lane. The arrival rate is real, and the limit is in . Lean's assigns at , where the throughput vanishes; Lemma 1 and (16) are therefore stated for , and the goal's is positive. At or the idle queue's junk value carries weight zero. The strict inequality (the proof writes ) keeps the threshold's denominator nonzero, and it is necessary for the equivalence. The goal is not trivialized by vacuous hypotheses: the instance , , , , satisfies all of them, with strictly inside . A statement that drops the exclusion , uses one for all , or feeds the full rate to both D-policy queues would not be this result.
A complete development needs finite sums and products, factorials, polynomial-ratio limits at infinity, and a monotonicity argument for ratios of power series truncations. The loss-queue layer (stationary law, throughput, travel time, its closed form, monotonicity and heavy-traffic limit) is reusable for any model, including the paper's integrated policy. Contributions to any milestone, and alternative proofs of Lemma 1, are welcome.
The apparel industry is a large source of carbon emissions, water use and landfill waste, and much of that footprint comes from garments being discarded early. Fast-fashion retailers such as Zara and H&M combine two operational choices: they offer a very large number of styles each season, and they replenish the styles that turn out to be popular through quick response, i.e. production during the selling season at a higher unit cost. Their garments are also widely reported to be of low quality, which shortens their useful life and reduces the chance of reuse.
X. Long and J. Nasiry, Sustainability in the Fast Fashion Industry (SSRN 3486502; Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2021.1054), give an operational explanation of low quality: it is driven by the firm's incentive to offer variety. The paper's headline (abstract, and the first sentence of its conclusion) is that when variety is chosen by the firm, quality falls as consumers become more sensitive to fashion or as introducing new styles gets cheaper. This mission formalizes that result and the chain of propositions leading to it.
A firm sells one season of a fashion product. Before the season it chooses a number of styles (design cost ), a common quality , and an inventory per style produced at unit cost . Styles are points on a circle of unit circumference (Salop's circular city). During the season, a trend uniform on the circle and a market size are realised. All consumers buy the style closest to the trend at their valuation
where is the arc distance, is a base value, and and measure the sensitivity to quality and to fashion. Demand above is met by quick response at unit cost with ; unsold units of the other styles are wasted.
The paper shows that equally spaced styles are optimal (Lemma 1), computes the expected price and the expected quick-response volume , and arrives at the firm's problem (1):
An optimal solution is a feasible triple with the largest expected profit. The parameters satisfy and ; is any real number.
For admissible parameters, problem (1) has an optimal solution, and
where each comparison changes one parameter, keeps the others fixed, and holds between every optimal solution before the change and every optimal solution after it. Monotonicity is weak: on part of the parameter space the optimal quality does not move.
In attack order:
The result separates two channels by which fashion sensitivity could affect quality. For a fixed number of styles, the optimal quality does not depend on , or at all (p. 17). All of the effect therefore runs through variety: more styles mean more leftover inventory or more reliance on expensive quick response, and the firm cuts quality to lower the unit cost. Policy conclusions in the paper rest on this mechanism. The disposal-cost and production-tax analyses of §5 ask whether a regulator can reverse the quality decline, and the environmental-impact comparison (Corollary 3) compares fast fashion with a single-style firm.
The paper proves the result with Karush–Kuhn–Tucker conditions on a non-concave reduced problem, split into four regions of and several cases in . No machine-checked proof of any of its statements exists. A formal development would certify the region analysis, which the paper itself states with thresholds that are easy to mistype. It would also supply a reusable treatment of monotone comparative statics for every selection of a non-unique optimum. Two printed slips are already corrected in the statements: the expectation "" on p. 11 should read , and the optimal-inventory display on p. 14 needs .
The reduced profit is not concave in : on its second derivative changes sign, and the optimum can jump between , an interior critical point , and the region-III value . Differentiating an optimality condition, the implicit-function argument the paper uses for , says nothing about these jumps or about ties. The goal is stated for every optimal solution, including the parameter values where two values of are optimal, so a proof needs an argument valid across jumps.
Everything is real-valued. Parameters form a record with an admissibility predicate. Problem (1) is one explicit real function, and the feasible set is , , , with the number of styles a real number as in the paper's analysis. "Optimal" means a feasible maximiser over this set. "The optimal " is read as the -component of every optimal solution; "increases/decreases" are weak; parameter changes are strict and vary one record field ({ P with γ := γ₂ }). Ties at the thresholds of Proposition 3 are handled by asserting uniqueness of only off the thresholds. The circle is AddCircle (1 : ℝ), whose metric is the arc distance and whose Haar measure is the uniform probability; the uniform market size is an interval integral divided by . Lemma 1 is stated in the reduced form its proof uses: equal spacing minimises the expected nearest-style distance. The paper's standing assumption that the base value is high enough to make quick response always worth using does not enter (1) and is not a hypothesis.
The goal is a statement about every joint maximiser of the expected profit (1) over , , . It compares parameter values that differ in one coordinate only, and it asserts that an optimum exists. For a fixed number of styles the optimal quality does not depend on , or , so a formalization about the per- optimum would be trivially true; the content lies entirely in how the optimal variety responds.
A proof needs only real analysis: one-variable optimisation of quadratics, existence of a maximiser of a continuous coercive function, and an increasing-differences (Topkis-type) monotonicity argument. A proved abstract version of the latter is on the platform, Supermodularity.Monotonicity.argmax_mono_of_strictly_increasing_differences. Lemma 1 needs integration on AddCircle and a convexity inequality over arc lengths. Contributions of alternative proofs of Proposition 3, and of reusable lemmas on comparative statics of argmax sets, are welcome.
A two-sided platform (a ride-hailing service, a marketplace, a payment network) earns money only when its two sides transact, so its value depends on the stock of participants on both sides. A young platform has to decide not only how fast to grow but also which side to grow, and it does so through the prices it sets on each side. Whether to subsidize drivers or riders, sellers or buyers, is a recurring operational decision, and the economics literature on two-sided markets (Rochet and Tirole, 2003; Armstrong, 2006) studies it mostly in static models.
Lian and van Ryzin (SSRN 3310559, later published in Management Science, 2021, doi:10.1287/mnsc.2020.3832) pose the question dynamically: supply and demand stocks grow with the surplus each side receives and decay at their own attrition rates, and the platform chooses prices over time to maximize discounted profit. Their first main result, Theorem 1, says that the optimal mix of the two sides at any moment depends only on the current size of the market, and it describes exactly how that mix moves as the market grows. This mission formalizes Theorem 1 and the lemmas its proof rests on.
A supply stock and a demand stock generate transactions per unit time, where the output function is homogeneous of degree : for . The returns to scale are decreasing if and increasing if . Buyers value a transaction at , sellers incur cost . Supply and demand decay at attrition rates and grow with adoption coefficients ; the platform discounts at rate .
When prices are unconstrained, the two stocks reduce to one market size and a balance , the share of the size held by supply. With the output is , and the size evolves by
where is the platform's per-transaction margin. The platform maximizes over balance and margin paths (problem (13)). The net welfare rate is
The paper assumes (Assumptions 1–4) that is twice differentiable and positive on , nonnegative at and , strictly concave (), that has a unique zero , the output-maximizing balance, and, when , that .
In Lean the primitives are the fields of TwoSidedGrowth.Balance.Model (with ASCII names bs0 bd0 bs1 bd1 for the four 's), the assumptions are the structure Model.Standing, and h, out, G, kappa, IsBalance, Admissible, profit are the objects above.
Write . For every market size the optimal balance is
in the sense that exactly one balance satisfies (14); it is the unique maximizer of on ; and along any size path the balance path yields at least the discounted profit of every other admissible balance path on every finite horizon. Moreover, as grows from to , moves monotonically:
The balances and are the durability-maximizing balances: all of the market on the side that attrites more slowly.
Theorem 1 separates the two controls of the growth problem: the balance is chosen myopically from the current size, and only the margin, which determines how fast the size moves, remains a dynamic decision. Every later result of the paper (the stationary size of Theorem 2, the subsidy and growth policies of §4) analyses a one-dimensional problem in because of this reduction. The table also has a direct managerial reading: a small market with decreasing returns should be balanced for output, a large one for durability, and with increasing returns the order is reversed.
The result is proved in the paper, partly in prose ("the other three cases can be checked similarly"). No machine-checked version of it is known. The formal development adds a precise reading of (14) when is unbounded at the ends (as it is for the paper's own Cobb–Douglas example, where the printed claim that is bounded by and fails), explicit monotonicity and limit statements for all four cases, and a machine-checked version of the profit identity that underlies the reduction.
The identity of Lemma 5 is an integration by parts, and the argmax of a strictly concave function is unique. The work lies elsewhere. The first obstacle is that need not be bounded on , so has to be read as an extended inverse with three regimes, and the argmax characterization must handle the boundary cases where is monotone on and its maximum sits at an endpoint where has no derivative. The second is the monotonicity: the naive argument differentiates everywhere, but is constant at or on whole intervals of sizes when is bounded at an end, and it is not differentiable where it reaches the boundary; monotonicity has to be proved for the clamped function directly, and the derivative formula (34) only on the open set of interior balances, through the inverse function theorem. The limits require continuity of the extended inverse at and the divergence of at the other end of the size range.
TwoSidedGrowth.Balance; the single definition file Setting holds the model and all derived objects.IsBalance: an interior root of , or when on , or when on . It is not defined as an argmax of , and the profit of (13) is the integral of , not the right-hand side of Lemma 5; either shortcut would make the main conjuncts definitional and is ruled out.Retailers that sell both through physical stores and online increasingly offer buy-online-pickup-at-store (BOPS): a customer reserves an item online against the store's inventory and collects it in the store. Whether this helps the retailer is not obvious. BOPS changes which customers draw on the store inventory, and therefore how much stock the store should carry and how often a visiting customer finds the item. Gao and Su (Management Science, 2017) modelled BOPS with customers who respond to store inventory availability and found that it need not be profitable for every product; Hu, Xu, Xue and Yang (Management Science 68(2), 2022; accepted manuscript SSRN 3214047) ask when it helps, through the inventory side. They identify two opposing effects: demand pooling, where BOPS moves online demand onto the store inventory, and demand depooling, where BOPS splits off customers who used to buy in the store. This mission formalizes their first effect, Proposition 3: in a stated region of costs, BOPS benefits the retailer.
A retailer owns one brick-and-mortar store and an online channel fulfilled from a distribution centre. On a probability space there are two customer segments with random market sizes: store-only customers, who buy only in the store, and omni-customers, who may buy in the store or online. The store sells at price with unit cost ; the online channel sells at with unit cost . A store visit costs a customer , waiting for an online delivery costs . The base surpluses are online and in the store, and Assumption (U) holds throughout.
The retailer chooses a store order quantity before demand is realized. A customer who visits the store finds the item with probability equal to the store's fill rate , where is the demand facing the store (Deneckere and Peck). Customers decide on the basis of a belief about the fill rate; the retailer orders on the basis of beliefs about the fractions of each segment that shop in the store.
A rational-expectations (RE) equilibrium is a profile in which customers' choices are optimal for the believed fill rate, the order quantity is optimal for the believed choices, and both beliefs are correct. When several exist, the paper selects the Pareto-dominant one. The optimal order quantities , (BASE, with only store-only customers, respectively both segments, in the store) and (BOPS, store-only customers in the store) define fill rates .
If
then Pareto-dominant RE equilibria exist under BASE and under BOPS, and at any such pair the retailer's expected profits satisfy
Proposition 3 is one half of the paper's comparison of BOPS with independent channels (Figure 3 of the paper): together with the depooling effect (Proposition 4) it partitions the cost region below the diagonal into areas where BOPS helps, hurts, or is neutral. It isolates a mechanism that does not appear in models with exogenous store demand: the fill rate, and hence customers' channel choices, respond to the inventory decision.
The paper's proof is short once the equilibria are characterized, but it is a proof in the paper's normal-demand model, where the statement does not hold (see below). The mission produces a corrected, machine-checked version: an explicit equilibrium model with rational expectations and Pareto selection, the characterization of the equilibria that the comparison needs, and the comparison itself. None of these results has a machine-checked proof.
The comparison of profits is easy once one knows which equilibrium each strategy selects; the work lies in the equilibrium analysis. Equilibria are fixed points of a map that couples a newsvendor problem with a discrete choice through the fill rate, and the fill rate is a ratio of expectations of the optimizer. Showing that a candidate profile is consistent, that the remaining profiles are not, and that the selected one Pareto-dominates every other, requires comparing optimal values of different newsvendor objectives and monotonicity of optimizers between them (Lemma 2), without closed forms. The obvious shortcut, reading off the equilibria from the paper's case tables, is not available: the tables are the theorems to be proved.
All objects live in the namespace OmniPool.BOPS; a single definitions file encodes the profits (2) and (4) term by term, the fill rates, the choice rules in utility form, and the RE equilibria of Definitions A1 and A2 as fixed points.
The goal asserts existence of Pareto-dominant equilibria under both strategies; without these conjuncts the universally quantified comparison could hold vacuously. Defining by the paper's region tables instead of through equilibria would make the goal a tautology and is ruled out.
Infrastructure needed: integrability of truncated demands, monotone comparative statics for maximizers of functions with increasing differences, and pointwise identities between the profit expressions. The equilibrium definitions are reusable for the paper's other results (Propositions 4 and 5) and for RE models of omnichannel retail. Proofs of the milestones, and formalizations of Propositions 1(i) and 2(ii)–(iii), are welcome.
Mean-variance analysis, the trade-off between the expected value and the variance of a portfolio's outcome, is the most widely used criterion for portfolio choice in practice. In continuous time it has two well-known defects when applied to terminal wealth: the criterion is time-inconsistent (a strategy that is optimal today is no longer optimal tomorrow), and the resulting equilibrium strategies of Basak and Chabakauri (2010) and Björk, Murgoci and Zhou (2014) prescribe a dollar amount in the stock that does not scale with wealth, which is at odds with how investors and advisers think in terms of portfolio fractions.
Dai, Jin, Kou and Xu apply the mean-variance criterion to the log-return of the portfolio instead of to wealth. They show that, in the classical complete market with constant coefficients, the resulting equilibrium strategy is a constant fraction of wealth, that it coincides with the classical optimal strategy of Merton (1969) for a CRRA investor with relative risk aversion , and that the investor's preference parameter is in one-to-one correspondence with a target annual return. The last fact is what the paper uses to elicit from an investor's stated target return.
A bond pays the constant interest rate . One stock has price with constant drift , volatility , and a standard Brownian motion on a probability space. An investor with horizon holds the fraction of wealth in the stock. A feedback strategy is a function of time and current log-wealth . The log-wealth then solves the stochastic differential equation (6)
For a time and a log-wealth , the investor evaluates a strategy through the reward function
the mean minus times the variance of terminal log-wealth for the process started at . Here is a constant (Assumption A). A strategy is admissible if .
Because is time-inconsistent, optimality is replaced by an equilibrium, following Björk, Khapko and Murgoci (2017). For and , the perturbation holds the constant fraction on and follows afterwards. An admissible is an equilibrium strategy (Definition 1) if, at every , every and every ,
With the market price of risk, the mission's two named quantities are
In Lean these are piHat M and aHat M for a market M : Market with fields μ r σ γ T; the SDE is IsLogReturn, admissibility Admissible, the reward J, the perturbation spike and Definition 1 IsEquilibrium.
A supporting item (not a milestone) states the reward of an admissible deterministic policy, (p. O–10); another states that and all its perturbations are admissible.
Part (i) shows that the dynamic mean-variance criterion on log-returns and CRRA expected utility of terminal wealth share the same optimal strategy in a complete market, although the first is time-inconsistent and the second is not. Part (ii) gives a closed-form, strictly increasing link between the target annual return and , which is the basis of the paper's procedure for eliciting the risk parameter (Corollary 1) and of its comparisons with terminal-wealth mean-variance strategies.
The result is proved on paper; nothing in it has a machine-checked proof. Formalizing it requires a working account of the Itô integral of deterministic integrands against Brownian motion (Gaussianity of the integral, its mean and variance, and uniqueness of solutions of an SDE with deterministic coefficients) in the form of the published step-sum relation EthierKurtz.HasBrownianItoIntegral. That account is reusable by any mission that computes moments of linear SDEs.
The paper's proof is three displays long because it takes the moment formulas for granted. Mathlib has Brownian motion (IsBrownianReal) but no Itô integral, no Itô isometry and no existence theory for SDEs, so each of the following is real work:
The equilibrium inequality itself is pointwise algebra once the reward is known.
EthierKurtz.HasBrownianItoIntegral, in elapsed time from , with the integrand set to after the horizon.Classical.epsilon); under admissibility the choice is immaterial.Market.Standing. The coordinates of are assumed measurable.Trivializing encodings are ruled out: is defined from the SDE and never by the closed form of Appendix C.2, and the goal's conclusion (not its hypotheses) asserts admissibility of and of every perturbation, so the equilibrium claim cannot hold vacuously. The moment milestone concludes , because Lean's integral and variance are on non-integrable inputs.
Welcome contributions: the Gaussian law of for deterministic under the step-sum relation; existence and uniqueness for (6) with deterministic coefficients; and the algebraic milestones, which are independent of the stochastic layer.
Two-stage stochastic linear optimization is the standard model for decisions taken before uncertainty is revealed and corrected after it: capacity before demand, inventory before transport capacities, generation commitments before load. In practice the probability distribution of the uncertainty is unknown and only historical samples are available, so the stochastic problem has to be replaced by a data-driven one. The sample average approximation (SAA) is consistent but can overfit badly on small samples; distributionally robust formulations hedge against this, but for two-stage problems they are typically intractable.
Bertsimas, Shtern and Sturt (arXiv:1907.07142v4, published as a Technical Note in Operations Research, 2022) study sample robust optimization (SRO): each sample is perturbed adversarially within a small ball intersected with a known support polyhedron. SRO is equivalent to two-stage distributionally robust optimization over a type-∞ Wasserstein ball (Bertsimas, Shtern, Sturt 2018, Proposition 3, as cited on p. 7), and evaluating its objective is NP-hard even for one sample. The paper proposes a tractable multi-policy approximation (MP), with one linear decision rule per sample, and proves that it recovers the optimal value and the optimal decisions of the underlying stochastic problem as the data grow, without assuming relatively complete recourse.
The data are , , , and an affine right-hand side . The second-stage cost of a first-stage decision under the realization is
equal to when no recourse is feasible. With a random vector of law , the stochastic problem is
The support of lies in a known polyhedron . Given i.i.d. samples , a radius and an -norm, the uncertainty sets are and
A linear decision rule is a policy ; the set of them is . The multi-policy approximation chooses, besides , one rule per sample, feasible on its own set:
The single-policy approximation (SP) uses one shared rule for all .
Assume [A1] ; [A2] is finite and ; [A3] the optimal set of (OPT) is nonempty and bounded; [A4] there are and such that around every some linear decision rule is feasible on . Then
and almost surely every accumulation point of optimal first-stage decisions of (SRO) or (MP) is optimal for (OPT).
Theorem 2 says that a linear or second-order cone program with variables and constraints (Proposition 1) is a consistent estimator of the optimal value and decisions of a two-stage stochastic linear program, under assumptions comparable to those for SAA, for unbounded and without relatively complete recourse. Theorem 1 adds that (MP) is always a valid upper approximation of (SRO), so the same limit holds for the intractable SRO problem.
The result is proved in the paper; nothing here is open. No part of it has been machine-checked. A complete development would give a verified model of two-stage linear programs with extended-valued recourse, a verified sample-robust and multi-policy layer, and the polyhedral lemmas on balls intersected with polyhedra (Lemmas 5, 9 and display (3)), which are reusable for other robust and distributionally robust convergence results. The two cited consistency statements (milestones 1 and 7) would be the first formal consistency results for SAA with extended-valued convex integrands.
The upper bound cannot be obtained by plugging an optimal into (MP): need not admit any linear decision rule feasible on a neighbourhood of a sample, and without relatively complete recourse a sample near the boundary of the feasible region may admit none at all. The proof perturbs towards the point given by [A4], which requires the uniform radius of display (3), obtained from an induction over the faces of in Appendix C. Lemma 1's direction [A4] [A6] is a second induction over face dimension (Appendix B).
The lower bound reduces to SAA, but the SAA consistency it needs is for an extended-valued, merely lower semicontinuous convex integrand (King and Wets 1991), for which Mathlib has no epi-convergence theory and no law of large numbers for random lower semicontinuous functions. A uniform law of large numbers on a compact set does not apply: the feasible region need not be bounded and is off a polyhedron.
Vectors are Fin k → ℝ; the -norm is that of PiLp p for an arbitrary p : ℝ≥0∞ with 1 ≤ p, the dual norm is , and the same p is used on in Lemma 3. Every optimal value (, , , the SAA, SRO, SP and MP values, , , ) is an infimum or supremum in EReal: "min" and "max" are read as inf and sup, attainment is never assumed, infeasibility gives , and the factor is the real . The expectation is the platform definition DupacovaWets.Consistency.expect ( when , else ), which agrees with the usual expectation whenever is finite. Samples are ξ 0, ξ 1, …, independent with law and ; the paper's are the first . The radii are deterministic. (MP) is stated as printed with policies. Faces of are nonempty sets , and the relative interior is intrinsicInterior.
Trivializing encodings are ruled out: is not real-valued with a junk value for infeasibility, the expectation is not a Bochner integral of a real truncation, optimal values are not real sInfs, [A4] is the printed local condition and not the global single-rule condition of Proposition 2, and the accumulation-point clauses quantify over sequences that are optimal for all large (requiring optimality at would make them vacuous).
Disclosed readings: the accumulation-point clauses of Theorem 2 hold on one almost-sure event for every eventually-optimal sequence; Lemmas 2 and 3 and display (3) carry §4.2's standing [A2]–[A3], the support condition, and optimality of ; Lemmas 5 and 9 assume the appendix's normalization but not minimality of the representation; display (3)'s set-builder, which omits its bound variable, is read as in Theorem 3; Lemma 2 is stated as printed with , although its proof derives the equivalent form with and swapped.
Contributions welcome: proofs of any milestone, in particular LP strong duality in this inequality form for Lemma 3, the polyhedral Lemmas 5 and 9, and the SAA consistency results, which are reusable beyond this mission.
In the first weeks of the COVID-19 pandemic, diagnostic testing capacity in many countries was a small fraction of the population, and policy discussion centred on waiting for more accurate tests before deploying them widely. Drakopoulos and Randhawa (SSRN 3565245; Management Science, 2021, doi:10.1287/mnsc.2021.4029) treat a test as an information product: an agent's decision to request a test depends on how much the test's result could change that agent's own action. When tests are rationed among those who ask, the accuracy of a test therefore determines not only what is learned from each test but also who asks for one. The paper shows that, under scarcity and uniformly random rationing, a planner can strictly prefer a slightly imperfect test to a perfect one. The result speaks to operations managers and public-health planners who allocate scarce diagnostic capacity, and to the literature on pricing and allocating information goods.
A unit mass of agents has private priors of being infected, distributed with density on and distribution function ; write . An agent who acts (seeks treatment, self-isolates) earns , where is a normalized cost; an untested agent acts iff , with expected utility .
A -test has false positive rate and true positive rate , with ; the -test is the perfect test. The value of the test to an agent is , where is the expected utility of acting optimally after observing the result. Two critical values
split the agents into low-likelihood (, never act), medium-likelihood (, follow the test) and high-likelihood (, always act). Only medium-likelihood agents request a test, so the demand is .
A mass of kits is scarce and is allocated uniformly at random among requesting agents, so each requester is tested with probability . The planner gains for every infected agent who acts and loses for every uninfected one; its objective is the expected net gain over the population (display (9) of the paper with ). Finally
Assume a perfect test is available, , and . Then , and
In the order of the paper's argument:
The result. Proposition 2 gives explicit sufficient conditions, in terms of the density of priors at the extremes, under which accuracy and social value come apart: when many agents have priors near (respectively near ), lowering the specificity (respectively the sensitivity) of the test discourages those agents from requesting it and frees kits for agents whose actions depend on the result. It is the paper's main formal argument against waiting for a perfect test under scarcity, and it isolates the mechanism — demand that responds to test quality — that the paper's later examples and observations build on.
Formalizing it. The result is proved in the paper; it has no machine-checked proof. A formalization fixes the model unambiguously (who requests, how kits are rationed, what the planner counts) and checks the proof's calculus, including one-sided derivatives at the boundary of the set of tests and a derivative of a parametric integral whose limits and integrand both move. Formalizing the proof also checks the printed derivative , whose middle term is printed as although the condition the paper derives from it, and the corrected computation, give ; milestone 12 states the corrected value.
The planner's objective is defined agent by agent from behaviour, so the first obstacle is to show that the set of requesting agents is exactly the interval (Lemma 1) and to turn into the three-integral closed form; only then is a function of through , and . The second is the derivative at the perfect test. At the thresholds sit at the endpoints and of the prior's support, so the derivatives exist only from one side, the integrand is evaluated at an endpoint where a density is not determined pointwise, and the availability moves with the thresholds. The naive argument "a more accurate test always helps" holds when tests are plentiful (Proposition 1 of the paper, where ); under scarcity the congestion term is what can reverse the sign, and it has to be tracked exactly.
All objects live in the namespace ScarceTesting.PerfectTest, in one definitions file Setting. Conventions:
f with IsPriorDensity f: nonnegative on , interval-integrable on , total mass ; cdf f x is . Values , are read with ContinuousWithinAt f (Icc 0 1) at the endpoint, a disclosed reading of "density with value ".if D ≤ κ then 1 else κ / D, so that zero demand gives .S integrates each agent's expected contribution against ; it is not defined by the paper's simplified formula, which is a milestone.A complete development needs Lebesgue and interval integrals with variable limits, the fundamental theorem of calculus at an endpoint of continuity, and one-sided derivatives of parametric integrals. The Bayesian value-of-a-test layer (Lemma 1, display (6)) is reusable for other models of testing and information products. Proofs of any milestone are welcome independently.