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?
Best subset selection fits a linear model using at most of the available features: it minimizes the residual sum of squares subject to the sparsity constraint , where counts the nonzero coordinates of . Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) show that best subsets overfits when the signal-to-noise ratio is low, and propose adding a shrinkage penalty with to the same constrained problem. Their statistical results (oracle inequalities, a lower bound for best subsets, a BIC-type choice of ) are the subject of the companion missions II–VI of this series.
The estimator is a mixed-integer program. To compute it in practice, and to warm-start the mixed-integer solver that certifies optimality, the paper uses a discrete first-order (DFO) method: a proximal-gradient iteration in which the proximal step is a projection-like operation onto the set of -sparse vectors with a norm penalty. The method descends from iterative hard thresholding (Blumensath & Davies, 2009), from proximal gradient methods for composite problems (Nesterov, 2013), and from the discrete first-order algorithms of Bertsimas, King and Mazumder (Annals of Statistics, 2016). This mission formalizes the paper's convergence guarantee for it, Proposition 2.
Vectors live in with the Euclidean inner product and norm . Write for the number of nonzero coordinates and . For the penalty is the norm itself, not its -th power.
Let be a differentiable convex function whose gradient is -Lipschitz:
The motivating case is with . The composite problem (7) is
For the quadratic model of around is
and the thresholding operator is the set of minimizers
which can contain several points when the have ties. A DFO sequence with constant starts at a -sparse and, for , picks any
Assume in addition and . For every DFO sequence:
(a) if , then is non-increasing in and converges to some ;
(b) if , then for every
The statement holds for any of the stated class and any choice in the set-valued operator; nothing about least squares is assumed.
Proposition 2 is what makes the DFO method a sound component of the paper's computational pipeline. The objective values never increase, so every iterate is a feasible point at least as good as the warm start. Part (b) says that the step length is small after iterations. A point whose step vanishes is a fixed point of the update, which the paper calls a first-order stationary point (Definition 1). The stopping rule of the algorithm () is therefore reached in at most steps.
The result is proved in the paper, in half a page that defers its central inequality (22) to Proposition 6 of Bertsimas, King & Mazumder (2016). It has not been formalized. A machine-checked version produces three reusable pieces: a descent lemma for functions with Lipschitz gradient on , the variational characterization of the sparse proximal step, and a sufficient-decrease-to-rate argument for any descent method. These are the same pieces that iterative hard thresholding, proximal gradient, and block-coordinate methods for problems need.
The difficulty is moderate, and it lies in the infrastructure rather than in any single step. The descent lemma (9) needs the fundamental theorem of calculus along a segment for a function on a Euclidean space, combined with the Lipschitz bound on the gradient. The feasible set is not convex, so no convex-analysis argument (subgradient optimality, firm nonexpansiveness of a proximal map) applies to the thresholding step. Inequality (22) must instead be obtained by comparing the minimizer with the feasible competitor itself, which is why the hypothesis appears. Part (a) also needs a lower bound on for its limit to exist and be nonnegative, which the general class of does not provide on its own.
is EuclideanSpace ℝ (Fin p), the gradient is Mathlib's gradient f, and coordinates are -based. Membership in is a predicate: feasibility plus minimality against every -sparse competitor. No selection from the set is fixed, and existence of minimizers is not assumed. A DFO sequence is any β : ℕ → ℝᵖ satisfying the update for every , indexed from as printed. The stopping rule and the support-restricted polishing Step 2 are not part of it. The penalty is for and the Euclidean norm for , and every theorem assumes and . The minimum over is a finite infimum over a nonempty index set.
Three hypotheses are added to Proposition 2 as printed, each disclosed in the item. The proof's claim "" is false for a general convex with Lipschitz gradient ( sends to ), so and are assumed. The update divides by , and allows , so is assumed. "Decreasing" is read as non-increasing. Convexity of is kept as in the paper's setting (7)–(8), though only the gradient bound is used. Proposition 1 is stated with an existential ordering: for a fixed sorting permutation the printed claim fails under ties.
The statement cannot be trivialized by restricting or the run. The goal quantifies over every of the class and every sequence obeying the update, the limit in (b) is the actual limit of the objective values, and the rate holds for every . Not formalized here: the mixed-integer formulations, the continuation and local-search heuristics of §2.4, Definition 1, and the paper's statistical results (missions II–VI). Contributions of reusable infrastructure, such as a general descent lemma or a lemma turning summed decrease into a rate, are welcome as separate theorems.
Most online advertising is sold by auction, one impression at a time, to advertisers who manage a budget over many auctions rather than a value for a single one. Since 2019 the major ad exchanges have moved from second price to first price auctions, in which the winner pays its own bid. A budget-constrained advertiser in a first price auction must therefore shade its bids twice: once because of the budget, and once because of the payment rule. Whether these two effects admit a coherent equilibrium, and of what form, is the question behind Balseiro, Kroer and Kumar, Contextual Standard Auctions with Budgets: Revenue Equivalence and Efficiency Guarantees (Management Science, 2023, doi:10.1287/mnsc.2023.4719).
Earlier work on pacing equilibria treated second price auctions, where truthful bidding is dominant without budgets (Balseiro, Besbes and Weintraub 2015; Conitzer et al. 2022). In first price auctions with a single deterministic item, an equilibrium may fail to exist (the paper's Online Appendix A). The paper restores existence by letting items carry a random context and values depend on it linearly. This mission formalizes its first main result, Theorem 1: an equilibrium of a simple, interpretable form exists.
An item has a context , a feature vector drawn from a law with a density. There are buyers. Each buyer has a type , a weight vector and a budget , drawn independently from a law with a density on
Buyer values item at , and . The seller reveals , then runs a first price auction with a public reserve price : a bid wins if , where is the strategy of the competitors, and the winner pays its bid. A budget only needs to hold in expectation over and the competitors' types.
A strategy is a symmetric first price equilibrium (SFPE, Definition 1) if for -almost every type the bid function solves
A pacing function scales values down to paced values . Let be the distribution function of the highest of i.i.d. paced values, and for let
with if and if . The value pacing–based strategy (Definition 2) is
For a buyer facing competitors who use , the dual function is for .
The paper states that Proposition 2 combined with Proposition 1 implies Theorem 1.
Theorem 1 says that budget-constrained buyers in contextual first price auctions have an equilibrium that is described by one scalar per type: shade the value by the factor , then bid as an unconstrained buyer would in an i.i.d. first price auction against paced competitors. This is the object on which the rest of the paper is built: revenue equivalence across standard auctions (Theorem 2) and a liquid-welfare price of anarchy of at least (Theorem 3) are both statements about pacing-based equilibria. Practically, it supports the use of pacing for budget management in first price auctions, with pacing multipliers computed as for second price auctions.
The result is proved in the paper; every proof is in its online appendix, which is not part of the source this mission cites. Nothing in the paper is formalized. A formalization would check a strong-duality argument for a non-convex problem and an infinite-dimensional fixed-point argument whose topology the authors chose with care, and it would produce reusable pieces: multivariate total variation, compactness of bounded-variation sets in , and the first price equilibrium bid against an arbitrary (possibly atomic) value distribution with a reserve price.
The buyer's problem is not convex in the bid function, so standard convex duality does not give strong duality; Proposition 1 needs a direct argument combining Lagrangian optimality (Lemma 1), differentiability of in , and complementary slackness. Lemma 1 itself cannot quote the textbook first price equilibrium, because the paced value distribution may have atoms and the reserve price creates discontinuities.
The fixed point lives in an infinite-dimensional space of pacing functions. The obvious topologies fail: the set of bounded pacing functions is not compact in any , and in the weak-* topology of upper hemicontinuity of the best-response correspondence is hard to obtain; restricting to Lipschitz functions loses the property that best responses stay in the set. The paper restricts to functions of bounded total variation, which requires the monotonicity of Lemma 2 and the variation bound of Lemma 3.
Contexts are Fin d → ℝ, types are pairs (w, B) : (Fin d → ℝ) × ℝ, and is the explicit sum . A single Model structure holds , and Model.Standing collects the assumptions of §2.2 together with four that the paper uses without stating them: , , nonempty and bounded (so ), and measurability of and . Pacing functions are measurable functions on that are nonnegative on ; values off are irrelevant since .
The conventions fixed in Lean:
IsMinOn, over in Propositions 1–2 and over in Lemma 5 and , as printed.EReal, with Euclidean and test fields supported in ; is with respect to Lebesgue measure. Lemma 4 is stated on the image of in Lp ℝ 1 (volume.restrict Θ), in its norm topology.A formalization in which is defined by its closed form, in which non-integrable payments count as zero, or in which the strategy need not be measurable would make the milestones easier without proving the paper's theorem; these readings are excluded by the definitions above.
A complete development needs: first price equilibrium bids for general atomic distributions with reserves; measurability of parametric integrals; a duality argument for one-dimensional Lagrangian relaxations; multivariate bounded variation and its compact embedding in of a box; and the Kakutani–Fan–Glicksberg theorem in a locally convex space. The bounded-variation and fixed-point parts are reusable beyond this mission. Proofs of any milestone, and alternative arguments, are welcome.
A person using a machine's advice may decide more accurately, but attention is costly. Before asking what a machine changes, the baseline decision has to be understood: how often would the person choose the action associated with a good state without machine input? Boyacı, Canyakmaz, and de Véricourt study this question in a model of a decision maker who can acquire information about an unknown binary state and pays for the expected reduction in uncertainty. Their working paper derives a closed form for the decision maker's choice probability. That baseline is used later in the paper to compare decisions with and without machine input.
The information cost follows the rational inattention approach: a decision maker chooses how much information to process while considering its effect on the final action. In the discrete choice setting, Matějka and McKay (2015) characterize optimal conditional choice probabilities. The paper adopts their equivalent choice probability representation in §4. This mission isolates the first consequence of that representation, Theorem 1, before the paper introduces the machine.
The unknown state is good, , with prior probability , and bad, , with probability . The decision maker selects either (declare good) or (declare bad). A correct action earns one unit, and an incorrect action earns zero. Write for the probability of choosing when the state is , and for the probability of choosing when the state is . A strategy is any pair ; the pair may lie on the no-information diagonal or on the boundary of the square.
The unconditional choice probability is . The accuracy is . Binary entropy, measured with the natural logarithm, is , with . Given an information-cost parameter , the cognitive cost in the paper's choice probability representation is
The decision maker maximizes net value over the whole square. An optimal pair is one whose value is at least that of every feasible pair. The source originally introduces a general distribution of information signals and a Bayes consistency condition in problem (2). Section 4 and footnote 8 adopt the equivalent conditional choice probability representation used here. The equivalence itself is an input from Matějka and McKay (2015), rather than a claim of this mission.
For and , define the thresholds
The goal is the paper's Theorem 1: every optimal pair has the same unconditional choice probability,
The same theorem states , that is non-decreasing in the prior, and that the lower threshold increases while the upper threshold decreases as increases. This mission includes all these clauses in its single goal. The intermediate milestones formalize the paper's conditional choice equations, the algebraic interior candidate, its threshold crossings, and its slope and threshold derivatives.
The formula partitions prior beliefs into three regimes. With a sufficiently low prior, the decision maker always chooses ; with a sufficiently high prior, the decision maker always chooses . Between the thresholds, the probability of choosing changes continuously with the prior. The threshold movements describe how a higher information cost changes the region in which information processing affects the choice. In the paper, these probabilities feed into accuracy, error rate, effort, and machine input comparisons.
The paper proves the result mathematically. The statements here are open Lean targets, so compilation of their declarations does not amount to machine-checked proofs. A complete development would verify the optimality characterization and the closed form, then provide reusable binary entropy and constrained optimization lemmas. It would also expose a precise baseline that subsequent missions can import after publication.
Equations (4)–(6) alone do not select the optimum: both and satisfy them for every prior. The printed uniqueness phrase in Lemma 1 therefore cannot be carried into a theorem about all solutions of those equations. The formal target says instead that every maximizing strategy satisfies the conditional choice equations, and Theorem 1 identifies the probability selected by maximization. The endpoint strategies, where entropy is evaluated at zero or one, must remain in the feasible set. One must also distinguish the algebraic interior root from the optimizer when that root leaves .
Lean represents probabilities and costs as real numbers. The strategy space is the full closed square , and IsOptimal compares net value against every point in that square. The prior in the goal and Lemma 1 lies strictly between zero and one, as in the paper's §4 setting; is strictly positive. Boolean state and action types are unnecessary in this first mission because the paper's §4 representation is already the pair of conditional probabilities. The general-signal distribution of problem (2) is not encoded here.
The entropy function is Mathlib's Real.binEntropy, with natural logarithms and the endpoint values used by the paper. The threshold definitions reproduce Theorem 1 exactly. pBar is the interior algebraic expression from Appendix A, and pClosed is only the right-hand side of equation (11). Neither defines the optimizer. In particular, defining the starred optimal probability by the closed form would remove the theorem's main claim. The goal quantifies over every optimal pair and asserts that its computed choice probability equals that expression.
Contributions to the proof will need results about binary entropy at the boundary, derivatives of the objective in the interior, existence and characterization of maximizers on a compact square, and elementary inequalities for the exponential thresholds. The entropy and compact optimization infrastructure can support later formalizations beyond this paper. The four listed milestones follow the authors' Appendix A argument; alternative proofs of the same faithful statements are welcome.
Certify the separation exponent using OpenAI's construction. Sensitivity counts individual bit flips that change the output; block sensitivity counts disjoint sensitive blocks. Both are maximized over inputs. The notation fixes one input, and denotes the all-zero input.
The goal requires arbitrarily large sensitivity and for every . OpenAI's depth-nine seed, with , supplies a slightly larger exponent; the displayed decimal must be certified exactly.
This mission is the campaign's foundation. Its central reusable milestone turns a finite certificate , , , and into the asymptotic claim at exponent . Normalization and sensitivity growth are proof obligations. Later missions import this theorem and the shared definitions.
OpenAI's quantitative separation is already proved on Prove2Me. This mission certifies the numerical exponent and the reusable bridge; its goal remains Open until all required proofs are accepted.
The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum total cost. Worst-case bounds on it over whole classes of cost functions are classical (Roughgarden and Tardos, 2002; Correa, Schulz and Stier-Moses, 2004). In practice the demands and cost functions of a traffic model are estimated, never known exactly, so a second question matters as much as the worst case: how much does the PoA of a given game move when its data move?
Wu and Möhring (arXiv:2007.13979v3, published in Mathematics of Operations Research, 2023) answer this with a metric on games that compares demands and cost functions simultaneously. They show that the PoA is continuous, that it is Hölder continuous with exponent near every game whose costs are Lipschitz, and that it is not uniformly Hölder continuous. This mission formalizes their Theorem 12 (§4.3): at two special classes of games, games with constant costs and games with strictly increasing continuously differentiable costs, the exponent improves to , so the PoA is locally Lipschitz. The authors motivate the result by the differentiability results of Cominetti, Dose and Scarsini (2020), which suggest Lipschitz behaviour at games whose costs have strictly positive derivatives.
Fix a finite set of arcs, a finite nonempty set of origin–destination (O/D) pairs, and for each a set of at least two paths, each a nonempty set of arcs; every arc lies on some path. A game consists of arc cost functions , continuous, non-decreasing and non-negative on , and demands with total demand ; moreover for . These games form the game space .
A flow routes each demand, . The arc flow is , the path cost , and the total cost . A flow is a Wardrop equilibrium (WE) if every used path of a pair is a cheapest path of that pair. The SO cost is the minimum total cost, the WE cost is the total cost of a WE flow (all WE flows have the same cost), and the PoA is
The distance of two games and is
which compares cost functions only on the range both games use, plus their values at the respective total demands.
Let .
then there are and such that
The goal leaves the constants unspecified; only their existence, depending on alone, is asserted.
At a general game with Lipschitz costs the PoA is only Hölder continuous with exponent in this metric, and the paper shows that no exponent works uniformly over the game space. Theorem 12 identifies two natural classes of games at which the sensitivity is linear: constant costs (the PoA equals and grows at most linearly under perturbation) and strictly increasing costs, which include affine costs with positive slopes. For these games an estimation error of size in demands and costs changes the PoA by .
The result is proved in the paper; it is not formalized anywhere. A complete development would also provide machine-checked equilibrium-comparison estimates between two games of one demand slice ((4.39)–(4.40)), which are reusable for any stability analysis of Wardrop equilibria. The paper's explicit constants in (4.41)–(4.46) are off by a factor (the last step of (4.40) uses ); the existential Theorem 12 is unaffected, and a formalization with correct explicit constants is a welcome addition.
The PoA is a ratio of two optimal values, and the perturbed game may change the demand vector and the costs at once, including the costs on , which 's hypotheses do not control. A direct comparison of and therefore fails: the WE flows live in different feasible sets, and the hypotheses on say nothing beyond . The general Hölder- argument loses a square root exactly where it bounds the distance between the arc flows of the two equilibria through an approximate-equilibrium estimate; obtaining exponent requires an estimate in which the flow difference enters linearly, and this is where strict monotonicity of the costs is needed. Constant costs are degenerate in the opposite direction: the WE is far from unique, and only costs, not flows, can be compared.
The model follows §2–§3.2 of the paper and reuses the published definition KellyStochasticNetworks_Wardrop for arc flows, feasibility and the Wardrop condition. Paths are nonempty incidence columns (a generalization of loop-free paths that the proofs do not use); is nonempty and Condition 1 is standing (, every arc on a path). Costs are functions constrained on only. is an infimum over all flows, a supremum over WE flows, ; the distance is (3.3) with the sup norm on demand and endpoint vectors and a supremum over the compact set . The derivative in Theorem 12b) is derivWithin on , one-sided at the endpoints, and is ContDiffOn ℝ 1 on that interval.
Every statement quantifies over games in the game space only: off it, would be a junk ratio such as . The paper prints the conclusions of Theorem 12 and (4.33) with a strict inequality, which fails at ; the non-strict form is posed, and no hypothesis is added (distinct games can have distance ). Milestones (4.39) and (4.40) are posed for two arbitrary games of one demand slice, the general form of the paper's step for its auxiliary game.
A complete development needs existence of SO and WE flows on the game space, the variational characterization of Wardrop equilibria, the mean value theorem on a closed interval with one-sided derivatives, and continuity of in the metric; contributions of any of these as separate lemmas are welcome. The source is the arXiv preprint v3; the published Mathematics of Operations Research version is not the cited artifact.
Traffic users choose routes for themselves, while a planner may choose routes that minimize everyone's combined travel cost. The price of anarchy measures the cost of the users' equilibrium relative to the planner's optimum. Travel demand and arc latency functions are estimated from data and change over time, so a ratio that changes abruptly under a small input change would be difficult to interpret or use. Wu and Möhring study this sensitivity for nonatomic congestion games, where each individual user has negligible influence on arc flows. Their preprint proves that the optimum cost, equilibrium cost, and their ratio vary continuously over the game space they define. This mission isolates that foundational continuity result. It supplies the qualitative starting point for the paper's later Hölder and Lipschitz estimates.
The cited artifact is arXiv:2007.13979v3, dated 2021. The article subsequently appeared in Mathematics of Operations Research in 2023, but theorem numbers and pages here refer to the preprint.
Fix finite sets of arcs, of routes, and of origin–destination pairs. Each route serves one pair and contains at least one arc. Every arc belongs to some route, and every pair has at least two routes. A game assigns each arc a nonnegative, nondecreasing, continuous latency function and each pair a nonnegative demand . The total demand is . These are the paper's basic model and standing combinatorial assumptions (pp. 10–11 and 14).
A feasible flow puts nonnegative traffic on routes so that the traffic for each pair sums to its demand. The induced arc flow is . Its total cost is
A social optimum (SO) is a feasible flow minimizing total cost. A Wardrop equilibrium (WE) is a feasible flow in which every route carrying positive traffic has minimum cost among the routes serving the same pair. Write for the SO cost and for the WE cost. The paper shows that all SO flows have the same cost and all WE flows have the same cost (pp. 11–12 and 18).
A generalized game has the stated nonnegative demands and regular latency functions. The game space further requires and for every arc and every , the paper's Condition 2. On this space, the optimum cost is positive and the price of anarchy is defined by
For and , the paper's distance is the maximum of three discrepancies: the sup norm of , the largest for and , and the sup norm of . The last term compares costs at the two games' respective demand endpoints. Games with equal demands and equal latency functions up to that demand are identified as equivalent (pp. 15–17, (3.1)–(3.3)).
The supporting milestones establish a positive lower bound for and an upper bound for (Lemma 3), the distance properties of generalized games (Lemma 4), and behavior of feasible, SO, and WE flows under convergent game sequences (Lemma 5). The goal is the paper's Theorem 6, p. 19: for any sequence with and ,
The theorem establishes that sufficiently small changes in both demand and latency data produce small changes in the two total costs and their ratio. It allows the PoA to be treated as a stable observable of a game, including where the identity of an optimum or equilibrium flow changes. The result is qualitative: it does not supply a uniform rate of change. The same paper investigates sharper rates under additional assumptions (§4).
The mathematical result is proved in the paper. In this mission its statements and definitions are compiled Lean drafts, while proofs of Theorem 6 and its milestone lemmas remain open. A completed development would make the game-space metric, limit-of-flow statements, and cost continuity available for later sensitivity results on nonatomic routing.
Pointwise continuity of each does not by itself control an optimum or equilibrium when demands change: the feasible-flow sets change with , and a flow for one game need not be feasible for another. A converging sequence of games can also have different optimal or equilibrium flows at every index. The distance compares functions only on demand-relevant intervals, so limits of costs must respect those varying intervals. Finally, continuity of the quotient requires a positive optimum cost throughout the game space; the paper's Condition 2 is what makes that denominator meaningful (pp. 15–19).
Lean uses finite types for arcs, routes, and pairs; a route is a nonempty – incidence column and is assigned to one pair. This admits arbitrary route collections rather than insisting on loop-free directed graph paths. The standing network predicate records the nonempty pair set, nonempty routes, every arc's membership in a route, and at least two routes per pair. Costs are total functions on the reals, with continuity, monotonicity, and nonnegativity required only on . Flow feasibility, arc flow, the Wardrop condition, and the potential reuse the published KellyStochasticNetworks_Wardrop definition. The total cost uses the arc formula; is an infimum over feasible flows and a supremum over WE flows. On valid games these recover the paper's common SO and WE costs.
The distance uses the sup norm on finite vectors and a real supremum over the bounded shared demand interval. Convergence is stated sequentially, following the paper, without imposing a metric-space instance on raw games that may be equivalent. Every theorem involving quantifies over the game space, so a zero denominator or an empty equilibrium set cannot supply a spurious value. The route-count and arc-count factors in Lemma 3 are the actual finite cardinalities. Contributions that establish existence and compactness of relevant flow sets, equivalence of the arc and path cost formulas, and the stated limit properties are useful beyond this theorem.
Dividing indivisible goods fairly among agents is a basic problem of fair division. Most of the literature assumes that the agents' valuations are known to the algorithm. In practice the algorithm only sees what the agents report, and an agent may misreport to get a better bundle. For allocation without money, truthful mechanisms are very restricted: for two agents with additive valuations, truthfulness and fairness are essentially incompatible (Amanatidis, Birmpas, Christodoulou and Markakis, EC 2017, reference [3] of arXiv:2109.08644v2).
Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644v2; Mathematics of Operations Research, 2024) drop truthfulness and ask a different question: do the pure Nash equilibria of a mechanism lead to allocations that are fair with respect to the agents' true valuations? They show that Round-Robin's equilibria are EF1 and that a modified cut-and-choose mechanism for two agents has equilibria that are MMS and EFX. This mission formalizes the last result of §4.2: a statement about every mechanism whose equilibria always exist and are always EFX.
There are two agents, and , and a finite set of indivisible goods. Agent has a non-negative value for each good and values a bundle additively, . Zero values are allowed. An allocation is a partition of : every good goes to exactly one agent.
A mechanism takes a bid profile , with the values agent claims, and returns an allocation of all goods. A bid profile is a pure Nash equilibrium (PNE) for the valuations (Definition 2.7) if no agent can obtain a bundle of strictly larger true value by switching to any other non-negative bid vector .
The class studied here (p. 18) consists of the always-EFX mechanisms: for every valuation profile on , has at least one PNE, and every PNE leads to an allocation that is EFX with respect to . The class is non-empty: the paper's Mod-Cut&Choose belongs to it (Theorem 4.3).
For every always-EFX mechanism , every valuation profile and every PNE ,
The number may depend on the instance and the equilibrium. The theorem asserts the strict separation from , with no explicit constant.
Theorem 2.6 is tight: for every there are EFX allocations that are not -MMS. Theorem 4.7 says that such allocations never arise as equilibria of a mechanism in the class, so strategic behaviour in an always-EFX mechanism yields strictly more than the generic EFX guarantee. For four goods the paper proves that equilibria of the class are fully MMS (Theorem 4.5); whether that holds for more goods, or whether a uniform exists, is left open in the paper's discussion (p. 22). A full MMS result would imply that computing best responses in any polynomial-time mechanism of the class is hard.
The result is proved on paper. As far as the platform's records show, none of these statements has a machine-checked proof. Formalizing it produces a reusable layer for strategic fair division: bids, best responses and PNE over all non-negative bids, EFX in the positive-goods form, and the two-agent EFX ⇒ -MMS bound.
The goal is a statement about an arbitrary mechanism, known only through two properties that hold on all valuation profiles. The natural first attempt, arguing from the allocation alone, cannot work: an EFX allocation can be exactly -MMS, so the equilibrium property must be used. The proof has to couple the equilibrium of the given instance with an equilibrium of an auxiliary instance on the same goods, about which nothing is known except that it exists and is EFX. Controlling what the mechanism outputs on mixed bid profiles, built from the bids of the two equilibria, is where the work lies. Zero-valued goods are essential to the argument, because EFX ignores them.
Fin 2 (agent 1 is 0), goods are Fin m for an arbitrary m; good (or
) is j - 1. Valuations are real per-good values with non-negativity as a hypothesis;
bundle values are sums, so additivity is built in. Bids are real vectors with non-negative
entries.LittleCharity.MMS.mms with two labelled, possibly empty,
bundles.Trivializing readings are ruled out: the conclusion requires strictly and the same for both agents; measuring fairness with bids instead of true values, restricting deviations, or asking for a uniform over the class would each change the theorem.
Contributions welcome: proofs of Theorem 2.6 and the two counting steps (pure finite combinatorics over additive valuations), the case analysis for , and the final coupling argument. The maximin-share facts used (such as ) are also useful elsewhere.
Dividing indivisible goods fairly is a central problem of computational social choice. With additive valuations, the fairness notions of interest are relaxations of envy-freeness, since exact envy-freeness is often impossible with indivisible items. The strongest relaxation in common use is envy-freeness up to any good (EFX) (Caragiannis et al., 2019); a different, share-based benchmark is the maximin share (MMS) (Budish, 2011).
Most algorithms that produce such allocations take the agents' valuations as input. When agents report these valuations themselves, they may misreport, and truthful mechanisms without payments are known to be very limited (Amanatidis, Birmpas and Markakis, 2016). Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) instead ask what fairness survives at the pure Nash equilibria of a non-truthful mechanism, measured with the agents' true values. This mission formalizes one of their answers: for two agents and four goods, every equilibrium of a mechanism whose equilibria always exist and are always EFX is in fact an MMS allocation.
There are two agents, and , and a set of indivisible goods. Agent has a non-negative value for each good , and values a bundle additively, . An allocation is a partition of : every good goes to exactly one agent.
A mechanism receives a bid profile , where is the value agent claims for each good, and outputs an allocation of all goods. A profile is a pure Nash equilibrium (PNE) if no agent can obtain a bundle of strictly larger true value by changing her bid to any other .
The class of always-EFX mechanisms (§4.2) consists of the mechanisms that, for every valuation profile on , have at least one PNE, and whose every PNE yields an EFX allocation with respect to . The class is non-empty: the paper's Mod-Cut&Choose mechanism belongs to it (Theorem 4.3).
For and every always-EFX mechanism , every valuation profile and every PNE of for that profile,
Without incentives, an EFX allocation for two agents guarantees only of the maximin share, and this is tight already for four goods (Amanatidis, Birmpas and Markakis, 2018; Theorem 2.6 of the paper). Theorem 4.5 shows that the equilibrium structure of any always-EFX mechanism closes this gap completely on four goods: strategic behaviour, rather than degrading fairness, forces the outcome from EFX up to MMS. It is the first step of the paper's separation between equilibrium EFX allocations and generic ones; Theorem 4.7, a companion mission of this series, extends it to any number of goods with an approximation factor strictly above . The authors suspect the exact statement fails for five or more goods, so the four-good case is where the full MMS guarantee is known.
The theorem is proved in the paper. To our knowledge, neither it nor its lemmas have a machine-checked proof. The mission adds the statement over an abstract class of mechanisms, quantified over all mechanisms and all non-negative bids, which is a reusable template for "every equilibrium of every mechanism in a class" results in mechanism design without money.
The theorem is about an arbitrary mechanism of which nothing is known except the two equilibrium properties of the class. The direct approach, analysing an EFX allocation of the given instance, cannot succeed on its own: Theorem 2.6 exhibits EFX allocations on four goods that miss the maximin share by a factor , and the equilibrium property for the given valuation alone does not exclude them. The argument has to use the class hypothesis on a second, auxiliary valuation profile on the same goods, and couple the equilibria of the two profiles through deviations of a single agent. The remaining difficulty is the finite case analysis on the bundles of four goods and the maximin share, which is a maximum over all two-bundle partitions.
Lean represents agents as Fin 2 and goods as Fin m (here Fin 4), both 0-based. Valuations are per-good real values v i g with the hypothesis ; bundle values are finite sums, so additivity holds by definition. A mechanism is any function from bid profiles Fin 2 → Fin 4 → ℝ to bundle assignments Fin 2 → Finset (Fin 4). The maximin share reuses the published definition LittleCharity.MMS.mms with two labelled, possibly empty bundles. The goods of the lemmas are a bijection of Fin 4 sorting agent 1's values.
The class hypothesis is the paper's in full: the mechanism allocates all goods on every non-negative bid profile, has a PNE for every non-negative valuation profile on the same four goods, and every such PNE is EFX. EFX is Definition 2.1, removing only goods the envious agent values positively; best responses range over all non-negative bid vectors; EFX and MMS are measured with the true valuations, not the bids. A formalization that restricted deviations to a subset of bids, measured EFX or MMS on bids, or used the stronger EFX that removes every good (in the hypothesis, this would weaken the theorem) would be a different and weaker statement and is excluded.
Lemma 4.6 on the page writes in its conclusion where is meant; the Lean states it for agent 1. No hypothesis beyond the page's is added.
A complete development needs finite case analysis over the partitions of four goods and the definitions above. The fairness definitions and the class of mechanisms are reusable for the companion mission on Theorem 4.7. Proofs of any milestone are welcome independently.
Community detection asks for a hidden partition of the nodes of a graph from its edges. Its simplest probabilistic benchmark is the two-community stochastic block model (SBM), in which the minimum bisection problem is the maximum a posteriori estimator. That problem is NP-hard, so convex relaxations are used in its place, and the question is when a relaxation still returns the hidden partition exactly. For semidefinite relaxations this question has sharp answers (Abbe, Bandeira, Hall 2016; Bandeira 2018). Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2) ask the same question for the most common linear programming relaxation of minimum bisection, the metric relaxation. They show that it recovers the planted bisection in very dense graphs when (their Theorem 6). This mission is their converse in the very dense and dense regimes, Theorem 7: above explicit thresholds the LP fails with high probability.
The node set is , even. A bisection is a partition with . The cut vector of has exactly when and lie on different sides. For a graph with adjacency indicators , the metric relaxation is
over , with the first family over distinct with and the second over . The LP recovers the planted bisection if is its unique optimal solution.
In the SBM a bisection is first drawn uniformly at random; then each pair on the same side is an edge with probability and each pair across with probability , independently, with . The Erdős–Rényi graph has every pair an edge with probability . The dense scaling (20) is , with , ; is the very dense regime. An event holds with high probability (w.h.p.) if its probability tends to as .
For a graph , is the shortest-path distance ( across components), is the diameter, and is the average distance. is the edge set of , the set of edges across the planted bisection.
Let , with , , and if . If one of
holds, then
Theorem 6 and Theorem 7 together bracket the success region of the metric relaxation in the very dense regime: recovery for , failure above the curve (22). In the dense regime, Theorem 7 gives explicit linear thresholds above which the LP fails. The proof reduces failure to a deterministic distance criterion (Theorem 5, posed in mission 4 of this series) and turns asymptotic distance distributions of random graphs into statements about an LP.
The results are proved in the paper, partly by citing Bollobás's diameter theorems and Shimizu's average-distance theorem; none of them has a machine-checked proof. Formalizing the mission yields, besides Theorem 7, the diameter and average distance of dense Erdős–Rényi graphs (Propositions 12 and 14) and the monotone coupling between Erdős–Rényi graphs and the SBM (Proposition 11), each of which is usable beyond this paper. The coupling and (26) are also the inputs of the logarithmic-degree result (Theorem 8, mission 7).
The deterministic half is short: once , and are pinned down, the case computations (28)–(29) reduce to inequalities between explicit expressions in , and . The difficulty is the random-graph input. The diameter of for needs the second-moment analysis of the number of pairs at distance greater than (Bollobás, Corollaries 10.11–10.12), and the average distance needs the finer limit law for path counts at the critical exponent , where the constant appears. A first-moment argument gives only one side of each estimate. Concentration of and (26) is a Hoeffding bound, but it must hold uniformly over the random planted bisection.
Nodes are Fin n and graphs SimpleGraph (Fin n). A bisection is its side with . The LP variable is a symmetric, zero-diagonal array Fin n → Fin n → ℝ, with no box constraints, so uniqueness is uniqueness over . Probabilities are finite sums over all graphs (and all bisections for the SBM). Edge probabilities are clamped into , which affects only finitely many . SBM limits run over even . Distances are in ℕ∞ and in , so disconnected samples have infinite diameter and average distance; no real truncation is used.
Disclosed choices:
Two encodings would make the statements trivial, and both are excluded. Unnormalized LP variables would make uniqueness false. Reading in via toReal would make the upper bounds hold for disconnected graphs.
The deterministic distance criterion (Theorem 5) is posed in mission 4 and is not restated. Contributions are welcome on the coupling, Hoeffding-type concentration of edge counts, and the Erdős–Rényi distance asymptotics. These are reusable for any finite random-graph development.
Fair division of indivisible goods asks how to split a set of items among agents with different values so that nobody has strong grounds to complain. Algorithms with fairness guarantees, such as Round-Robin, which always produces an allocation that is envy-free up to one good (EF1) when agents report their true additive valuations (Caragiannis et al., 2019), assume that agents report truthfully. Real agents are strategic, and truthful reporting is generally not an equilibrium of sequential allocation mechanisms (Kohler and Chandrasekaran, 1971). Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) ask instead whether the outcomes of a mechanism's pure Nash equilibria are fair. For that question to be meaningful, equilibria must exist.
Timeline.
An instance is a triple : a set of agents, a set of goods, and for every agent a non-negative value for every good . Valuations are additive: . Zero values and ties are allowed. All goods must be allocated.
Agents do not report . Each agent submits a bid , and a mechanism maps the bid profile to an allocation. In Round-Robin (Mechanism 1) the agents take turns in the order . At each turn the active agent receives the still-available good with the largest bid. Ties are broken lexicographically: beats for agent if , or if and has the smaller index.
A bid is a best response to if for every . A profile is a pure Nash equilibrium (PNE) if every agent's bid is a best response (Definition 2.7). The mechanism reads only bids. The bundles are judged with the true values.
For every instance with non-negative additive valuations,
Theorem A.3 is half of the paper's headline result for Round-Robin. Theorem 3.3 says that every PNE is EF1 with respect to the true valuations, and Theorem A.3 says that a PNE always exists. Together they show that a designer using Round-Robin gets EF1 outcomes at equilibrium on every additive instance, not only on strict ones. Without existence, the fairness of equilibria would be vacuous on the instances with ties or zero values, which arise naturally (indifferent agents, worthless goods).
The result is proved in the paper, modulo the cited Theorem A.2. As far as is known, none of it is machine-checked. A complete formalization would check the bluff-profile equilibrium of Aziz et al. for bid-based Round-Robin with lexicographic tie-breaking and deviations over all real bid vectors. It would also repair a gap in the perturbation argument. The page measures the perturbation against the smallest difference between two goods, which does not bound the difference between two bundles (values : the good gap is , but and differ by ). The milestones use the bundle-level gap, which makes the argument go through.
The obstacle is Theorem A.2. Truthful bidding is not an equilibrium: on page 7 of the paper, with two agents and three goods, agent 1 gains by bidding for a good that agent 2 would otherwise take first. So an equilibrium must be constructed, and verifying it requires bounding the value of every deviation of every agent. A deviation changes the order in which all later goods are taken, so its effect is not local. The equilibrium property quantifies over a continuum of real bid vectors. Reducing to strict positive valuations also requires care: a perturbation that is small for each good can still reverse a comparison between two bundles.
Agents are Fin n with [NeZero n], goods are Fin m, both 0-based. Values are v : Fin n → Fin m → ℝ with 0 ≤ v i g, and val v i S is the sum over S. Bids are non-negative real vectors. IsPNE mech v b requires every bid to be non-negative and every agent's bid to be a best response against all non-negative deviations, with bundle values computed from the true v.
Round-Robin is computed step by step. rank c sorts goods by non-increasing bid with a stable sort, which implements the lexicographic tie-breaking. rrFrom s G runs Round-Robin from start agent s on goods G. The goal uses only roundRobin = rrFrom 0 univ (Mechanism 1). goodGap is the page's , and bundleGap is the repaired one used in milestones 2–3.
The goal has no positivity or injectivity hypothesis. Several statements would trivialize it and are excluded: an equilibrium over rankings or over a finite menu of bids instead of all of ; bundle values measured on bids instead of true values; and Round-Robin with arbitrary rather than lexicographic tie-breaking, which would change the mechanism.
Needed infrastructure: the run of Round-Robin as a function of rankings, invariance of the allocation under bid changes that preserve the ranking, and the bluff-profile construction. These are reusable for any sequential allocation mechanism. The equilibrium-transfer milestone holds for any mechanism and is elementary. Lemma A.1 (a strict perturbation preserving best responses, p. 23) is formalized in the companion mission on EF1 equilibria. Contributions of the infrastructure above, of a proof of Theorem A.2, and of alternative existence proofs are welcome.
The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability , and edges across with probability . The task of exact recovery is to identify the hidden halves from the graph alone.
The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.
Let with even. A bisection is a partition with . For a graph let if and otherwise. The metric relaxation (LP-P) is
the first constraint for all distinct with , the second for all , and . The cut vector of a bisection has for on the same side and otherwise. (LP-P) recovers the planted bisection when is its unique optimal solution.
In the Erdős–Rényi model every pair of nodes is an edge independently with probability . In the SBM a bisection is first chosen uniformly at random; then pairs inside or inside are edges with probability , pairs between them with probability , all independently. is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to as . The graph is very dense when and are constants.
For a finite graph and , a -factor (or -factor) is a set with exactly edges of at each node ; counts edges with one endpoint in and one in ; , are the minimum and maximum degrees; and the node connectivity is the minimum number of nodes whose deletion disconnects (the number of nodes, for a complete graph).
For constants ,
The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with ), is the goal of mission 3 of this series and is not restated here.
The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant , but not up to the threshold that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.
Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the -factor criterion for bipartite graphs, Tutte's -factor theorem (Mathlib has only the perfect-matching case ), and the Bollobás–Thomason theorem for random graphs, together with degree concentration for and the bipartite SBM. Each is reusable well beyond this paper.
The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's -factor theorem and the bipartite -factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.
Nodes are Fin n (0-based). A bisection is a Finset with . Points of are symmetric arrays with zero diagonal; (LP-P) has no box constraints (they are implied by the constraints and adding them would change the LP). Recovery means: is optimal and every optimal solution equals .
The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into , which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along for the SBM. The standing assumption is not built into the law, so that is the case .
Disclosed readings: the printed of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree and Proposition 4 with , the least even integer (the proof assumes even). as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on .
A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.
Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.
A firm with open positions often cannot interview and offer sequentially: hiring seasons are short, and offers go out in one batch. Some recipients decline, so the firm overbooks, sending more offers than it has positions, and pays for every hire beyond capacity. The same trade-off appears in airline and hotel overbooking and in university admissions. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study this Simultaneous Offering problem as one of three hiring-pipeline models, and analyse the natural class of value-ordered policies, which offer to the best candidates first. Their Theorem 3 shows that a value-ordered policy built from a linear-programming relaxation guarantees a fraction of the optimum when every value is at least . This mission formalizes the converse, Theorem 4: no value-ordered policy can guarantee more than .
An instance has positions and candidates. Candidate accepts an offer with probability , independently of the others, and then adds value . The firm chooses a set of candidates and sends all offers at once. If is the random set of acceptances, the reward is
so each hire beyond capacity costs (the paper rescales values so that this cost is ). Write for the expected reward of offering to , and for the best expected reward; randomizing over offer sets cannot do better.
Candidates are labelled so that . A value-ordered policy with parameter offers to . An instance is -bounded, , if for all . Without such a bound value-ordered policies can be arbitrarily poor (§6.1); measures how soft the capacity is, from nearly hard ( close to ) to nearly compensated by any hire ( close to ), and both theorems take .
For let be the mean of a Poisson variable truncated at , and
In Lean these are SimInstance, reward, OPTsim, valueOrdered, TauBounded, expMinPois, ratioObj, alpha and beta in the namespace HiringLP.SimUpper.
For every , and there is a valid, sorted instance with positions such that
The instance has type-1 candidates with , , , and type-2 candidates with , . With and :
Proposition EC.5: optimal , exist, , and . Proposition EC.6: if and only if , which holds whenever .
Theorem 4 bounds what any value-ordered policy can guarantee on -bounded instances, against the true optimum rather than an LP relaxation. With Theorem 3 it brackets the best guarantee of the class between and , and by Proposition EC.6 the two coincide when , in particular for all when . In that region the paper's truncated-LP policy is the best value-ordered policy in the worst case. The instance also shows why the restriction to value-ordered policies costs something: the optimum offers to the reliable type-2 candidates, while a value-ordered policy must first exhaust the slightly more valuable unreliable ones.
The results are proved in the paper. None of them has a machine-checked proof; this mission produces a formal version of Theorem 4 and the finite- estimates on which its proof rests, together with a reusable finite-sum encoding of independent acceptances, truncated Poisson and Binomial expectations, and the constants , .
The milestones are exact identities and inequalities at a fixed ; the hard part is the passage to the limit. The page's proof lets with and replaces by . The goal, however, asks for one finite instance on which the bound holds for every simultaneously, including of order and the values that also offer to type-2 candidates. A pointwise limit for each fixed does not give this; the Binomial–Poisson error has to be controlled uniformly in , and the error must fit inside the slack , part of which the term already uses. Note also that the comparison runs the wrong way for the obvious argument: is concave and the Binomial is less spread than the Poisson, so is at least its Poisson counterpart and a one-sided comparison cannot replace an approximation bound.
All randomness is finite. The expected reward is an explicit sum over the accepting sets with product probabilities; the Binomial pmf, its truncated mean and its tail are finite sums written by hand. The truncated Poisson mean is the series with the Poisson pmf. All quantities are real. Candidates are Fin n, so the paper's candidate is index ; sortedness is the hypothesis Antitone v in Valid, which also contains , and . is the maximum over all offer sets, never over value-ordered ones. is the supremum over and over . The page leaves implicit in ; the goal quantifies over every and requires the instance to have exactly positions. The quantifiers are "for all , there is an instance, for all ".
The goal does not fix the hard instance: any instance proves it. A formalization in which the comparison is with the best value-ordered policy, in which is a free parameter, or in which the reward is defined by the proof's Binomial formula would be a different statement and is ruled out by the definitions above. The definitions are not specialized to the hard instance, which appears only as a separate definition used by the milestones.
A complete development needs: finite sums over subsets with product weights and the reduction to a Binomial count for identical candidates; summability and continuity of the truncated Poisson mean; a Binomial–Poisson approximation bound uniform in the number of trials; concavity of in . The Poisson and Binomial infrastructure is reusable well beyond this mission. Proofs of the milestones, of the companions, and of auxiliary approximation lemmas are all welcome.
Payment channels let two parties make repeated transfers while using an on-chain transaction only when a channel needs resetting. They require funds to be committed in advance. The economic choice is therefore between the transaction fees saved by using a channel and the opportunity cost of funds tied up in it. Guasoni, Huberman, and Shikhelman give a stochastic cost model in which this tradeoff can be compared for one-way and two-way payment streams (Guasoni et al., 2023, §§1 and 3). Their small-discount-rate result makes the difference between the two arrangements quantitative: the optimal one-way cost grows like , while the optimal symmetric two-way cost grows like .
The paper was published online in Management Science on November 6, 2023. This mission concerns Theorem 3(i)–(ii) in that published version, especially the cost expansion (8). The paper proves these asymptotic claims; the task here is to state them precisely in Lean and develop machine-checked proofs of the stated cost laws.
Two nodes exchange unit payments. Payments from node 1 to node 2 arrive at rate , and payments in the reverse direction arrive at rate . Each payment stream is a Poisson process, and the streams are independent. The continuously compounded discount rate measures the opportunity cost of committed capital. A channel reset costs , while an on-chain payment costs . Node 1 commits and node 2 commits . The channel balance moves by one unit at each payment; at a boundary, a reset replenishes it (Guasoni et al., 2023, §§1.1, 3.1 and 5).
The paper's closed-form bidirectional cost is given in equations (3)–(4). It uses two characteristic roots and , determined by the payment rates and . This mission uses the formula at equal rates . A separate unidirectional cost from equation (1) describes a stream in only one direction. Its optimizing size is denoted below. The exact channel model has integer balance states; the paper optimizes the closed forms over positive real channel sizes in its asymptotic analysis.
Write for the infimum of the unidirectional cost over , and for the infimum of the symmetric bidirectional cost over . These are functions of and as well as of ; the compact paper notation suppresses those arguments. The term has its usual uniform meaning as with and fixed: its absolute value is at most a constant times for all sufficiently small positive .
Theorem 3(i), equation (7), states
The same part states that an optimal size is . The mission records that size claim using the explicit optimizer displayed after equation (2) (Guasoni et al., 2023, pp. 6–7).
The mission's goal is the cost clause of Theorem 3(ii), equation (8):
This includes the constant correction and a two-sided error estimate of order . The theorem also states that optimal commitments are equal and each has size . That separate size clause is outside this proposal; the goal does not assert the existence or location of a minimizing pair (Guasoni et al., 2023, p. 7).
The different exponents distinguish the two designs even when both can make frequent off-chain payments. At small , the model's optimal symmetric bidirectional cost grows more slowly than its optimal unidirectional cost. The formulas also retain the next constant term, allowing a comparison beyond the leading growth rates. The paper relates this difference to the amount of capital that must be committed by the participants (Guasoni et al., 2023, p. 7).
A formal proof would connect the exact channel-cost formulas, a two-variable infimum, the diagonal specialization, bounds on the hyperbolic cosecant, and real asymptotics in one reusable development. The supporting statements are useful separately: the root expansion concerns a quadratic characteristic equation, and the diagonal reduction concerns a symmetric optimization problem. The paper supplies proofs of the mathematical results; the remaining work is their faithful machine-checked formalization.
The cost depends on and on sizes that grow without bound as approaches zero. An expansion valid for each fixed size does not by itself justify substituting a size that varies with . The target asks for a uniform remainder at the infimum, including its constant term. The cost must be controlled from both sides over every admissible positive size; evaluating one promising size supplies only one side of that comparison. The paper's proof of Theorem 3 uses formal small- expansions of the cost and first-order conditions, and the stated error rate calls for care when these are applied to moving optimizers (Guasoni et al., 2023, pp. 11–12).
The Lean definitions reproduce equations (1), (3), and (4). The one-way and two-way costs are separate functions, matching the paper's separate treatment of the unidirectional boundary case. Real powers are used for the real-size optimization; the balance lattice in the exact stochastic model uses integer sizes. Both optimal costs are infima over strictly positive real sizes. The symmetric infimum is not defined by choosing a particular size or by assuming that the minimum is attained. All rates in the asymptotic theorems satisfy , the reset cost satisfies , and the filter sends to zero through positive values. Consequently a Big-O constant may depend on and but cannot depend on .
The on-chain costs for one stream and for two equal streams supply the paper's economic comparison, although does not occur in this mission's cost goal. The diagonal milestone omits that on-chain term because it is constant in the channel sizes; it states a midpoint cost inequality so no minimizer is assumed. The proof's root expansion is recorded for both and . The paper's assertion that the symmetric minimizing sizes equal is explicitly omitted. The development does not fix a numerical value of , permit an -dependent Big-O constant, drop the term, or replace the infimum by cost at a chosen size.
The mission needs real-power identities, properties of and , nonempty bounded-below cost sets, infimum estimates, and Mathlib's Asymptotics.IsBigO on the positive-side neighborhood of zero. Results about real asymptotics and symmetric minimization can be reused beyond this channel model. Contributions proving the cost milestones, the root expansion, the diagonal inequality, and the goal are all within scope.
Climate impact investing refers to investors who tilt their portfolios away from companies with large greenhouse-gas emissions. Its stated aim goes beyond aligning portfolios with values: by raising the cost of capital of polluting companies, it is meant to change what those companies do. De Angelis, Tankov and Zerbib (SSRN 3562534, published in Management Science, 2022, doi:10.1287/mnsc.2022.4472) build an equilibrium model in which this mechanism can be computed. Green investors penalize the expected climate externalities of companies. Companies choose emission schedules to maximize their market value net of abatement costs. Prices, portfolios and emissions are determined jointly.
Section 4 of the paper asks what happens when the green investors are uncertain about future climate externalities, for instance because news on climate risk or regulation arrives in rare large shocks. Its answer is that, in the most common market configuration, more uncertainty makes green investors hedge by holding more brown assets, which weakens the incentive to abate, so that equilibrium emissions rise as climate uncertainty grows. This mission formalizes that result and the chain of statements behind it.
Fix a date in a horizon ; every object below is evaluated at that date, and its subscript is dropped where harmless. There are companies, indexed by , with asset covariance matrix (positive definite). Green investors hold wealth share , regular investors the rest, with risk aversions .
Company emits at rate and pays the marginal abatement cost . The green investors attach to company the climate externality , the companies use , and all 's are positive. With a rate of time preference , the time factors are and .
Climate uncertainty is a Poisson process of intensity : a smaller means rarer, larger shocks, i.e. more uncertainty. For a fixed externality vector , the equilibrium of Proposition 5 is described by a scalar solving
and the green portfolio is . Without uncertainty, and the portfolio is . When the companies take as given (the large-market assumption), company 's optimal emission rate is
and itself must then solve the fixed-point equation , where
Its solution is . Finally, is the schedule without uncertainty.
Assume condition (24) at the date : for all and all . Let solve the fixed-point equation. Then the sign of the green portfolio's externality without uncertainty decides the direction of the response:
the opposite if , and with unchanged emissions if it is .
In the order of the attack:
Companion statements cover Proposition 6(i) (the green portfolio's market risk increases in ), Lemma 1, and the algebraic core of Proposition 5.
The result. Proposition 8(iii) is the paper's headline claim about uncertainty, and it is quoted in its abstract: uncertainty about future climate externalities, by making green investors hedge, can push companies to increase their emissions. The paper's Lemma 1 shows that the positive case, a green portfolio with positive climate externality, is the common one. The sign condition is therefore not a curiosity. It separates markets where uncertainty undermines impact investing from markets where it strengthens it.
Formalizing it. The proofs in the appendix are short and leave several steps implicit, and in two places the printed formulas do not match their own derivation (see the scope section). A machine-checked version settles the precise hypotheses under which the comparative statics hold. It also provides reusable statements about scalar fixed-point equations of the form with nondecreasing . No part of this paper has been formalized before.
At a fixed schedule, everything follows from the fact that is affine and nondecreasing in . Once the schedule is endogenous, is nonlinear and in general not monotone, so neither uniqueness nor monotonicity in comes for free. The work lies in turning condition (24) into monotonicity of . That requires differentiating the quadratic form through the schedule and controlling its sign company by company. The limit as needs bounds on along the solution path rather than the formal Taylor expansion in the paper gives for (20).
The stochastic layer is not formalized: Brownian cash-flow news, subjective measures built by Girsanov's theorem, CARA utility maximization, the Poisson process of climate shocks, and Propositions 1 and 5 as equilibrium statements. The statements start from the objects the proofs start from: the first-order and market-clearing system (45), and equations (20), (22) and (23). Everything is stated at one fixed date , with vectors in indexed by Fin n, positive definite and Mathlib's matrix inverse.
The standing assumptions are hypotheses of the statements:
The relation is assumed only where it is used, in the core of Proposition 5. The solution maps and enter only through the hypothesis that each value solves its equation. A theorem that assumed monotonicity of , uniqueness, or the sign of would trivialize the goal; the goal assumes only condition (24).
Disclosed corrections of the printed text:
Two readings are fixed. "Monotonically increasing" for is strict. The emission response is weak, because at the schedule does not depend on . "Reallocate towards brown assets" means that the green portfolio's climate externality falls as falls.
The development needs elementary real analysis: the intermediate value theorem on , monotonicity from derivatives, and limits at infinity. It also needs finite-dimensional linear algebra for positive definite matrices. The lemmas about are reusable beyond this mission. Proofs of the companion statements, which are algebraic, are welcome as warm-ups.
The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) prepares a parametrized quantum state whose measurement yields a candidate solution of a combinatorial optimization problem. Its level-one version alternates a single phase operator and a single mixing operator and is simple enough to analyse by hand. In arXiv:1412.6062 the same authors applied it to Max E3LIN2 with bounded occurrence: given linear equations mod 2, each on exactly three bits, with every bit in at most equations, satisfy as many equations as possible. A uniformly random string satisfies half of them in expectation; the question is by how much an algorithm can beat .
Without the occurrence bound no efficient algorithm achieves unless P = NP (Håstad, J. ACM 2001). With every bit in at most equations the history, as recounted on pp. 2–3 of the paper, is:
Section III, formalized here, studies the typical case: it fixes the triples and draws the right-hand sides at random, and shows that the QAOA then reaches an advantage of order , the order of the classical algorithm, on all but a vanishing fraction of the instances.
An instance on bits with equations is a list of triples with , no triple repeated, together with right-hand sides ; equation is . The instance has occurrence at most if every bit lies in at most triples. Write and ; equation is satisfied by exactly when .
Let be the number of equations satisfied by , viewed as a diagonal operator on the -dimensional space spanned by , let , and let be the uniform superposition. For angles the level-one QAOA state is
Measuring it in the computational basis gives a string; is the expected number of satisfied equations.
In Section III the triples are fixed and the instance is drawn uniformly from the choices of right-hand sides; and denote the mean and variance over this choice. The mixing angle is and the state analysed is , following the paper's sign convention.
For an equation with bits , the polynomial collects the equations that share exactly the bit with it, and is its number of terms.
For every E3LIN2 family of triples with occurrence at most , every and every ,
With and fixed, all but a fraction of the instances reach . This is the paper's closing sentence of Section III with an explicit failure probability.
The result shows that on random-sign instances with any fixed bounded-occurrence structure, a single layer of QAOA beats a random assignment by , the same order as the best known classical guarantee and better than the paper's own worst-case bound by a logarithmic factor. It was one of the first concrete performance statements for the QAOA on a problem where its advantage over random guessing could be compared with the best classical guarantee. The average-case technique, an exact single-clause formula followed by an average over independent signs and a dependency count, applies to other local constraint problems.
The statements are proved in the paper by hand; none of them, and no QAOA performance bound, has a machine-checked proof on the platform. The mission produces a verified link from the quantum state to a classical average (25), a finite second-moment method over sign vectors, and an explicit Chebyshev form of the concentration claim.
The central step is (25): turning the expectation of in the state into a classical average over bits. It requires conjugating three Pauli operators through the mixer at , expanding the phase operator around the three bits, and showing that equations sharing two bits with the clause cancel. A direct computation in the -dimensional space does not scale with and does not give a closed form.
For the variance, the naive bound by pairs gives nothing. The argument needs exact independence of clause terms whose sign dependencies are disjoint, which rests on (25) showing that each term depends only on its own sign and on the signs of the equations sharing exactly one bit with it, and then a combinatorial count of linked pairs.
Bit strings are Fin n → Bool with true the bit ; the quantum layer reuses the published QAlgorithms definitions (Qubits, act, prob, uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary). The phase operator is the full count of satisfied equations, which differs from the paper's of (6) by the constant ; the resulting states differ by a global phase and all probabilities agree. Triples are strictly increasing and pairwise distinct, which encodes "exactly three variables" and . is a natural number. is the uniform average over all right-hand-side vectors, over all strings.
Two pins are disclosed. The angle range is added to (50) and the goal, since the lower bound needs . The goal's threshold is (50)'s exact lower bound, not the paper's (54): is the large- limit and is false at every finite , so (51)–(53) are stated as a limit instead. The goal is about the expected satisfied count of the measured state; the sampling procedure, circuit size and the search over are out of scope.
A trivializing reading is excluded: the probability is over the instances on the fixed triples, not over a single instance, and the bound is about the quantum expectation at (at the mean has the opposite sign and the statement would be false).
A complete development needs finite averages over with independence of coordinates, the single-clause formula (25) in the -dimensional Hilbert space, and Chebyshev's inequality on a finite uniform space. The (25) computation and the second-moment count are reusable for other QAOA analyses. Contributions to any milestone are welcome, in any order.
The joint replenishment problem (JRP) is a basic model of inventory coordination: several items are ordered from one supplier, each item pays its own ordering and holding costs, and an additional item-independent joint ordering cost rewards ordering the items at common times. Two accounting conventions are studied. In the periodic JRP (also called the general integer model; see the survey of Goyal and Satir, 1989) the joint cost is charged at every point of a common grid, whether or not an item is ordered there; in the aperiodic JRP it is charged only at actual order times.
For decades the literature produced heuristics and enumerative algorithms for the JRP without a polynomial-time exact algorithm and without evidence that none exists. Schulz and Telha (arXiv:2007.09045v1; published in Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard) showed that already the two-item problem is at least as hard as integer factorization, in both variants. For the periodic JRP the paper notes (p. 10): "No hardness results were previously known for the periodic JRP."
Timeline, as recorded in the paper (pp. 4–5):
An item with ordering cost and holding cost , replenished every time units, where is a positive integer, has the EOQ cost
In the two-item periodic JRP, item has parameters and an integer period , and a joint ordering cost is incurred every time units, where divides both periods. At an optimum , and the problem is to minimize objective (3) of the paper,
An optimal solution is a pair of positive integers whose value is at most the value of every pair of positive integers.
Given a natural number , the instance of Lemma 2 is
with objective written and item 2's cost . Fixing leaves the single-variable problem (4):
An odd composite number is an odd integer that is not prime.
For every odd composite : the coefficients of the instance above satisfy and are natural numbers at most ; the instance has an optimal solution; and every optimal solution satisfies
The goal does not say which non-trivial divisor is: optimal solutions need not be unique (for both and are optimal).
The result. Lemma 2 says that an exact solver for the two-item periodic JRP, applied to an instance whose coefficients have size , returns a pair from which a non-trivial divisor of is read off as . Repeating on the factors yields the full factorization, so a polynomial-time algorithm for the two-item periodic JRP would give a polynomial-time algorithm for integer factorization (Theorem 1(b), p. 12). Since the security of RSA-type cryptosystems rests on the belief that factoring is hard, the lemma explains why exact algorithms for even two items have not been found. Section 3 of the paper extends the same construction to a reduction from a range-divisor problem that is NP-complete under randomized reductions, assuming the Riemann hypothesis; that extension is a separate mission of this series.
Formalizing it. The result is proved in the paper, and the proof is short. To our knowledge it has no machine-checked proof. This mission produces a Lean statement of the reduction's correctness with the explicit instance, and its proof together with the intermediate steps of the paper's argument. One printed step needs a correction (milestone 4, see below), which a machine-checked proof makes explicit.
Two points need care. First, the claim concerns every optimal solution of a problem over all pairs of positive integers, so it needs both a global lower bound for every pair with and the existence of an optimum, which the paper does not state: the objective must be shown to attain its infimum over an infinite discrete domain. Second, the step separating non-trivial from trivial greatest common divisors depends on a divisor of a specific size: the printed claim "a non-trivial divisor with " is false for , whose only non-trivial divisor is . The corrected bound still gives the value that the argument needs, but only because for every odd composite . A direct convexity argument for item 2 alone does not finish the proof: item 1's cost and the joint cost interact through , which is not convex in either variable.
This mission formalizes the correctness of the reduction behind Theorem 1(b); polynomial running time is not formalized. Theorem 1(b) itself, the recursion that turns one divisor into a full factorization, primality testing, and the treatment of even (p. 10) are not stated.
Conventions committed to:
Odd M ∧ 1 < M ∧ ¬ M.Prime.Disclosed differences from the printed lemma: the goal names the explicit instance of the proof's first sentence instead of "there is an instance" (a stronger statement); it adds the existence of an optimal solution, so that "every optimal solution satisfies …" is not vacuous; and milestone 4 uses in place of the printed . Milestones 1–3 and 6 are stated for every with (or every ), which contains the paper's case. A formalization with an existential instance, an unattained or empty set of optima, or periods allowed to be would make the goal trivial or wrong; all three are excluded.
Infrastructure: the definitions (EOQ cost, objective (3), optimality over positive integer pairs) are short and local to this mission; the same objects appear in the companion missions of this series under their own namespaces. Mathlib supplies Nat.gcd, Nat.minFac and Nat.minFac_sq_le_self. Proofs of any milestone are welcome independently; the existence of an optimum is the one ingredient not present among the milestones.
The minimum bisection problem asks, for a graph on an even number of vertices, for a split of into two halves of size that cuts as few edges as possible. It is NP-hard, and it is also the maximum a posteriori estimator for the two-community stochastic block model, the standard random model of networks with community structure. A tractable surrogate is a convex relaxation. Semidefinite relaxations of minimum bisection are known to recover a planted community structure under near-optimal conditions; Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) ask the same question for the cheaper and more classical linear programming relaxation, the metric relaxation obtained by outer-approximating the cut polytope by triangle inequalities.
This mission covers the deterministic, sufficient side of their analysis (§3.1 of the paper): explicit conditions on a graph with a planted bisection under which the LP relaxation returns exactly that bisection. These conditions are the input to the paper's probabilistic recovery theorem for the very dense block model (Theorem 6).
Let . A bisection is a partition of with . A fixed but unknown bisection is the planted bisection. Write and for the subgraphs induced on the two sides, and for the bipartite graph of the edges with one end on each side. Two degree parameters describe the instance: , a degree inside the communities, and , a degree across them. A graph is -regular if every vertex has exactly neighbours.
The cut vector of the planted bisection has for on the same side and otherwise. With if and otherwise, and the convention , the metric relaxation is
The LP recovers the planted bisection if is an optimal solution and the only one.
Assume and contain -regular subgraphs on the same node sets, and is a subgraph of a -regular bipartite graph with the same bipartition. Then
Theorem 4 is a deterministic certificate: any graph that can be sandwiched between a regular within-community graph and a regular across-community graph with a degree gap of is solved exactly by a polynomial-size LP. For regular instances the threshold is tight: for and any in range, the paper's Theorem 2 constructs regular graphs on which even the exact minimum bisection fails to recover the planted bisection. The sandwich form is what makes the result usable for random graphs: the paper's Theorem 6 shows that in the very dense block model with constant edge probabilities and the sandwich hypotheses hold with high probability, so the LP recovers the communities.
None of these statements has, to our knowledge, a machine-checked proof. A complete development gives a verified dual certificate for the metric polytope, a verified version of Mangasarian's uniqueness criterion for linear programs in the general form , (useful well beyond this paper), and the monotonicity lemmas that transfer LP recovery between graphs.
Optimality of (Proposition 1) needs an explicit dual solution of (LP-P), with one multiplier per triangle inequality, and the bookkeeping that verifies the dual equality constraint for every pair in six cases. Optimality alone is not recovery: the obvious argument, exhibiting a dual solution, says nothing about other optima, and the LP has many fractional feasible points. Uniqueness requires a strictly complementary structure and a separate argument that the linear system attached to the active constraints has only the zero solution; on the page this step uses Dirac's theorem on Hamiltonian cycles inside each community. Finally, the passage from regular to sandwiched graphs is not a perturbation statement: adding or deleting edges changes the objective, and the lemmas rely on the bounds , which are implied by the triangle inequalities rather than imposed.
Vertices are Fin n (0-based), a graph is a SimpleGraph (Fin n), and a bisection is a finset V1 with 2 * V1.card = n; the other side is its complement. A point of is an array x : Fin n → Fin n → ℝ that is symmetric with zero diagonal, and these two conditions are part of LP feasibility. Recovery is optimality of the cut vector together with equality of every optimal solution to it. Regularity of and with one common degree is "every vertex has exactly neighbours on its own side"; regularity of is "every vertex has exactly neighbours on the other side". Degree conditions are compared in .
Committed readings:
Two encodings would trivialize the mission and are ruled out: an array without symmetry and zero diagonal (its unconstrained entries make uniqueness false), and an LP with added box constraints (a different polytope). Dirac's theorem, used inside the proof of Proposition 2, is posed separately on the platform (AppliedComb.Graphs.dirac) and is not restated here. Contributions welcome: the dual certificate of Proposition 1, a general-purpose proof of Theorem 3 from LP duality, and the two monotonicity lemmas.
Two firms developing competing innovations face a decision that a single firm does not: a rival's discovery can end the value of continuing the project. If the first discovery wins the payoff, each firm chooses how much to spend per period while knowing that greater spending may change both its payoff on success and its speed of discovery. The investment decision therefore depends on what the rival chooses. Danmo Lin's model separates these two channels and asks when competition itself raises a firm's chosen R&D intensity Lin (2022).
This mission concerns the paper's race of two financially unconstrained firms. The result is a comparative statics claim about a firm's best response to its rival, together with existence of a symmetric pure-strategy equilibrium. The paper proves the result in Appendix A.6. The problem here is to give machine-checked statements and ultimately a proof for the same stochastic race, including its strategy ranges and first-arrival payoffs.
Firm chooses a fixed investment intensity , the amount it pays per unit time while the race continues. Its technology has parameters . If it discovers first, its mean project payoff is . Its discovery time is exponentially distributed with rate . The discovery times are independent, represented by the product law , and the earlier discovery wins. Both firms stop paying at . The loser receives no discovery payoff. Future cash flows are discounted at rate Lin (2022), §3.1.
The technology conditions are , , and . A project is scalable when its discovery payoff increases with investment, corresponding here to . It is accelerable when investment increases its discovery rate, corresponding to . The model permits the two firms' parameters to differ. The lower intensity is ; the upper intensity is . The standing condition makes a nondegenerate range in which investment takes place Lin (2022), (2), (7).
Write for Firm 's expected discounted payoff from the first-arrival race. Its best-response set contains every maximizer of over its own fixed interval , holding the rival's intensity fixed. A pure Nash equilibrium is a pair in which each intensity belongs to that firm's best-response set. This set-valued definition keeps the claim meaningful when there is more than one maximizer.
The first milestone identifies each expected payoff with the closed form in Lemma 2:
The second milestone is the Appendix A.6 cross-partial identity. For Firm 1, the expression equals . It is strictly positive when both discovery rates rise with intensity and Firm 1's project surplus is nonzero Lin (2022), (A.27)–(A.28).
The goal is Proposition 3. When both projects are accelerable, higher rival investment orders the best-response sets upward, with strict movement for an old response above . When neither project is accelerable, the best-response sets are constant in the rival's intensity. For identical firms, the theorem asserts a symmetric pure Nash equilibrium:
Best-response sets are required to be nonempty for every positive rival intensity. The ordering statements therefore make substantive claims about actual choices Lin (2022), Proposition 3.
The result distinguishes a change in the timing of innovation from a change in its eventual payoff. In an accelerable project, a rival who spends more discovers faster, and the firm's optimal investment response moves upward. If investment cannot affect discovery speed, a rival's intensity does not alter the firm's best-response set in this model. The equilibrium clause says the symmetric game has at least one profile at which neither firm gains by changing its own intensity. These are statements about competition's effect on project spending, rather than only about the numerical value of a firm Lin (2022), §3.1.
The mathematical result is proved in the paper; the mission seeks a Lean formalization of that known result. The expectation-to-value identity requires a reusable treatment of independent exponential discovery times and discounted spending stopped at the first arrival. The best-response statement then supplies a precise set-valued comparative statics target. A verified development of these ingredients could be reused for other innovation races and first-arrival games. This mission does not claim that such a machine-checked proof already exists.
The payoff is an expectation over two random times, with the prize awarded only to the earlier discovery and spending stopped at their minimum. The closed form must agree with that stochastic expression for each positive pair of intensities. The comparison of best responses involves all maximizers, including possible ties and boundary choices. A derivative of one selected optimizer is not a well-defined substitute when the optimizer is set-valued; moreover, strict response cannot be demanded at the lower endpoint. Equilibrium existence must hold for the same best-response correspondence that defines the competitive race. These points make a direct translation of the paper's derivative notation insufficient Lin (2022), Appendix A.5–A.6.
Lean uses real intensities, real technology parameters, Real.rpow for the power functions, and ProbabilityTheory.expMeasure for each discovery time. Their product measure encodes independence. Firm 1's discovery time is the first coordinate throughout, including Firm 2's payoff. The two firms have separate technology records. A best response maximizes the expectation from (8) over the own interval ; that interval never depends on the rival's action. The named closed form is separate from the expectation and appears in the Appendix A.6 milestone. The random payoff on discovery is represented by its mean , as the paper's calculation uses only that mean. The other cash-flow component of the underlying firm value is independent of the R&D choice and is omitted from the race payoff.
The hypotheses , , and positive intensities are explicit. The comparison allows any positive rival intensity, while each firm's own maximization uses (7). The paper's derivative claims about are posed as orderings of complete best-response sets; strictness is asserted for an old response above . Both firms must be accelerable for the increasing-response clause, and the symmetric equilibrium clause applies to identical technologies. The strict inequality in (A.28) includes the necessary nonzero-surplus condition, since its square vanishes at the upper endpoint. These choices and the printed endpoint issue are recorded in the mission's moderation notes.
The target excludes empty best-response sets, rival-dependent feasible ranges, payoffs defined by the closed form (9), an equilibrium asserted without mutual best-response membership, and comparisons that discard the strict interior part. A complete development will need integration and exponential-distribution facts, continuity and maximizer existence on compact intervals, ordered best-response sets, and a fixed-point argument for the symmetric correspondence. The first-arrival probability and integration results can be reused beyond this paper; contributions to those interfaces and to the two stated milestones are welcome.
Two-sided platforms for dating, freelancing and housing do more than list participants: they decide whom each participant is shown. When search is costly and agents leave the market over time, the platform's choice of assortments (which types of agents meet which, and how often) determines who matches, and agents respond strategically by deciding which matches to accept. A platform that ignores those responses can design meetings that agents then decline.
Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search in a stationary flow economy and ask how much welfare a platform can secure when it controls only meetings, while agents retain the decision to accept. Computing the optimal assortments is NP-hard to approximate within 24/23 (their Theorem 4.2), so the relevant question is whether a constant fraction of the best conceivable welfare is reachable at all. Their Theorem 4.1 answers it with the factor 4, measured against the platform's first best, a benchmark in which the platform also dictates acceptance.
The mission formalizes the existence part of Theorem 4.1 and the chain of results in §4 of the paper that leads to it.
There are finitely many types on two sides, a set and a set ; write and let denote a generic type on the side opposite to . Agents of type enter at rate and each agent leaves unmatched at rate . When an agent of type meets one of type , both observe one symmetric utility drawn from a law on with no atoms and finite mean; they match, and leave with utility each, if both accept.
The platform picks an assortment for each type: type meets type at rate . Agents use thresholds and accept exactly when , so a pair matches when . With population masses and matching rates , the assortments induce a stationary equilibrium when, for every type,
These are constraints (6a)–(6f) of the paper; the last one, (6e), says each threshold equals the type's expected utility, which is the agents' best response. The welfare is the flow of realized utility,
The first-best relaxation (§4.1) drops (6e) and replaces by a free pairwise threshold : the platform chooses both the meetings and which matches happen. Its welfare is the same expression with .
For every market satisfying the standing assumptions there are assortments, thresholds, rates and masses satisfying (6a)–(6f) such that, for every first-best feasible candidate ,
Theorem 4.1 is a price-of-anarchy statement for platform design: restricting the platform to meetings, and letting agents choose acceptance selfishly, costs at most a factor 4 against a platform that dictates everything. Since every equilibrium candidate is also a first-best candidate with the same welfare, it gives a 4-approximation to the optimal directed search as well. The construction behind it has a structure that is itself informative: the equilibrium consists of disjoint submarkets in each of which one side has a single type.
The results are proved in the paper; none of them has a machine-checked proof in Lean or another proof assistant on record. Formalizing them yields a checked model of stationary search markets with threshold play, a checked reduction of the first best to a generalized assignment LP, and two graph lemmas (forest support of LP optima, the star-forest halving) that recur in rounding arguments for generalized assignment and budgeted allocation.
The first best is easy to reach once Proposition 4.4 linearizes it; the obstacle is incentives. Turning a first-best solution into an equilibrium by keeping its meeting rates fails, because agents raise or lower their thresholds relative to the pairwise thresholds the platform would choose, and constraint (6e) couples every type's threshold to all thresholds on the opposite side through . The paper therefore has to control equilibrium thresholds without computing them, which it does only in star-shaped markets, and it needs a case analysis there (Case 1 and Subcases 2(a), 2(b) of Proposition 4.8) in which the meetings of the first best are sometimes discarded. Each of the reductions loses a factor: 2 in the passage from a forest to stars and 2 inside each star.
The sides are separate finite types M and W with one law F m w per pair, serving both sides. The standing assumptions are ; for every type; each a probability measure with no atoms (NullSingletonClass, the paper's "continuous distribution"); and an integrable identity under each . The positivity of and the integrability are added: the paper uses both implicitly. Tails are taken over . LP feasibility includes , which the paper leaves implicit; Lemma 4.6 also assumes nonnegative capacities. is the supremum of over , never defined as a fixed point.
"Approximation of the first-best optimum" is stated against every first-best feasible candidate, so no supremum appears. An induced stationary equilibrium always includes the best-response constraint (6e); a formalization that drops it, or that lets the equilibrium use pairwise thresholds, makes the goal compare the first best with itself and is ruled out. With an empty side both welfares vanish and the goal holds, as in the paper.
The "polynomial-time" part of Theorem 4.1 is not posed: the paper's computational model (oracle access to the laws, footnote 15) is not specified precisely enough to formalize. The source is the arXiv v2 preprint (18 Aug 2021); the Management Science version may number results differently. Proofs of any milestone, auxiliary lemmas about tail integrals of atomless laws, and LP vertex arguments are all welcome.
Online display advertising is sold through ad exchanges, and much of its value comes from targeting: showing an ad to consumers known to be interested in the advertised product. For two decades the main tracking technology was the third-party cookie, under which an exchange can follow a consumer only after an advertiser agrees to share the data from its own website. Google's proposed replacement for Chrome, the Topics system, instead lets the browser itself assign consumers to interest categories. Advertisers no longer control that data, and the categories are coarse, so some ads reach consumers who are not interested.
Johnson, Jungbauer and Preuss (SSRN 3898798, Nov. 2022; published in Management Science, 2024, doi:10.1287/mnsc.2022.03385) study how data sharing and consumer control shape competition between ad exchanges. Their §3 adds a Topics-style category system to the base model and asks when advertisers use it, and how the exchange that runs it profits from its accuracy. This mission formalizes that section.
There are two advertisers and two exchanges. ADX1 runs the Topics system. It reaches all consumers interested in the product category, but reaching a mass one of them takes ad impressions; is the system's inaccuracy. ADX2 offers retargeting through another technology. An advertiser bidding there reaches a fraction of the consumers who recently visited its own website. An impression costs . A consumer reached by a single advertiser is worth the monopoly profit , and one reached by both is worth the competition profit . The parameters satisfy
where is the share of the ad price an exchange keeps.
The advertisers bid simultaneously, each on one exchange. Write for the profit of an advertiser on exchange when its rival is on (p. 17):
An equilibrium is a pure Nash equilibrium of this symmetric game. ADX1's revenue is per impression sold on it, and an advertiser bidding on ADX1 buys impressions. The proof of the main result uses the thresholds
and the accuracy threshold
In Lean these objects are Params, Params.Standing, payoff, IsNE, revenue, w₁, w₂ and tauTilde, in the namespace AdDataSharing.Topics.
Bidding on ADX1 means cross-targeting the rival's visitors, which Topics cannot avoid. The goal therefore says that both advertisers cross-target exactly when the system is not too inaccurate, and that this region is never empty.
Proposition 5 is the entry point of the paper's Topics analysis. It identifies when a category-based system is actually used, and it implies that removing advertisers' property rights over their data leads to more information being shared about consumers' purchase interests. Proposition 7 adds an incentive result: inside the region of use, the exchange running Topics gains from making it less accurate, because inaccuracy sells more impressions. A weaker rival exchange widens that region. Corollary 2 adds a regulatory point: a privacy rule that sets a high minimum inaccuracy can lead the exchange not to introduce the system at all. Corollary 2 compares against ADX1's equilibrium revenue in the base game of §1, which mission 1 of this series formalizes; its definitions are shared with this mission.
The results are proved in the paper, and none of them has a machine-checked proof. Formalizing them also corrects the printed statement. Display (6) on p. 17 omits a factor , and with the printed threshold the equivalence of Proposition 5 is false. The mission states the threshold that the page's own deviation condition gives.
The algebra is elementary, and the care lies in the equilibrium bookkeeping. "In the equilibrium both advertisers bid on ADX1" is a uniqueness claim. At the profile is still an equilibrium, but the asymmetric profiles are equilibria too. A proof that only checks deviations from therefore gets the wrong boundary. A proof also has to rule out every other profile, using and the signs of the denominators. Each threshold is a quotient, and its denominator is positive only because . Proposition 7 (i) compares two different games, and Corollary 2 needs equilibrium existence together with a threshold that is uniform in the profile.
All quantities are real. The game is the platform's general two-player pure Nash equilibrium CompetingChains.Cournot.IsPureNash, which this mission references, applied with payoffs and . There is no contracting stage and no equilibrium selection, as footnote 22 of the paper states. Deviation inequalities are weak, so the exact conditions read and where the proof writes strict inequalities as sufficient conditions.
Three assumptions are added relative to §3, and each is disclosed. is used throughout the paper and stated on p. 21. is the reading of "a fraction ". comes from the base model, where it reads . The inequalities and are kept as paper assumptions; they are inert here. Divisions outside the standing assumptions return Lean's junk value , and every theorem assumes the standing assumptions.
Several formalizations would trivialize the targets, and none is used. "Both advertisers bid on ADX1" is defined through IsNE and uniqueness, not as an inequality on payoff numbers. The printed threshold (6) is never posed. Statements quantifying over all equilibria also assert that an equilibrium exists, so they cannot hold vacuously. All definitions are local to this mission except the referenced Nash equilibrium notion. Contributions are welcome on any milestone, and a reusable lemma characterizing pure equilibria of symmetric games would serve all of them.
Every Bitcoin transaction recorded on the blockchain pays a fee, and the blockchain processes only a few transactions per second. The Lightning Network is a layer-two protocol that moves repeated payments off chain: two parties lock funds in a payment channel, exchange payments by updating the channel's balance, and touch the blockchain only to open, close or reset the channel. Whether a channel is worth opening is an economic question. Locked funds forgo interest, and a channel whose balance is exhausted must be reset on chain at a cost.
Guasoni, Huberman and Shikhelman (Management Science, 2023) model this trade-off with Poisson payment streams and continuous discounting, and obtain closed-form channel costs (their Theorem 1). Their Theorem 2 turns those costs into necessary conditions: a channel can be cheaper than settling every payment on chain only if the on-chain fee exceeds an explicit threshold depending on the reset cost, the payment rate and the interest rate. This mission formalizes Theorem 2, its two proofs, and the on-chain benchmark (Lemma 1) against which every channel is measured.
Node 1 pays node 2 one unit at the jumps of a Poisson process with rate , and node 2 pays node 1 at the jumps of an independent Poisson process with rate . The discount rate is the opportunity cost of capital per unit of time, is the cost of resetting a channel, and is the cost of one on-chain transaction. Node commits the amount to the channel.
On-chain settlement. If every payment of a stream with rate is settled on chain, the expected discounted cost is , where is the -th arrival time (Lemma 1). Two streams of rate cost .
Unidirectional channel. If only one node pays, at rate , a channel of size costs (Theorem 1(i), equation (1))
Bidirectional channel. With
(equation (4)), a channel with sizes costs , the expression (3) in , and . In the symmetric case it simplifies, with , to
A channel costs less than on-chain transactions if, for some size, its cost is strictly below the on-chain cost of the streams it carries.
For and any fee :
Theorem 2 gives the qualitative conclusion of the paper in quantitative form: channels pay off only when on-chain fees are high, reset costs low, payment rates high, or interest rates low. Read as a contrapositive, it says that below the thresholds, settling on chain is at least as cheap for every channel size, so no optimization over sizes is needed to rule a channel out. The expansions show the two thresholds scale differently in the interest rate, linearly for a unidirectional channel and as for a symmetric bidirectional one. The paper's subsequent asymptotic results (Theorem 3) rely on the same reductions.
The theorem is proved in the paper; nothing here is open. To our knowledge none of it is formalized. A formalization adds a machine-checked verification of a proof that contains several informal steps: a minimizer of a two-variable function is assumed to exist, two inequalities are stated non-strictly where strict ones are needed, and one sentence states an "if and only if" with where is meant. Lemma 1 also requires the discounted sum over a Poisson process to be integrable, which the paper's renewal argument takes for granted.
The bidirectional cost (3) is a ratio of differences of real powers of two algebraic numbers, and its minimum over two sizes has no closed form, so the threshold cannot be read off an explicit optimum. The paper replaces the optimum by reductions whose rigorous versions are the substance of the work: the passage from (3) to the symmetric form, the reduction of a two-variable minimization to the diagonal (asserted in the paper through a Hessian computation and the existence of a minimizer, neither of which is carried out), and a lower bound on that holds on all of and is not in Mathlib. The obvious approach of bounding the cost at its minimizer fails for the same reason it fails on paper: no minimizer is given. For part (i), the minimizer involves , and the minimal value still depends on through two terms, so a condition on alone does not follow by rearrangement. Lemma 1 requires an exchange of expectation and infinite sum over a Poisson process, which the paper's renewal argument assumes.
uniCost and biCost are the paper's expressions (1) and (3) with real sizes and real powers (Real.rpow). Theorem 2's proofs minimize over real sizes, and the hypotheses quantify over real sizes, so the statements imply their versions for natural sizes. The probabilistic derivation of (1) and (3) from the balance random walk is the subject of the sibling mission Channels I.QueueingFundamentals.Foundations.IsExpInterarrivals of i.i.d. exponential interarrival times; the conclusion asserts integrability as well as the value .𝓝[>] 0) with and fixed.Ruled out as trivializing: fixing , or ; restricting to natural sizes without saying so; an existentially chosen ; weakening either strict inequality; or an on-chain cost under which the comparison is vacuous.
Needed infrastructure: real-power calculus and convexity on , and bounds, little-o expansions of and near their base points, and the Laplace transform of Gamma laws for Lemma 1. The csch inequality (22) and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome independently.
When one breached contract forces the next party to breach its own contract, a single failure travels down a loss chain: agent 1 (the initiator) causes a loss to agent 2, which can then no longer honour its agreement with agent 3 and causes it a loss , and so on until agent causes a loss to a final victim. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss should be shared among the agents of the chain, with the aim of encoding the answer in a smart contract that settles such disputes automatically.
Their central rules are the fixed-fraction rules , under which every agent pays a fixed fraction of the loss it caused and the initiator also pays the remaining fraction of the total. An axiomatic characterization (their Theorem 1) singles out the whole family but not a particular member. This mission formalizes the paper's game-theoretic argument for the midpoint : the cooperative game that records which coalitions are liable for which losses has the midpoint allocation as both its Shapley value and its nucleolus, the two best-known single-valued solutions of cooperative game theory.
Agents are with . A loss problem is a vector , where is the loss agent causes to agent ; the total loss is . The fixed-fraction rule with parameter assigns
A transferable-utility game on is a function assigning a real number to every coalition . The liability game of is
a coalition is liable for the losses its members caused only if it contains the initiator, without whom no loss would have occurred. The contribution of player to the grand coalition is .
Two solution concepts are compared with .
A game is convex if and for all .
For every ,
where the second identity is stated as: is an imputation of with lexicographically minimal sorted excess vector, and every imputation with this property equals .
The result. Theorem 1 of the paper leaves a one-parameter family of rules, and a designer who writes the rule into a contract must still choose . Theorem 3 gives a reason for that does not depend on the axioms: if losses are treated as the worth of coalitions, two solution concepts that are built on unrelated principles (average marginal contributions on one side, lexicographic minimization of complaints on the other) both return . Together with the paper's Theorem 2 (equidistance from ideal allocations, a separate mission of this series) it makes the midpoint the paper's recommended rule.
Formalizing it. The paper proves Theorem 3 by citing two results of Muto, Nakayama, Potters and Tijs (1988) on big boss games, the nucleolus formula (their Theorem 4.2) and the coincidence of Shapley value and nucleolus for convex big boss games (their Theorem 4.5); the paper itself proves only convexity and the marginal contributions. A formal proof must therefore establish the nucleolus of directly from Schmeidler's lexicographic definition. No nucleolus definition exists on the platform (searched 2026-10-14), and this mission introduces one. The Shapley value and convex games are reused from the platform's published definitions, and the core-contains-the-Shapley-value theorem for convex games is already proved there.
Convexity and the marginal contributions are finite case analyses. The Shapley identity is a weighted sum over all coalitions not containing a player and needs the combinatorial identities behind the weights; for only the position of the initiator relative to matters.
The substantive part is the nucleolus. Its definition compares sorted vectors of excesses, so an argument cannot treat one coalition at a time: showing that a candidate is lexicographically minimal requires controlling how a change of the payoff vector permutes the order of all excesses. The obvious first idea, minimizing only the largest excess (the least core), generally leaves a set of imputations rather than a point, so the comparison must go down the whole sorted list. Coalitions whose excesses tie, which happens for instance when some , are where informal arguments about sorted excess vectors are usually loose, and a formal proof has to handle them.
Fin n with the initiator at index 0; [NeZero n] encodes , which the paper assumes because . Loss vectors are Fin n → ℝ with the hypothesis IsLoss ℓ ().Finset (Fin n) → ℝ. The Shapley value is the published Supermodularity.Cooperative.ShapleyValue and convexity the published Supermodularity.Cooperative.IsConvexGame (the supermodular form, equivalent to the increasing-marginal-contribution form used on p. 24).Nucleolus file: imputations with efficiency and individual rationality, excess over all coalitions including and , sorted by ≥ into a list, and compared with List.Lex (· < ·). Including and does not change the order, since their excess is at every imputation.Contributions welcome: proofs of the milestones; general lemmas on sorted excess vectors (e.g. Kohlberg-type criteria for the nucleolus), which are reusable for every later nucleolus result; Schmeidler's existence and uniqueness theorem; and the general big boss game results of Muto et al. (1988).
A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves positions empty; sending too many hires beyond capacity at a cost. This trade-off is the same as overbooking in revenue management (airline seats, hotel rooms), with the difference that candidates are heterogeneous in both value and acceptance probability.
Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three hiring-pipeline models through linear programming relaxations. This mission formalizes their lower bound for the third model, Simultaneous Offering (§3.3 and §6 of the paper). The question it answers is practical: how much is lost if the firm restricts itself to value-ordered policies, which send offers to the most valuable candidates for some , instead of searching over all offer sets? Value-ordered policies are natural, because a firm rarely wants to withhold offers from its best candidates, and the optimal one is computable by a short dynamic program. The paper shows (Example 1, p. 25) that they can be arbitrarily bad in general, and that they are provably good when every candidate's value is bounded below.
An instance has positions and candidates, . Candidate accepts an offer independently with probability and then contributes value . Candidates are labelled so that . The firm chooses an offer set ; with the random set of acceptances, the reward is
the cost per candidate hired beyond capacity being normalised to . is the best expected reward over offer sets. For the instance is -bounded, , if for all ; the interesting range is , since for offering to everyone is optimal.
The benchmark is the LP relaxation
which charges the overage cost on the expected number of hires. Write and .
The algorithm , for , takes an optimal LP solution , scales its total mass by to , and fills mass from the most valuable candidate down: while the prefix mass stays at most , one fractional entry, then zeros. Offers are then sent independently with probabilities , so the algorithm randomises between two value-ordered policies. Its expected reward is .
The guarantee involves the truncated Poisson mean and
For , every , every optimal solution of and a maximiser of the objective defining ,
Theorem 3 makes value-ordered policies an -approximation on -bounded instances, through Lemma 10. The factor tends to as for fixed : at it is at least (Corollary 4). The paper's Theorem 4, the subject of the companion mission in this series, shows that no value-ordered policy beats the same expression with the supremum over , so the analysis is tight wherever the two suprema coincide. The interpretation of is how soft the capacity is: the bound degrades exactly as the overage cost dominates candidate values.
The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it has been machine-checked. A complete development would give the platform an overbooking-type stochastic selection model with an exact expected reward, an LP benchmark, and the truncated-Poisson constant that recurs in prophet-inequality and online-matching analyses (the -uniform correlation gap of Yan 2011). Proposition EC.2 and the monotonicity of are reusable on their own.
The obvious argument compares the algorithm's random number of hires with the LP's expected number and loses everything to the overage term: the LP pays , the algorithm pays , and Jensen's inequality points the wrong way. The gap must be controlled by a sum of independent Bernoulli variables against a Poisson variable of the same mean, uniformly over how the mass is spread across candidates. A second difficulty is the regime , where the LP optimum deliberately exceeds capacity; a direct bound there does not reduce to the first case, and the paper's reduction (Lemma 14) changes the instance rather than the algorithm. Tie cases make the LP optimum non-unique, which the formal statements must handle explicitly.
Candidates are Fin n (0-based), all quantities are real. The sorted labelling is part of instance validity (Antitone I.v), as the paper assumes after relabelling; ties may be ordered arbitrarily. Every expectation is an explicit finite sum over the hire sets with independent probabilities ; there is no measure theory. The truncated Poisson mean is the series of the Poisson pmf. is the supremum of the objective over the feasible set, which is the LP value; is the supremum over . is any maximiser of the objective over ; one exists by continuity. A candidate with receives , which changes no reward.
The algorithm's reward is the exact expected reward of the run with independent offers, never the bound produced in the paper's proof, and the comparison is with the LP value at an optimal solution, not with the objective at an arbitrary feasible point; is the supremum of the specific Poisson expression, not a free constant.
Two statements carry disclosed hypotheses, because the printed versions fail at ties: Lemma 12 assumes , , , and Lemma 14 assumes . Counterexamples are in the items' Formalization Notes. Theorem 3 and Lemma 13 need neither and hold for every optimal LP solution.
A complete development needs Poisson series manipulations (the closed form, concavity of ), a Bernoulli-to-Poisson comparison for , and fractional-knapsack structure for the LP. Contributions of alternative proofs of any milestone, and of the Poisson facts as standalone results, are welcome.
Proof-of-work blockchains such as Bitcoin pay a block reward to the miner that first solves a computational puzzle. The chance of winning is proportional to a miner's share of the total computing power (hash rate), so mining is a contest in which every miner pays for hash rate and the reward is split in proportion to it. Over time mining moved from general-purpose hardware to specialized chips, and this raised the question of whether access to better hardware concentrates mining in a few hands, which would weaken the decentralization the protocol relies on for security. Arnosti and Weinberg (arXiv:1811.08572) showed that cost asymmetries alone already concentrate mining in a proportional-share contest.
Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021; published in Management Science, 2023) model this as a two-stage game. Miners first decide how much to invest in the newest hardware, which lowers their cost per unit of hash rate. They then compete in the mining stage. Their Proposition 5.1 describes the equilibrium of the investment stage: which miners invest, how much, and how the number of active miners depends on the fixed cost of entering. This mission formalizes that result, corrected where the printed statement is false.
There are miners. Miner starts with a cost-per-hash , sorted so that . The newest hardware has cost-per-hash , with for every . In the first stage miner replaces a fraction of its hardware, which leaves it with cost-per-hash
where measures adjustment costs ((3.1)–(3.2)). Write , read as when .
In the second stage, the mining stage, miner chooses a hash rate . With , its payoff is
with reward , capacity parameter and fixed entry cost ((3.4)). An equilibrium hash rate profile is a profile from which no miner gains by changing its own hash rate (Definition 3.2(i)). Proposition 4.1 of the paper shows that it exists and is unique, and posing that result is the subject of mission 1 of this series. The active set is , and is the set of miners active without investment. The entry cost is paid by a miner outside that invests.
An equilibrium investment is a profile from which no miner can raise its payoff by changing , the mining stage being replayed at the new profile (Definition 3.2(ii)). The threshold profile invests in miners and in the others; this is the form (5.1).
Assume is generic: no potential entrant's gross mining profit at equals . Then:
The result says three things about the effect of hardware upgrades on decentralization. Incumbents never drop out: every miner active before investment invests the cost-minimizing amount and stays active. Entry is ordered: in the threshold equilibrium the miners that enter are the most efficient ones. A higher fixed cost of entry admits weakly fewer miners. The paper's later propositions (5.2–5.5), which describe how hash rates and shares move after investment, start from this equilibrium.
Formalizing it adds two things. First, a machine-checked statement of what is actually true. The printed uniqueness is false, and the corrected statement separates what holds for every equilibrium from what holds within the threshold family. Second, a formal two-stage game in which the second stage is replayed at every deviation of the first, through an explicit equilibrium selection. None of the results of the paper has been formalized before; the platform has no contest or rent-seeking game.
The printed proof argues that an active miner's profit decreases in its own cost "irrespective of the cost parameters of other miners", citing Proposition B.1. Proposition B.1 is a derivative at a fixed set of active miners. Investment can change that set, so the proof needs a global monotonicity of the equilibrium profit across changes of the active set, in the own cost and in the presence of rivals. That step is not in the paper.
The obvious uniqueness argument also fails. Take two potential entrants with nearly equal initial costs and room in the market for only one of them. Either one can enter while the other stays out, and both profiles are equilibria. The numbers are , , , , and any : both and are equilibrium investments. So no proof can rest on "a miner never invests while a cheaper one does not", which the paper asserts on p. 45.
Miners are Fin N and 0-based: Lean miner i is the paper's miner . Hash rates, costs and parameters are real numbers. The mining stage is defined for an arbitrary cost vector, not assumed sorted, because investment can reorder costs. The equilibrium property "" is written as "no deviation is profitable", over and over . The mining equilibrium enters as a selection with the hypothesis that is an equilibrium hash rate profile for every . Proposition 4.1 makes it unique; it is not defined by a closed form. The fixed cost enters only the investment stage, inside the branch of (3.4). Derivatives are HasDerivAt statements along one coordinate. "Decreasing" is weak, as in the paper's footnote 12.
The goal is the corrected Proposition 5.1. The printed uniqueness among all investment profiles is not posed, and neither is the p. 45 claim that a miner cannot invest while a cheaper miner does not. Both are false by the instance above. Three hypotheses are added to the paper's: ; for every (the paper allows equality, under which is constant and every is a best response); and the genericity of , which excludes finitely many values. Without the selection hypothesis the goal would be about an arbitrary function. Without the existence in part 1 the "every equilibrium" clause could be vacuous. Both are in the statement, so neither trivialization is available.
A complete development needs the mining-stage results of mission 1 of this series: existence and uniqueness of the mining equilibrium (Proposition 4.1) and the participation condition (Proposition 4.4). Since one draft cannot import another, this mission redefines the mining stage in its own namespace PoWMining.Investment. The new work is a global comparative-statics argument for the mining equilibrium across changes of the active set. It is reusable for any proportional-share contest with convex costs. Contributions are welcome on the milestones in any order, on that global monotonicity, and on the existence half of part 1.
Optimal stopping with partial information sits between two classical problems. In the secretary problem a decision maker sees values in random order, knows nothing about how they are generated, and must stop on the best one; the optimal guarantee is . In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee, relative to the expected maximum, is the constant : Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better on every distribution, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017, doi:10.1145/3033274.3085137) gave a rule that achieves it. Practical settings, such as pricing from historical data, lie in between: the distribution is unknown, but samples of it are available.
Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) interpolate between the two problems with the -sample-driven optimal stopping problem: each of adversarial values is independently revealed in advance (a sample) with probability , and the remaining values arrive online in random order. At this is the secretary problem; as it approaches the i.i.d. prophet inequality. They show that the optimal competitive ratio of the limit problem is the value of an infinite-dimensional linear program, and they construct an explicit threshold rule whose guarantee is the root of a scalar equation.
Prior work on learning a distribution from samples obtained guarantees with samples (Correa, Dütting, Fischer, Schewior, 2019) and with samples (Rubinstein, Wang, Weinberg, 2020). Theorem 9 of the paper, the goal of this mission, gives such a guarantee with samples.
Fix . The guarantee of the explicit threshold rule is the number solving
Lemma 7 of the paper shows that (19) has exactly one root in . The i.i.d. prophet constant is the solution of
The proof of Theorem 9 (Appendix B.9) works with three auxiliary functions of , each depending on as a parameter:
Appendix B.7 also names the two sides of (19): and . In Lean, IsAlphaTilde p a and IsAlphaStar s are shared predicates in SampleDrivenOS.Limit; aB9 s p, bB9 s p, cB9 s p, fB7 p α, and gB7 p α are in SampleDrivenOS.Linear.
It is stated for every root of (19) and every solution of the integral equation; neither existence nor uniqueness is assumed.
The explicit rule's guarantee is a lower bound on the optimal ratio , and Theorem 8 (a separate mission of this series) shows as . Theorem 9 makes that convergence quantitative and uniform: the guarantee is at least linear in , so with , an online set of size and samples the rule earns of the expected maximum. This improves the sample complexity of the earlier learning-based results by a polynomial factor, in a model more general than theirs.
The theorem is proved in the paper; it has no machine-checked proof. The proof is elementary real analysis on explicit series and integrals, and one of its steps is a numerical check that the paper does not carry out in print. A formalization turns that numerical claim into a certified inequality and checks a chain of estimates in which one inequality sign is misprinted (see Formalization scope).
The statement is about two implicitly defined numbers. has no closed form, and is defined by an integral equation. Evaluating both numerically at finitely many proves nothing for the remaining , and the inequality is tight at (), so no uniform slack is available near .
Concavity of would give the result immediately, and the paper reports it numerically, but the authors were unable to prove it; the argument must avoid it. The remaining work handles infinite series whose terms depend on through both and : differentiating such a series term by term requires uniform control of the derivative series, comparing it with an integral needs a monotonicity argument, and one step needs a bound valid on an entire two-parameter region rather than at a point.
IsAlphaTilde p a (with ) and IsAlphaStar s (with ). Statements quantify over every solution. Both exist, so the goal is not vacuous: existence of is Lemma 7 (posed in the second mission of this series), and existence and uniqueness of are posed as CorreaThreshold.Adaptive.beta_star_existsUnique (512ff915-7ec1-4d24-87b3-bc8adfee6bad).tsum over i : ℕ with the paper's index shifted to i + 1. For parameters in all series are summable, so tsum is the true sum; summability is part of what solvers prove, never a hypothesis. Differentiability of is likewise a conclusion (HasDerivAt), never assumed.Real.log 0 = 0 makes the integrands' values at equal their limits, so the interval integrals are the true integrals. Every division (, ) is at a positive argument under the stated ranges, and every logarithm's argument is positive.CorreaThreshold.Adaptive.inv_beta_star_gt (ce70487c-b155-4e47-9ce8-8348dc1b1645). The upper bound (numerically ) is posed nowhere and is welcome as a lemma.deriv (which is at non-differentiable points), or replacing by a chosen value all change the theorem. None is used.tsums under a dominating series, Riemann-sum comparisons for monotone integrands, a Chebyshev-type integral inequality for two decreasing functions, and certified interval arithmetic for a two-variable inequality such as milestone 8.