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?
Platforms that earn money from their users' activity make two linked decisions about the data that activity generates: how much of it to record and store, and how much to spend protecting what they store. Stored data lets a business tailor its services and sell data-driven products, but it also attracts adversaries (hackers, data brokers, unauthorized third parties) whose access harms users, who then use the service less. Fainmesser, Galeotti and Momot, Digital Privacy (Management Science 69(6), 2023, doi:10.1287/mnsc.2022.4513; author manuscript SSRN 3459274), build a tractable model of this trade-off and solve it in closed form. Their first main result, Theorem 1, gives the profit-maximizing data strategy explicitly and shows that a business whose revenue depends more on data both collects more and protects more. The result is the basis for the paper's policy analysis (data protection standards, Pigouvian taxes on stored data) and for its comparison with the social optimum, which is the subject of a companion mission.
A unit mass of identical users each choose an activity level . The business stores a fraction of every user's activity and protects it at level , at cost . With average activity and a mass of active adversaries, a user's utility is (display (1))
where measures network effects and the users' benefit from tailored services built on stored data. Adversaries have access costs with uniform on and gain ; letting , the mass of active adversaries is . Proposition 1 shows that for every data strategy with this users–adversaries subgame has a unique equilibrium,
with consumer surplus ; when nothing is stored, . The business's profit is (display (2))
where the revenue model is the share of revenue that is data-driven: is a purely usage-driven business, a purely data-driven one. A business optimum is a strategy that maximizes over .
The Lean development uses the same names: abar, omegaStar, CS, profit, Feasible, IsBusinessOpt, the best-response quantities Ch (), kappa (), Cl (), xiBR, the threshold psiL (), the interior root xiI (), and the closed forms xiStar () and CStar ().
For fixed , , and every , let
Then is a business optimum, and both and are weakly increasing on .
Theorem 1 is the statement that a business's revenue model alone orders its data practices: holding users and costs fixed, moving toward data-driven revenue never lowers collection and never lowers protection. The paper uses it to explain why consumer surplus is maximized at an intermediate revenue model (Proposition 2), and as the benchmark against which it evaluates regulation in §6. The closed form also makes the regime structure explicit: no collection when protection is expensive, full collection when it is cheap, and an interior solution in between.
The result is proved in the paper (App. A.2–A.3, with the proofs of Lemmas 1–2 in Online App. B), but parts of that proof are informal: several steps are "easy to check" or "can be derived similarly", one case is treated and the other left to the reader, and the second-order conditions are referred to a general lemma in Online App. C.5. No machine-checked version exists. A formal proof certifies the closed form, including its boundary cases, which the printed formula handles through an infinite square root.
The profit is not jointly concave, so first-order conditions do not settle the problem. The argument intersects the two best responses (Lemmas 1–2), and two candidate strategies survive in the intermediate regime: and the interior point. Choosing between them requires comparing profits across all and showing the comparison flips exactly at . Monotonicity in is harder still: as moves, so do both thresholds and , so a fixed can cross from one regime to another, and and must be shown monotone within each regime and across the switches. Within the interior regime depends on both directly and through , so differentiating the closed form does not by itself give the sign.
All parameters are explicit real numbers; every optimum is taken over , , never over . The page's ranges are , , , . The following are added and disclosed in each item: everywhere (otherwise and (6) divide by zero and no maximizer exists); and in Theorem 1 and the App. A.2 summary (formula (5) divides by ); in Proposition 1 and Lemma 2 (the adversary mass ); in Lemma 2.
Three conventions are fixed. First, for every , the paper's value at where (3) is . Second, whenever , the page's own reading of the infinite square root in (5). Third, is written as , so that at . Using Lean's at either of the first two places makes Theorem 1 false, not trivial, and is ruled out by these definitions. Theorem 1 asserts that is a maximizer: uniqueness fails at , . Monotonicity is MonotoneOn on with fixed; a Monotone statement with junk values outside would not be the paper's claim.
A complete development needs only real analysis from Mathlib: one-variable calculus for the best responses, square-root and absolute-value manipulations for the closed form, and a profit comparison across regimes. The best-response lemmas are reusable for the companion mission on the social optimum. Contributions of proofs of any milestone, and of auxiliary lemmas such as , are welcome.
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.In Bayesian persuasion a sender who observes the state of the world commits to a signaling scheme, a receiver updates her belief by Bayes' rule and acts, and the sender chooses the scheme that maximizes her own expected payoff (Kamenica and Gentzkow 2011). The classical theory assumes the receiver maximizes expected utility, so her payoff is linear in her belief. Many applications violate this: a customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold, a commuter who values route reliability, a buyer who dislikes uncertainty about a product. Anunrojwong, Iyer and Lingenbrink (arXiv:2208.03758v3) call such receivers risk-conscious: the receiver's utility of action at belief is an arbitrary function of .
The paper's first result reduces the sender's problem, an optimization over distributions of posteriors, to a finite-dimensional convex program (program (7)). This mission concerns its second main result: in the practically important binary persuasion setting (two actions, the sender always weakly prefers action ), when the region of beliefs at which the receiver rejects action is convex, program (7) collapses further to a linear program whose feasible region is the convex hull of finitely many explicit beliefs.
Let be a finite set of states and the simplex of beliefs, with the Euclidean topology. For , is the point-mass belief at ; states are identified with their point masses. The prior is . The receiver has actions and utility . The optimality regions are
and the differential utility is , so and inside . The sender's utility is with for every .
Two assumptions are used.
From these data the paper builds finitely many beliefs. and are the states where action , respectively , is optimal under full information, and the states where action is uniquely optimal. For and ,
the mixture of and with the most weight on at which action is still optimal, and .
A candidate solution is a pair of vectors in , with the joint probability of state and action . The sender's objective is . Program (7) maximizes it subject to and ; program (10) subject to , and .
Under Assumptions 1 and 2, with for all :
Together these say that (7) and (10) have the same optimal value and every optimal solution of (10) is optimal for (7): (7) "can be optimized by solving" (10).
Theorem 3 replaces an optimization over a convex set described only implicitly through by a linear program over an explicit polytope. It identifies a canonical signal set: irrespective of the prior, an optimal scheme only needs to induce beliefs in , that is, either reveal the state or leave the receiver uncertain between one state of and one of . Lemma 7 gives a simple full-persuasion test, , and Proposition 3 a threshold structure of the induced actions that the paper uses in its queueing application. For expected-utility receivers the corresponding statements reduce to classical facts about concavification; the content here is that they survive non-linear utilities under a single convexity condition.
On the formal side, the results are proved in the paper and nothing about them is machine-checked. A complete development would give a verified reduction of a family of non-linear persuasion problems to linear programs, and a reusable library of convex-hull facts on the simplex (decompositions of the simplex into hulls of point masses and segment points). The formalization also corrects the paper at one point: the proof of Theorem 3 asserts that every optimal solution of (7) is feasible for (10), which fails when the sender is indifferent between actions in some state; the goal is stated in the form the proof establishes.
The inclusion of (10)'s feasible region in (7)'s is immediate once . The content lies in the converse: is an arbitrary closed set whose complement in the simplex is convex, and one must show that every point of is a convex combination of point masses in and the boundary points on the edges of the simplex. The natural first idea, to argue with extreme points of , does not work directly: need not be convex, its convex hull need not be closed a priori, and the extreme points of are not in general on edges of the simplex. Assumption 2 constrains only the complement of , so it has to be transported to a statement about itself. A second difficulty is that in a solution of (7) may put weight on states in or on interior beliefs, and it must be moved to without lowering the objective.
Ω → ℝ with [Fintype Ω] [DecidableEq Ω]; is Mathlib's stdSimplex ℝ Ω; is Pi.single ω 1; actions are Fin 2; is convexHull ℝ; is the zero vector.ρ : (Ω → ℝ) → Fin 2 → ℝ, and is defined from it by Eq. (1), intersected with the simplex; values of ρ off the simplex are irrelevant. Assumption 1 is IsClosed (P ρ a) for both actions.sSup, used only for , , where the set contains and is bounded by .t : Fin 2 → Ω → ℝ with a common objective. Theorem 3 is stated as (i) and (ii) above, never through a supremum of objective values. A formalization in which (10) only needs to have some feasible point, or in which the supremum of an empty or unbounded set of values is compared, would be trivial or meaningless and is not the target.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.
Personal data lets a firm tailor its product to each customer, and the same data exposes the customer to the risk of a breach. The EU's General Data Protection Regulation (GDPR, 2018) and the California Consumer Privacy Act give consumers rights over that data. Data collection must be opted into separately from the purchase, and stored data must be erased on request. Ke and Sudhir (SSRN 3643979; Management Science 2022, doi:10.1287/mnsc.2022.4614) build a two-period model of a data-driven market to ask what these rights do to prices, purchases, profits and consumer surplus.
To isolate the effect of privacy rights, the paper needs the equilibrium of the same market without them. That equilibrium is its Proposition 2, the benchmark of §3.2. Every comparison in §3.3 (segmentation, prices, profit, consumer surplus, Corollaries 1–3) contrasts it with the equilibrium under privacy rights (Proposition 1, the companion mission of this series).
A monopolist sells a basic good over two periods. A unit mass of consumers has valuations uniform on , and the outside option is worth in each period. Firm and consumers discount the second period by . A consumer values a personalized good at , where equals or with probability each, . She learns her only at the start of period 2, and the firm never observes it. Write
The paper keeps Assumption 1, , throughout.
No privacy rights. A first-period purchase reveals to the firm, and the consumer bears an expected breach cost in every period the firm holds her data. The data cannot be erased, so a first-period buyer bears in period 2 as well, whatever she does then. In period 2 the firm offers each past buyer the personalized good at a price tailored to her valuation, and offers the basic good at a price to those who did not buy in period 1. A non-buyer who buys the basic good in period 2 also bears .
The firm chooses , then as a function of , and . Consumers choose whether to buy in period 1, anticipating the second-period prices. An equilibrium satisfies four conditions:
Let
Under the standing assumptions and Assumption 1 there is an equilibrium with the following outcome in each regime.
The closed forms , , , , are the paper's (pp. 49–51).
The appendix proof (pp. 48–51) supplies the steps, in order:
Proposition 2 describes how a data market behaves when the firm owns the data. A consumer who buys is locked in: the firm extracts the low type's full valuation of personalization, and both types keep buying. Consumers anticipate this hold-up, so first-period demand shrinks. Once , the firm no longer sells the basic good in period 2, and the market becomes "now or never". Once it closes. The paper's comparisons of segmentation, prices, profit and consumer surplus with and without GDPR rights all start from these regimes.
Formalizing it gives the platform a two-period equilibrium with data lock-in. That equilibrium has its own fixed point: the consumers' threshold depends on the second-period price, and that price depends on the threshold. The result is proved in the paper, partly by first-order conditions ("It is easy to verify that the second-order optimality condition is satisfied"). It has not been machine-checked. Formalizing it also fixes a typo in eq. (7), which prints a stray in the numerator of .
The obvious argument is the paper's: guess threshold strategies, solve the first-order conditions, read off the regimes. Each step is calculus, but an equilibrium must hold at every history, not only along the guessed path. The solver must exhibit and the consumers' choices after every first-period price, including prices at which nobody or everybody buys. It must show that the consumers' threshold and the firm's are a fixed point at each such price. It must then prove that the firm's first-period price is a global maximizer of a piecewise objective with a kink at . On each side of the kink the objective is a different quadratic, and on the far sides the threshold leaves . The first-order conditions alone show none of this.
The Lean development lives in the namespace GDPRDataMarkets.Benchmark. Its conventions:
Params.Standing, and Assumption 1 is Params.Assumption1. The goal carries both as hypotheses.A formalization in which the profits are the paper's closed forms rather than integrals over the consumers' optimal choices would make the goal calculus. So would one in which the second-period price or the consumers' choices are optimal only on the equilibrium path, or one that drops Assumption 1 or a bullet of the proposition. The statements here do none of these.
Assumption 1 enters the proof only through (p. 49), which makes the optimal personalized price. The milestone for that step assumes exactly this weaker condition.
Infrastructure needed: interval integrals of linear functions, Lebesgue measure of intervals, and maximization of concave quadratics. The equilibrium predicate is reusable for variants of this model, such as other breach-cost structures. Proofs of the milestones in any order are welcome.
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.
Many quantum algorithms end in a measurement that succeeds only with some probability . Two questions follow: how to raise that probability, and how to learn its value. G. Brassard, P. Høyer, M. Mosca and A. Tapp answered both in Quantum Amplitude Amplification and Estimation (arXiv:quant-ph/0005055, 2000; Contemporary Mathematics 305, 2002). Amplitude amplification generalizes Grover's search (Grover 1996) to an arbitrary algorithm and an arbitrary notion of success. Amplitude estimation combines amplification with the quantum Fourier transform to estimate with error of order after applications of , where classical sampling needs order samples. Quantum counting, quantum Monte Carlo integration (Montanaro 2015) and many quantum speedups for statistics and finance rest on this estimation step.
Timeline:
Let be a finite-dimensional Hilbert space with computational basis and a distinguished zero state . A quantum algorithm without measurements is a unitary matrix on , and a Boolean function calls a basis state good when . Write for the splitting into the projections onto the good and the bad subspaces. The initial success probability is , the probability that measuring gives a good state, and is the angle with .
The operator flips the sign of the amplitudes of good states, flips the sign of the amplitude of , and the amplification operator is
For an integer , the quantum Fourier transform is , and the controlled power is . The phase state is , and is the circular distance. The algorithm applies to , measures the first register to obtain , and outputs .
For every positive integer , the event
has probability at least when , and greater than when . If then with certainty. If and is even, then with certainty.
Further statements from the same development are included as companion targets: the success probability after rounds, Theorem 2 (quadratic speedup), Lemma 5 (the phase-generalized ), Theorem 13 (counting) and Corollary 14.
Theorem 12 is the quantitative core of quantum estimation algorithms. Its error bound scales as in the number of applications of , and that scaling is the quadratic speedup behind quantum counting (Theorem 13), quantum mean estimation, and quantum Monte Carlo methods for option pricing and risk analysis. The exact clauses for make the estimator usable as a zero-error test for the existence of a good state.
All results here are proved in the paper and widely reproduced in textbooks; none is open. What the mission adds is a machine-checked account with the paper's constants: , the strict tail bound , and the additive term . It also covers every modulus , not only powers of two, and arbitrary and , not only uniform search. Related statements are posed on the platform but unproved:
QAlgorithms.Nannicini.amplitudeEstimation_error is the special case , , with a bit-string presentation of the algorithm.QAlgorithms.Nannicini.groverOperator_eigenstates states (3)–(4) for an abstract reflection.QAlgorithms.DeWolf.amplitudeAmplification covers (8) and the half of Theorem 2.The Grover theorems already proved on the platform treat a single marked item with a uniform start.
The obvious argument has two parts: rotates a plane by , and phase estimation reads off . Neither part settles the measurement law. The outcome probability is a sum over the second register of the squared amplitudes of an entangled state. Reducing it to two independent phase-estimation laws requires orthonormality of , and that holds only for . The goal does not assume this: the degenerate cases , where do not exist, must be handled separately.
On the phase-estimation side, the tail bound for must be strict and must hold for every . The bound for relies on a minimization over that needs , while the goal has no such hypothesis, so the small cases need their own argument. Finally, the second eigenphase appears as , and the matching outcome wraps to at .
States are vectors over a finite type (the paper writes ), operators are matrices, and is Bool. is assumed unitary and is written . The second register is Fin M with ; is the platform's published Fourier matrix ShorAlgorithms.Shared.fourierMatrix (same sign and normalization as (13)), is its conjugate transpose, and is an explicit matrix on Fin M × ι. The outcome law is the sum over the second register of squared moduli of the final state, and an event's probability is the sum of the outcome probabilities over it. is computed from , and , and . The goal assumes neither nor , and it keeps the strict inequality for . The step "after step 2, ignoring global phase" is stated with its phase written out.
A formalization that takes or as a free parameter, assumes the mixture form of the outcome law, or reasons about without deriving them from and would make the goal trivial. The statements here do none of these: every quantity is computed from , , and . The clauses "uses exactly evaluations of " (Theorem 12) and "requires exactly evaluations" (Corollary 14) are not formalized, because the matrix model has no oracle whose calls could be counted. Theorem 13 is stated for any unitary sending to the uniform superposition, which includes , as the paper allows on p. 20.
A complete development needs:
The phase-estimation part (Lemma 10, Theorem 11) does not depend on amplification and can be reused by any later formalization of Fourier-based phase estimation. Proofs of individual milestones, and lemmas on Fin M Fourier sums, are welcome.
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.htmlIn inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.
The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.
Costs lie on the unit sphere of , . In period nature presents a feasible set , compact, nonempty and of diameter at most , and a -Lipschitz context . The forward problem with cost has solution set . The decision-maker plays some , nature reveals an expert action for the true cost , and the regret over periods is
The knowledge set is the set of costs in the initial set under which every expert action seen so far was optimal.
The angle between nonzero vectors is , and the uncertainty angle of a set is ; a minimizing is a circumcenter. The initial set is pointed when .
For a positive diagonal and an orthonormal , the ellipsoidal cone is
a cone with axis and elliptical cross-section. The effective difference of period is (and if the difference vanishes).
EllipsoidalCones with parameter starts from the circular cone , a circumcenter of , and plays the axis as proxy cost. With it keeps the cone if
and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.
With there is an absolute constant such that for every , , closed pointed with , , admissible instances and run,
The constant is left unfixed: the shape is the claim, and the proof's explicit constant rests on a step that fails at .
The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.
The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the case of Lemma B-1.
Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.
Costs live in EuclideanSpace ℝ (Fin (m+1)) with , actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. is stored as its diagonal , as a real orthogonal matrix, and is written . Lean periods are -based: Lean period is the paper's period . This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.
Standing assumptions carried by the statements: , , feasible sets nonempty, compact and of diameter at most , contexts -Lipschitz, a closed subset of , . Pinned and disclosed choices:
The run predicate is satisfiable: a circumcenter of a closed nonempty exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of is nonzero. A formalization in which no run exists, or in which may depend on or , does not state Theorem 3.
A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.
Stochastic 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.
Markets organized by platforms (social networks, marketplaces, messaging services) exhibit network effects: a user values a platform more when more users join it. A standing concern in competition policy is that such markets "tip" towards one dominant platform, and the usual remedy proposed is to foster entry. Ekmekci, White and Wu (Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025) develop a tractable model of platform oligopoly in which platforms compete in net fees, the price a user pays net of the interaction value the platform delivers, and use it to examine policy interventions. Their Proposition 4 shows that the intuition "more platforms, less dominance" can fail: with strong network effects, adding a third platform to a duopoly can produce an equilibrium whose leader is larger than any platform of any duopoly equilibrium.
The net-fee approach is the authors' alternative to the "insulated equilibrium" of White and Weyl (2016); the paper's §5 specializes it to Logit demand, where pricing formulas are explicit.
There are platforms and one side of users. Platform charges a net fee ; write . Demand has the Logit form (13): with outside-option weight ,
and in this mission there is no outside option, , so the shares sum to one. Platforms are ex ante identical: common marginal cost and common interaction value . Platform 's profit ((8) with one side) is
the net fee plus the interaction value the platform extracts per user, less cost, times its share. A net-fee equilibrium is a pure-strategy Nash equilibrium: no platform can raise by changing its own net fee to any . Duopoly is , triopoly .
At an equilibrium, each net fee satisfies the Logit pricing formula (14), . For equilibria with one dominant platform of share and equal small platforms of share , the paper reduces the equilibrium conditions to a zero of the characterization function
For : duopoly has an equilibrium, and there exist a triopoly equilibrium and a platform with
The comparison is against every duopoly equilibrium and every platform in it, not against one selected equilibrium.
The result. Proposition 4 is a counterexample to a policy presumption: entry need not reduce concentration in markets with network effects. With a third platform, the two small platforms can split the fringe so thinly that the leader's share rises above anything sustainable in a duopoly. The result identifies an explicit parameter window; together with the companion results on interoperability (Propositions 6 and 7 of the same paper), it frames which interventions reduce dominance in this model.
Formalizing it. The proposition is proved in the paper partly by a numerical check ("we can verify", p. 50), and its printed interval is slightly too wide at the bottom: at the symmetric duopoly equilibrium the paper's own criterion requires . A machine-checked proof would settle the corrected statement, replace the numerical step by an argument, and make the equilibrium characterization through (including the step from first-order conditions to global Nash equilibrium) available for the other results of the series. None of these statements is formalized anywhere to our knowledge.
Three steps resist the obvious argument.
NetFeePlatform.Competition. The definitions file Setting declares the Logit demand demand w t j, the profit profit w c γ lam t j (with an interoperability term , set to throughout this mission), the global Nash predicate IsEquilibrium, and the diversion ratio; GChar declares . Platforms are indexed by Fin J.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.
Large online retailers such as Amazon, Walmart and JD.com run a retailer-led marketplace: they sell products on their own account and, on the same storefront, host independent third-party sellers whose sales they tax. How the platform charges those sellers is a live question for competition authorities and for the platforms themselves. Real marketplaces mostly use ad valorem fees (a percentage of the seller's revenue, the "referral fee"), sometimes together with per-item charges. Hervas-Drane and Shelegia (Management Science, 2025) build a model of such a marketplace in which the platform chooses its fee, steers part of the demand, and decides which products to sell itself under a capacity constraint. In their Appendix B.3 they ask whether a per-unit fee would serve the platform better than the ad valorem fee, and answer that it would not: provided the per-unit fee is not a subsidy, the platform sets it to zero (Lemma B.1). The comparison echoes the classical public-finance question of ad valorem versus specific taxation under imperfect competition (Suits and Musgrave, 1953).
There is a unit mass of products, indexed by their value to consumers, distributed by a probability measure (the CDF of the paper) on , where is the common marginal cost of supplying a unit. Each product is its own market, with a unit mass of unit-demand consumers and one potential third-party seller . The monopolist :
The game has three stages: announces ; each decides whether to enter, then chooses which products to sell; then prices are set. In a product sold by alone (SBT) she charges and earns . In a product sold by both (SBMT), serves the steered consumers at and charges
so earns . A product sold by alone (SBM) earns him . Sellers enter the products of the marketplace set , that is when .
An allocation is a measurable set of products with . 's profit adds over , over and over , and his profit at fees is
For every maximiser of over with ,
The goal asserts nothing about existence of a maximiser or about the value of ; it constrains every maximiser.
The result. Lemma B.1 justifies restricting the platform's instrument to an ad valorem fee, which is how the paper's main analysis (entry modes, the positive optimal fee, fee regulation) proceeds. It also isolates a mechanism: a per-unit fee raises the seller's effective marginal cost and so the price she must charge, while an ad valorem fee with the same entry threshold extracts more from high-value products. The paper notes on p. 19 that once subsidies are allowed the conclusion reverses; that is a different optimisation and not part of this mission.
Formalizing it. The result is proved on paper in a short argument; it has no machine-checked proof. A formal proof must make precise what the paper leaves implicit: that is a supremum over all allocations, re-optimised after a fee change, that the profit gain from the fee switch is strictly positive and survives the supremum, and which degenerate corners (a foreclosed marketplace, full capacity with full steering) must be excluded. The model file is shared in form with the series' two other missions, which formalize the paper's entry-mode theorem (Proposition 2) and the positivity of the optimal ad valorem fee (Lemma 2).
The milestone algebra is elementary. The difficulty is in passing from a pointwise gain to the value function. The fee switch raises 's revenue on every marketplace product above for a fixed allocation; is a supremum over allocations, so a pointwise strict gain does not by itself give a strict gain of the supremum. When the gain is bounded below uniformly over allocations, through the positive mass of . When the SBMT gain vanishes, and an allocation that covers almost all marketplace products gains nothing; ruling out that the supremum is approached by such allocations requires comparing with a different fee pair, and uses that has a density and full support. The naive reading, "keep 's allocation fixed and compare", only gives a lower bound on the new value and is not itself a proof of optimality failure.
Lean conventions, all in the namespace RetailerMarketplace.UnitFee:
μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0, μ ≪ volume (a density), Integrable (fun v => v) μ (finite mean, never stated in the paper but needed for profits to be finite), and full support on , ∀ a b, c ≤ a → a < b → 0 < μ (Set.Ioo a b) (the reading of in the paper's display (3)).0 < c is a standing hypothesis (the paper's and " such that " presuppose it); is Assumption 1; .vT and the switched fee appear only under and .PiM is sSup of the profits of all measurable allocations of mass at most ; under integrability the set is nonempty and bounded above, so this is a genuine supremum.A formalization that fixes 's allocation in the definition of , restricts allocations to intervals, takes the supremum over a set that may be unbounded, or replaces "every maximiser has " by "some pair beats " would trivialize or change the statement, and is ruled out.
A complete development needs set integrals over the marketplace set, the bathtub-type comparison of allocations, and order properties of sSup on ℝ. The model file and the milestone lemmas are reusable for any fee-design question in the same model. Proofs of the milestones, of the goal, and of intermediate lemmas about PiM (monotonicity in the fees, strict improvement under the fee switch) are welcome.
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.
Affirmative action policies are usually designed reductively: one adjustment for women, another for a racial minority, a third for applicants from low-income families. An applicant who belongs to several categories gets the combined adjustments. A long literature in sociology and law, beginning with Crenshaw's account of intersectionality (1989), argues that people at the intersection of several disadvantaged categories (for instance Black women) can stay underrepresented even when every single category is proportionally represented. Carvalho, Pradelski and Williams, Intersectionality: Affirmative Action with Multidimensional Identities (Management Science, 2025), give this debate a decision-theoretic model. They ask whether any policy that treats identity dimensions independently can achieve proportional representation of every intersectional group.
Their first main result answers that question for a general class of score adjustments and for generic score distributions. This mission formalizes that result, Theorem 1, together with the lemmas its proof uses.
A decision maker admits a share of a unit-mass pool of applicants. Each applicant has a score in an interval and an identity , with . Category is the set of identities with . Write and for the vectors of zeros and ones and for the -th basis vector. The identity equals when the sum is computed coordinatewise in the integers.
The population is a probability measure on , with marginal masses . The space consists of those whose conditional score laws are continuous (atomless) and have full support on . carries the relative weak topology, the topology of weak convergence of probability measures.
A policy family is a set of strictly increasing bijections that is rich (for all some has ) and commutative (). Additive shifts on are an example. A policy assigns to each identity a map . Given a threshold , an applicant of group is accepted when , subject to the capacity constraint
The accepted share of is , the fraction of the accepted who belong to . The outcome is representative if for every (Definition 2). A policy is nonintersectional if implies , and intersectional otherwise (Definition 1). Nonintersectional policies are the reductive ones: is the composition of the maps over the categories that belongs to.
A property is generic in if it holds on a dense open subset of . Theorem 1 states: there is a dense open such that for every ,
"Yields a representative outcome" means that some threshold satisfies the capacity constraint at level and gives for every . Nothing about is fixed beyond richness and commutativity, and nothing about beyond membership in .
The result. Theorem 1 separates two classes of policy. The reductive class, which covers the way most affirmative action programmes are written, cannot generically deliver proportional representation of intersectional groups, however its category-wise adjustments are tuned. A policy that adjusts each intersectional group separately can. The negative part holds for every rich commutative family, not only for additive or multiplicative adjustments, so the impossibility does not come from a particular functional form. The later results of the paper build on this one. They measure how badly reductive policies fail, give the nongeneric conditions under which they succeed (Proposition 3, which is the subject of the companion mission), and treat imperfectly intersectional policies.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked version exists. A formalization has to make several things precise:
The paper's proof of Lemma 2 also concludes with a formula valid only for the additive family (p. 23), so a complete formal proof would supply the missing argument for a general .
Part (b) and the necessary conditions behind part (a) follow from the definitions. The hard step is genericity (Lemma 2). Openness requires the quantiles to depend continuously on in the weak topology. It also requires the map to be continuous, where each is itself determined by and . The obvious argument writes this map as an explicit formula, , and that formula holds only for additive shifts. For a general rich commutative family, continuity of the transport map must come from the structure of as a group of homeomorphisms of an interval acting freely and transitively. Density requires perturbing the law of group while keeping the perturbation inside . This is where enters: for , and there is nothing to perturb independently.
The Lean development fixes the following conventions.
Fin n → Bool, and is checked coordinatewise on Bool.toNat.ProbabilityMeasures on , whose Mathlib topology is that of weak convergence. is the subtype of measures for which every group of positive mass has no atoms and positive mass on every nonempty open subinterval of .Several trivializing formalizations are ruled out:
A complete development needs:
The first two are reusable well beyond this mission. Contributions to any milestone are welcome, and proofs of the quantile-continuity facts as standalone lemmas are especially useful.
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.