Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In the secretary problem candidates arrive one at a time in uniformly random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones and must accept or reject irrevocably, aiming to accept the best candidate overall. Dütting, Lattanzi, Paes Leme and Vassilvitskii, Secretaries with Advice (arXiv:2011.06726), study a family of variants in which each candidate also carries a signal about its quality, and show that for many of them the optimal stopping rule is the solution of a finite factor-revealing linear program whose dual can be solved greedily by backward induction.
One of their main examples is the secretary problem with samples: before the candidates arrive, further elements of the same random order are revealed as a sample, and a candidate's signal is the number of sample elements smaller than it. This model interpolates between the classical problem (, optimal success probability tending to ) and, as , the full-information problem of Gilbert and Mosteller (1966). The paper's Theorem 17 gives the optimal dual solution of this LP in closed form.
Fix natural numbers (secretaries) and (samples). Rounds are ; signals are . The dual LP of §5 has the coefficients
with for , and reads
The greedy solution (equation (8) of the paper) sets and, going backwards,
The un-clipped recursion is the same backward induction with the removed. In Lean, the generic recursion (8) is greedyDual (and unclippedDual) over an arbitrary finite signal type, and the samples instance is samplesGreedy n k i s (resp. samplesUnclipped) with s : Fin (k + 1). Products with equal .
For every and : , and for
Theorem 16 of the paper shows that the greedy dual solution is optimal and that the optimal policy for secretaries with samples is a threshold policy in the signal: accept a best-so-far candidate in round iff its signal is large enough. Theorem 17 makes this solution explicit, so the optimal thresholds can be read off from the sign of a closed-form expression rather than computed by running the backward recursion, and it is the discrete precursor of the paper's Corollary 18, which recovers the Gilbert–Mosteller full-information thresholds in the limit .
The identities are proved in the paper by explicit manipulation of finite sums and products of binomials. No machine-checked version exists. A formal proof checks the long index computations of the proof and of Appendix B, and closes a gap: the paper proves the identity for the un-clipped recursion only ("for the proof we can ignore the ") and does not argue why the clipped greedy solution has the same form. The goal as stated here, with the maximum, is the statement the paper asserts.
The identities are rational-function identities in , and the round indices, with sums whose ranges depend on the summation variables and products whose ranges may be empty. The natural first idea, induction on directly on the formula, requires the key identity for , a double sum over and of products of rising factorials; the paper handles it by a second backward induction over , and both the base case and the step re-index sums with shifted bounds and boundary terms such as and .
The passage from the un-clipped to the clipped recursion is a separate difficulty: once is clipped to at a later round, the sums used at earlier rounds differ from those of the un-clipped recursion, and the closed form survives only because the clipped entries do not affect the relevant sums. That argument is not in the paper.
Fin (k + 1) in the recursion and naturals in the formulas. All arithmetic is in ; naturals are cast before , and the natural differences , , appear only where the ranges keep them non-truncated.Finset.Icc a b, empty when , matching the paper's convention.greedyDual is reusable for any instance of the paper's factor-revealing LP (the binary-classifier model of §6 included). General lemmas about sums of rising factorials (ascPochhammer) and binomial re-indexing developed for the milestones are welcome contributions.The European Union's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers privacy rights over the personal data that firms collect: data may be collected only with explicit consent (opt-in), consent is separated from the purchase itself, and a consumer may later have her data deleted (erasure, the "right to be forgotten"). The same regulations carry a data security mandate, because data held by a firm is exposed to breaches. Regulators, firms and economists want to know how these rights change what data is collected, what prices are charged, and who gains.
Ke and Sudhir (SSRN 3643979; published in Management Science, 2022, doi:10.1287/mnsc.2022.4614) build a two-period model in which a firm sells a basic good, may collect a consumer's data with her consent, and uses the data to sell a personalized good in the second period. Consumers trade off the personalization benefit against the expected cost of a data breach. This mission formalizes the paper's first main result, Proposition 1: the equilibrium of the monopoly market with privacy rights. The companion mission (number 2 of this series) formalizes the benchmark without privacy rights.
A monopolist faces a unit mass of consumers whose valuation of the basic good is uniform on . A consumer values the personalized good at , where with probability each and . Write
A consumer learns her only after the first period, and the firm never learns it. Both sides discount the second period by . Each period in which the firm holds a consumer's data costs her an expected breach cost .
Period 1. The firm posts a price . Each consumer chooses among not buying, buying without opting in, and buying and opting in. Opting in reveals to the firm and costs .
Period 2. The firm posts a basic price and offers each opted-in consumer a personalized price . A consumer who did not opt in buys the basic good iff ; she never opts in in the last period. An opted-in consumer either keeps her data and buys the personalized good, with utility , or erases her data and takes .
An equilibrium is a profile in which every personalized price maximizes the expected revenue from consumer at basic price ; after every first-period price , the basic price maximizes the firm's second-period profit; after every , every consumer's first-period action is optimal; and maximizes the firm's total profit over all real prices. The paper also imposes Assumption 1:
Under Assumption 1, an equilibrium exists with the following outcome in each regime. The constants and are those of the paper's appendix.
The equilibrium personalized price, eqs. (1)–(2):
which is optimal whenever , a condition Assumption 1 guarantees above the opt-in threshold.
The opt-in threshold, eq. (4):
The second-period basic price, eq. (3): if , and otherwise.
The remaining milestones are the identification of the firm's profit with the reduced first-period profit of p. 15, and the three cases of the appendix proof that locate its maximizer.
Proposition 1 is the basis of the paper's comparative statics and policy conclusions. The comparison with the benchmark (Proposition 2) shows when privacy rights raise or lower opt-in, profits and consumer surplus. Corollary 3 shows that under privacy rights, opt-in and profit fall strictly with the breach cost. In the paper's interpretation, the result explains how data-security investment and the rights themselves interact: privacy rights let consumers avoid the hold-up problem of sharing data before knowing its value to them.
The result is proved on paper in the appendix, by reducing the game to a piecewise-quadratic maximization. It has not been machine-checked. A formal proof adds a fully specified equilibrium concept with optimality at every history and an explicit treatment of tie-breaking and knife-edge regimes. It also corrects one misprint in the SSRN text (the price in case B(i)). This is the platform's first two-period data-market game with opt-in and erasure; existing privacy items are one-shot models.
The difficulty is that the goal is a statement about a game, not about the closed forms. A solver must exhibit strategies at every history, including first-period prices far from equilibrium and arbitrary basic prices. They must then show that the consumers' choices form a threshold set whose measure and integrals are the ones the reduced profit assumes.
The tempting shortcut is to read eq. (2) as the firm's personalized price everywhere. Eq. (1) shows it is optimal only in case (i); for small the firm prefers to price only to the high type or to let both types erase. The equilibrium survives because no such consumer opts in, which must be shown from the consumers' side. The global maximization of the first-period profit over all real involves a function with kinks at , at the price where , and where reaches . Both halves of Assumption 1 are used in comparing its pieces.
Parameters are a structure Params with fields kL, kH, d () and c; , , the standing assumptions (, , ) and Assumption 1 are definitions, and every theorem carries both predicates as hypotheses. Consumers are with Lebesgue measure. Expectations over are averages of the two types. All quantities are real numbers, and prices range over all of .
Committed conventions:
Profits are integrals over the sets of consumers defined by the profile's own choices. A formalization that defined profits by the paper's closed forms would be trivial and is excluded. So are optimality checked only on the equilibrium path, a dropped Assumption 1, a missing bullet of the proposition, and a uniqueness claim. A sorry-free check confirms that the hypotheses are satisfiable at the paper's figure point , , .
The development needs interval integrals and Lebesgue measure of intervals on , and elementary real inequalities with square roots. The reduced-profit identity (consumers' optimal choices form threshold sets up to null sets) is the reusable core and would serve the benchmark mission too. Proofs of individual milestones are welcome independently.
A permissioned blockchain is a shared ledger that only invited parties may write to. In supply chains it is promoted as a way to make the provenance and quality of goods verifiable by the end consumer: a manufacturer who joins records how a good was produced, and consumers can read that record. Joining is costly, and the parties who pay the cost are not the parties who benefit most from the information. Whether such a technology is adopted at all is therefore a question about incentives, not engineering.
G. Iyengar, F. Saleh, J. Sethuraman and W. Wang, Economics of Permissioned Blockchain Adoption (SSRN 3602376; Management Science, 2023, DOI 10.1287/mnsc.2022.4532), build a stylised supply chain with vendors, price-competing manufacturers and consumers with an outside option, and show that welfare-improving adoption can fail to arise in equilibrium. This mission formalizes the first of the paper's two main results, Proposition 4.8, together with the welfare comparisons it rests on. A companion mission formalizes the second, the self-financing transfers of Proposition 4.9.
There are two vendors, of high and low quality , and a set of manufacturers, of each type . A consumer of horizontal type obtains utility from a good with and otherwise, plus the vertical utility ; here , and measures horizontal differentiation. Consumers can always take an outside option , drawn from a continuous distribution supported on . The high type vendor produces at cost , ; the low type vendor at a strictly increasing convex cost with and strictly increasing derivative (Assumption 1, items 1–2).
Manufacturer may join the blockchain at cost () or not (). Three scenarios are compared: full adoption (all adopt), partial adoption (exactly the high type manufacturers adopt) and non-adoption . The paper's Proposition A.1 gives each scenario's equilibrium in closed form: every consumer's best manufacturer offers utility
the low type vendor price is , , (the high type price is always ), the low type market shares are , , , and . Manufacturers earn zero gross profit in every scenario because of price competition.
Welfare in scenario is the sum of vendor welfare (revenue minus production cost of both vendors, (10)), manufacturer welfare and consumer welfare ((12)). The adoption game (8) lets each manufacturer choose to maximise . An adoption failure is a situation in which full adoption raises total welfare, , but is not an equilibrium of the adoption game.
With fixed and ,
at every such at which Assumption 1 holds. The threshold is left unspecified, as in the paper.
The proposition isolates a mechanism: blockchain information raises consumer surplus, which grows without bound in , while Bertrand competition prevents the manufacturers who pay for adoption from capturing any of it. The conclusion is a market failure that persists however valuable the information is, and it motivates the paper's transfer scheme (Proposition 4.9), in which a consumer access fee finances the adopters. The welfare comparisons of Propositions 4.1–4.6 are reusable on their own: they quantify who gains and who loses from information disclosure in a vertically and horizontally differentiated market.
The results are proved in the paper (App. A.2, pp. 33–36). None is machine-checked. This mission produces a checked version of the welfare comparisons and of the failure result in the reduced form described below; the proofs as printed use a density for and a second derivative of , neither of which the model assumes, so a formal proof has to avoid both.
The equilibrium part is light once the gross profit is zero. The substance is in the welfare comparisons. Consumer welfare is an expectation of an outside option with an arbitrary continuous law: strict monotonicity in needs positive mass of below , which is a consequence of Assumption 1 rather than an assumption, and the growth in of has to be bounded below without a density. Vendor welfare involves the generalised inverse , which is below : the comparison must handle the regime where the low type vendor's share collapses to zero and the regime where it is interior, and must obtain continuity of from convexity rather than from a second derivative.
The paper describes a signalling and pricing game but does not define its equilibrium concept precisely; Proposition A.1 states the outcomes and every proof in App. A.2 uses only those closed forms. The mission adopts the same reduced form, disclosed in every item: welfare is evaluated at Proposition A.1's prices, shares and utilities; the manufacturers' gross profit is the constant for every adoption profile (the paper's statement in the proof of Proposition 4.3, p. 34); an equilibrium of the adoption stage is a pure Nash equilibrium of (8) with that payoff, expressed with AGT.IsPureNash from the published agt_games vocabulary. The signal accuracy is fixed at , as in the paper's main text.
Conventions: manufacturers are Fin 2 × Bool × Fin m (the Boolean records ), adoption profiles are Boolean functions, is ProbabilityTheory.cdf μ for a probability measure on , is an argument of every statement with , and . The standing assumptions are bundled in Model.Standing: , , , , , an atomless probability measure with and positive mass on every interval , strictly increasing and convex on with and a strictly increasing derivative there. One hypothesis is added to the paper's: has a finite mean, which the paper uses (its proof of Proposition 4.1 integrates ) without stating it. Assumption 1, item 3, depends on through and is a hypothesis at each ; it is satisfiable (for instance with , , , , , ) and monotone in .
The formalization rules out the trivializing readings: the equilibrium predicate is concrete, not an abstract hypothesis; the integrals are of integrable functions, so no junk value enters; the inverse of is the explicit supremum, not Function.invFun; and , not , is held fixed as grows.
Needed infrastructure: expectations of as a function of (monotonicity, growth), and the generalised inverse of a strictly increasing derivative of a convex function. Both are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the density and the second derivative of the printed proofs.
Many transactions are priced by negotiation rather than posted prices: business-to-business procurement, used cars, real estate, the purchase of a company. Before negotiating, a buyer can often spend effort finding out how much the object is actually worth to it, through inspections, trials, consultants or market research. That information serves two purposes. It improves the joint decision of whether to trade at all, and it changes how the surplus of trade is split. Liang Guo's Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360) studies how a buyer's endogenous information acquisition interacts with the two primitives of bargaining: the parties' bargaining powers and the seller's cost.
The first finding of the paper, Proposition 1, concerns how much information the buyer gathers. Its comparative statics in the seller's cost are non-monotone, and this non-monotonicity drives the later results of the paper, in which a seller can be worse off with more bargaining power or a lower cost. This mission formalizes Proposition 1 in its general form, for an arbitrary prior. A companion mission (Gathering Information before Negotiation II) formalizes the payoff reversals under a uniform prior and a linear information cost.
A seller can supply one unit of a product at cost . A buyer's true value of the unit is unknown to both parties; the common prior law of is , with a finite mean .
Before negotiating, the buyer acquires a truth-or-noise signal : with probability the signal equals , and with probability it is an independent draw from . Because the parties are risk neutral, only the buyer's posterior mean
matters. Ex ante, has the distribution function
The buyer chooses the informativeness in an interval at a cost that is increasing, with and .
After observing , the parties trade exactly when and split the net surplus according to their bargaining powers , . Anticipating this, the buyer chooses to solve
where is the total ex ante surplus (7). A solution of (6) is written ; in general there may be several, and denotes the set of all of them.
Two sets are compared in the induced set order when and for all , .
Whenever the optimal sets compared are nonempty,
The buyer's optimal information acquisition increases with its bargaining power, and first increases and then decreases with the seller's cost, turning at the prior mean .
The result. The first part of Proposition 1 says that a buyer with more bargaining power gathers more information, because it captures a larger share of the surplus that information creates. The second part is the less expected one: a higher seller cost shrinks the gains from trade, yet it raises the buyer's incentive to become informed as long as the cost is below the prior mean , and lowers it only beyond. Information is most valuable when trade is a close call. The paper's later results (Corollary 1, Propositions 2 and 3) build on this: since information acquisition responds to and , the seller's equilibrium payoff need not increase in its own bargaining power or decrease in its cost. The paper also notes (p. 11) that the monotonicity in needs only that a higher is a mean-preserving spread, which is why the statement is posed here for every prior with finite mean.
Formalizing it. The proposition is proved in the paper, in a short appendix argument that differentiates under the integral and appeals to Topkis's theorem. To our knowledge it has not been machine-checked. The mission produces a density-free formalization: the rotation property and the mean-preserving-spread property of the truth-or-noise family, the integration-by-parts identity for the expected positive part, and the two increasing-differences statements, which together with the already formalized Topkis theorem give the goal.
The paper's argument is first-order: it computes cross-partial derivatives such as and reads off their signs. Without a density these derivatives need not exist, and the information cost is assumed only increasing, so need not be differentiable, concave or even continuous in . The statements here are therefore in difference form, and the cross effects must be established as inequalities between integrals over different distributions of .
The second obstacle is the shape of the comparative statics. Topkis's theorem gives a monotone optimal set in the induced set order on a parameter range where increasing differences hold, but the cost has increasing differences only on and decreasing differences on . The referenced platform theorem, by contrast, asks for increasing differences on the whole product of the decision and parameter spaces, so it does not apply to as it stands.
The obvious shortcut of picking a selection from the optimal set and proving it monotone does not work: the cross differences are only weakly positive (they vanish when lies outside the support of ), so the strict version of Topkis's theorem does not apply, and two different maximizers need not be ordered.
The prior is a probability measure on with integrable identity and positive mean . The paper's additional assumptions on (continuous and differentiable, strictly positive density on a bounded support ) and are dropped: every statement is posed for all priors with finite mean and all real , which implies the paper's case. is ProbabilityTheory.cdf μ, and is defined from it by the page's formula. The interval satisfies ; is monotone on it with ; in every statement.
The total ex ante surplus is defined as , which is (7) after the change of variables . The bargaining stage is not modelled; the paper's reduction to (6) is built into . The optimal level is the set of maximizers of over (optSet), never a chosen element. "Increases" is the induced set order, and every comparison assumes both optimal sets nonempty, which is the paper's presumption that (6) has a solution.
Trivializing formalizations are ruled out: is never given by a closed form or by the integration-by-parts expression (that identity is a milestone), is never defined by a formula or a threshold rule, and the nonemptiness hypotheses prevent the induced set order from holding vacuously on an empty optimal set.
The development reuses the platform definitions Supermodularity.Lattices.InducedSetOrder and Supermodularity.Monotonicity.IncreasingDifferencesOn and the proved theorem Supermodularity.Monotonicity.argmax_increasing_of_increasing_differences. The rotation and mean-preserving-spread lemmas for truth-or-noise signals, and the tail-integral identity for integrable , are reusable beyond this mission. Contributions of any of the milestones, of alternative proofs that avoid the integration by parts, and of the strict versions under the paper's density assumption are welcome.
Not posed in this mission: the benchmark (3)–(5), Corollary 1, Propositions 2–7, and the extensions of §4–§5.
In many trades the buyer does not know how much the good is worth to it, and can find out before negotiating: a firm commissions due diligence before an acquisition, a hospital pilots a device before negotiating its price, a household inspects a house before making an offer. Such information has two effects. It makes the trade decision better informed, which enlarges the total surplus, and it is paid for by the buyer alone, while the surplus it creates is shared through bargaining.
L. Guo, Gathering Information before Negotiation (SSRN 3930651; Management Science, doi:10.1287/mnsc.2022.4360), studies how this interaction shapes the seller's payoff. Its headline is a reversal: a seller with more bargaining power, or with a more valuable outside option, can be worse off, and a seller with a higher production cost can be better off. The reason is that the buyer's information choice reacts to these parameters, and the reaction can outweigh their direct effect. This mission formalizes that reversal for the paper's worked example, the uniform prior with a linear information cost.
A seller and a buyer negotiate over one unit of a good. The seller's cost is . The buyer's value is unknown to both parties; the common prior is the uniform distribution on , with mean . The bargaining powers are for the buyer and for the seller.
Before negotiating, the buyer chooses an informativeness , with . It then observes a truth-or-noise signal : with probability it equals , and otherwise it is an independent draw from the prior. The buyer's posterior mean is . The information cost is linear,
If the parties trade and split the net surplus in the proportions ; otherwise they do not trade. The total ex ante surplus is
and the buyer chooses to maximise
The optimal set is the set of maximisers of on . The seller's equilibrium expected payoff is
Write for the surplus gain of maximal information, and when , otherwise. For fixed , the cost thresholds are the endpoints of the set of costs at which .
For every selection of optimal information levels:
A drop at means: for some , every value just to the right of is strictly below every value just to the left.
the uniform display of p. 13. The proof of Corollary 1 (p. 30) then contributes three steps: is constant and then increasing, and convex; the optimum is a corner, ; and vanishes for extreme costs, rises and then falls in , and peaks at . Corollary 1 (p. 13) gives the two threshold rules: (i) for and for ; (ii) exactly for .
The result. Without information acquisition, the seller's payoff is increasing in its bargaining power and in its outside option and decreasing in its material cost: these are the direct effects. Proposition 2 shows that each of them can be reversed by a discontinuous jump. The mechanism is that the buyer stops gathering information when its own share of the surplus becomes too small (high ) or the trade decision becomes clear-cut (extreme ). The result bears on when a seller should prefer to commit to a weaker bargaining position, and on why cost increases need not hurt a seller facing an uninformed buyer.
Formalizing it. The paper calls Proposition 2 an immediate consequence of Corollary 1. That corollary rests on a short appendix argument whose printed version contains slips: the peak of is printed as , strictness is claimed on a closed interval at whose endpoints , and "" fails at when the two corners tie. A machine-checked development settles exactly which form of each claim is true. The result has been proved informally in the paper; it has not been formalized before.
The obvious argument treats as a function and differentiates . That does not work here. At the thresholds is not single-valued, and between them it is constant, so the whole content lies in the jumps. A jump statement must hold whichever optimal level is selected at each parameter, and it must compare values on both sides of a threshold whose location depends on . Showing that the thresholds are well placed requires the inverted-U shape of , which comes from an explicit but piecewise integral. The corner property needs convexity of across the kink at , where the two branches of the closed form meet.
All quantities are real numbers. is the interval integral over the uniform prior after the change of variables ; no density is assumed. The bargaining stage is not modelled; the payoffs are the paper's reduced forms (6) and . Conventions: (the paper's ); with ; non-degenerate; when , which avoids and keeps . Monotonicity is claimed on each side of the jump point, open at that point (and across the other cost threshold), and the jump whenever the threshold is interior. In (ii) and (iii), are assumed to satisfy " iff " for all , which determines them; when the buyer never gathers information this forces .
The paper states Corollary 1 and Proposition 2 for four focal priors (uniform, exponential, logistic, modified Pareto) but works out only the uniform one. This mission is pinned to the uniform prior and the linear cost.
A trivializing formalization is ruled out: is not defined by its closed form (that closed form is a milestone), is the set of maximisers of and not a threshold rule, and the goal quantifies over every selection from that set, so neither Corollary 1 nor Proposition 2 holds by definition.
A complete development needs piecewise interval integrals of , convexity of a function with a junction, and the fact that a convex function on a segment attains its maximum at an endpoint. All of these are general facts, reusable beyond this mission. Proofs of the milestones in any order are welcome; Proposition 3 and the other priors are not posed here.
Category: Textbook
Review status: This is a private draft revision for the owner's review. The existing published SortIndicesAnalysis.call is marked Proved on Prove2Me. The new headline theorem is a separate draft derived from that contract; its proof remains local. The reused proof library and the new correctness-and-runtime wrapper compile locally with Lean 4.33.1; their axiom checks contain no sorryAx. The new proof has not been submitted to Prove2Me. No public submission or publication is authorized by this revision.
This mission belongs to the CLRS fourth-edition formalization series. It presents sorting through an indexed binary min-priority queue, using the heap representation and heap-order ideas of Chapter 6, §§6.1–6.2, and priority-queue operations of §6.5.
It reuses Lunjia Hu's published .algo implementation, definitions, and correctness-and-cost call contract unchanged. The program inserts identifiers with their keys and then repeatedly extracts the minimum. The result is a fresh sequence of sorted identifiers; the original keys remain unchanged. Equal keys may occur in either order.
This implementation differs from the in-place max-heap HEAPSORT of §6.4: it allocates auxiliary sequences and constructs the heap by repeated insertion. Accordingly, this draft targets an sorting bound. Constant extra space, linear-time bottom-up construction, stability, and a matching worst-case lower bound are outside this theorem's claims.
For every initial heap, every allocated key-sequence reference, and every natural length , the source-facing sort_indices.Call terminates with a final heap and a fresh allocated result reference. Its first entries are a permutation of , ordered by the corresponding original keys. Previously allocated caller sequences and objects, and all collections, are preserved. The output outside this prefix is unspecified.
Negative integer keys, duplicate keys, and are included. The key reference must be allocated even for the empty case. The sequence model is total on integer indices; specifies the finite input prefix. Integers are mathematical, unbounded integers.
The headline theorem retains the existing per-clock Budget n (2n) for the same completed call and adds a uniform asymptotic statement. There is a positive natural constant , chosen independently of the heap, keys, length, and initial counters, such that
Here is the sum of the increments of sort_steps, heap_comparisons, and heap_swaps. Each clock may start at an arbitrary value. If , the existing contract bounds these increments by , , and respectively. It therefore retains the reusable explicit bound
The clocks count the source's marked sorting-loop iterations, heap comparisons, and heap swaps. They do not count every arithmetic operation, array access, allocation, or compiler transition, and do not measure integer bit complexity, Lean checking time, or elapsed machine time. For the empty input the named event count can be zero although initialization and allocation still occur.
The single supporting milestone is the existing, proved SortIndicesAnalysis.call. It combines termination, sorted-permutation correctness, preservation, freshness, and per-clock budgets. Its implementation reuses the published indexed-heap insertion and minimum-extraction contracts.
The new headline is CLRS.HeapSortIndices.correctness_and_running_time. It imports that established call theorem and derives a uniform asymptotic consequence without repeating the heap correctness proof. Clients can apply the same call contract with their actual initial heap and counters, obtain sorted identifiers, and continue with the resulting heap. No new copy of the heap or runtime definitions is required.
The checked proof of the new headline is retained locally for review. A draft theorem statement may display a sorry placeholder; that placeholder is not an accepted proof or a Prove2Me verification result. An independent read-back of the formal statement is included in the local review package.
The following files are reproduced unchanged from Lunjia Hu's public v0.1.4 source. Project import root: examples/kruskal. Entry file: sort_indices.algo.
indexed_heap.algo# An indexed binary min-heap for Dijkstra's priority queue.
# vertices[position] and positions[vertex] are inverse on the active prefix.
# keys is indexed by vertex; position -1 means the vertex is not in the heap.
# Clients use nonnegative vertex identifiers, so pop_min can use -1 for empty.
class MinHeap:
vertices: Seq
positions: Seq
keys: Seq
size: Int
def __init__(self) -> None:
self.vertices = const(0)
self.positions = const(-1)
self.keys = const(0)
self.size = 0
def swap(self, i: Int, j: Int) -> None:
a = self.vertices[i]
b = self.vertices[j]
# @exchange
self.vertices[i] = b
self.vertices[j] = a
self.positions[a] = j
self.positions[b] = i
tick("heap_swaps")
def sift_up(self, i: Int) -> None:
# @up_loop
while i > 0:
parent = (i - 1) // 2
tick("heap_comparisons")
if self.keys[self.vertices[parent]] <= self.keys[self.vertices[i]]:
return
self.swap(i, parent)
i = parent
def sift_down(self, i: Int) -> None:
# @down_loop
while 2 * i + 1 < self.size:
child = 2 * i + 1
right = child + 1
if right < self.size:
tick("heap_comparisons")
if self.keys[self.vertices[right]] < self.keys[self.vertices[child]]:
child = right
# @compare_child
tick("heap_comparisons")
if self.keys[self.vertices[i]] <= self.keys[self.vertices[child]]:
return
self.swap(i, child)
i = child
def push_or_decrease(self, vertex: Int, key: Int) -> None:
i = self.positions[vertex]
if i < 0:
self.keys[vertex] = key
i = self.size
self.vertices[i] = vertex
self.positions[vertex] = i
self.size += 1
self.sift_up(i)
else:
tick("heap_comparisons")
if key < self.keys[vertex]:
self.keys[vertex] = key
self.sift_up(i)
def pop_min(self) -> Int:
if self.size <= 0:
return -1
vertex = self.vertices[0]
last = self.size - 1
self.swap(0, last)
self.size = last
self.positions[vertex] = -1
if last > 0:
self.sift_down(0)
return vertex
def is_empty(self) -> Bool:
return self.size <= 0
sort_indices.algo# Order the identifiers [0, count) by their keys using a reusable binary heap.
# This supplies Kruskal's sort-by-weight step: insert every identifier, then
# extract minima. It is not the in-place HEAPSORT procedure from CLRS Chapter 6.
# Only identifiers are reordered; keys are unchanged. Equal-key identifiers
# may appear in either order.
from indexed_heap import MinHeap
def sort_indices(keys: Seq, count: Int) -> Seq:
queue = MinHeap()
result = const(0)
index = 0
# @insert
while index < count:
tick("sort_steps")
queue.push_or_decrease(index, keys[index])
index += 1
index = 0
# @extract
while index < count:
tick("sort_steps")
result[index] = queue.pop_min()
index += 1
return result
The compiler is Algo2Lean, numbered release v0.1.4, public source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, with Lean 4.33.1. Generation uses project mode, the two source files above, entry sort_indices.algo, generated namespace Algo.«sort_indices», and standalone=false.
The hosted compiler archive was downloaded and verified against its release manifest and checksums. All 196 payload files agree with the pinned public source. Generation under that archive's native Python bridge and its released Pyodide 314.0.7 runtime produces identical bytes for all six generated modules and two shared libraries. The release archive and source identities were recorded separately.
The corresponding Prove2Me modules match those raw outputs after two recorded packaging adaptations: rewriting project/runtime imports to Definitions.Def_*, and adding the platform's autoImplicit/backward-definitional-equality option prelude. All remaining bytes, including declaration bodies, are unchanged. The compiler archive SHA-256 is 52b3978479b4f4cc473e11471d839c6c96aafe0ffc73bbeeea4e785228f4fdf0.
Separately, all 18 modules in the published proof dependency closure have been checked locally with Lean 4.33.1 using the accepted proof bodies. To combine separately submitted proof files locally, non-target helper declarations are made private and final solution declarations receive unique audit names; theorem statements and proof bodies are retained, and the named targets are checked against their published types. This local proof packaging is distinct from the generated-code import adaptation above. The axiom audit found only propext, Classical.choice, and Quot.sound, with no sorryAx in the reused results.
These reproduction checks establish generation and packaging correspondence. Lean proof checking is a separate check; neither establishes a proof of compiler correctness.
Algorithm implementation and reused heap/sorting proofs: Lunjia Hu. This draft presents their reusable sorting contract in the CLRS series and adds the uniform-bound wrapper. The source and proof attribution are retained.
An error-correcting code stores or transmits messages as words over a finite alphabet, adding redundancy so that the original word can be recovered after some symbols are corrupted. The basic question of coding theory is the trade-off between the amount of redundancy and the number of errors that can be corrected. The Hamming bound (also called the sphere-packing bound) is the first and most widely taught upper limit on this trade-off. It is due to R. W. Hamming (1950), who introduced the Hamming distance and the Hamming codes in the same paper (Hamming 1950).
This mission formalizes the bound as it is stated in Theorem 1.7.2 of the textbook Essential Coding Theory by V. Guruswami, A. Rudra and M. Sudan (web draft, §1.7, p. 21). It is the first mission of a series following that book. The result is used throughout the book to define perfect codes (Definition 1.7.3) and as the baseline against which later bounds (Singleton, Plotkin, Elias–Bassalygo, the linear-programming bound) are compared.
Let be a finite alphabet with symbols, and let . A word of length is a function , and is the set of all words. A code of block length is a subset ; its elements are codewords.
The Hamming distance between two words is the number of coordinates in which they differ. The dimension of is the real number (Definition 1.2.3 of the book). The book calls an code when its minimum distance equals (Definitions 1.4.1 and 1.7.1).
The Hamming ball of radius around a word is (Definition 1.6.1).
For every word and every radius ,
This is equation (1.18) in the book.
If any two distinct codewords of are at Hamming distance at least , then
The hypothesis is "minimum distance at least " rather than "exactly ". Every code satisfies it, so the goal contains the book's Theorem 1.7.2 as stated.
The result itself. The bound says that a code correcting errors can have at most codewords, so its rate is at most . Codes meeting it with equality are the perfect codes: the Hamming codes, the binary repetition codes of odd length, and the two Golay codes. The bound's asymptotic form, , is one of the standard upper bounds on the rate–distance trade-off and is the reference point for the stronger bounds later in the book.
Formalizing it. The theorem has been proved since 1950 and appears in every coding theory text. Mathlib has the Hamming distance (hammingDist) but no notion of a code's distance, no Hamming-ball cardinality formula, and no sphere-packing bound. This mission supplies those, with the dimension stated through the real logarithm exactly as in the book, so later missions in the series can cite it.
The mathematics is elementary. The work lies in the counting step: showing that exactly words lie at distance exactly from a fixed word. This identity has no ready-made counterpart in Mathlib, and the alphabet carries no algebraic structure, so translating every ball to a ball around a fixed word is not available. The final step, taking of both sides, must also handle the conventions of the real logarithm on degenerate inputs.
α with [Fintype α] [DecidableEq α], and is Fintype.card α. Words are functions Fin n → α, and is Mathlib's hammingDist.Finset (Fin n → α). The distance hypothesis quantifies over pairs of distinct codewords.Real.logb q |C|, a real number. The ball volume is the natural-number sum , cast to , where is computed in as (d - 1) / 2.hammingDist, Mathlib.InformationTheory.Hamming. https://leanprover-community.github.io/mathlib4_docs/Mathlib/InformationTheory/Hamming.htmlStochastic matching with patience models kidney exchange, online dating and labour platforms: every edge of a graph is present only with some probability, the only way to learn whether it is present is to probe it, and a probed edge that turns out to be present must be added to the matching. Each vertex also has a patience , a limit on how many of its edges may be probed. The goal is a probing strategy whose expected matched weight is a large fraction of what the best adaptive strategy obtains. Since the best strategy is hard to compute, algorithms are compared with the value of a linear program (LP (3) below), which upper-bounds every probing strategy (Bansal, Gupta, Li, Mestre, Nagarajan, Rudra, Algorithmica 2012).
Bansal et al. gave a -approximation for stochastic bipartite matching. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892v3) single out the case in which one side of the bipartition has unit patience, for every . This case contains "Problem A" of Hikima et al. (AAAI 2021), whose approximation ratio transfers to their integrated two-stage problem ISPCB; Hikima et al. obtained from the bound of Bansal et al. For the special case in which one side has arbitrary patience and the other unlimited patience, Borodin and MacRury had already obtained the same guarantee through an online problem.
Let be a finite bipartite graph; denotes the set of edges at a vertex . Each edge has a weight and an activation probability , independently across edges. Every has patience ; every has a patience .
LP (3). A vector is feasible when and, for every vertex ,
Write and .
The algorithm. A dependent rounding (Gandhi, Khuller, Parthasarathy, Srinivasan, J. ACM 2006) turns into a random set of rounded edges with , at most one rounded edge at each , at most at each , and the negative correlation property (2): for , and ,
In the rounded graph every is the centre of a star. Each probes its rounded edges in decreasing order of weight and is matched to the first active one; is the weight of that edge ( if none), and .
For every feasible , every rounding with the properties above and every decreasing-weight probing order,
The paper's proofs are in §4, pp. 16–19.
Combined with the LP upper bound (Lemma 1 of the paper, from Bansal et al.), Theorem 2 is a -approximation for stochastic matching on bipartite graphs with a unit-patience side, improving and generalizing the guarantee of Hikima et al. for Problem A and, through their reduction, for ISPCB. By the paper's account (§1.1, p. 4), the guarantee rests on a new ingredient, a -balanced ordered contention resolution scheme for rank-1 matroids under negative correlation, in which the algorithm chooses the order: the per-star bound of Lemmas 7 and 9 holds for every rounding satisfying (2), not only for independent activations.
The result is proved in the paper; none of it has been machine-checked. This mission formalizes the per-star analysis and the theorem for an abstract rounding described by its properties, which is reusable for any algorithm that probes stars after a negatively correlated rounding.
If the rounded indicators at a vertex were independent, Lemma 7 would be an equality and the remaining work would be the deterministic inequality of Lemma 8. They are not: the rounding is dependent, and Example 1 (p. 19) shows that this dependence can raise the probability that a particular edge is blocked to , so that no correlation-agnostic contention resolution scheme is better than -balanced. A per-edge guarantee, of the kind a contention resolution scheme that ignores correlation provides, is therefore unavailable: the bound of Theorem 2 holds only for the total weight collected at each , and the negative correlation property (2) is one-sided, so it can be used only in the direction in which it holds.
Finset.sum_range_by_parts), and . Proofs of any milestone, and of the theorem from the milestones, are welcome.The Lightning Network (LN) is a layer-two payment system for Bitcoin. Two parties open a payment channel by locking funds on the blockchain and can then pay each other off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it has to carry. Guasoni, Huberman and Shikhelman (SSRN 4439190, version of February 3, 2023; published in Management Science, 2024) ask which network topologies support a given pattern of payments at least cost, using only qualitative properties of the channel cost derived in their earlier work on channel sizing (Guasoni, Huberman and Shikhelman, Lightning Network Economics: Channels, 2022, cited in the paper as [GHS22]).
One of the paper's central findings is that adding a new hub node, and routing the traffic of a group of nodes through it, reduces cost in a broad class of networks. This explains, from cost considerations alone, why hub-and-spoke structures emerge in deployed payment-channel networks. This mission formalizes the deterministic sufficient condition for that phenomenon (Theorem 3.8) and the chain of lemmas in Appendix B.1 that proves it.
Fix a finite set of nodes. A Lightning Network is an anti-symmetric real matrix : is the net flow from to in the channel between them, , and means there is no channel.
A channel cost is a function that is strictly increasing on (MO), even (SY), zero at zero (CI), and strictly subadditive, for (SA). It satisfies (SA+) with a nonnegative, strictly increasing on if for all , : when the flow of a channel grows -fold, its cost grows by at most . The cost of the network is .
For a node and a set of nodes, is the number of channels of into , the smallest and the largest absolute flow of these channels, the minimum degree, and the discrepancy, the maximum over nodes of with a channel in . For these are , , , , , and is the average degree.
The hermetization of deletes all channels among nodes of , adds a new node , and joins each to by a channel carrying , its net flow towards ; every node keeps its net flow. is hermetizable if hermetization strictly reduces the cost, and the network is hermetizable if some is.
Under (MO)–(SA+), every network with at least one channel and
is hermetizable. The cost function and are arbitrary subject to the axioms.
Theorem 3.8 turns a qualitative property of channel costs into a checkable topological criterion: if a network is dense relative to how unequal its channel flows are, a cost-reducing hub exists. The paper uses it to argue that such restructuring is profitable for an intermediary who charges part of the savings, and its probabilistic companion (Theorem 3.9) shows that random networks whose channel costs have light tails are hermetizable with high probability. The degree-to-subgraph Lemma B.4 is a standard tool of extremal graph theory (Diestel, Graph Theory, Prop. 1.2.2), and Lemma B.3 is the classical -core peeling.
Mathematically the result is proved in the paper. None of it is formalized: Lean's Mathlib has minimum degree and induced subgraphs but neither Lemma B.4 nor the correctness of -core peeling, and there is no formal model of payment-channel networks or of hermetization. The mission produces that model, machine-checked versions of the Appendix B.1 lemmas, and a statement of Theorem 3.8 under axioms that are actually satisfiable (see below).
The cost comparison in Lemma B.1 is node by node: the channels of a node inside are replaced by one channel to the hub carrying their sum. The obvious bound on the hub channel's cost uses only monotonicity and subadditivity, and that is too weak: a single channel carrying the sum of flows can cost almost as much as the channels it replaces, while the deleted channels are each shared by two nodes. The quantitative axiom (SA+) is what makes the comparison strict, and the discrepancy controls how unequal the replaced flows may be.
Passing from the average degree of the whole network to a subnetwork in which every node has high degree is the second step, and it must keep track of the fact that the discrepancy of an induced subnetwork can be smaller but never larger than that of the network. Lemma B.4 needs an argument that the deletion process cannot exhaust the graph; a counting argument that treats every deleted vertex alike loses exactly the margin needed.
Nodes form an arbitrary finite type V; the network is Λ : V → V → ℝ with anti-symmetry IsLN. The hub is the extra element none of Option V. The cost is the form. In Lemmas B.1 and B.2 all degree data are those of the subnetwork induced on ; in Theorem 3.8 those of the whole network. has the junk value for a node without channels, so every statement assumes the relevant nodes have a channel, and the discrepancy is a maximum over nodes having a channel.
Two axioms are corrected from the printed page and the correction is part of the statement. (SA) is printed for , which at reads ; it is stated for all , the form the paper's Appendix D verifies. (SA+) is printed for all , which fails at and, for the paper's own example cost, at every ; it is stated for , . Under the printed axioms every theorem would hold vacuously.
is strictly increasing but not assumed onto, so is replaced throughout by the equivalent -form: becomes , as in the paper's own proof of Lemma B.1. Theorem 3.8 therefore assumes and, explicitly, that the network has a channel (implied by the printed hypothesis). Lemma B.4 adds and reads "average degree " as "at least ", as its proof does. The polynomial-time clause of Theorem 3.8 and the bound of Lemma B.3 are complexity claims and are not formalized; Lemma B.3 is posed as correctness of the procedure in its proof, which finds minimum degree (the printed statement says ).
Formalizations that would trivialize the mission are excluded: a specific cost such as or a specific ; hermetizability defined by the per-node inequality instead of the cost comparison; Theorem 3.8 with the empty set allowed to witness hermetizability (the strict cost decrease rules it out); Lemma B.4 without nonemptiness; and Lemma B.3 as "there exists an algorithm".
The definitions (network, cost axioms, degree data, hermetization, peeling) are reusable by the companion missions on this paper. Proofs of any milestone are welcome, Lemma B.4 and Lemma B.3 being independent of the network model.
In inverse optimization, an observer sees decisions made by an expert who solves an optimization problem, and wants to recover the expert's unknown objective. Besbes, Fonseca and Lobel study a contextual version: in each period a feasible set and a context function are revealed, a learner must act before seeing the expert's choice, and then observes the expert's optimal action. The learner pays the expert's cost of its own action. This models, for example, a platform imitating a dispatcher's routing decisions or a recommender learning a user's trade-offs, where only optimal choices, not costs, are ever observed (Besbes, Fonseca, Lobel, arXiv:2106.14015).
For the one-period (offline) problem the paper shows that the circumcenter policy, which acts as if the unknown cost were the center of the smallest revolution cone containing the set of costs still consistent with the data, is minimax optimal (Theorem 1). The natural online policy is to apply it greedily in every period. This mission formalizes the paper's Theorem 2, which shows that this greedy policy can fail badly: its worst-case regret can grow linearly in the horizon, even when the initial uncertainty is small in a precise geometric sense.
Costs live in and actions in . The true cost lies on the unit sphere . An action set is a nonempty compact subset of of diameter at most ; a context function is a -Lipschitz map . The forward problem with cost has solution set
The angle between nonzero vectors is , set to if either vector is . The uncertainty angle of a set is
and a circumcenter is a unit vector attaining this infimum. A set is pointed when , i.e. it fits inside an open half-space cone.
Online protocol. In periods nature reveals and , the learner picks , and then an optimal expert action is revealed. Starting from a closed set , the knowledge set is
the regret is , and the worst-case regret is its supremum over and admissible instances. The greedy circumcenter policy chooses .
There is a closed, nonempty, pointed such that
Concretely: there are and such that for every horizon some and admissible admit a greedy run, and every greedy run (any circumcenter, any tie-break) has regret at least . The constant is left existential, as the page claims only .
The result separates offline from online learning in this model. Theorem 1 makes the circumcenter the best one-shot guess, yet Theorem 2 shows that one-shot optimality says nothing about information collection: a greedy learner can keep choosing actions that are wrong by a fixed margin while the revealed expert actions cut away only slivers of the knowledge set. This is the reason the paper introduces its EllipsoidalCones algorithm, which acts greedily on an enlarged ellipsoidal-cone superset and attains logarithmic regret for pointed initial sets. Theorem 2 is the lower bound that makes that design necessary.
On the formal side, the paper's proof is complete but compressed; it asserts the circumcenter of a three-generator spherical polygon "using Definition 2" and leaves the induction's geometric inclusions to the reader. A machine-checked version fixes the normalization of the circumcenter and the quantitative condition behind "", and gives a reusable formal treatment of uncertainty angles and circumcenters, which the paper's other results (Theorem 1, Theorem 3, Lemma 10) all use. No result of the paper has a formal statement or proof on Prove2Me yet.
The arithmetic of Step 3 is elementary once the knowledge sets are known. The difficulty is in Steps 1 and 2. Identifying the circumcenter of requires a minimax argument over the whole sphere: one must show that no other unit vector has a smaller maximal angle to the three extreme rays, and that the minimizer is unique, which rests on Lemma 2. The greedy policy is defined through this minimizer, so without uniqueness nothing can be said about its actions. Step 2 then needs an exact description of each knowledge set: showing that the new half-space makes the previous one redundant inside requires the sign information carried by the other constraints. A naive bound on the regret that ignores the knowledge-set dynamics fails, because a priori the policy might learn after a few periods.
Vectors are EuclideanSpace ℝ (Fin d), so norms, diameters and Lipschitz constants are Euclidean. The angle uses the paper's convention ; Mathlib's InnerProductGeometry.angle is not used. Action sets are required to be nonempty (otherwise no action exists). Periods are -based in Lean: Lean period is the paper's period , and Lean's knowledge set at is the paper's . The construction and the goal are in dimension , as in the proof; the goal holds for every action dimension .
The worst-case regret is never written as a real supremum, whose junk values would decide the statement. The lower bound is stated by exhibiting the instance. A run of the greedy policy is a predicate quantifying over every circumcenter choice and every minimizer, and nature's sequences are arbitrary. Two pins relative to the page: the printed circumcenter is normalized as in Step 3, and Step 3 assumes , which the page's "" needs (the goal uses ).
Two trivializations are ruled out. Without pointedness the claim holds for with antipodal costs, so is part of the goal. A bound over all runs would hold vacuously if no run existed, so the goal also asserts that a greedy run exists.
A complete development needs spherical geometry of polyhedral cones (extreme rays, angles to a cone), continuity of the uncertainty-angle objective for Lemma 2, and elementary trigonometry. The Geometry and Online definitions are shared with the other missions of this series and are reusable for any work on inverse optimization or learning from revealed preferences. Proofs of any milestone are welcome, as are alternative arguments for Lemma 2.
Remote driving, or tele-driving, lets a human operator in a control center drive a vehicle over a wireless link. A ride-hailing platform that adopts it decouples drivers from vehicles: a driver is attached to a vehicle only while that vehicle carries or fetches a customer, and is released the moment the trip ends. Since an idle vehicle needs no driver, the platform can run a fleet of vehicles with drivers. The operational question is how much service is lost by having fewer drivers than vehicles.
Benjaafar, Wang and Yang study this question with a loss queue in which the service rate depends on the number of idle vehicles, capturing the fact that pickups take longer when fewer vehicles are free (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). The state-dependent rate builds on the spatial capacity model of Besbes, Castro and Lobel (doi:10.1287/opre.2021.2112). Their main finite-system results describe how the service level changes with the number of drivers in three regimes of vehicle supply. This mission formalizes the third regime, where vehicles are ample. The source is the authors' 2023 SSRN working paper; all labels and page numbers below refer to it.
A fleet of vehicles is operated by remote drivers. Customers request trips according to a Poisson process with rate . A request that arrives when all drivers are busy is lost. When customers are in service, each one completes at rate , so the total completion rate is . The rate is defined for real . Let
The number of customers in service is a birth–death chain on . Its stationary law is
and the service level is the long-run fraction of demand served, .
The paper's standing assumptions on the rate are:
The supply-rich regime is the case , that is, : even with every vehicle busy, the system clears work faster than it arrives. In this regime there is a unique with , and exactly when .
In the supply-rich regime, is strictly increasing in . For every with ,
The first part of Theorem 1.C says that, when vehicles are ample, every driver removed costs some service. The second part says the cost is small once exceeds by a margin. The bound is increasing and concave in , so a platform can run noticeably fewer drivers than vehicles at a controlled loss of service. The paper's numerical study (Figure 7) reports reductions of 35–60% in the number of drivers at a service loss below 0.01. The same objects carry over to the paper's asymptotic Theorem 2.C, where the driver-to-vehicle ratio needed in a large supply-rich market tends to .
The result is proved on paper and has no machine-checked proof. The work this mission adds is formal:
is a ratio whose numerator and denominator both change with . For the drivers beyond , monotonicity is immediate, since each additional factor shrinks the numerator while the denominator grows. Below , and the numerator grows, so that argument fails, and the comparison has to use the shape of on . The shape of (Lemma 3) has to be derived from concavity and monotonicity of alone: the assumptions give no smoothness, although the paper's proof differentiates twice. The page argues the two ranges separately, so the step across also has to be covered. The lower bound needs care at the integer part of : the sum in the denominator is taken from , which is at least 1 only because .
Needed infrastructure: finite products and sums over Finset.Icc, StrictConvexOn/StrictConcaveOn on intervals, and the intermediate value theorem for a function that is continuous on . The model file is shared, up to namespace, with four companion missions on the same paper. Proofs of the general facts used here are reusable beyond this mission and are welcome as separate contributions: the product of a positive increasing linear function and a positive antitone concave function is concave, and the reciprocal of a positive strictly concave function is strictly convex.
Low interest rates are meant to stimulate investment, yet periods of monetary easing have coincided with weak corporate investment and large debt-financed share buybacks and dividends. Acharya and Plantin (SSRN 3484935; Management Science, 2025, doi:10.1287/mnsc.2022.01440) explain this with a moral-hazard channel: when the market rate falls below the rate at which shareholders discount the future, firms borrow against future output to pay out cash today (a leveraged payout). The payout lowers the shareholders' retained stake and with it their incentive to make the firm productive.
The paper then asks how a central bank should set the interest rate after a temporary productivity shock when wages cannot fall. Cutting the rate raises investment but degrades productive efficiency through leveraged payouts. Proposition 12 answers the question by the size of the shock: small shocks should be met by leaving the rate unchanged ("leaning against the wind", in the sense of Stein, 2012), and only large shocks may justify a cut.
An economy consists of a discount rate , an effort-cost parameter (not the circle constant), a capital-good technology and a consumption-good technology . Both satisfy the Inada conditions: , , , ; is twice continuously differentiable on with , and is continuously differentiable with strictly decreasing. A unit mass of workers supplies one unit of labour; goes to the capital-good sector and to the consumption-good sector. The laissez-faire steady state solves
At date 0 one cohort of workers is hit by a shock : its technology is . Its first-best labour solves . The date-0 wage is rigid at .
The central bank chooses the date-0 rate . With , entrepreneurs exert effort and hire labour with
The rate at which is the lowest feasible rate. The planner maximizes the date-0 surplus
An optimal rate , with labour , maximizes over every feasible rate.
There is such that
The threshold is pinned from both sides: the first clause alone holds for close to 1, the second alone for .
Proposition 12 is the paper's policy prescription. Together with Proposition 11 (with unregulated leverage the optimal date-0 rate is at most and investment falls short of the first-best) it says that the second-best response to a shock under a rigid wage is non-monotone in the shock size: a central bank that cuts rates for every shock overreacts to small ones.
The result is proved in the paper, in Appendix B, and has no machine-checked proof. The paper's argument is a sketch at three points: Step 1 appeals to "a standard continuity argument", Step 2 to the envelope theorem (66), which presumes a unique differentiable optimum, and the existence of an optimum is taken for granted. A formal proof settles these points and makes the role of explicit. The printed statement also carries a slip (it reads where is meant), which the formalization corrects and records.
The surplus need not be concave in , so first-order conditions do not identify the optimum, and the optimum must be compared globally across the feasible rates . Near both the efficiency gain and the scale term vanish, so the sign of near is a second-order matter: the gap is of order , and the argument breaks down if . The naive argument " is continuous in , so persists near " fails without a uniform estimate, because the optimizer need not depend continuously on . A tie between an interior optimum and may occur at .
The Lean development fixes one economy E : Economy (fields R, π, f, g, lstar, wstar with (20)); the shock and the first-best labour (IsFirstBestLabor E ρ lρ) are separate parameters, so that varies with everything else held fixed. Effort is effort E r, labour demand the relation IsLaborDemand E r l (which includes ), and optimality IsOptimalRate E ρ ru lu is global: against every rate and every feasible labour demand at . Derivatives are deriv, used only where the Inada conditions give differentiability.
Conventions and deviations from the page:
A trivializing formalization is ruled out: optimality is never local, , and are tied to their defining equations, the existence of an optimal rate for is asserted rather than assumed, and the clauses for and are stated together, so that neither nor near 1 satisfies the goal for free.
A complete proof needs the inverse function theorem for , compactness of the feasible rates , the mean value theorem for at , and a uniform second-order estimate near . The continuity and differentiability of the labour response, and the existence of an optimal rate, are reusable for the companion mission on Proposition 11. Proofs of any milestone, and alternative arguments for Step 1 that avoid the envelope theorem, are welcome.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry. Every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936; the term is from Naimpally–Piotrowski–Wingler 2006), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. The answer is known to be yes for strictly convex spaces (CKOW 2016), for ℓ₁ and ℓ₁-sums of strictly convex spaces (Kadets–Zavarzina 2016, 2018), for finite ℓ∞-sums of strictly convex spaces (Haller–Leo–Zavarzina 2022 for two summands; Kurik 2025 under an extra hypothesis), and for c and for c₀ under continuity of the inverse (Leo 2022), among others; it is open for L¹[0,1] and C[0,1].
A recurring step in these proofs is to show that the map preserves the unit sphere and then that a sphere-preserving map is linear. The published versions of the second step assume homogeneity on rays, or oddness, in addition to sphere preservation (CKOW 2016, Lemma 2.5; Zavarzina 2018, Corollary 2.6; Kadets–Zavarzina 2018, Lemma 2.9). This mission formalizes a version that needs only sphere preservation, together with a strengthening in which surjectivity onto the ball is replaced by coverage of the target sphere. The results come from an unpublished research project on the plasticity problem.
and are real Banach spaces, and .
A map is nonexpansive if for all .
In Lean a map of balls is a function F : X → Y on the whole space, constrained on the ball by Set.MapsTo, Set.SurjOn and LipschitzOnWith 1; its values outside play no role.
The goal and its milestones, from the most special tool to the strongest statement:
In U10 and U16, and are nonzero.
The result. U10 reduces the plasticity problem in every real Banach space to sphere preservation, and U16 to coverage of the target sphere by the image of the sphere; the reductions hold between two different spaces, which matters because the plasticity problem is equivalent to its two-space form (Kurik 2025, Theorem 3.1). They also show that sphere preservation, preservation of every norm, and being an isometry are equivalent for nonexpansive surjections of unit balls.
Formalizing it. The proofs exist only in the project's own notes and have been checked by AI referees and partly by the author; a machine-checked proof is the independent confirmation sought. Mathlib has no theory of nonexpansive or averaged maps, so the development will contribute uniform asymptotic regularity of averaged nonexpansive maps (Borzdyński–Wiśnicki; Goebel–Kirk 1990, Theorem 9.4), U16 needs the Bishop–Phelps theorem, which Mathlib also lacks, and the quantitative form of A01 needs the sharp rate of Cominetti, Soto and Vaisman for averaged maps (arXiv:1206.4195, Theorem 1); it is not needed for U10 or U16.
No injectivity, oddness, homogeneity, smoothness or continuity of an inverse is assumed, so none of the standard routes to linearity applies: Mazur–Ulam needs an isometry, and the published sphere-preservation lemmas need homogeneity on rays. In U16 the map need not even be onto the ball.
Real scalars; arbitrary (not necessarily separable) Banach spaces, with CompleteSpace and, in U10 and U16, Nontrivial.
The conclusion of U10 and U16 is a LinearIsometryEquiv agreeing with F on the closed unit ball, so it includes surjectivity of the linear map.
A01 concludes Set.EqOn H id on the closed unit ball.
Statements are not to be weakened by adding injectivity, continuity of an inverse, or finite dimension.
Published inputs (Goebel–Kirk, Bishop–Phelps, Banach's fixed-point theorem from Mathlib) may be added as separate cards and imported by proof sketches.
Many network goods are bought in more than one variety at once. Gamers own both a PlayStation and an Xbox, households subscribe to several streaming services, and users keep accounts on competing social networks. A consumer who multihomes pays twice but enjoys the exclusive content of both products and the network of both user bases. Much of the literature on competition with network effects, starting with Katz and Shapiro (1985) and Farrell and Saloner (1985), assumes that every consumer buys exactly one product. In the paper's own single-homing benchmark (a Hotelling duopoly with network effects), equilibrium prices and profits are strictly decreasing in the strength of the network effect.
Foros, Kind and Stähler (SNF Working Paper 16/21, 2021; published in Management Science, 2025, doi:10.1287/mnsc.2022.00613) let consumers choose endogenously between buying one good and buying both. Without network effects, multihoming makes prices strategically independent (Kim and Serfes, 2006; Anderson, Foros and Kind, 2017), since a consumer's purchase of one good does not depend on the price of the other. Once some consumers multihome and network effects are present, the comparison flips for a range of parameters: network effects make prices strategic complements and can raise both prices and profits. This mission formalizes the paper's Proposition 2, which says exactly when network effects raise the equilibrium price and the equilibrium profit, compared with a market without them.
Two firms sit at the ends of a Hotelling line of unit length, on which a unit mass of consumers is spread uniformly. A consumer at who buys good pays a mismatch cost , with , and . Good has exclusive features worth , and buying it yields a network benefit , where is the strength of the network effect and the expected number of buyers of good . Throughout, (Assumption 1 (i) of the paper). Marginal costs are zero.
When some consumers buy both goods and expectations are fulfilled (), the demand for good at prices is the multihoming demand
Maximizing over gives the reaction function , (15).
This mission treats symmetric firms, . The symmetric fixed point of (15) is the price , and the profit is :
Some consumers multihome and some singlehome exactly when lies in the partial-multihoming range , with
The comparison benchmark "without network effects" is the same model at , where and . The two thresholds of the result are
For , and :
Milestones 4–6 together give , so both thresholds lie inside the partial-multihoming range and every branch of the goal is attained.
Proposition 2 is the paper's answer to whether network effects help or hurt competing firms once consumers can buy both products. In the single-homing benchmark they always hurt. With partial multihoming, network effects raise prices when exclusive content is scarce () and raise profits on the wider range ; in between, on , prices fall but larger sales more than compensate. The thresholds indicate when a firm benefits from stronger network effects, a question the paper's conclusion raises for technology choice.
The result is proved in the paper by hand algebra. This mission produces machine-checked statements of every display of the proof in Appendix A1, first half, in the paper's exact closed forms. Nothing in this model has been formalized before.
The price comparison is a sign check on a rational function. The profit comparison is not: is a quadratic in whose positive root involves , and placing that root relative to and requires comparisons such as . Squaring is valid only once both sides are known to be nonnegative, a fact the paper uses without stating, and the comparisons degenerate to equalities at , so every strict inequality depends on . A naive approach that clears denominators without tracking their signs, or that squares without checking signs, proves nothing.
All parameters are real numbers; , , are explicit arguments. The standing assumptions are explicit hypotheses: , (Assumption 1 (i)), and , strengthened to wherever a strict comparison with the case without network effects is made. The overlapping features cancel from every object and are not a parameter. Assumption 1 (ii)–(iii) (market coverage, positive market shares) is not needed by any statement and is not added.
The model's demand is (14), the multihoming demand under fulfilled expectations; its derivation from consumer choice, and the full pricing game with its single-homing regime and deviations, are not formalized. The profit is defined as price times demand (14), not as the closed form (26), which is a milestone. "Assume partial multihoming" is the parameter range . Proposition 4, the paper's equilibrium characterization, is not posed, because it is false as printed (a profitable deviation exists inside its stated range). Milestone 3 adds , since the quadratic in also has a negative root. The paper's milestone sentences give one direction ("lower if ", "larger if "); the companion directions that Proposition 2 asserts are posed too.
The thresholds are the printed closed forms with Real.sqrt: is never defined as "the root of ", which would make the profit threshold true by definition, and is the literal . Every denominator is positive under , and those hypotheses are kept so that no conclusion relies on Lean's division by zero or on the square root of a negative number.
Needed: real-field algebra, Real.sqrt monotonicity and squaring lemmas, and sign analysis of quadratics. No measure theory or game-theoretic library is needed. Contributions of any milestone, in any order, are welcome.
Online platforms run experiments on subjects that arrive one at a time: a user opens an app, a customer reaches a checkout page, a patient enters a trial. Each subject must be assigned to control or treatment at once, before the next one arrives, and the quality of the final estimate depends on how well the two groups resemble each other in their observed covariates. Classical sequential randomization such as Efron's biased coin (Efron 1971) balances the group sizes; Zhao and Zhou (arXiv:2201.12936, Management Science 2025) instead measure imbalance by an online matching cost and ask how small it can be made against an adversarial sequence of covariates.
Their pigeonhole design partitions the covariate space into cells and balances the two groups inside each cell. With one continuous covariate the paper shows (Lemma 3 and Corollary 1) that uniform cells achieve an expected cost of order , against for complete randomization (Lemma 2). This mission concerns the matching lower bound, Lemma 4: no choice of pigeonholes does better than .
A horizon of subjects, with even, arrives at times . Subject carries a covariate , and the whole sequence is fixed in advance by an oblivious adversary. An assignment puts each subject in the control group or the treated group .
The discrepancy of the split (display (1), p. 11) is the cost of a minimum-weight perfect matching between the two groups:
A pigeonhole design (Definition 3, p. 16) takes a partition of into pigeonholes. When subject arrives:
The design's expected discrepancy on is the average over these fair coins.
An interval partition is given by breakpoints , ; its pigeonholes are , and the cell lengths are .
There are an absolute constant and a threshold such that for every even and every interval partition of , some arrival sequence gives
The partition is arbitrary and the hard sequence is chosen after it; and do not depend on or on the partition.
Milestones 5 and 6 (with ) together give the goal.
Lemma 4 makes the upper bound of Lemma 3 meaningful as an optimality statement: among all pigeonhole designs on one continuous covariate, uniform cells are optimal up to the factor . It also locates the source of the rate in a tension between two kinds of randomness. Long cells let fair coins inside a cell create imbalance across the cell's length. Many cells leave one unmatched subject per cell, and these must be matched across cells. The rate cannot be improved by tuning the partition alone; doing better requires designs outside the pigeonhole class.
The paper's proof is a short sketch, and no part of it has been machine-checked. A formal proof would supply an explicit hard instance for every interval partition, including the rounding of the counts to even integers and the instance for the many-cell case, which the paper leaves unspecified. Lemma EC.2 is a classical result (Blyth 1980) that also has no formal proof in Mathlib.
The algebra of milestones 3 and 4 is elementary. The difficulty lies in the two cases.
In the few-cell case, the per-cell bound of milestone 2 must be computed from the design's actual run. That requires showing that on the alternating instance the first member of each pair always meets a tie in its cell, and that the global cap never alters an assignment. The matching cost must then be bounded below. On the line the optimal matching is determined by the order of the points, so a cell's internal imbalance cannot be cancelled by subjects of other cells, and this needs proof. The ideal counts are not even integers, and the rounding must not destroy the bound.
The many-cell case is the least specified step. The paper's sketch (an odd number of subjects per cell, then a coupling with complete randomization) does not say where the unmatched subjects lie. As printed, it does not handle a partition that mixes one long interval with many short ones; such a partition must be handled by a combination of the two constructions. Lemma EC.2 needs a sharp local estimate of the binomial distribution: the error term is , which is finer than what a plain central limit theorem gives.
Many accounting frauds have come to light through whistleblowers rather than through audits, and regulators now run programs to encourage tips: since the Dodd–Frank Act of 2010 the U.S. Securities and Exchange Commission pays awards for original information that leads to a successful enforcement action. Empirically, whistleblower involvement is associated with better enforcement outcomes (Call, Martin, Sharp & Wilde, 2018), and employees are a leading source of fraud detection (Dyck, Morse & Zingales, 2010). A natural conjecture is that more whistleblowing raises the chance that an audit failure is caught, and so pushes auditors to work harder.
Nan, Tang & Ye (Management Science, 2025) show in a small game that this conjecture can fail. Their main result, Proposition 2, characterizes exactly when increasing whistleblowing intensity lowers equilibrium audit quality. This mission formalizes that result together with the equilibrium it is about.
A firm is good () with probability and bad () otherwise.
where the posterior is computed by Bayes' rule from the probabilities above. 4. Auditor's program. She pays damages when an audit failure is caught, and minimizes
An equilibrium at intensity is a triple of mutual best responses in which the enforcer's posteriors are computed at the actual . The paper assumes and . Write for the enforcer's incentive and for the auditor's incentive.
In Lean, a Model carries with these restrictions. The posteriors are postW1, postW0; the best-response predicates are IsEnforcerBR and IsAuditorBR; the equilibrium is IsEquilibrium M τ a e1 e0. An equilibrium path A (IsEquilibriumPath M A) assigns to every an equilibrium audit quality .
Fix and , and let
There is a threshold , depending only on and positive when , such that for every model with these and , and every equilibrium path ,
The milestones follow the paper's equilibrium analysis and its proof of Proposition 2:
Proposition 2 separates two effects of intensity. The direct effect is that a tip triggers high investigative effort more often, which raises detection and audit quality. The indirect effect, the silence effect, is that with more intense whistleblowing silence becomes reassuring, so the enforcer investigates less without a tip. The result says the indirect effect dominates exactly when the enforcer's incentive is above an explicit threshold and the auditor's incentive is below a threshold. The paper builds its welfare analysis on it: the planner's optimal intensity (Lemma 2, Proposition 3) and the reward-design extension of §4.
The theorem is proved in the paper (Appendix, pp. 31–34), and Proposition 1 is stated without a printed proof. As far as is known, none of it has been machine-checked. A formal proof would check the computer-algebra steps the paper summarizes as "it is simple to verify" or "after some algebra manipulation". It would also make precise two points the printed proof leaves loose. First, the derivative of in fails to exist where the equilibrium crosses the kink of . Second, the printed comparison "" is reversed: is what holds and what the argument needs.
The equilibrium audit quality has no closed form; it is the root of the gap function , which involves a and rational functions of . The obvious attempt, differentiating the closed-form equations (7)–(9) in , gives an expression whose sign is not visible. Its sign depends on , and on which branch of the the equilibrium lies.
The paper splits by branch. On , the sign of is controlled by a single-crossing property in and by the limit at , which yields . Turning this into a threshold on requires the comparative static of in . Each of these steps is a polynomial inequality in four or five variables over a box. They are routine to check numerically, but proving them requires explicit sign certificates.
Model. The intensity is a hypothesis of each statement, not a field.deriv is not used for this, because it returns at a kink. By Proposition 1 the path is unique on .Contributions that are welcome include sign certificates for the polynomial inequalities of p. 33, an implicit-function argument for the derivative of the equilibrium path off the kink and a proof of Proposition 1, for which the paper prints none.
Remote driving, or tele-driving, separates the driver from the vehicle: a human sitting in a control centre drives a car over a network link and can switch to another car as soon as a trip ends. Commercial pilots of this model exist for car delivery and ride-hailing, and it gives a platform a new design choice. A conventional ride-hailing fleet has one driver per car. A tele-driven fleet can run more cars than drivers.
Benjaafar, Wang and Yang model this choice as a queueing system and ask how the service level depends on the number of drivers when the number of vehicles is fixed (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). Idle vehicles still matter even when nobody is driving them: they are spread over the service region, so the car nearest a new request is closer, and trips (pick-up plus ride) finish faster. A driver count below the vehicle count therefore trades fewer servers for shorter service times. This mission formalizes the paper's first main result, Theorem 1.A, which says when that trade can strictly improve service. The mission follows the 2023 SSRN working paper (version of 1 June 2023) and its numbering.
A platform has vehicles and remote drivers. Trip requests arrive as a Poisson process of rate . A request that finds all drivers busy is lost. While customers are in service, each trip ends at the exponential rate , a function of a real . The paper's standing assumptions on this rate are:
The number of customers in service is a birth–death chain with birth rate and death rate , truncated at . With
its stationary law is for . The service level, the long-run fraction of requests served, is
The paper restricts throughout to and . It splits fleet sizes into three regimes by thresholds . In the supply-limited regime , demand exceeds the trip-completion rate in every state: for all .
For , if
then there is a threshold such that is strictly increasing in for and strictly decreasing for , with . If (5) fails, is non-decreasing in on .
Theorem 1.A says that removing drivers from a fleet can strictly raise the fraction of demand served, and Condition (5) says exactly when. The condition compares the average trip-completion rate with the completion rate when every vehicle is occupied. In a standard multi-server loss system, where , the condition never holds and more servers always help. The result makes the optimal driver count a well-posed line search over a unimodal function, and the companion Theorems 1.B and 1.C of the paper (intermediate and supply-rich regimes) rest on the same recursion.
The paper's proofs are short but leave gaps a formal proof must close. To our knowledge no part of the paper has been machine-checked. The mission produces a complete formal statement of the model and of the theorem, under the paper's own assumptions, together with the lemmas the published argument passes through. Milestones 2–4 hold in every regime, so they also serve the proof of Theorem 1.B.
Two steps resist the obvious argument. First, the blocking probability is not a monotone function of anything simple: each driver count truncates the birth–death chain at a different state, so the comparison between and drivers is a comparison of two different stationary laws. Second, the published argument for the first step of the dichotomy appeals to " by Assumption 2", which Assumption 2 does not imply. A correct proof must handle the case where the blocking probability increases already from one driver to two. Strict convexity of must also be proved without derivatives, because the formal rate is only assumed concave, not differentiable.
All objects live in the namespace TeleDriving.ScarceFleet. The rate is a function mu : ℕ → ℝ → ℝ, meaningful for real . , the products , and are explicit definitions following (1)–(3). The committed conventions are:
The threshold is bounded, , and no hypothesis on the shape of or is assumed. A threshold or an assumed monotonicity would make the theorem trivial. The dichotomy milestone carries no regime hypothesis, because the argument of App. C.1 does not use one.
Useful infrastructure, reusable beyond this mission, includes: mediant inequalities for with ; the fact that the product of a positive linear function and a positive, antitone, strictly concave function is strictly concave; and the induction pattern that turns a one-step recursion test into global unimodality. Proofs of any milestone, alternative arguments, and proofs that dispense with the regime hypothesis are all welcome.
The European Union's General Data Protection Regulation (GDPR, in force since 2018) shifted control over personal data from firms to consumers: data may be collected and processed only with the consumer's consent, and consent may be given for some uses and withheld for others. Online retailers use consumer data in two opposite ways. Saved shopping carts, stored addresses and location sharing make shopping more convenient for the consumer; the same data can also be monetized against the consumer, through targeted advertising, data sales or other exploitation. Whether giving consumers control over these uses helps them, and what it costs firms and society, is a question for regulators and for operations managers of e-commerce platforms alike.
F. Xu, X. Wang and F. Zhang, Consumer Privacy in Online Retail Supply Chains (Management Science, forthcoming), build a stylized model in which both uses of data appear and the consumers' disclosure decisions are taken under rational expectations. This mission formalizes the paper's single-firm result: when one vertically integrated e-commerce firm sells directly to consumers, the GDPR always raises the firm's profit and social welfare, but it raises consumer surplus only when the product's valuation is below an explicit threshold. A companion mission treats the supplier–retailer chain of the same paper, where the GDPR can hurt all three parties.
A unit mass of consumers values one product at . A consumer's inconvenience cost is uniform on . The data quality is , and monetizing data at intensity costs the firm with . Write
The firm first decides whether to collect data (), then sets a price . Production is free. A buyer who hides her data gets . A buyer who discloses gets : the data scale her inconvenience down by the factor , and the firm extracts from her. Without collection only hiding is available. A consumer buys iff her best buying utility is nonnegative.
Two data policies are compared.
The firm's profit is . Consumer surplus is the integral over of each consumer's realized utility (zero for non-buyers), and social welfare is profit plus consumer surplus. A subgame-perfect equilibrium (SPE) is a profile with an REE response after every , an optimal price over after each , and an optimal .
Let . SPEs exist under both policies, and for every SPE of the mode and every SPE of the mode,
The theorem separates two effects of the GDPR on consumers. The direct privacy effect removes the exploitation loss of every discloser. The indirect pricing effect works the other way: without the exploitation revenue the firm no longer discounts the price to attract disclosers, and once the market under the GDPR is fully covered the firm raises the price sharply. The threshold says exactly where the second effect overtakes the first. The result that profit and welfare rise regardless of shows that in a single-firm market the GDPR is never welfare-reducing; the supply-chain mission shows that this conclusion fails once a supplier sets a wholesale price, which is the paper's main policy message.
The paper's proofs (e-companion, Appendix C, pp. ec21–ec24) work with closed forms and leave several steps to "it can be verified". A formal proof checks the reduction from the game to those closed forms: existence and uniqueness of the REE at every price including the saturated range, global optimality of the prices over all of , and the collection decision against the full no-collection subgame. To our knowledge no part of this paper has been machine-checked.
The obvious argument plugs the printed formula into the profit (3) and maximizes. That formula solves the REE condition only while the market is not saturated; on the saturated range the REE intensity is the constant , and the profit is a different function of . The firm's problem is therefore a maximization of a piecewise function with a kink at full coverage, and the price comparison has to cover prices above (no sales) and the subgame without collection.
The consumer-surplus comparison involves two piecewise quadratics with different breakpoints, , and their single crossing at lies in the middle region where one mode is saturated and the other is not. Strictness of the profit and welfare comparisons needs the identity and its relatives.
All objects are real numbers; , and are hypotheses of every statement. The paper does not state ; at nothing is sold, every outcome is , and every strict claim fails, so is a disclosed standing assumption.
Sets of consumers are measured by Lebesgue measure on ((volume S).toReal); consumer surplus is the interval integral . Indifferent consumers buy and disclose (a null set). The REE uses an IsMaxOn condition over and the disclosing quantity defined from utilities; neither nor is hard-coded. The firm's profit is defined from the REE response, not from the paper's (3). A strategy profile specifies a price for both collection decisions and an REE response at every with ; the comparisons in the goal are between on-path outcomes of such profiles.
The goal is not a comparison of printed closed forms: those are milestones 6–7. It asserts existence of an SPE in each mode, so "every equilibrium" is not vacuous; no price range is restricted and no off-path action is omitted.
Display (2) is stated in its corrected two-branch form for ; Lemma 1 is stated for , with the REE intensity at . The paper's Table 1 (p. 12) misprints the purchase condition of disclosers and is not used.
A complete development needs volumes of intervals, the REE fixed point, maximization of concave piecewise quadratics over , and square-root threshold algebra. No probability or limits are involved. The consumer-stage definitions are shared verbatim with the supply-chain mission and may later be merged. Proofs of any milestone, and of auxiliary lemmas such as , are welcome.
Large online retailers such as Amazon run two businesses on one storefront. They sell products themselves, and they host a marketplace on which third-party sellers sell, paying the platform a percentage of their revenue. A retailer that also runs the marketplace can decide which products to sell itself, and it controls which offer most consumers see. Competition authorities have asked whether this dual role lets the platform appropriate third-party sellers' business, and empirical work (Zhu and Liu, 2018) finds that Amazon enters only a small, high-performing subset of marketplace products.
Hervas-Drane and Shelegia (Retailer-Led Marketplaces, Management Science, 2025) give a model in which these choices can be computed. Its main result, Proposition 2, says which products the platform sells itself when its assortment is limited. This mission formalizes that proposition together with the pricing and entry results it rests on.
There is a unit mass of products. Each product is an independent market indexed by its consumers' valuation . Valuations are distributed according to a probability measure on with CDF . Every unit costs to supply. Each market has a unit mass of unit-demand consumers, who buy at a price only if .
The monopolist retailer sets an ad valorem fee on the third-party seller's revenue. He can steer a share of consumers (the inattentive ones) to the seller of his choice; the remaining buy from the cheapest offer, with ties going to . He has capacity : he can supply at most a fraction of all products.
The game has three stages. In Stage 1 sets . In Stage 2 each product's third-party seller decides whether to enter, and then chooses which products to enter. In Stage 3, in each market both present firms price sequentially: quotes first, then quotes and steers. The solution concept is subgame perfect equilibrium.
Proposition 1 solves Stage 3. A product supplied by alone (SBM) earns him . A product supplied by alone (SBT) earns her and earns him the fee . When both supply it (SBMT), charges
and earns . Lemma 1 says enters exactly the products , the marketplace products. An allocation of is any measurable set of products with . His total profit is the SBM profit on below , plus the SBMT profit on above , plus the fee on marketplace products outside .
Assume (Assumption 1) and . Let and
Then:
Proposition 2 is the step that the rest of the paper builds on. Display (4) writes the monopolist's profit as a function of the fee by plugging in the thresholds , , , of Proposition 2. The optimal fee (Lemma 2, Proposition 3) and the policy comparisons of §6 (a pure-retailer response, fee regulation, steering bans) are all statements about that function. The two modes are also the paper's empirical prediction. A platform with little capacity, effective steering and a high fee competes only in the top marketplace products. With more capacity it also takes products no third party sells.
The paper proves Proposition 2 in Appendix A. The proof is an informal capacity-allocation argument. No machine-checked version exists. A formal proof has to turn the argument about entering the products of highest marginal profitability first into a statement about all measurable allocations of mass at most . It must also prove uniqueness up to null sets, and handle the corners , and that the prose passes over.
The obvious argument ranks products by the marginal profitability of entry and fills capacity from the top. Two facts make this harder than it looks. First, the ranking is not monotone in . Below the gain is ; above it is , which starts again from at . So the optimal set is an upper level set of a piecewise function, and in Mode II it has two components. Second, the claim is about every measurable set of mass at most , not about thresholds. Optimality needs an exchange argument against arbitrary sets, and uniqueness needs the level sets of the gain to be -null. Locating the thresholds also needs continuity and strict monotonicity of , which come from the density and the full-support hypothesis.
Proposition 1 has its own subtlety. At the monopolist is indifferent between matching 's price and charging . 's best price exists only if 's strategy breaks this tie in 's favour, so the equilibrium has to be stated for strategies defined at every price of .
Products form a probability measure μ : Measure ℝ. The standing hypotheses are:
Integrable (fun v => v) μ, which the paper never states but which is needed for profits to be finite;The foreclosed corner () is not covered. Marketplace products are encoded as . Optimal allocations quantify over all measurable sets of mass at most , and uniqueness is up to -null sets. Restricting allocations to intervals or to unions of two intervals would assume the conclusion, and the formalization does not do it.
In Proposition 1, 's strategy is a function of 's price that is a best response at every price, and 's price is optimal against it. Uniqueness of the SBMT outcome is stated only for and , where it holds. Lemma 1's duopoly clause likewise needs .
Two definition files carry the model:
Model: , the marketplace set, the Proposition 1 payoffs, , , , allocations and profit;PricingGame: the three pricing games and their equilibria.The bathtub-type lemma behind Proposition 2 is reusable beyond this mission: among measurable sets of mass at most , an upper level set of a weight maximizes its integral. Contributions of that lemma, of the milestones, and of alternative proofs are welcome.
During the COVID-19 pandemic most U.S. payers began reimbursing a telehealth consultation at the same rate as the corresponding office visit, a policy called pay parity. Many states have since made it permanent, on the stated ground that it improves patients' access to care. In acute care (primary and urgent care) a telehealth visit sometimes cannot resolve the problem and the patient must also come to the office: a duplicate visit. Duplicate visits are paid as well, and they consume office capacity.
Çakıcı and Mills (MSOM 2024; this mission follows the SSRN working-paper version of August 19, 2024) model a provider who splits capacity between an office and a telehealth channel, and patients who choose a channel strategically. Their main finding for the setting in which demand exceeds capacity is that pay parity can make the provider's revenue-maximizing choice and the access-maximizing choice disagree: for a moderate duplicate-visit probability the provider prefers telehealth while patients are better served by an office-only practice. This mission formalizes that result and the equilibrium analysis on which it rests.
A provider serves at total rate and devotes the fraction of its capacity, the telehealth commitment, to telehealth. Episodes of care arrive at rate . Each patient balks (value ), visits the office, or uses telehealth; a telehealth visit needs a duplicate office visit with probability . A resolved episode is worth ; waiting costs per unit of sojourn time; the co-payments are and ; an office visit costs an extra inconvenience . With the proportions choosing the office and telehealth, the expected sojourn times are
and the expected utilities are (office) and (telehealth). A patient equilibrium is a split in which every action used is a best response.
The paper assumes , , and, with , that . In the large-market setting some patients balk at every . There the equilibrium is of one of four types, by region of : balk/office on , balk/office/telehealth on , balk/telehealth on , all-balk on , with explicit thresholds and explicit proportions . The patient access rate and the provider's revenue rate under telehealth reimbursement (office revenue ) are
The commitment that maximizes telehealth usage in the balk/telehealth region is .
Fix all parameters except and , with . There are thresholds such that, for every admissible , pay-parity revenue is maximized over at when and at when ; access is maximized at when and at when ; and for
The thresholds are existential; no closed form is fixed, so the statement survives any later computation of them.
In attack order: Lemma 2 (order of ); Theorems 1–3 (where each equilibrium type occurs) and Lemma 3 (); Theorem 4 (shape of in ); Corollaries 1–2 (the maximizers of and are or ); Proposition 3 (the two thresholds). Two further items are not milestones: the uniqueness of the large-market equilibrium proportions, and Proposition 5 (the reimbursement aligns the two objectives).
The result is the paper's argument against pay parity in acute care: when duplicate visits are neither rare nor frequent, paying telehealth at parity induces the provider to adopt it although fewer patients are then seen. Proposition 5 shows the misalignment disappears under the less-than-parity reimbursement , which pays the same per patient seen through either channel. The thresholds and are what turn this into a policy statement about measurable duplicate-visit rates.
The paper proves these results by hand. None of them has a machine-checked proof, and nothing about strategic channel choice with duplicate service exists on Prove2Me. Formalizing them checks a case analysis with four regions, two square-root closed forms and an intermediate-value argument in . The formalization has already exposed two places where the printed statements need a hypothesis (see Formalization scope).
Each step is elementary; the difficulty is bookkeeping. The equilibrium characterization requires solving the indifference conditions in each region and choosing the root of a quadratic that gives stable queues. The shape results require continuity of and across region boundaries and concavity of a function of the form . The obvious comparison of the closed-form values at and at does not suffice on its own: the closed-form value at is the revenue only when lies in the balk/telehealth region, which fails for some admissible parameters. Whether that failure matters for the maximization is the central question.
All objects are real-valued closed forms in the namespace TelehealthParity.Access. The definition Setting holds the parameters (the arrival rate is lam, since λ is a Lean keyword), , the region-wise proportions, , , the large-market condition and the predicate Admissible p q. The definition Equilibrium holds the sojourn times, utilities and the equilibrium predicate. Conventions:
Admissible p q collects , assumption (6), Lemma 2's ordering condition, the large market, and . The last is not printed; the proof of Lemma 2 presumes it, and Lemma 2 fails without it.IsMaxOn over ; "linear" is affine.Excluded trivializations. , and are closed forms, not suprema or argmaxes. The goal states the strict misalignment and the full threshold characterization, not a comparison with one point. A sorry-free sanity check shows that the hypotheses hold on an admissible instance in the misaligned range (, , , , , ).
Welcome contributions are proofs of any milestone. The real-analysis lemmas (concavity of , maximization of piecewise functions that are continuous across region boundaries) are reusable beyond this mission.
Large technology firms often buy small startups mainly to hire their staff, a practice known as acquihiring. Antitrust authorities review acquisitions that may reduce competition in product markets, but an acquihire can instead reduce competition in the labour market: a firm that buys the employer of a scarce worker no longer has to outbid that employer for her. Bar-Isaac, Johnson and Nocke study this effect in a three-player model: a startup, its essential employee, and a potential acquirer (CRC TR 224 Discussion Paper No. 500, 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604).
In the paper's baseline model (Proposition 1) the acquirer, whenever it hires the employee, does so by buying the startup, and the employee always prefers direct wage competition. This mission formalizes §6, where the employee's private benefit from staying at the startup is her private information. That uncertainty softens wage competition, so acquihiring is no longer always chosen, and the paper derives the exact threshold at which the acquirer switches.
An employee produces value if she works for the acquirer and if she works for the startup. At the startup she also enjoys a private benefit , which only she observes and which is uniformly distributed on . She has an outside option worth , and wages are unrestricted real numbers. The standing assumptions of §6 are
The acquirer chooses between two modes.
A pair is an equilibrium of this wage game when each offer is a best response to the other over all real wages.
The quantities named in the statements are Lemma 5's wages
the indifferent type , and the threshold
Under the standing assumptions, , is a direct-hiring equilibrium, and
In addition, every type of employee is strictly better off under direct hiring than under acquihiring.
The proposition separates two effects that coincide in the baseline model. Without private information, wage competition is Bertrand-like: the winning firm must match the losing firm's full willingness to pay, so buying the competitor is always cheaper. With a privately known benefit, competition between the two employers resembles product differentiation, and each offers less than the employee's productive value. Direct hiring then becomes profitable when is close to , and acquihiring is chosen only when exceeds . Corollary 4 compares this threshold with the efficiency threshold and finds a band of parameters in which acquihiring occurs although it lowers total surplus. That band is the paper's case for labour-market scrutiny of acquisitions.
The results are proved on paper, by first-order conditions and a quadratic comparison. None of them has a machine-checked proof, and the platform has no prior formalization of wage competition, monopsony or acquisitions. The mission adds an explicit Bayesian wage game with expected profits written as integrals over the type distribution, with global best responses rather than first-order conditions. The objects are small enough to be reused for other two-firm wage-posting models with a uniformly distributed taste shock.
The algebra of Proposition 5 is a quadratic inequality in . The work is in Lemma 5. The page solves first-order conditions inside the region , , where both expected profits are concave quadratics. An equilibrium, however, requires that no deviation pays anywhere on the real line, including offers so low that no type accepts and offers so high that every type accepts. Outside the interior region the profit functions are piecewise (zero below, linear above), and each piece has to be compared with the interior optimum. The expected profits are interval integrals of indicator functions, so evaluating them requires the measure of the set of accepting types. Ties between the two offers occur with probability zero, and the statements are insensitive to how they are broken.
All quantities are real numbers. The parameters , , form a structure, and the five standing inequalities form a predicate that every theorem except the pure-algebra milestone takes as a hypothesis (that milestone needs only ). Expected profits, the poaching probability and direct-hiring welfare are of bounded, piecewise-constant integrands, hence interval integrable. A verification file evaluates the acquirer's profit at Lemma 5's wages to its closed form on one instance, and exhibits instances of both branches of the proposition and of the window in Corollary 4. Ties go to the startup.
Conventions committed to:
The direct-hiring profit is an integral over the type distribution evaluated at wages that are proved to be an equilibrium. It is not a closed-form payoff taken as a definition. Dropping any standing inequality would change Lemma 5 (the poaching probability leaves ) or Proposition 5 (the second root comes back into range). The employee-preference clause is part of the goal, and no equilibrium is claimed unique beyond what the page derives.
Contributions welcome: the interval-integral evaluations of step functions, the global best-response argument for Lemma 5, and the quadratic comparison with .
Technology firms often buy small startups mainly to obtain their staff, a practice known as acquihiring; Chatterji and Patro (2014) identify 98 such deals between 2009 and 2013. Bar-Isaac, Johnson and Nocke (CRC TR 224 Discussion Paper No. 500, 2024, www.crctr224.de; published in Management Science, 2025, doi:10.1287/mnsc.2024.04604) study the labour-market side instead. A firm that wants a startup's essential employee can compete for her in wages, or it can buy her employer and so remove the only rival bidder for her services. Their baseline model, the subject of this mission, isolates that choice. It shows that whenever the acquirer hires the employee, it does so by buying the startup, and that the employee is always worse off as a result.
This mission is the first of a series of three on the paper. The second formalizes the extension with Nash bargaining over the price and possible poaching after a failed bid (Proposition 2). The third formalizes the version in which the employee's private benefit is private information (Proposition 5).
There are three players: a startup , an employee , and a potential acquirer . The employee generates value when working at the startup and when working at the acquirer. At either firm she is paid a wage of at least the floor (written wl in Lean), and at the startup she also enjoys a private benefit . Throughout the paper,
In Lean these four numbers form the structure Params (fields va, vs, b, wl), and the displayed assumption is the predicate Params.Standing.
The acquirer first chooses a mode.
The paper restricts attention to equilibria in undominated strategies: no firm offers or bids more than its willingness to pay (footnote 13). A continuation equilibrium of each mode is a profile (offers, bid, and the accept/decline rules of the employee and of the startup at every possible offer) in which every player best-responds, both on and off the path of play. The total surplus of an outcome is if the employee ends up at the acquirer and if she stays; wages and the price are transfers. An outcome is efficient when its surplus equals .
For every continuation equilibrium of the direct-hiring subgame and every continuation equilibrium of the acquihiring subgame:
where denotes the acquirer's payoff and the employee's payoff under each mode. The goal also states that continuation equilibria exist away from the knife edges (direct hiring) and (acquihiring), so that the universal statements are not vacuous. In words: if the acquirer hires the employee, which happens exactly when , then it does so through acquihiring, and the employee always prefers direct hiring.
The proposition carries the paper's main message in its simplest form. Buying the startup removes wage competition: the acquirer pays the startup its retention profit and then pays the employee only the floor . It never compensates her for the private benefit she loses. As a result, acquihiring occurs whenever , including the range in which it destroys surplus, and the employee loses relative to direct hiring in every case. Formalization adds a fully explicit version of the equilibrium analysis. The paper calls Lemmas 1 and 2 "immediate" and does not spell out the employee's tie-breaking or the off-path behaviour that the equilibrium concept requires. Here each subgame is an explicit predicate on strategy profiles, so a complete proof also has to show that the stated outcomes are the only ones. The results are proved in the paper. No machine-checked proof of them is known, and the platform currently has no formalization of acquisitions or of wage competition between firms.
The algebra is elementary; the work lies in the uniqueness half of Lemma 1. Exhibiting one equilibrium is routine. Showing that every equilibrium has the stated outcome requires ruling out each alternative: a winning offer above the rival's reservation level can be undercut, and a losing firm with surplus left can overbid. Each deviation has to be shown both feasible (at least , which is where the standing assumption enters) and profitable against the employee's rule. A naive treatment that fixes the employee's choice only on the equilibrium path fails, because a firm's deviation could then be "punished" by an employee who chooses the worse offer. A treatment with strict tie-breaking fails too: when the acquirer would want the unattained infimum , and no equilibrium would exist. Lemma 2 needs the same care with the startup's acceptance rule. There, the bid is not unique when .
All quantities are real numbers. The direct-hiring profile DHProfile consists of the two offers and a Bool-valued acceptance rule acceptA x y defined at every pair of offers . The predicate IsDHEquilibrium requires:
The acquihiring profile AHProfile consists of the bid, the startup's acceptance rule at every bid, and the two post-bid wages. The predicate IsAHEquilibrium requires:
The standing assumption ( and ) is a hypothesis of every theorem. Footnote 13 enters only through these caps. The other hypotheses added relative to the page are:
The knife edges and are not covered by the page's case distinctions, and the corresponding clauses stay conditional on strict inequalities. Milestones 3–4 and the employee's preference hold at the knife edges as well and are stated without exclusions.
The payoffs are never defined by their closed forms ( or as definitions would turn Proposition 1 into arithmetic), the standing assumption and the employee-preference clause are never dropped, and the declined bid is never claimed unique.
All definitions live in AcquihiringMonopsony.Baseline.Model. The direct-hiring wage game, an asymmetric Bertrand contest for a single worker with a private benefit at one firm, is reusable for the other missions of this series. Contributions are welcome at every level: proofs of the two lemmas, of the payoff identities, and of the goal from them.
Online marketplaces such as Amazon are both the storefront of third-party sellers and a retailer in their own right. A platform that observes how well a seller's product sells can later launch a competing product in the same space, and empirical work finds that it does so selectively: Zhu and Liu (2018, Strategic Management Journal) report that Amazon is more likely to enter product spaces with high sales and ratings. A seller who anticipates this faces a strategic choice about how much to invest in her product before the platform decides.
Qi, Song and Xiao (Management Science, 2025) model this interaction as a two-stage game and ask how the seller's investment responds to the threat of entry. Their answer depends on whether the seller ultimately benefits from the platform's entry, which can happen through spillovers: the platform's own investment in the product space also raises the value of the seller's product. This mission formalizes the case in which the seller does not want the platform to enter, the protective regime, and the paper's characterization of her optimal effort there (Proposition 3).
The parameters are a degree of spillover , a referral rate (the share of the seller's revenue paid to the platform), a competition intensity , the seller's effort-cost coefficient , and the platform's fixed entry cost . The platform's own cost coefficient is normalized to .
In the first stage the seller's product has base value ; she chooses an effort at cost , raising the value to , and sells a quantity at price , keeping the fraction of revenue. In the second stage the platform, having inferred , decides whether to enter. If it does, it invests in the product space and the two compete in quantities.
The paper reduces the second stage to closed forms. Write for the left side of condition (5),
which says that the seller stays in the market after entry and is assumed throughout. With an explicit polynomial denominator , set (equation (8)). The seller's two-stage profits under non-entry and entry are
The platform enters iff the product value exceeds a threshold , where is a second explicit polynomial in (Proposition 1). Hence the seller's total profit is
The protective regime is ; there for every effort. The benchmark efforts and , equations (9)–(10), maximize and respectively.
In the protective regime, with defined by , there is such that an optimal effort is
and the optimal first-stage quantity is .
The result identifies strategic underinvestment as the seller's response to an unwelcome entrant: for intermediate base values she chooses less effort than her first-best so that the product's value sits exactly at the entry threshold. For low base values no distortion is needed, and for high ones the required distortion costs more than entry does. This explains why a seller's investment may fall short of what her own costs and demand would justify, and it is the starting point of the paper's analysis of non-entry commitments (Proposition 5).
The result is proved in the paper; nothing here is open. No part of it is formalized. A machine-checked version adds a complete check of a proof that compresses several steps into "verifiable" remarks: the positivity of and the sign of under (5), and the single sign change of that defines .
The seller's objective is discontinuous at , so the first-order condition alone does not locate the optimum: the candidates are the two unconstrained maximizers and the cutoff, and which one wins depends on . The step that needs care is the existence of a single switching point : it requires comparing the value of the constrained non-entry problem with the unconstrained entry optimum as a function of , and showing that the comparison changes sign once. The polynomial sign facts behind , namely and on the parameter box under (5), are elementary but involve quartic polynomials in three variables.
All quantities are real numbers. The standing ranges , , are hypotheses, as are condition (5) (assumed by the paper from p. 12 on) and (not stated by the paper, but presupposed by its formula for ; with the threshold degenerates to 0). Only the branch of and for which (5) holds is formalized; the paper's proof also covers the regime where (5) fails, with .
The closed forms (6), (7), the entry gain and are definitions taken from the paper. Their derivation from the second-stage Cournot game (Lemmas 1–2) is the subject of the companion mission On the Platform’s Entry I. The piecewise profit is the printed one, with the tie assigned to non-entry.
Efforts range over all of . This is the paper's implicit domain and it matters: the optimal effort is negative for some parameters (for instance , , and slightly above ), so a version restricted to would be false. "Optimal" means a global maximizer, with ties allowed; at two efforts are optimal and at the middle interval is empty.
Trivializing formalizations are ruled out: is pinned by its defining equation rather than chosen, every hypothesis is satisfiable (at , one has ), and the sign conditions keep from collapsing to a junk value of division or square root.
A complete development needs only real analysis of quadratics and polynomial inequalities on a box; contributions of reusable lemmas on maximizing concave quadratics under a threshold constraint are welcome.
A portfolio manager who observes side information (a covariate , such as a market indicator) before choosing a portfolio wants to control the loss of the asset returns conditional on the observed covariate value . The conditional law of given is unknown and must be learned from historical pairs . When itself was never observed, the empirical conditional law is undefined, and kernel or nearest-neighbour estimates are fragile. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research, 2025) robustify the conditional decision with an optimal transport ambiguity set: the decision maker hedges against every joint law of within transport distance of the empirical law. The resulting objective is a ratio of two linear functionals of , so the standard Wasserstein distributionally robust duality (Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) does not apply directly.
The paper settles every regime of the three parameters (ball radius , fiber radius , minimum fiber mass ). This mission formalizes the simplest regime, , where the answer is negative: the worst case does not depend on the data at all.
The covariate space and the return space are Polish spaces with their Borel -algebras. Two ground costs and combine into the separable cost . The data define the empirical measure .
The optimal transport cost between two probability measures on is
the infimum over couplings with marginals and . The ambiguity set is the ball .
Given a covariate value and a radius , the neighbourhood is , and is the fiber set. For a loss at a fixed decision and a law with positive fiber mass, the conditional expected loss is
The paper's standing Assumption 2.4 requires: (i) and are symmetric, non-negative and continuous, and vanishes exactly on the diagonal; (ii) every has a unique projection onto ; (iii) every boundary point of has points outside at arbitrarily small cost.
With the fiber is . With the fiber-mass constraint is taken as the strict inequality , so that the conditioning event is never null.
For every , every and every loss ,
both sides in .
The proposition shows that conditioning on a single covariate value with an optimal transport ball is uninformative: the worst-case conditional loss equals the robust optimization value for every data set. This is what motivates the rest of the paper: either a minimum fiber mass (Theorem 3.2) or a fiber of positive radius (Section 4) is needed for the data to matter. The paper contrasts this with the type- Wasserstein ball, for which it points to existing results to compute the worst case.
For the platform, the mission sets up the shared model of the series: the separable ground cost, the empirical measure, the fiber, the conditional expectation as an extended-real ratio, and the paper's Assumption 2.4. The ball representation (milestone 1) is used by every other mission of the series; it rests on the existence of optimal couplings on Polish spaces, which Mathlib does not yet have. The result is proved in the paper; no machine-checked proof is known to exist.
The statement is an equality of two suprema over very different index sets, and neither inequality reduces to the other. The natural first idea, that the worst case is attained by a small perturbation of the empirical measure, fails: the empirical measure may put no mass on the fiber , or put its mass there at returns far from where is large, and the value must be reached for every data set. Points of the data sitting exactly at are the delicate case, since the transport budget charges for every displacement of mass. The ball representation (milestone 1) is the hard infrastructure step in its "only if" direction: it needs an optimal coupling, i.e. attainment of the transport infimum on Polish spaces, which is absent from Mathlib.
Samples are indexed by Fin N with . The ground cost is as a -valued function. The transport cost reuses the published RWPI.SqrtLasso.transportCost, an infimum over couplings whose first marginal is and second marginal is ; the paper's "min" is not built into the definition. The radius enters as ENNReal.ofReal ρ, and the goal assumes as on the page (). Expectations use the published ModelRiskOT.Duality.extIntegral, in , so the loss is arbitrary: no measurability, boundedness or integrability. The loss stands for at an arbitrary fixed decision, which is how "for any feasible " is read. The fiber at is ; that it equals follows from Assumption 2.4(i). The boundary in Assumption 2.4(iii) is the topological frontier in .
One hypothesis is added to the paper and disclosed: is not isolated for (for every some has ). This is Assumption 2.4(iii) at when the boundary of is read in an ambient Euclidean space, as the paper's remark on p. 11 does; the proof uses it, and without it the statement fails at an isolated that is also a sample point.
Trivializing encodings are excluded: the supremum ranges only over probability measures in the ball with strictly positive fiber mass, so the conditional expectation is never evaluated at a null fiber; no Bochner integral (which is for a non-integrable loss) is used; cannot enter through ofReal; and the feasible set is exactly intersected with the positive-mass constraint.
Contributions welcome: the existence of optimal couplings for lower semicontinuous costs on Polish spaces (reusable far beyond this mission), the decomposition of couplings with a finitely supported marginal, and the two halves of the goal.
Ride-hailing platforms are expected to add autonomous vehicles (AVs) to fleets that today consist of human drivers. AVs have a cost advantage: a human driver must earn a reservation wage for every hour on the platform, while an AV owner pays a fixed capital cost per calendar hour and a smaller variable cost per operating hour. Whether that advantage reaches riders as lower prices depends on how the market is organized: who owns the AVs, and whether AVs and human drivers are dispatched on the same platform.
Z. Lian and G. van Ryzin study this question in Capturing the Benefits of Autonomous Vehicles in Ride-Hailing: The Role of Market Configuration (Management Science, 2025). This mission formalizes one of their central results: when a single AV supplier (a monopoly) shares a common platform with perfectly elastic human-driver supply, its choice of AV capacity is a newsvendor problem, and the optimal capacity is the pure human-driver fleet size of the scenario at a critical fractile of the demand distribution. The version formalized here is the authors' 2023 SSRN working paper (abstract 3716491, version of 23 August 2023); all theorem and equation numbers refer to it, not to the published article.
Vehicles and demand. Riders' values for a ride-hour are uniform on . In a scenario with potential demand mass , serving the demand rate requires the price , and generates the revenue , where is the trip time. Pickup times depend on the number of open vehicles through with and . Minimizing over gives the minimal fleet needed to serve ,
and the maximal utilization . The function is a strictly increasing bijection of ; its inverse is the largest demand that vehicles can serve.
Human drivers (HVs). In this mission HV supply is perfectly elastic at reservation earnings per hour (the paper's ). A demand rate is a pure-HV equilibrium when revenue covers the minimal HV cost, ; among stable equilibria the paper selects the largest, the maximal stable equilibrium , with fleet size . The market is loose when .
AVs. AVs cost per operating hour and per calendar hour, and (Assumption 1). On a common platform, the paper shows (Proposition 6) that the variable profit per AV at fleet size is
Scenarios and the monopoly problem. Demand has scenarios with masses and probabilities . The monopoly chooses a capacity , then a fleet in each scenario:
Let be the smallest index with . In a loose market,
is an optimal capacity for (5).
The result. Proposition 8 says that, on a common platform with elastic human-driver supply, a monopoly AV supplier never undercuts the human drivers' price: in every scenario it deploys at most the pure-HV fleet size, so riders pay the pure-HV price, and the whole cost advantage is retained by the supplier. Its capacity is set by the classical newsvendor trade-off between the margin of a used AV and the fixed cost of an idle one. With a cheap fixed cost the supplier covers the peak scenario; with an expensive one it covers only the lowest scenario and lets human drivers serve the rest. These conclusions drive the paper's policy comparison of market configurations.
Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version exists. A complete development requires the analysis of (real powers with exponent ), the identification of the maximal stable equilibrium under the loose-market condition, a monotonicity argument for the AV-only profit along the inverse , and the discrete newsvendor argument over a piecewise-linear concave objective. The last part is reusable for any discrete-scenario capacity problem.
The newsvendor step is elementary once the objective is in the form (20). The work lies in reaching (20) from (5). That requires, in each scenario, showing that the maximum over of is attained at . Below this is linear growth; above it, the profit is a function of , an inverse of a sum of a fractional power and a linear term with no closed form, and its decrease rests on the loose-market condition placing beyond the revenue-maximizing demand . Without the loose-market condition the claim fails: in a thin market the only equilibrium is , and the supplier's AV-only profit need not decrease past it. The continuity of at uses the equilibrium identity , which itself depends on identifying the maximal stable equilibrium.
Fin I (0-based): the paper's scenario is index , is a sum over indices strictly above , and "the smallest " is IsLeast.IsMaxStableEq on given numbers , not a choice function.