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?
text of abstract (We present a utilitarian review of the family of matrix groups , in a form suited to various applications both in optics and quantum mechanics. We contrast these groups and their geometry with the much more familiar Euclidean and unitary geometries. Both the properties of finite group elements and of the Lie algebra are studied, and special attention is paid to the so-called unitary metaplectic representation of . Global decomposition theorems, interesting subgroups and their generators are described. Turning to -mode quantum systems, we define and study their variance matrices in general states, the implications of the Heisenberg uncertainty principles, and develop a U(n)-invariant squeezing criterion. The particular properties of Wigner distributions and Gaussian pure state wavefunctions under action are delineated.)
This mission is the statement-level formalization of The Real Symplectic Groups in Quantum Mechanics and Optics (arXiv:quant-ph/9509002v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §IV (4.20): Euler decomposition (seed paper result) (§IV (4.20): Euler decomposition (seed paper result), PDF p. 16). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We introduce a Gaussian version of the entanglement of formation adapted to bipartite Gaussian states by considering decompositions into pure Gaussian states only. We show that this quantity is an entanglement monotone under Gaussian operations and provide a simplified computation for states of arbitrary many modes. For the case of one mode per site the remaining variational problem can be solved analytically. If the considered state is in addition symmetric with respect to interchanging the two modes, we prove additivity of the considered entanglement measure. Moreover, in this case and considering only a single copy, our entanglement measure coincides with the true entanglement of formation.
This mission is the statement-level formalization of Gaussian Entanglement of Formation (arXiv:quant-ph/0306177v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Parametrization of pure Gaussian covariance matrices (Lemma 1, Eq.(16), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
13 results of the paper are not stated yet, because the library lacks an interface they need:
The applications of the general formulae of channel capacity developed in the quantum information theory to evaluation of information transmission capacity of optical channel are interesting subjects. In this review paper, we will point out that the formulation based on only classical-quantum channel mapping model may be inadequate when one takes into account a power constraint for noisy channel. To define the power constraint well, we should explicitly consider how quantum states are conveyed through a transmission channel. Basing on such consideration, we calculate a capacity formula for an attenuated noisy optical channel with genreral Gaussian state input; this gives certain progress beyond the example in our former paper.
This mission is the statement-level formalization of Information capacity formula of quantum optical channels (arXiv:quant-ph/0105042v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lossless number-state entropy maximum and capacity (Eqs.(58)-(59), PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
9 results of the paper are not stated yet, because the library lacks an interface they need:
We give two integrability criteria for representations of Banach--Lie algebras as skew-symmetric unbounded operators on a dense domain of a Hilbert space.
This mission is the statement-level formalization of Integrating representations of Banach--Lie algebras (arXiv:1003.0999v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Product rule for a strongly continuous operator path (Lemma 4, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
We extend the mathematical theory of quantum hypothesis testing to the general -algebraic setting and explore its relation with recent developments in non-equilibrium quantum statistical mechanics. In particular, we relate the large deviation principle for the full counting statistics of entropy flow to quantum hypothesis testing of the arrow of time.
This mission is the statement-level formalization of Quantum Hypothesis Testing and Non-Equilibrium Statistical Mechanics (arXiv:1109.3804v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 1.1 (Proposition 1.1, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
40 results of the paper are not stated yet, because the library lacks an interface they need:
In most communication schemes information is transmitted via travelling modes of electromagnetic radiation. These modes are unavoidably subject to environmental noise along any physical transmission medium and the quality of the communication channel strongly depends on the minimum noise achievable at the output. For classical signals such noise can be rigorously quantified in terms of the associated Shannon entropy and it is subject to a fundamental lower bound called entropy power inequality. Electromagnetic fields are however quantum mechanical systems and then, especially in low intensity signals, the quantum nature of the information carrier cannot be neglected and many important results derived within classical information theory require non-trivial extensions to the quantum regime. Here we prove one possible generalization of the Entropy Power Inequality to quantum bosonic systems. The impact of this inequality in quantum information theory is potentially large and some relevant implications are considered in this work.
This mission is the statement-level formalization of A generalization of the Entropy Power Inequality to Bosonic Quantum Systems (arXiv:1402.0404v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Three scalar thermal-entropy asymptotics (§IV.B Eq. (86); §VI.B Eqs. (103), (104), PDF p. 17). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
We show that the cross Wigner function can be written in the form where is the Fourier transform of and is a metaplectic operator that projects onto a linear symplectomorphism consisting of a rotation along an ellipse in phase space (or in the time-frequency space). This formulation can be extended to generic Weyl symbols and yields an interesting fractional generalization of the Weyl-Wigner formalism. It also provides a suitable approach to study the Bopp phase space representation of quantum mechanics, familiar from deformation quantization. Using the "metaplectic formulation" of the Wigner transform we construct a complete set of intertwiners relating the Weyl and the Bopp pseudo-differential operators. This is an important result that allows us to prove the spectral and dynamical equivalence of the Schr"odinger and the Bopp representations of quantum mechanics.
This mission is the statement-level formalization of Metaplectic formulation of the Wigner transform and applications (arXiv:1401.3388v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Periodicity, two elliptic invariants, and coordinate-pair rotations (Remark 5: periodicity and elliptic invariants, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
23 results of the paper are not stated yet, because the library lacks an interface they need:
We consider a quantum generalization of the classical heat equation, and study contractivity properties of its associated semigroup. We prove a Nash inequality and a logarithmic Sobolev inequality. The former leads to an ultracontractivity result. This in turn implies that the largest eigenvalue and the purity of a state with positive Wigner function, evolving under the action of the semigroup, decrease at least inverse polynomially in time, while its entropy increases at least logarithmically in time.
This mission is the statement-level formalization of Contractivity properties of a quantum diffusion semigroup (arXiv:1607.04242v6). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Order comparison of second derivatives at a common zero minimum (Lemma 3 (Appendix C), PDF p. 29). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
13 results of the paper are not stated yet, because the library lacks an interface they need:
We consider energy-constrained infinite-dimensional quantum channels from a given system (satisfying a certain condition) to any other systems. We show that dealing with basic capacities of these channels we may assume (accepting arbitrarily small error ) that all channels have the same finite-dimensional input space -- the subspace corresponding to the minimal eigenvalues of the input Hamiltonian. We also show that for the class of energy-limited channels (mapping energy-bounded states to energy-bounded states) the above result is valid with substantially smaller dimension . The uniform finite-dimensional approximation allows to prove the uniform continuity of the basic capacities on the set of all quantum channels with respect to the strong (pointwise) convergence topology. For all the capacities we obtain continuity bounds depending only on the input energy bound and the energy-constrained-diamond-norm distance between quantum channels (generating the strong convergence on the set of quantum channels).
This mission is the statement-level formalization of Uniform finite-dimensional approximation of basic capacities of energy-constrained channels (arXiv:1707.05641v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Monotonicity of the perspective of a nonnegative concave function (Lemma 1, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
Unitary equivariance is a natural symmetry that occurs in many contexts in physics and mathematics. Optimization problems with such symmetry can often be formulated as semidefinite programs for a -dimensional matrix variable that commutes with , for all . Solving such problems naively can be prohibitively expensive even if is small but the local dimension is large. We show that, under additional symmetry assumptions, this problem reduces to a linear program that can be solved in time that does not scale in , and we provide a general framework to execute this reduction under different types of symmetries. The key ingredient of our method is a compact parametrization of the solution space by linear combinations of walled Brauer algebra diagrams. This parametrization requires the idempotents of a Gelfand-Tsetlin basis, which we obtain by adapting a general method arXiv:1606.08900 inspired by the Okounkov-Vershik approach. To illustrate potential applications, we use several examples from quantum information: deciding the principal eigenvalue of a quantum state, quantum majority vote, asymmetric cloning and transformation of a black-box unitary. We also outline a possible route for extending our method to general unitary-equivariant semidefinite programs.
This mission is the statement-level formalization of Linear programming with unitary-equivariant constraints (arXiv:2207.05713v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.2: equivariance characterized by the Choi commutator (Proposition 2.2: equivariance characterized by the Choi commutator, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
15 results of the paper are not stated yet, because the library lacks an interface they need:
A nonprofit choosing how to serve people with different needs may have two ways to use an additional dollar: offer more product variants, or deliver a larger fraction of each product. Beneficiaries can sometimes finish an incomplete product themselves, but doing so takes effort. Zhang, Atasu and Ramachandran study this choice for services such as incremental housing and temporary shelter. The question is how a limited budget changes the optimal combination of variety and completion.
The paper’s main text first models the beneficiaries’ needs and the nonprofit’s costs, then derives the allocation pattern in Lemmas 1–2 and Proposition 3. This mission targets those results in the authors’ SSRN version. The optimization is over a continuous variety level, as the paper explicitly assumes in §4.2; the integer case has a different comparative static for completion at footnote 5 on p. 13.
A variety level describes how many equally spaced variants the nonprofit offers to a unit mass of beneficiaries with uniformly distributed ideal locations. The analysis treats as a real decision variable. A completion level is the fraction of each variant the nonprofit provides. Heterogeneity reduces the utility of a complete variant with distance from a beneficiary’s ideal. Aggregating the closest variant’s utility gives §3, pp. 7–8.
Each beneficiary may complete at most of the product. With quadratic effort cost , where , optimal self-completion effort is . The nonprofit’s expenditure is , where , , and for . Its total net benefit is
At a budget , a decision is feasible when , , and . An optimal decision is a feasible decision whose value of is at least that of every other feasible decision. Without the budget constraint, the same domain , defines the unconstrained problem §3, p. 10 and §4.2, pp. 12–13.
The standing assumption that provision is worthwhile says some satisfies . Let be the unconstrained optimal variety: it is when ; otherwise it is the solution above of . Write and . These are the unconstrained completion level and the budget needed to afford that pair Lemma 1, p. 12.
Lemma 1 asserts that maximizes without a budget constraint. Lemma 2 says every optimal decision exhausts its budget below :
Proposition 3 is the goal. It asserts thresholds , a small-budget variety , and middle-regime decisions such that an optimal pair can be selected as
Both and are nondecreasing on the middle interval, using the paper’s weak meaning of “increasing.” The goal characterizes using the appendix’s function : if , and otherwise is its zero. It also requires . These conditions retain the paper’s small-budget regime and prevent an arbitrary threshold from making it empty Proposition 3, p. 13; proof, Online Appendix p. 2.
The three regimes identify when a nonprofit should spend an increment of budget solely on completion, when variety and completion should rise together, and when additional budget no longer changes its choice. Lemma 1 also says that, even with ample funds, completing the entire product need not be optimal because beneficiaries can add value through their own effort §4.2, pp. 12–14.
The paper proves these claims analytically. This mission asks for machine-checked proofs of the continuous model’s optimization statements, including the attainment and feasibility of each claimed optimum. The reusable part is a compact interface for a two-variable budget-constrained optimization problem with a beneficiary best response. There is no existing machine-checked proof of these particular claims in the platform catalog at drafting time.
The binding-budget curve crosses the point , where beneficiary effort changes formula. Thus optimizing a single smooth expression over all variety levels does not cover the problem. A stationary point calculated in one region also must be checked against feasible points in the other. The argument needs to establish global optimality and preserve the bounds as the budget changes Online Appendix pp. 2–3.
The appendix’s candidate threshold in one case can exceed when the unconstrained variety is . Proposition 3 itself asks only for a threshold , so the formal goal retains that existential form. The proof’s candidate must be capped at in that case; the middle interval can then be empty. This discrepancy is recorded for solvers, who should establish the proposition as stated rather than assume the appendix’s candidate always satisfies the bound Online Appendix p. 3.
All quantities are real. The Lean model stores , , and as separate functions and requires the two derivative identities, positive and nonnegative for . It uses the closed formula for and the minimum formula for effort. The hypotheses , , and make explicit the economic parameter and budget domains; is needed for the stated variety characterization, and is implicit in the paper’s increasing quadratic effort cost. The paper’s , , and worthwhile-provision assumption are retained.
Optimality always includes membership in the feasible set. This rules out an out-of-domain maximizer. The upper regime asserts that the displayed pair is an optimum, allowing other optima when . Division by and is used only at varieties ; the standing assumptions imply there. The goal fixes by the paper’s formula and pins down , so it cannot be discharged by choosing arbitrary empty budget ranges. Proofs of the two appendix monotonicity claims, the binding-budget lemma, and the global small-budget optimum are welcome along with the goal.
Electric vehicle adoption depends on both the number of drivers willing to buy a vehicle and the availability of places to charge it. These decisions reinforce one another: an additional charging pile reduces expected search cost, while an additional vehicle increases demand for charging. A city may subsidize the vehicle purchase, each charging session, or the construction of a pile. The instruments can have different effects even when the public spending they require is equal. Zhang and Dou study these tradeoffs in a two location market with different pile costs and charging inconvenience. Their 2021 paper gives conditions under which one subsidy has a greater marginal effect on gross social surplus than another.
The target here is the paper's Theorem 3. It addresses a local comparison of policy instruments at a given policy mix. It does not claim that a policy satisfying a condition is globally optimal or that the same ranking holds after a large change in subsidy.
There are two locations, A and B. A fraction of potential drivers resides at A and the remainder at B. Driver type measures the annual benefit of using an electric vehicle. In the base model it has distribution for , with . A vehicle costs per year, and each driver needs one charging session every years. A session occupies a pile for time .
At location , a session has regulated fee , waiting cost , and expected search cost when expected pile utilization is . Drivers at A charge at A. Drivers at B choose between the locations using the paper's logit probabilities and ; their expected cost is a log sum of the two location costs. The purchase threshold is , where is the vehicle purchase subsidy. These thresholds, the purchase probabilities , and the choice probabilities determine the arrival rates and .
Charging service providers choose piles per provider to maximize annual profit, taking expected utilization as fixed. The number of providers is ; a pile at costs annually. A policy pays per pile and per session, in addition to per vehicle purchase. A rational expectations equilibrium matches each expected utilization with the actual ratio , while the provider's pile choices maximize profit. The mission uses the positive pile regime of the paper's equilibrium analysis. In it, Theorem 1 determines .
Gross social surplus, denoted , has three components in equation (8): the external benefit , the integral of driver surplus above each purchase threshold, and provider surplus. The total subsidy value and the government's objective are represented separately. The goal compares derivatives of per equal increment in subsidy value, following the normalization in the proof of Theorem 3.
Theorem 1 asserts existence and uniqueness of the positive pile equilibrium. The proof of Theorem 3 also states that provider break even makes its gross social surplus equal to
This is a theorem about the surplus defined by equation (8), not its definition. The milestone list also records the purchase subsidy derivative and bounds on the usage and pile subsidy derivatives given in the paper's technical proof.
The goal is Theorem 3. Write . For a pile subsidy mix , a sufficient condition for the purchase subsidy to yield at least as much additional gross social surplus as the paper's pile subsidy direction at equal marginal spending, when the pair is balanced and the subsidies are nonnegative, is
For a nonnegative usage subsidy mix , a sufficient condition for usage subsidy to yield at least as much is
Here is the efficiency of the vehicle purchase subsidy relative to subsidies paid to providers. The inequalities are local sufficient conditions; they make no claim about large policy changes.
The two conditions connect the subsidy ranking to pile cost, search cost, charging time, and subsidy efficiency. They identify parameter regimes in which a city can increase gross social surplus more through charging side support, or more through vehicle purchase support, at equal marginal subsidy value. This gives a precise comparison within the paper's model, complementing its separate results on spatial mismatch and policy optima. The source result and its proof are published in the authors' version; this mission asks for a machine checked formalization of that known result.
A complete development would also supply reusable results on the exponential tail integral, derivatives of logit choice probabilities, and the relationship between a profit maximizing provider choice and equilibrium utilization. Those statements are useful for other two sided adoption and infrastructure models that combine provider investment with consumer choice.
Changing a subsidy changes more than the direct transfer. It changes utilization, search costs, the logit split of B's charging sessions, vehicle purchase thresholds, and both arrival rates. A comparison that looks only at the direct increase in purchases misses the displacement of charging activity between A and B. The pile subsidy comparison is especially sensitive to the direction in which the two pile subsidies change: equal changes in and do not have equal marginal effects or equal costs. The equilibrium quantities must also be connected to the derivatives of the actual surplus expression rather than to an assumed closed form.
The Lean model uses real valued parameters, policies, utilizations, arrival rates, and pile counts, with two explicit locations. It fixes , as the base model does. The standing assumptions are , , , , , , and . It also requires : the externality is described as a benefit, and the derivative comparisons use its nonnegative contribution. The interior regime is and at both locations. Positive purchase thresholds are required at derivative evaluation points because the exponential distribution has a boundary at zero.
Equation (10) is expressed by , with utilization constrained below one. This excludes a division by zero that would otherwise create a false zero pile equilibrium in Lean. The distribution function is zero below zero. The subsidy value is , read from the proof's displayed derivatives on p. S10 and its treatment of pile subsidies on p. S9. The goal quantifies over every equilibrium selection on the interior regime and asserts such a selection exists. Its marginal comparisons use and the pile subsidy direction . A pile subsidy pair is balanced if no feasible nonnegative pair with the same equilibrium subsidy value yields higher gross social surplus. The goal requires this condition for the pile subsidy comparison and requires nonnegative subsidies at each policy mix.
The formalization must retain equation (8)'s driver surplus integral and provider surplus. Defining by the break even closed form would make the goal circular. Contributions on the source's integral, equilibrium existence, derivative bounds, and the connection to the selected equilibrium are within scope.
Manufacturers of durable products — airlines' aircraft, consumer electronics, cars — increasingly hand the after-sales product service (help desks, repair, field maintenance) to a third-party provider. The provider is often more cost-efficient, and the brand can concentrate on its core product. The price of outsourcing is visibility: once the service is run by someone else, the brand no longer observes the service environment that drives the cost of serving customers, and it pays the provider on the basis of a belief that drifts away from reality as unobserved shocks accumulate.
Y. Wang, M. Li, N. Ma and H. Zhang (MSOM 2024, doi:10.1287/msom.2022.0222) model this trade-off with a martingale model of forecast evolution (MMFE, in the sense of Heath and Jackson 1994): the environment evolves by multiplicative mean-one lognormal shocks, and after outsourcing the brand stops seeing them. Their Proposition 4 shows that this loss of visibility alone — with no switching cost, a cheaper provider and a product-value gain — can make outsourcing unprofitable. The question belongs to the operations literature on service outsourcing under information asymmetry (e.g. Hasija, Pinker and Shumsky 2008; Feng, Ren and Zhang 2019).
A single service period is described by the following data.
Partial observability. The brand holds a belief about the environment. The true environment is , where the unobserved shock is lognormal with mean and variance parameter (the variance of ). Equivalently, with .
Payment. Without reporting, learning or monitoring, the brand pays ; when the true environment exceeds the belief, the provider's participation constraint forces the payment up to . With full observability the payment would be always.
Value of outsourcing. , and is the same expectation with the full-observability payment. The error function is .
For all parameters satisfying the standing assumptions:
with a pointwise nonnegative loss term (part (a): only an upward drift of the belief matters);
(part (b)); and (part (c)) there exist admissible parameters with , and some such that .
The result. Proposition 4 separates two effects that are usually conflated in the outsourcing literature: environment uncertainty, which makes outsourcing more attractive (the provider absorbs a growing cost), and partial observability, which erodes its value. It shows that the second can dominate on its own: the value lost when the belief overshoots the true environment grows with the accumulated variance, and with a long enough relationship it wipes out both the provider's cost advantage and the product-value gain. This underpins the paper's later analysis of learning and monitoring (§5.1–§5.2), which are evaluated by how much of this loss they recover.
Formalizing it. The result is proved in the paper; nothing in it is machine-checked. The mission produces a checked version of the benchmark analysis with every hidden convention made explicit: the representation of the lognormal shock, the payment rule at the boundary, and the per-period reading of . Along the way it produces reusable facts about mean-one lognormals — the mean identity, the closed form of their lower tail and of their truncated first moment in terms of erf, and the monotonicity of the tail in the volatility — which recur wherever MMFE-type forecast evolution is used.
The model-level algebra is short; the work is in the probability. The parts of the argument that are not routine are:
The obvious shortcut — replacing by an erf formula and proving monotonicity of erf — is exactly what the mission excludes: the closed form of is not stated in the paper and must be derived from the model.
All objects live in the namespace PSOutsourcing.PartialObs in one definitions file. Conventions committed to:
gaussianReal 0 1; the shock is xi s z = exp(s z − s²/2) and the true environment is xi s z * db.Real.log 0 = 0 cannot express the paper's ); Lemma 3(c) adds , which its proof uses; derivatives are stated with HasDerivAt.A formalization in which is defined by its closed form, or in which the payment ignores the participation constraint, trivializes the goal and is ruled out: is the expectation of the period-profit difference under the stated payment rule.
Infrastructure needed: erf and its relation to the standard normal distribution function, the Gaussian moment generating function (Mathlib's mgf_gaussianReal), truncated lognormal moments, and differentiation of Gaussian tail probabilities in a parameter. These lemmas are reusable well beyond this mission, and contributions of them as standalone theorems are welcome.
How far apart are two preferences? Distance functions on preference relations are used to deduce a consensus ranking from a collection of individual preferences. The classical answer is the Kemeny–Snell metric (Kemeny and Snell 1962), proposed axiomatically for linear orders and extended by Bogart (1973) to partial orders. It counts rank reversals between two orders and weighs all of them equally: swapping the two best alternatives costs as much as swapping the two worst.
For a decision maker who chooses from menus, these swaps are not equivalent. A disagreement at the top of the ranking changes what is chosen from many menus; one at the bottom changes almost nothing. Weighted Kendall-type metrics on linear orders (Can 2014; Hassanzadeh and Milenkovic 2014) were proposed for this reason, but they live only on linear orders. Nishimura and Ok (2022) instead compare two preferences by the sets of maximal elements they select in every menu. Their domain is the set of acyclic orders, which contains linear orders, partial orders, preorders and the non-transitive acyclic relations that arise as revealed preferences. Their main result, Theorem 3.1, is an axiomatic characterization of this family of semimetrics.
Let be a nonempty finite set of alternatives. For a binary relation on , the asymmetric part is defined by iff and not , and the symmetric part is . is an acyclic order if it is reflexive and there is no cycle of pairwise distinct elements. The set of all acyclic orders is . A generic acyclic order is written , with strict part and symmetric part ; a second one is , with strict part . For , the set of maximal elements is
For a positive (possibly zero) measure on , the -top-difference semimetric is
The axioms use elementary perturbations. For distinct not comparable by , the single addition makes strictly better than . It is when are -incomparable and when , and it is admitted only when the result is acyclic. For , the single deletion is . An acyclic is a one-step perturbation of toward , written , in either of two cases:
An order is in-between and if it is reached from by a finite nonempty chain of one-step perturbations toward .
For distinct , the partial order ranks every alternative other than strictly above both and and makes no other comparisons, and adds . Put . For a semimetric on with values in :
For every nonempty finite and every semimetric on ,
The "if" direction:
The "only if" direction:
Theorem 3.1 gives a complete description of a family of preference distances that is sensitive to where in a ranking two preferences disagree. The weight in Axiom 3 is the number of menus in which a change at is visible. Taking to be the counting measure gives the top-difference semimetric (Theorem 3.2, with the normalization Axiom 2). The paper then uses to compute diameters of classes of orders, to find best transitive approximations of acyclic preferences, and to compare with weighted Kendall metrics. All of these rest on the additivity (Axiom 1) and on the perturbation calculus of §2.3.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been machine-checked. The mission formalizes the definitions and the proof's structure: the reachability theorem for acyclic orders (Theorem 2.2), the menu-wise decomposition (Lemma 3.3), the counting identity behind Axiom 3, and the reconstruction of from . The perturbation calculus and the reachability theorem are reusable for other order-theoretic distances.
The "if" direction rests on Lemma 3.3. The obvious generalization fails: for the literature's notion of betweenness (), Example 2.1 (p. 10) shows that maximal sets can move away from the target, and additivity breaks. Condition (2) is exactly what restores it, so it must be kept.
The "only if" direction has two hard points. First, Theorem 2.2: arbitrary additions and deletions need not lead from to . A deletion may violate (2), and an addition may create a cycle in a non-transitive relation. The perturbations must be chosen in a particular order. Second, the count of the menus affected by a single addition, and its interaction with acyclicity, must be established exactly, since Axiom 3 fixes these constants.
Everything sits in the namespace PrefSemimetric.TopDiff, with one definitions module Model. The conventions are:
X → X → Prop over [Fintype X] [DecidableEq X]. The goal assumes [Nonempty X], as in "nonempty finite set".IsAcyclicOrder. Acyclicity is reflexivity plus irreflexivity of the transitive closure of the strict part, which is equivalent to the page's absence of cycles of distinct elements.IsSemimetric): nonnegative, zero on the diagonal, symmetric, and satisfying the triangle inequality.Nb b R - 1 is natural-number subtraction; it is exact in its clause, because itself is counted.Two trivializing readings are ruled out. "In-between" keeps consistency condition (2); with the literature's weaker betweenness, the "if" direction is false. Axiom 3 keeps its acyclicity provisos, and dropping them would constrain on cyclic relations. A sorry-free sanity file confirms that the axioms are satisfiable (by ), that a genuine one-step perturbation exists, and that display (8) holds for the counting measure on a two-element set.
Not formalized: Theorem 3.2, Lemma 2.1, Examples 3.1–3.2 and §§3.4–6 (weighted Kendall metrics, computational formulas, diameters, best transitive approximations, non-embeddability). Contributions are welcome on any milestone. Theorem 2.2 and Lemma 3.3 are the natural entry points.
Bibliographic data as cited in the paper's reference list (arXiv:2203.04418v1, p. 29).
In linear regression with a budget, an experimenter holds candidate experiments, each described by a vector , and may run only of them. If the experiments in are run and the unknown parameter is estimated by least squares, the covariance of the estimate is proportional to . A-optimal design chooses to minimise the trace of that matrix, which is the mean squared error of the estimator. The criterion is one of the classical optimality criteria of experimental design (Pukelsheim, Optimal Design of Experiments, SIAM 2006) and appears in feature selection, sensor placement and matrix sparsification.
Selecting the best -set exactly is NP-hard (the paper proves this in its Theorem 1.7), so the question is approximation. Avron and Boutsidis (SIAM J. Matrix Anal. Appl. 2013) connected A-optimal design to volume sampling (Deshpande–Rademacher, FOCS 2010), which samples a set with probability proportional to , and obtained the approximation ratio . Nikolov, Singh and Tantipongpipat (arXiv:1802.08318; Mathematics of Operations Research, 2022) reweight volume sampling by a second measure that can depend on a solution of the natural convex relaxation. Their first result, Theorem 1.3, shows that the approximation ratio of this scheme is controlled by a single combinatorial property of , approximate -wise independence. Their later theorems obtain ratios (when ) and (when is large) by exhibiting such measures.
Let be a real matrix and . For , is the submatrix of the columns indexed by , so . The A-optimal design problem is
with the value for sets whose Gram matrix is singular.
The convex relaxation (1)–(3) replaces the indicator of by :
Write for the matrix with columns , , so that , and .
Let () be the subsets of of size exactly (at most) , and a probability measure on them. Proportional volume sampling with measure (Definition 1.1) is the distribution with
The measure is -approximate -wise independent with respect to a feasible (Definition 1.2) if for all with and ,
For a square matrix with eigenvalues , is the -th elementary symmetric polynomial ; .
Algorithm 1 (p. 8) solves the relaxation for , samples , and pads with arbitrary indices to size if it is smaller.
If is an optimal solution of (1)–(3) and is -approximate -wise independent with respect to , then the output of Algorithm 1 satisfies, for every -set ,
so the algorithm is an -approximation in expectation, and some -set has objective at most (the integrality gap is at most ). The constant is a parameter: the goal fixes no value of it, so later constructions of better measures plug into it unchanged.
Theorem 1.3 turns an approximation question about a continuous, spectral objective into a question about the marginals of a distribution on sets: any measure with approximately independent - and -marginals relative to the relaxation's solution yields an approximation algorithm with the same ratio, and simultaneously bounds the integrality gap of the relaxation. The paper's Theorems 1.4 and 1.5 are proved by applying it to hard-core distributions, giving a -approximation for and a -approximation for .
The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. The formalization produces, beyond the theorem itself, a reusable linear-algebra layer that the pinned Mathlib lacks: the Cauchy–Binet formula for Gram matrices, its extension (4) to all elementary symmetric functions of the spectrum, and the identity . These are standard tools for determinantal point processes and volume sampling, and a later formalization of the hard-core constructions (Theorems 1.4, 1.5) would build directly on this mission's goal.
The reduction itself is a short calculation once both sides of (5) are written as ratios of sums over - and -subsets; the difficulty is in the linear algebra that produces those ratios. Identity (4) needs Cauchy–Binet for non-square matrices together with the relation between the coefficients of the characteristic polynomial, its roots and sums of principal minors; none of this is in Mathlib in the required form, and the eigenvalue side requires that the characteristic polynomial of a real symmetric matrix splits over . Applying (4) to every separately and exchanging the order of summation is bookkeeping between index sets of different sizes, which is where informal proofs are quietest. The expectation also has to be handled honestly at sets with singular : they are never sampled, but the paper's displayed equality on p. 9 counts them, so the first display holds only as an inequality.
Everything is over , with index sets Finset (Fin n) and a Matrix (Fin d) (Fin n) ℝ. A probability measure on is a nonnegative function on subsets of with total mass vanishing on sets larger than ; this covers as a special case. is the elementary symmetric function of the real roots of the characteristic polynomial, applied only to symmetric matrices. Lean's matrix inverse is on singular matrices, so every comparison of objectives assumes positive definiteness of the inverted matrix, and OPT is expressed by quantifying over -sets with positive definite Gram matrix rather than by an infimum.
The statements add the following, each disclosed in the item's Formalization Note: (for the natural-number subtraction ); a positive normaliser , which Definition 1.1 presupposes; positive definiteness of , which is what a finite CP means; Definition 1.2 in cross-multiplied form; and "" in place of the printed "" in the first display of p. 9. Theorem 1.3 assumes a suitable only for the optimal , as the remark after the theorem says; this implies the printed form. The padding of Algorithm 1 is an arbitrary map with and on the support of .
The goal is not inequality (5) alone and is not defined as a sum of minors, and the expectation is not defined as the ratio of p. 9; any of those would make milestones true by definition. A sorry-free sanity file shows that all hypotheses of the goal are simultaneously satisfiable (, , , the point mass at , ).
Contributions are welcome at every milestone; the Cauchy–Binet layer (milestones 2 and 3) is reusable well beyond this mission and is the natural place to start.
Deferred acceptance and top trading cycles are strategy-proof: submitting one's true preference ranking is optimal whatever the other participants do (Roth, 1982). School-choice and residency-match systems around the world use them for this reason. Yet laboratory and field data show participants misreporting systematically, most often by leaving popular options out of their list or by ranking options with high admission chances above options they prefer (Chen and Sönmez, 2006; Hassidim, Marciano, Romm and Shorrer, 2017; Chen and Pereyra, 2019; survey by Hakimov and Kübler, 2021). One line of explanation treats these reports as mistakes; another looks for preferences under which they are optimal, such as expectation-based loss aversion (Dreyfuss, Heffetz and Rabin, 2022).
V. Meisner's paper Report-dependent utility and strategy-proofness proposes report-dependent utility: on top of the value of the option she is assigned, a participant cares about where that option sits in the list she submitted, enjoying acceptance by her reported top choice and disliking acceptance only at the bottom. The paper's Proposition 2 says exactly when truth-telling survives such preferences, for every strength of the report-dependent component. This mission formalizes Proposition 2 and the steps of its proof.
A participant ranks options, labelled . She gets a report-independent payoff from being matched with option , and the options are labelled so that
A rank-ordered list (ROL) is a bijection from options to ranks ; its -th ranked option is . The true ROL ranks options by . She also receives a report-dependent payoff when matched with her -th ranked option, where is decreasing.
The other participants' reports are fixed. An option is attainable () if the participant would be matched with it by ranking it first. The attainability distribution is a probability distribution on the states ; the may be correlated in any way. In a strategy-proof mechanism she is matched with the highest-ranked attainable option of her list, so her match probability at rank under is
and her expected payoff is
Under the truth these are and . The true ROL is optimal if for every .
In Lean, options and ranks are Fin n, a ROL is Rt : Equiv.Perm (Fin n) (option ↦ rank), the truth is 1, is a function (Fin n → Bool) → ℝ, and , are matchProb P Rt r, payoff v ρ P Rt.
For every non-truthful ROL : for all decreasing if and only if
Hence the true ROL is optimal for every decreasing if and only if (3) holds against all non-truthful ROLs.
Proposition 2 gives a testable condition, stated only in terms of beliefs about admission, under which no report-dependent taste of any size can break truth-telling: no alternative list may raise the probability of being matched with one of the top ranked options, for any . Conversely, when an alternative list does raise such a probability, as ranking a safe option first does, a strong enough report-dependent payoff makes that list strictly better than the truth even though the mechanism is strategy-proof. The paper uses this to separate settings in which truthful reports are predicted from those in which self-selection is predicted, and contrasts it with Proposition 1, under which every list is optimal for some beliefs.
The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission provides one, together with a reusable finite model of matching under correlated attainability (match probabilities of the highest-ranked attainable option, the expected payoff (1)) and the stochastic-dominance property of the truthful lottery, which other results about rank-ordered lists in strategy-proof mechanisms can import.
The two directions are elementary in spirit but need care. The "only if" direction in the paper takes a limit of decreasing functions ; a formal proof has to exhibit an actual strictly decreasing and control the report-independent term uniformly. The "if" direction rests on two facts the paper asserts briefly: that the true lottery stochastically dominates every other (which is a statement about the match rule under arbitrarily correlated attainability, not an assumption), and a summation-by-parts rewriting of that uses the equality of total match probabilities across lists. The paper's inequalities "" and the final "" are strict as printed but hold only weakly, so the formal statements use .
Fin n, 0-indexed (Lean index is the page's ). A ROL is Equiv.Perm (Fin n) mapping options to ranks; the -th ranked option is R.symm r; the truth is 1. States are Fin n → Bool; is a real weight function and IsAttainabilityDist P says it is nonnegative with total mass one. Probabilities are finite sums; there is no measure theory.matchProb P R r is the weight of the states in which the rank-r option is attainable and every option ranked above it is not: the highest-ranked attainable option is matched, as on p. 5. The distribution does not depend on the submitted list.StrictAnti ρ, the model's standing assumption; the equivalence also holds for weakly decreasing . The order is a hypothesis (Antitone v). The normalizations and are not imposed: all lists have the same total match probability, so adding a constant to or leaves unchanged, and the statement with them is equivalent. "Non-truthful" is Rt ≠ 1. Condition (3) is Condition3 P Rt, with rbar : Fin n the page's shifted by one and Iic rbar the ranks .Fin n and Fin n → Bool, permutations of Fin n and Mathlib's summation by parts. Proofs of any milestone are welcome, as are alternative proofs of the goal that bypass the decomposition.In many emerging economies, smallholder farmers decide each season how much of their land to give to an export crop, sold through a local processor at a price linked to the world market, and how much to keep for a traditional alternative crop. Yields are uncertain and often correlated across neighbouring regions because they share weather. Governments and development agencies frequently protect farmers with a minimum guaranteed price: no processor may pay less than per unit of harvest. Whether such a floor encourages too little, enough, or too much planting relative to the processing capacity of the region is a policy question with direct consequences for farm income and processor utilization.
Li, Kouvelis and Dada (SSRN 3531158; published in Manufacturing & Service Operations Management 26(2), 2024, doi:10.1287/msom.2022.0076) model this as a two-stage game between two farmers and two capacity-constrained processors, and characterize the land-allocation equilibria in closed form for all-or-nothing yields. This mission formalizes that characterization, together with the second-stage pricing results it is built on.
There are two regions , each with one farmer and one processor. The processed crop sells at the world price . Processor has unit processing cost and capacity , with , and the minimum guaranteed price satisfies .
Second stage. Farmer has planted units of land and harvests , where is the random yield. Both farmers sell first to the winning processor (Processor 1 on ties); a winner who cannot absorb the whole harvest first takes the harvest of its own region's farmer, and the residual goes to the losing processor up to its capacity (Theorem 1 of the paper). Processor 's profit is its margin times the amount it procures. Its willingness to pay is the highest price at which winning at is no worse than losing at (conditions (7)–(8)). The processors then settle as in a second-price auction (Theorem 3): if , Processor 1 wins and the final prices are ; otherwise Processor 2 wins and they are . Farmer 's revenue is the sum of her sales to the two processors at the final prices.
First stage. Farmer 's expected profit is
where is the per-unit cost of export-crop land, including the forgone alternative crop, and is a constant. An equilibrium is a pair in which each maximizes given the other farmer's choice.
All-or-nothing (AON) yields. Each takes the value or . In the symmetric IID chain the processors are identical (, ), the farmers are identical (, ), and the yields are independent with .
In the symmetric IID chain with , and the participation condition :
The theorem shows that the price floor is the decisive policy lever. A low floor leaves farmers with thin margins and produces under-planting together with a whole continuum of equilibria, so total production is pinned down but its split between regions is not. Intermediate floors coordinate both farmers on filling exactly the processing capacity. A high floor makes planting so attractive that both farmers plant enough to fill both processors on their own, and part of the harvest goes unsold whenever both crops succeed. These regimes underlie the paper's later comparisons of ownership structures and yield correlations (§4–§5).
The result is proved on paper; it has no machine-checked proof. Formalization adds a precise model of a second-stage protocol that is described partly in prose, and it pins down the boundary cases. Checking the printed statement already corrected three points: part 2 of Theorem 6 is false as printed, the participation condition must be strict for part 1, and the threshold of part 4 must be strict.
The profits are piecewise linear in , but the pieces come from nested and operations in the allocation rule, multiplied by a WTP that is itself a ratio of such terms. Each farmer's best response is therefore discontinuous and has to be found region by region. The two farmers are not symmetric even in the symmetric chain, because Processor 1 wins every tie and so farmer 1's harvest is served first. Equilibrium claims are global: "unique equilibrium" requires excluding every other point of , including allocations above and corners where a farmer plants nothing. The WTPs are defined as suprema, so identifying them with (9)–(10) is a separate optimization over all competing prices.
All quantities are real numbers. The model is one definition, AgriChain.LandAlloc.Model: the chain, the allocation of Theorem 1 indexed by the winning processor, the profits (5)–(6), the WTP sets defined by (7)–(8) and the WTPs as their suprema, the final prices of Theorem 3 with ties going to Processor 1, the revenues (11)–(12), AON yield laws, the expected profits (13)–(14) as finite sums over the four yield outcomes, and the equilibrium. The equilibrium is the published generic pure-Nash predicate CarbonDoubleCount.Planner.IsPureNash, with feasible sets . and are real parameters, as in the paper from (13) on.
Hypotheses added to the goal: , , and (the thresholds divide by , and , and the bound needs ); (the over-production equilibrium plants ); the participation condition of p. 19, made strict; and part 4's threshold, made strict. "Unique equilibrium" is an "if and only if", asserting existence. Part 2 of Theorem 6 is not posed: at , , , its hypotheses hold, but the unique equilibrium is , whose total is below . Theorem 5 (p. 18) and part 2 of Theorem 4 are not posed either.
The goal is about the equilibria of the full model. Defining the WTPs by (9)–(10), defining by the two-term AON form, or stating Theorem 6 for a hand-simplified symmetric profit would make the milestones definitional and is ruled out. Contributions are welcome on every milestone. The WTP computation and the AON reduction are reusable for the paper's other correlation structures (§4–§5).
A repair supplier can invest in capacity before a service contract begins, while the customer may know more about how often her equipment fails. The supplier must choose both an incentive to maintain uptime and a menu that gives customers reason to reveal their failure rates. Li, Mishra, and Netessine study this interaction for maintenance, repair, and overhaul services. Their model compares a price per repair with a performance-based contract (PBC), under which the supplier is paid for the product's uptime. The latter ties revenue to the outcome the customer values. The paper asks when that arrangement can preserve the full-information outcome despite asymmetric information about product reliability. Li, Mishra, and Netessine, SSRN author version, §§1, 3, 5.
The specific result targeted here is Proposition 5(i). The two customer types differ both in failure rate and in the value of their outside options. This creates countervailing incentives: the customer with the less reliable product need not always be the one seeking a better contract. The paper identifies a range of outside-option ratios in which a single separating PBC menu gives each type the same contract she would receive if the supplier knew her type. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
A contract period has length one. A product has failures at a rate , and the supplier sets a repair rate by investing in capacity. Each repair requires a random lead time. The product's uptime is one minus total downtime. The paper's expected-uptime expression is . It uses this expression to turn the stochastic model into the closed-form payoffs of its supplementary equation (B.39). Li, Mishra, and Netessine, §3, pp. 7–10, and supplement (B.39), p. 9.
There are two types, and , with . The probability of the low-failure type is . Type can decline the contract and obtain her reservation payoff ; the setting has . The supplier receives per unit uptime from a customer choosing contract and incurs a capacity cost plus expected material cost . The customer's payoff, evaluated at her actual failure rate , is , where is revenue per unit uptime. The supplier's corresponding payoff is . Li, Mishra, and Netessine, §§3–4 and supplement (B.39).
A menu contains one positive-price, positive-rate contract for each type. Individual rationality (IR) requires that each type's payoff from her designated contract reach her reservation payoff. Incentive compatibility (IC) requires that neither type prefer the other contract. In problem (9), the supplier maximizes her prior-weighted payoff over all menus satisfying both IR and both IC constraints. Under full information, the two types can be optimized separately; Proposition 1(ii) gives the first-best PBC repair rate and the price . Li, Mishra, and Netessine, Proposition 1, p. 12; problem (9), p. 18.
The goal formalizes Proposition 5(i). Define the first-best menu by offering to type and to type . Condition (10) is
When this condition holds and both first-best prices are positive, the first-best menu is feasible for problem (9) and achieves at least the supplier payoff of every feasible menu. Both IR constraints bind, so each customer's information rent is zero; the two repair rates differ, so the menu separates the types. Li, Mishra, and Netessine, Proposition 5(i), p. 18.
The milestones follow the paper's stated calculations: the binding-IR price and reduced objective from (B.6)–(B.7); the PBC part of Proposition 1(ii)–(iii); the two IC slack formulas (B.41) and (B.42); and the first-best payoff bound used at the end of the proof of Proposition 5(i). The joint-profit benchmark is . Li, Mishra, and Netessine, supplement pp. 3–4 and 9.
The result identifies a parameter region in which screening does not reduce productive efficiency or leave an information rent to either customer type. The supplier can offer the same repair capacities and prices as in the full-information problem while satisfying each type's participation and truthful-choice requirements. This makes the full-information outcome a concrete benchmark for the other regions of Proposition 5, where one or more constraints bind differently. Li, Mishra, and Netessine, Proposition 5, pp. 18–19.
The mathematical result is proved in the paper. This mission asks for machine-checked proofs of the model identities and the first region of its screening theorem. The reusable artifacts are the explicit PBC menu, the four feasibility constraints, the separation between supplier and joint profit, and a uniform upper bound over every feasible menu. No existing platform theorem found in the local prior-art index has this paper's contract space and payoffs.
The first-best solution optimizes a contract separately for each known type. With private failure rates, a customer can choose the contract intended for the other type; solving the two full-information problems alone therefore does not establish a feasible screening menu. The signs of both IC slacks must agree with the ratio interval in condition (10), and every denominator in the ratio and in the first-best prices must be nonzero. Feasibility still is not enough for the conclusion: optimality compares the candidate with all positive-price, positive-rate menus satisfying the four constraints, including menus with slack IR constraints. Li, Mishra, and Netessine, problem (9), p. 18, and supplement (B.39)–(B.43), p. 9.
The Lean development uses real-valued prices, rates, costs, payoffs, and prior weights. It represents expected uptime and expected payoffs by the paper's closed form (B.39), ; it does not encode the underlying Poisson failure process or random repair times in this first mission. The model keeps a separate customer payoff, supplier payoff, and joint-profit function, so is never confused with . The menu's feasibility predicate contains exactly the four constraints of problem (9), plus the strict positivity of both prices and both repair rates written under its maximization sign. The objective uses the prior weights and . Li, Mishra, and Netessine, §§3–5.2 and supplement (B.39).
The standing predicate makes the parameter domain explicit: , , , , and . The order of the two outside options is stated in the paper's setting; is needed for the ratio in (10). The goal also assumes , because a first-best menu with a nonpositive price is not in problem (9)'s admissible set. The algebraic IC milestones explicitly exclude zero denominators, and the goal's ratio condition with the standing order rules out its degenerate denominator cases.
The candidate's optimality is stated against every feasible menu. Restricting competitors to first-best-form or binding-IR menus would make the main theorem weaker. Useful contributions include proofs of the source's algebraic identities, the first-best profit properties, the global upper bound, and Proposition 5(i) itself. The omitted stochastic expected-uptime identity and the remaining cases of Proposition 5 are separate formalization work; the present goal uses the closed form printed by the paper.
When a bank run forces asset sales, the sale price can reflect buyers’ beliefs about the condition of other banks as well as the assets being sold. In the two-bank model of Li and Ma, observing two runs makes buyers more pessimistic about the aggregate state than observing one. That change in beliefs lowers the market price precisely when both banks need liquidity. The paper studies whether a regulator can commit in advance to a purchase price that reduces joint failures while recovering its expected expenditure. Its Proposition 3 gives a specific break-even policy in a limiting version of the model.
The paper proves the policy result in its accepted manuscript, dated 28 October 2021, and was published in Management Science in 2022. The result is mathematically known. The work here is to state its price, payoff, and risk claims as machine-checkable theorems with the paper’s parameter restrictions visible.
There are two banks and two aggregate states, good and bad . In state , each bank’s asset portfolio produces a cash flow uniformly distributed between a state-dependent lower bound and a common upper bound . The good state has the higher lower bound: . Conditional on the state, the banks’ cash flows are independent. The prior probability of is ; the probability of is . These are the primitives of §2.1 of Li and Ma.
Each bank finances a unit portfolio using equity , retail deposits , and positive wholesale debt . A wholesale creditor who withdraws early receives a gross factor , while one who waits receives , where and . The debt obligations used throughout are
Assumptions (1)–(3) say in both states, , and . The candidate market-price interval begins at and ends below . The upper-cash-flow condition in footnote 29 is . It keeps the uniform probabilities within their intended range on this interval. Footnotes 25 and 27 explain why the interval is nonempty and ; see pp. 13 and 15 of the accepted manuscript.
Buyers who observe bank runs use a posterior probability of state , with . Their expected profit from buying one unit at price is . A market break-even price solves in . The two prices differ because the number of runs changes buyers’ posterior. In the paper’s regime, a committed regulator price gives the critical cash flow
The regulator’s expected payoff averages purchase gains over the two states and the possibilities of one or two runs, exactly as in equation (22). The systemic-failure probability is the prior-weighted probability that both banks’ cash flows fall below , using the closed uniform formula on p. 26 of Li and Ma.
The milestone path establishes the existence of the two market prices, their ordering, the payoff identity (23), the signs of at those prices, and the monotonicity of payoff and systemic risk. The main target is Proposition 3: a unique regulator price lies strictly between the market prices,
Both and decrease strictly as the committed price rises through . Among all prices in the regulator’s program (20)–(21),
the price minimizes and satisfies . This is the limit interpretation of the comparison printed at the end of Proposition 3.
The theorem identifies a precommitted price at which the regulator breaks even across possible numbers of runs, while a buyer who acts after observing the run count must break even conditional on that count. The resulting interval between and is where liquidity support can lower joint failures without an expected transfer. The program also excludes saving banks whose cash flow is below ; the policy result meets that solvency restriction.
A checked formalization would make the paper’s assumptions and the links among posterior prices, regulator payoff, and systemic risk explicit. Proposition 3 is proved in the paper; its Lean proof and the supporting results in this mission remain to be completed. The definitions of the uniform two-state model, posterior weights, and payoff sums can support later formal work on related liquidity policies, while the paper-specific financial parameters remain tied to this model.
The regulator cannot choose a price from the simple interval between two fixed asset values. Each price changes the cash-flow threshold at which runs lead to failure, which changes the posterior beliefs used in and the probabilities weighting . A direct comparison of with either market price therefore does not determine the sign of the regulator’s total payoff. The proof must control both market-contingent profits and their state and run-count weights before the break-even price and its risk effect can be certified.
Lean represents the aggregate state by a two-constructor type and the primitive bank data by one parameter structure. The standing predicate includes assumptions (1)–(3), , , , , footnote 29, and positive wholesale debt. The last condition makes the model’s financing convention explicit. The formulation uses the paper’s closed forms in the limit; it does not encode creditor signals or the full global game.
Uniform probabilities are not clipped, because the relevant threshold lies inside the cash-flow support on the stated price interval. The market prices are characterized by their break-even equations rather than chosen from a prior existence assumption: a milestone establishes their existence. is defined by equation (22), not the later identity (23), and the policy goal asserts existence and uniqueness of its zero. The feasible set is exactly program (20)–(21). Strict decrease means strict antitonicity on . Lean’s real division is total at zero, so the critical-threshold formula has junk values at singular inputs; every claim uses the economically valid interval. Useful contributions include proofs of the market-price milestones, the payoff identity and signs, and the two monotonicity results.
A firm can have valuable operations yet fail when a temporary cash shortfall leaves it unable to pay its bills. Cash reserves protect the firm, but holding them is costly. In Lee and Rivera’s study, the manager also doubts the probability model for future shocks. The manager evaluates a policy under the least favorable model within a prescribed set of plausible models. This makes the composition of pessimism a decision linked to the firm’s cash position. The paper’s central qualitative claim is that adverse beliefs respond to recent shocks in a way resembling extrapolation bias: a recent shock changes the manager’s assessment of future shocks of the same type.
The result belongs to the paper’s 2019 working version, Extrapolation Bias and Dynamic Liquidity Management. The later Management Science article has a different title. The theorem and equation numbers here refer to the working version, especially §2, §3.3, §4.1 and Appendix A.
The firm has a positive size δ and cash reserves M. Its cash ratio is m=M/δ. The manager chooses an investment rate i, which raises expected size growth but incurs an expenditure g(i)=i+θi²/2. The size process has a permanent shock with volatility σδ; operating cash flow has an independent temporary shock with volatility σY. The manager discounts at rate r. Cash earns r−λ, so λ is its carry cost. At cash exhaustion the firm either issues equity, paying proportional and fixed costs ρ₁ and ρ₀, or liquidates for a fraction ω of the ambiguity-only benchmark value δqᴬ. These objects and their cash-management interpretation follow the working paper’s model and HJB equations.
The manager allows drift changes h=(hᴾ,hᵀ) in an ambiguity ellipse,
The superscripts P and T mean permanent and temporary. The two radii κP and κT limit how much each drift can be distorted. A distortion h changes expected size growth by σδhᴾ and expected cash flow by σYhᵀ. The manager chooses i against the least favorable h. On the ellipse boundary, the model writes hᴾ=−κP cos φ and hᵀ=−κT sin φ for an angle φ in [0,2π].
The paper uses a scaled value function F: firm value at size δ and cash M is δF(M/δ). In the no-payout region 0≤m≤m*, F satisfies the max-min Hamilton–Jacobi–Bellman equation (25), with payout boundary m*. The conditions at m=0 compare refinancing with liquidation, and the value is linear in cash above m*. The ambiguity-only benchmark qᴬ is determined by the paper’s equations (36)–(38). For an increasing concave F, the worst-case angle and distortions are defined by (26)–(27).
For every cash ratio in the no-payout region, the angle from (26) is the unique minimizer of the HJB expression among admissible angles. Its associated worst-case distortions satisfy four shock-response inequalities:
Here the first subscript names the belief component and the second names the shock. The four coefficients are the derivatives in the display on p. 21, multiplied by the corresponding shock loading of the cash ratio. When F″(m)<0, the temporary-shock inequalities are strict. The permanent-shock inequalities are strict when also m>0. This states the paper’s §4.1 claim at the boundaries where its printed strict wording would otherwise fail.
The attack path follows four statements in the working paper: Lemma 4 equates minimization over the filled ellipse with minimization over its angle-parametrized boundary; Proposition 3 (19) gives the investment and belief-allocation conditions for the two-state HJB; equations (26)–(27) give their scaled counterparts; and §4.1 describes how beliefs change as the cash ratio rises. The milestone list retains the printed passages verbatim and identifies the necessary corrections in its titles.
The result identifies which adverse cash-flow model the manager uses at a given cash position. With little cash, temporary losses can force costly financing or liquidation, and the adverse model weighs them more heavily. With more cash, the adverse model shifts toward permanent shocks to firm size. The sign pattern translates that change in beliefs into responses to realized shocks. It supplies a precise meaning for the paper’s claim of endogenous extrapolation bias within this cash-management model.
The paper gives analytical HJB conditions and illustrates the time-varying beliefs in Figure 4.1. This mission asks for Lean proofs of the qualitative allocation and sensitivity statements for the paper’s stated variational system. The local formalization records three corrections to the working paper’s formulas and prose, so solvers have a single explicit target rather than relying on incompatible printed expressions.
The obvious appeal to worst-case beliefs does not by itself establish which point of the ellipse minimizes the HJB expression, whether that point is unique, or whether its angle remains in the required quadrant. The HJB also mixes investment and belief allocation, while the target concerns derivatives of the belief allocation with respect to the cash ratio. Finally, the printed strict signs fail at m=0 and at a smooth payout boundary where F″(m*)=0. The theorem must account for both endpoints while preserving the paper’s interior claim.
Lean represents parameters in a structure, the ellipse as a subset of ℝ×ℝ, and F as a global C² real function restricted to nonnegative cash. The scaled solution predicate includes monotonicity, concavity, the attained max-min equation (25), and the boundary conditions (28)–(31). The HJB angle interval is the closed [0,2π] of (25). No real supremum of an empty or unbounded set is used. The benchmark predicate records (36)–(38) and the positive transversality gap r−µ−iᴬ.
The working paper has three relevant slips. Lemma 4’s h-form HJB omits the volatility multipliers present in (11)–(12), so the formal statement restores them and uses the paper’s γ=2 restriction. Proposition 3 (19) prints an extra δ in the investment condition; the formal statement uses the condition implied by (18). The last sentence of §4.1 p. 20 reverses the belief monotonicity directions implied by the preceding prose and the p. 21 sensitivity display; the formal statement follows the latter. Strictly positive κP, κT, σY, ω and qᴬ specify the nondegenerate regime in which the arctangent formula and liquidation value carry their intended meaning.
The scaled solution predicate prevents an arbitrary concave function from replacing the paper’s value function. The target requires the displayed angle to be the actual unique minimizer of (25), and its divisions have positive denominators under the model assumptions. Reusable work includes the ellipse minimization and real-analysis facts behind the angle’s monotonicity. Contributions proving these milestones or the final sensitivity theorem are within scope.
Humanitarian organizations (HOs) have long helped refugees with in-kind assistance: food, hygiene and shelter items bought at wholesale cost and handed out. Cash assistance, money that refugees spend at local stores, has grown quickly. In 2014 it was 6% of the $25 billion of humanitarian assistance worldwide; by 2019, cash and vouchers were 18% (High Level Panel on Humanitarian Cash Transfers 2015; Jódar Vidal et al. 2020, both as cited by Kotsi, Wu and Pedraza-Martinez). Cash lets refugees buy what they need and brings revenue to the host community. It also creates demand that a local retailer with market power can exploit: field reports from Swaziland and Uganda describe price increases after cash programmes began, and UNHCR advises in-kind assistance "where increased demand on markets will cause inflation".
Kotsi, Wu and Pedraza-Martinez (MSOM 24(6), 2022) model this as a game between an HO and a monopolist retailer. Without intervention the retailer answers cash assistance by raising its price above the monopoly price it charged before the refugees arrived. That hurts local residents and reduces the quantity of goods refugees receive. The paper then designs interventions run by an HO-government partnership. One of them is price-dependent cash assistance (PDCA): the HO announces how much cash it will give as a function of the retailer's prices. This mission formalizes the paper's result that a correctly designed PDCA schedule makes a chosen target price the retailer's own optimal choice.
An HO has budget . It gives a fraction to the refugees as cash and spends the rest on goods bought at unit cost . A monopolist retailer buys at the same unit cost and sets the retail price.
In the symmetric-goods case every good has the same cost and price , and is the local residents' aggregate demand. Refugees spend their cash in full, buying units. The retailer's profits from refugees and from residents are
and its total profit is . Assumption 2 of the paper: is continuously differentiable, on where , and is unimodal with unique maximizer . The pre-arrival maximum profit is .
The HO-government partnership picks a target . It is feasible if the retailer earns at least its old profit, , and residents are no worse off, which the paper writes as . The symmetric PDCA scheme (equation (27)) pays the cash fraction
when the retailer sets price . The retailer then earns .
In the general -good model, prices are vectors, is the refugees' demand under cash fraction and in-kind bundle , and the PDCA policy of Proposition 4 is a clipped linear function of a weighted price index .
Assume Assumption 2, concave on , and a feasible target with and . Then , and
with the unique maximizer when (§6.3, p. 22).
The goal is the paper's positive design result. Without a policy, the retailer's best response to cash assistance is a price above (Proposition 1 of the paper). The PDCA scheme reverses this incentive with no price regulation: the government only monitors that announced prices are kept. Every feasible target, including the one that maximizes social welfare, can be implemented this way, and the retailer still earns at least . Proposition 4 gives the general -good recipe: weight each price by the retailer's marginal profit, and let the cash fraction fall with the price index at the rate that offsets the marginal gain from raising prices.
The results are proved in the paper, which argues the symmetric case in two paragraphs. No machine-checked version exists. Formalizing them makes several conditions explicit that the text leaves implicit. The slope of the scheme must be non-positive, which needs . The clipped branches must be compared with the unclipped concave profit. The general proposition is established at the level of the first-order condition.
The obvious argument says that the PDCA profit has a critical point at by construction, so is optimal. This fails twice. First, the schedule is clipped to , so the profit is only piecewise smooth and is not globally concave: on the branch the profit need not be dominated by a concave function through unless the comparison is made explicitly. Second, the middle branch is concave only if the schedule's intercept is non-negative, which depends on the sign of and hence on and Assumption 2. The uniqueness clause needs strict versions of each comparison and fails without .
All quantities are real. Prices range over ; the scheme, the profits and the slope are explicit defs transcribing (18) and (27), with as Lean's deriv, used only at points where Assumption 2 makes differentiable. is the value , not a supremum. Assumption 2 is read on : continuously differentiable there, on , and nondecreasing on , nonincreasing on , with its unique maximizer. " concave" is read on . Feasibility uses the retailer clause and ; the refugee-utility clause of (26) is dropped, which strengthens the goal. In the -good model, and are abstract functions, partial derivatives are Fréchet derivatives on unit vectors, and Proposition 4 assumes , and differentiability at the target, and concludes the first-order condition (A.13) of its proof; the mission does not state the -good global optimality (16).
The goal must not be replaced by the first-order condition alone (milestone 3) or by an assumption that the PDCA profit is concave: it quantifies over every price , with the clip of (27) in place.
The development needs only one-variable calculus and convexity from Mathlib. The hypotheses are satisfiable: for , , , , , , the target profit exceeds . Proofs of any milestone, and statements of the paper's Propositions 1, 3 and 5 for the same model, are welcome.
Biopharmaceuticals such as vaccines and therapeutic proteins are produced by living cells grown in a bioreactor. In a batch fermentation the cells multiply until the medium is depleted and the culture enters a stationary phase, after which the batch is harvested. A bleed–feed operation removes part of the culture and replaces it with fresh medium, restarting exponential growth in the same bioreactor and saving the cost of cleaning, sterilising and setting up a new batch. Regulators cap the number of bleed–feeds per batch. The operational question is when to bleed–feed: too early forgoes biomass that would have grown, too late risks the culture entering the stationary phase first and the opportunity being lost.
Koca, Martagan, Adan, Maillart and van Ravenstein model this decision as a finite-horizon Markov decision process and show that, under conditions on the growth and risk profile, the optimal policy is described by three thresholds (SSRN 3659907; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1163). The paper reports an implementation at MSD (Merck), and threshold rules of this form are what can be written into production plans.
The state of a batch is :
Starting from biomass , the biomass at age is , and continuing for one period earns the increment . The culture stays in exponential growth with probability , where the rate is zero up to a critical biomass and strictly increasing beyond it; otherwise it enters the stationary phase and earns nothing more. The critical age is the least age at which .
The value function is defined by the optimality equations: and, for ,
with and . Bleed–feed is optimal in when and ; continuing is optimal when .
Assume Condition (4), for ; Condition (5), for and ; and Assumption 1, that bleed–feed is optimal at age whenever . Then there are thresholds , and with
In the paper's order: the risk profile facts of §3 (p. 12); Remark 1 and Propositions 1–2, giving monotonicity in the age and Theorem 1; Propositions 3–4, giving monotonicity in the growth rate and Theorem 2; Propositions 5–6, giving monotonicity in the count and Theorem 3. Theorems 1, 2 and 3 are the three clauses of the goal, each under its own hypotheses (Theorem 3 needs none).
The result turns a dynamic program over a continuous state into three monotone rules, each with a direct operational reading: bleed–feed older cultures, faster-growing cultures, and cultures early in their bleed–feed budget. The thresholds are monotone in the remaining coordinates (Corollary 2 of the paper), which is what makes the policy tabulable for a production plan.
The paper proves the result on paper; nothing about this model is formalized. A complete development gives a machine-checked monotone-comparative-statics argument for a reset-type MDP with a continuum of states and an expectation over a general distribution, including the measure-theoretic content the paper leaves implicit: that is an honest integral of a bounded measurable function. The formalization also repairs two printed points that matter for correctness (see Formalization scope).
Each monotonicity result is a backward induction a few lines long on paper, but the inductions interact. Monotonicity in holds trivially before the critical age and needs Condition (4) after it; the age threshold requires gluing the two regions, which the paper does not spell out. Monotonicity in compares two cultures whose critical ages differ, and its base case at age rests on Assumption 1. Monotonicity in requires , an inequality between integrals whose integrands are themselves defined by the recursion, so integrability and measurability in must be carried through the induction. A pointwise argument that ignores the integrals proves nothing about .
All declarations live in the namespace BleedFeed.ControlLimit. One definition file holds the parameters (Params), the standing assumptions (Standing), , , , the critical age, the value recursion , , , the predicates BleedOpt and ContOpt, Condition (4), Condition (5) and Assumption 1. Ages and counts are natural numbers; everything else is real. is a probability measure on with , and is a Bochner integral against it.
Committed conventions, each disclosed in the statements:
"Optimal" is always the comparison of with in the optimality equation, never a threshold policy assumed in advance, and is the integral, not a free parameter: a formalization in which could vanish by non-integrability would make continuing always optimal and the thresholds trivial. The hypotheses of the goal are jointly satisfiable with (checked on an explicit instance).
Contributions welcome: proofs of the milestones; general lemmas on measurability and integrability of finite-horizon value recursions over a real parameter; and a sharper, non-vacuous instance witnessing Condition (5).
Many service providers are paid under a contract that makes them responsible for a customer's costly failures over a fixed window: a hospital penalized for heart-failure readmissions within 30 days, or a maintenance contractor responsible for engine replacements. A preventative appointment lowers the chance of such a failure, and the sooner it takes place the fewer customers fail while waiting. Capacity for appointments is limited. A clinic plans a fixed number of base slots per period at no incremental cost, and can add a limited number of surge slots (overtime, external staff) at a cost per slot. The scheduler therefore trades the cost of surge capacity against the discounted cost of failures caused by delay.
B. Grant, I. Gurvich, R. K. Mutharasan and J. A. Van Mieghem (SSRN 3092667; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0932) model this trade-off as an infinite-horizon discounted dynamic program, motivated by follow-up appointments for heart-failure patients at Northwestern Memorial Hospital. Their first optimality result, Proposition 1, identifies when the simplest policy, booking every request in the earliest period with a free slot, is optimal.
Time is divided into periods. The appointment book at the start of a period is , where is the number of appointments already booked periods ahead and is the booking horizon. Each period has slots: base slots and surge slots. A valid book has for every and .
At the start of each period new requests arrive, i.i.d. across periods with law supported on . The scheduler books them: an action is admissible (1) if (no same-period booking), for , and . If the requests do not fit, every free slot is filled and the remaining overflow requests are sent elsewhere at cost each.
Between periods each booked customer independently fails with probability , at cost , and leaves the book; the others move one period closer, so the next book is a product of binomial thinnings of with survival probability (4). A customer who reaches the appointment shows with probability and afterwards fails within the contract window with probability ; a no-show (probability ) fails with probability . Serving appointments costs (5). The expected one-period cost (7) is
and a policy is valued by its expected total discounted cost (9), with discount factor .
The First-Available (FA) policy books the requests into periods in order, filling every free slot of a period (base, then surge) before using the next.
If
then FA is optimal: for every admissible policy and every valid book .
Proposition 1 gives a closed-form, state-independent and arrival-independent sufficient condition under which the scheduler needs no optimization at all: book every request as early as possible, using surge capacity whenever base capacity is full. The paper's numerical study finds FA optimal in a large fraction of realistic scenarios, so the condition marks out a regime in which a hospital can use the simplest rule without loss. Together with Propositions 2 and 3 of the paper (base-first and base-first/last-surge policies) it maps out which simple policy to use as the surge cost varies.
The paper's argument for Proposition 1 compares the expected discounted cost of one customer booked at delay with surge against the same customer at delay without surge, and concludes optimality from the comparison. That step is an incremental-cost heuristic: the passage from the four inequalities (17)–(20) to optimality of FA in the dynamic program is asserted in one sentence, not proved. Milestones 4 and 5 formalize the algebra the paper does carry out; the bridge from (17)–(20) to optimality of the policy is the open part of this mission. As far as is known, no machine-checked proof of this result or of any optimality result for appointment scheduling with surge capacity exists.
The obvious argument is the paper's: each request is cheaper earlier, so book it earlier. In the dynamic program the requests interact. A customer booked early occupies a slot that a later arrival could have used; failures free slots again; surge cost is charged on the realized number of customers present at the appointment, after failures; and overflow depends on how full the book was left by earlier decisions. A single-customer comparison does not account for any of these, and the per-customer cost of FA (12) need not even be monotone in the delay for every parameter choice. Any argument has to account for the whole state of the book, not one customer at a time.
All objects live in the namespace SurgeAppt.FirstAvail. Costs and probabilities are real numbers and counts are natural numbers. A book is a function , indexed as on the page; the transition reads into and sets . The cost (7) is computed with the surge cost (5) and the expected failure term written as a finite sum over next books. A policy is a sequence of decision rules (Markov deterministic, possibly non-stationary); it is admissible if each decision at a valid book with satisfies (1), including the forced action when (1) is empty. The value (9) is the series over the law of the book at time ; it is never defined as a fixed point. Condition (13)'s minimum is read as "for every pair ", which is vacuous when .
Hypotheses added to the page and disclosed in every statement: , , , , and ; the page's , and with are kept. History-dependent and randomized policies are not modelled; the paper's remark after (11) that a stationary optimal policy exists licenses comparing FA against Markov policies.
The goal is not trivialized: the competitors are every admissible Markov policy, not only first-available-like ones; the admissibility of FA is part of the conclusion, so a rule that skipped bookings could not qualify; and the value is a convergent series of bounded nonnegative costs, not a junk value.
A complete development needs: finite discounted MDP facts (milestones 2 and 3, reusable for any finite-state model with constrained actions), properties of the product-binomial kernel, and a comparison argument for the goal. Proofs of any milestone, alternative arguments for the goal, and counterexample searches that probe the boundary of (13) are welcome.
On-demand service platforms (home cleaning, tutoring, handyman and care services) match customers with independent providers and keep a commission on every transaction. Once a customer and a provider have met through the platform, both can save the commission by transacting directly the next time. This platform leakage (also called disintermediation) is a central operational concern for such platforms: it erodes revenue and can make the platform unviable. Platforms counter it with lower commissions, perks such as insurance and payment protection, and enforcement.
He, Savin, Goh and Teo (SSRN 3550646; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1179) build a queueing-game model of this trade-off. The platform sets the share of each fee it pays out, providers choose whether to work on the platform, off it, or not at all, and customers choose where to queue. The paper's main result for perfect information, Proposition 3, gives the exact range of the customers' counterparty risk (the extra cost of transacting off-platform) in which leakage occurs at the platform's optimum. This mission formalizes that result and the chain of results its proof rests on.
There are two provider types , with providers of type . Customers value type- service at , every provider serves at rate , and customers pay per unit of waiting time. With the squared coefficient of variation of service times, put . Aggregate demand arrives at rate with (supply-constrained service, (1)).
Customers. An on-platform queue of providers at fee with demand rate has expected wait ; a single off-platform provider has . Off-platform customers bear an extra cost . Customers join each queue until their net utility equals that of the outside option, which determines the equilibrium demand rates and .
Providers. A provider of type has opportunity cost rate , with . Off the platform he sets a fee maximizing , earning utility . On the platform, when type- providers share a symmetric fee , each keeps the share of the fee and earns . A provider participation equilibrium (Definition 1) is a pair of head counts on and off the platform from which no provider wants to switch among on-platform, off-platform and outside options. When several equilibria exist, providers settle on the one with the most providers on the platform.
Platform. Anticipating these responses, the platform chooses payout ratios to maximize its profit rate
absorbing the counterparty risk on every on-platform transaction.
The paper's closed forms are and , and the non-platform opportunity cost is .
With
the platform's problem has an optimum, and at every optimal payout pair and in the selected participation equilibrium,
At the paper's own optimal payout ratio the equivalence (25) holds whenever .
The result separates the two forces behind leakage. Below , counterparty risk is cheap enough that the platform finds it profitable to pay providers enough to stay. Above , off-platform service is so unattractive to customers that providers prefer their outside option. Leakage is confined to the interval between, so a platform can read off whether perks that lower , or changes in pool size , push a provider type into or out of the leakage regime. The interval shrinks as grows, which is the paper's case that larger provider pools protect platforms.
The result is proved in the paper, by hand. No machine-checked version exists. The mission produces a formal model of a queue-based Stackelberg platform game: customer queue-joining equilibria, symmetric fee equilibria among providers, participation equilibria with a selection rule, and an optimizing leader. This structure recurs throughout the platform-operations literature (Taylor 2018 and its successors) and is reusable for related models.
Each step is elementary in isolation; the work is in the chain. The platform's objective depends on through the selected participation equilibrium, which is discontinuous in : it jumps from to providers at . Optimality must therefore be argued over a piecewise objective, not by first-order conditions. The natural first idea, evaluating everything at the closed-form , proves only the third clause of the goal. The goal also quantifies over every optimum, including ties at , where the platform is indifferent between keeping and losing a type. The final equivalences then require nontrivial manipulation of nested radicals in (A9)(ii).
Everything lives in the namespace PlatformLeakage.Perfect, in one definition file and eight theorem files. Parameters are a structure Params, with real values and natural-number head counts; the provider types are an inductive PType with constructors h, l. Every statement assumes Params.Std: , , , , , , and (1). Positive parts are max x 0, and square roots are Real.sqrt, with every radicand nonnegative under Std.
Committed conventions:
Classical.epsilon).A formalization that states the goal only at of (23), or that defines utilities by , would be trivial and is ruled out. Proofs of any milestone, and reusable lemmas on nested radicals or on piecewise-monotone optimization, are welcome.
Firms facing a new technology rarely decide in the dark: they run pilots, prototypes and market tests before committing. The management literature on disruptive technologies (Christensen, The Innovator's Dilemma, 1997) argues that incumbents fail because they evaluate new opportunities with tests tuned to their existing business, and that entrants succeed because they test differently. Gans's paper (NBER Working Paper 29091, published as Experimental Choice and Disruptive Technologies, Management Science 2023, doi:10.1287/mnsc.2022.4496) turns this into a decision-theoretic question: when a firm may choose which experiment to run, and experiments differ in how they trade false positives against false negatives, which one does it choose?
The first result of the paper, Proposition 1, is the building block for everything after it (incumbent versus entrant choices, competition, cooperation). It says that the optimal experiment is biased toward the firm's own predisposition, echoing the result of Che and Mierendorff (Optimal Dynamic Allocation of Attention, American Economic Review, 2019) that information seekers choose news sources that reflect their own bias.
A firm decides whether to exploit a new technology. The state of the world is (the technology works) or (it does not). Exploiting earns in state and in state ; not exploiting, the status quo, earns . The payoffs satisfy . The firm's prior probability of is , with .
Without information the firm exploits when , that is, when , where the no-information threshold is
An experiment yields a signal or , with and (Table 1 of the paper; is the sensitivity and the specificity). Experiments are costless; the firm runs exactly one, chosen from the experiment set
Put . The w-biased experiment is : a working technology always produces , so the signal is conclusive bad news. The n-biased experiment is : the signal is conclusive good news.
After observing the signal, the firm decides whether to exploit. A decision rule assigns an action to each signal; there are four. The value of an experiment is the expected payoff under the best of the four rules. An experiment is optimal if it lies in and no experiment in has a larger value.
The paper states Proposition 1 as "the firm optimally chooses the w-biased experiment" if and the n-biased one if , and adds that, "for all but a degenerate case, these are the only two experiments that will be optimally chosen". The goal records both: the biased experiment is optimal over , and it is the unique optimum. The degenerate case is excluded, as in the paper.
The result. Proposition 1 says that a firm predisposed to exploit designs its test so that only a conclusive "no" can change its mind, and a firm predisposed not to exploit designs it so that only a conclusive "yes" can. The rest of the paper applies it with firm-specific payoffs: an incumbent, whose status quo is valuable, has a higher threshold than an entrant (Proposition 2), and this difference drives the paper's account of why incumbents and entrants experiment differently with disruptive technologies (Propositions 3–5). Without Proposition 1 none of these comparisons is defined.
Formalizing it. The result is proved in the paper (§7.1, p. 31), but the proof covers only the comparison between the two biased experiments; the claim that no other experiment is optimal is argued graphically from Figure 1, and the proof leaves the case to "the same way". The mission produces a machine-checked proof of the full statement over , with uniqueness. To our knowledge no part of it has been formalized before.
The obvious argument compares along the frontier of with the slope of the indifference curves. That argument fixes the decision rule "exploit iff ", while the firm's value is the best of four rules: for priors far above the firm exploits after both signals of , and the comparison then changes form (the two cases of the proof on p. 31). A proof over must handle the maximum of four piecewise-linear functions of and show that it is uniquely maximised at one vertex. The printed slope expression on p. 13 also has its axes interchanged relative to Figure 1, so it cannot be transcribed as it stands.
All quantities are real numbers. States and signals are Bool; a decision rule is a function Bool → Bool; the value of an experiment is Finset.sup' of the expected payoff over the four rules, so the firm's post-signal choice is optimal by construction. Joint probabilities are prior times Table 1 entry; posteriors use real division and are stated only for signals of positive probability. Two hypotheses are added to the paper's and recorded in the definitions: (at the biased experiments tie) and (otherwise is empty and ). Optimality is maximisation over , and experiments are equal when both precisions are equal.
Defining the value as the payoff of the single rule "exploit iff " (the display ) would trivialize the goal into milestone 6 and is ruled out: the value is always the best rule. Comparing only and is milestone 5, not the goal.
The development needs only finite sums and elementary real inequalities; no probability library is required. Contributions of proofs of any milestone, and of alternative proofs of the goal, are welcome.