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?
A service platform makes decisions on two sides of a market. It charges consumers a price and pays independent providers a wage, then earns a margin only when it can match a consumer with a provider. Capacity is another decision available to the platform: it can limit how many matches it will carry, for example by limiting the active provider pool. Hu and Liu ask whether committing to this limit before setting price and wage changes the competitive outcome. Their submitted manuscript models this question for two competing platforms and states a two-sided counterpart of the quantity-precommitment result associated with Kreps and Scheinkman. The point matters for platform operations because a capacity decision can determine the price, wage, volume, and profit that emerge after both platforms react. Hu and Liu, submitted manuscript, §3.5.
There are two platforms, indexed by ; denotes the other platform. The potential market size is . Each platform posts a consumer price and a provider wage . Demand and supply are the positive parts
where . The demand substitution factor and the supply substitution factor both lie in . Higher rival prices raise a platform's demand; higher rival wages reduce its supply. A platform can serve only the smaller of its demand and supply. Its profit without a capacity limit is the margin times that number of matches. These are the manuscript's displays (1)–(3). Hu and Liu, submitted manuscript, pp. 8–9.
The first game is quantity competition. Each platform chooses a nonnegative matching quantity . The prices and wages that clear demand and supply at those quantities are
A platform earns . A quantity Nash equilibrium is a nonnegative vector at which neither platform can gain by choosing any other nonnegative quantity while the rival quantity stays fixed. The inverse price and wage appear in the proof of Lemma 6, where the profit function is written as (F.3). Hu and Liu, submitted manuscript, p. 14 and Online Appendix p. 32.
The second game is capacity precommitment. In stage one, each platform chooses a nonnegative capacity , the most matches it can make. In stage two, both platforms simultaneously choose prices and wages. Platform then serves matches and earns . A second-stage Nash equilibrium lets a platform change its price and wage together. A subgame-perfect equilibrium specifies stage-two play after every admissible capacity vector and requires that no platform benefit from changing its stage-one capacity and then following the continuation for the changed vector. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix §A.
The goal is Proposition 1: capacity precommitment and quantity competition have the same equilibrium price, wage, matching quantity, and profit for each platform. Writing for a capacity profile and its continuation plan, and for a quantity equilibrium, the target is
The goal also asserts that an equilibrium of each game exists, so this comparison has actual outcomes to compare. Lemma 6 gives the unique quantity equilibrium and its closed forms. The subgame analysis in Online Appendix §A.1 gives a platform's best response to fixed rival price and wage. Lemma 7 states that demand and supply both equal committed capacity in the two-stage equilibrium. These three statements are the mission's milestones. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix p. 1.
Proposition 1 supplies an operational interpretation of quantity competition in a market where each platform controls both consumer price and provider wage. A quantity outcome can arise through an earlier capacity choice followed by ordinary spot-market price and wage decisions. The conclusion covers four separate outcomes for each firm, so it supports comparisons of capacity policies in terms of what consumers pay, what providers receive, how many matches occur, and platform profit. The result is proved in the manuscript; its proofs are in Online Appendix §F of the same cited artifact. Hu and Liu, submitted manuscript, p. 15 and Online Appendix p. 33.
The formalization asks for machine-checked proofs of these known statements under explicit equilibrium conventions. It also creates reusable definitions for a two-sided market with positive-part demand and supply, a quantity game, and a two-stage capacity game. The paper's displayed formulas become auditable statements about every equilibrium of those games rather than numbers inserted into the definition of an outcome. No machine-checked proof of this specific proposition is asserted here.
The central issue is the full two-stage game. A stage-two platform changes price and wage jointly, and a stage-one capacity deviation leads to a new stage-two equilibrium. Checking a price deviation while holding wages fixed, or checking only capacities near a proposed equilibrium, does not establish the proposition. The positive parts in demand and supply also create zero-profit price-and-wage equilibria. Such equilibria can be used as off-path continuations and can change the set of stage-one equilibria. The formal target therefore selects positive profit for each platform whenever a subgame equilibrium permits it. The manuscript's Appendix §A distinguishes several regions of capacity profiles; this regime structure is part of the difficulty of proving a statement about all deviations. Hu and Liu, submitted manuscript, Online Appendix §§A.1–A.2.
Lean uses Fin 2 for platforms and a named rival map. Prices and wages are real-valued. Capacities and chosen quantities are nonnegative reals. The standing parameters are and ; these ranges keep the market-clearing denominators and nonzero. Demand and supply retain the manuscript's positive-part operation even when it is inactive at a positive equilibrium.
A continuation plan maps every capacity profile to a pair of price and wage profiles. At every nonnegative capacity profile it must choose a second-stage Nash equilibrium. For each platform, if that subgame has an equilibrium in which it earns positive profit, the chosen equilibrium must give it positive profit. This includes a subgame in which its rival committed zero capacity. This selection is an explicit addition to the printed equilibrium language, needed because the unqualified statement admits zero-profit off-path punishments. The stage-one Nash condition evaluates a capacity deviation using the continuation plan at the deviated capacity. The manuscript does not specify strategy sets; the stated real and nonnegative domains make them explicit. The goal ranges over equilibria rather than defining outcomes from Lemma 6's closed forms, and it asserts existence to prevent a vacuous comparison.
Contributions can establish the market-clearing identities, the quantity equilibrium and its uniqueness, joint price-and-wage best responses, the capacity-binding result, and the existence and outcome claims of Proposition 1. The generic two-player Nash predicate and the positive-part market model are reusable beyond this mission.
A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.
The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.
For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:
The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.
For vehicle count k, arrival rate a, region S, and density g, write the workload factor as
The heavy traffic expression from the paper's Theorem 3 is
The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.
For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor
When η < 1, the target is the two sided estimate
The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.
The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.
The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.
The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.
The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.
Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.
The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.
A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.
In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.
The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).
There are two privately known product qualities, . A seller commits to a price pair , where is paid by crowdfunding backers and is charged in the regular selling period. The project needs a financing target , so a feasible pair satisfies and . Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).
All funding customers have the same taste , uniformly distributed on and unknown to the seller. They believe quality is and back the campaign when . Thus success has probability . After a successful campaign, true quality becomes known. A fraction of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times is at least (manuscript, pp. 10–11).
Write for the seller's expected total profit when true quality is and customers believe . The expressions and distinguish the regions in which returning customers buy for sure or with a conditional probability. Write for the maximum of over feasible pairs. In particular, is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).
In a separating equilibrium, the two seller types choose different feasible pairs and . Funding customers believe the product is high quality exactly at and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).
Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in . Its crowdfunding price is
and its retail price follows the three cases of equation (11), depending on whether lies below , between that threshold and , or above the second threshold (manuscript, p. 23, Lemma 4).
The goal is Proposition 2 in the small-quality-gap regime . Define by its equations, requiring :
When , the goal states that the unique separating equilibrium surviving the intuitive criterion has and the low type at his full-information optimum. Relative to every full-information optimum of the high type, it also states
The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).
The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).
The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.
The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds , in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).
Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains , with , and . The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed and remain available for the page 41 equations; is only used away from its zero denominator. Suprema range over all feasible pairs , , and “optimal” means the displayed pair attains that supremum.
The manuscript's Proposition 2 needs the additional bound . Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with ; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all . Lemma 4 also records its displayed domain . The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.
The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.
Markets with network externalities can support several levels of adoption at the same price. A consumer's willingness to buy may rise when many other consumers buy, while the ordinary price effect still works in the opposite direction. A price and an aggregate demand curve can therefore identify several self-consistent quantities without identifying which one consumers reach. In Network Externalities and Market Dominance, Akerlof, Holden and Rayo study this selection problem before analyzing firms' pricing decisions (accepted manuscript, §2.1).
The paper uses an introspective equilibrium: consumers begin with an impulse about firm 1's sales and repeatedly revise consumption in response to the previous level. The resulting limit gives a selection rule tied to an observable starting condition rather than to an arbitrary choice among fixed points. The mission formalizes Proposition 1 of the accepted manuscript, dated September 16, 2022. Its source is the repository manuscript; the numbering and printed pages here refer to that artifact, not the journal typesetting (Akerlof, Holden and Rayo, Proposition 1, p. 10).
There is a unit mass of consumers, each with unit demand. Write for firm 1's relative price, and let be its current total sales. The aggregate demand is the quantity that would be demanded at price if consumers believed sales were . With one firm, the paper sets the second firm's price and quantity to zero, so the same two-argument demand map applies. With two firms, is the difference of their prices. An equilibrium quantity is a feasible fixed point,
The inverse demand curve gives a price at which a given quantity is self-consistent: for . The market assumptions say demand is continuous in price and feasible quantity, decreases with price, and increases with believed quantity. The formal market records weak monotonicity together with strict price comparisons at an inverse-demand point on the nonsaturated part of the range. These comparisons give the signs used in the paper's footnote 12 (§2, p. 5; footnote 12, p. 10).
An In/Out curve has two quantity thresholds . The curve is strictly decreasing and convex on , strictly increasing on , and strictly decreasing and concave on ; convexity and concavity here are weak. Define and . The endpoint conditions are and . At a price between the thresholds, the intersections of with the three branches are , , and . At either threshold price, two adjacent branch labels can name the same quantity (footnote 7, p. 6; §2.1, p. 8).
The consumers' impulse lies in . Level- consumption is the actual iteration , or with at level zero. An introspective equilibrium is the limit of this sequence as (Definition 1, p. 9).
For , the three branch quantities are distinct and exhaust the feasible equilibrium quantities. At or , two distinct quantities remain. The milestone from §2.1 also records uniqueness within each branch. Footnote 12 records where lies above or below between these intersections (§2.1, p. 8; footnote 12, p. 10).
The goal is the full two-part Proposition 1. When , the branch equilibria exist and
When or , exactly one feasible quantity solves , and converges to it for every . The proof's convergence and uniqueness passages are separate milestones, so the goal retains both claims without taking either as an extra assumption (Proposition 1 and proof, p. 10).
Proposition 1 ties a market's adoption outcome to the initial impulse. In the multiple-equilibrium price range, the middle equilibrium separates impulses that select the low and high quantities; outside that range, the selected quantity is independent of the impulse. This makes the refinement usable when the subsequent economic analysis asks how a price or a change in expectations can move the market between dominant firms (§2.1–§3).
The paper proves the result in ordinary mathematics. The remaining work here is a machine-checked proof of its precise selection statement and of the source passages that support it. The definition layer also supplies a reusable interface for continuous aggregate demand and inverse demand on a bounded quantity interval. There is no claim that this paper's later pricing-game propositions have already been formalized.
The inverse-demand picture shows three crossings, but a picture alone does not establish that every branch crossing exists or that no additional feasible fixed point is present. At a threshold, two branch labels meet, so a claim that always demands three distinct quantities would be false. Outside the threshold interval, the paper's reference to a unique intersection of fails at prices beyond or : the equilibrium can instead be a saturated fixed point at or . The formal statements must cover those prices with (Proposition 1 and proof, p. 10).
The convergence claim concerns a specific recursive sequence from every allowed impulse. Fixed-point existence by itself does not identify that limit or its dependence on the impulse. The market assumptions also require care at the saturation endpoints: strict decrease in price on the whole real line would conflict with nonnegative demand at , while merely weak decrease permits extra fixed points that would defeat the selection claim.
Lean represents prices and quantities by real numbers and restricts feasible quantities and impulses to . A Market stores , , continuity of on real prices and feasible quantities, range bounds, weak monotonicity in quantity and price, the inverse-demand identity, and the strict nonsaturation signs from footnote 12. The paper says demand is strictly increasing in quantity below ; the formal interface uses weak increase because its own saturated consumer model can have a constant zero-demand segment. The strict price signs make explicit the stronger reading of “decreasing” needed at inverse-demand points. Both choices are disclosed in the setting item. The polynomial and clamped-demand example in the local verification file witnesses that the assumptions are consistent.
IsInOut retains every monotonicity, convexity, concavity, threshold-order, and endpoint condition of footnote 7, even when a clause is unused in a proof. The branch quantities are predicates that include their intervals and the equation ; the goal asserts their existence before quantifying over them. IsIntrospectiveEq uses Function.iterate and Tendsto for the prescribed , so it cannot be satisfied by selecting an unrelated fixed point or sequence. Outside the threshold interval, uniqueness is over feasible fixed points of , including and . The assumptions apply to the aggregate map for either one or two firms; consumer types, their distribution, the micro-foundations, the firms' pricing game, profits, the WIN constraint, Corollary 1, and later sections are outside this mission.
A complete development needs continuity and intermediate-value results, monotonicity and convexity of real functions on intervals, and convergence of bounded sequences of real numbers. The market and level- definitions can be reused by later work on equilibrium selection. Contributions may prove the listed milestones, supply independent proofs of Proposition 1, or build the interval-dynamics lemmas they require, while retaining the statement's full price and impulse domains.
Entrepreneurs sometimes sell claims on a product before it exists. A token can represent a claim on a future unit, and its eventual market price can depend on how much the entrepreneur produces. That link creates a production incentive absent from a simple sale of equity. Malinova and Park study whether the token allocation can fund a venture while preserving the output choice that maximizes operating profit Malinova and Park, 2023. Their Proposition 3 gives a contract that does so under exogenous demand. This mission formalizes that proposition, including its investor break-even calculation and the uniqueness of the pre-sale size.
The paper first examines two simpler arrangements. Giving investors a fixed fraction of revenue leaves the entrepreneur paying the full marginal cost while receiving only part of the marginal revenue, which induces underproduction. Selling a fixed number of output units without a later revenue share induces overproduction: an extra unit reduces the price of units already promised to investors, a cost the entrepreneur does not bear. These comparisons are Lemmas 1 and 2 of the paper Malinova and Park, pp. 18–20. Proposition 3 combines an output pre-sale with a share of tokens issued after production.
At time zero, an entrepreneur must pay a set-up cost and obtains financing from investors. At time one, the demand intercept is observed. It is uniform on , and producing units gives the inverse price . Each unit costs , where . With no financing distortion, monopoly output and operating profit are
For a realized payoff , . The project's net present value is . This mission assumes , the positive-NPV case of Proposition 3. Equation (3) evaluates it as Malinova and Park, p. 14.
Under the proposed token contract, investors buy initial tokens at time zero, providing . If production exceeds , the entrepreneur issues more tokens and grants the initial holders the fraction of those new tokens. If production is at most , token-holders receive the full output and a refund of the unused production funds, . Let and be the resulting realized payments to the entrepreneur and investors. Their definitions follow the two output branches of the contract Malinova and Park, pp. 21–24, 39–40.
For every demand realization and every feasible output, monopoly output maximizes the entrepreneur's realized payment under this contract:
The claim includes the low-demand branch , where several outputs can yield zero to the entrepreneur. No uniqueness of the production choice is claimed.
Investors must receive in expectation. For , this requirement is equivalent to the paper's equation (16):
Proposition 3 and its Appendix A proof assert that the equation has exactly one positive solution , that the solution lies below , and that the entrepreneur then receives Malinova and Park, pp. 24, 39–41. Milestones cover the revenue share, the high- and low-demand cases, the investor integrals, the entrepreneur's expected payoff, and the existence and uniqueness of the break-even size.
The result shows that token financing can preserve monopoly output in this model even though the two simpler token arrangements distort it. It identifies both the later-token share and the unique number of units to pre-sell, with investor break-even and the entrepreneur's full positive NPV in one contract. That contract provides the baseline for the paper's comparative statics and its later moral-hazard comparison of equity, tokens, and debt Malinova and Park, Propositions 4 and 8.
The result is proved in the cited paper. The remaining work here is a machine-checked development of its piecewise payoffs, interval integrals, and real-analysis claims. This proposal contains open Lean statements and definitions; it does not claim that their proofs have been completed. The expectation, monopoly payoff, and contract representations can also support subsequent formalizations of the paper's cost and demand comparisons.
The simple first-order calculation behind the revenue share covers the branch , but it does not establish the entrepreneur's incentives when output is at most the pre-sale. In that branch her contractual payment is zero, and the refund rule changes the investor payment. The output claim must compare every across both branches, including the threshold .
The financing claim has a separate difficulty. Investors receive three different payments over the demand ranges , , and . Their expectation must equal the explicit cubic equation, while the entrepreneur's expectation must equal its left-hand side. A root argument stated only for the cubic would omit the economic break-even assertion. The paper also uses the interior bound when evaluating the entrepreneur's expectation Malinova and Park, Appendix A, pp. 39–41.
Lean uses real parameters and a real interval integral for uniform demand. The expect definition integrates the realized payoff over and divides by ; endpoints have zero mass. The definitions qm and pim use a nonnegative maximum to represent no production below cost. The entrepreneur and investor payments use the contract's two branches. NPV is defined from the integral, while the formula in equation (3) is a theorem. Equation (16) is a predicate on , while the corresponding expected-profit identity is another theorem. No closed form replaces an expected realized payment by definition.
The hypotheses , , , and express the paper's positive-cost, productive, positive-NPV setting. A milestone about an integral over the upper demand region assumes ; a milestone about the cubic expected profit uses the same range. Proposition 3 states the break-even equivalence on the interior and establishes that its unique positive solution lies there. Output optimality is among under the specified contract. The paper does not define a space of all possible financing contracts, so the Lean statement does not claim an optimization theorem over such a space.
The secondary token market, the physical redemption mechanism, bankruptcy costs, consumer welfare, and the institutional discussions of Sections I and V are outside this mission. Needed reusable work includes real interval integration of piecewise polynomial payments, algebraic comparisons of quadratic payoffs, and strict monotonicity of the break-even cubic. Contributions that prove the listed statements while retaining the realized-payoff definitions are welcome.
Agricultural subsidies can raise total crop supply while changing which farmers produce it. A payment tied to planted input gives a larger reward per unit of harvested output to a farmer who needs more input for that output. A payment tied to harvested output gives the same reward per unit of output to every farmer. These differences matter when a government cares about the distribution of production and income across farms as well as total supply. Fan et al. (2023) study these effects in a finite market where farmers choose quantities and compete through a common market price.
This mission isolates the paper's distribution result for a combined subsidy, which pays on both planted input and harvested output. It asks how a difference in the dispersion of farmers' input-to-output ratios between two otherwise identical markets affects their equilibrium output and profit. The result is Proposition 4 of the SSRN version. The paper proves it in Online Appendix A, p. 4. The result is mathematically stated and proved in the paper; the machine-checked formalization of its statement and proof is the work here.
There are farmers, indexed in the paper by . Farmer must plant units of input to harvest units of output. Thus is an input-to-output ratio; a smaller ratio means more output per unit of input. The ratios are listed in nondecreasing order. Planting costs per unit of input, harvesting costs per unit of output, and total harvested output is . The market-clearing price is , where .
Under a combined subsidy , farmer receives per unit of output. The first part is payment for planted input and the second for harvested output. A farmer choosing while the other farmers' outputs stay fixed has profit
An equilibrium is a nonnegative output vector at which no farmer gains by changing its own nonnegative output. Costs and subsidies are real-valued: the paper permits a subsidy larger than its associated cost and also permits a negative subsidy, or tax. The formulas in this mission concern equilibria at which every farmer produces a positive quantity.
To compare dispersion, let be the sum of the largest entries of a vector . A vector majorizes , written , when for every and their total sums agree. The weak sub-majorization relation keeps the top-sum inequalities and drops equal totals. With this direction, says that is more dispersed. These are the orders of Definition 1 in Fan et al..
The first milestone formalizes Proposition 3's active branch. Write and . At an equilibrium with every farmer active, it states
The remaining milestones formalize the increment identities written in the proof of Corollary 1 and the two order properties invoked in the proof of Proposition 2: majorization under an affine map, and weak sub-majorization under an increasing convex map. These are the results used to interpret the change in each farmer's output and profit when a subsidy changes.
Consider markets and with the same , but with ratio vectors . Give them the same subsidy and let . For a vector of equilibrium outputs, is the difference between outputs at and ; is defined using . Profit increments use the corresponding profits at those equilibria. Proposition 4 asserts
The equality means majorization in both directions. These comparisons form one goal theorem so every part of Proposition 4 remains present. Proposition 4, p. 13 is the source for the target.
The first output comparison says that greater dispersion in input-to-output ratios leads to greater dispersion in equilibrium production under the same combined subsidy, while the total output stays equal. The increment comparisons identify which changes preserve or distinguish that dispersion when planting and harvesting payments increase. The profit statements give the corresponding order for farmer earnings. They make the distributional effect of a subsidy explicit rather than reducing it to a claim about aggregate crop supply.
A formal development supplies reusable definitions for finite majorization, this Cournot market, and best-response equilibrium. It also separates the paper's claimed order relations from the algebraic equilibrium formula. Proofs of the paper's known results remain to be checked in Lean. The mission makes no claim that Proposition 4 is an open research problem.
Directly comparing farmer in the two markets cannot establish majorization: the order compares sums of the largest coordinates, which need not belong to the same farmers in each market. The sign of can change because planting payments are unrestricted, so the ordering of farmers by output can reverse. Profit is quadratic in output, and the profit comparison is weak sub-majorization rather than equality of totals. Subsidy increments introduce additional equilibria; an increase in the planting payment can also alter which farmers are active. These features must be accounted for in a statement that retains every clause of Proposition 4.
Lean represents the paper's farmers by Fin N, so paper farmer has Lean index . The shared parameter record contains ; each market supplies its own sorted vector . A standing predicate records , , the ordering of , and . The positive-ratio condition makes explicit that each ratio is formed from positive physical quantities. The two markets have the same parameter record, and no sign restriction is imposed on costs or subsidies.
The combined payment is a per-unit-output vector . Equilibrium is a best-response condition over nonnegative output, not a definition by Proposition 3's formula. The top-sum order uses all subsets of farmers, with equal total sums required for majorization. Averages range over all farmers because the theorems work in the all-active regime. This rules out treating a formula-defined output vector or a weakened order as the market result.
The goal explicitly assumes positive output at the baseline and at both shifted subsidies. Positivity at the planting-shifted subsidy is needed for the paper's fixed-active-set increment formula but is unstated in Proposition 4. Positivity at the harvesting-shifted subsidy is implied by this market model; it is kept explicit without assuming an equilibrium-uniqueness theorem. The supporting increment milestone also includes an active equilibrium at the midpoint harvesting subsidy. The majorization lemmas can be reused for other finite-vector models, and the equilibrium characterization can support later analyses of this paper's subsidy programs.
In reward based crowdfunding, customers must decide whether to back a product before its quality is known to them. The entrepreneur knows that quality and chooses a funding price. A high quality entrepreneur may therefore use price to convey information, but the same price is available to a low quality entrepreneur. The choice also changes the chance that the campaign meets its financing target. Bolandifar, Chen, Kouvelis, and Zhou study how these effects interact when the entrepreneur chooses a second, regular selling price after the campaign succeeds. The one price mechanism in this mission concerns the case in which only the funding price is posted in advance.
The question matters to the design and interpretation of crowdfunding campaigns. A lower funding price can be a credible quality signal even though it forgoes immediate revenue. Whether that signal is sustainable depends on the later selling opportunity, the financing target, and the different incentives of the two quality types. The paper gives a precise threshold for the financing target below which one separating outcome survives a refinement of the equilibrium concept.
The entrepreneur's product has privately known quality , either low or high , with . The financing target is . The entrepreneur posts a funding price . Funding period customers all share a taste uniformly distributed on and evaluate the product using believed quality . They back it when . The funding market has size one, so a successful campaign raises at least and occurs with probability for . The formal definition extends this probability by zero for larger prices.
After success, true quality is revealed and the entrepreneur sets a regular selling price . A fraction of regular period customers have the same taste as the funding customers. Their taste distribution is therefore updated after success. The other regular customers have a fresh, independent uniform taste. The regular market also has size one. Production cost, salvage value, and discounting contribute no additional terms. Conditional regular period profit is , the two branch function in equation (2) of the manuscript. Its optimal value is the supremum over feasible . The total expected profit is the success probability times .
A separating equilibrium assigns different feasible funding prices and to the two entrepreneur types. Customers believe quality is high at and low at every other price, including off path prices. Under those beliefs, neither type benefits from a feasible deviation. The intuitive criterion removes an equilibrium if an off path price would strictly improve the high type's profit while strictly reducing the low type's profit, were customers to interpret that deviation as a high quality signal. This is the paper's stated test, with the strict low type comparison used in its appendix.
Define the price threshold
The goal is Proposition 1 of the manuscript. If , there is a separating equilibrium surviving the intuitive criterion, and every surviving separating equilibrium has exactly the prices
The formal goal also says that no separating equilibrium exists when . Its scope on this side of the threshold follows the manuscript's proof and the nondegenerate funding market; the printed “otherwise” sentence does not hold literally when .
Lemma 1 identifies the optimal regular price and its attained profit in each of three funding price ranges, split at and . Lemma 2 identifies the funding profit's single peak and the maximizing price . The three parts of Lemma 3 characterize the low type's mimicking indifference prices, the high type's upper indifference price, and the ordering of these thresholds. These are the milestones leading to Proposition 1.
The proposition gives both types' prices and shows why the high type's credible signal is a lower funding price than the low type's. It also identifies a financing target above which this separation disappears within the paper's nondegenerate range. The result relates a platform design parameter, the target, to equilibrium information revealed by price.
The result is proved in the cited manuscript, with proofs in Appendix A. The remaining work in this mission is a machine checked proof of the model's price optimization and equilibrium claims. The definition of the two period payoff, the treatment of the later optimal price, and the explicit deviation predicates may be reusable for other crowdfunding signaling mechanisms. The draft statements are open proof targets; the present mission does not claim those proofs are already formalized.
The later optimal price changes form as the funding price crosses two thresholds. That makes total expected profit a piecewise function, even before the two types' incentives are compared. Maximizing either type's full information payoff alone does not determine a separating equilibrium: the low type might imitate the high type, while the high type might deviate to a price customers would interpret as low quality. The intuitive criterion imposes a further comparison at prices outside the equilibrium path. The claim requires all of these comparisons with the same underlying payoff definition.
Lean uses one tuple of real parameters and the standing restrictions , , and . The prior probability of high quality does not occur in the separating price statements. The regular profit is the printed equation (2), with a positive regular price at most true quality. Campaign success probability is clipped at zero for funding prices above believed quality. Funding prices range over all reals at least ; the maximum profits are defined as suprema over those feasible prices. Milestones assert attainment, so those suprema cannot be replaced by convenient formula values.
The model uses the paper's market size, cost, salvage, and discount normalizations. Lemma 1 excludes : at that endpoint the printed third case can specify an infeasible regular price. Lemma 2 assumes and quantifies only over the four true and believed quality combinations. Lemma 3 is stated for to avoid its circular printed preamble, and one threshold comparison is expressed as a strict profit inequality because the lower crossing can lie below . Proposition 1 does not assert pooling existence, which would require the omitted prior; its no separation clause is restricted to .
Contributions toward the piecewise optimization lemmas, the threshold characterization, and the equilibrium theorem are welcome. The separating equilibrium is defined by incentive comparisons over all feasible deviations, and its refinement is defined by the off path deviation test. The optimal profits are supremum values of the model payoffs. These choices keep the goal from collapsing into a restatement of a closed form or of the paper's derived necessary and sufficient conditions.
Certify the classical quadratic separation between sensitivity and block sensitivity: .
For a total Boolean function , write for the input obtained by flipping the coordinates in . Its sensitivity is . Its block sensitivity is the largest number of pairwise disjoint nonempty sets that satisfy at a common input .
The goal is to prove that for every and every integer , there is a total Boolean function with
The construction milestone is Rubinstein’s quadratic separation: for each integer , there is a function on bits with
These exact bounds imply the goal because and sensitivity grows without bound. This is a known theorem; the task is to formalize it using the campaign’s shared definitions.
The main combinatorial work is controlling sensitivity at every input and proving the matching block-sensitivity bounds. Lean represents functions as (Fin n → Bool) → Bool; both measures are maxima over all inputs. The goal reuses SensitivityCampaign.AchievesExponent, so it has exactly the same meaning as the campaign’s stronger targets. No composition theorem is required for this family argument.
References: David Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica 15 (1995), 297–299, DOI. The statement and construction are also recalled in Theorem 1 of Madars Virza, Sensitivity versus block sensitivity of Boolean functions (2010), arXiv:1008.0521.
A firm can learn a customer's preference before choosing a customized product, or it can let the customer choose a requested design. The two approaches assign the design decision to different parties. That matters when design changes both the value of a sale and a cost the seller must incur before the price is negotiated. Guo's study of customer voice in customization compares these approaches in a model where a buyer has private information about how much it values quality. The payoff comparison asks who gains from holding the design right and whether the answer survives a modest fixed cost of using that approach.
This mission concerns Proposition 8 of the SSRN author copy, printed page 23. The result is a comparative statement about two already specified separating equilibrium outcomes. Earlier results in the same paper characterize when the outcomes arise: Proposition 1 treats communication before seller design, and Proposition 3 treats a buyer's design request. Proposition 8 compares the parties' payoffs at the qualities associated with those outcomes. Its four clauses distinguish gross payoff rankings from net rankings after an incremental fixed cost. The paper states Proposition 8 without a separate proof; its surrounding discussion explains its interpretation. All page and result numbers here follow the SSRN version of 2023-11-29.
There is one seller and a unit mass of buyers. Each buyer has one-unit demand and a privately known quality preference , with type and . The high type has population share , while the low type has share . A product's quality is a nonnegative real number . Producing a unit of quality costs , and offering that product incurs a selling cost , where . The selling cost is incurred before the price is settled. The seller makes a take-it-or-leave-it offer with probability ; the buyer does so with probability . These primitives and the timing are specified in Section 2.
In A-Learning, the buyer sends a costless message about its preference and the seller chooses the design. In O-Learning, the buyer requests a quality and the seller decides whether to accept it. The paper compares separating outcomes, so each type is associated with its true preference when the equilibrium payoff is evaluated. The pricing stage is represented by the paper's payoff formulas. If the seller regards a buyer's preference as , its payoff from quality is
The buyer's payoffs and retain the nonnegative parts in equations (5) and (9): each is , with its arguments ordered as in the relevant equation. For type , the paper's A-Learning and O-Learning equilibrium qualities are
Write and . The seller's expected gross payoffs are and . The buyer payoffs and evaluate and at type 's quality and truthful preference. These are the payoffs defined around equations (8) and (13) of the paper.
The first comparison says that the seller earns more from its own design, while each buyer type earns more from its requested design:
The two fixed-cost clauses hold the preference levels, population share, bargaining weight, and production-cost coefficient fixed while the positive selling-cost coefficient varies. For every seller-side incremental fixed cost , there is a positive threshold such that
For every buyer-side incremental fixed cost and each type , there is a positive threshold such that
The goal is the conjunction of these four clauses, exactly the payoff content of Proposition 8. The milestone list also includes the paper's strict quality comparison and its observation that the quality difference tends to zero as tends to zero. The printed statement and discussion are on pages 22–23.
The gross comparisons separate the seller's and buyers' preferences over who chooses quality. The fixed-cost clauses show why the party favored by the gross comparison need not favor that approach once its own extra effort or implementation expense is counted. The thresholds make this claim uniform over all sufficiently small positive selling costs, rather than treating the single case . This distinction is relevant when comparing preference solicitation, which requires seller effort, with buyer-led design, which requires customer effort.
Formalizing the result gives a reusable two-type model of quadratic production and selling costs, the two reduced-form buyer payoffs, and a finite-population expected-payoff calculation. It also creates separate targets for each clause, so the gross-payoff and small-cost claims can be checked independently. The result is proved in the mathematical paper only to the extent of its stated Proposition 8 and accompanying discussion; the local Lean statements in this proposal compile with proof placeholders and do not yet constitute machine-checked proofs.
The two approaches select different quality formulas, and O-Learning uses a minimum of two expressions. As changes, that minimum can switch branches. The buyer payoff formulas also contain maxima with zero, so replacing them unconditionally with simplified quadratic expressions would change the model. A valid payoff comparison must account for the relevant branch and preserve the strict inequalities for both buyer types. For the fixed-cost clauses, pointwise closeness at does not itself state a uniform claim for every sufficiently small positive ; the threshold must be positive and chosen before .
The Lean model uses a two-constructor buyer type, real parameters , and a Standing predicate carrying every displayed positivity and interval assumption. Qualities are real-valued, with the paper's intended domain ; the closed-form equilibrium qualities in this mission are nonnegative under those assumptions. Expected seller payoffs use a finite sum over exactly the high and low types, weighted by and . Buyer payoffs use the original maxima with zero. The pricing stage is in reduced form through equations (4), (5), and (9). The model and payoff notation are local to CustomerVoice.Payoffs, because the other missions' definitions are unpublished drafts.
The statements compare the printed closed-form qualities without adding the separate inequalities that guarantee both separating equilibria exist. Thus their domain is all parameter choices satisfying Section 2's standing assumptions; this is the stronger reading identified in the paper's planning notes for Proposition 8. In the small- statements, withS changes only the selling-cost coefficient, and the quantified values of satisfy . The proof targets cannot be reduced by deleting the nonnegative parts of the buyer payoffs, allowing a zero threshold, or checking only the limit at . Contributions to the elementary quality comparisons, branch-sensitive payoff inequalities, and positive-side limits all support the goal. The finite weighted-payoff and limit infrastructure can be reused in other small-cost comparisons.
A delivery vendor controls both how a courier serves orders and what customers pay. Serving one order per trip avoids waiting for a second order, but serving two together can save travel time when demand is high. If the vendor can change its price, it also changes the rate at which customers join the system. The preferred dispatch rule therefore depends on an economic decision as well as a queueing calculation. Chen and Hu study this interaction for a single courier in a disk-shaped market and compare the vendor's revenue under dedicated and two-order batch delivery in their paper. The present mission concerns their crowded-market results, Propositions 3 and 4, in the authors' SSRN version of 2022-09-21.
The paper first analyzes fixed demand rates, then lets the vendor choose a demand rate by setting a price. The latter decision changes the comparison: customers with a high cost of waiting favor a less crowded, dedicated service, while sufficiently patient customers can make batching more profitable. The service radius has an analogous effect. The paper's threshold is expressed through the product of wait cost and radius, so these two comparative statics describe the same switch Chen and Hu, §5 and Online Appendix A.
A vendor is located at the center of a disk of radius . Customers arrive at locations uniformly distributed over that disk. The vendor has one courier and chooses between dedicated delivery, one order per round trip, and batch delivery, two orders per trip. The effective demand rate is . A customer incurs wait cost at rate and has a valuation in . The vendor's price induces its chosen demand rate. Chen and Hu give the dedicated service rate and batch service rate in equations (4) and (9).
The paper uses the following expected waiting times, with variation coefficients and :
Dedicated delivery is evaluated for ; batch delivery for . The first batch term is the wait to form a pair. The final term represents travel while the other order is delivered. The batch in-line wait is the paper's Kingman-based approximation for an queue, whereas the dedicated in-line wait uses its expression equations (5), (11), and (12).
In a finite market, the valuation distribution affects the price needed to induce demand. As the potential arrival rate grows, the paper's crowded-market revenue becomes
For each dispatch rule, insert its wait into this function and optimize over its stable demand range. The resulting optimal revenues are denoted and . The mission uses suprema to express these values. The paper motivates this limiting objective in (14)–(15) and Lemma 1 (16)–(17).
The goal is a single such that, for every ,
Thus the wait-cost threshold at a fixed radius is , and the radius threshold at a fixed wait cost is . At the threshold the two optimized revenues agree. For the paper's numerical , it reports Online Appendix (A.7)–(A.8).
As either or increases through its threshold, the optimal demand rate has a downward jump and the corresponding optimal price has an upward jump. The formal statements require both one-sided limits to exist and the inequalities between them to be strict. They cover every selection of optimal demands, including any ambiguity at the tie. These are parts (ii) of Propositions 3 and 4.
The milestones cover strict concavity of the revenue objectives, their explicit optimizers and values where attained, the single crossing of the revenue gap, the demand comparison at the tie, and the two propositions individually. The goal combines those propositions through the common product .
The threshold tells the vendor which dispatch rule maximizes limiting revenue after the price has been adjusted optimally. It also locates a discontinuous operational change: a small movement in customer impatience or service area across the threshold changes the chosen mode, demand rate, and price. Comparing the waiting-time formulas at one fixed demand would not provide this revenue decision, because each mode can choose a different demand rate Chen and Hu, §5.
Chen and Hu prove the paper result analytically, while the threshold and its supporting claims here are proposed Lean statements awaiting proofs. A completed formalization would connect exact claims about the rational waiting-time expressions, optimization over open stability ranges, the unique revenue crossing, and one-sided limits. It would also record which conclusions use the paper's approximated batch wait and numerically estimated coefficient. These are reusable patterns for queue-based pricing models, even though this mission formalizes this paper's particular geometry and service rules.
The two dispatch modes have different singular boundaries and different optimizers. The batch wait diverges as demand tends to zero, yet batch revenue can have a finite boundary supremum that is not attained for some parameter values. The dedicated objective has a different service-rate pole. Consequently, replacing either optimization with an unrestricted real supremum, or asserting that every batch supremum has a maximizer, changes the claim. The revenue comparison also needs one crossing for the full positive range of , including values beyond the range where the appendix's interior batch optimizer applies. Finally, a strict jump in demand does not by itself supply the existence of both one-sided limits; the formal statements ask for those limits explicitly Online Appendix A.
Lean uses real-valued and the paper's closed-form waits, service rates, and limiting revenue. The name lam denotes . The batch coefficient is a real parameter satisfying , an explicit interval around the paper's numerical rather than a claimed exact evaluation of its integral. Every threshold statement assumes ; the auxiliary optimum statements use the page's range when they assert an interior maximizer. The domains are and , with zero excluded for batch because its wait is singular. The optimal revenues are defined as suprema of the actual objective images. The threshold is existential and is never defined from the desired answer.
The formal development does not construct the Poisson arrival process, random trip lengths, queue, or approximation behind the waits. It takes the paper's equations (5) and (12) as definitions. The finite-density function is recorded for context, but Lemma 1's convergence from finite to limiting optimized revenue is outside this mission's milestone list; the goal is explicitly the crowded-market limit. The printed (A.6)–(A.8) contain a coefficient error in the batch value, so the formal batch value uses the corrected expression and defines the revenue gap directly from the suprema. The printed batch optimization interval includes zero, which the stated waiting-time formula does not support. Definitions for objectives, stable domains, optimal demand, and one-sided jumps are reusable within related pricing formalizations. Contributions that establish the stated optimizer, crossing, or limit claims without changing their domains are within scope Chen and Hu, equations (12), (15), (A.3)–(A.8).
Augmented Lagrangian methods are a standard tool for constrained optimization, and first-order primal-dual variants of them are used when the objective is large, nonsmooth or nonconvex and second-order information is too expensive. Zhu, Zhao and Zhang (arXiv:2007.12219v1, published in Mathematics of Operations Research, 2024) analyse such a method, NAPP-AL (Nonconvex Auxiliary Problem Principle with Augmented Lagrangian), for problems with a nonlinear equality constraint, a closed convex set constraint, and a nonsmooth nonconvex term. They prove a sublinear rate in general and a linear rate under a local error bound they call the value proximity error bound (VP-EB).
An error bound is only useful if it holds in recognisable situations. Section 6 of the paper answers the question "can VP-EB ever be satisfied in a natural setting?" with two sufficient conditions. This mission formalizes the first: the Kurdyka–Łojasiewicz (KL) property with exponent , the condition behind most linear-rate results for nonconvex first-order methods since Attouch and Bolte (Math. Program. 2009) and Bolte, Sabach and Teboulle (Math. Program. 2014).
The problem (P) is
with , , , a linear map , and smooth, lower semicontinuous and possibly nonsmooth, and closed and convex. Primal-dual points are , with . The augmented Lagrangian with penalty is
The stationarity set (p. 6) collects the vectors with , , , where , is the limiting subdifferential and the normal cone. is the least norm in , and when is empty.
NAPP-AL updates by minimizing over a linearization of the smooth parts plus plus a Bregman term built from a strongly convex kernel ; it updates by a linearized quadratic step and by the multiplier step . The step lies in with given by the paper's formula (8). Assumptions 1 and 2 (Lipschitz gradients, , coercivity on the feasible set, a lower bound on ) are the paper's standing hypotheses.
For and , let . has the KL property at with exponent if, for some ,
VP-EB holds at if, for some , every iterate with and satisfies .
For a run of NAPP-AL under Assumptions 1–2 and (8), and an accumulation point of :
The constants of VP-EB are existential, as in Definition 5.1.
There is such that, whenever ,
Proposition 6.1 turns the paper's Theorem 5.1 (linear convergence under VP-EB) into a statement about a property that is known to hold for wide classes of functions: semialgebraic and subanalytic functions satisfy KL inequalities, and exponent is established for many structured problems (for instance by Li and Pong, Found. Comput. Math. 2018). With it, a user who verifies the KL exponent of obtains a linear rate for NAPP-AL.
The result is proved in the paper; none of it is machine-checked. A formal proof requires the residual bound of Theorem 4.1(iv) for NAPP-AL, which the companion mission on the sublinear rate states as a milestone, and the conversion of a KL inequality on the strict level band into an error bound on the half band. A formal version also pins down a convention the paper leaves implicit: where the stationarity set is empty, the KL inequality is satisfied trivially because the distance is .
The deduction itself is short once Theorem 4.1(iv) is available; the difficulty is that Theorem 4.1(iv) is not. It asserts a uniform constant with , which needs the boundedness of the iterates (from the sufficient decrease of the potential and coercivity on the feasible set), a lower bound on the steps through (8), and the optimality conditions of the nonsmooth, nonconvex subproblem (5), including the sum rule under local Lipschitz continuity of . Applying the KL inequality directly, without a residual bound tied to the algorithm, gives nothing: the KL inequality controls by a distance to , and only the algorithm links that distance to the step.
The Lean development works in EuclideanSpace ℝ (Fin k). Primal-dual points live in with the Euclidean norm of the stacked vector written out explicitly (tnorm), not Mathlib's sup norm on the product. is a continuous linear map with its operator (spectral) norm; is the infimum of over unit vectors. is an infimum in , equal to on the empty set. The algorithm is a relation on given sequences: global minimality in (5) and (6) and the update (7); existence of minimizers is not asserted.
Readings disclosed relative to the page: are real valued with gradients Lipschitz on the whole space; is Lipschitz on an -neighbourhood of each point of ; ; the normal cone is empty off ; VP-EB is the inequality of Definition 5.1 without its presupposition that the sequence converges; the KL property for uses the paper's set of p. 6. Proposition 6.1 says only "generated by NAPP-AL"; the hypotheses of Theorem 4.1 (Assumptions 1–2 and the step rule (8)) are included because the proof uses Theorem 4.1(iv).
Trivializing encodings are ruled out: the distance is not Metric.infDist (which is on the empty set), the product norm is not the sup norm, is not a matrix with an entrywise norm, local Lipschitz continuity of is not Mathlib's relative notion, and the normal cone is not nonempty off .
A complete development needs Theorem 4.1(iv) for NAPP-AL and thus most of §§3–4 of the paper (Proposition 3.1, Lemmas 4.1–4.3). That infrastructure is shared with the other missions of this series and is reusable; contributions of any of those lemmas are welcome. The source is the preprint arXiv:2007.12219v1, not the published version; all numbering is the preprint's.
Sellers often ask customers what they want before designing a product or service. The answer can affect both the quality delivered and the price paid. Because a customer can send a costless, unverifiable message, the seller cannot assume that a stated preference is true. Guo's customization model asks when the customer's own incentives make truthful communication sustainable. This matters for products with substantial presale effort, such as prototypes, proposals, and sales assistance: the seller incurs that effort before the final transaction price is set. The paper distinguishes this selling cost from the cost of producing the eventual product. This mission concerns the paper's A-Learning game, in which the seller learns through a customer's message before choosing quality.
Each buyer wants one unit of a product with quality . A buyer with preference values it at and can decline to trade. The preference is private and has two possible values, . The high type has prior share . Producing quality costs and selling it costs , with . The selling cost is incurred at the design stage. In the final price-setting stage, the seller makes a take-it-or-leave-it offer with probability ; the buyer makes the offer with probability . These are the assumptions of §2, pp. 5–9.
Under A-Learning, the buyer sends one of two costless messages before the seller chooses quality. A separating message rule sends different messages for the high and low types. On receiving message , the seller believes the type is . If its belief is , the seller's expected payoff from offering quality is
At a given quality, a buyer whose actual type is receives
The maxima preserve the buyer's option not to purchase. In the paper's perfect Bayesian equilibrium, the seller's beliefs agree with the types that send the observed messages, the seller chooses a nonnegative quality maximizing for each message, and each type chooses a message maximizing its own payoff. With two distinct messages and a separating rule, both messages occur on the equilibrium path. These payoff and equilibrium conditions are stated in §3.2, pp. 11–12, equations (4)–(7).
The seller's printed optimal design for belief is
With , the two incentive compatibility conditions are and . The supporting targets identify the seller's optimal design, characterize informative equilibrium by these two conditions, and express each condition as a threshold on type heterogeneity. They follow §3.2, pp. 12–13.
The goal is Proposition 1: an informative A-Learning equilibrium exists exactly when
The weak inequality includes the boundary at which a buyer is indifferent between messages. The Appendix's proof uses strict inequalities in a corresponding line; the statement on p. 13 and Proposition 1 use weak ones. The milestone list retains the source's optimal-design sentence, equations (6)–(7), and the two threshold sentences in their order in the SSRN author copy.
The theorem gives a precise answer to whether costless buyer communication can transmit preference information before a seller customizes a product. The condition separates the two possible failures of truthful reporting: a high type may prefer the design induced by the low message, and a low type may prefer the design induced by the high message. It also shows why the relevant threshold depends on bargaining power and both cost coefficients, while the prior share does not enter this particular equilibrium-existence condition. The result is a theorem of the paper; the mission seeks its machine-checked formulation and proof.
The formal development makes the equilibrium claim more than a comparison of two algebraic payoffs. It must connect an actual separating message strategy, beliefs, a seller optimum, and buyer best responses to the two incentive conditions. The model's payoff definitions and equilibrium predicate are reusable for other statements about A-Learning in the paper, including comparisons of equilibrium quality and payoffs. The threshold lemmas can also be reused when comparing A-Learning with O-Learning.
Costless messages alone impose no truthful-reporting discipline. A seller's belief changes both the design chosen after a message and the price a buyer might face. The high and low types therefore face different deviation incentives. A comparison that ignores the seller's design decision misses the equilibrium requirement; a comparison that treats every buyer as purchasing misses the low type's option to refuse an overpriced high-quality product. The second issue is visible in the terms of equation (5). The equilibrium result has to hold at equality in the thresholds as well as above them.
The Lean model uses real parameters and a two-constructor type for buyer types. Its standing assumptions are exactly , , , , and . A separate two-constructor type represents the two possible messages. Quality is real and every seller optimization ranges over ; optimality means that the chosen design attains the maximum. Buyer deviations range over both messages. Beliefs identify the types on the equilibrium path. The type's purchase option is kept in both maximum terms of the buyer payoff.
The price-setting stage is represented by the paper's reduced-form payoffs (4) and (5), without a separate bargaining game. The prior share is retained among the standing primitives even though it cancels from Proposition 1. The closed-form design is used in and the incentive conditions, while an equilibrium requires actual seller maximization. An equilibrium is not defined as the conjunction of incentive conditions, and is the printed maximum of the two explicit fractions. Separation rules out a one-message or pooling interpretation. The supporting statements require real arithmetic, optimization on a nonnegative domain, and finite case analysis for the two types and two messages. Contributions that preserve these definitions and the paper's weak boundary are welcome. The known proofs behind the milestones are in the Appendix of the SSRN version, pp. 27–28.
Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in , compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.
This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.
Let denote the real output of a quantum algorithm under one run, and let be its probability law. The mean is , and the variance is . The result assumes a known with . Although the paper describes a circuit that prepares and measures , its accuracy statements depend on the distribution of ; the Lean interface therefore represents a run as a measurable real random variable on a probability space.
For real thresholds , the truncation returns when and zero otherwise. The variants and retain the output below and at or above , respectively. They do not clip a value to a threshold. The size is . These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.
Algorithm 2 estimates a nonnegative mean using the base interval and the half-open bands for . It sets and , then adds the base estimate to times each band estimate. A successful Algorithm 1 call means that its estimate of a -valued output differs from by at most , the accuracy bound of Theorem 3, pp. 8–9.
Algorithm 3 rescales by , draws one sample from , and centers the rescaled output at . It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy and recombines their estimates. The two calls are specified to fail with probability at most each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.
When every Algorithm 1 call satisfies its accuracy bound and , the output of Algorithm 2 obeys
The constant is chosen once for a fixed positive universal constant from Theorem 3. It is independent of and .
For , , and , Algorithm 3 returns with
This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.
Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.
The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.
A bound for one -valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.
Lean uses probability measures and measurable real outputs for the laws of and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of , so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's and formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.
The hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression occurs only on bands indexed by .
The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.
Online advertising platforms sell billions of ad impressions a day, mostly by auction, to advertisers who care about the features of the impression (the user, the page, the time) and who spend under a budget fixed in advance. To keep spending within budget, platforms and advertisers use pacing: every value is multiplied by a factor smaller than one, so that the buyer bids less aggressively and spreads its budget over the whole campaign. Balseiro, Kroer and Kumar (2023) study the equilibria that pacing produces when items carry feature vectors and buyers' values are linear in them. They prove that a pacing-based equilibrium exists in the first price auction (Theorem 1), that the same pacing is an equilibrium of every standard auction with the same expected payments (Theorem 2), and that its liquid welfare is at least half the optimum (Theorem 3).
This mission concerns §6, Structural Properties, of that paper: what the equilibrium pacing multipliers look like as a function of the buyer's type. Its goal, Proposition 3, says that buyers who share a budget and whose weight vectors point in the same direction are paced down to one common weight vector. It is the qualitative statement behind a practical observation: scaling up the targeting weights of a budget-constrained advertiser without raising its budget does not change the outcome.
An item has a context , drawn from a law with a density. There are buyers; each has a type consisting of a weight vector and a budget , drawn independently from a law with a density on
The value of type for item is , and . The item is sold by first price auction with reserve price , and every buyer must respect its budget in expectation over the context and the other buyers' types.
A pacing function shades the value of type to the paced value , equivalently replaces by the paced weight vector . Let be the distribution function of the highest of independent paced values. The value pacing–based strategy bids , where
with when and below the reserve. A buyer of type facing competitors who bid has the dual function
the supremum over bid functions ; is the Lagrange multiplier of its budget constraint.
§6 assumptions. Reserve prices are zero; the support of is convex and compact; and takes values in with
the minimizer being unique. This is uniqueness of the best response, not of the equilibrium. A type with is unpaced, and paced otherwise. Norms are Euclidean.
Let be a unit vector and such that for some .
Proposition 3 describes equilibrium pacing along each direction of weight space as a single threshold. Along a ray with budget , buyers below a critical scale do not exhaust their budget and are unpaced; every buyer above it is paced down to the critical type, which spends its budget exactly. Equilibrium paced values, hence allocations and payments, are therefore constant above the threshold. By the paper's revenue equivalence result the same description holds for the pacing equilibria of all standard auctions, which makes it a statement about budget-constrained advertisers in general, not about one auction format.
The result is proved in the paper, with all proofs in its online appendix; the appendix is not part of the source this mission cites. No part of it has been machine-checked. The mission formalizes the statement on top of a from-scratch model of contextual budget-constrained first price auctions (types, pacing, the bidding function , the buyer's dual function), which is shared with the other missions of this series.
The dual function is a supremum over bid functions in which the competitors' bids themselves depend on , so the equilibrium condition is a fixed point: appears both inside the objective and as its minimizer. Comparing two buyers on the same ray requires relating their dual problems, and a buyer with weight vector does not simply face a rescaled problem, because the budget does not scale with . Part 2 requires in addition that the largest unpaced buyer exists, which needs continuity of on the support; continuity of an argmin requires uniqueness of the minimizer and continuity of in the type and the multiplier jointly. The monotonicity statement is a comparative-statics argument for a family of minimization problems parameterized by the type.
Types are pairs (w, B) : (Fin d → ℝ) × ℝ, values are the explicit sums , and the Euclidean norm is written as , never Lean's sup norm on Fin d → ℝ. is Mathlib's Measure.support. The expectation is over the product of and copies of ; ties win, as in the paper's tie-breaking rule. Bids are measurable, nonnegative and have an integrable payment, and is defined as the supremum over such bids (p. 7), not by its closed form. is defined by an explicit case split so that the case gives .
Standing assumptions: ; ; measurable inside the strictly positive orthant; and probability measures with densities, , ; measurable; and the §6 assumptions above, with the unique best response stated as membership, minimality and uniqueness over . Disclosed additions: ; ; nonempty and bounded (so that is finite); , since is defined on and is evaluated on . The maximization set of part 2 is read inside with the budget fixed, and the existence of the maximizer is part of the conclusion, so the statement is not vacuously true when no maximizer exists. The milestones are posed on , where uniqueness is assumed.
The development needs the support of a measure, argmin continuity (a maximum theorem for a unique minimizer), and comparative statics of parametric minimization; the auction model is reusable by the other missions of the series. Contributions of supporting lemmas on (its convexity in , continuity, the closed form of p. 8) are welcome.
The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.
For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold , and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.
Let with even. A bisection is a partition with ; its cost in a graph is the number of edges between and . Given a fixed planted bisection , an optimization problem recovers it if its unique optimal solution corresponds to .
The cut vector of has exactly when lie on different sides. With for edges and otherwise, the metric relaxation is
the first family over distinct and the second over , with . Every bisection's cut vector is feasible.
The distance is the length of a shortest – path ( across components). The diameter is and the average distance is .
The Erdős–Rényi model draws each edge independently with probability . The SBM chooses a bisection uniformly at random, then draws each pair inside a side with probability and each pair across with probability , independently, where . The logarithmic-degree regime (21) is
An event holds with high probability if as .
with high probability.
Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).
The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all , including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant ) the LP does succeed when ; Theorem 8 shows that at logarithmic degree no such window exists.
Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.
The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.
Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side with . The LP variable is a symmetric, zero-diagonal array , which is a point of ; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in and the average distance in , so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into , which matters only for the finitely many with . "With high probability" is a limit of probabilities equal to ; for the SBM the limit runs along . Logarithms are natural.
Disclosed choices relative to the printed statements: Theorem 8 prints only , and is added as the SBM's standing assumption (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary is left out.
The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every , the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.
A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.
In auctions with interdependent values, the value an agent assigns to an outcome depends not only on her own private information but on the information of the others: a bidder for drilling rights values a tract according to every bidder's geological survey, and a buyer of a used asset values it according to every inspector's report. Each agent observes only her own signal, while the mechanism designer knows how values depend on the full signal profile. Maximizing welfare truthfully is then much harder than with private values: the VCG mechanism no longer applies, and without structural assumptions on the valuations no ex-post truthful mechanism gives a good approximation of the optimal welfare (the source's Examples 1.2–1.3).
Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384) identify submodularity over signals (SOS) as a condition under which constant or near-constant approximations become possible, including for combinatorial auctions, where agents value bundles of items. For single-dimensional signals that take values, they give a -approximation under SOS (Theorem 6.1) and, under the stronger condition strong-SOS, a -approximation (Theorem 6.5). This mission formalizes the second result.
Timeline. Milgrom and Weber (1982) introduced the interdependent value model for auctions; Dasgupta and Maskin (2000) studied efficient auctions under the single-crossing condition. The computer science literature then gave approximation results for simple single-parameter settings (mostly single-item auctions or matroid constraints), again largely under single crossing or its variants, e.g. Roughgarden and Talgam-Cohen (2016) and Eden, Feldman, Fiat and Goldner (2018), as surveyed in the source. The SOS paper (arXiv v2, 2019; journal version in Mathematics of Operations Research, 2024) drops single crossing and gives, in its own words, the first welfare approximation guarantees for multi-dimensional combinatorial auctions with interdependent values.
There are agents and items. Agent holds a signal , and is the signal profile. For every bundle , agent 's value is , with ; for nonempty it is weakly increasing in every signal and strictly increasing in .
A function of the profile is strong-SOS if for every coordinate , every and profiles coordinate-wise,
Raising one signal helps less the higher the profile, including the raised coordinate itself; in particular the effect of an agent's own signal is concave. SOS asks this only when the raised coordinate starts from the same value in both profiles.
An allocation gives pairwise disjoint bundles. A deterministic mechanism maps reported signals to an allocation and payments; it is ex-post IC if, whatever the true signals and with the others truthful, no agent gains by misreporting, and ex-post IR if truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.
Let . Random Bucket picks uniformly, calls the high agents, and allocates to them a bundle assignment maximizing , the values with every high signal lowered to ; agent receiving pays . Random Sampling splits the agents uniformly at random into and , allocates to a bundle assignment maximizing , and charges nothing. k-SS runs Random Bucket with probability and Random Sampling otherwise.
For strong-SOS valuations, k-SS is universally ex-post IC-IR and, for every grid profile and every feasible allocation ,
The theorem shows that the price of truthfulness in combinatorial auctions with interdependent values grows only logarithmically in the number of signal values once values are concave in the agents' own signals, compared with the linear of the SOS mechanism. It also exhibits a decomposition of optimal welfare into a part driven by the other agents' signals (OTHER) and a part driven by the agent's own signal (SELF), each covered by a different randomized mechanism; this template recurs in later work on interdependent values.
The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact model behind a proof that is stated in a few lines and checks it against the paper's own appendix: the printed display (9) omits a factor 2 (it fails for one agent with , , ), and the mission states the corrected inequality, which is the case of the paper's display (12) and is what the ratio requires.
The obvious route compares the mechanism's allocation with the optimal one agent by agent, but the mechanisms allocate by proxy values computed from modified signal profiles, and the optimal allocation's value at the true profile is not directly comparable with any single proxy. Covering SELF requires bounding an agent's own-signal contribution within a bucket by its value at the bucket floor, which needs concavity in the own signal and is false under SOS alone. Covering OTHER requires the Key Lemma 3.1 on random zeroing of signals. Incentive compatibility needs the argmax to be read off the proxy profile alone; an argmax with tie-breaking on the full report fails it.
Signals are natural numbers and every hypothesis (nonnegativity, monotonicity, SOS, strong-SOS, the selectors' optimality) is quantified over the grid only. with is a disclosed reading: the buckets cover only for powers of two. The empty bundle is worth , and the monotonicity clauses apply to nonempty bundles. The argmax of each mechanism is an arbitrary selector that sees only the bucket index (or ) and the proxy profile and returns a feasible maximizer; theorems quantify over all such selectors. Random Sampling zeroes all of , the agent's own signal included (the paper's "" is read as ). Expectations are finite uniform averages; at Lean's makes the Random Bucket term vanish, matching .
The approximation is stated for every feasible allocation and with true values at the truthful profile, not with proxy values or a supremum; IC and IR are stated for each deterministic component, not for the mixture's expectation. Replacing the average over partitions by an existential, or the explicit payments by existence of payments, would not be this theorem.
The model layer (signal grid, combinatorial valuations, SOS, ex-post IC-IR, OTHER and SELF, Random Sampling) is shared with the companion missions and lives in InterdepSOS.KHL and InterdepSOS.RSV; strong-SOS, Random Bucket and k-SS are defined in InterdepSOS.KSS. Lemma 6.3 and the decomposition (7), which the proof uses, are posed in the companion mission on k-HL. Proofs of the milestones, and reusable lemmas on concavity in the own signal and on random zeroing, are welcome. The source is the arXiv v2 preprint; the journal version in Mathematics of Operations Research (2024) is not what the mission cites.
The minimum bisection problem asks, for a graph on an even number of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.
Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.
Let be a simple graph on , and write for an edge with ; set if and otherwise. A bisection is a partition of into two sets with . One fixed bisection, unknown to the solver, is the planted bisection; is the set of edges with one end in and the other in .
The cut vector of the planted bisection has exactly when and lie on different sides. The metric relaxation is the linear program, with ,
where (1) ranges over distinct with and (2) over . The LP recovers the planted bisection if is its unique optimal solution. The objective at is .
The graph distance is the length of a shortest – path ( across components). The diameter and the average distance are
The average is over all ordered pairs, the diagonal included. For define
For a connected graph on nodes with a planted bisection,
The proof of Theorem 5 works with the point ,
The mission poses three statements about it, for a connected on nodes:
The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, is small and (18) asks only that exceed roughly . In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.
Theorem 5 is not deep, but it is exact. The milestones fix the witness ; the work is in checking it. The obvious candidate, the graph metric itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by , which depends on and on the factor , is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization (ordered pairs, diagonal included), the factor , and the sign of , and must use wherever it divides by . In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.
Fin n (0-based). The planted bisection is a finset with , and . is the number of pairs adjacent in and on different sides.LPRecovers G V1 says that the cut vector of is optimal and every optimal point equals it.SimpleGraph.edist (in ), is SimpleGraph.ediam, and is the printed formula computed in . and use their real values. All statements assume connected, where these values are finite and .Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound .
Large-scale computing systems route incoming tasks to servers through dispatchers, one per task type. A task can only run on a server that holds the data or software it needs, so the set of admissible pairs forms a bipartite compatibility graph between task types and servers. Full flexibility (every server can serve every type) gives the best load balancing but requires each server to store everything. A central question is how sparse the compatibility graph can be while keeping the performance of the fully flexible system.
For the power-of- policy JSQ() (an arriving task samples compatible servers and joins the shortest of their queues), Rutten and Mukherjee (arXiv:2008.07562v2, Math. Oper. Res. 2023) identify two deterministic graph conditions, proportional sparsity and subcriticality, under which the occupancy process has the same mean-field limit and the same steady-state limit as in the fully flexible system (their Theorem 3.4). They then show that natural random designs satisfy both conditions almost surely. This mission covers the second random design: task types with inhomogeneous levels of flexibility, where each edge incident to task type is present independently with its own probability (Theorem 3.6 of the paper).
Earlier work on JSQ-type policies with constrained compatibility includes the stability analyses of Bramson (Ann. Appl. Probab. 2011) and of Cardinaels, Borst and van Leeuwaarden (Queueing Syst. 2019), to which subcriticality is equivalent for a fixed system (Remark 3 of the paper), and the mean-field analysis of the supermarket model on graphs by Budhiraja, Mukherjee and Wu (Ann. Appl. Probab. 2019), whose load condition is stronger than the condition (A.19) used here (Remark 11 of the paper).
For each there are a set of servers and a set of dispatchers. A compatibility graph is with , and the neighbourhood of is .
Proportional sparsity (Definition 3.1). For every ,
Every set of servers is seen by all but a vanishing fraction of dispatchers in roughly its global proportion.
Subcriticality (Definition 3.3). For each , and nonempty there is a probability distribution on such that, with ,
Some static routing of sampled sets loads no server asymptotically beyond its capacity.
The random graph. Given edge probabilities , the graph contains each pair independently with probability . Write and . Only the law of each is prescribed; the graphs for different may be coupled arbitrarily, and "almost surely" refers to any such coupling.
If, as ,
then almost surely is proportionally sparse and satisfies the subcriticality condition.
implies subcriticality. 3. Lemma B.2. If and , then satisfies the subcriticality condition almost surely.
The goal is the conjunction of Lemmas B.1 and B.2 under (3.5).
Combined with Theorem 3.4 of the paper, the goal says that JSQ() on a random compatibility graph with dispatcher-dependent flexibility behaves, in the large-system limit and in steady state, like JSQ() on the complete bipartite graph. Condition (3.5) allows the least flexible task type to be compatible with only about times a diverging factor of servers in expectation, far below , and allows strongly heterogeneous flexibility levels as long as the spread measured by is controlled. Remark 8 of the paper notes that for and equal probabilities, leaves a dispatcher isolated with probability tending to one, so the growth conditions are close to necessary.
The result is proved in the paper (Appendix B). As far as is known, none of it has been machine-checked. A formal proof requires a quantitative Chernoff bound for binomial tails, a bounded-differences (Azuma–Hoeffding) inequality for functions of independent Bernoulli variables, a union bound over all subsets of servers, and the first Borel–Cantelli lemma in a setting where only per- marginal laws are fixed.
Proportional sparsity quantifies over every subset of the servers. A concentration estimate for one fixed , or one fixed dispatcher, is not enough: whatever bound is used must survive a union over subsets, so a merely vanishing failure probability per dispatcher does not suffice.
Subcriticality is a maximum over all servers of a sum whose terms are not independent: depends on the edge itself, and a term is unbounded in the regime where is small. A direct concentration inequality for this sum therefore does not apply, and the logarithmic factors in (3.5) reflect the need to control all neighbourhood sizes and all servers at once.
Independence across is not available, so almost-sure statements cannot use the second Borel–Cantelli lemma or any law of large numbers along ; every bound must be summable in .
Fin N, dispatchers Fin (M N) with 0 < M N assumed, and a graph is a Finset (Fin N × Fin (M N)).A complete development needs binomial Chernoff bounds, a bounded-differences inequality and Borel–Cantelli for summable bounds; these are reusable for other random-graph statements. Proofs of the deterministic (A.19) reduction and of either lemma are welcome independently.
Online matching platforms for dating, freelancing or ride sharing do not match agents themselves. They decide whom each agent gets to see and how often, and the agents then accept or reject. Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search. The platform designs assortments, which are rates at which types of agents meet, and the agents play an equilibrium of the induced search game. The platform's design problem only makes sense if every choice of assortments leads to a single, well-defined equilibrium outcome. Otherwise "the welfare of an assortment" is not a function of the assortment. This is not automatic: even for simple asymmetric preferences under random meetings, multiple stationary equilibria can arise (Burdett and Coles 1997).
This mission formalizes that well-posedness result, Proposition 3.1(1) of the paper, together with the fixed-point and iteration lemmas of Appendix A.3 and Appendix B.3 on which its proof rests. It is the companion of the mission on the paper's quarter-approximation theorem (Theorem 4.1), which uses the same model.
The source is the arXiv v2 preprint (18 Aug 2021). The Management Science version may number results differently.
There are finitely many agent types on each side of the market, a set and a set , with . Agents of every type leave the market unmatched at a life-event rate , and type arrives at rate . When an agent of type meets an agent of type , the pair draws one utility . Valuations are symmetric: both agents receive if they match, and . Each is a probability law on with no atoms (a "continuous distribution").
An assortment for type is a family of rates at which type- agents meet type- agents on the opposite side. Under a threshold strategy with threshold , a type- agent accepts a meeting if and only if . A meeting turns into a match when both agents accept, i.e. when . If every type plays a threshold strategy, the expected utility of a type- agent is (equation (5))
A type's own threshold enters its own utility through .
One type's equation. Fix the thresholds of the opposite types. Write for the right-hand side of (5) with replaced by . Lemma A.3 states that has exactly one solution. The best-response map of Appendix A.3 sends a profile to the profile in which each type's new threshold is that solution, computed against the opposite side's thresholds in . A best-response sequence starts at the all-zero profile and applies this map repeatedly.
For any fixed assortments there is exactly one threshold profile with
Uniqueness ranges over all real profiles.
Proposition 3.1 is what makes the platform's problem OptimalDirectedSearch well defined. Assortments determine a unique threshold profile. That profile determines the matching rates (Lemma 3.2) and, through stationarity, the population masses. Welfare is then a function of the assortments, and the program (6) used for Theorem 4.1 encodes exactly this fixed point as its incentive constraint (6e). The constructive proof also yields an algorithm: iterate best responses from zero, and the iteration stops after rounds.
Formalizing it adds three things beyond the paper. First, a checked version of an argument the paper gives informally, including the odd/even sandwich of the iteration, which the paper proves in a few lines. Second, a reusable fixed-point and unimodality lemma for ratios of tail integrals, , which recurs in reservation-value arguments in search theory. Third, an exact accounting of the hypotheses: integrable utilities and the reading of the best-response map. To our knowledge none of these results has been machine-checked.
The obvious route to uniqueness, a contraction argument for the map , fails. That map is neither monotone nor contractive in general, since raising a type's own threshold can raise or lower its utility. Existence by Brouwer's fixed-point theorem gives no uniqueness and no algorithm. The best-response iteration does not converge monotonically either: its odd and even iterates move in opposite directions, so convergence in finitely many rounds is a combinatorial statement about the order of the thresholds, not a limit argument. A formal proof also needs continuity and monotonicity of tail integrals of atomless laws, which Mathlib provides only in pieces.
The two sides are separate finite types M and W. A threshold profile is a pair of functions (M → ℝ) × (W → ℝ), ordered componentwise. A market records , and the laws F m w : Measure ℝ. The standing assumptions are:
NullSingletonClass);Tails are and . Capacity (2), flow balance (3) and stationarity (1) are not hypotheses, because Proposition 3.1 holds for any fixed assortments.
The best-response map is encoded as a relation: each new threshold solves its own equation against the opposite side's input thresholds. This is the paper's reading ("This map is a best response by Lemma A.3"). Evaluating (5) at the old profile, own old threshold included, would be a different map. Under that reading finite convergence and the p. 37 claims are false: with one type per side, , and uniform on , its iterates are rational and converge only in the limit to .
Two formalizations would trivialize the goal, and both are ruled out. Uniqueness is over all real profiles, not only nonnegative ones or those reached by the iteration. The tail integrals are not allowed to vanish by default for non-integrable laws, because integrability is a hypothesis. is encoded with a constant chosen before the market.
Not formalized: the agents' Markov decision process of Appendix A.1. Consequently "this strategy profile is a Nash equilibrium", item 2 of Proposition 3.1, Lemmas A.1–A.2 and the best-response sentences of Lemma A.3 and Proposition A.4 are out of scope.
Contributions welcome: continuity and monotonicity lemmas for and for atomless integrable laws, which are reusable well beyond this mission, and proofs of the milestones in any order.
In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent holds a private signal , and every agent's value is a publicly known function of the whole signal profile .
With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking values.
Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, -single-crossing condition, with ratios depending on and . Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.
There are agents and items, and signal values. Each agent has a signal , and is the grid. Agent 's value for a bundle at the profile is ; the empty bundle is worth , and for nonempty , is weakly increasing in every signal and strictly increasing in . We write for the profile with agent 's signal replaced by , and for the profile that keeps the signals of the agents in and sets those in to .
A function of the profile is SOS if for every coordinate , all with , and grid profiles with coordinatewise,
The setting is SOS when every is.
A feasible allocation gives disjoint bundles ; its welfare at is . A deterministic mechanism maps reported profiles to an allocation and payments. Agent 's utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.
The mechanism k-HL runs, with probability , Random Threshold: choose uniformly in , call the high agents, allocate to them a feasible allocation maximizing , and charge agent receiving the price . Otherwise it runs Random Sampling: split the agents uniformly at random into and , allocate to a feasible allocation maximizing , and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.
For SOS valuations with signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile and every feasible allocation ,
where the expectation is over , over and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.
Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the -approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.
The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.
Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid , with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in receive nothing, agents outside receive nothing) must match the mechanism exactly.
Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below ; a condition on all of would be stronger than the paper's. The empty bundle is worth and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive .
The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of ) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, and , never an existential or universal quantifier over or . The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of , the agent's own included (the page's "" is read as ). For , and the threshold average is the empty sum.
Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing .
Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.
The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.
Dividing indivisible goods among agents with different preferences is a central problem of fair division, with applications from inheritance and course allocation to the assignment of compute or shared resources. The standard fairness notion for indivisible goods is envy-freeness up to one good (EF1), introduced by Budish (2011): no agent prefers another agent's bundle once a single good is removed from it. EF1 allocations always exist for additive valuations, and the simplest algorithm that finds one is Round-Robin: the agents take turns in a fixed order, and each picks her favourite remaining good.
That guarantee assumes the algorithm knows the agents' true values. A mechanism only sees what the agents report, and Round-Robin is not truthful: an agent can gain by claiming that a good she likes moderately is her favourite, because she knows nobody else will take the good she likes most. Amanatidis, Birmpas, Christodoulou and Markakis (EC 2017) showed that already for two agents no truthful mechanism without payments can always produce EF1 allocations once there are more than four goods. Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (WINE 2021; Mathematics of Operations Research, 2024) therefore ask a different question: if agents bid strategically and reach a pure Nash equilibrium, is the resulting allocation still fair with respect to their true valuations? For Round-Robin the answer is yes, and this is the paper's main technical result.
Timeline:
There are agents and goods . Agent has a non-negative value for every good, and her value for a bundle is the sum . Values may tie and may be zero.
Each agent reports a bid vector . Round-Robin (Mechanism 1) processes the agents in the order ; the active agent receives the available good with the highest bid in , ties broken in favour of the good with the lower index, until no good is left. So it runs rounds and the last one may be incomplete. It returns an allocation .
The bid is a best response to the others' bids if no other bid vector gives agent a bundle of larger true value . A profile is a pure Nash equilibrium (PNE) if every bid is a best response. An allocation is EF1 if for all with there is with , and EF from 's perspective if for all .
For every instance and every PNE of Round-Robin,
The milestones follow the paper's argument:
The two-agent case, Theorem 3.2, has its own short proof and is included as a companion statement.
The result. Theorem 3.3 shows that a simple, non-truthful mechanism keeps its fairness guarantee under strategic play. Every stable outcome of the bidding game is EF1 for preferences the mechanism never sees. Round-Robin has a PNE in every instance (Theorem A.3, a separate mission of this series), so the guarantee is never vacuous. Theorem 3.4, the statement about the first mover, is of independent interest: it is the strategic analogue of the classical fact that the first agent in Round-Robin envies nobody. The run-comparison Lemma 3.7 is a general tool for sequential allocation mechanisms.
The formalization. The theorem is proved in the paper; it has no machine-checked proof. Formalizing it requires a precise model of Round-Robin with lexicographic tie-breaking, best responses over the continuum of bid vectors, and a careful treatment of ties in valuations. The paper's appendix handles ties with a perturbation argument whose published construction has a gap, so a formal proof also settles that step.
The obvious approach does not work for . With two agents, envy-freeness and proportionality coincide: a non-EF1 allocation leaves an agent with less than half her value, and deviating to her truthful bid would guarantee half (Lemma 3.1). With three or more agents, an agent who envies another agent's bundle may still hold her proportional share, so no single deviation is obviously profitable. One would like to argue that a best response is "at least as good as truth-telling", but the best-response bundle and the truthful bundle are not comparable good by good.
The paper instead replaces a best-responding first mover by an imaginary truthful agent with the same view of the same allocation (Lemma 3.5). The construction is recursive, round by round, and requires controlling how a run of Round-Robin changes when one agent's ranking changes. That is the content of Lemma 3.7, whose induction needs Claim 3.8 to exclude the one bad configuration. Ties in valuations need a further perturbation argument (Lemma A.1).
Agents are Fin n with [NeZero n], goods are Fin m, both 0-based; agent 1 is 0 and picks first. Valuations and bids are real functions Fin n → Fin m → ℝ, with non-negativity stated as hypotheses; bundle values are finite sums, so additivity holds by construction. Round-Robin is defined step by step. At each step, the agent whose turn it is takes the first available good in the stable sort of the goods by non-increasing bid, which is the lexicographic tie-breaking of Mechanism 1. The definition is generalized to a start agent and a good set (rrFrom s G), so that Mechanism 1 is rrFrom 0 univ and the Round-Robin of p. 10 is rrFrom ℓ (M \ H), wrapping around after agent . Lemmas 3.1, 3.5, 3.7, A.1, Claim 3.8 and Theorem 3.4 are stated in that generality, with agent in the role of agent 1; the page states the instance , . The goal is stated for Mechanism 1 only.
Deviations in the best-response predicate range over every non-negative bid vector, not over rankings, truthful bids or a finite menu. Restricting them would weaken the PNE hypothesis and change the theorem. EF1 is measured with the true valuations, never with the bids. Ties are broken lexicographically; an "any tie-breaking" Round-Robin would be a different, nondeterministic mechanism. The goal assumes no strict values, no positive values, no distinct bids and no divisibility .
Lemma A.1 is posed in the reading its proof supports: the profile is fixed before the perturbed valuation is chosen. Read with one valuation for all profiles, the lemma is false.
The development needs only finite sums and finite sets from Mathlib. Contributions to the general run-comparison machinery (how pick and allocBefore behave under a change of one agent's ranking or of the start agent) are reusable for the companion mission on existence of equilibria and for other sequential mechanisms.
Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers based on multiplicative weights and sampling, such as the randomized algorithm of Grigoriadis and Khachiyan (GK95), approximate the value of an game in time sublinear in the size of the matrix. Carmon, Duchi, Sidford and Tian (arXiv:1903.02675) and van Apeldoorn and Gilyén (arXiv:1904.03180) use such game solvers, classical or quantum, as linear-programming solvers. For that to work, the reduction from a linear program to a game must be explicit, with the exact error budget that the game solver has to meet.
This mission formalizes that reduction as it is stated in §4 of van Apeldoorn and Gilyén (2019), Lemma 12 (p. 14). The paper uses it to turn its quantum zero-sum game solvers into quantum LP solvers with cubic dependence on (Theorem 13, p. 15).
The linear program. Let , and . The primal LP (4) and its dual (5) are
The paper's standing assumptions (p. 12) are:
The game. In a zero-sum game with payoff matrix , the column player picks a mixed strategy in the standard simplex , and the row player picks the row with the largest payoff. The value of the game (LP (1), p. 2) is
The reduction. Fix a threshold . With the all-ones vector of length , the game matrix (6) acts on the variables (the original variables, one slack variable and one homogenizing variable):
Write for its value, and set the error level .
For every , every threshold with , and every estimate with ,
This is the paper's "finding the optimal value of the game (6) up to additive error suffices to correctly conclude either or ", with the decision rule its proof uses.
The goal splits into the two exact implications of the proof:
The milestones follow the printed proof, all on p. 14:
The result. Lemma 12 is the bridge that makes any approximate zero-sum game solver an approximate LP solver. It turns the question "is ?" into a single approximate value computation, and binary search over (p. 12) then locates to additive error . The constant is the price of the reduction. It fixes how accurately the game must be solved, and therefore the and factors of Theorem 13. The same reduction appears, in other forms, in classical sublinear LP solvers.
Formalizing it. The lemma is proved in the paper; this mission produces a machine-checked version with every constant explicit. That is not a formality here. As printed, the second row of (6) is , and with that row the lemma is false: for , , , , , and , one has but . The derivation on p. 13 gives , which the mission uses. Step (7) of the proof is written for and needs in general. The mission states the lemma with both repairs, so that later LP-solver formalizations can cite an exact statement. To our knowledge no machine-checked version of this reduction exists.
Each step is elementary, and the difficulty is bookkeeping. The game value is an infimum over the simplex, and the second case needs a strategy that actually attains it, or an approximation argument with slack. The homogenizing variable is pinned only approximately: an approximately optimal strategy satisfies only up to . That error is multiplied by and , whose signs are arbitrary, so the inequalities that look natural for nonnegative data fail for negative or . The relaxed constraints then pass through weak duality, where the dual bound enters, and the errors have to add up to exactly . A reading with would cover only half of the binary search.
Data. is Matrix (Fin n) (Fin m) ℝ, is Fin m → ℝ and is Fin n → ℝ: constraints are indexed by Fin n and variables by Fin m, as in (4). The paper's index letters in §4 vary.
Standing assumptions. A structure LPStanding A b c R r OPT collects them:
The last item is the paper's assumption of strong duality, in the form its proof uses. It is a hypothesis, not a theorem to derive.
The game. The matrix (6) has rows Fin 2 ⊕ (Unit ⊕ Fin n) and columns Fin m ⊕ Fin 2 (with = inr 0 and = inr 1), and its second row is the corrected .
The value. The value is sInf of the image of stdSimplex under . It is not an infimum over a membership proposition, which in Lean would return and make the first case vacuous. LP (1)'s side constraint is omitted because it is inactive for entries in .
Constants. exactly, with .
Added hypothesis. is the one hypothesis not written in the lemma. §4 supplies it through the binary search range, and through the requirement that (6) be a game with entries in .
Trivializing formalizations are ruled out. LPStanding is satisfiable, the second row forces , the value is not junk on a positive game, and the goal is stated for every estimate within rather than only at . A sanity file checks the first three on small instances.
Infrastructure. Everything is built from Mathlib's stdSimplex, Matrix.mulVec and dotProduct. The attainment of the value of a finite matrix game (milestone exists_strategy_le) and weak duality with relaxed constraints are reusable beyond this mission. Proofs of any milestone are welcome, and so are alternative proofs of the second case that avoid attainment by a slack argument.
In large data centres, an incoming task often cannot run on every server: its data, software or licences sit on only some of the machines. Such strict compatibility constraints are modelled by a bipartite graph between task types (dispatchers) and servers. For the fully flexible system, in which every task can go to every server, the JSQ() policy (sample servers at random and join the shortest queue) is described in the large-system limit by the mean-field ODE of Vvedenskaya, Dobrushin and Karpelevich (1996) and Mitzenmacher (1996). Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify two graph conditions, proportional sparsity and subcriticality, under which JSQ() on a sparse compatibility graph has the same mean-field limit and the same steady state as the fully flexible system (their Theorem 3.4).
The two conditions are useful in system design only if there are natural graph families that satisfy them. A storage designer controls the server degree: the number of task types a server can process is roughly proportional to the data it must store. Theorem 3.5 of the paper answers this design question for random graphs. If every server stores data for task types chosen uniformly at random, then together with a mild density condition suffices, even when is negligible compared with the number of task types. This mission formalizes Theorem 3.5's graph-theoretic content and the chain of lemmas in Appendix A that proves it.
A system with servers and dispatchers has a compatibility graph with . The neighbourhood of a dispatcher is ; that of a server is .
Proportional sparsity (Definition 3.1): for every ,
In words, for every set of servers, all but a vanishing fraction of the dispatchers see in roughly the proportion .
Subcriticality (Definition 3.3) with sample size : there are probability distributions on the sets such that
Think of a static policy that routes a task arriving at to a server in a sampled set according to . The condition says that no server receives more than its fair share of load. Its uniform-weight special case is condition (A.19):
The random graph. Let . For each , each server independently chooses its neighbourhood uniformly among the -subsets of , so every server has degree exactly . All graphs live on one probability space, but only the law of each is prescribed; the joint law across different is arbitrary.
If and , then almost surely
The result. Theorem 3.5 shows that the performance of the fully flexible JSQ() system, in the mean-field limit and in steady state, can be achieved with a server degree that grows arbitrarily slowly. The only requirement is that each dispatcher's mean degree grow faster than . Each server then needs to store data for only task types, a vanishing fraction of the types. The threshold matches the scale below which some dispatchers have too few neighbours to share the load evenly.
Formalizing it. The result is proved in the paper, and no part of it has been machine-checked. The mission produces reusable statements about random bipartite graphs with fixed left degree: hypergeometric concentration over all large dispatcher sets, the degree lower tail, and a Borel–Cantelli argument without independence across . It also produces a deterministic reduction from subcriticality to (A.19). That reduction is shared with Theorem 3.6 of the same paper (inhomogeneous random graphs). The printed proof of Lemma A.5 has a gap: (A.23) bounds the probability that some dispatcher has low degree by , but the union over dispatchers gives . This is not summable when grows faster than every polynomial, which the hypotheses allow. A complete formal proof must close this gap or show that low-degree dispatchers contribute too little to matter.
Every statement is almost sure along the whole sequence, but the graphs for different may be coupled arbitrarily, so no strong law over is available. Each a.s. claim needs a failure probability that is summable in , followed by the first Borel–Cantelli lemma. Proportional sparsity quantifies over all server sets , and Lemma A.2 over all dispatcher sets . The obvious argument would concentrate each separately and take a union bound. It fails because is only of order , which may be far smaller than and , so per-dispatcher tails cannot absorb an or union. Uniform control over all large sets (Lemma A.2) is therefore the crux. For subcriticality, the difficulty is that the maximum over runs over servers while the minimum degree runs over dispatchers.
Fin N, dispatchers Fin (M N); a graph is a Finset (Fin N × Fin (M N)), and a random graph is a measurable random adjacency matrix Fin N → Fin (M N) → Bool (the space of p. 13).Tendsto … atTop atTop). is Real.log, so the ratio is at , which does not affect a limit.Finset.powersetCard, and Borel–Cantelli for eventually-uniform statements over families of finite sets.On reward-based crowdfunding platforms such as Kickstarter, a project creator fixes two numbers before launch: the pledge level , the amount a backer commits, and the campaign duration . Both are set once and cannot be revised. A higher pledge earns more per backer but turns away backers whose valuation falls short, and a longer campaign reaches more backers but makes them wait longer for a project they value less the further away its delivery is. Zhang, Savin and Veeraraghavan (Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022; manuscript SSRN 3065267) model this trade-off with two kinds of backers. Independent backers decide on their own valuation. Herding backers arrive in proportion to the pledges already collected, so early success attracts more pledges. The paper asks when the creator should exploit herding and when it should ignore it.
This mission formalizes the paper's answer in the simplest setting it treats: every independent backer values the project at the same , and every herding backer at the same .
A campaign has a population of independent backers, who arrive at rate times the number still to come. Every backer discounts the project's value at rate : a backer arriving at time with valuation pledges if and only if . Herding backers arrive at time at rate times the number of pledges so far, where is an arrival rate and a propensity to pledge, and they pledge under the same discounted-value rule. Valuations lie in and enter only through the survival functions and of the two valuation laws.
The paper solves the pledging dynamics in closed form (its Propositions 1 and 2). The numbers of pledging independent and herding backers at time are
The total number of pledges is , and the creator's problem (18) is
With identical valuations, for and for , and likewise with , where . Proposition 6 adds the constraint , under which every independent backer pledges from the start.
Let , , and set , , and
If and , then on Proposition 6's feasible set the unique maximizer of is
Proposition 6 separates two regimes. When herding backers value the project at least as much as independent ones, the optimal campaign is short, , and its pledge is at least . When herding is weak () and independent backers value the project enough more than herding ones, the creator's best response is to price herding backers out entirely and run the campaign that would be optimal if no herding backer existed. The threshold (33) quantifies "enough more". Together with Proposition 3(b), which fixes the duration and finds that the optimal pledge sits exactly at the highest level that keeps every independent backer in from the start, these results give a creator explicit rules rather than a numerical optimization.
The paper states that the proofs of Propositions 3 to 7 are in an online Technical Appendix, which is not part of the manuscript this mission cites; the manuscript's own Appendix proves only Propositions 1 and 2 and Corollaries 1 and 2. None of the results has a machine-checked proof. Formalizing Proposition 6(ii) would supply a verified proof of a result whose published proof is not in the source held here, and would check the threshold (33), whose grouping of terms is read off the typeset page.
The objective is defined through nested integrals of step functions, so it is not differentiable everywhere: the jumps of and put kinks in where and where or , at which a backer type starts or stops pledging during the campaign. Setting a gradient to zero does not identify the optimum. The obvious argument for the goal, that herding backers do not pledge at and so the no-herding optimum is optimal, compares only campaigns that exclude herding backers; it says nothing about the campaigns with a lower pledge level that do attract them. Those campaigns gain a herding term growing exponentially in times the time during which herding backers pledge, and the comparison must hold uniformly over the whole feasible region, which is what the threshold (33) is for. Uniqueness, not only optimality, must also be shown.
All objects live in the namespace CrowdfundRM.Identical. Parameters form a structure Campaign with fields Ihat, k, r, Lh (for ), q, vbar, Fbi, Fbh. The standing assumptions, implicit in the paper, are , , and that each survival function is nonincreasing, takes values in , equals below and from on. Identical valuations set , to the step functions above with .
Conventions: real numbers throughout; the pledge counts are the closed forms (5) and (11); the feasible set of (18) adds , which requires; "the optimal" is the unique maximizer over the stated feasible set, and Proposition 6(i), which does not claim uniqueness, asserts that a maximizer exists and bounds every maximizer; "sufficiently long" in Proposition 3(b) is an unspecified threshold ; is added in Proposition 6(ii) because and divide by . The paper's has an undefined and is read as . In (33) the factors and multiply only the first bracket.
The following formalizations would trivialize the targets and are ruled out: defining by the explicit formulas (14)–(15) or by the paper's single formula (17) instead of (5) and (11); stating optimality through sSup or a first-order condition; stating Proposition 6(i) for maximizers without asserting that one exists; and stating Proposition 3(b) with a chosen threshold or with Proposition 6's narrower feasible set. The pledging differential equations themselves and their solution (Propositions 1–2) are formalized in the companion mission on triangular valuations; this mission works from their closed forms.
Infrastructure needed: interval integrals of monotone step functions, the exponential, logarithm and real power from Mathlib. Explicit evaluation of the nested integrals under step laws (Corollary 1) is reusable for any proof in this model. Contributions are welcome on each milestone and on lemmas such as continuity of on the feasible set and the closed form of in each region of .
In hiring, admissions and procurement, candidates are often judged by scores that are known to be biased: two candidates from different groups, schools or evaluation pipelines cannot be compared by their observed scores, while two candidates from the same pipeline can. Salem and Gupta (SSRN 3444283, published in Management Science, 2023) model this situation as a poset secretary problem. The decision maker sees only a partial order between candidates, namely the comparisons that are trustworthy, and must still make irrevocable online selections.
The classical secretary problem and its -selection variant (Kleinberg, 2005) assume a total order. With only partial comparisons, the natural question is how much the missing comparisons cost. Salem and Gupta answer it in terms of the width of the poset. This mission formalizes their lower bound: no algorithm can do better than a factor of the width.
A finite set of candidates carries a partial order . Each candidate has a true score . The scores are nonnegative and pairwise distinct, and they are consistent with the order: implies . The pair is an instance. Candidates arrive in uniformly random order. An algorithm knows and a capacity , observes the comparisons of among the candidates that have arrived, and selects at most candidates, irrevocably. It never observes the scores.
The offline optimum is
An algorithm is -competitive if on every instance (Definition 3.4).
The width of is the largest number of pairwise incomparable candidates (an antichain).
Because an algorithm sees only the poset and the arrival order, on a fixed poset its randomness (arrival order and internal coins) induces a probability distribution on the selected set, supported on sets of at most elements, and does not depend on the scores. Such a is called a selection rule with capacity . Its expected score is . The selection probability of is .
The instance of the lower bound is : disjoint chains of elements each, with elements in different chains incomparable (Figure 8 of the paper, with ).
For every and there is a poset of width such that for every selection rule with capacity and every there is a consistent scoring with and
Equivalently, for every algorithm, , the supremum taken over the scorings of .
The result shows that the width of the poset is a genuine barrier: whatever the algorithm, an adversary choosing scores after seeing how the algorithm spreads its selections can force a ratio arbitrarily close to . The paper's ProxyLabel algorithm has competitive ratio at most when the width is known (Corollary 5.1, p. 15). Together the two results show that the best achievable competitive ratio in the poset secretary problem is of order , which the paper calls order-optimal. The lower bound also covers the group-bias model of the paper: groups whose members are compared only within their group form exactly the instance used here.
On the formal side, the result is proved in the paper but has no machine-checked proof. The mission produces a formal model of score-independent randomized selection on a finite poset, a formal offline optimum with selections, and the width of a disjoint union of chains. These can be reused for other lower bounds in online selection.
The argument is short, and the work lies in getting the quantifiers and the encoding right. The printed statement places "there is an instance" before "for any algorithm". Read literally this is false for : on a fixed instance, the algorithm that always selects the highest-scoring elements achieves ratio . The proof establishes the other order: the poset is fixed, then the algorithm, then the scoring. A formalization must keep the scoring chosen after the algorithm while preventing the algorithm from depending on the scores.
The printed chain of inequalities also needs care. Its middle step drops the term , which the stated constraints on the perturbation do not make nonpositive. The bound therefore holds for perturbations chosen small enough, not for every perturbation satisfying the printed constraints. The existence of distinct, order-consistent scores meeting all the constraints at once has to be shown, and so does the identification of the optimum with the heavy chain.
Elements form a finite type with a partial order. A consistent scoring is a function to that is nonnegative, injective and strictly monotone (). These are the standing assumptions of the model (§3.1, p. 7), not additions. is a finite maximum over subsets of at most elements. Width is the published definition AppliedComb.Posets.width, the size of a largest antichain, not a minimum number of chains, so the width milestone is a real claim. Algorithms are represented by selection rules: nonnegative weights on subsets summing to and vanishing on subsets of more than elements. This class contains the selected-set law of every online algorithm, so a lower bound for it is a lower bound for online algorithms. Expectations and probabilities are finite sums. Competitiveness is stated as together with , with no division by an expectation that may vanish. The hypotheses and are standing: with the poset is empty, and with every ratio is . The instance is the sigma type with Mathlib's disjoint order.
Trivializing formalizations are ruled out explicitly. A selection rule must have total mass , so the zero rule does not make the expected score vanish. It must respect the capacity, so the rule selecting everything is excluded. The scoring is quantified after the selection rule, never before it and never as an input to it. is part of the conclusion.
The development needs finite sums over subsets, the order on sigma types, and antichains. Contributions are welcome on any milestone. The width of a disjoint union of chains and the pigeonhole bound on selection probabilities are reusable beyond this mission.