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?
Banks hold claims on one another. When one bank cannot pay, its creditors receive less, which can push them into default in turn. Clearing models compute the payments and wealths that are consistent across the whole network. Regulators and researchers use them to measure systemic risk and to price interbank debt. The basic model is that of Eisenberg and Noe (2001), doi:10.1287/mnsc.47.2.236.9835. Rogers and Veraart (2013), doi:10.1287/mnsc.1120.1569, added bankruptcy costs: a defaulting bank recovers only part of its assets.
The value of a bank's debt or equity is an expectation over random endowments. For general endowments that expectation requires partitioning the endowment space into up to default regions (Gouriéroux, Héam and Monfort 2012), and with bankruptcy costs those regions need not be convex. Banerjee and Feinstein, Pricing of debt and equity in a financial network with comonotonic endowments (Operations Research 2022; arXiv:1810.01372), observe that when all endowments are driven by one factor (they are comonotonic), banks default in a fixed order as the factor falls. Default probabilities and the prices of debt and equity then have closed forms.
There are banks and an outside society node. Bank owes a total of ; the fraction of it is owed to bank (), and the fraction to society (Assumption 2.1). The matrix is the relative liabilities matrix. Banks start with endowments . A bank with negative wealth defaults and keeps a fraction of its external assets and of its interbank assets.
With componentwise, the clearing process is
and a variant , which replaces by its positive part, is used in the appendix. The greatest clearing wealth is the largest real solution of . Bank 's payment is and its equity is .
If the set of defaulting banks has indicator , the clearing equations are linear. With the diagonal 0–1 matrix of ,
Comonotonic endowments are for a nonnegative random factor and a nondecreasing map (Assumption 3.2). The solvency threshold of bank is (Definition 3.4). Banks are numbered so that , with and (Assumption 3.5). On exactly banks default; and are and at that default set, with and .
With , for every bank :
The goal is the theorem as printed, with one added hypothesis (see Formalization scope).
Theorem 3.6 turns the valuation of every bank's debt and equity in a network with bankruptcy costs into one-dimensional integrals of the factor, replacing the default regions of the general case. The default probabilities depend only on the thresholds , which in turn depend only on the map and not on the law of . The same formulas price debt and equity in the paper's numerical study of the European banking system, and they are the starting point for the comonotonic bounds of Lemma 4.1, which are not part of this mission.
The paper gives a one-sentence proof of Theorem 3.6 and proves its appendix results largely by citation (Tarski, Milgrom–Roberts, Rogers–Veraart, input–output theory). No part of it has been machine-checked. A formalization supplies the missing steps: the identification of the two clearing maps, the attainment of the thresholds, nonsingularity of the linear systems, and the decomposition of the expectations. It also produces, as a reusable by-product, the Rogers–Veraart clearing model with its greatest fixed point, which other financial-network results can build on.
The obvious argument is: banks default in order, on each interval of the wealth is affine in , so integrate piece by piece. Two steps of it fail as stated.
First, the threshold is an infimum, and the paper treats it as attained ("the minimal value such that firm is solvent"). With bankruptcy costs the wealth jumps when a bank defaults, even for continuous , so attainment needs an argument about the greatest fixed point under decreasing endowments. Without right-continuity of it is false.
Second, the greatest fixed point of is not reached by Tarski's theorem on , because is not monotone below . That every real fixed point lies above uses Assumption 2.1. Nonsingularity of also rests on Assumption 2.1. Matching the default set to the interval then combines monotonicity (Proposition A.6) with the ordering of Assumption 3.5.
Fin n; bank i is the paper's bank . The data are , , , (structure Network), with the standing assumptions bundled in Network.Standing. is the supremum of the real fixed points of in the lattice ; payments and equity follow Definition 2.2. Default sets are finite sets of banks. Inverses are Matrix.inv.i.When banks are hit by losses they sell assets to restore their leverage targets, and these fire sales depress prices for every other holder of the same assets. The resulting deviation of market capitalization from its fundamental value is a systemic externality: it depends not on any single bank's portfolio but on how the stock of each asset is distributed across banks. Awiszus, Capponi and Weber (arXiv:2003.10121, Operations Research 2022) ask which distribution of a fixed stock of assets among banks with fixed budgets minimizes this externality, as measured by the expected squared deviation of market capitalization from fundamentals. The question matters to macroprudential regulators, who can influence portfolio overlap among banks, and it connects to the literature on overlapping portfolios and price-mediated contagion (Greenwood, Landier and Thesmar, 2015; Capponi and Larsson, 2015).
The paper's answer is explicit: the optimal mean squared deviation has a closed form, the optimum is computed by a two-step "aggregate first, then allocate" procedure, and the optimal allocation is unique exactly when there are two banks.
There are assets and banks. A holding matrix records in entry the holding of asset by bank , so column is bank 's portfolio. Initial prices are normalized to .
Let . Then
the f-efficient holding matrix is unique if and only if , and in that case it equals
The result itself. Theorem 4.1 gives the smallest achievable mean squared deviation of market capitalization from fundamentals for a given asset supply, budget profile and systemic significance profile, as an explicit function of the shock moments. It is the benchmark against which the paper measures the inefficiency of observed and diversified holdings (Section 4.2 shows that full diversification is f-efficient only in a degenerate case) and drives the comparative statics of Section 5. Part b) says that with three or more banks efficiency leaves an affine family of optimal allocations of dimension , so a regulator has residual freedom to pursue other objectives at no cost in market efficiency.
Formalizing it. The result is proved in the paper; no machine-checked version is known. The formal development delivers the theorem together with a reusable treatment of minimizing a positive definite quadratic form over a hyperplane, the existence part of the transportation-type linear system , , , and an exact rank computation for the structured matrix . The uniqueness characterization in part b) depends on that rank computation, which the paper carries out by Gaussian elimination on block matrices.
The minimization over is a -dimensional quadratic program whose objective is degenerate: it depends on only through the -vector . Strict convexity therefore cannot give uniqueness, since the objective is constant along every direction in which and the constraints do not change, and the obvious argument for part b) fails. Existence is not automatic either: is unbounded, and one must show that every point of the hyperplane is attained as by a feasible , which fails when is constant. The uniqueness statement is a dimension count: it needs the exact rank of the constraint matrix , whose rows carry exactly two linear dependencies under Assumption 3, so that the solution set has dimension , which is positive as soon as and .
Fin K, banks are Fin N, all quantities are real; holding matrices are Matrix (Fin K) (Fin N) ℝ. The paper's banks 1 and 2 are the indices 0 and 1.Matrix.inv, which returns on singular matrices. Every statement that mentions , or assumes for all (Assumption 2), and every statement that divides by assumes .Module.finrank of the kernel of .Fin.cast.The development needs the Sherman–Morrison identity for a diagonal-plus-rank-one matrix, the minimizer of a positive definite quadratic form under one linear constraint, explicit constructions in , and a rank computation. Contributions of reusable lemmas for these, and of proofs of the milestones in any order, are welcome.
A customer who is told that service will be delayed can use the announced wait to decide whether to stay, leave, or plan around the delay. A service operator needs to know whether a changing, customer-specific announcement actually predicts the eventual wait more accurately than a fixed announcement. Bassamboo and Ibrahim studied this question for the last-entered-service (LES) announcement, which reports the wait of the last customer to enter service, and for a static announcement based on the mean wait of delayed customers. Their empirical examples show that neither method wins uniformly across queueing regimes; the comparison depends on how the announcement and the eventual wait move together (Bassamboo and Ibrahim, 2021, §§3–4 of the submitted manuscript).
The mission isolates the paper's general comparison criterion. Its statement needs no particular arrival process, service discipline, or queue length. This makes the result a reusable mathematical test for predictors in other service systems as well as for LES. The paper itself notes that the criterion applies irrespective of the specific queueing model, subject to the moment conditions under which its mean-squared errors and correlations are defined (submitted manuscript, §4.2, p. 14).
Let be the real-valued waiting time of a delayed customer in steady state. Operationally, the paper takes the virtual waiting time and conditions on : has the conditional distribution of a positive wait. Let be a real-valued predictor issued to that customer. To compare a prediction with the outcome, the pair must be jointly distributed; their separate marginal distributions cannot determine the correlation. Both are represented as functions on one probability space in Lean.
The static announcement, denoted , always reports . A changing predictor can instead respond to the system's current state. The paper's mean-squared error of is the expectation of its squared discrepancy from the outcome:
Write and for variance and covariance. When both variances are positive, the Pearson correlation is . The coefficient of variation of the delay is . These are the quantities in §4.2 and equation (3) of the submitted manuscript (published article; mission citations use the submitted manuscript's page and equation numbers).
The first milestone establishes the error of the static predictor from its definition:
The next two milestones give the expanded error identity from the proof of Proposition 1 and its normalized form, equation (4). Suppose and with . Proposition 1 states
The goal is Corollary 1, equation (5). If has the same mean and variance as , it compares the two predictors at the exact threshold :
Both inequalities are non-strict. The corollary is stated for a general predictor ; applying it to LES requires a separate analysis of the LES wait and its correlation with the arriving customer's wait. The submitted manuscript supplies that model-specific analysis later in §5 (Bassamboo and Ibrahim, 2021).
Under the corollary's equal-mean and equal-variance assumptions, the comparison of two expected squared errors reduces to one correlation. A predictor with correlation at most offers no mean-squared-error improvement over the static announcement; a predictor above that threshold does. The equality case is included. Proposition 1 also records how a mean shift or a variance change modifies this comparison, which is useful when a proposed announcement is biased or more variable than the delay.
The paper proves these identities. This mission asks for machine-checked proofs of their statements in Lean; the draft theorems themselves are open proof obligations. A completed development would provide reusable definitions of predictor MSE, the constant mean announcement, Pearson correlation, and coefficient of variation, together with exact interfaces for later queueing results. It does not assert that the paper's LES limit theorems are already formalized.
The key mathematical work is passing from the expectation of a squared difference to the variance and covariance terms while keeping the two random variables on the same probability space. In Lean this requires the integrability consequences of square integrability, the relation between covariance and the centered product, and careful handling of the square-root normalization. Merely replacing MSE and correlation by unrelated real parameters would erase that work and yield an elementary numerical equivalence. The proposed definitions are therefore the expectations and covariance stated in the paper, and the goal quantifies over actual random variables.
The boundary also needs attention: the predictor has zero variance and ordinary Pearson correlation has a zero denominator. The term involving correlation is multiplied by , so the displayed identity still has a meaningful value under the Lean convention described below. Proposition 1's other denominator, , requires a positive delay mean and variance in the intended setting.
Lean uses an arbitrary measurable space with a probability measure and real-valued functions on that space. It does not construct the underlying queue; §4.2 makes the comparison at the level of the joint law of the delay and prediction. Each theorem explicitly assumes where both appear. This supplies finite second moments for the paper's variances and MSE and avoids Lean's default value for a nonintegrable real integral. The EA identity only needs .
Positive variance of is explicit in Proposition 1, its expansion, and the corollary. It gives the intended domain of correlation in the equal-variance corollary and prevents equation (4) from failing under division by zero. Proposition 1 additionally assumes , as expected for a positive conditional wait, so . No condition is imposed: at , Lean evaluates the zero-denominator correlation as zero and the entire correlation term vanishes. The error is defined with as in equation (3), although the proof writes the reversed difference. Contributions toward the integral identities, covariance normalization, and the final inequality are welcome; the four definitions may also serve other prediction-error formalizations.
Firms that serve several geographic markets must decide both how much to produce and where to sell it. A capacity limit couples those regional decisions: an extra unit sent to one region cannot also be sent to another. Different transport costs and demand curves make a collection of independent single-region Cournot models inadequate. Alsabah, Bernard, Capponi, Iyengar and Sethuraman study whether this coupled quantity game has a determinate outcome. Their 2020 author version proves a unique equilibrium allocation and characterizes it through firms' marginal profits. This mission concerns that result, Theorem 4.5 on p. 12 of that version.
There are firms and regions . Firm sells quantity in region . Its total output is , constrained by capacity . The total sales in region are . The inverse demand function gives the price when total sales are . Firm pays production cost per unit and transport cost per unit sent to region . Its profit at allocation is
A strategy for firm is any nonnegative regional allocation whose total is at most . A Nash equilibrium is a feasible profile at which no firm can gain by changing its entire regional allocation while the others hold theirs fixed. This is the feasible unilateral-deviation definition in the paper's Definition 3.1, p. 8.
The marginal profit in region is
For a vector of marginal-profit levels, condition (2) says and for every firm and region. Proposition 4.2 gives a unique nonnegative allocation satisfying these conditions, denoted , when lies in the box , where and . The reduced-form operator assigns firm zero marginal profit if its output at is below capacity. Otherwise it assigns the marginal-profit level at which its output under equals . This is the two-case definition on p. 11; it depends on the other firms' marginal-profit levels through .
Lemma 4.3 asserts that has exactly one fixed point in the marginal-profit box:
Theorem 4.5 identifies every equilibrium of the original quantity game with the allocation at that fixed point:
The goal includes existence of and the equivalence, so it asserts both existence and uniqueness of the equilibrium allocation. Its milestones follow the paper's supporting statements: existence of a pure equilibrium, marginal-profit conditions, existence and uniqueness of , continuity and comparative statics, fixed points of , and the link from an equilibrium to a fixed point. The Algorithm 4.1 computation clause of Proposition 4.2 and the iteration-convergence clause of Lemma C.5 are identified as partial milestones; their full printed text is retained in the milestone provenance.
The result establishes that capacities, regional demand, and unequal shipping costs still lead to a single predicted sales allocation under the paper's regularity conditions. It also gives a common language for comparing the original game with a smaller game in marginal-profit vectors. Subsequent results in the paper analyze changes in costs, capacities, prices, and consumer surplus relative to this equilibrium Alsabah et al., §§5–6; those later comparative-statics claims are outside this mission.
The mathematical result is proved in the cited paper. The goal here is a machine-checked Lean development of its model, its fixed-point characterization, and the existence and uniqueness theorem. The current proposal contains definitions and theorem statements, with proofs open. The pure-Nash relation is a published reusable definition; the market model, complementarity allocation, and operator are new interfaces that could also support later formalizations of the paper's comparative-statics results.
An equilibrium of the quantity game satisfies the marginal-profit conditions, but those conditions alone describe candidate allocations and do not replace feasible unilateral deviations. Conversely, a fixed point of does not become an equilibrium merely from the fixed-point equation: the capacity-constrained regional payoff problem still has to be connected to the allocation . Uniqueness also requires control of how all firms' regional sales respond when one marginal-profit coordinate changes. Lemma C.4 records weak and strict changes, including boundary cases where a firm stops selling in a region. The existence lemma invokes a general pure-strategy equilibrium argument; the statement is kept even though that infrastructure is substantial in Lean.
Lean uses Fin N and Fin R for zero-based firm and region indices. An allocation has type Fin N → Fin R → ℝ, with the firm coordinate first, the transpose of the matrix orientation in the paper. Finite sums give firm and region totals. The inverse demands are on , strictly decreasing and concave on nonnegative quantities; deriv is therefore the ordinary derivative at the quantities used here. The paper phrases Assumption 1 for direct demand on and then uses regularity of its inverse . The formal model makes that inverse-demand regularity an explicit assumption. It also states , as implicit in the interval , positive capacities, and nonnegative production and transport costs. Those sign assumptions are needed for the box and the two branches of to have the stated meaning. No positivity of prices at all quantities or finite choke quantity is assumed.
IsEquilibrium uses the published CarbonDoubleCount.Planner.IsPureNash relation, testing every feasible full strategy deviation. Qhat is chosen as the unique solution of condition (2), and Phi is computed from that allocation and the market capacities. On the stated box, the proposal's milestones establish that the selection and inverse branches denote the paper's objects. The intended theorem excludes encodings that choose an active set freely, pass or as arbitrary parameters, or substitute first-order conditions or coordinatewise deviations for Nash equilibrium. The definition layer and results on continuity, monotonicity, and fixed points are reusable parts of the development. Contributions that prove these stated targets or provide supporting analysis of the firm's concave payoff problem are within scope.
A visible patroller gives an attacker information: the attacker can observe when a location is vacant and wait for a favorable moment. This changes the patrolling problem from choosing how often to visit each location to choosing a movement rule that remains effective against an adversary who chooses the attack time. The preprint The Uniformed Patroller Game studies this setting on a star network, where the patroller moves between a central base and the locations she protects. Its main result characterizes a robust attack delay and a robust patroller reflection rule for every attack duration, as well as exactly when those choices are unique. The source here is arXiv:1908.07366v2, by Alpern, Chleboun, and Katsikas; the later journal article has a different title and author list.
The network has a centre and end nodes. Each end node is a location to defend; the centre is a base and is not an attack location. A Markov patroller strategy is a pair . When at , the patroller goes to each specified end node with probability and stays at with probability . When at an end node, she returns to with probability and otherwise stays at that same end node. Thus , , and . The strategy does not depend on which node the attacker selects.
The attacker chooses an end node and an integer delay . After the patroller leaves , the attacker counts consecutive periods of her absence. If she returns before periods pass, the count resets. Otherwise the attack begins in the th period of absence. It lasts periods and is intercepted if the patroller visits during that interval. The paper requires because a one-period attack could always begin immediately after departure. This mission also takes , ensuring another end node exists and the conditional attack event has positive probability under the admissible strategies.
Let be the first positive step at which the patroller, having just left for , returns to . The starting state is already the first period of absence. The interception probability is the paper's equation (17):
The patroller maximizes and the attacker minimizes it. A saddle point is a pair of strategies for which neither can improve by changing alone, with comparisons over all admissible and all end-node-and-delay pairs . A strategy is called optimal if it occurs in a saddle point. The source analyzes pure strategies in these parametric sets; a pure saddle remains a saddle if independent randomization of these strategies is permitted.
Theorem 1 asserts that some optimal patroller strategy has and pairs with an attack at any end node with . It also asserts two exact uniqueness regimes:
The patroller's centre-to-end probability is selected optimally; it is not fixed in the main statement. The attack node is immaterial by symmetry, but it remains an explicit part of every attacker strategy. The theorem is posed over the full strategy sets, so its uniqueness assertions cannot be satisfied by restricting those sets to the displayed choices.
The milestone list follows the source's symmetry reduction, Lemmas 1–3, equations (3) and (15), and Propositions 1–2. For , Proposition 1 identifies and the value . It also identifies optimal reflection probabilities below one. For odd , Proposition 2 identifies the unique optimal patroller strategy , permits every attacker delay, and gives
For general even , the statement that an optimum has is recorded separately. It is needed to support the delay-uniqueness clause, while the paper illustrates this interior maximum numerically in Figure 2 rather than proving it as a numbered result.
The theorem reduces the strategic choices in this game: regardless of attack duration, delay two is an optimal response, and full reflection is compatible with an optimal patrol. The uniqueness clauses explain when alternatives are possible. With odd duration, the zero-holding random walk makes all delays equally good for the attacker. With duration two, a range of reflection probabilities below one remains optimal for the patroller. Those facts distinguish a recommendation that is optimal from one that is forced by the game.
The paper gives arguments for its numbered results, but this mission's Lean theorems are open statements awaiting machine-checked proofs. A completed development would provide a reusable finite-path model of conditional hitting probabilities and a formal game-theoretic treatment of the full delay set. The even-duration interior-maximizer milestone also calls for an analytic proof of a property that the preprint supports with plots. The finite-path and generic saddle-point definitions can be reused outside this particular star network.
The apparently direct comparison of attack delays fails because the patroller's state at attack start depends on surviving the entire waiting period without a return to . The conditional distribution at that start time changes with . Likewise, increasing reflection probability can change both the trajectory and the event on which the payoff is conditioned. A comparison of one-step transition probabilities alone does not establish a comparison of . Exact uniqueness is more delicate still: at the chain alternates between centre and end nodes, creating genuine ties between delays for odd durations. The even-duration argument needs an optimum away from this boundary.
Lean represents the original star as Option (Fin n), with none denoting and some i denoting end node . It builds finite-step taboo path probabilities and defines by the ratio above, rather than by a closed-form solution or by the three-state reduction. The two-player saddle predicate is a separate generic definition; the paper-specific model supplies its strategy types and payoff. The definitions use real probabilities. The conditions , , , , , and are explicit. They make the relevant conditioning event nonempty and ensure the natural-number indices and mean the intended periods.
Lemmas 1–2 count the attack start as and count interception by ; the model instead uses at departure and later transitions from the attack-start state. Lemma 3's printed claim that odd makes delay two uniquely optimal conflicts with Proposition 2 at . The milestone states a corrected strict claim under , for all , and records the discrepancy. Contributions to the model's finite-path identities, the three-state symmetry reduction, the numbered lemmas, the case propositions, and the even-duration interior maximum are all within scope.
Many allocation problems in online advertising are decisions about order, not only about membership. A search engine that rewrites an incoming query into one of several ad-matching configurations, or a publisher that runs a sequence of ad allocations over a day, extracts revenue that depends on which configurations are used and on the order in which they are applied: advertisers' budgets are spent down along the way, so a configuration run early changes what a later one can earn. Classical submodular set functions cannot express this order dependence, and the guarantees developed for them do not apply directly.
Alaei, Makhdoumi and Malekian (arXiv:1009.4153v4; Management Science, 2021) introduce sequence functions, which assign a value to every finite sequence of actions, and identify a sequence analogue of monotonicity and submodularity under which a simple greedy rule is provably near-optimal. They apply the discrete version to query rewriting in sponsored search and a continuous version to online ad allocation with budgets.
Timeline:
Let be a finite set of actions. A discrete sequence is a tuple with and every ; for it is the empty sequence . Its length is , and denotes the set of all discrete sequences. The concatenation lists the elements of followed by those of . For the refinement is its prefix of length , with .
A sequence is dominated by , written , if can be obtained from by removing some of its elements while keeping the order of the remaining ones. Thus but .
A discrete sequence function is any . The marginal value of appending after is
The function is sequence-non-decreasing if whenever , and (display (10)). It is sequence-submodular if
(display (11)): appending the same sequence gains less after a longer history. Assumption 2 requires both properties.
The optimization problem (12) is, for a length budget ,
For , a sequence is -greedy if at every step its choice is within a factor of the best single-action marginal value (display (13)):
Under Assumption 2, for every , every -greedy of length and every sequence with ,
Applied to the optimum of (12), this is the paper's display (14), .
For sets, the bound of Nemhauser, Wolsey and Fisher is the reference guarantee for greedy selection. Theorem 3 transfers it to sequences: any objective that can be shown sequence-non-decreasing and sequence-submodular inherits a guarantee for a greedy rule, with no further analysis. The paper uses this for query rewriting (Theorem 4) and, through the continuous analogue, for budgeted online ad allocation (Theorem 2). The parameter covers the common situation in which the best next action can only be found approximately, for instance by solving a subproblem with an approximation algorithm.
Theorem 3 is proved in the paper. As far as a search of the Prove2Me catalog shows, no sequence-function model and no sequence-submodular greedy bound has been formalized there; set-function greedy bounds exist on the platform only as separate, set-based statements. This mission produces a machine-checked version of the discrete model and of the guarantee, which later missions on sequence or string submodularity can import.
The set-function argument compares the greedy set with the optimum by adding the optimum's elements one at a time to the current greedy set and using that the union is at least as valuable as the optimum. For sequences the comparison object is , and two features of the order break the direct transcription. First, sequence-submodularity only compares marginal values after a dominated history, so each comparison has to be arranged so that the shorter history is a subsequence of the longer one, in the right order. Second, the averaging over the elements of produces a factor , while the recursion needs the uniform factor ; the replacement relies on feasibility together with nonnegativity of , which comes from monotonicity. A formal proof also has to handle the indices of the refinement and the edge cases , and that the printed argument passes over.
All declarations live in the namespace SeqSubmod.Discrete.
List S over a type S with [Fintype S]; concatenation is ++, the empty sequence is [], and is A.length.List.Sublist (A <+ B), the subsequence order. It is neither the prefix order nor the subset order of the underlying sets.marginal u B A := u (A ++ B) - u A is , with the arguments in the paper's order.H[i] is the paper's and H.take i is . The maximum over is Finset.univ.sup', which needs [Nonempty S]. This is added and harmless: with no actions the only sequence is empty.A trivializing formalization is ruled out: a prefix or subset order, a reversed (11), a dropped , or an existentially quantified would each change the theorem, and none is used.
A complete development needs telescoping sums of marginal values along a list, an averaging argument over a finite sum, the recursion (40), and the inequality , which Mathlib provides. The definitions file is reusable by any later work on sequence functions, including the continuous model of the paper's §3, which is not part of this mission. Proofs of the milestones, alternative proofs of the goal, and tightness examples are all welcome contributions.
A defined benefit pension promises payments whose form depends on a member's employment and retirement status at death, and on the existence and later survival of a qualifying dependent. The same member can generate very different death benefits while employed, after leaving with preserved rights, or after retirement. A scheme may specify a salary-related lump sum before exit, a revalued preserved-rights benefit in deferment, a spouse's continuing pension after death, and instalments under a fixed pension guarantee. Coordination rules determine which payments coincide.
This mission formalises a finite-horizon actuarial contract in which the payable cash amounts and their dates follow explicit benefit switches, rather than being inferred from names such as “spouse's pension” or “death benefit”. The pension and multiple-state foundations are described by Dickson, Hardy and Waters (2020), Chapters 8–11, https://doi.org/10.1017/9781108784184. The contractual rules here are independently defined examples.
Scheme rules and governing documents determine legal entitlement and tax treatment. No salary multiple, spouse percentage, contribution refund or guarantee is universal.
Time is measured in integer anniversary ticks, numbered from valuation time zero. Let be a finite mortality horizon, the employment exit tick and the pension commencement tick. The coherent contract satisfies . A member death-year index means death occurs during and a death-related lump sum is paid at tick . The terminal index denotes no death within the observable horizon. A dependent's corresponding death index is , with the same convention. A same-tick death is treated as non-qualifying; within-year ordering needs a finer model.
The joint mortality law has masses summing to one. At member death , is the probability of a qualifying spouse, conditionally independent of the hypothetical dependent death index given . A spouse qualifies only when , then receives payments while . Eligibility is fixed at death; later mortality is checked at each due date.
An active death has , a deferred death has , and a retired death has . Define benefit amounts , and at settlement for these disjoint regimes. The active benefit can include an optional salary multiple, an accrued-service amount and a contractual refund. The deferred death lump uses preserved annual pension multiplied by revaluation and an explicit pension-to-capital factor measured in years; any contribution refund is a separate cash amount. The retired benefit is a distinct lump-sum rider if the scheme provides one. No component is automatically cumulative with another merely because both appear in the model.
Let be the original member pension payable at anniversary , conditional on the member surviving that date. Let , and be survivor pensions fixed from the death regime, with survivor indexation multiplier . The amounts can reflect salary or service to death, preserved rights, or a fraction of a retirement pension. The main survivor contract pays for ; a separate immediate alternative allows . Amounts are per instalment, with consistent monthly units when required.
A retirement guarantee of ticks covers pension due dates . After a retired member dies, remaining guaranteed member instalments continue to the contractual recipient. Under the parallel rule the surviving spouse also receives its separately payable pension. Under the replacement rule the survivor pension is suppressed while the guarantee remains payable, then resumes when eligible after its expiry. A separate commutation switch can replace all unpaid estate-guaranteed instalments with one lump sum at death settlement, priced using consistent forward discount factors. No guarantee or payment alternative is universal.
Existing joint-life mathematics provides basic survivor occupancy identities. This mission extends them to the three death regimes. For and :
The indicators are pairwise disjoint, preventing multiple death-regime claims.
The second family constructs the realised present value for a full benefit contract from the paid lump sum and the dated instalments. Write for the discount factor to time zero and for the sum of original member pension, qualifying survivor instalment and remaining guaranteed payment under replacement switch . Then
The death lump is zero for the censored member state. The instalment horizon obeys in the root: right-censored members and spouses remain alive at every priced tick. Extension beyond needs a new mortality model.
The principal target establishes an equality between mortality-event valuation and the payment-date component EPVs, together with a second equality accounting for guarantee coordination. With for expectation over the actual member and dependent death cells, for the separately priced death, member, spouse and guarantee payment streams, and for the qualifying retiree-survivor pension suppressed during the guarantee:
The overlap is separately priced using , survivor mortality, death regime and payment eligibility. It is not introduced as a residual defined by subtracting two values.
The event-based formulation follows member status and the amount payable at death. The payment-date formulation uses explicit mortality conditions at each cashflow date, as in the valuation models of Dickson, Hardy and Waters (2020), Chapter 11, https://doi.org/10.1017/9781108784184. Agreement provides an auditable reconciliation between those independently constructed views. Where the spouse receives income while guaranteed member payments continue to an estate, valuing the two promises separately is appropriate. Where a contract suppresses that survivor pension, the overlap term quantifies the adjustment required to prevent charging for both.
Supporting targets cover exit, retirement and guarantee endpoints, and frozen survivor entitlement. Further results mix dependent-age mortality scenarios and value child pensions with an explicit cessation age.
A death benefit calculated from salary or preserved rights at a member's death differs from a pension instalment conditional on living at a subsequent payment date. Moving from a double sum over member and dependent death times to a sum over payment dates must respect that distinction. In particular, multiplying an unconditional probability of marriage at every later instalment would introduce a new eligibility test absent from the contract. The overlap between an estate guarantee and a spouse pension creates a second risk of overvaluation when the intended rule replaces one stream with the other.
Boundary cases are sensitive to strict and weak inequalities. A guarantee ending at has no payment at that endpoint under the due-in-advance anniversary convention adopted here. Same-grid member and dependent death is not automatically resolved by a continuous-time assumption. The project therefore has to distinguish mathematical cashflow identities, genuine survival-law properties and scheme-specific premises throughout its theorem graph.
Lean 4 represents joint death-year cell masses and real-valued finite sums with targeted Mathlib imports. It supports arbitrary dependent-life mortality associations and user-supplied discount factors, salary schedules, preserved rights, revaluation multipliers and survivor indexation. Salary multiples, contribution refunds, deferred benefit valuations and retirement lump sums are switches or amounts supplied by a contract. The retirement guarantee has zero, parallel and replacement regimes. Payment streams may be represented on a finer integer grid to accommodate monthly schedules, but no mathematical identity in the annual kernel asserts exact continuous-payment equivalence.
The principal theorem assumes a normalised joint mortality law, , and . The event-to-payment equality follows from explicit realised payments, not a vacuous equality hypothesis, independence assumption or constant-rate restriction. It relies on genuine death-year and survivor eligibility indicators, rather than stipulating valuation equality in the hypotheses. Continuous-time integration and stochastic marital-history transitions remain future extensions. Finite spouse age-difference mixtures and age-limited child payments are included as separate supporting results. Statutory GMP/excess floors and pension tax rules are outside the contractual core until a scheme type and applicable legal basis are separately verified.
We develop a theory of exact transmission of finite-dimensional -algebras through quantum channels. These algebras describe hybrid classical-quantum information, allowing the dimension of the quantum system to depend on the classical message. Allowing arbitrary encodings and decodings yields a transmission set of algebra types, ordered by embedding, that unifies zero-error information theory with operator-algebraic error correction. We ask if this set admits a dominating algebra into which every transmittable algebra embeds. Our central finding is that domination can fail even in small dimensions. In its absence, several incomparable maximal algebras can describe different optimal uses of the same channel, forcing the user to select one depending on the operational task and the type of information to be preserved. We introduce hybrid capacities that reconstruct the only possible dominating algebra type and present a complete finite characterization of domination using minimal forbidden algebra types. We identify dominating algebras for channels whose operator systems are graph-isomorphic to -algebras, including highly divisible channels, and for channels with zero one-shot zero-error quantum capacity. Under tensor products, we prove that joint coding can produce new algebra types, giving an algebraic analogue of superadditivity from Shannon theory. Domination can fail for the joint use of two channels, even when both channels separately admit dominating algebras. Finally, we construct a channel whose -fold tensor powers have doubly exponentially many maximal algebra types, attaining the largest possible growth scaling for finite-dimensional channels. Consequently, new transmittable algebra types appear at arbitrarily large block-lengths for this channel, so its full transmission structure cannot be generated from any finite collection of bounded-block-length codes. △ Less
This mission is the statement-level formalization of Transmitting algebras through quantum channels (arXiv:2609.40054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main nonexistence result; Example 4.2 and (4.3) (Main nonexistence result; Example 4.2 and (4.3), PDF p. 30). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
Firms that already buy a service from an incumbent supplier regularly re-source the contract: they invite new suppliers, the entrants, to compete in a descending open-bid auction. Entrants may be cheaper but are unproven: before the contract can be awarded to an entrant, the buyer must pay for qualification screening (visits to the supplier's facility, purchasing and testing sample products), and an entrant passes only with some probability. Industry practice splits into screening every entrant before the auction (pre-qualification) and screening only the winner after it (post-qualification). Zhang, Chen and Katok, “Now or Later?” When to deploy qualification screening in open-bid auction for re-sourcing, Operations Research 69(6), 2021, compare the two formats in equilibrium.
In the post-qualification format (POST), the incumbent needs no screening, so he faces a genuine dynamic decision: as the clock price falls and entrants drop out, when should he quit? His drop-out price determines the buyer's procurement cost in POST, and Theorem 2 of the paper characterizes it completely. This mission formalizes that theorem.
Costs lie in an interval . The incumbent's cost is . There are entrants with i.i.d. costs of density and c.d.f. , supported on . Screening one entrant costs the buyer , and an entrant passes with probability . In POST, the clock descends from ; when the incumbent drops out at price , the price jumps down by the decrement , and the incumbent ends up with the contract at price only if all remaining entrants fail screening. The paper assumes and Assumption 1: is nondecreasing and convex.
Before the incumbent quits, an entrant with cost stays until the price reaches his effective cost . With entrants left at price , the highest remaining entrant cost therefore has c.d.f. and density . Writing , the incumbent's value solves the Bellman system (8)–(10):
Here is the planned drop-out price. The integral covers the event that an entrant drops out first, at price ; the second term covers the event that the incumbent quits at and all entrants then fail screening.
Theorem 2 introduces four objects. is the floor of the minimum over of . The compete threshold is the first price at which falls below . The switching price is the least price above at which quitting is worth as much as competing down to . The candidate drop-out rule is .
For all , and :
and . The goal also asserts that are well defined and satisfy . It asserts the monotonicity of part (i): and are nondecreasing in , is nonincreasing in , and is nonincreasing in and nondecreasing in . Finally, is nondecreasing in and and nonincreasing in .
The proof in the e-companion (pp. ec5–ec11) provides the milestones, in attack order:
The theorem turns an infinite-horizon-looking stopping problem into a compete-or-fold rule. Either the incumbent stays in until the price falls to the threshold , or he drops out immediately. The choice depends only on how many entrants remain and on whether the price is above the curve . With Lemma 2 and Theorem 1 (the entrants' strategies), this completes the equilibrium of POST. The paper's comparison of POST and pre-qualification, and its closed form for the buyer's expected cost, both rest on this equilibrium.
The result is proved in the paper; it has not been machine-checked. A formal proof would check a long argument with an intricate induction: Lemma EC.2 interleaves the strict monotonicity of with the monotonicity of in and . It would also check the treatment of the boundary case , where the proof appeals to the convexity in Assumption 1.
The obvious argument differentiates in and reads off the sign. That fails because the derivative involves , which is itself the value of an optimization. Its sign is controlled by the explicit function only after an induction on shows that has the form wherever it matters. The induction must carry the ordering of , and across different and (Claim EC.1) at the same time. Another difficulty is that must be evaluated beyond the current price: is defined at the reference price and may exceed .
All prices and costs are real numbers, and is a natural number with . The standing assumptions (including Assumption 1) are hypotheses of every statement. One hypothesis is added to the page: is positive and continuous on . The page's own formulas divide by and differentiate (9) in . is defined as , not taken as a parameter, and is the integral of .
The max in (8) is a real supremum over the compact feasible interval; that it is attained is part of the goal. The integral in (9) is a signed interval integral, so is given by (9) for as well. The minimum defining is read as an infimum over , because the ratio has a zero denominator at . The page's is taken over the reals. "Optimal drop-out price" means a maximizer in (8): at two maximizers exist, so uniqueness would be false. The derivative (EC.7) is stated away from the kink . Milestones use the open price domain the proof uses.
The game-theoretic layer is not modelled. The hypothesis "entrants follow Lemma 2 and Theorem 1" is how the page derives (8)–(10), and the statement is about (8)–(10). A formalization that states only the sign pattern of or the inductive hypothesis would be trivializing; the goal states optimality of in (8) for every , , , together with part (i).
A development needs differentiation under a parametrized integral (the fundamental theorem of calculus for ), continuity of in , and real-analysis facts about convex functions crossing a line. These are reusable for other auction and optimal-stopping models. Proofs of any milestone are welcome, as are proofs of the fold-only case independently of the compete case.
Restaurants, clinics and amusement venues that announce a waiting-time standard compete not only on price but on how unpleasant the wait feels. Waiting-area entertainment (a piano player, a television, a play area) lowers the perceived cost of waiting, and when several providers sit in one service cluster, a food court, a mall, a strip of restaurants, a single entertainment option can serve all of their customers at once. Yuan, Dai, Chen and Gavirneni (MSOM 2021) model this choice and ask when providers that compete on price but jointly fund entertainment, a form of co-opetition, do better than a single provider serving the market alone.
The model builds on the waiting-time-standard and volume-based capacity framework of Allon and Federgruen (Operations Research 2007) and on linear cost-allocation schemes of the yardstick type. Its central comparison concerns the even cost split: does sharing the entertainment bill outweigh the margin lost to price competition?
Customers arrive at a provider as a Poisson stream and the service time is exponential. With service fee and entertainment level , a local monopolist faces the arrival rate
where is the maximum demand rate, the price sensitivity, the waiting cost per unit time, the announced waiting-time standard and the effectiveness of entertainment. Entertainment costs with . To keep the expected wait at the provider buys service rate at marginal cost , so its profit is
The monopoly profit is the greatest value of over , .
Under co-opetition two symmetric providers share one entertainment level. Write , , margins , a price-competition intensity and . Provider 's arrival rate is . The cost is split by with cost-sharing factor , and provider earns
Providers first set margins simultaneously; then they jointly choose to maximize . A symmetric equilibrium has , jointly optimal at , and no deviation , followed by the joint optimum it induces, raises a provider's profit. The equilibrium profit is . Throughout, the parameters satisfy and .
With an even split () there is a threshold such that, for every and every symmetric equilibrium at ,
No value of is fixed: the goal asserts only the threshold shape of the comparison.
and . 2. Proposition 3(i) at . A symmetric equilibrium exists, and every one satisfies
The result separates two effects of clustering. Sharing one entertainment option halves each provider's cost, which supports a higher entertainment level and more demand; price competition erodes margins. Proposition 7(ii) says that, under an even split, the comparison with a local monopolist is decided by a single cut-off in the competition intensity, which is what lets the paper conclude that co-opetition can restore monopoly profit levels when competition is mild, and it is the reference point for the paper's analysis of unequal cost-sharing rules (Propositions 6 and 8) and of the design of cost allocation.
The paper's proofs sit in an online supplement; no machine-checked proof of any of these statements is known. Formalizing them produces a verified analysis of a two-stage game with a joint second stage, including the existence of the symmetric equilibrium, which the paper uses but which requires a global, not first-order, argument.
The co-opetition equilibrium is defined by a two-stage game: a price deviation changes the jointly chosen entertainment level, so a provider's payoff as a function of its own price is a composition with an argmax and need not be concave. Verifying that the first-order point of Proposition 3 is a global best response, and that every symmetric equilibrium satisfies the first-order conditions, is the step a direct first-order computation does not deliver. The threshold of Proposition 7(ii) then requires comparing an implicitly defined equilibrium profit, through its root equation in , with the implicitly defined monopoly optimum, and showing that the difference changes sign exactly once in ; monotonicity of alone does not give a sign change.
Everything is real-valued. Prices are encoded by margins , for the equilibrium and for every deviation, matching the page's domain . The joint entertainment stage maximizes over , and a deviation is evaluated at every joint optimum it induces. is any greatest element of the set of monopoly profits over , . The goal and milestones fix ; Proposition 3 for is out of scope.
Disclosed conventions: the capacity bound is the strict instead of the page's (at equality a degenerate profile with zero margins and no entertainment makes both profits equal to and falsifies the strict clause); the demand is read as , as in §3 and Proposition 3(ii), since the §4 display double-counts ; the cost share is read as , the first of the page's two inconsistent forms (they agree at ); "decrease" is strict; "the opposite holds" is the strict .
The goal is stated about genuine equilibria of the game and the genuine monopoly optimum. Replacing by the closed form of Proposition 3, or by the formula of Proposition 1, would turn the goal into a one-variable real-analysis fact and is not the paper's statement.
A complete development needs: the monopoly first-order analysis (joint concavity on , ); strict concavity of the joint second stage for positive total margin; the envelope argument for a provider's deviation; existence of a symmetric equilibrium; implicit-function comparative statics in . Lemmas on implicitly defined roots of type equations are reusable. Contributions of intermediate lemmas, including the existence of the equilibrium, are welcome.
Many financial assets (corporate and municipal bonds, swaps, asset-backed securities) trade over the counter (OTC): there is no central exchange, and a trade requires that a buyer and a seller find each other. Empirically, a large share of OTC volume passes through intermediation chains, in which an asset moves from the original seller to the final buyer through several dealers. Search-theoretic models explain how such chains form. Duffie, Gârleanu and Pedersen (2005) introduced continuous-time search and bargaining in OTC markets, and Hugonnier, Lester and Weill (2016) let investors' valuations take a continuum of values, so that dealers emerge endogenously as the investors with intermediate valuations.
Shen, Wei and Yan add a search cost: an investor who looks for a trading partner pays a flow cost . Investors with extreme valuations then prefer to stay out of the market, and participation becomes an equilibrium choice. The paper's Theorem 1 is the foundation of everything that follows in it: every proposition on chain length, trading volume, price dispersion and welfare is stated "in the equilibrium of Theorem 1".
Time is continuous. A continuum of investors of total mass trades an asset in supply , with ; each investor holds or unit, and the asset pays a coupon of per unit of time. An investor of type values the coupon at . Types are redrawn independently at intensity from a probability density on with c.d.f. . Everyone discounts at rate .
A non-owner either stays out or searches to buy; an owner either stays out or searches to sell. Searching costs per unit of time. Write for the densities over types of buyers, sellers, inactive non-owners and inactive holders, and , . A buyer meets sellers at rate and a seller meets buyers at rate , with .
Let be the values of the four activities, and . When a type- buyer meets a type- seller, the surplus is
they trade iff , and the buyer, with bargaining power , pays .
For cutoffs , , non-owners search to buy iff and owners search to sell iff . A steady-state intermediation equilibrium (Definition 1) consists of cutoffs , densities satisfying the flow balances (12)–(18) and market clearing (19), and value functions solving the Bellman system (8)–(11) under which these cutoff rules are optimal. Types in are the intermediaries: they search to buy when they hold nothing and search to sell as soon as they hold the asset.
There is an explicit threshold , built from the right-hand sides of the cutoff equations
with , the explicit functions (66), (64) of , , such that for
a steady-state intermediation equilibrium exists, and every such equilibrium has cutoffs equal to the unique roots of (20) and (21), densities (55)–(63), value functions (79)–(82), and the trade rule "trade iff " with prices (6).
The milestones follow the paper's proof. Step I solves the flow equations for given cutoffs: (55)–(57), (61)–(63), the populations (64) and (65)–(66), and the densities between the cutoffs (58)–(60), together with the existence of the steady state. Step II derives the slopes (77)–(78), the value functions (79)–(82), the trade rule (83)/(7), the cutoff equations (20), (21) with their unique roots, and the threshold (84). Step III shows that the cutoff rules are optimal for the closed-form values.
Theorem 1 gives a closed-form description of an OTC market with endogenous participation and an endogenous dealer sector. The search cost splits the population into three groups (passive low types, intermediaries, passive high types), and the length of intermediation chains, trading volumes and price dispersion are all computed from the explicit densities and value functions. Every comparative-statics result of the paper (for example, that a lower search cost lengthens chains) is a statement about the equilibrium this theorem constructs.
The result is proved in the paper, with gaps: the verification of the trade rule outside the dealer region is called "straightforward", Step III treats one of four cases, and uniqueness of the solution of the Bellman system is not argued. No part of it is machine-checked. The mission asks for a complete formal proof, and its definitions give a reusable Lean model of a continuous-time search-and-bargaining steady state with endogenous participation, which no existing formalization provides.
Step I is not just algebra. Between the cutoffs, the flow equation (18) couples each density with integrals of the others, and its solution comes from a Riccati-type equation for . As printed, the densities (59)–(60) do not solve it. Step II differentiates parametric integrals of the positive part of the surplus, which needs the monotonicity of before that monotonicity is proved. That uniqueness is the main gap: the paper takes it for granted. Monotonicity of the right-hand sides of (20)–(21) in the cutoff rests on decreasing and increasing, which is asserted, not shown. The obvious approach, plugging the closed forms into Definition 1, gives only existence; uniqueness requires showing that every solution of the flow equations and of the Bellman system is the closed-form one.
All quantities are real numbers; is written lam and is Δbar. The standing assumptions are , , , , and a probability density on (nonnegative, integrable, total mass ); and . The densities are required to be nonnegative and integrable, and the value functions bounded and measurable on , so that no integral takes Lean's default value .
The equilibrium predicate is Definition 1 itself: flow equations (12)–(19), Bellman system (8)–(11) multiplied through by , and optimality of the cutoff rules ( below , above, and likewise for owners). The closed forms are separate definitions, and is defined from (20)–(21) as the common value of their right-hand sides at the crossing point; it is never a parameter. A formalization that defined the equilibrium by its closed form, or took as a hypothesis, would make the goal trivial and is excluded.
Corrections and conventions, all disclosed in the items:
The definitions are split into a model module (parameters, steady state, Bellman system, optimality, equilibrium, prices) and a closed-form module (, , the cutoff equations, , densities, slopes, value functions). The model module is reusable for the paper's later results (trading volumes, chain length, comparative statics in , , , ) and for the non-intermediation equilibrium of its Theorem 2. Proofs of individual milestones, and lemmas on the monotonicity of , and of the cutoff equations, are welcome as separate contributions.
Collaborative projects often assign different tasks to different firms while making each firm bear part of the cost of a late project. A supplier's decision to spend more time on its task can therefore impose delay costs on a manufacturer, and the manufacturer's own schedule can impose costs on the supplier. The incentives differ from those of one firm controlling the whole schedule. Song, Zhao, and Xu study this tension in a two-stage project and ask whether knowing the other firm's costs always improves the final schedule. Their answer includes a precise case in which the project finishes sooner when the supplier does not know the manufacturer's cost type. The held source is the authors' SSRN preprint, §§3–5.1 and Theorem 6; it was later published in Manufacturing & Service Operations Management.
The question matters for partnerships in which task costs are private but delays affect all participants. In such a setting, a change in information can change the supplier's first move, even though the manufacturer's final decision still responds to the work already done. The result concerns project duration, a directly observable outcome, rather than an abstract welfare comparison.
A serial project has one supplier task followed by one manufacturer task. The supplier is firm 1 and moves first. The manufacturer is firm 0, observes the supplier's action, and moves second. Each action is either keep (), retaining the benchmark task duration, or delay (), adding one period to that task. The project's delay relative to the benchmark is the number of delayed tasks: zero, one, or two periods. The paper considers this deterministic-duration setting under Assumption 1(b) and Condition 2 (preprint, pp. 10–12).
Firm saves in direct cost when it delays its own task. The first period of project delay incurs a shared penalty ; the second adds . The subscript identifies the firm that pays a share, and the superscript identifies the period of project delay. Each firm pays its share whenever the project is late, regardless of which firm caused the delay. For example, the profile gives the supplier payoff and the manufacturer payoff , while gives and . These are the payoffs in Figure 5b (preprint, Appendix p. 1).
Under symmetric information, both cost types are known. The outcome is a subgame-perfect equilibrium: the manufacturer chooses a best response after either supplier action, and the supplier chooses its preferred first action in light of those responses. Under asymmetric information, the supplier instead has a belief over possible manufacturer types. The belief assigns masses , , and to types with low, medium, and high savings relative to their two penalty shares. The supplier maximizes its expected payoff under that belief. The actual manufacturer, whose type need not coincide with the supplier's guess, still acts after seeing the supplier's choice (preprint, Assumption 2, p. 16).
The goal is the paper's Theorem 6. Let the two equilibria use the same supplier type and the same actual manufacturer type. Write and for their respective project delays. Away from payoff ties, the mission asks for the exact characterization
The milestones establish the manufacturer's dominant actions (Lemma 2), the supplier's action against manufacturer best responses (the supplier clause of Lemma 2), the five symmetric equilibrium cases (Theorem 2), and the asymmetric supplier decision threshold (Theorem 5). The final milestone is the paper's observation that only Case 2 of the symmetric equilibrium table can lead to a strictly shorter project under asymmetry. Their statements and indices come from the held preprint, pp. 12 and 17 and Appendix p. 5.
The characterization identifies exactly when less information changes a one-period symmetric outcome into a zero-delay asymmetric outcome. In the relevant regime, the manufacturer would keep after either supplier action. The information change matters because the supplier's belief may make keeping its own task more attractive than it is when the manufacturer's low-saving type is known. Outside the stated regime, the same model does not yield a strictly shorter project through this information change. This bounds the paper's counterintuitive claim to explicit, checkable cost and belief conditions (Theorem 6, p. 17).
Song, Zhao, and Xu prove the result in the paper. The mission's Lean statements are compiled, but the theorem proofs remain open. Formalizing them would create a machine-checked account of the complete two-stage game, its equilibrium predicates, and its belief-dependent outcome comparison. The general sequential-game interface and the finite-belief representation can support other small extensive-form games; the project payoffs and time-dependent risk-sharing conditions are specific to this paper. Contributions to the equilibrium lemmas, the belief threshold, and the final comparison are all useful.
One cannot compare the supplier's actions while holding the manufacturer's action fixed. The manufacturer responds after observing what the supplier did, and a medium-saving manufacturer changes its response between and . Nor can one infer the actual manufacturer's response solely from the supplier's belief: believed types determine the supplier's expected payoff, while the actual type determines the second move. These two dependencies make a simple comparison of isolated payoff entries insufficient. The strict case table also omits ties, and the paper's “keep otherwise” at the belief threshold requires care when an equilibrium is defined by weak payoff maximization.
Lean represents savings and penalty shares by real numbers, actions by a two-constructor type, and project delay by a natural-number count of delayed tasks. Assumption 1(b) and Condition 2 are bundled in a standing predicate: , , , and . Positive savings are explicit, as required by the paper's cost interpretation and used in its proof of Lemma 2. A separate genericity condition excludes equality at the four individual payoff thresholds. The goal also excludes : at that tie the paper's printed Theorem 6 and Theorem 5's “keep otherwise” convention do not determine the same strict if-and-only-if claim under weak best response.
The belief has finite support, nonnegative weights, and total weight one. Its class masses are computed from those types; they are never free probability parameters. Believed types satisfy Assumption 2's class ordering, but need not satisfy Condition 2's global-optimum inequality for the actual project. The actual manufacturer's type need not be in the belief's support. Symmetric and asymmetric equilibria are predicates over complete strategies, and the target quantifies over their outcomes. Theorem 5 uses a payoff-based decision rule that selects keep when expected payoffs tie, matching its “keep otherwise” clause; the goal excludes that tie. Defining the symmetric outcome by Theorem 2's table or the supplier's asymmetric action by Theorem 5's threshold would erase the mathematical content, so both are derived from the payoffs.
Patrolling protects a border or facility perimeter against an intruder who needs uninterrupted time to complete an attack. The defender controls when patrollers pass; the attacker controls when to strike. In a patrol game, the question is how to time patrols when the attacker can observe them (Lin, Optimal Patrol of a Perimeter).
An observing attacker can wait until a patroller has passed before starting. Lin's result shows that a randomised schedule still gives the defender the same optimal detection probability as against a blind attacker, in closed form.
Fix three parameters: a dispatch rate , an attack duration and a detection probability .
Defender. A pure strategy is a nondecreasing sequence of times in at which patrollers pass a fixed location. With the number of patrollers dispatched by time , the sequence is feasible if it satisfies condition (1) of the paper,
A mixed strategy is a probability measure on sequences under which almost every sequence is feasible.
Attacker. The attacker chooses an operating window with , watches the patrollers go by, and at a time of his choosing starts an attack that occupies and must end by . The choice of may depend on everything observed up to and including time : it is a stopping time of the arrival process.
Payoff. Each patroller passing during the attack detects it independently with probability . If the attack meets patrollers it escapes with probability , so the detection probability of against is
The defender moves first and maximises; the attacker responds and minimises. This Stackelberg game is . Its value is (2):
The claimed optimal schedule puts blue patrollers deterministically at , with , and . It puts a red patroller at each independently with probability . When is an integer there are no red patrollers, and the blue ones pass at fixed intervals of .
For all , , :
Items 2 and 3 state , attained at .
The result. Watching the patrollers gives the attacker no improvement in the game value. The value interpolates at , giving a closed-form trade-off between patrol rate, attack duration and detection reliability. The same schedule supports the paper's Theorem 3 (invisible patrollers) and Theorem 4 (a whole perimeter).
Formalizing it. The paper proves the result; this mission seeks a machine-checked proof. The development must specify the attacker's information, almost-sure feasibility of the random schedule, and the converse. It also supplies a reusable model of continuous-time patrol games with adaptive attackers.
For a fixed window, the blue count is fixed and its red slot is independent. An observing attacker instead chooses a stopping time from past arrivals. The proof must account for which red slots he has seen. The half-open window matters: with , an attacker starting at an empty red slot meets only patrollers.
The converse is harder because a feasible mixed strategy may have infinite expected count in every window even when each path has rate . An argument based only on the expected count therefore fails.
Lean namespace PerimeterPatrol.Visible. Schedules are maps (patroller passes at ) with the product -algebra. Feasibility requires Monotone s, , and the limit (1) along atTop, with counts given by Nat.card. A mixed strategy is an IsProbabilityMeasure that is almost surely feasible. The attacker's information up to time is the -algebra generated by the counts , . An attack is a start-time rule with a fixed window , , such that is measurable for that -algebra for every . The detection probability is a Bochner integral of a -valued function. is the pushforward of i.i.d. uniform draws on , with the red patroller at present iff the -th draw is below .
Conventions committed to:
Nat.floor and Nat.ceil, exact for positive arguments;The attacker class includes measurable adaptive stopping times; the optimal schedule must be a probability measure; and the value is characterized through the two game inequalities rather than an unrestricted real supremum or infimum.
Needed infrastructure: counting functions of nondecreasing sequences, the stopping-time and independence argument for the red slots, the strong law of large numbers (Mathlib's ProbabilityTheory.strong_law_ae) for the long-run rate of , and an averaging argument over start times for the converse. The counting and stopping-time lemmas for point processes on are reusable beyond this mission. Proofs of any milestone, and alternative routes to the converse, are welcome.
Not formalized here: Theorem 3 (p. 9) as a separate item, Theorem 4 (the perimeter game, p. 10), Theorem 5 (the finite-horizon simultaneous game, p. 11) and the remarks of §2.1 and §5.
Every day a hospital ward with a fixed number of beds decides which patients go home. Sending a patient home early frees a bed for the next admission, which matters when the ward is congested and arrivals board in the emergency department or elective surgeries are cancelled. Sending a patient home too early raises the chance that the patient is readmitted, which is costly for the patient and, under the U.S. Hospital Readmissions Reduction Program, for the hospital. Shi, Helm, Deglise-Hawkinson and Pan (SSRN 3202975; Operations Research 2021, doi:10.1287/opre.2020.2044) model this trade-off as a Markov decision process over a census of patients indexed by class and length of stay (LOS), fit personalized readmission-risk curves to hospital data, and implement the resulting discharge policy at a partner hospital.
The structural question behind their policy is who to discharge first. Hospitals usually rank patients by their current, absolute readmission risk. The paper's Theorem 2 (p. 15) instead ranks types by how fast that risk falls with a further day of stay: a type whose risk curve is flatter from now on should be discharged before a type whose risk is still dropping quickly. This mission formalizes that ranking result, in a corrected form.
There are patient classes and a maximum length of stay . A type is a pair of a class and a LOS . A state counts the patients of each type, and the census is . A discharge action counts the patients of each type sent home. Class has a minimum LOS , and an action is feasible at when (3), for (4), and every patient at LOS leaves.
Between two daily decision epochs and , new patients and readmitted patients arrive at LOS , and every patient who was not discharged ages by one day: (5) and (6). Each epoch costs the holding cost for beds (7), plus the discharge cost (8), where is the readmission risk of a class- patient discharged at LOS and is the readmission penalty. Each risk curve is continuously differentiable and nonincreasing in the LOS.
Strong dominance (Definition 1, p. 14): iff
Writing for one discharge of type , a schedule with trajectory over a horizon has total cost .
For an initial state, an arrival path and a horizon , let with , and . Then every feasible schedule has a feasible schedule with such that, for all ,
Since the feasible schedules are finitely many, some optimal schedule discharges a patient only after all patients.
Theorem 2 is the paper's main structural result. It turns a high-dimensional MDP, whose state is a census over types, into a ranking problem: once types are ordered by strong dominance, the remaining decision is how many patients to discharge (Corollary 1, p. 16), which the paper then approximates with a univariate linear-quadratic heuristic (§5). The ranking also has a direct operational reading: discharge by marginal, not absolute, readmission risk.
No machine-checked version of this result exists. Formalizing it settles exactly which hypotheses the interchange argument needs. Doing so already exposed that the statement as printed is false (see Difficulty), so the mission's output is the corrected theorem with a checked proof, together with a reusable finite-horizon, pathwise model of class-by-LOS patient flow.
The obvious argument is a single interchange: if a patient is discharged at epoch while a patient stays until a later epoch , swap their discharge epochs. The census path does not change, and Proposition 2 shows the discharge cost does not increase. The step that fails is the one the paper defers to Appendix B.3: the dominated patient, kept from to , may pass the maximum LOS before , and then the swap is not available. The appendix's repair does not close the gap. With , , , , no arrivals, , and one and one patient on day , we have , yet the unique optimum discharges the patient alone (cost 1013), and every schedule that obeys the rule costs at least 1014. The added hypothesis guarantees that the dominated patient can wait as long as the dominating one, so the swap always exists.
The remaining difficulty is bookkeeping: the interchange changes two cohorts by over an interval of epochs, and feasibility (counts, minimum LOS, forced exit at ) must be checked along the new trajectory. Repeated interchanges must also be ordered so that fixing one epoch does not break an earlier one.
Fin M, LOS indices Fin (J+1), counts natural numbers, costs real numbers. Epochs start at . Arrivals, new and readmitted, form one exogenous deterministic path, as Remark 4 (p. 12) prescribes for §4. Every statement is pathwise on a finite horizon , the setting of the paper's interchange argument. The long-run average cost (9) is not used, since a finite interchange cannot change it.deriv with the absolute values of (15).intervalIntegral.integral_eq_sub_of_hasDerivAt) and monotonicity of integrals are the analytic substrate for Proposition 2. The trajectory and interchange lemmas about class-by-age cohorts are reusable for other census models. Proofs of any milestone are welcome independently.Not formalized: Theorem 1 (existence of an average-cost optimal policy), Corollary 1 (threshold form), Propositions 1 and 3, and Lemma 1.
Flow networks model the movement of material, traffic, electricity, or gas through connected systems. In many such models, the required net flow at each vertex varies with a parameter, so the object of interest is a whole family of optimal flows rather than one solution. When edge costs are nonlinear, solving a new optimization problem for every parameter value gives no finite description of that family. Joachims, Klimm and Warode study two approximations of this parametric problem: one approximates each edge's marginal cost, and the other interpolates selected optimal flows. This mission concerns their marginal cost approximation result, Theorem 5.
The paper builds on an exact method for piecewise quadratic edge costs by Klimm and Warode. A piecewise linear approximation of each marginal cost has a piecewise quadratic integral, so it brings general convex costs into the class handled by that method. The question is how fine the linear interpolation mesh must be for the resulting flows to be close to optimal under the original costs. The paper gives local step size bounds involving the second derivative of each marginal cost. The target here is a corrected version of that guarantee, with the precise corrections stated below.
A network consists of finite sets of vertices and edges . Every edge has a tail and a head. The graph is strongly connected and has neither self loops nor parallel directed edges. For an edge flow , its net inflow at a vertex is the sum of flows entering that vertex minus the sum leaving it. Two balanced demand vectors determine a demand for . A flow is feasible when its net inflow equals that demand. In the directed case all edge flows are nonnegative; in the undirected case their signs are unrestricted.
Each edge has a marginal cost that is strictly increasing, differentiable, nonpositive on negative arguments, and nonnegative on positive arguments. Its edge cost is . The total cost is the sum of edge costs, and is the minimum total cost of a feasible flow at parameter . These sign conditions make the edge costs nonnegative. The paper calls them homogeneous marginal costs, although this is a sign condition rather than algebraic homogeneity. Section 5.2 gives the model and its approximation criterion.
For each edge, choose a strictly increasing mesh from to , where
The linear spline joins the values of at adjacent mesh points by straight chords. The minimum cost flow function for these spline marginal costs is tested under the original costs: . This convention is essential because a small optimal cost for the spline instance alone says nothing about the cost under .
The milestones follow the paper's argument in order.
The goal is the corrected Theorem 5. It states that either of the paper's two explicit step size regimes, involving , , , and , makes the spline instance's minimum cost flow function satisfy
The first regime bounds each step by a local maximum of and the magnitude of at a mesh endpoint. The second adds monotonicity and sign conditions on and uses its endpoint values. The formal theorem retains the constants , the factor in (18), and both distinct denominators in Theorem 5. Theorem 5, pp. 17–18 is the source for the exact formulas.
The guarantee applies to an entire interval of demand parameters. It converts local numerical accuracy of the marginal cost splines into a bound on the original total cost at every parameter value, while preserving feasibility. The edge flow bound explains why it suffices to approximate marginal costs on a finite interval even when edge flows are otherwise real valued.
The paper proves the intended result by a paper argument, but its printed Theorem 5 has a counterexample when a mesh crosses zero without including zero: the spline can lose the marginal cost sign condition, and at zero demand the spline optimum can have positive original cost while the true optimum has cost zero. The corrected goal records a valid target for machine checked proof. Formalizing it also yields reusable definitions of finite flow networks, convex separable edge costs, parametric approximation, and chord splines. No machine checked proof of this theorem is claimed by this mission.
Pointwise closeness of marginal costs does not directly compare the two optimized flows, which may differ on every edge. A direct comparison at the spline optimum must also account for the original optimum and for how the edge costs accumulate across the network. The interpolation estimate alone does not settle this: a mesh interval crossing zero can change the sign of its chord at zero, even when every step size bound in the printed theorem holds. The shape condition in Theorem 5(ii), read literally with the third differentiability assumption, also forces the second derivative to vanish on the negative half line. The mission keeps that condition as printed rather than silently replacing it with a more symmetric one.
Lean represents vertices and edges by finite types, net inflow by finite sums, and each edge cost by a real interval integral based at zero. A Boolean flag selects the directed case with or the undirected case with no sign constraint. The general finite lower and upper bounds of problem (14) are outside this mission. The optimal cost is the real infimum of feasible costs; the graph and balanced demand assumptions give feasible flows, and the sign assumptions bound their costs below. The spline is computed from its mesh values, with its end chords extended linearly outside . Meshes are indexed from zero in Lean, regardless of the paper's two indexing styles.
The corrected Theorem 5 requires zero to be a mesh point on every edge. In regime (i), it replaces by . In regime (ii), both entries of the factor are square roots of ; this matches the equality used in the printed proof. Lemma 4 and Theorem 5 explicitly require , since both step-size bounds and (15), (16) divide by it (with zero demands, a one-point mesh and , Theorem 5 would otherwise fail), and its second marginal cost family is continuous, strictly increasing, and sign preserving. These conventions and corrections are recorded in the source analysis for Theorem 5.
A proof must use the chord spline determined by and the mesh; replacing it by an arbitrary close function would discard the numerical claim. Likewise, the bound is never a hypothesis of Lemma 4 or of the goal: it is milestone 1, and assuming it would remove the combinatorial half of the argument. Milestone 6 is stated on rather than on all of as printed, because the linearly extended end chord of a convex function lies below it. Contributions to the flow bound, Lemma 4, the spline estimate, or the final connection between them are all within scope. The flow and spline definitions can also support other approximation results beyond this theorem.
A buyer can face public and financial losses when a remote supplier violates labor, safety, or environmental standards, even if the buyer did not cause the violation directly. The buyer and an intermediate supplier can spend resources to help the remote supplier reduce this risk. Their incentives depend on who pays for the effort and who bears the loss when a violation is detected. Huang, Song, and Swinney model these choices in a fixed three-tier supply chain and characterize which firm takes the downstream responsibility effort. Their result gives a precise threshold rule for when the buyer should act, let the intermediate supplier act, or leave both of them idle (Huang, Song, and Swinney, SSRN author version, 2021, §§3–4).
The mission concerns the paper's base model and Theorem 1. It is a known result with a proof in the online supplement to the paper. The formalization target is to reconstruct that result as a theorem about the sequential game itself, with the parameter assumptions and boundary cases stated explicitly. The paper also studies external stakeholder pressure, two-tier comparisons, and variants of the effort model; those later results are outside this mission.
A Tier 0 buyer sources from a Tier 1 supplier, which sources from a Tier 2 supplier. The buyer sells one product with deterministic demand . Each tier has a fixed per-unit margin and chooses responsibility effort at linear cost , with . Only Tier 2 can experience a responsibility violation. Tier 0 and Tier 1 efforts are substitutes: their combined contribution is . Tier 2 effort complements that contribution and also has a baseline return . The effective total effort is therefore (§3.1, pp. 7–9).
An actual violation has probability . Conditional on a violation, the public detects it with probability , so the probability of a detected violation is . Each firm loses a fraction of demand times its margin, plus an indirect financial loss . Its total loss is . The paper's expected profit and loss-adjusted effort cost are
The ratio measures effort cost relative to the firm's loss from a detected violation. The paper assumes , which keeps Tier 2's best response positive even when the buyer and Tier 1 make no effort (§3.2, pp. 10–12, equation (1)).
The game is sequential. The buyer chooses first; Tier 1 observes it and chooses ; Tier 2 observes both and chooses . A best response at either supplier maximizes that supplier's expected profit among nonnegative efforts after the observed history. The buyer anticipates these responses and maximizes its resulting profit. The paper chooses positive effort when zero and a positive effort tie (§3.2, pp. 10–12).
The central target is Theorem 1 on pp. 14–15. The selected buyer optimum has no outcome in which both the buyer and Tier 1 exert positive effort. Its effort choices fall into three Table 2 rows: control, in which Tier 0 acts and Tier 1 does not; delegation, in which Tier 1 acts and Tier 0 does not; and no effort, in which neither downstream firm acts. Tier 2 still exerts effort in each row. Table 2 specifies all three efforts, the actual violation probability , and the detected probability (Table 2 and Theorem 1).
The threshold rule is
The milestone list follows the paper's two supplier best-response lemmas, the buyer's piecewise reduced profit in the proof of Theorem 1, and the comparisons that separate the candidate outcomes. Each milestone is stated about profits and best responses, rather than merely restating a Table 2 row (Lemma 1, p. 12; Lemma 2, p. 13; Online Supplement, p. 1).
The theorem identifies a buyer's optimal responsibility-management regime using the ratios , the Tier 2 baseline , and the model's risk parameters. The distinction matters because a buyer's direct effort can displace the Tier 1 supplier's effort: a low effort cost for the buyer alone does not settle which firm should act. Table 2 also turns the chosen regime into an explicit violation probability, so the result characterizes both private effort and the supply chain's responsibility outcome (Theorem 1 and discussion, pp. 14–15).
The source paper proves Theorem 1; the Lean declarations in this mission are open proof targets. Formalizing them will supply reusable definitions for a three-player sequential effort game and a checked route from the suppliers' optimality conditions to the buyer's full equilibrium classification. Later statements about stakeholder pressure and the two-tier comparison can build on the same model once the base theorem is proved.
Tier 1's best response changes at : below that point it offsets some of the buyer's effort, while above it Tier 1 exerts zero effort. The buyer's reduced profit therefore changes form at the same boundary. Optimizing a single smooth expression across all nonnegative would miss that change. The equality cases also matter: at the control–delegation boundary the two choices have equal buyer profit, and the paper's convention selects positive buyer effort (§4.1 and Online Supplement §A, proof of Theorem 1).
Lean represents all parameters, efforts, profits, and probabilities as real numbers. The three tier indices are explicit fields, and every player's feasible efforts are nonnegative. A separate sequential-game definition gives the argmax meaning of both supplier best responses and buyer optimality. The paper-specific model defines , , the exponential risk function, equation (1), the Table 2 rows, and . The goal quantifies over every pair of supplier best-response strategies; it does not define those strategies as the formulas to be proved in Lemmas 1 and 2. Buyer optimality ranges over every feasible effort, rather than over the three candidate rows.
The model's standing predicate records , , , , , , , , and . Positive demand, nonnegative indirect loss, positive total loss, and positive make economic sign and division conventions explicit where the source uses them without a separate assumption. The denominator of is positive in the only region where Theorem 1 uses it, . Real logarithms and square roots are used only with positive arguments in the applicable equilibrium rows. At , the control effort is zero and its row coincides with the no-effort outcome; the theorem retains the paper's weak inequality.
The initial reusable work is the sequential-game interface and the two best-response characterizations. Contributions that prove those results, the reduced-profit identity, the domination and comparison statements, or the full threshold classification all advance the mission. Statements obtained by assuming the Table 2 formulas are already optimal would bypass the result being formalized.
Some organizations grow by asking each member to recruit a successor. The incentive facing a member depends on where the revenue generated by later members goes. A transfer rule may reward the recruiter, keep the revenue with the entrant, or divide it among several predecessors. Hougaard, Moreno-Ternero, and Østerdal ask which fixed rule gives the greatest total expected payoff when members choose recruitment investments for themselves. Their model covers a sequential hierarchy with no fixed terminal generation, so both incentives and the possibility of a very long hierarchy matter. The authors also discuss recruitment and blockchain rewards as interpretations of the same transfer problem. Hougaard et al.
The paper distinguishes a centralized benchmark from a decentralized design problem. In the centralized benchmark, investments can be chosen to maximize the hierarchy’s total value directly. In the decentralized problem, each agent chooses an investment privately after the allocation rule has been announced. The result targeted here is the paper’s Theorem 2 for the decentralized problem, in the authors’ Universidad Pablo de Olavide working-paper version dated August 3, 2021. Its page numbering and theorem labels refer to that version. Hougaard et al.
Agents are numbered . Agent is present initially. If agent has arrived, she invests and recruits agent with probability . The common technology is strictly increasing and strictly concave, starts at , takes values below one, has an unbounded right derivative near zero, and has convex ratio on positive investments. These conditions apply throughout the model. A member may invest any nonnegative amount; there is no budget ceiling. Hougaard et al., §2
Each arrival creates one unit of value. An allocation scheme has entry for the share of agent ’s unit given to agent . Shares are between zero and one, shares to a later agent are zero, and each row sums to one: . Write and for the probability that agent arrives. Conditional on arriving, agent receives her own share, pays her investment, and may receive shares from later arrivals. The paper denotes this conditional expected payoff by ; equation (1) gives its full series. Hougaard et al., pp. 7–9
A profile is a Nash equilibrium of a scheme if, for every agent and every alternative , changing only to cannot raise that agent’s conditional payoff. This includes agents reached with probability zero under the current profile: each is still a player in the induced game. The hierarchy’s expected length is , and its expected investment is . Transfers cancel in the total, so the social value is associated with the profile rather than the scheme and equals when the series are finite. Hougaard et al., pp. 8–10
A scheme is decentralized socially optimal when at least one of its equilibria has social value at least as high as every equilibrium under every valid allocation scheme. This existential choice of a supporting equilibrium matters because a scheme can have more than one equilibrium. The comparison concerns outcomes agents can sustain in equilibrium, rather than all investment profiles, including those a planner could impose without incentives. Hougaard et al., pp. 10–12
Let keep agent ’s initial unit with agent and give the entire unit created by each later agent to that agent’s immediate predecessor:
with every other entry zero. The goal asserts both existence and uniqueness:
Equality is entrywise equality of schemes. The goal does not assert that every scheme has a unique equilibrium. Under , the supporting equilibrium is constant, , with . Hougaard et al., Theorem 2, p. 12; proof of Proposition 1, p. 27
The milestone list follows the claims used in the paper’s proof: finite investment gives finite expected length; the best length at fixed expected investment is attained; a constant profile of the same length uses less investment than a nonconstant profile; a weighted gross-return identity accounts for all later arrivals; a nonconstant equilibrium is surpassed in social value by the unique constant profile of equal length, supported as an equilibrium; the equilibrium under is identified; and the two parts of Theorem 2 are established separately. The length and value comparisons use the source’s own quantities , , , and . Hougaard et al., proof of Theorem 2, pp. 20–27
Theorem 2 identifies the complete transfer table that gives the largest attainable social value under private investment choices. It rules out every other feasible scheme, including schemes that spread a successor’s revenue across several predecessors. The result also fixes a reference point for the paper’s comparison with centralized investment and for its later analysis of rules that optimize the initiator’s payoff instead. Those later results concern different objectives and are outside this mission. Hougaard et al., §§3–4
The paper proves the result on paper. The formalization task is to give a machine-checked proof of its exact claim, including the infinite-horizon payoffs and the quantifiers over all schemes and their equilibria. The definitions of nonnegative-action equilibrium, sequential survival weights, and extended-valued expected returns can also support later work on sequential incentive systems. No proof of this theorem is supplied by the draft statement itself.
The obvious hope is that a rule that fully rewards the immediate recruiter must produce the best outcome because it ties each payment to the next successful addition. That observation does not compare all possible equilibria: a different rule may redistribute receipts from several future arrivals and change investment at every stage. The hierarchy has no finite horizon, and an agent’s gross expected receipts can be infinite. A complete argument must control those series while comparing a nonconstant equilibrium to a constant one, then establish that no different transfer entry can support an equally good outcome. The paper’s proof organizes these obstacles in Steps 0–5. Hougaard et al., pp. 20–27
Lean represents agents by natural numbers, with zero as the initial agent. Profiles and schemes are real-valued functions; validity requires nonnegative investments and row-stochastic, lower-triangular transfer shares. The technology structure carries every standing assumption of §2. Differentiability is stated on positive investments together with continuity at zero from the right, consistent with the paper’s infinite right derivative there. Hougaard et al., pp. 7–10
Expected length, expected investment, and gross receipts are sums in extended nonnegative reals. Conditional payoffs and social values use extended reals. The value convention assigns negative infinity when expected investment is infinite; otherwise it uses the finite real difference . Step 0 supplies the finiteness of in that latter case. The maximum-length function takes a supremum over profiles with exactly the specified expected investment, and its milestone includes finiteness and attainment. These choices retain the source’s possible infinite payoffs and avoid an accidental zero value for a divergent real series. Hougaard et al., footnote 8 and proof of Theorem 2, Step 0
Steps 2–3 require a disclosed boundary reading: “nonconstant” means differing investments among agents with positive probability of arrival, and the profile has finite expected length. Without these conditions, a profile can differ only after recruitment has stopped, or have infinite length, making the printed comparison false. The Step 3 identity carries the no-self-transfer condition used where the paper invokes it. The goal itself has no such extra conditions. The equilibrium definition ranges over every agent and every nonnegative unilateral deviation, and decentralized optimality compares every equilibrium of every valid scheme; neither class is empty by definition. Contributions proving the eight milestones, the goal, or reusable lemmas for their infinite sums and concavity claims are in scope. Hougaard et al., pp. 9–10, 24–27
Managers are often accused of short-termism: boosting current cash flow at the expense of long-run firm value. Hackbarth, Rivera and Wong (Management Science, 2022; working paper SSRN 3060869) study short-termism inside a dynamic-agency model of a levered firm. A risk-averse manager exerts two unobservable efforts: long-term effort , which raises the growth rate of firm size, and short-term effort , which raises current profitability. The firm issues perpetual debt with coupon , and shareholders choose the manager's incentive contract and the default time.
Debt distorts incentives through debt overhang (Myers, 1977): shareholders bear the cost of effort but share its benefits with bondholders, so they underinvest. The paper's question is whether debt also distorts the mix between short- and long-term effort, and whether that distortion is a separate agency cost or a consequence of underinvestment. Proposition 5 answers the second question: if shareholders commit to the long-term effort an unlevered firm would choose, they voluntarily choose the unlevered short-term effort too. Excessive short-termism is then an indirect cost of debt, transmitted only through long-term effort.
Firm size evolves as and is absorbed at a lower boundary . Profitability evolves as , and the two shocks have correlation . Efforts lie in the effort box , . Effort costs , where may have either sign (complements or substitutes). Everyone discounts at , the manager has CARA coefficient , and the corporate tax rate is .
The paper reduces the shareholders' problem to an ODE for the equity value . Write
where is the manager's incentive-risk term. The levered HJB (18) is . With it is the unlevered HJB (25). The unlevered value solves (25), has , is twice continuously differentiable on , and has linear growth, as in Proposition 3. Its maximizers form the unlevered effort policy.
Two constrained problems compare commitment regimes. Both impose, at a default threshold , value matching , smooth pasting , and transversality as .
For every coupon , every unlevered value solving (25), every associated effort policy , every function and every threshold ,
The unlevered value and its policy are hypotheses, matching the objects used in the paper's statement and proof.
with the paper's . 2. Section of the joint maximizer (A.4.2). For every slope , maximizes over . 3. (A.26). For every and , the maximum over of is attained at , so the right-hand sides of (A.29) and (A.27) agree.
The result. Proposition 5, together with Proposition 4 (with independent effort costs, debt does not affect short-term effort), shows that debt affects the two efforts asymmetrically. Debt distorts long-term effort directly through underinvestment, and short-term effort only through its interaction with long-term effort in the cost and risk terms. A contract or covenant that pins down long-term effort therefore removes the short-termism distortion as well. The converse fails: committing to does not recover . The paper's calibration (§5) quantifies the value of these commitment regimes. Proposition 5 guarantees that two of them coincide, so the no-underinvestment numbers are also the no-overhang numbers.
Formalizing it. The result is proved in the paper, and no part of the model is formalized anywhere to our knowledge. This mission produces a machine-checked statement of the levered-firm HJB, the unlevered effort policy as a constrained maximizer, and the two commitment problems. It also gives a corrected version of the appendix display (A.26), which as printed omits a factor , the factor in one cross term, and contains a stray sign. These objects can be reused for later statements of the paper, such as Proposition 4 and the comparative statics of §4.4.
The proof has no analytic depth. The work is in the encoding, where the obvious readings fail in specific ways:
All quantities are real numbers. The parameters form a structure, and the standing assumptions of §2 (, , , , , , ) are one predicate. Its single added clause is , which the transversality limit presupposes. No concavity assumption and none of the paper's Conditions 1–2 are imposed.
Conventions committed to:
deriv f and deriv (deriv f), and is required to be on the open set .IsGreatest of the image, so attainment is part of the statement.The trivializing encodings are ruled out: NU maximizes over , NO fixes , and comes only from the unlevered maximization at , never from a hypothesis about the levered integrand.
Not in scope: the continuous-time contracting results (Proposition 1, which needs martingale representation), the verification theorems (Propositions 2, 3, 6, 7, which rest on Strulovici–Szydlowski 2015), Proposition 4, Lemmas 1–2 and the calibration. Contributions are welcome on all three milestones and the goal. The model file is self-contained and depends only on Mathlib.
Companies often sell a machine-learning product before its model has reached its final quality. Use of the product then yields data that can improve later versions. This feedback is the AI flywheel studied by Gurkan and de Véricourt. A firm may hire a specialist to develop the model, but the specialist's effort is costly and hidden. More customer data can then change both the product's future quality and the cost of inducing effort. The authors ask how that interaction changes the firm's price and data collection relative to a firm that develops the model itself. Their working paper reports that the direction depends on how the effect of effort varies with dataset size Gurkan and de Véricourt, 2021/2022.
The setting connects a pricing decision to an incentive decision. A lower price attracts more buyers and supplies more data for the next period, yet it also gives up current revenue. When a provider trains the model, the value of additional data depends on how data alter the provider's chance of producing a high-quality result under effort and under shirking. The theorem isolates that change through one ratio rather than requiring a particular parametric learning curve.
There are two periods and a unit mass of potential buyers in each. A buyer's sensitivity to algorithm accuracy is uniformly distributed on . The algorithm's accuracy is either or , where . Given a dataset of size , a provider who exerts effort produces high accuracy with probability and pays cost ; a provider who shirks produces it with the lower probability and pays no effort cost. The firm observes accuracy and can condition payments on it, while effort itself is unobservable.
If the firm collects data at capacity , the buyer model gives period revenue
First-period sales add data to the initial dataset . When the first algorithm has low accuracy, the provider retrains it on ; when accuracy is already high, no retraining is needed. The data impact
measures the relative effect of effort on the high-accuracy probability. The paper assumes is convex on the relevant data interval Gurkan and de Véricourt, §3.2.
The firm's contract selects four nonnegative payments, one for each accuracy outcome in each period, and two first-period data quantities, and . Its expected profit and two incentive constraints are Problem (6)–(9) in the working paper. The first-best benchmark fixes each payment at and removes the incentive constraints. Write for the low-accuracy data quantity of an optimal contract and for that of an optimal first-best plan.
The main target is Theorem 1 of the working paper. For interior optimal prices, it compares the two global optima:
Since price and purchased quantity move in opposite directions in this buyer model, collecting more data corresponds to charging less than the first-best price. The three cases cover equality, underpricing, and overpricing without fixing a learning-curve formula Gurkan and de Véricourt, Theorem 1.
The milestones follow the paper's stated results. Lemma 1 characterizes the last-period myopic quantity and revenue. Lemma 2 identifies the optimal accuracy-contingent payments when first-period data choices are fixed. Proposition 1 characterizes the unique optimal contract and its reduced data-choice objective; Proposition 2 gives the unique first-best plan and places its low-accuracy data quantity above the myopic quantity. Two claims in the proof of Theorem 1 record the weak comparison and the distinctness of interior optima under strict monotonicity.
The theorem specifies the direction of a distortion in a firm's choice of data collection. Its conclusion depends on the relative change in two learning curves, not merely on the fact that more data improve model accuracy. In the increasing-impact regime, the contracting firm collects more data than the first-best firm; in the decreasing-impact regime, it collects less. The result gives a qualitative comparison for pricing and data acquisition when algorithm development is outsourced Gurkan and de Véricourt, §4.2.
The result is proved in the source paper; the task here is to give its two-period model, contract constraints, and comparison a Lean proof. The definitions also provide a reusable small model of two-outcome, two-period moral hazard with limited liability. A complete development would let later statements about welfare, capacity, or alternative contracts reuse the same precise optimization problems. No existing platform definition matches this paper's model, and the draft theorem statements currently have compilation placeholders rather than machine-checked proofs.
The first obstacle is the contract itself. Payments in the second period affect the provider's expected continuation payoff and thereby the first-period incentive constraint, so choosing each period's payments independently does not describe Problem (6). The data choice changes the probability of later accuracy and the incentive cost at the same time. A direct comparison of the two full objective values does not determine whether lies above or below ; the paper's comparison depends on how the data impact changes with . Strict inequalities also need interior optimal choices. At a boundary, two distinct objective functions can select the same endpoint even when is strictly monotone.
The Lean development uses real-valued data sizes, payments, probabilities, and revenues. It represents the learning curves and as functions on , with hypotheses restricted to . Feasible data choices lie in , and keeps every evaluated learning-curve value inside the stated domain. The standard-uniform quantile is the identity on its support. The second-period value is the supremum of revenue over ; Lemma 1 supplies its attained maximum. Both contract and first-best optimality are global over their respective feasible sets.
The standing assumptions include positive effort cost and low accuracy, , strictly increasing concave learning curves and , differentiability of both curves, and convexity of . Positive and strict make the paper's uniqueness conclusions well posed. Differentiability is weaker than the twice-continuous differentiability mentioned in the source's later proofs. The paper's condition favoring effort in both periods motivates the chosen contracting problem; effort is already imposed by its two incentive constraints. Interiority of the optimal low-accuracy quantities is an explicit hypothesis of the comparison theorem, reflecting the paper's assumption that optimal prices neither cover nor exclude the entire market Gurkan and de Véricourt, §3.4 and EC.1.
The goal concerns optimal solutions of the full six-variable contract problem and the full first-best problem. Defining and only as maximizers of the reduced one-variable objectives would omit the contract's incentive constraints. A complete proof needs real optimization on compact intervals, concavity and differentiability facts, and a precise account of the payment constraints. Contributions to those components and to the stated milestones fit this mission.
Firms decide not only how to pay workers but whom to put together. A long empirical and theoretical literature on teams asks whether homogeneous ("specialized") or heterogeneous ("diverse") teams perform better. Most arguments for diversity are informational: diverse teams bring different knowledge or perspectives. Glover and Kim (SSRN 3344922, published in Management Science 2021, doi:10.1287/mnsc.2020.3762) give an argument based on incentives instead. In a repeated relationship, teammates who can watch each other can enforce effort by threatening to punish a shirker (mutual monitoring). The same ability lets them coordinate against the principal (tacit collusion). Whether production efforts are complements or substitutes determines how strong each force is. The paper shows that diverse teams, whose efforts are complements, can be cheaper to motivate even when specialized teams are more productive. This mission formalizes the paper's main comparative-statics result about this trade-off.
The model belongs to the literature on implicit incentives in repeated teams, which studies relational contracting and mutual monitoring among agents (Arya, Fellingham and Glover 1997; Che and Yoo 2001). Its new element is that the team's technology depends on its composition.
A principal hires four agents for two tasks each period. Each task is done by a team of two agents. Each agent chooses effort (shirk or work) at cost , with , and all parties share a discount factor . A team of kind (specialized or diverse) produces with probability when of its two members work, and otherwise. The agent receives a wage on success and nothing on failure.
The standing assumptions are:
The normalized punishment is . Two thresholds matter:
The principal's programs (Appendix A) minimize the wage subject to constraints:
The least feasible wages are (diverse), (specialized, mutual monitoring only) and (specialized, collusion-proof). Expected wages are . The principal's per-period payoffs are and . With , the output threshold is
Assume , and write . Then
In attack order:
Proposition 2 says that patience affects the two compositions in opposite directions once collusion matters. As long as only mutual monitoring binds, more patience helps specialized teams more, because their larger normalized punishment is multiplied by . Beyond the specialized team must be paid to prevent its members from taking turns shirking, and this cost grows with . The threshold below which diversity is optimal therefore rises with patience past . So the model predicts that long-lived teams with valuable but not too valuable output should be diverse, for incentive reasons alone.
The proofs in the paper are short calculations, and the proof of Proposition 1 compares the gap only at , and . A machine-checked development certifies the closed forms of the three programs, the strict monotonicity on whole intervals (not only at sample points), and the derivative claim. To our knowledge none of these results has been formalized.
Each wage is a minimum over a feasible set defined by inequalities. The specialized (M-IC) constraint changes form at , and the (No-cycling) constraint takes over at . A solver must first identify the binding constraint on each region and show that the least element exists, which is Lemmas 1 and 3, before any monotonicity argument starts. The obvious approach, comparing the two closed forms termwise, fails on : there both expected wages decrease, and the claim is that the specialized one decreases faster. That requires the ratio condition together with A.1 and A.3, not just the sign of each derivative. Strictness at the kinks and , where the piecewise wage is not differentiable, also needs care.
All quantities are real numbers. A technology is a structure Tech with fields f0 f1 f2. Assumptions A.1–A.3 are kept in the paper's ratio form inside Standing. The optimal wages are not defined by closed formulas. Every theorem about them takes arbitrary functions ws wd : ℝ → ℝ with the hypothesis that, for each , ws δ and wd δ are the least elements (IsLeast) of the Appendix A feasible sets. Defining the wages by their closed forms would make Lemmas 1 and 3 hold by definition, and that trivializing formalization is ruled out. The specialized (M-IC) constraint is piecewise at , exactly as printed.
Conventions:
StrictAntiOn, StrictMonoOn).deriv on the open interval , so it also asserts differentiability.Not formalized:
The development needs only real inequalities, maxima of finitely many functions, and one-variable calculus from Mathlib. Contributions are welcome at every milestone. Lemmas 1 and 3 are reusable by anyone working on further results of the paper.
Lenders, employers and insurers increasingly screen applicants with learned scores, and regulators and the fair machine learning literature ask that such screening be fair across demographic groups. Two notions are standard. Equal treatment (ET) asks that the same decision rule be applied to everyone, regardless of group; the paper notes that it is what the law currently requires. Equal opportunity (EO), proposed by Hardt, Price and Srebro (2016), asks instead that qualified applicants be accepted at the same rate in every group. EO is often presented as the notion that protects a disadvantaged group better, because it corrects for differences in how well the screening technology separates good from bad applicants in each group.
Most analyses of these notions take the classifier as given. Fu, Aseri, Singh and Srinivasan point out that a profit-maximizing firm also chooses how much to invest in learning, and that a fairness constraint changes that choice. Their Theorem 2 identifies a regime in which, once the firm's learning response is taken into account, EO accepts no larger a share of the protected group's qualified applicants than ET does. The result is a short, fully explicit comparative-statics statement about a parametric model, which makes it a natural target for formal verification.
A bank screens loan candidates from two groups of equal (unit) size: a protected group and a regular group . A good candidate repays and earns the bank ; a bad candidate defaults and costs it . The proportions of bad candidates are and , with , and the expected profit and loss per group are
with the paper's assumption (hence ).
The bank chooses a learning effort . In group , scores of bad candidates are uniform on and scores of good candidates uniform on , where the learning rates satisfy : learning separates the regular group faster. The bank accepts a candidate of group whose score exceeds a threshold , and pays the learning cost . Its profit is equation (1) of the paper: expected profit from accepted good candidates minus expected loss from accepted bad candidates, summed over the two groups, minus .
The coverage rate of group is the fraction of its good candidates that are accepted,
Under ET the bank must use ; under EO it must equalize the coverage rates, (equation (6)). Writing for the bank's optimal decision under constraint , the quantity of interest is , the protected coverage rate at that optimum.
The paper focuses on the low-loss case (case (1), p. 17) and on learning costs in a middle range: with
it assumes with , so that learning is neither so cheap that it separates perfectly nor so expensive that the market fails.
Under the standing assumptions, the low-loss case and the cost range above, if
then for every optimal ET decision and every optimal EO decision
Theorem 2 is the paper's main statement about the protected group. It says that a constraint designed to raise the protected group's acceptance of qualified applicants can fail to do so once the firm re-optimizes its investment in learning: when lending to the protected group is risky enough relative to its return, the EO-constrained firm learns less, and the protected group's coverage rate is no higher than under ET. The paper uses it, together with its Theorem 3 on success rates, to argue that the choice between fairness notions should account for endogenous learning, and it explains the condition's dependence on the learning-efficiency gap and the expected loss .
The result is proved in the paper by first-order conditions and algebra. It has not been formalized. The formalization adds a machine-checked passage from the bank's joint optimization over thresholds and effort, with the piecewise-linear profit (1), to the closed-form comparison: the threshold reductions and the existence and location of the optimal efforts are asserted in the paper with little or no argument, and the mission makes each of them an explicit, checked statement.
The algebra of (53)–(59) is short. The work lies upstream of it. The profit (1) is a sum of min and max terms, and its maximization over thresholds must be carried out case by case on the positions of relative to the four breakpoints ; under EO the thresholds are further tied by constraint (6). The first-order conditions (47)–(48) identify the optimal efforts only once unimodality and interiority are established, and these hold only in the stated cost range: at its endpoint the ET optimum sits exactly at the boundary . Substituting the closed forms (51)–(52) directly into the conclusion skips all of this and is not the theorem.
Everything is real-valued and lives in the namespace UnfairML.Coverage. One definitions file holds the parameters (Params: ), the derived quantities, the standing assumptions (Standing), the low-loss case (LowLoss), the cost , profit (1), the coverage rate, the EO constraint (6), the optimality predicates IsOptET and IsOptEO, the reduced profits of case (1), and the cost range CostRange.
Conventions committed to:
A goal stated about maximizers of , or with (51)–(52) substituted, would be a different and much weaker statement and is ruled out. The cost range is satisfiable only when ; a sorry-free check that all hypotheses of the goal hold together for an explicit rational instance accompanies the development.
No Mathlib extension is needed beyond real analysis on intervals (monotonicity from derivatives, IsMaxOn). Contributions are welcome at every milestone; the threshold reductions are self-contained piecewise-linear arguments and a natural starting point.
Humanitarian organizations (HOs) such as the Red Cross or UNICEF keep prepositioned stock ("prepo") of relief items in distribution centres, so that they can fly supplies to a disaster area in the first days after a rapid-onset event. A second source is local purchasing in or near the affected region after the disaster strikes: it is cheaper per unit and supports the local economy, but local supply is uncertain (a severe event can destroy it), and buying it requires cash that the HO may not have at the right moment. Budgets of HOs are tight and partly random: a fixed budget at the start of a cycle, a steady inflow of donations, and an emergency fund raised once a disaster is in the news.
Eftekhar, Song and Webster (SSRN 3210309; published in Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0956) model the HO's choice of a prepo level under budget, demand and local-supply uncertainty. Their single-cycle result answers a practical question: when is the classical newsvendor rule (stock the critical fractile of demand) the right prepositioning policy, once local supply and budget constraints are taken into account?
A prepo cost cycle starts when the HO chooses a prepo level and ends after the relief period of the next disaster. The unit cost of prepo is normalized to . The parameters are a holding cost per dollar-period; a local supply cost multiple ; a unit shortage cost ; an initial budget , with ; and a funds inflow rate .
On a probability space, the random time to the disaster , the relief demand , the local supply and the emergency fund are nonnegative and integrable, and is independent of ; , . When the disaster strikes, the money available for local spend is
The HO buys locally first, units, leaving the local shortage ; prepo covers and is unmet. The expected cycle cost is
and the HO solves . The auxiliary model relaxes the local budget constraint, replacing by :
With , the number is a -fractile of the net demand , and the threshold budget is
with the support of and the lower end of the support of .
If , then
The paper prints "". The last equality is false in a corner: if and almost surely, then , and any with makes infeasible. The goal states the printed equality under the extra condition, and the optimality of under alone.
Proposition 2(b) says that a well-funded HO can plan prepositioning with a newsvendor rule on net demand : the optimal shortage probability is , set by holding cost, disaster frequency and shortage premium, and the budget matters only through the cap . Below the threshold, the same rule gives an upper bound on optimal prepo (Proposition 2(a)), so separates the regime where the heuristic is exact from the one where it overstocks. The comparative statics of §4.2 and the dynamic policy of §5 build on this single-cycle analysis.
The paper's proofs are in an online supplement. This mission produces a machine-checked version of the threshold result without density assumptions, and with a corrected statement. No part of this model is formalized elsewhere: the platform's newsvendor results concern models without local supply, random budgets or a budget cap.
The cost couples three nonsmooth effects: the cap on local purchases, which depends on through the budget, the split of the shortage between prepo and unmet demand, and the expectation over a joint law with no density. The obvious argument, "above the cap never binds, so and eq. (4) applies", proves only that and agree on . For the cap can bind, so could in principle dip below to the right of . Ruling this out needs the global inequality . Eq. (4) itself is a newsvendor argument at a generalized fractile: is convex but not differentiable at atoms of , and the case , where the inverse is , must be handled.
All quantities are real; expectations are Bochner integrals over a probability measure . The standing assumptions, bundled in Params.Standing and Env.Standing, are: , , , , ; measurable, integrable and almost surely nonnegative; independent of (stated on p. 6, unused by the statements). The conventions are:
IsMinOn), since is convex but not strictly.is defined as the expectation of the operational cost (the first line of the display on p. 7), and as the separate closed expression of p. 9; a formalization defining by its closed form, or as above the threshold, would make the milestones trivial and is excluded.
Not formalized: the second clause of Proposition 1 (it needs the densities and derivatives (2)–(3)), Proposition 2(a), (c)–(e), the comparative statics of §4.2 and the dynamic model of §5. The development needs only Mathlib's integration and independence API; the newsvendor lemma at a generalized fractile (milestone 3) is reusable for other newsvendor models. Proofs of any milestone are welcome, as are a proof of Proposition 2(a) from the same definitions.
A manufacturer that receives evidence of a product defect must decide whether to disclose it. A regulator that receives a report must decide whether to investigate immediately. The regulator's announcement can itself change consumer demand while the investigation is under way, so a policy intended to reveal defects may change the manufacturer's incentive to report. Cho, DeMiguel, and Hwang study this interaction for vehicle defects, comparing a U.S. policy that announces an investigation with a U.K. policy that keeps it confidential. Their analytic model identifies circumstances in which the manufacturer conceals a signal even though the expected harm is substantial. This mission formalizes the U.S. equilibrium characterization in Proposition 2 of the authors' accepted manuscript.
A product is either defective, , or nondefective, . The prior probability of defect is . A manufacturer receives a private signal indicating a possible defect. Its reliability is , and after this signal the manufacturer's posterior probability of defect is
The product sells at price over a unit-length life cycle. Consumers arrive at unit rate and have valuations uniformly distributed on . A defective unit causes expected harm . The ordinary demand rate is . When the U.S. regulator announces an investigation, consumers account for possible harm during its mean duration , so the temporary demand rate is . The model assumes , ensuring positive demand even during an announcement. These choices follow §3 of the manuscript.
After a positive signal, the manufacturer chooses report () or no report (). After a report, the regulator chooses immediate investigation () or no immediate investigation (). A later voluntary investigation can occur if the product is defective. Its time has constant density on , while the probability of no such investigation is . An investigation costs the regulator . If a defect is found, the manufacturer recalls previously sold units at unit cost and compensates consumer harm. A discovered cover-up carries penalty with discovery probability . If no investigation takes place, the manufacturer bears fraction of consumer harm. These payoffs determine three U.S. manufacturer profits, , , and , from equations (1), (3), and (5) of the manuscript.
The regulator maximizes social welfare , the manufacturer's profit plus consumer surplus minus investigation cost. The two welfare values after a report are and . The regulator chooses when these values tie. The manufacturer chooses when its profits tie. The regulator's action after is , since there is no report to investigate at time zero. These conventions are stated in §§4–5 and the proof of Proposition 2 of the manuscript.
The regulator's threshold result, the U.S. half of Proposition 1, says that there are and a curve on , with values in and , such that
Proposition 2 adds and a reporting curve with the analogous domain and endpoint value. The goal is the unique subgame perfect equilibrium for every admissible and :
The last profile records the regulator's response if a report had arrived; on the realized path the regulator does not investigate immediately. The milestone list follows the source's two welfare and profit identities, the two harm thresholds, Proposition 1's U.S. response, and the reporting rule in Step 1 of Proposition 2's proof. Each formula comes from the accepted manuscript, pp. 13, 15, 28, and 30–31.
The characterization locates the cover-up region in the harm–reliability plane. Under the U.S. announcement policy, a report can depress sales during an immediate investigation, while concealment risks a later penalty. The model shows how these forces produce an intermediate-reliability band in which the manufacturer conceals even a high-harm signal. The result can therefore be used to compare disclosure incentives under investigation policies using the same payoff primitives. The authors prove the result in the paper; the remaining task here is to formalize its stated assumptions, integral payoffs, threshold identities, and equilibrium claim in Lean. The local prior-art search found no existing formalization of this particular game.
The regulator's and manufacturer's choices each depend on a difference between payoffs defined by several integrals. The closed forms are cubic expressions in harm, and the threshold claims require their signs to be controlled on the full interval . Checking a few parameter values does not establish those interval-wide claims. At the equilibrium boundaries, both actors' tie rules matter: without them, the claimed unique strategy profile is not determined. The proof must also keep the thresholds independent of the point being classified.
The development uses real numbers for all model parameters and values. One Params record contains ; neither nor is a field of that record. Params.Standing collects the source's sign and range restrictions, including , , , , and . It also requires : the paper's definition of reliability divides by , and its threshold fractions divide by .
Profit and consumer-surplus expressions use intervalIntegral for the manuscript's valuation and voluntary-investigation integrals. Their integrands are polynomials or constants on finite intervals, so the usual nonintegrability default is irrelevant here. The posterior formula represents the signal law at the point needed by the theorem; the full joint signal distribution is not reconstructed. Likewise, the investigation lead time enters through its mean , as it does in the paper's expected-payoff formulas. The polynomial closed forms are named separately and linked to the primitive payoffs by milestone theorems.
IsSPNE is the tie-broken sequential best-response condition for the two decisions, with fixed after no report. Proposition 2 quantifies the four thresholds before all and , constrains their relevant domains, and characterizes every equilibrium profile in each region. This prevents thresholds chosen separately at each point, a vacuous regulator curve, or an existence-only restatement. The reusable work is the interval-integral algebra and interval-wide polynomial threshold arguments. Contributions on those identities, the threshold theorems, and their equilibrium assembly are all within scope. The U.K. equilibrium and later welfare comparisons are separate results in the paper.
An experiment may compare two ways to select initial participants in a social network. Each selected seed set can lead to a different outcome, and the experiment observes only the outcome for the seed set actually selected. Chin, Eckles and Ugander study how known selection probabilities let observations from one experimental design estimate the outcomes of two other seeding strategies. Their setting includes one hop targeting and random targeting, but their statistical results apply to any two stochastic strategies with known probabilities. The central result here is their Proposition 2: the Hájek estimator, which normalizes the observed importance weights separately for the two strategies, is consistent and asymptotically normal. These properties are needed to interpret a large experiment's estimated difference and its uncertainty. Chin, Eckles and Ugander, §§2–3.3 and Proposition 2.
Let be a countable space of possible seed sets, including any network information that varies across the superpopulation. Strategies and give probability mass functions and on . An experimental design distribution gives the law of each observed seed set. A fixed function records the potential outcome for each possible seed set. For a draw , the observed outcome is . The design supplies independent draws with common law ; the outcome is a deterministic function of each draw. The paper allows outcomes such as counts and fractions and does not require a finite seed space. Chin, Eckles and Ugander, pp. 8–9.
The strategy means are and . Their difference is the superpopulation contrast . For a seed set with positive design probability, its importance weights are and . Write , with analogous notation for . The paper's estimator in equation (7) separately normalizes the two sets of weights:
The design can be a mixture of and , but the proposition also addresses other designs. The formal statement therefore leaves general. Chin, Eckles and Ugander, equations (2), (4), (5), (7), pp. 9–10.
The first targets are the weight moment identities, the limits of the four sample averages, and almost sure consistency of . The joint central limit theorem for those averages and the variance identity connect these to the goal. These targets follow the displays and sentences in the proof of Proposition 2, Appendix A.2. Chin, Eckles and Ugander, pp. 39–40.
The goal is the corrected full strength of Proposition 2. Under full support of the design on the support of either strategy and finite second moments for the four weighted coordinates,
where the variance is the value specified by the paper's equation (15),
The variance is determined by the two strategies, the design, and the outcomes; it is not a free variance parameter. The almost sure limit records the strong form supplied by the sample average law. Chin, Eckles and Ugander, Proposition 2 and equation (15), p. 14.
The result identifies both the value approached by the normalized estimator and its leading large sample variance. The two normalized terms are correlated because a single observed seed set contributes information about both strategies. Equation (15) retains that dependence, so the uncertainty of their difference is not obtained by adding two separate variance formulas. The paper uses this result to motivate inference for a superpopulation contrast rather than a finite collection of villages, for which a single observation per village does not identify each village's variance. Chin, Eckles and Ugander, §3.3, p. 14.
The mathematical result is published in the cited preprint. This mission asks for a machine checked statement and proof of its corrected version, plus reusable facts about weighted moments, strong laws for transformed samples, and a four coordinate central limit theorem. The proof infrastructure can serve other comparisons of two policies under a common sampling design. The Horvitz–Thompson result in Proposition 1 is related but is a separate theorem and is outside this mission. No proof of Proposition 2 is currently included in the mission's local formalization.
The estimator is a difference of two random ratios. At small sample sizes, either normalizing sum can vanish, and the two ratios are dependent. Applying a variance formula for one self normalized estimate twice would discard their covariance. There is also a source level obstacle: the printed positivity assumption permits the design to omit a seed set on which both strategies assign equal positive probability. Such a set does not affect the strategy contrast pointwise, but it changes the separate means and the normalizing weight expectations. The printed hypothesis therefore does not imply the moment identity used in Appendix A.2. Chin, Eckles and Ugander, Assumption 1, p. 11, and proof of Proposition 2, p. 40.
For example, take three seed sets with , , and . The paper's Assumption 1 holds, but and the Hájek estimator approaches . This mission labels the replacement support condition as a correction. The printed intermediate expansion of the delta method variance also has a sign error in a cross term; equation (15) itself is retained. Chin, Eckles and Ugander, pp. 11, 14, 40.
Lean represents by an arbitrary countable type with measurable singletons, by PMF, and the sample by measurable independent maps from one probability space, each with law . The natural number is the number of sampled villages: Lean uses draws in place of the paper's . Probabilities enter real arithmetic through ENNReal.toReal; a PMF assigns finite mass to each point. Full positivity says whenever or . It is stronger than the paper's contrastive Assumption 1 and is needed for the separate means and normalization identities.
The four second moment conditions apply to , , , and under . They make the joint covariance finite even when is unbounded. The consistency milestone uses only the first moments it needs. The variance is the real integral from equation (15), then converted to a nonnegative real variance for Mathlib's Gaussian law. Lean's total division assigns zero weight when ; such a seed set is not observed under the design. The estimator is zero at , and a finite sample with a zero normalizing sum uses Lean's division by zero value. The almost sure and distributional limits address the paper's asymptotic claim.
The intended statement includes every countable seed space and every qualifying independent sample. Restricting to a finite seed space, assuming the estimator's limit or a central limit theorem, or selecting an arbitrary Gaussian variance would change the claim. The development needs Mathlib's probability measures, integration, strong law, Gaussian laws, distributional convergence, and moment theory. Contributions that establish the listed milestones or develop the general joint limit and ratio tools are in scope.
Traffic, packet and evacuation networks are often studied with atomic dynamic flows: individual agents move through a network over time, queue at congested links, and each wants to reach its destination as early as possible. The deterministic queuing (Vickrey) model makes the queue at every link explicit: a link has a capacity, and agents beyond it wait in a queue. In the atomic, discrete-time version, simultaneous arrivals at a queue must be ordered by some tie-breaking rule, and that rule decides whether the resulting routing game has an equilibrium.
Hoefer, Mirrokni, Röglin and Teng (2009, 2011) and Werth, Holzhauser and Krumke (2014) studied atomic routing over time in deterministic queuing models, and found non-existence of equilibria and computational hardness in several variants; Harks, Peis, Schmand, Tauer and Vargas Koch (2018) studied competitive packet routing with priority lists. Scarsini, Schröder and Tomala (Operations Research, 2018) proved that a Nash equilibrium exists when priorities are placed on agents, in single-origin, single-destination networks. Cao, Chen, Chen and Wang (Operations Research 2021) showed that with agent priorities and several origins an equilibrium can fail to exist (their Example 3, a rock–paper–scissors cycle). They proposed instead to break ties by edge priorities at each vertex, and proved that equilibria then always exist. This mission formalizes that existence theorem.
A network instance consists of the following data.
The agent set is the disjoint union of all these, and may be infinite.
Each agent chooses at time a path from his starting vertex to . For the path must begin with ; this is his strategy set . At every time unit only the head of the queue on an edge leaves it, and it reaches the head of the edge one unit later. Agents entering an edge are ranked by the edge-priority DQ rule, applied in this order:
denotes the time agent reaches vertex under the profile , and is if he never does.
The normal-form game has players , strategies , and cost . A profile is a Nash equilibrium (NE) if for all and . It is an iteratively dominant NE (IDNE) if the agents can be reindexed such that for every , every vertex on and every profile of the agents outside ,
The goal makes no finiteness assumption on and fixes no constants.
The result. Theorem 1 gives an equilibrium for every network with edge priorities: multiple origins, initial queues and an unbounded stream of inflows are all allowed. With agent priorities, equilibrium can fail to exist in exactly this setting. The IDNE carries more structure than an NE. Arrival times along each agent's path are independent of later agents' choices, and no agent who enters later at the same origin overtakes an earlier one. The paper uses these properties in its study of subgame-perfect equilibria for adaptive agents (p. 12; §5).
Formalizing it. The result is proved in the paper; nothing here is open mathematically. To our knowledge no part of it is formalized in any proof assistant. The mission produces:
The paper proves Lemma EC.2 in a transformed game on an infinite graph (Lemma EC.1). The mission instead states everything directly in , so a complete development must either carry out the transfer or reprove the lemma natively. For infinitely many agents, the claim that every agent is eventually indexed (milestone 3) is asserted in the paper without a separate argument; the formal proof has to supply one.
The obvious argument fails at the no speed-up property. Adding agents to a network can make some other agent arrive earlier. The paper's Example 4 (pp. 15–16) has such a chain effect: removing an agent delays another. So the claim that agent 's arrival times are unaffected by everyone after him is not monotonicity of congestion. It holds only for the specific order and paths produced by the selection procedure, and it must be proved by an induction that carries invariance (equality in (EC.2)) and domination (inequality in (EC.2)) together.
The tie-breaking is the second difficulty. The selection compares candidates backwards from : by arrival time, then by incoming-edge priority, then one edge further back. The argument has to show that this order matches the queue rule (R0)–(R4) at every vertex, including (R3) for agents starting mid-network.
Everything lives in the namespace AtomicDynFlow.IDNE.
Network and agents. Instance V E A carries the graph as finite types V, E with tail, head, d, and the priorities as lists inc v of incoming edges, highest priority first. Initial queues Q0 e are listed head first, and inflows inflow r v highest original rank first. The standing hypotheses are fields:
The agent type A is arbitrary and may be infinite.
Dynamics. queue π s e is a computable, list-based simulation of the queue on each edge at each time, under a partial profile π : A → Option (List E), where none means the agent is absent. arrival π i v : ℕ∞ is , with ⊤ for (p. ec4). The starting-vertex time is for initial-queue agents and for (Algorithm 1, Step 2).
Equilibria. The reindexing of Definition 2 is an injective whose range is an initial segment, with agent receiving index . Definition 2 quantifies over every vertex of the path, the starting vertex included.
Selection. The pruning (S1)–(S3) is a backward pairwise comparison of candidate pairs (Before, IsSelected). Milestones 2 and 4 are -native versions of the e-companion statements, and Lemma EC.1 is not formalized.
Ruled out. Three encodings would trivialize the goal, and none is used:
A sorry-free check of the paper's Example 2 shows that agent waits at and reaches at time , and that removing agent lets him arrive at .
Welcome contributions: proofs of the milestones in any order. Milestone 5 needs only the definitions. Milestones 1 and 2 are the technical core, and general lemmas about the queue simulation (FIFO within an edge, monotonicity in entry times) are reusable throughout.