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?
An experience good is a product whose value a consumer learns only by consuming it: a new streaming service, a meal-kit brand, a novel drug. When two firms launch competing experience goods in a new product category, every first-period sale does two things. It earns a first-period margin, and it creates a repeat consumer whom the firm can price to in the second period, while the rival's first-period buyers become potential switching consumers. When firms can price by purchase history (behaviour-based pricing), the second-period prices to repeat and switching consumers differ, and the value of a first-period sale is set by how profitable each group is.
Z. Chen, C. Stanton and C. Thomas (Management Science 70(6), 2024) study this competition when trying one good is informative about the other (an information spillover, of strength ). Their Theorem 1 isolates what drives profits in every symmetric equilibrium, whatever the second-period equilibrium looks like: competition for first-period share pushes the first-period price exactly to the level at which a firm's total profit equals what it would have earned from switching consumers alone. The result connects to the literature on experience goods and introductory pricing (Bergemann and Välimäki, 2006) and on behaviour-based price discrimination (Fudenberg and Villas-Boas, 2006), where the role of switchers is usually derived in models without spillovers.
Two firms and have a common marginal cost . Firms and consumers discount the second period by . A unit mass of ex-ante identical consumers buys at most one unit per period.
The second period has already been solved. A firm earns in the second period per unit of its own first-period buyers (repeat consumers) and per unit of the rival's first-period buyers (switching consumers). Both are independent of first-period market shares, because consumers choose in the first period before learning their values.
In the first period the firms set prices simultaneously. Buying either good at price gives a consumer present surplus , where is the common gross value of a first-period purchase including its option value for the second period; not buying gives . Firm 's first-period share is if and , a given tie share ( for , for , with ) if the two surpluses are equal and at least , and otherwise. Firm 's two-period profit is
A price is a symmetric equilibrium when no firm can raise its profit by any unilateral deviation from to another real price.
For every symmetric price at which consumers buy (),
and in that equilibrium each firm earns , for every tie share .
Theorem 1 says that in any symmetric equilibrium a firm's total profit is the discounted profit from switching consumers. The first-period price fully dissipates the extra value of a repeat consumer over a switcher. Consequences drawn in the paper include: profits are positive only if the second-period equilibrium has switchers (); the result holds for every spillover strength, including ; and with firms and two periods (Appendix D) profits fall to zero. The theorem is the backbone of the paper's later comparative statics in .
The result is proved in the paper; nothing here is open. The mission produces the first machine-checked version of the argument, stated for both firms, for any real second-period profits, and for both directions: a covered symmetric price is an equilibrium exactly when it equals . To our knowledge no part of it has been formalized before.
The mathematics is elementary, and the difficulty is in the discontinuities. Demand jumps between , the tie share and as a price crosses the rival's, so profit is not continuous in a firm's own price. Undercutting by yields a profit that approaches but never reaches , so the "only if" direction cannot pick a single best deviation. It has to use deviations by arbitrarily small . The corner tie shares give one firm zero share at the symmetric profile, so the identity has to be pinned down by combining both firms' incentives, not one firm's. The printed proof also carries a slip (below) that a transcription would turn into a false statement.
Everything lives in the namespace SpilloverDuopoly.Switchers. The single definition file Model holds a structure Params (fields c, delta, lam, piR, piS, V, u0, all real), the predicate Standing (, , ), the surplus CS, the shares shareA, shareB, the profits profitA, profitB, the predicate IsSymEq and the price pStar. IsSymEq uses the platform's published two-player pure Nash predicate CrossLicensing.ExPost.IsNE with both strategy sets equal to .
Committed conventions:
The equilibrium predicate quantifies over every real deviation for each firm. It is not defined through or through the two deviations the proof checks, and the shares come from surplus comparisons, not from a "cheaper wins" rule. So the goal cannot be closed by unfolding definitions. Contributions welcome: proofs of the milestones and the goal, and a formalization of the paper's second-period equilibria (Proposition 1, Corollary 1) that would instantiate .
A drug regulator approves a candidate drug when its clinical trial rejects the null hypothesis of no effect at a fixed significance level . FDA guidelines recommend the same threshold, , for every disease (Bravo, Corcoran and Long, p. 2). A uniform threshold balances the wrong errors for some diseases. For a severe disease with no available treatment, wrongly rejecting an effective drug (a type II error) can cost far more than wrongly approving an ineffective one (a type I error). For a crowded therapeutic area the balance is the other way. Regulators have responded with expedited programmes (Fast Track, Breakthrough Therapy, Accelerated Approval), and decision-analytic work has asked how trial design should account for the harm of each error (Montazerhodjat, Chaudhuri, Sargent and Lo, 2017).
Bravo, Corcoran and Long (2021) add the drug development pipeline and the market to this question. Candidate drugs arrive in clinical trials, some are abandoned, the rest are reviewed, and approved drugs stay on the market for a while. The optimal then depends on operational quantities such as trial duration and attrition, and not only on the costs of the two errors. The paper's main analytical result is a set of comparative statics. The optimal level is higher for diseases with long trials, high attrition and few compounds in development. This mission formalizes that result together with the analytical steps of its proof.
A two-armed trial with patients per arm measures an outcome of standard deviation . The information of the sample is . Under the alternative hypothesis, which says the drug has effect , the Wald statistic is approximately normal with mean and variance one. A drug is effective with prior probability . With the standard normal distribution function, the probabilities that a drug is approved and effective (AE), approved and ineffective (AI), or rejected and effective (RE) are
Drugs enter trials at rate . Each trial is a race between completion at rate and abandonment at rate , so drugs reach review at rate , and the outcome streams have rates . Approved effective drugs fall into one of therapeutic classes and stay on the market at exit rate . Approved ineffective drugs leave at rate . With and , the paper's expected numbers of effective and ineffective drugs on the market are and .
Each effective drug on the market yields health benefit and each ineffective one costs , valued at per unit. Approving an effective drug yields , approving an ineffective drug costs , and rejecting an effective drug costs . The expected net benefit is
and an optimal approval policy is a maximizer of over .
The optimal approval policy is
Each clause compares two parameter vectors that differ in one parameter only.
Proposition 1 turns the model into policy statements. The approval bar should be lower for diseases with long trials (small ), high attrition (large ) or few compounds in development (small ), and for drugs whose rejection is costly. It should be higher where ineffective drugs linger on the market (small ). Part (c) shows that the natural intuition fails in general: more promising candidates (larger ) and longer effective market lives (smaller ) call for more lenient approval only when the market for effective drugs is not crowded, . Figure 3 of the paper shows decreasing in over most of the range when the condition fails. The paper's numerical study estimates for many diseases, and these monotonicity properties are what make those estimates readable.
The result is proved in the paper; nothing here is open. No machine-checked version of Theorem 1 or Proposition 1 exists. A formalization needs to supply what the paper calls "direct computation" and "straightforward differentiation": the concavity of the Gaussian power curve, the interior first-order condition, and the implicit-function argument. The printed derivatives (A.19) and (A.20) drop positive factors, and the formal statements give the corrected derivatives.
The obvious argument is to differentiate the first-order condition. That needs to be interior, unique and differentiable in each parameter, and the paper asserts all three without proof. Interiority depends on the behaviour of the power curve's slope at the endpoints: it tends to as and to as . That in turn needs facts about the normal quantile that Mathlib does not package.
For , and , has no sign at a general . Its sign is known only at the optimum, through the first-order condition. A pointwise sign argument therefore does not work, and one has to argue along the optimal path. In part (c) the side condition is a condition at the optimum, so it must hold at every parameter value between the two being compared. Checking it at the two endpoints only does not give the monotonicity.
All declarations live in the namespace FlexApproval.Statics. and on are the published Cohen2019.Robust.Phi and PhiInvReal. A parameter vector is a structure of real fields plus . The model fixes the following conventions:
deriv. Derivatives in a parameter are stated with HasDerivAt and an explicit value, never as a bare deriv sign, which would hold trivially wherever the derivative fails to exist. The derivative in is taken through , since .The optimal policy is never defined by the first-order condition (5). Doing so would make Theorem 1 a tautology and the comparative statics a statement about a formula. Every statement quantifies over maximizers of .
Useful infrastructure beyond this mission: smoothness and the endpoint limits of the normal quantile, concavity of Gaussian power curves (ROC curves of the equal-variance normal model), and a monotone comparative-statics lemma for strictly concave objectives. Proofs of individual milestones are welcome, and so are alternative routes to Proposition 1 that avoid the implicit function theorem.
Not formalized: Proposition 2 (ordering of in ), Proposition 3 (monotonicity and diminishing increments of the optimal value in ), the queueing derivation of (4), and the numerical study of §5.
Negative advertising (comparative advertising that points to a rival's flaw) is used both in product markets and in political campaigns, and its regulation differs across jurisdictions: until the 1990s it was not permitted in numerous countries of the European Union (Anderson and Renault, 2009). Many models of advertising take the products' positions as given. Bostanci, Yildirim and Jerath (Management Science, 2023) ask what happens when a firm chooses its product position knowing which advertising war that position will invite. Their main finding, Proposition 2, is that permitting negative advertising can make an entrant give up differentiation: it places its product next to the incumbent's, and both firms then advertise positively.
The mechanism is a spillover effect: products positioned close together tend to share attributes, so revealing that the rival's product has a flaw also raises the probability that one's own product has it. Co-location therefore disarms negative advertising.
There are two locations, and , each with a unit mass of consumers whose ideal product sits there. The incumbent (firm 1) is at ; the entrant (firm 2) chooses . A consumer at buying product at gets utility , where the distance is at the own location and at the other, and the reservation value is uniform on . Not buying gives .
Each product has a positive attribute , equal to with probability and otherwise, and a negative attribute , equal to with probability and otherwise; . The normalization makes . Under co-location ; apart, the attributes are independent.
The timeline: the entrant positions; nature draws the type profile , seen by the firms only; each firm simultaneously chooses (advertise its own positive attribute, advertise the rival's negative attribute, or nothing), truthfully; consumers update their beliefs by Bayes' rule and buy. The price is normalized to 1, so a firm's payoff is its demand. A perfect Bayesian equilibrium (PBE) consists of the entrant's location, advertising strategies at both locations, and consumer beliefs, such that consumers choose optimally, the ads form a Nash equilibrium of every advertising sub-game, the location maximizes the entrant's expected demand, and beliefs follow Bayes' rule.
A firm is a weak opponent of if it cannot advertise ( and ), and a strong opponent otherwise.
Under the standing assumptions, Assumption 1′ (, ), and
there is a PBE in which the entrant co-locates, every firm holding the positive attribute advertises it after co-location, and after locating apart a firm that can attack a strong opponent does so.
The result links two decisions usually studied separately. Positioning models predict differentiation to soften competition; Proposition 2 shows that when the advertising stage follows positioning, the entrant may prefer to co-locate, and that banning negative advertising (Proposition 1 of the paper) changes the positioning outcome. This bears on the regulation of comparative advertising and on the welfare comparisons of §4 of the paper.
The formalization produces a checked version of a result whose printed parameter region is wrong. The printed conditions are not sufficient: at , , , , , , every printed condition of the proof holds, yet the entrant earns by co-locating and by locating apart, so the described profile is not an equilibrium. The mission states the corrected theorem, and a machine-checked proof would settle that the corrected region is right. The result has not been formalized before.
The obvious argument fills in Table 1 and compares demands case by case, which is what the paper does; its slips sit in exactly that bookkeeping. Two places need care. First, demand is piecewise linear in the posteriors: whether a firm steals the rival's location depends on the sign of , and ties are broken differently under co-location (equal split) and apart (closer product), so each lemma is a case analysis whose boundaries matter (Lemma 4's printed strict condition fails at its boundary). Second, the entrant's location payoff is an expectation over 16 type profiles under a correlated prior; the paper's two closed forms both carry errors, so the comparison has to be recomputed rather than copied. The goal then requires checking every advertising sub-game at both locations, including those off the equilibrium path.
Everything is finite and real-valued; no measure theory is needed. Firms, locations and ads are small inductive types; a type profile is a pair of Boolean functions; the prior is the product of two correlated Bernoulli pairs. Consumer behaviour is built into the demand function: consumers choose the product with the larger posterior expected attribute minus distance, buy iff the reservation value is at least minus that maximum, and break ties as in footnote 11 of the paper. The uniform cdf is clipped to . Beliefs are probability mass functions on type profiles; the PBE definition requires Bayes' rule wherever the observed outcome has positive prior probability, and only consistency with the truthful ads elsewhere.
Corrections relative to the page, all disclosed in the item statements: in Assumption 1 (printed ); the added condition (the proof claims this region is excluded, but it is not, and there the profile fails); ; (A5′), (A6′), (A1d′) in place of (A5), (A6), (A1d); and Lemma 4 with a weak inequality.
The goal is an existence statement over all profiles satisfying every PBE condition; beliefs are computed by Bayes' rule, not defined as Table 1's numbers, and demand comes from consumer choice, not from the paper's demand tables, so neither the table nor the closed forms hold by definition.
All definitions live in one file, NegAdPosition.CoLocate.Model. Proofs of the milestones in any order are welcome; Table 1 and the closed forms are mechanical but long, and reusable tactics for sums over the 16 type profiles would help every item.
A seller choosing between a first-price auction (FPA) and a second-price auction (SPA) needs to know whether the payment rule changes expected revenue. In the classical independent private-value benchmark, the two formats can be revenue equivalent. Balzer and Rosato examine a different setting: a bidder’s value depends on other bidders’ private signals, and the bidder dislikes outcomes that fall below a reference lottery formed from the bid she chooses. Their result gives a precise revenue ranking under these preferences. The paper was published online in Management Science in 2020 in its Articles in Advance pagination Balzer and Rosato.
The question matters because a payment rule changes both what a winner pays and which monetary outcomes she anticipates. In an FPA the winner pays her own bid. In an SPA she pays the highest opposing bid, so her payment varies with competitors’ signals even when she wins. Balzer and Rosato distinguish the risk of winning versus losing, which they call extensive risk, from variation in value or payment among winning outcomes, which they call intensive risk. Their analysis asks how these risks affect bidding and the seller’s expected receipts Balzer and Rosato, §§3–4.
There are bidders. Each observes a signal drawn independently from a continuously differentiable distribution on , where and the density is strictly positive. Bidder values the item at . The value is nonnegative, increasing in every signal, strictly increasing in the bidder’s own signal, twice continuously differentiable, and symmetric in opponents’ signals. The distribution of the highest of the opposing signals has cumulative distribution and density Balzer and Rosato, §2.1 and §3.1.
A realized outcome is a value-payment pair . Its comparison point is another such pair . Gain–loss utility is for and for , with denoting the item and money dimensions. Here , , and . Total utility is
For outcome lottery and reference lottery , expected utility averages this expression over an independent draw from each lottery. Under a choice-acclimating personal equilibrium (CPE), a type assesses each possible nonnegative bid against the lottery that the same bid induces. A symmetric increasing strategy is a CPE when bidding maximizes this self-referenced expected utility for every type. The paper maintains Assumption 1, , through its CPE results Balzer and Rosato, Definition 1 and Assumption 1.
The main target is Corollary 1. For any symmetric CPE strategies and in the FPA and SPA, respectively, let and be the expectation of the sum of all bidders’ payments. Then
The milestone list follows the paper’s CPE results: the direct-utility representations (10) and (12), existence and bid formulas for every symmetric equilibrium in Propositions 7 and 9, the common equilibrium-utility identity in the proof of Proposition 11, and Proposition 11’s comparison of utilities and payments. These targets retain the distinction between a lottery-based preference definition and the formulas derived from it Balzer and Rosato, pp. 10–11 and Appendix.
The corollary tells the seller which format yields more expected revenue within this model. When bidders have no loss aversion over money, the two formats yield the same revenue even though values are interdependent. With positive monetary loss aversion, the FPA yields strictly more. Proposition 11 gives the bidder-level comparison behind this statement: equilibrium utility is the same in both formats, while each type above the lowest pays more in expectation in the FPA when Balzer and Rosato, Proposition 11 and Corollary 1.
The result is proved in the paper but is not yet machine-checked in this mission. A completed formalization would connect the primitive gain–loss utility, lottery construction, CPE incentive condition, interim payment comparison, and ex ante revenue ranking. The auction data module can also support other results about independent signals and interdependent values; the loss-aversion module records the additional preference and equilibrium structure.
The expected utility of a bid changes when the bid changes because the reference lottery changes with it. Treating the comparison point as fixed would describe a different equilibrium concept. An SPA also exposes winners to variation in the payment itself, which is absent from the FPA. Thus the two formats cannot be compared merely by inserting the same bid into different payment formulas. The paper’s two direct-utility displays and its payment comparison are separate substantive targets Balzer and Rosato, §4 and proof of Proposition 11.
Lean uses real-valued signals, values, bids, and payments, and exactly bidders, so an opponent always exists. The signal law is a density-weighted measure on ; opponent and all-bidder signals use product laws. Strategies are measurable, nonnegative, and strictly increasing on the signal support. The model requires measurable values so mapped lotteries are genuine measures. A bid wins only when it strictly exceeds every opposing bid; ties have probability zero under the stated atomless signal law and strict monotonicity. Values of strategies outside the support do not affect the lotteries.
Revenue is defined directly as the expectation of the sum of payments, rather than by the payment formulas that the results seek to establish. Likewise, CPE is the incentive inequality over every nonnegative bid, and expected utility is built from the primitive outcome and reference lotteries. The direct-utility formulas are theorem targets, not definitions. The conditional value is used only when , where ; the bid formulas (11) and (13) are stated on because their displayed denominators vanish at the lower endpoint for some bidder counts.
The paper writes the intensive-risk term with a conditional density of value, although that density need not exist for private values. Lean instead uses a double expectation over the winning-signal region. The paper’s printed prefactor in (10) is inconsistent with a reference lottery induced by the deviation; the formalization uses . This correction is recorded on both representation milestones. Contributions toward the measure identities, equilibrium existence, envelope identity, and bidder-level payment comparison are all within scope.
A cryptocurrency user can attach a fee to a transaction, and a miner can choose which waiting transactions enter the next block. When the most valuable waiting transactions compete for a limited number of places, the fee rule affects both the user's bid and the amount the user expects to pay. Basu, Easley, O'Hara and Sirer study a protocol that charges every included transaction the minimum included fee. This makes the fee visible from the block itself, but it also lets a bidder affect the price when that bidder supplies the lowest winning bid. Their Result 3 asks how much this incentive matters when many users are active. Basu et al., §4 and Result 3, pp. 13–16.
The result is a useful distinction for the design of a multi-unit fee auction. Truthful bidding can fail as an exact dominant strategy even while the maximum expected benefit from deviating becomes small in a large active market. The paper treats this as one part of a proposed fee mechanism; the claims about miner payments, fill penalties and longer-run blockchain behavior are separate from Result 3. Basu et al., §4, pp. 13–16.
A block has places for transactions. There are other active users besides the bidder being studied, with . Each user's value for inclusion in the current block and each allowed bid lie in . The others' truthful bids form a vector . Write for its th highest entry, counting repeated values. The rule places the highest bids in the block. A winning bidder pays the lowest of those bids. Basu et al., §3, pp. 10–11; §4, pp. 13–16.
For a bidder with value who bids , let be the current-block payoff: value less the charged fee when included, and zero otherwise. A bid strictly above wins; the bidder then pays . A bid equal to loses under the tie convention used here. The strategic gain is the best admissible payoff minus the payoff from bidding one's value,
The model draws active users' values independently from a common continuous density on , with throughout that interval. Thus the joint law of is the product law of draws. A bidder knows their own value and the number of active users, but does not observe the other users' values or bids before choosing their own bid. The expected strategic gain therefore fixes the bid before averaging over the others' values :
The goal is Result 3. Its first clause says that truthful bidding fails to be a dominant strategy: for every admissible number of other active users, there is a valid profile and an admissible deviation with higher current-block payoff. Its second clause concerns the expected strategic gain when the others bid truthfully:
The quantifier over makes the convergence uniform across the bidder's possible values. It follows the paper's claim for “any bidder” and the value-independent upper bound stated immediately before Result 3. Basu et al., Result 3, p. 16; proof, pp. 21–22.
The milestone list records the statements in the paper's proof: an explicit profitable deviation when ; no profitable bid below the lower threshold; the two possible prices for a winning slot; the pointwise bound ; the bound ; and the assertion that this expected spacing tends to zero as grows. These are intermediate targets, not replacements for the goal about strategic gain. Basu et al., proof of Result 3, pp. 21–22.
The theorem identifies what the mechanism does and does not guarantee for a user. It rules out an exact dominant-strategy interpretation of truthful bidding for the minimum included fee protocol, while bounding the incentive to depart from truthfulness in a sufficiently large active market. Without the first clause, a claim of truthfulness would be misleading; without the second, the protocol would lack the paper's quantitative reason to expect truthful behavior to be nearly optimal when participation is high. Basu et al., §4, p. 16.
The paper gives the mathematical result and an appendix argument. This mission asks for a machine-checked account of that result, including the auction payoff, the order statistics, and the probability statement; these claims are open Lean targets in the proposed mission, not already machine-checked results. The definitions of the finite order statistic and of gain from an admissible deviation can be reused in later multi-unit auction formalizations. The density and product-law interface may also support other bounded-support order-statistic results.
A pointwise payoff comparison is not by itself an asymptotic statement. The gain depends on the entire vector of other bids through two adjacent order statistics and on a supremum over all allowed bids. Turning its bound into a statement about expectations requires those random quantities to be measurable and integrable. The spacing between the st and th highest of draws then has to vanish in expectation for the stated class of densities. Merely showing that this spacing is nonnegative or at most gives no decay with . Basu et al., proof of Result 3, p. 22.
There is also a boundary issue in the auction itself: a bid tied at the last included position requires a specified outcome. The protocol states the payment for included users but does not prescribe a complete deterministic tie rule for this one-bidder analysis. The chosen strict inclusion threshold makes every payoff a total function, and the continuous value law makes ties irrelevant to the expected-gain limit.
Lean represents the other active users as Fin m → ℝ, their th highest value as a real supremum defining kthHighest, and their i.i.d. values as Measure.pi of a density law supported on . The density assumption includes , continuity on that interval, , and total integral one. The slots satisfy : has no and the fee rule becomes a first-price case. The index is the number of other active users; the convergence is conditional on that count, matching the model's statement that bidders know how many users are active. Basu et al., §3, p. 11; Result 3, p. 16.
Bids range over . The gain is computed from the protocol payoff by a supremum over that interval; it is not defined as the adjacent order-statistic spacing or as a closed expression for the optimum. The expected gain takes the supremum over bids of expected payoffs, not the expectation of the pointwise supremum, since a bidder cannot condition a bid on the others' bids. The theorem explicitly requires integrability of the payoff of every admissible bid, so the real-valued integral cannot acquire meaning from Lean's default value for a non-integrable function. The first clause uses a concrete admissible bid profile; the second uses the product law of truthful others. The participation probability , the total potential user count , miner rewards, and the multi-block averaging parameter do not enter this conditional one-block claim. Basu et al., §3–§4, pp. 10–16.
The development needs finite order statistics, a measurable payoff and gain, probability laws from continuous densities, and integrability and convergence of adjacent order-statistic spacings. Contributions that establish those interfaces or prove the quoted intermediate claims serve the stated goal directly.
A Nash equilibrium of a two-player game is a pair of choices from which neither player can improve by changing their own choice alone. Computing one equilibrium is a central task in algorithmic game theory. For unrestricted bimatrix games, their payoff tables may encode difficult equilibrium computations. The structure of a rank-one bimatrix game gives a more specific question: can one equilibrium be found in time polynomial in the binary description of the game, even when equilibria are not isolated? Adsul, Garg, Mehta, Sohoni and von Stengel answer this with their BINSEARCH algorithm in Fast Algorithms for Rank-1 Bimatrix Games, Theorem 19. Their analysis explicitly includes degenerate games, which can have continua of equilibria (p. 5).
The paper develops a geometric account of rank reduction, parameterized linear programs, the connected set of equilibria of the auxiliary games, and the binary search procedure. The present mission targets the algorithmic result. The separately stated results on enumeration, exponentially many equilibria, and a structure theorem are outside this mission (Adsul et al., §§6–9).
An bimatrix game has payoff matrices . Player 1 chooses a row and player 2 chooses a column. A mixed strategy assigns nonnegative weights summing to one to a player's pure strategies. Write and for the two simplices. Against mixed strategies and , the payoffs are and . The pair is a Nash equilibrium when each strategy maximizes its owner's payoff against the other. These are the paper's definitions on pp. 4–5.
The games studied here have the form
The sum of the two payoff matrices is , so its rank is at most one. Zero vectors are allowed; the zero-sum case is included. A real parameter defines an auxiliary game . The set consists of triples for which is an equilibrium of that auxiliary game. The desired equilibria are the triples in that also satisfy (equations (10)–(12)).
For each , a primal linear program minimizes subject to , , and . Its dual maximizes subject to and . Their optimal solutions describe the auxiliary equilibria. The sets and identify the inequalities that can be slack or the coordinates that can be positive on the dual optimal face. They define a face of the parameterized primal polyhedron (equations (17)–(29)).
The goal is Theorem 19: for rational of combined binary length , and polynomial-time LP solvers returning extreme optimal solutions, Figure 2's BINSEARCH finds a Nash equilibrium of in polynomial time in . In the formal statement, a polynomial is chosen before the dimensions, game data, and admissible LP-selection oracle. It bounds the number of main-loop iterations, the bit length of every midpoint parameter passed to , and the bit length of every returned , including the parameter passed to the final :
for every optimal returned by the final dual LP, with the stated bound on each intermediate parameter. The ordered milestones cover best responses (Lemma 1), rank reduction (Lemma 6 and Theorem 7), primal-dual optimality (Lemma 9), preservation of the bracket (Lemma 17), the segment test (Lemma 18), and separation of distinct breakpoints (proof of Theorem 19).
The theorem gives an algorithm whose performance guarantee depends on the input's bit length, not on the number of equilibria. This matters for degenerate games: a continuum of equilibria does not by itself supply an algorithm to find one. The auxiliary LPs also connect game-theoretic best responses to ordinary finite-dimensional optimization. These claims and their precise scope are in §§4–5 of the paper.
The paper proves the theorem on paper. This mission asks for a machine-checked version of its formal statements and, ultimately, the proof. The definitions of best responses, primal and dual feasible sets, optimal faces, breakpoints, and a rational-input LP oracle are reusable in other formalizations of parametric games. The draft theorem declarations contain proof placeholders; they are targets rather than completed machine-checked proofs.
Ordinary bisection finds an interval containing an equilibrium parameter, but it can continue indefinitely when the equilibrium lies at a breakpoint: the two bounds can remain in neighboring segments. Repeated midpoints also create parameters whose bit descriptions grow with the number of iterations. Figure 2 therefore uses additional LPs that search the current optimal face and, in a strict branch, replace the answer by a breakpoint. A correctness proof must cover every permitted extreme optimal answer from these LPs, including degenerate faces, and must bound the separation of rational breakpoints (pp. 17–22).
Lean represents pure strategies by zero-based Fin m and Fin n, mixed strategies by real standard simplices, and payoffs by real matrices and vectors. The goal's input entries are rational and cast to reals for the LPs. It assumes : the paper leaves this implicit, while its minimum over the entries of and both mixed-strategy simplices require nonempty index sets. The game may be degenerate and may have rank zero.
LP optima are members of feasible sets whose objective is least or greatest on the full feasible objective image. An extreme LP solution also lies in the feasible set's extreme-point set. A selection oracle is constrained whenever an optimal extreme solution exists, and the goal asserts that every LP actually called during the run has such an answer. This excludes arbitrary values from an oracle at an infeasible or unbounded call. The initial bracket is the minimum and maximum entry of ; every branch and BR replacement follows Figure 2. The breakpoint endpoint symbols and are represented by absent optional finite endpoints in Lemma 18.
The running-time clause is an iteration bound together with a bound on the binary size of the midpoint and returned LP parameters; it does not formalize a machine model or the assumed polynomial-time LP solver. The goal is about the specified BINSEARCH run for every admissible selection oracle. Existence of some Nash equilibrium or termination for one hand-picked oracle would not express Theorem 19. Lemma 6 uses , the condition used in its printed proof; with a freely fixed , its printed implication (a) to (b) is false. A full development needs finite-dimensional LP duality, extreme-point and rational-vertex bounds, convex optimal-face geometry, and control of the run invariant. Contributions proving these components are welcome.
A bilevel program is an optimization problem in which one of the constraints is itself an optimization problem. An upper-level decision maker (a leader) chooses ; a lower-level decision maker (a follower) responds with an optimal solution of a problem parameterized by ; the leader's cost depends on both. Stackelberg games, toll setting on transportation networks, hyperparameter selection in machine learning, and many pricing and network design problems in operations research have this form. See Dempe, Foundations of Bilevel Programming (Kluwer, 2002), and Dempe and Zemkoho (eds.), Bilevel Optimization (Springer, 2020).
Necessary optimality conditions for bilevel programs are hard to obtain because the follower's optimality is not a standard constraint. The value function approach of Outrata (1990) replaces " is optimal for the lower level" by the single inequality , where is the optimal value of the lower level. This gives an equivalent single-level problem, but a well-known obstacle follows: Ye and Zhu (1995) showed that the standard nonsmooth constraint qualifications (nonsmooth MFCQ, equivalently NNAMCQ) fail at every feasible point of this reformulation. KKT-type conditions have therefore relied on calmness (Clarke 1983) or on partial calmness (Ye and Zhu 1995), both of which are strong.
Gfrerer (2013) introduced directional versions of regularity conditions, required only along one critical direction. Bai and Ye (arXiv:2004.01783, Mathematics of Operations Research 2022) carry this idea to the value function approach. They define calmness in a direction, prove a directional KKT condition for a general inequality-constrained problem under it, and apply this to the value-function reformulation of a bilevel program. This mission formalizes that chain, up to the paper's Theorem 5.1.
Let , and be continuously differentiable. For each , is the solution set of the lower level program : subject to . The bilevel program is
The value function is , and the value-function reformulation is
All norms are Euclidean, and is the open unit ball. For a direction and , the directional neighbourhood is
It is a cone of half-angle governed by around the ray through , cut at radius ; for it is the whole ball .
(VP) is calm at in direction if there are such that for every perturbation of the right-hand sides and every that satisfies the perturbed constraints. The same definition (Definition 3.1) applies to a general problem (P): s.t. .
A map is directionally Lipschitz at in direction if it is Lipschitz on for some . Its directional derivative is .
The directional limiting subdifferential collects the limits of Fréchet subgradients with , and .
The critical cone of (VP) consists of the with
Let be a local minimizer of (BP). Suppose is directionally Lipschitz and directionally differentiable at in direction , that , and that (VP) is calm at in direction . Then there exist , and with
Theorem 5.1 gives a KKT condition for bilevel programs under a regularity assumption checked in one critical direction only. Directional calmness is weaker than classical calmness, because the neighbourhood is smaller than a ball. The conclusion is also sharper than the nondirectional KKT condition: the subdifferential of is the directional one, and the multipliers satisfy the extra orthogonality conditions with and . Example 3.1 of the paper is a bilevel program in which partial calmness and calmness fail but calmness in a nonzero critical direction holds. Theorem 5.1 applies there, and the classical results do not. Section 5 of the paper derives verifiable sufficient conditions (directional quasi-normality, Theorems 5.2–5.3) from it.
The result is proved in the paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A formal proof would check a chain that passes through Ekeland's variational principle, a Fermat rule and a chain rule for limiting subdifferentials, and a limiting argument with directional sequences. The general Theorem 3.1 is reusable for any inequality-constrained program with directionally Lipschitz constraints.
The obvious route is "calmness gives exact penalization, then Fermat's rule". For directional calmness this only says that minimizes the penalized function on the directional neighbourhood, which is not a neighbourhood of . Fermat's rule cannot be applied at itself, so the stationarity must be produced at points inside the cone that approach along the direction, and then passed to the limit. That passage needs the multipliers to be bounded and the limiting subgradients to be directional ones.
The bilevel step adds two obstacles. The constraint is nonsmooth and extended-valued, so its subdifferential has to be split exactly into and the -part of . And when the conclusion still requires an element of , which exists only because is directionally Lipschitz.
EuclideanSpace ℝ (Fin q) (E q). The pair lives in WithLp 2 (E n × E m), the Euclidean product; the bare product type would carry the sup norm. Theorem 3.1 and its milestones are stated on any finite-dimensional real inner product space, which is linearly isometric to ; this lets the goal apply Theorem 3.1 on the product.EReal-valued infimum: when the lower level is infeasible, when it is unbounded. The constraint of (VP) is evaluated in EReal. " directionally Lipschitz" includes finiteness of on , which Definition 2.4 leaves implicit because it is written for real-valued maps. Directional differentiability is that of as a real function on that set, and its value is passed explicitly and enters the critical cone.NonconvexSplitting.Shared.IsRegularSubgrad, and the directional normal cone is the published SetConstrSOC.Directional.dirLimNormal. Each is an inner product, and is . "" is stated as the existence of one that makes the sum zero, including when .A complete development needs Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle) and the Fréchet and limiting subdifferential calculus: the Fermat rule, the sum rule with a smooth function, and the chain rule for a Lipschitz composition. It also needs the fact that Lipschitz functions have bounded subgradients. These are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the subdifferential calculus lemmas as separate theorems.
Call centers and other many-server service systems serve several classes of customers, each with its own service-time distribution, patience distribution and cost of waiting or abandoning. A customer who waits longer than its patience time abandons. The system manager decides, whenever an agent becomes free, which class to serve and which customer inside that class to serve.
Classical scheduling rules for such systems, such as the rule of Atar, Giat and Shimkin (2010) and the generalized rule of Long, Shimkin, Zhang and Zhang (2020), serve customers of the same class first-come, first-served (FCFS). Bassamboo and Randhawa (2015, published in Management Science 2016) showed that FCFS within a class is suboptimal when patience times are not exponential: as a customer waits, the conditional distribution of its residual patience changes, and serving by time in queue can reduce cost. Their fluid analysis showed that a single class should be split into at most two FCFS subclasses.
Bassamboo, Randhawa and Wu (Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1190) combine the two decisions, across classes and within a class, in one fluid optimization problem. Their structural result is that the fluid-optimal schedule needs within-class differentiation for at most one class; every other class is served FCFS. This is the basis of their "mostly-FCFS" policy. This mission formalizes that result together with the two lemmas stated before it.
There are classes and a total capacity of agents. Class arrives at rate , has mean service time with , and its patience time has distribution with survival function . The offered wait of a customer is the time it would wait before service if it were infinitely patient; means the customer is never served. A customer offered wait incurs an average cost , obtained in the paper by integrating a cost over service time and patience (display (5)).
In the fluid model, class receives capacity and is divided into subclasses, each served FCFS. Subclass has arrival rate , offered wait and capacity . The within-class program (6) defines the class cost function
the infimum ranging over and all subclass rates, waits and capacities. The middle constraint says that the rate of customers of subclass who remain patient long enough to reach service does not exceed the subclass's service rate. The across-class program (2) is
A plan is a choice of capacities and, for each class, a subclass configuration feasible for (6) at ; a fluid-optimal solution is a feasible plan of least total cost .
The fluid-optimal solution to (2) with defined in (6) splits the classes into at most subclasses; in particular for at most one class , and for this class . Formally: every feasible plan is weakly improved by a feasible plan with
Proposition 1 is what makes the paper's policy simple. Lemma 1 alone would permit every class to be split in two, giving up to FCFS queues with their own priority rules; Proposition 1 says that one non-FCFS class suffices, so a fluid-optimal schedule can be implemented as a priority ordering of classes with time-in-queue differentiation in at most one of them. Combined with Lemma 2, which makes (2) a convex allocation problem, it underlies the index-based characterization of the optimum in Proposition 2 and the mostly-FCFS and multi-class time-in-queue policies of §4.
The paper's proofs are in an online appendix that this mission does not use. To our knowledge none of the three results has a machine-checked proof. The formal development provides a reusable encoding of the fluid model of a multi-class queue with abandonment, with offered waits that may be infinite, and a checked version of the sparsity statement underlying the mostly-FCFS policy.
The program (6) has an unbounded number of subclasses, offered waits drawn from , and arbitrary cost and survival functions, so the feasible set is not a fixed finite-dimensional polytope and the infimum need not be attained. Lemma 1 for each class separately does not give Proposition 1: splitting each class into two subclasses is consistent with Lemma 1 and violates Proposition 1. The bound in Proposition 1 depends on capacity being free to move between classes, with only the total budget shared; with each held fixed the claim fails. The statements must also respect the never-served subclass , which the paper uses to represent LCFS as the offered-wait vector .
Everything lives in the namespace HetImpatient.FluidSplit, in one definitions file HetImpatient.FluidSplit.Model and three theorem items.
Fin m; a class configuration carries its own number of subclasses J : ℕ, with subclasses Fin J, and feasibility requires J ≥ 1. The number of subclasses is otherwise unbounded.ℝ≥0∞, so is allowed. Rates, capacities and costs are real numbers.A statement that drops the comparison of costs, or builds "at most two subclasses" into the definition of feasibility, is trivial and is not what is formalized here: the improved plan must be feasible and no more costly, and feasibility permits any number of subclasses (a sanity check confirms that a plan splitting two classes is feasible).
Welcome contributions: proofs of Lemma 1, Lemma 2 and Proposition 1, and supporting lemmas about subclass configurations stated for this model.
A firm that owns a strong brand can use the brand name on a new product outside its core business. This brand extension can be produced in-house or licensed to a specialized firm against a royalty. Brand licensing is a large business: its revenues reached US$315.5 billion in 2022 (Licensing International, cited in the paper's endnote 2). The marketing literature has long documented a risk: a poor extension can damage the brand and lower demand for the core product. This risk is called brand dilution. The empirical literature surveyed in the paper's introduction (Colucci, Montaguti and Lago 2008; Jayachandran et al. 2013; Bărbulescu Robinson et al. 2015) finds that dilution is associated more with licensing than with internal development. The prevalent reading is causal: a licensee, who does not own the brand, has scope for opportunistic behaviour that damages it.
Bacchiega, Colucci, Denicolò and Magnani (Management Science 70(5), 2024) build a game-theoretic model of the brand owner's choice between no extension, in-house development and royalty licensing, with moral hazard on the licensee's side and a reciprocal effect of the extension's quality on the core product's demand. Their central result, Proposition 3, runs against the causal reading. Among parameter values where the brand owner is indifferent between the two modes, switching from in-house development to licensing always raises the quality of the extension. The empirical correlation must therefore come from selection, not from licensing itself.
There are two products, a core product and an extension, both sold monopolistically. Efforts and are the products' perceived qualities. The parameters are the perceived distance between the products, the technological distance , the core market size , the extension market size , the magnitude of the reciprocal effect and a benchmark quality ; the cost parameter is normalized to .
The intensive margin is the set of parameters where .
For every in-house equilibrium and every subgame-perfect licensing equilibrium with extension effort , if
then
with strict inequality when charges every nonempty open interval.
The goal is stated about the equilibria themselves, not about the closed forms the paper derives for them.
Proposition 3 separates two explanations of the same correlation. If licensing caused dilution, a brand owner who switched from in-house development to licensing would lower the extension's quality. In the model the opposite happens at the margin of indifference. The core product's quality falls under licensing, because the brand owner internalizes only part of the extension's effect on it. To stay as profitable as in-house development despite the costs of a vertical chain, the licensed extension must be of higher quality. Dilution under licensing then appears where licensing is chosen for other reasons, for example at the extensive margin (Proposition 2 of the paper), not because of the mode itself.
The result has been proved on paper, through explicit closed forms in Appendices A, B and F. As far as is known it has no machine-checked proof. The mission adds three things. It checks the closed forms of the equilibrium, including the global optimality and uniqueness of the first-order solutions. It handles the corners the paper treats in words: the royalty constraint , and the licensee's zero effort when exceeds the quality index. And it checks the sign computations, where the printed (F.4)–(F.6) contain slips. The comparison it builds, between a centralized optimum and a subgame-perfect equilibrium of a three-stage moral-hazard game, appears throughout the licensing and franchising literature.
The obvious comparison fails. In general and cannot be ranked: the licensee has a lower cost of effort, but it ignores the reciprocal effect and faces a royalty that erodes its margin. The ranking holds only on the intensive margin, which is defined implicitly by the equality of two equilibrium profits. Using that equality requires the full closed-form equilibrium of both modes, including that the first-order solutions are the global, unique optima on the non-negative orthant and in every subgame of the licensing game. One then eliminates through and signs a rational function of on the whole parameter box. The degenerate corners and , where the royalty is indeterminate and both modes earn the no-extension profit, are excluded only by the strict inequality , so they have to be handled explicitly.
All quantities are real numbers; a model is a structure Params with fields α θ μ ρ lam ε (lam is ), and Params.Standing bundles , , , , , . Every effort and royalty ranges over . The extension profit and output carry a positive part, so that nothing is sold when the royalty exceeds the quality index. The core profit is , as on the page. The in-house equilibrium is any maximizer of (7) on the non-negative quadrant. A licensing equilibrium is a strategy profile — the licensee's effort rule , the royalty rule and the core effort — optimal in every subgame. The licensee's participation decision is not modelled, because it never binds under a pure royalty. The no-extension benchmark enters as " exceeds for every ". The dilution clause is stated for an arbitrary probability measure on for the shock (weak inequality), and strictly for every such measure of full support.
The goal must not be restated with the closed forms (A.2), (B.2) in place of the equilibria, nor with in place of the profit equality, since either turns it into an algebraic identity about the paper's formulas. The milestones (F.4) and (F.6) state corrected forms of the printed expressions: the right-hand side of (F.5) is , and the numerators of (F.4) and (F.6) read .
A complete development needs elementary real algebra and two-variable concave quadratic optimization on orthants and half-lines; Mathlib suffices. The subgame-perfect equilibrium of a sequential game with continuous actions is reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
Continuous limit-order markets reward speed. When the fundamental value of an asset moves, a trader with a faster connection can trade against stale quotes before the quoting liquidity provider can cancel them. This practice, sniping, is a direct transfer from liquidity providers to fast traders, and it has been documented and analysed as a cost of the continuous-trading design (Budish, Cramton and Shim, 2015). One market-design response, used by the Investors Exchange (IEX), whose exchange application the SEC approved in June 2016, is a short, fixed delay on all incoming messages combined with midpoint peg orders: hidden orders that rest at the midpoint of the national best bid and offer and that the exchange re-prices before a delayed sniping order can reach them. The delay therefore protects pegged orders from sniping, while ordinary quotes at the best bid and offer remain exposed.
Aldrich and Friedman (2019, SSRN 2999059), published in Management Science in 2023 (doi:10.1287/mnsc.2022.4370), build a model of such a market in which impatient investors choose between protected midpoint pegs and immediate market orders, and proprietary traders choose between providing quotes and sniping them. Their baseline result is a closed-form, unique equilibrium describing how much order flow the protected midpoint attracts and how many market makers and snipers the market supports. This mission formalizes that baseline result.
A parameter vector consists of the flow cost of speed , the midpoint execution fee , the investor gross surplus , the discount rate of a resting pegged order, the arrival rate of investors on each side of the market, and the rate at which the fundamental value jumps up (and, separately, down) by one tick. The standing restrictions are , , , , , . The discount factor is .
The order imbalance records the hidden midpoint queue: means resting sell pegs, means resting buy pegs. A fraction of investors send pegs, the rest market orders, and each arrival is a buy or a sell with equal probability. A peg always joins the queue or executes against a contra-side peg; a market order executes against a contra-side peg if one rests and otherwise at the best bid or offer. One arrival maps a distribution to , with
The discrete Laplace law is .
Under , the expected net surplus of a midpoint peg order and of a market order are
With real masses of market makers and of snipers, their flow profits are
A market equilibrium (Definition 3.1) is a triple such that either and , or and ; and with .
Under the standing restrictions there is exactly one market equilibrium, namely
The goal asserts both that this triple satisfies Definition 3.1 and that every triple satisfying Definition 3.1 equals it.
The proposition gives the baseline against which the paper measures the effect of order protection. Its closed forms show that the peg share is independent of the sniping intensity , that it falls with gross surplus and rises with patience , and that the sniper mass does not depend on because the market-maker mass adjusts. The paper's later sections compare this benchmark with a market in which pegs are not protected, and its welfare and empirical comparisons with IEX data are calibrated on these formulas (Table 2 reports at the baseline parameters).
The result is proved in the paper; nothing here is open. A search of the Prove2Me catalog finds no part of it formalized: there is no machine-checked discrete Laplace stationary law, no limit-order-book equilibrium and no pegged-order model on the platform. The mission adds a checked version of the full argument, including the uniqueness half of Proposition 3.1, which the paper asserts but does not prove (its proof verifies only that is a fixed point).
The algebra of (3.2), (3.3) and (3.9) is short once the sums are evaluated, so the content lies elsewhere. First, the payoffs are defined as infinite series over a two-sided index, and their closed forms require summing geometric series on both tails, including the discounted tail . Second, uniqueness of the steady state in Proposition 3.1 is a statement about every nonnegative summable fixed point of on , not just a verification that is one. Third, uniqueness of the market equilibrium requires excluding every other triple: the interior branch and the corner must be shown to be mutually exclusive and exhaustive, and the case of a zero mass of market makers or snipers must be ruled out. The naive reading that "solving gives the equilibrium" misses the corner case and the requirement that the root lie strictly below one.
All quantities are real numbers, and the parameters are bundled in a structure Params with a predicate Params.Standing. The paper prints the restriction ; the formalization uses , as in Assumption A4a, which is among the proposition's hypotheses, because at the formula gives , which Definition 3.1 does not admit, and no equilibrium exists. The fee restriction is the proposition's , weaker than A4b's . The condition is derived from , not assumed.
One-sided sums are Lean tsums over , with indexed by ; a distribution on is a nonnegative family with HasSum p 1. is a natural-number power, so at is the point mass at , which is what the corner of Definition 3.1 evaluates. The payoffs , and the market-maker profit are defined by their series, not by their closed forms, so that (3.2), (3.3) and (3.5) are milestones rather than definitions. Division by zero returns zero in Lean; a zero mass then yields or , never zero profit, which matches the page.
A formalization that only checks that the formula triple satisfies the equilibrium conditions, or that defines by their closed forms, would drop the uniqueness claim or the steady-state analysis, and is not the target.
The development needs two-sided geometric series, tsum manipulation over and , and elementary bounds on Real.exp. The stationary-law uniqueness for a birth–death operator on is reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
Unused prescription medicines create disposal and public health costs, while a patient may use less medicine than a doctor prescribes. A regulator can make the pharmaceutical producer collect unused medicine, or charge a fee on dispensed medicine and use the proceeds to fund collection. These two policies charge the producer for different quantities. Alev, Atasu, Toktay and Zhang study how that distinction affects a producer's incentives to influence prescriptions and the regulator's choice of policy. The question matters when regulation changes both the amount prescribed and the share of unused medicine collected.
A patient has a need level and a preferred use level . They are independent and uniform on . The producer chooses a medicine price and two promotional effort levels, directed at the doctor and directed at the patient. Both efforts lie in . The doctor chooses a prescription to maximize
Here is the unit health benefit and is the doctor's reputational cost per unit of over-prescription. At indifference the model selects . The amount used is ; the remaining is unused. These choices and the tie convention reproduce the doctor's rule in Lemma 1, p. 15.
Under end-of-pipe control (EC), the planner sets a collection rate . The producer pays unit cost to collect that fraction of unused medicine. Under source reduction (SR), the planner charges the producer a fee for each dispensed unit and collects unused medicine at rate . The SR planner must fund collection without a deficit. For either policy, the producer maximizes expected revenue minus the quadratic promotion costs and its policy cost. The doctor must receive nonnegative utility for every need level.
The planner evaluates expected doctor utility, producer profit, and planner surplus, then subtracts two harms. Environmental disutility is ; social disutility from uncollected unused medicine is . The resulting expected total welfare is maximized subject to the collection, fee, producer participation, and no-deficit constraints. The planner may choose among producer actions tied for maximal profit. The full primitives and constraints are those of Section 3, pp. 8–14.
The producer thresholds in the appendix's stated regime are
Write and for the attained maximum welfare values under the two policies. Proposition 4 and Table 2, pp. 17–18, give the mission's goal: the models tie for ; they tie when and ; SR weakly wins when and . When and , a threshold divides SR's weak advantage below it from EC's weak advantage above it. Above that threshold, an EC welfare optimum eliminates over-prescription, encoding the paper's requirement .
The milestones cover the doctor's prescription rule, the producer's optimal profit in each prescription region, the health-benefit and collection-cost thresholds, the EC environmental threshold, and the appendix's SR replication claim. Together these are the named results and displayed steps used by the paper's welfare comparison.
The result identifies when a fee on every dispensed unit can match or improve a direct collection obligation, and when the direct obligation can weakly improve welfare because it acts on unused medicine. Its threshold form connects a medicine's health benefit and the cost and harm of its disposal to the preferred regulatory instrument. The comparison also separates the ability to discourage over-prescription from the value of doing so: a policy may allow its elimination without making it welfare maximizing.
The paper proves these claims analytically in its stated appendix regime; this mission asks for machine-checked proofs of the game model, equilibrium welfare comparisons, and threshold results. The proposed Lean theorems are currently open. The model definitions are reusable for the paper's producer-preference and advocacy results, which are outside this mission.
Comparing the two policies at a fixed prescription quantity misses the producer's response. Changing a collection rate or unit fee changes the producer's optimal price and promotion, which can switch the doctor's choice between prescribing need and over-prescribing. The planner must also respect producer participation, and SR must cover its collection costs. The welfare comparison therefore requires the feasible equilibria in both prescription regions and careful treatment of ties at the switching boundary. The online appendix, pp. 1–5, records the relevant region calculations.
Lean represents all parameters, actions, and policies by real numbers. It computes expectations by iterated interval integrals over independent uniform . The prescription response, producer profit, planner surplus, disutilities, and welfare are defined from the Section 3 formulas. Welfare is the supremum over feasible planner policies and producer optima, with attainment asserted in the goal. The model never defines welfare by an appendix closed form, and the three named thresholds are fixed to the appendix formulas rather than left as free witnesses. The environmental threshold must also lead to an EC optimum without over-prescription, so an empty or arbitrary switch does not satisfy the intended claim.
The goal states the appendix's , , and regime, together with , , and nonnegative disutilities. The restriction is the appendix's nonnegative-profit convention. In this regime , so the first column of Table 2 has no instance with ; it remains stated because it belongs to the printed table. Proposition 1's strict ordering of health-benefit thresholds requires , a disclosed strengthening of that milestone's premise. The doctor's tie goes to over-prescription; the planner can select among producer optima; price has no sign restriction. EC uses only its collection rate, so the unused fee field of the shared policy record has no effect. The participation condition is pointwise in need. The SR half of Proposition 3, later propositions, numerical study, and regimes outside the printed proof are outside this mission.
Many tasks on high-dimensional data ask not for the nearest neighbours of a query but for how many data points lie close to it. Density estimates of this kind feed outlier detection, kernel density estimation, classification by neighbourhood counts, and the tuning of nearest-neighbour search itself. Exact counting needs a scan of the whole dataset for every query, and uniform random sampling needs about samples per unit of relative accuracy, which is prohibitive when the neighbourhood is a tiny fraction of the points.
Locality-sensitive hashing (LSH) is the standard tool for finding near neighbours in sublinear time: a random hash function sends nearby points to the same bucket with higher probability than distant ones (Indyk–Motwani 1998; for angles, the random-hyperplane family of Charikar 2002). Wu, Charikar and Natchu (arXiv:1809.07471; Mathematics of Operations Research, 2022) turn LSH tables into a counting device. Their estimator LSH Count samples from the buckets near the query and corrects the bias of hashing by importance weighting, so that the number of samples depends on how well the hash concentrates the neighbourhood rather than on .
The dataset consists of unit vectors , and the query is a unit vector. For a set of angles, the neighbourhood is
and the target is its size .
A table is built from a random hash function , which stores in the bucket . For a set of Hamming distances, is the set of points of table whose bucket is at a Hamming distance in from the query's bucket , and is their number. The collision probabilities are
for one random table, , and is the expected pool size of one table.
LSH Count with parameters :
The table bias is the mean of given the tables.
For and , if
then
This uses tables and samples in total, the of the printed Theorem 1 (p. 6).
Theorem 1 bounds the cost of counting near neighbours with LSH: the sample complexity replaces the ratio of uniform sampling by the ratio of the expected pool size to the expected number of neighbours in the pool. When the hash concentrates the neighbourhood, this is a large saving, and the number of tables depends only on and . The same template (importance weights from known inclusion probabilities, a variance split into a sampling term and a design term, median of means) recurs in randomized estimation; Lemma 4's decomposition is the step that makes the two sources of error separately controllable.
The result is proved on paper. No machine-checked proof of it, or of any LSH-based estimator, is known. The mission produces a formal proof with explicit constants. Theorem 1 is printed with ; the constants here are the ones its proof determines, and one of them corrects the printed proof: the final display of Lemma 6 (p. 17) drops a factor that its own target inequality needs. The mission also produces reusable, generic pieces: the deterministic median lemma and a Chernoff bound for independent events with probability at most .
The arithmetic of each lemma is short; the difficulty is the probability model. The samples are not independent of the tables: their law is uniform on a random pool whose size is itself random, and the weight divides by that size. Unconditional moments therefore require conditioning on the tables and then averaging over them, and the cross terms in Lemmas 2 and 5 separate a single table from pairs of distinct tables . A tempting simplification samples uniformly from the set of distinct points in the probed buckets; it makes Lemma 1 false whenever a point is probed in several tables, because the weight then no longer averages to . A second tempting step treats as unconditionally independent, which would give an error of order and lose the table term , which does not decay in ; the samples are independent only given the tables. The Chernoff step needs independence across the estimators, which comes from building each estimator from fresh tables.
Fin n, so duplicates count separately; vectors live in EuclideanSpace ℝ (Fin d), and is InnerProductGeometry.angle.ProbabilityTheory.variance, Chebyshev's inequality (meas_ge_le_variance_div_sq), the moment generating function of a sum of independent indicators (measure_ge_le_exp_mul_mgf), and List.insertionSort. The median lemma and the Chernoff step are independent of LSH and reusable.Not in scope: Theorem 2 (Multi-Probe Count) with Lemmas 7–9; the running-time Theorems 3–4; the random-hyperplane collision formulas (Theorems 5–6, Lemma 12, (1)); the experiments.
After the financial crisis of 2007–2009, standardized over-the-counter derivatives were moved to mandatory central clearing: a central counterparty (CCP) becomes the buyer to every seller and the seller to every buyer, so that the original counterparties are insulated from each other's default. The CCP in turn protects itself by a default waterfall and collects two kinds of prepaid collateral from its clearing members: initial margin, which absorbs only the losses of the member who posted it, and the default fund, which is shared and mutualizes losses across members. Losses beyond both layers are borne by the surviving members through ex-post contributions. Regulators set both requirements, yet there was little theory of how the two collateral types should be combined.
Wang, Capponi and Zhang (Management Science, 2022) model this as a moral-hazard problem. Posting collateral raises a member's pledgeable income in the sense of Holmström and Tirole (1997) and so strengthens its incentive to manage risk; but because the default fund is mutualized, a member's incentive to hedge also depends on whether the other members hedge. The paper's headline result, Proposition 2, characterizes exactly when all members hedge as a function of the two collateral requirements. Its optimal-mix result (Proposition 3) and the policy discussion are built on it.
There are risk-neutral clearing members (dealers). A credit event occurs with probability ; in it, every dealer owes to its protection buyer. Each dealer holds an asset whose return is independent across dealers and of the credit event. It chooses an action : hedging () gives a bad-state probability and good-state return , risk-shifting () gives and , with , , and expected returns satisfying . A dealer starts with assets and receives the price from buyers of risk aversion , so its balance sheet is . The pledgeability is
and Assumption 2 requires .
Each member posts initial margin and default fund with , . Default-fund posting costs an extra per unit, and ex-post contributions are financed at unit cost with . If of the other members hedge, the number of defaults among them has law (the sum of independent binomials with parameters and ), and a surviving member's expected loss-sharing contribution and financing cost is
A member taking action earns
Members play a simultaneous game in pure strategies. A Pareto-dominant Nash equilibrium is a Nash equilibrium that gives every member at least its payoff in every Nash equilibrium.
The cutoff is the least default fund in at which hedging is a best response when all other members hedge, and is the least initial margin at which this holds with .
For every collateral pair with , , , there is exactly one Pareto-dominant Nash equilibrium, and
For every , is the unique solution in of
On the function is piecewise linear, strictly decreasing, continuous and convex, with slope at least , and with slope greater than whenever .
The proof in the paper's appendix gives the attack path. Lemma IA.1 gives the explicit ceiling-sum expression (A28) for and its properties (positive, strictly decreasing in , and , piecewise linear, continuous, zero at ) and the binomial moments . Inequality (A2) reduces "hedging is a best response" to . Step 1 shows that the cutoffs are unique, sorts the equilibria into three cases, and rules out asymmetric equilibria by (A4)–(A5). Step 2 computes the slope of off the kinks (A7), locates the kinks (A8), compares one-sided slopes at a kink (A9)–(A11), and Step 3 gives the closed forms (A15) and (A17).
Proposition 2 answers a regulatory question in closed form: given the initial margin, it names the smallest default fund that makes prudent risk management the outcome that members coordinate on. A slope of above means that a unit of default fund buys more incentive than a unit of initial margin, because the fund is mutualized. That trade-off is what makes the optimal collateral mix of Proposition 3 interior or a corner, and it drives the paper's comparative statics in the number of members and the financing cost.
The result is proved in the paper with an implicit-function argument; it has not been machine-checked. A formal proof would certify the equilibrium classification, including uniqueness of the Pareto-dominant equilibrium, which the paper argues case by case, and the shape claims. It would also make precise the regime in which the paper's "slope greater than " holds: when the prefunded default fund at already covers the shortfall of all other members (), the slope is exactly on an initial interval. The goal states the corrected claim. The binomial and piecewise-linear lemmas are reusable for other loss-mutualization models.
The equilibrium half is a finite game, but the natural argument "hedging is a strategic complement, so the extreme profiles are the only equilibria" needs strict monotonicity of in for every collateral pair, including the boundary where all vanish. It also needs weak inequalities handled carefully, since Nash equilibria here allow ties.
The shape half is harder. is defined implicitly by an equation whose left side is piecewise linear in with breakpoints that move with . A direct implicit-function argument gives derivatives only away from these kinks. Piecewise linearity, convexity and the slope bounds require locating every kink, showing that the ratio crosses each integer once, and comparing one-sided derivatives across a kink. The obvious claim that every slope lies in is false when the ratio exceeds .
All quantities are real numbers and members are indexed by Fin N. The paper's standing assumptions are bundled in Standing: conditions (1)–(3), Assumptions 1 and 2, , , , . To these the formalization adds , and , without which the model degenerates ( when ). Assumption 1 ( above the explicit bound (A18)) is a standing assumption of the paper that Proposition 2's proof does not use; it is kept. The expectation is the finite sum against the law of (A29), which encodes the paper's statement that depends on the other members' actions only through the number who hedge.
, and are defined as least incentive-compatible values (infima of nonempty sets bounded below), not as solutions of (18). Showing that they solve (18) and (A3), uniquely, is part of the targets, so the goal cannot be met by unfolding a definition. The Pareto-dominant equilibrium is not defined as "all members hedge": (17) is an equivalence over all profiles. "Piecewise linear" means finitely many breakpoints with affine between them, and "continuous and convex at the kinks" is stated as continuity and convexity on . The Nash equilibrium is the published generic pure-Nash relation CarbonDoubleCount.Planner.IsPureNash.
A complete development needs elementary binomial identities, one-dimensional implicit-function and monotone-root arguments, and one-sided derivatives of piecewise-affine functions; no measure theory is required. Proofs of individual milestones, in particular Lemma IA.1 and (A2), are welcome independently of the goal.
The U.S. Food and Drug Administration's accelerated approval pathway permits some drugs to reach patients before their clinical benefit has been fully confirmed. A manufacturer then promises a post-market study, but completion requires costly effort that the regulator cannot directly observe. If the study becomes overdue, withdrawal is a process rather than an instantaneous event. The time that process takes changes the manufacturer's incentive to finish the study. Xu, Zhao, and Petruzzi model this interaction and ask how withdrawal enforceability and the chance of a favorable study result affect compliance Xu, Zhao, and Petruzzi, SSRN preprint, 2019.
The question matters to a regulator setting a study deadline. A stronger withdrawal process can reduce the expected time a drug remains on the market after missing that deadline. A higher probability of confirming clinical benefit makes successful completion more valuable to the manufacturer. The paper's Proposition 2 compares these two changes through the largest study-cost type that a deadline can induce to comply.
A drug enters the market under accelerated approval at time zero. Its patent expires at time . Before expiry it earns a profit rate while accelerated approval remains in effect, and a rate after conversion to regular approval. The regulator chooses a deadline . If the study is still incomplete at , the regulator starts withdrawal; the additional withdrawal time is exponentially distributed with rate . Thus increasing shortens the expected withdrawal delay. Sales under accelerated approval stop at unless the study finishes earlier.
The manufacturer chooses a nonnegative effort , interpreted as the patient recruitment rate for a study requiring patients. For , the completion time follows a Gamma distribution with shape and rate . At the study never completes. A completed study confirms benefit with probability . If confirmation occurs before , the drug earns the regular-approval rate until ; otherwise it leaves the market at completion. For realized and , revenue is
The effort cost is , where is the manufacturer's cost type and . The resulting expected profit is for positive effort. With no effort, profit is . An effort is optimal if it maximizes this profit over all nonnegative efforts. The manufacturer complies at a deadline if some positive effort is optimal; a tie with zero effort counts as compliance, as in the paper's comparison . Let be the positive cost types for which some feasible deadline induces compliance, with the other parameters fixed. The compliance threshold is the supremum of that set.
The goal is the paper's Proposition 2. For fixed and admissible rates and probabilities, it asserts
The proof in the paper supports strict inequalities for a strict parameter increase when the initial compliant-type set is nonempty. This guarded strict version is included in the goal. If the set is empty, its Lean real supremum is zero, so an unconditional strict statement would be false.
The milestones record the integral representation of profit and the no-effort closed form, the single crossing of the deadline kernel, the threshold characterization from Proposition 1, and the two comparison steps used for enforceability and success probability. Together they connect the operational study model to the cost-type threshold. They are statements from Proposition 1 and the proofs of Propositions 1 and 2 in the same SSRN preprint.
The threshold tells the regulator which manufacturers can be induced to finish a required study by choosing an appropriate deadline. Raising it means that a manufacturer with a higher effort cost can still find positive effort optimal. The result concerns whether compliance can be induced; it does not assert a particular optimal deadline, a user-fee menu, or patient welfare. Those require further parts of the paper's mechanism-design model Xu, Zhao, and Petruzzi, §§4–5.
The mathematical result has a paper proof. This mission's Lean statements give it a precise computational interpretation: the completion and withdrawal distributions, the revenue rule, the no-study case, maximization over feasible effort, and the threshold are all explicit. The local index found no existing platform theorem with this model and conclusion. A complete development would add machine-checked proofs and reusable facts about Gamma completion probabilities, exponential delays, bounded expected revenue, and optimal effort. The present draft statements themselves are not proofs.
Comparing profit at the same deadline and effort does not settle the enforceability claim. Increasing changes both the return from completion and the benchmark profit from never completing, while the deadline that gives the best compliance incentive can move. Similarly, a positive payoff change at a fixed effort does not by itself identify the largest complying cost type: the optimum must still be taken over all efforts, and the supremum over deadlines must be justified. The proof must also control the zero-effort boundary and establish that the relevant set of cost types is bounded.
Lean uses real values for time, rates, profits, effort, and cost type, and a natural number for sample size. Params.Standing includes , , , , and . The paper gives and derives the profit-rate order from its demand assumptions. Positivity of , finite positive , and are disclosed restrictions needed for the stated threshold and the paper's limiting argument. Types satisfy , deadlines lie in , and the two boundary regimes and discussed as limits in the paper are outside the mission.
The withdrawal delay is Mathlib's exponential measure and positive-effort completion is its Gamma measure. Since Gamma measure at rate zero does not represent a study that never completes, the profit definition has a separate branch equal to . Revenue integrands are bounded on the distributions' nonnegative support under the standing assumptions. The threshold is computed as the real supremum of cost types for which an actual positive maximizer exists at some feasible deadline. A formulation based only on a positive-effort supremum would make compliance automatic and would not represent the paper's decision rule. If no positive cost type complies, the real supremum is zero; boundedness and the nonempty case are explicit in the milestones and goal.
A full proof needs integration against the Gamma and exponential measures, continuity and existence of an effort maximizer, a characterization of the cost-type set, and comparison of profit across deadline choices. Measure and optimization lemmas from this work can be reused beyond the drug-study application. Contributions to those components and to the stated milestones are within scope; the deadline-dependent fee menu and patient-welfare optimization of later sections are not part of this target.
Firms that track their customers can charge a returning customer according to what they have learned about her, while a newcomer pays an introductory price. Consumers can respond by identity management: deleting cookies, using new accounts or anonymising tools, so that they keep being treated as newcomers. The economics of this behaviour-based price discrimination with strategic consumers goes back to two-period models such as Fudenberg and Tirole (2000); the closest privacy models are the two-period monopolies of Acquisti and Varian (2005) and Conitzer, Taylor and Wagman (2012).
Laussel, Long and Resende (2023) study the question in an infinite-horizon setting; the formalization cites their CIRANO working paper 2021s-29. A monopolist gradually expands its market by lowering an introductory price, as a durable-good monopolist does in the Coase conjecture, and recognises every passive customer after her first purchase. Consumers decide once whether to pay a privacy cost to remain anonymous. The paper's main analytic result, Proposition 1, states that under full information acquisition the firm leaves part of the market unserved exactly when privacy is cheap enough, and gives the threshold in closed form.
Time is divided into contracting periods with discount factor . A monopolist sells a non-durable good at zero marginal cost. A unit mass of consumers has types uniform on ; type obtains utility per period of consumption.
Under full information acquisition (FIA) a passive consumer who has bought once is recognised and charged exactly in every later period. A consumer may instead pay a once-for-all privacy cost in period and become active: she remains anonymous and buys every period at the introductory price offered to new customers. Types in are active and types below the pivot are passive.
The firm uses a quasi-linear cut-off rule with : in period the new passive customers are the types in , starting from . The path converges to , and types below are never served. Consumers hold a quasi-linear expectations rule : the lifetime net utility of the period- marginal passive customer when the state is . The introductory price is , and the firm's period profit at state and choice is
A Markov perfect equilibrium (MPE) is a profile satisfying, at every state :
It must also satisfy .
With the threshold
every FIA MPE satisfies:
Proposition 1 shows that consumer privacy can stop a dynamic monopolist from serving the whole market. Without active consumers the firm keeps lowering its introductory price until everyone buys, in line with Coasian dynamics. With them, every price cut is also collected by the anonymous high-value consumers, so the firm stops at a strictly positive . The gap identity makes the effect quantitative: the share of passive customers who are eventually served is linear in the privacy cost. These statements underlie the paper's managerial recommendation that a firm facing cheap identity management should not aim at full coverage, and its comparison with the partial-history (PHI) information structure.
The result is proved in the paper, but by computer algebra with several printed slips. The prior-art search found no machine-checked formalization of this result. A formal proof would turn the closed-form calculation into a checked argument about a precisely defined equilibrium notion. The mission also provides a reusable encoding of an infinite-horizon pricing game with rational-expectations consumers, specified by arbitrage, Euler and indifference conditions. Nothing comparable is on the platform.
The equilibrium conditions couple the cut-off slope , the pivot and the expectation rule. The Euler equation leaves an algebraic condition on whose admissible root must be unique for every ; without uniqueness, two equilibria with the same discount factor could have different expansion speeds. At the pivot condition is an inequality, so a calculation valid at an interior pivot does not settle the threshold case. The pivot also contains an infinite price series whose convergence matters to the claimed threshold.
The Online Appendix's closed forms (29), (30) and (31) do not follow from the model as printed: the envelope expression (23) has a sign slip. For example, at the corrected Euler equation gives , whereas the printed (29) gives . The Lean statements use the derivative of the period profit and omit those printed formulas.
Everything is real-valued. The definitions file IdentityMgmt.FIA.Model has the following parts:
Profile structure with fields ;Arbitrage, Euler (via Mathlib's deriv), Pivot, IsMarkovEq and IsMPE;cbarFIA.The formalization commits to the following conventions:
tsum, which is summable under the standing assumptions.The boundary condition is not part of the definition: it is Proposition 1 (iii), and must be derived. Defining , or by formulas, or taking as a root of the printed (29), would trivialize or falsify the goal and is ruled out. Every equilibrium quantity is a field constrained only by the model's conditions. The existence part of Lemma 2 guards against vacuity.
Not formalized: Lemma 1 (the cut-off structure of the privacy decision, which the model builds in), the first sentence of Corollary 1, Corollary 2 (a graphical argument), the numerical Corollaries 3–4, and the PHI analysis (Lemma 4, Proposition 2).
Contributions are welcome at every milestone. The most reusable pieces are lemmas computing the derivatives of the period profit, the closed form of the expansion path, and the evaluation of the pivot series.
First-price sealed-bid auctions are used for procurement contracts, treasury securities, timber, and, since 2019, most display advertising. The classical advice for how to bid comes from Bayes–Nash equilibrium: each bidder knows the distribution of the others' values, and everyone plays the equilibrium. Practitioners rarely have that information. In a survey of auction consultants reported by Kasberger and Schlag, almost none of the respondents modelled equilibrium behaviour, and most named the distribution of rivals' bids as something they could not quantify.
Kasberger and Schlag (SSRN 3044438, version of 3 September 2022) propose a bid that needs no such prior. The bidder lists the bid distributions she considers conceivable and chooses the bid whose worst-case shortfall from the best response is smallest: the minimax loss bid (a criterion axiomatized by Milnor 1954, Hayashi 2008 and Stoye 2011). This mission formalizes the paper's choice-based recommendation, variation in bidding (§6.2), where the closed-form bid depends only on the number of bidders, a reserve level and one trust parameter.
There are bidders. Bidder 1 has value and bids ; the highest bid wins and pays its bid, and ties are broken uniformly at random. If bidders (bidder 1 included) tie at the top with , bidder 1 receives ; otherwise she receives .
A bid distribution is any joint law of the opponent bids. The expected utility of a bid is , and its loss is
Given an ambiguity set , the maximal loss of is , and a minimax loss bid minimizes it over all .
The ambiguity set of variation in bidding, , has three ingredients: a probability , a threshold below which no one bids, and a bid distribution . Each opponent is independently constrained with probability , and a constrained opponent bids an independent draw from . The unconstrained opponents bid a vector with an arbitrary joint law on , independent of who is constrained. Every such gives a member of . The salient choice is uniform on , with and
These are the utilities of bidding just above, respectively below, a common bid of all unconstrained opponents.
For uniform on , , and :
In the order the paper's proof uses them:
Proposition 4 turns a minimax problem over an infinite-dimensional set of joint distributions into a single equation in one variable. The resulting bid can be computed from , , and , and comes with a guarantee: against every environment in the loss is at most . The paper evaluates this guarantee at and tests the bid on field data. The monotonicity in is the robust analogue of the equilibrium fact that bids shade less as competition grows.
The result is proved in the paper; it has not been formalized anywhere. A machine-checked version adds three things. It fixes the ambiguity set: the printed set is too large, and the formal one is the version under which the statements hold. It records exactly which hypotheses the argument uses (, ). And it checks the analytic steps, whose printed versions contain small slips. The first-price model, the loss, and the minimax loss bid are reusable for the paper's other two recommendations (Propositions 1 and 5), which use different ambiguity sets.
The definition quantifies over every joint law of the unconstrained bids, including correlated and atomic ones. The crux is Lemma 1: one must show that, for each bid, collapsing all unconstrained mass to a single point (just below the best response when bidding too high, just above the own bid when bidding too low) does not decrease the loss. Some worst cases are limits of point masses approaching a tie, and the tie-breaking rule matters at those limits, so the argument has to work with suprema rather than maximizers.
A natural first idea is to argue coordinate by coordinate, moving one unconstrained bid at a time. It fails: the shift that raises the loss depends on the realized pattern of constrained bidders, and a profile that is worst for one pattern is not worst for another. Once Lemma 1 holds, the rest is one-variable analysis, but uniqueness of the root of (3) needs the strict decrease of , which uses in an essential way.
Opponents are indexed by Fin (n - 1); bids, values, and are reals and is a natural number with . The payoff splits ties evenly among all tied bidders, bidder 1 included. Expected utility is a Bochner integral of this bounded measurable payoff. Best utility and maximal loss are real suprema; they are finite because utilities of non-negative bids are at most and the ambiguity set is nonempty. The minimax loss bid is a predicate on bids , defined from the maximal loss and never from Equation (3); the goal quantifies over bids satisfying it.
is built as a pushforward: i.i.d. pairs (Bernoulli() coin, draw from ) for the opponents, independent of , with ranging over all probability measures on concentrated on . The printed definition (p. 20) lets the law of the unconstrained bids depend on who is constrained and allows bids below ; under it Lemma 1 and Propositions 3–4 fail for , so the corrected set is used and the affected items are labelled "corrected". Lemma 1, the p. 22 formula and Proposition 3 are stated for uniform; the paper states them for general , and for general continuous the claim of Proposition 3 that the minimax bid lies in fails numerically.
Restricting the ambiguity set to point masses, or defining the minimax bid as the root of (3), would make the goal trivial; neither is done. Contributions on the measure-theoretic layer (expected utility of a point-mass environment, the reduction of Lemma 1) are reusable for any first-price robust-bidding problem; the calculus milestones need only Mathlib's real analysis.
Load balancing asks for an assignment of jobs to machines that keeps the largest machine load, the makespan, small. On unrelated machines the processing time of a job may depend arbitrarily on the machine; the deterministic problem has the classical -approximation of Lenstra, Shmoys and Tardos (1990). In many applications (virtual-circuit routing, assigning customers to warehouses, cloud jobs) the processing times are not known when the assignment is made, only their distributions are. The assignment is fixed up front, the sizes are then revealed, and the quantity to control is the expected makespan.
Timeline:
There are machines and jobs . On a probability space, the random variable is the size of job on machine . Jobs are independent: the vectors for different are independent, while the sizes of one job on different machines may be correlated. An assignment puts the jobs on machine , and its expected makespan is
Every size splits into a truncated part and an exceptional part . The effective size of a random variable at an integer is
The algorithm works at a scale on the sizes . With , the LP with parameter asks for with
The class loop starts with ; while it gives the machines the class and removes them. The class defines a generalized assignment instance with processing times and costs , which the Shmoys–Tardos algorithm rounds to an assignment with
There is an absolute constant such that for every instance and every :
For , taking , (A)–(C) give an assignment of expected makespan at most ; a binary search over loses a factor . The constant is left unspecified so that the goal survives any improvement of the lower-bound constants.
In attack order: Lemma 1 (exceptional items lower bound) and Lemma 4 (truncated items lower bound); Lemma 5 (valid inequalities) and Proposition 1 (LP lower bound), which give (A); Observation 1 (the class loop terminates; at most machines of class ) and Observation 2 (the GAP rounding), which give (B); Lemma 2 (effective-size Chernoff bound), the effective-size facts and , Observation 3 (tail ), Lemma 7 (union bound over classes) and Lemma 6 (expected makespan ), which give (C).
Theorem 1 shows that the expected makespan on unrelated machines, a quantity that is #P-hard even to evaluate for a fixed assignment (Theorem 4 of the paper), can be approximated within a constant factor by a polynomial-size certificate: an LP with one effective-size constraint per subset of machines, measured at the parameter . The same LP technique underlies the budgeted variant in the same paper and enters the later -norm results (Molinaro 2019). Lemma 6 is a converse of the valid inequalities that needs only one constraint per machine, which is what makes the rounding through the generalized assignment problem possible.
All results here are proved on paper; none is formalized. A formalization produces a reusable effective-size calculus (Lemma 2, Jensen-type bounds) in Mathlib's probability library, an expected-maximum lower bound for independent variables (Lemma 1), and a Lean version of the Shmoys–Tardos rounding with costs. It also records two corrections found while pinning the statements: Lemma 5's inequality (3) fails under the threshold as printed (a -machine instance with expected makespan has ), so the threshold is an absolute constant ; and Lemma 1 requires independence, which the page omits.
The obvious approach maps every random size to one deterministic number and balances those. The paper shows (p. 7) that every such approach loses a factor on unrelated machines: the right effective size of a job depends on how many machines it competes for, which is not known in advance. The LP sidesteps this with exponentially many constraints, one per subset of machines, and the rounding cannot satisfy them all. The upper bound therefore rests on the class loop picking, for each machine, one parameter such that few machines have small classes and machines of large class have tails decaying like . On the lower-bound side, Lemma 4 rests on the Kleinberg–Rabani–Tardos analysis of Bernoulli variables, which the paper only cites, and Observation 2 rests on the Shmoys–Tardos rounding, also only cited.
Machines are Fin m with and jobs Fin n, both 0-based. The probability space is (Ω, P) with Ω : Type and IsProbabilityMeasure P; sizes are X : Fin m → Fin n → Ω → ℝ, each measurable, nonnegative and integrable (integrability keeps and the expected makespan from collapsing to the Bochner junk value ). Job independence is iIndepFun (fun j ω i => X i j ω) P, independence of the per-job vectors, not of all variables. Logarithms are natural. The makespan is the supremum over the finite set Fin m. Truncation keeps , the exceptional part keeps . is a junk value , never used.
The LP's are functions of , fixed by (6). The class loop is a recursion with fuel that recomputes each round; an unclassified machine gets the junk class , which Observation 1 rules out for feasible . The Shmoys–Tardos algorithm is represented by its guarantee: an output of the rounding is any assignment satisfying (13)–(14). The goal bounds every such assignment, which is stronger than bounding the one the algorithm returns, and (B) asserts that one exists. Running time, the ellipsoid separation oracle and the binary search over are not modelled.
None of the definitions mentions an optimal assignment or its value. A goal of the form "there exists with expected makespan at most " is ruled out: it is true with , because a minimizer exists among the assignments.
Corrected statements: Lemma 1 adds independence (and drops "discrete"); Lemma 5 and Proposition 1 replace the threshold by an absolute constant , with the of (4) equal to ; Lemma 4's is an absolute constant . Welcome contributions: the effective-size Chernoff bound, the Jensen facts, Observation 1 (pure combinatorics of the class loop), the union-bound and tail-integral steps of Lemmas 6–7, and a cost-preserving Shmoys–Tardos rounding.
Related platform results: UnrelatedSched.TwoApprox.rounding_load_bound and MatousekLP.Scheduling.rounding_makespan_le (Proved) carry out the Lenstra–Shmoys–Tardos rounding for deterministic sizes without costs; WilliamsonShmoys.generalized_assignment_cost_preserving_rounding (Open) is a cost-preserving GAP rounding with load at most . None of them states Observation 2.
A manager can influence a project's output through effort, but the owner observes output rather than effort. When the manager can also trade privately in a financial market, a contract based on output and market returns changes both effort incentives and the manager's ability to hedge risk. The owner must decide what the contract pays, how sensitive it is to output, and how much market exposure it gives the manager. Huang, Ju and Xing formulate these choices as a continuous-time control problem in Optimal Contracting with Unobservable Managerial Hedging, the November 2017 working paper underlying the later Management Science article. This mission uses the working paper's equations and numbering.
The question is operational: given an initial promise to the manager, which admissible contract maximizes the owner's discounted cash flow? The paper's Proposition 2.3 answers with a payment boundary, a liquidation boundary, and sensitivities chosen from a two-dimensional control box. Formalizing that proposition requires the value to come from the control problem itself. The free-boundary equation alone does not identify a contract or prove its optimality.
The state is the manager's contract value, with initial promise . The owner controls the contract sensitivity , gross market exposure , and a nondecreasing cumulative payment process . The two shocks and are independent standard Brownian motions. The project is liquidated at . Time-zero payment is permitted and is charged to the owner.
Effort lies in and costs . The manager's effort response is the minimizer of over that interval. The regular controls lie in and . With and , the state dynamics of equation (21) are
The principal's value is the least upper bound of expected payoffs over admissible contracts from . Equation (24) includes the discounted output and effort flow, the discounted payment measure, and the liquidation payoff , all scaled by . Admissibility includes the paper's transversality condition (57). The value is a control value, not an arbitrary solution of a differential equation.
The first target is the value characterization of Proposition 6.4. On the continuation interval , is twice continuously differentiable and satisfies
Here and . At and above , ; at the boundary, and . Proposition 6.4 also states concavity on and strict concavity on .
The mission goal is the stronger Proposition 2.3: for each initial promise, a reflected contract attains . It pays immediately, makes further payments only when the contract value is at , and liquidates when the value reaches zero. Before liquidation its sensitivities come from maximizers of the displayed Hamiltonian's control-dependent terms. The market sensitivity is recovered from and by .
Proposition 2.3 connects a value function to an implementable payment and risk-sharing rule. The upper boundary describes when the owner returns part of the manager's contract value as cash; the lower boundary describes termination. Concavity records the owner's endogenous aversion to leaving value exposed to the manager's future actions. Without the attainment statement, a smooth solution of the HJB could remain only a candidate and would not determine an optimal contract.
The working paper gives an argument for these conclusions; the statements here are open Lean targets. A complete development would check the stochastic control value, the regularity and comparison steps, and the existence of the reflected contract against the same definitions. The finite-horizon Itô integral and independent Brownian coordinates come from the published Peng1990.SMP.Stochastic definition. The effort clamp and the model-specific contract are new definitions for this mission.
The control has both regular choices and a singular payment process . If one optimizes an unconstrained payment rate as though it were an ordinary bounded control, the Hamiltonian is unbounded whenever . The correct value therefore has a gradient constraint and a free payment boundary. Showing that the resulting boundary rule actually attains the value also requires a reflected stochastic equation up to the liquidation time. The two Brownian shocks must remain separate: merging them changes the information available to the controls.
Lean represents as time-indexed real processes on an underlying probability space. Brownian coordinate zero is the market shock; coordinate one is the idiosyncratic shock. The filtration is the Brownian filtration supplied by Peng1990.SMP.Stochastic, and Itô integral conditions hold on every finite horizon. This is the reduced principal's problem (24). The manager's separate optimization in Lemma 2.2 and the original output and market processes are outside the model; incentive compatibility enters through .
The formalization uses real-valued payoffs and an explicit least-upper-bound condition for every , so empty or unbounded feasible payoff sets cannot silently produce Lean's default real supremum. The control box is compact under the standing interval assumptions. Its Hamiltonian and net-contribution suprema are therefore genuine finite suprema. The convention for an empty set in the definition of is , matching the degenerate zero-continuation case. Derivatives at zero use one-sided, within-set derivatives.
The paper's formulas use and the proof uses a diffusion coefficient bounded away from zero. The model explicitly assumes and in addition to the paper's stated interval and cost bounds. Admissible contracts have integrable drift and payoff and finite expected discounted payments, so a nonintegrable real integral cannot become zero by Lean's total-function convention. Payments use the Stieltjes measure of , extended by zero before time zero; this charges an immediate lump sum. The transversality limit is taken along deterministic times as in the proof of Lemma 6.3. The value is the supremum of admissible contract payoffs, not a function postulated to solve the HJB. Contributions formalizing the comparison theorem, the singular-control dynamic programming step, or the reflected equation are directly useful to the goal.
In many service systems a waiting customer is harmed not only by the time spent in line but also by the other customers met there. Contagion in a clinic, a pharmacy or a government office during an epidemic is the motivating example of Hassin, Meilijson and Perlman, Queueing with Negative Network Effects (SSRN 4097977, 2022; Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1223). There the cost of joining a queue is a function of the number of meets, the customers present in the waiting room at the same time. A customer who joins a queue meets those ahead of her and those who arrive while she still waits. The second number is random and depends on the capacity of the waiting room, because arrivals that find the room full are turned away.
Strategic queueing in the tradition of Naor (1969) assumes a cost linear in waiting time; with negative network effects the relevant random variable is the count of meets, and equilibrium joining strategies and socially safe capacity regulations both require its exact distribution. Section 4 of the paper computes it: first as a row of a matrix power (Theorem 2), then in closed form, jointly with the number of arrivals that fill the room to capacity (Theorem 3). This mission formalizes that section.
An FCFS M/M/c/n queue has Poisson arrivals at rate , servers each working at exponential rate , and a waiting room of capacity : an arrival that finds customers waiting is lost. The server utilization factor is , and
is the probability that the next change of the queue is a service completion while all servers are busy.
A tagged customer arrives at position : customers wait ahead of her. The queue length is the number of waiting customers, herself included, not counting those in service. While she waits, every change of the queue is either a service completion (everybody moves up one place) or an arrival (which joins at the end if the queue length is below , and is lost otherwise). She enters service at the -th service completion.
For , and ,
with probability elsewhere; has the same law as ; and the expectation formula (4) for and the generating function (5) for , , hold. The statement depends on only through , as printed.
The result. Theorem 3 gives the exposure of a joining customer in closed form, as a finite sum of binomial terms in , instead of a power of an matrix. Through (5) it gives the expected utility of a customer facing the exponential loss , display (6), which is the input to the paper's equilibrium and safe-threshold computations for that loss function. The joint law with also records how often the room is filled to capacity during one customer's wait, the quantity that a capacity regulation acts on.
Formalizing it. The paper proves Theorem 3 in an Online Appendix that is not part of the preprint, and states (4) and (5) as straightforward corollaries. To the best of a search of the Prove2Me library, no transient result about a tagged customer in a finite-capacity queue, and no path count for a reflected walk with a capacity barrier, has been formalized. A complete development would give a machine-checked account of an embedded-chain argument, of the identification of the matrix , and of a reflection-type counting identity with two barriers.
The obvious route to is to enumerate the sequences of arrivals and completions until the -th completion. Two features break a plain ballot-type count. First, the walk is reflected at the capacity : an arrival at a full room is lost, so trajectories with the same number of joining arrivals do not have the same probability, as the paper remarks (p. 10). Only after also fixing do all trajectories become equally likely, which is why the closed form is a joint law. Second, the walk is absorbed when the customer enters service, so the count must also respect the lower boundary, and the subtracted binomial terms account for both constraints at once. Connecting the closed form back to the matrix of Theorem 2 requires identifying as the transition matrix of the queue size at consecutive service completions, a statement that itself relies on the memorylessness of the exponential clocks.
IsEventSeq). The reduction from the continuous-time queue to this sequence is the paper's own ("the probability that the next change will be a service completion", p. 9); it is disclosed, not formalized.A household can borrow against expected future income only while repayment remains preferable to default. In the baseline model of Choi, Koo, Lim and Yoo, this choice is imposed through a participation condition at every date: the household's remaining utility from its planned consumption must be at least its remaining utility after default. The constraint changes the borrowing limit from the present value of income to a smaller level that depends on the default penalty. Determining that level is useful for understanding which debts are sustainable when income fluctuates and contracts cannot force repayment. The paper gives a closed form for the limit and for optimal financial wealth in its baseline continuous-time model (Proposition 3.2, p. 11).
The result is known mathematically: it is stated and proved by the authors, with the proofs placed in an Online Appendix. This mission targets a machine-checked formalization of the baseline result. It also identifies smaller claims about the constants and the optimal multiplier that are useful independently of the stochastic verification theorem.
The household receives income with initial level . Its growth is a geometric Brownian motion driven by two independent standard Brownian motions and . The first is the source of risk priced by the traded stock; the second is the remaining income risk, which the paper assumes can be hedged. The state-price density prices future consumption. In the formal model both processes are given explicitly:
where . The rate gives the present-value benchmark for income. These are the paper's mortality-adjusted , , and discount rate ; the mortality intensity has already been absorbed into them (§2.1, pp. 4–6 of the preprint).
For risk aversion , , utility is . A consumption plan is a positive process measurable as information arrives. It is feasible from wealth when its discounted net cost satisfies and, at every , it meets the conditional participation constraint
Here is the information generated by the two Brownian motions through time , and is consumption after default. A larger means a less severe default penalty. The paper restricts and defines from its other parameters in (2.7) (pp. 6–7 of the preprint).
The endogenous credit-limit coefficient is
where , , and the positive quadratic root have exactly the formulas in (2.7) and Proposition 3.1. The first targets establish , , and . Proposition 3.4 then gives the dependence on the default fraction:
The central target is Proposition 3.2. For , the candidate consumption plan is feasible and maximizes expected utility among all feasible plans. Its optimal wealth , defined as the conditional present value of future net consumption, satisfies the closed form (3.10) and the bound
For , the feasible set is empty: the household defaults immediately. On the way, the mission states the two duality results of §3.1 that the paper's argument rests on. With a Lagrange multiplier for the budget and a non-decreasing shadow-price process , , for the participation constraints, the dual objective (3.4) is minimized by the running maximum
(Proposition 3.1, for multipliers with ), and the primal value satisfies the duality relation (Theorem 3.1). The algebraic milestones also identify the binding level and the unique admissible initial multiplier solving Proposition 3.3's equation. These targets follow §§3.1–3.2, pp. 8–12 of the preprint.
The coefficient turns a family of conditional participation conditions into a usable state-dependent debt bound. Its comparison with quantifies the difference between a limit based on priced income alone and one that lenders can sustain when the household can default. Proposition 3.4 states precisely how that bound shrinks as default becomes more attractive; at it reaches zero. The wealth formula also says where the optimal policy sits relative to the boundary at every time, rather than only at the initial date (Propositions 3.2 and 3.4 of the preprint).
Formalizing the result supplies reusable definitions for a continuous-time consumption problem with conditional participation constraints and a stochastic income stream. The constants, multiplier equation, and binding-level facts are separate theorem targets; the final theorem must additionally verify feasibility, optimality, and the conditional wealth identity. The present proposal contains open Lean statements, not verified Lean proofs.
The natural-limit calculation prices future income, but it does not establish an incentive-compatible borrowing limit: a plan can meet its time-zero budget and still violate participation at a later date. The candidate shadow price depends on the running maximum of an income-adjusted dual process, so the wealth identity involves an infinite-horizon conditional expectation of a path-dependent consumption process. The same candidate must satisfy every conditional participation condition and outperform every feasible plan. Checking only the closed formula for or defining wealth by the right side of (3.10) would leave these claims unproved. The paper places its detailed proofs in an Online Appendix unavailable with the pinned preprint.
Lean uses time , real-valued wealth and utility, and a natural uncompleted filtration generated by two Brownian coordinates. Infinite time integrals are over the real interval . Each participation condition holds almost surely for each fixed , matching conditional expectations' almost-sure meaning. The running maximum defining the shadow price ranges over ; continuous Brownian paths make that range compact. Its initial value is zero almost surely, as is the Brownian starting value, and it is nonnegative on every path. The optimization statement uses a greatest element of the feasible utility values, avoiding a real supremum with a default value on an empty or unbounded set.
The printed Problem 2.2 mentions a default time but does not define it. The formalization uses the static martingale budget that §3 prices in its Lagrangian; it represents consumption rather than the stock and futures positions. This is the form of the problem for which the goal states optimality. Plans carry the integrability needed for their budget, utility, and conditional expectations. The source leaves and a positive leading coefficient of the quadratic unstated; both are explicit because the reservation value and closed-form real powers otherwise become ill posed. Plans are strictly positive, so that utility is never evaluated at zero. The dual value is not defined as a real infimum: the duality relation is stated with least elements of the explicit set of values of the dual objective, and the integrability conditions (3.2) on shadow prices are genuine finiteness requirements, never default values. The optimal-stopping representation of the dual (Lemma 3.1) is not formalized. The initial multiplier is restricted to , the branch that makes the shadow price start at zero. The endpoint appears only in the comparative-statics result for , whose formula remains defined there.
The shared Brownian and Euclidean-state definitions are reused from the platform. The new model, candidate process, real-power calculus, conditional integrability, and stochastic verification are available as distinct contributions. The goal cannot be discharged by assuming optimality or by defining to equal (3.10): it identifies wealth through a conditional present value and proves the displayed formula separately.
In the rough Heston model of El Euch and Rosenbaum, the variance of an asset is driven by a fractional kernel with Hurst exponent , which matches the roughness observed in realized volatility. The model keeps one feature of the classical Heston model: the characteristic function of the log-price is explicit up to the solution of a deterministic equation, here a fractional Riccati equation
with complex coefficients that depend on the Fourier variable (El Euch–Rosenbaum 2019). Pricing a vanilla option by Fourier inversion requires this solution for many complex parameters, and the equation has no closed form. The standard numerical method, the fractional Adams scheme, is slow because of the memory of the fractional derivative.
Callegaro, Grasselli and Pagès (arXiv:1805.12587v4) observe that with zero initial condition the solution is a fractional power series whose coefficients obey an explicit convolution recursion. The series can be summed very fast, but only on its interval of convergence; beyond it they switch to a hybrid numerical scheme. Where the switch happens is governed by the convergence radius, and their Theorem 3.3 bounds it explicitly from below and, for parameters of equal sign, from above.
Fix and . Identifying the coefficients of the series in the Riccati equation yields the coefficient recursion (3.19)–(3.20):
where is the discrete convolution (so ). Each depends on only, so the sequence is uniquely determined; in Lean it is coeff α lam mu nu : ℕ → ℂ.
The convergence radius of is given by Hadamard's formula (3.21):
in Lean radius α (coeff α lam mu nu). With , and the Beta function , the paper introduces the constants
For :
In attack order: the Riemann-sum Lemma A.1 (A.39); Kershaw's Gamma-ratio inequalities (A.41); the coefficient upper bounds of (B.49) for and (B.51) for ; Proposition B.1 (a) (for the even coefficients vanish and solves (B.50)) and (b) (comparison ); Theorem 3.3 (c) (sign symmetry ); the lower-bound propagation of §B.1.2 (); the Riemann-sum bound (B.52) with ; and the lower-bound propagation of §B.2.2 ().
The lower bound is an explicit, parameter-dependent time up to which the series converges absolutely: on the Riccati solution, and with it the rough Heston characteristic function, can be evaluated by summing a series with no discretization error. The upper bound shows that for parameters of equal sign the radius is finite and of order , which is why the paper's hybrid scheme (series near , a numerical scheme beyond) is needed for long maturities. The two bounds together fix the scale on which the hybrid scheme switches methods.
The result is proved in the paper (Appendix B). The proof has not been machine-checked. A formal development adds a checked convergence guarantee for a recursion used in option-pricing code, and its auxiliary results (Kershaw's inequality for the Gamma function, which the pinned Mathlib does not contain, and Riemann-sum bounds for symmetric monotone functions) are reusable outside this paper. The paper prints a strict inequality ; its proof gives , which is what the goal asks. Upgrading to the strict inequality would be a sharpening beyond the paper.
The obvious approach is to bound by a geometric sequence and propagate the bound by induction through the recursion. It fails: the convolution contributes a factor that the Gamma ratio absorbs only when , and then with constants that are far from sharp. The propagated bound therefore needs a polynomial correction . That turns the convolution into a Riemann sum of , which is convex for and concave for , and controlling it takes a non-asymptotic Gamma-ratio inequality valid for every rather than Stirling asymptotics. For the upper bound on the radius, the coefficients must be bounded from below, which requires positivity, the vanishing of the even coefficients when , and a separate comparison between the cases , and .
Everything is stated about the coefficient sequence and its Hadamard radius. The fractional derivative, the Riccati equation itself and the function do not appear, as in the paper, which identifies the coefficients formally. Conventions:
coeff α lam mu nu : ℕ → ℂ, with ; the convolution at index runs over (Finset.Ico 1 j). Gamma factors are Real.Gamma of real arguments, cast to ; for every argument is at least .radius α a = liminf_{k→∞} ‖a k‖₊^{-1/(α k)} in ℝ≥0∞, with for , so vanishing coefficients (all even ones when ) do not lower the radius. Real bounds enter through ENNReal.ofReal.A trivializing formalization is excluded: the radius is Hadamard's in , not a supremum of convergence points computed in (which would be on an unbounded set), and the recursion carries the paper's and conventions, so that and, at , the coefficients are those of (), with and .
A complete development needs: real-analytic Gamma-function inequalities (log-convexity is in Mathlib; Kershaw's bounds are not); Riemann-sum estimates for symmetric monotone functions on ; the Beta integral (Mathlib has Complex.betaIntegral); and manipulations of -th roots in ℝ≥0∞. The Gamma-ratio and Riemann-sum lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the radius bounds, are welcome.
Not formalized: the "Moreover" sentences of Theorem 3.3 (b) (monotonicity and blow-up of the maximal Riccati solution) and (c) (convergence at the radius), the non-homogeneous Theorem 6.1, and the numerical scheme of §4–§5.
Whether a customer joins a queue depends on how congested she believes it is. Classical strategic queueing studies two extremes. In the visible queue of Naor (1969) every arrival sees the queue length and joins exactly when her net payoff is nonnegative; in the invisible queue of Edelson and Hildebrand (1975) arrivals see nothing and act on the stationary distribution alone. Many service systems sit between the two: a call centre announces nothing, a restaurant can be inspected only at some effort, an online service shows a vague busy indicator. Customers there can learn about congestion, but learning costs time and attention.
Canyakmaz and Boyacı model this middle ground with rational inattention (Sims 2003; Matějka and McKay 2015): each customer chooses what to learn about the number of customers in the system, paying a cost proportional to the mutual information between what she learns and the true state, and then joins or balks. Because every customer's prior is the steady-state distribution generated by everyone else's joining behaviour, the model has a fixed-point structure, and the basic question is whether a consistent pattern of beliefs and behaviour exists and whether it is unique. Theorem 1 of the paper answers both questions affirmatively for every positive information cost. The paper's later results (comparative statics, revenue-maximizing prices, the limits of a visible and an invisible queue) are all statements about this unique equilibrium.
Customers arrive to a single-server first-come-first-served queue as a Poisson process with rate ; service times are exponential with rate ; . A served customer receives the reward , pays the price , and pays per unit of waiting time. A customer who finds customers in the system and joins gets the expected payoff
and it is assumed that , so . Balking is worth .
The customer does not see ; she holds a prior on it and pays per unit of mutual information acquired. The paper reduces her problem to a choice of the unconditional joining probability :
after which she joins in state with probability given by the generalized multinomial logit formula
If all customers use , the queue is a birth–death process with arrival rates and service rate . Its unnormalized weights are , ; when ( is admissible) the stationary law is .
An equilibrium (Definition 1) is an admissible such that, with and , the consistency equation holds and solves (9) under the prior .
For all parameters with and ,
No relation between and is assumed: when the equilibrium joining probability is strictly below one.
The milestones follow the paper's proof of Theorem 1 and its Lemmas 1 and 2:
Existence and uniqueness are what make the model usable. The paper's comparative statics in , , , (Proposition 1), its unimodal revenue curve (Proposition 2), and the limits and recovering Naor's and Edelson–Hildebrand's equilibria (Corollary 1) are all statements about "the" equilibrium; without Theorem 1 they would have no object. The result also shows that information frictions do not create multiplicity here, in contrast to many congestion games with strategic complementarities.
The result is proved in the paper; nothing in it is open. As far as a search of the Prove2Me library shows, none of it is formalized: there is no machine-checked treatment of rational-inattention choice in queues, of the reduced problem (9), or of the monotone comparative statics of birth–death stationary laws in a joining parameter used here. A formalization would produce reusable pieces for strategic queueing (product-form laws with state-dependent arrival rates, single-crossing of stationary distributions) and for rational inattention (the first-order characterization of binary choice with Shannon cost).
The obvious argument — the best response is continuous, starts at and ends at , so it crosses the diagonal — fails at the right endpoint when : then is not admissible, the stationary law does not exist there, and the inequality that the paper's intermediate-value argument uses is not available. The behaviour of the best response as has to be controlled by an argument the paper does not give.
The uniqueness step of the paper compares first-order conditions under two priors. Turning that comparison into a statement about maximizers requires handling the boundary solutions of (9), where the first-order condition is an inequality, and the endpoint , where is unbounded below and the derivative series may diverge.
All series are infinite: interchanging differentiation and summation, and continuity of in , need domination arguments that the paper does not spell out.
Everything is in OpaqueQueue.Equilibrium. Parameters form a structure Params with fields lam, mu, R, p, C, θ; the standing assumptions and are the predicate Params.Standing. Values are real; states are natural numbers; the logarithm is natural. joinProb P q n is , weight P q k is , Admissible P q is together with summability of , stat P q n is , obj P g x is the objective of (9) for a prior g, IsOptimal P g x says solves (9), and IsEquilibrium P q is Definition 1. stat divides by a series that Lean evaluates to when it diverges; every statement about it therefore assumes admissibility.
IsEquilibrium requires optimality of in (9) under the equilibrium prior, besides the printed equations (14)–(15). Those equations alone are satisfied by for every parameter value (and by whenever ), so reading Definition 1 without optimality would make Theorem 1 false. The paper's own proof uses the optimizer of (23) as the best response. Stating the goal as the existence of a unique fixed point of an arbitrary or choice-based best-response function would also be unfaithful and is ruled out.
Lemma 1 is stated for priors with finite mean, under which (9) is finite on all of . The paper states it for the joining policy of problem (6); the mission states it for problem (9), to which the paper reduces (6). The reduction itself (Matějka and McKay 2015; Caplin, Dean and Leahy 2016), Corollary 1, Propositions 1–4, Theorems 2–3 and the numerical sections are outside this mission.
A complete development needs: summability and continuity of parameter-dependent series, concave maximization on an interval with one-sided derivatives, and single-crossing and stochastic-dominance arguments for laws on . Proofs of individual milestones, alternative arguments, and general lemmas on product-form birth–death laws are all welcome.
Sell-side analysts are ranked against each other. Published rankings, such as Institutional Investor's annual "All-Star" ranking cited in the paper, and the career outcomes tied to them, reward an analyst for being more accurate than peers, not only for being accurate. A common intuition holds that such competition disciplines analysts and makes their forecasts more informative for investors. Sanjay Banerjee's paper Does Competition Improve Analysts' Forecast Informativeness? (working paper, Alberta School of Business Research Paper No. 2017-311, 2017; later published in Management Science, doi:10.1287/mnsc.2019.3544) asks whether that intuition survives a model in which analysts best-respond to each other strategically.
The paper places itself next to the multi-sender cheap-talk literature (Krishna and Morgan 2001, Battaglini 2002). There, several senders typically reveal more than one. Two features separate this model: forecasts are scored against the realised state, and analysts' private signals are correlated conditional on the state. Its main result identifies exactly when competition makes forecasts less informative.
A state has prior ; for measuring information, and , so . Two risk-neutral analysts each observe a private signal of precision . Given the state, the signals have correlation . With , each ordered pair of signals has conditional probability if both equal the state, if both differ from it, and if they disagree.
Each analyst forecasts . A symmetric strategy is , with and . Under competition, an analyst whose forecast alone matches the state earns , the other earns , and identical forecasts earn each, with . The payoff convexity is
and the payoff is convex if , concave if . In the benchmark, an analyst is paid for his own accuracy only.
A symmetric equilibrium is a with such that, for each signal, the prescribed probability of a truthful forecast maximises the analyst's expected payoff, computed by Bayes' rule, when the other analyst plays . It is pooling if and separating if . A most informative equilibrium is an equilibrium that is coordinatewise at least every other equilibrium of the same game. Forecast informativeness is the posterior precision normalised by the prior precision,
Finally, the separation threshold of the rank game is
Fix , and with , and restrict to , as the paper does ("Results for are symmetric"). Let and be most informative equilibria of the rank game and of the benchmark at . Then
and conversely, if and , then for every both most informative equilibria exist and every such pair satisfies .
The paper prints "". At informativeness still drops (for , , : ). On it does not drop, because the separating profile remains an equilibrium. The interval is the paper's own reading: " at " (p. 26).
The milestones are the paper's numbered results that the proof uses:
The result. Proposition 5 (B.1) is the paper's main counterintuitive finding. Convex rank incentives combined with correlated information make analysts understate their private signals in order to differentiate themselves, and the market learns less than it would from two analysts who ignore each other. The conditions are sharp: with uncorrelated signals or a concave payoff, competition never lowers informativeness at . This is relevant to the design of analyst rankings and of tournament incentives for forecasters more generally.
Formalizing it. The result is proved on paper through seven claims and a case analysis over regimes of . The case analysis contains slips, such as the empty interval in Lemma 1, a sign error in (B.28), and boundary cases and assigned to the wrong regime. A machine-checked proof would settle the exact statement. To the best of our knowledge none of these results has been formalized; the mission produces the first formal model of this game.
Each analyst's best response depends on the other's strategy through a conditional law of the other's forecast, which is affine in , and through Bayesian posteriors, which are ratios of such terms. The equilibrium conditions are therefore piecewise-affine inequalities whose sign pattern changes with . The obvious argument would compute a single equilibrium and compare informativeness. It fails because the goal speaks of the most informative equilibrium. One must show that no other equilibrium dominates it coordinatewise, and in the high-convexity, high-correlation regime the relevant equilibrium is fully mixed and is defined through an implicit root (). The "only if" half requires excluding a decrease in every other regime, including , where the benchmark pools and one needs .
States, signals and forecasts are Bool (true = H, h, ĥ). A strategy is a pair σ : ℝ × ℝ, and the equilibrium set carries the restriction of p. 9. Expected payoffs are conditional expectations of the rank payoff (3) under the joint signal law and Bayes' rule. The equilibrium condition is that the prescribed mixing probability maximises the expected payoff over all of . The benchmark pays for a correct forecast, a positive rescaling of the paper's . A forecast pair of probability zero contributes zero to the expected posterior variance. The paper's standing restriction is part of the goal: below one half the decrease occurs on the mirror interval , and the condition would be vacuous.
The trivializing formalizations are ruled out. The net payoffs and informativeness are computed from the primitives, never from the paper's closed forms (A.13)–(A.14) or Lemma 3. The "if" half asserts that the most informative equilibrium exists. The benchmark value is the benchmark game's own most informative equilibrium, not written into the statement.
The "Furthermore, the decrease in information revelation increases with payoff convexity" clause is not part of the goal. Neither are Proposition 5 (A) and (B.2), Propositions 2 (B) and 3 (B), Lemmas 2–3, Proposition 4, Claim 6 and Appendix C. Corrected milestones are labelled in their titles:
A complete development needs:
Bool;The finite Bayesian-game layer (symmetric equilibria of a two-player game with binary types) is reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.
Naive Bayes is one of the oldest and cheapest classifiers for text and count data: given word counts for documents in two classes, it fits one multinomial distribution per class by maximum likelihood and classifies by the likelihood ratio. Its cost is a single pass over the data. In high-dimensional applications (text, genomics) one also wants the classifier to depend on few features, both for interpretability and to discard noise. Imposing that the two class distributions differ in at most coordinates turns maximum-likelihood fitting into a cardinality-constrained, nonconvex problem.
Askari, d'Aspremont and El Ghaoui (arXiv:1905.09884, Mathematics of Operations Research, 2024) show that the Lagrangian dual of this sparse problem is a one-dimensional convex problem solvable by bisection at essentially the cost of naive Bayes itself, and that its value is within a shift of four features of the true optimum. The shift comes from a duality-gap bound for separable problems in the line of Aubin and Ekeland (1976) and Ekeland and Temam, based on the Shapley–Folkman lemma.
There are features. A nonnegative data matrix with labels enters only through the class sums (the total count of each feature in each class), assumed entrywise positive. Write and .
The sparse multinomial naive Bayes problem (SMNB) at sparsity level is
where counts the coordinates in which the two class distributions differ. Without the last constraint the problem is ordinary naive Bayes.
For a vector , is the sum of its largest entries. Let
and . The relaxation (USMNB) has value
It is a convex problem in one variable. Its dual (D) is a concave maximization over with , which plays the role of a fractional feature-selection vector.
For ,
The constant four does not depend on , or the data. Numerically it is not tight (a shift of one suffices on random instances), but the goal keeps the paper's constant.
Milestones 1–6 follow the paper's proof of Theorem 3.6; milestones 7–9, on top of 1–4, are the paper's second, constructive route to the upper bound .
The theorem certifies that a convex problem of negligible cost brackets a nonconvex, combinatorial maximum-likelihood problem: the relaxation's value at lies between the true values at and . Whenever varies slowly in , which the paper observes past the "elbow" in the number of relevant features, the duality gap is small, and Propositions 3.8–3.9 turn the relaxation's solution into a sparse classifier with at most four extra features. The paper uses this to run feature selection on data sets with millions of features.
The results are proved in the paper (Theorem 3.5 is quoted from the literature). None is formalized. Formalizing them yields the perturbation-function duality-gap bound for separable nonconvex problems as a reusable statement, a verified variational formula for top- sums, and a check of a printed formula: the dual (D) as printed carries a spurious term , and the formal statement uses the corrected objective.
The lower and middle inequalities are weak duality once the dual is computed, and computing it is a separable calculation. The upper inequality is the content: it bounds a duality gap, and nothing in the one-dimensional structure of (USMNB) gives it. The naive approach, rounding the fractional of (D) to its top coordinates, has no a priori control on the loss. Both of the paper's routes need a Shapley–Folkman type argument, in which the number of nonconvex contributions is bounded by the number of constraints plus one. The Shapley–Folkman lemma itself is not in Mathlib (it is an open goal on the platform), and Theorem 3.5 also requires conjugates of extended-valued functions and the convex envelope of a sum of separable terms.
Features are indexed by Fin m, with fp fm : Fin m → ℝ entrywise positive. This positivity is stated on p. 7 and is needed because the formulas take . The standing assumption of §3.1 is carried by every statement about (SMNB). The commitments are:
EReal-valued functions on Fin d → ℝ. The conjugate is a supremum (p. 9 prints an infimum), and finiteness of each is added in Theorem 3.5 so that is a real vector.Proposition 3.8 is stated with the additional conclusion that the constructed point's value is at least the optimum of (D). Its proof establishes this, and without it the statement is met by a maximizer of and says nothing about (D).
A complete development needs Lagrangian duality for a separable problem, the perspective of , top- sums and their LP dual, Fenchel conjugates of extended-valued functions, and a Shapley–Folkman lemma. The last three are reusable well beyond this mission, and contributions there are welcome.
A seller of a product that gives immediate pleasure and delayed harm faces consumers who may plan to limit consumption and then consume more than planned. This setting applies to the paper's examples of cookies, soft drinks, cigarettes, and alcohol. A personal consumption goal is one way a consumer may restrain overconsumption. The question for the seller is whether that restraint calls for a lower or a higher price. In Amaldoss and Harutyunyan's model, both answers are possible: the direction changes with the harm from one unit of the product.
This mission formalizes the paper's comparison between the monopoly price when consumers set personal goals and the price when they have no goals. The comparison is Proposition 1 of the September 2022 SSRN version, p. 14 (PDF 15). The model is intentionally narrow. Consumers are identical, the seller has a single product, and all uncertainty is absent. These restrictions make it possible to isolate how a goal changes consumption and willingness to buy without attributing a price change to market heterogeneity or a change in production cost.
A unit mass of identical consumers obtains consumption value from quantity , where is the initial marginal value. Each unit causes delayed harm . A unit costs to buy. The seller's marginal production cost is normalized to zero. At the consumption stage, consumers discount harm by a present-bias factor with . Earlier, when deciding whether to buy and when choosing a goal, they count the harm without this discount. The quadratic coefficient is fixed at , as in §3 of the paper, pp. 7–9 (PDF 8–10).
A consumer may choose a personal goal . Consuming more than incurs goal disutility , with ; consuming no more than incurs none. Thus the benchmark utility when quantity is chosen is
and the utility with a goal is . The earlier planning-stage utility without a goal replaces by . With a goal, the same penalty is present at the goal-setting stage. These are the utilities in §4.1–4.2 of the paper, pp. 10–12 (PDF 11–13).
The sequence is price, purchase plan, personal-goal choice, quantity choice, and delayed harm. At the planning stage, a consumer correctly anticipates the subsequent goal and quantity choices. The consumer buys exactly when that anticipated utility is at least zero. Because the consumer mass is one, aggregate demand is the quantity purchased by one consumer. The seller chooses a nonnegative price that maximizes price times demand. The benchmark omits the goal and its penalty; the personal-goal regime includes both.
The supporting targets characterize the consumer's optimal quantity without a goal, benchmark demand, and the benchmark monopoly price; then optimal quantity at a fixed goal, optimal goal, the personal-goal reservation price, demand, and the personal-goal monopoly price. Each is indexed to an equation or paragraph in §4.1–4.2 of the SSRN version, pp. 10–14 (PDF 11–15).
The goal is Proposition 1. Define the comparison threshold
For , both monopoly problems have equilibrium prices. For any benchmark equilibrium price and personal-goal equilibrium price , the target is
The comparison does not assert a strict ordering at . The paper's statement describes more and less unhealthy products relative to ; its standing section range is (Proposition 1 and preceding paragraph, p. 14, PDF 15). The formal goal uses a strict upper endpoint for the price-uniqueness reason explained below.
The result identifies two opposing price outcomes under one behavioral change. A personal goal reduces the quantity purchased conditional on buying. It can also raise the price at which the consumer is willing to buy. Proposition 1 identifies which effect determines the monopoly price as harm varies. For a product below , the goal regime has the lower price; above , it has the higher price. The threshold is an explicit expression in valuation, present bias, and goal sensitivity, so the comparison is a parameter statement rather than a numerical illustration (Amaldoss and Harutyunyan, pp. 13–14, PDF 14–15).
The result is already proved in the paper, including a separate proof in the Web Appendix, pp. 2–4 (PDF 34–36). The proposed Lean statements have no machine-checked proofs yet. Formalizing this result would connect the paper's sequential consumer decisions to both monopoly optimization problems under one consistent set of definitions. The quantity, goal, participation, and price characterizations are useful beyond the final comparison: they state exactly where purchase on indifference and zero demand matter. They also provide a small reusable example of present-biased planning in a sequential pricing model.
The quantity choice changes formula at the goal: the goal penalty is active only above . Goal choice therefore depends on an anticipated optimum of a piecewise utility, while purchase depends on the utility of the resulting choice. A price that maximizes revenue must account for a jump from positive demand to zero demand at the consumer's reservation price. The tempting intuition that reduced conditional quantity always lowers the seller's optimal price fails because the purchase threshold also changes. The paper's two price formulas each have separate parameter regimes, and the comparison reverses only at the stated (§4.2 and Web Appendix, Proof of Proposition 1, pp. 12–14 and WA pp. 2–4).
All model quantities are real. Feasible purchase quantities, goals, and prices are nonnegative. The standing parameters satisfy , , , and ; Proposition 1 additionally assumes . The cost normalization and satiation coefficient are fixed. The goal penalty uses the strict indicator . A consumer buys when anticipated planning utility is nonnegative, including equality. This tie rule matters when the seller sets a reservation price.
The main comparison assumes . The paper takes in the remainder of the section, but at equality benchmark demand is zero at every nonnegative price, so every such price maximizes the same zero revenue. A comparison quantified over all equilibrium prices would then be false. The strict bound records this endpoint issue explicitly. Similar zero-consumption or zero-demand endpoints are excluded only where a milestone claims a unique goal or price.
The Lean definitions specify optimal quantities, optimal goals, demand, and monopoly prices through global maximization over the stated domains. Demand is derived from utility and the purchase rule. It is never defined by the closed-form equations that the milestones are meant to establish. This prevents the target from becoming true merely by defining prices to equal the paper's answers. The generic revenue-maximizer relation is a separate definition; the paper-specific model supplies its demand relations. A complete proof can use Mathlib's real-order and square-root theory together with reasoning about piecewise quadratic functions. Contributions that establish the consumer choices, purchase threshold, demand, or either price characterization are within scope.