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?
Large language models answer reasoning questions better when they are allowed to write out a chain of thought (CoT) before the final answer, but every generated token costs time and money. A large body of recent work therefore asks models to "think less": prompts such as "be concise" or "use at most 10 words", and training methods that shorten the reasoning trace. These methods trade accuracy for length, and the natural question is how good such a trade can possibly be.
Lee, Che and Peng (2025) study this question empirically on MATH-500, GSM8K and MMLU-Pro Math with 31 prompts and several frontier models. Their key observation is that, question by question, correctness is almost a threshold function of the response length: a model solves a question if and only if its chain of thought is at least as long as a question-specific token complexity. Under this hypothesis they derive the best possible accuracy–length tradeoff over all prompts, and show that existing prompting strategies are far from it (Table 4 of the paper). This mission formalizes that derivation: Theorem 1 of the paper and the steps of its proof in Appendix D.
Fix one language model and a dataset of questions . A prompt determines, for each question , a chain of thought of token length and a correctness indicator . The accuracy and the average token length of a prompt are
The two optimal tradeoff curves are the optimal accuracy at average budget and the minimal average length for accuracy :
Assumption 1 (token complexity hypothesis). There are numbers , the token complexities, such that for every prompt and question ,
The value marks a question the model never solves. The paper also assumes the prompts are rich: every vector of token counts is produced by some prompt. The answer is expressed through the empirical quantities
where is the largest accuracy any prompt can reach.
Assume Assumption 1, rich prompts, and pairwise distinct finite token complexities. Let be the largest finite with and the smallest finite with . Then for every and every ,
with both optima attained. As printed, the theorem defines , which does not depend on , and , which overshoots the quantile; both readings give wrong values on one- and two-question examples. The goal uses the thresholds that the proof and the text describe ("the highest value of τ that the LLM puts into the knapsack", "the α-quantile of the empirical distribution").
Milestones 4 and 5 allow ties among the token complexities; the goal's closed form does not.
Theorem 1 turns an optimization over all conceivable prompting strategies, an infinite and unstructured set, into a formula in the empirical distribution of numbers. Its consequence, Corollary 1, is that , the average token complexity of the solvable questions, is a lower bound on the average length of any lossless compression of the chain of thought; the paper's Table 4 uses it to show that current concise prompts leave a 3–11× reduction unrealized. The same characterization explains why adaptive strategies, which spend more tokens on harder questions, are necessary to approach the frontier.
The result has a pen-and-paper proof of a few lines in Appendix D; the prior-art search found no machine-checked version. Formalizing it adds a correct statement: the printed definitions of and are wrong, eq. (8) has a reversed inequality, and the closed form silently needs distinct token complexities. The mission records the correct versions with the counterexamples to the printed ones, and separates the tie-robust greedy form (milestones 4–5) from the CDF form (the goal).
The individual steps are elementary, but the obvious argument skips three points. First, passing from prompts to token vectors uses richness in both directions: an optimal prompt must be matched by a token vector and conversely, and the optima must be shown attained, not merely bounded. Second, the reduction to must handle questions with , which can never be selected. Third, the greedy claim is a statement about every feasible selection, not only the sorted ones, and translating the greedy count into the threshold forms and is exactly where ties break the formula, so distinctness must be used at that step and nowhere else.
Fin n; prompts are an arbitrary type; a Benchmark gives token lengths len : Prompt → Fin n → ℕ and correctness correct : Prompt → Fin n → Bool. Each (prompt, question) pair yields one deterministic chain of thought.ℕ∞-valued; is ⊤. Assumption 1 is correct P i = true ↔ τ i ≤ len P i ("above" read as , as the displayed formula on p. 5 shows). Every count or sum over filters on before converting to a natural number.IsGreatest/IsLeast predicates over the set of values achieved by prompts, never sSup/sInf, so empty or unbounded feasible sets cannot produce a junk value.The definitions (benchmark, empirical CDF over an ℕ∞-valued family, sorted prefix sums) are self-contained. A proof of the greedy milestones gives a reusable fact about unit-reward knapsacks. Proofs of any milestone and of the goal are welcome, as is a formalization of Corollary 1 on top of the goal.
An entrepreneur deciding whether to continue a project may value continued control even when liquidation would generate more cash. The project has a known liquidation value, but its final cash flow is uncertain. An accounting signal changes what the entrepreneur expects from continuation and can therefore change the decision. A regulator who cares about total cash flow can choose how much the signal reveals. Jiang and Yang ask which accounting rule best corrects the entrepreneur's excessive willingness to continue and show that the answer has a precise threshold form (Jiang and Yang 2023, §§2–3). The mission formalizes their main threshold characterization for the regulator's reduced problem.
The question belongs to information design: a decision maker chooses a signal before the state is known, anticipating how another party will act after observing it. The result gives a concrete instance in which the optimal signal is neither arbitrary disclosure nor full disclosure. It also identifies a parameter range in which the regulator can obtain the same liquidation decisions as if the entrepreneur had no private benefit.
At date 1 a project can be liquidated for or continued to produce a random date 2 cash flow . The prior law of has a density and full interval support , where . The entrepreneur receives an additional private benefit from continuation. The regulator counts the project's cash flow, not that private benefit. These assumptions and the common prior are from §2 of Jiang and Yang.
An accounting rule reveals information about . The signal induces a posterior probability distribution and hence a posterior mean . Under decision rule (4), the entrepreneur continues exactly when ; on equality they terminate, following the paper's tie rule. The regulator's payoff after that posterior is
The formal representation of a rule is a distribution over posteriors. It is Bayes plausible when its average posterior equals the prior ; the regulator's value is . This posterior representation is the one used in the paper's Appendix A.1 and is consistent with the general Bayesian persuasion framework of Kamenica and Gentzkow 2011. For an event of positive prior probability, denotes .
A threshold rule at sends a high signal precisely on . It sends the low signal when . The strict boundary agrees with Proposition 2; because the prior has a density, the single boundary state has probability zero.
For and , the goal is the corrected endpoint form of Proposition 2. There is a threshold whose reveal policy attains at least the value of every Bayes-plausible accounting rule. Its two cases are
The interior solution is unique. The entrepreneur follows the signal: continuation after the high signal and termination after the low signal. The first case gives the first-best liquidation decision, which continues precisely for .
The milestone list follows the source's Appendix A.1: reduction from Bayes-plausible posterior rules to a binary signal probability ; the relation between the two binary mean constraints (A.1) and (A.2) in each prior-mean regime; the threshold shape associated with the appendix's multiplier; the first-best case; existence, uniqueness, and optimality of the interior threshold; and the closing implication that joins the low-prior-mean case to the first-best case. Together these statements connect the general accounting-rule problem (5) to the threshold formula (6).
The theorem specifies when disclosure can neutralize the private continuation benefit and when a more conservative threshold is required. In the latter case the low signal must put the entrepreneur exactly at the continuation indifference point. The threshold characterization also underlies the paper's claims about full disclosure and how the optimal rule changes with and (Jiang and Yang 2023, Corollaries 1–2). Those corollaries are consequences of the present target, not assumptions of it.
The paper proves Proposition 2 mathematically; the Lean goal and milestone statements here remain open for machine-checked proofs. A complete development would provide a reusable posterior-to-binary reduction for a payoff with two linear segments, plus formal results about conditional means under full interval support. The referenced Bayes-plausibility definition is already published on Prove2Me. Proposition 1 of the paper concerns financing contracts and is outside this reduced regulator problem; its proof is in an online appendix not held with the cited PDF.
The regulator ranges over every Bayes-plausible distribution over posteriors, while the proposed optimum uses only two signals. Checking that a given threshold is best among threshold rules leaves this larger comparison unresolved. The regulator's payoff also switches formula at the entrepreneur's indifference mean, so a direct global smoothness argument does not apply. Finally, the conditional mean below a moving threshold must reach at one and only one interior point under the prior's support conditions. The binary reduction and these boundary properties are substantial parts of the formalization.
Lean uses real cash flows and a probability measure on with , mass one on , and positive mass on every open subinterval. A published definition supplies Bayes-plausible measures on the Giry space of posterior measures and the two-cell reveal policy. The strict high cell is ; equality goes to the low cell and termination. Conditional means are ratios of restricted integrals to event probabilities, and every event used by the theorem has positive prior mass. Bounded support makes the relevant posterior means finite almost everywhere under a Bayes-plausible rule.
Two endpoint guards repair the source's literal Proposition 2. At , its asserted interval is empty. At , the interior equation need not have a solution: with uniform on and , its left side is positive for every positive threshold. The goal therefore assumes and . The paper's assumption (1), involving investor reservation value, is absent from the reduced problem (5), and Appendix A.1 treats a prior-mean case that assumption would exclude; it is not imposed here.
The comparison in the goal covers all Bayes-plausible accounting rules. The payoff uses the entrepreneur's posterior-mean response, including the tie rule. A development that compares only threshold rules or fixes the entrepreneur's action to the signal would not establish this target. Contributions to the binary reduction, conditional-mean continuity and uniqueness, and optimality of the two threshold cases are directly reusable.
In a linear bandit problem, a learner chooses a vector and observes a noisy scalar response that carries information about an unknown parameter. Regret analyses often need to control the sum of the learner's uncertainty in the directions it chooses. The familiar elliptical potential lemma does this when uncertainty is represented by the inverse of a deterministic, successively updated Gram matrix. Bayesian learning presents a different object: the posterior covariance of the unknown parameter given the observations. It changes with the realized data and can increase on an individual sample path. Hamidi and Bayati's technical note establishes a potential bound for this posterior object under general prior and noise distributions and uses it to analyze linear Thompson sampling.
The deterministic lemma and the posterior result answer related but distinct questions. In the deterministic setting, the update is fixed by the chosen vectors. Here, actions may depend on earlier observations and the next posterior covariance is itself random. The mission concerns the latter claim, including the observation model that gives the covariance its meaning.
Let be a probability space with an increasing filtration . An unknown parameter obeys almost surely. At time , the learner chooses an -measurable action with almost surely. An observation , measurable at time , has conditional mean and conditional variance at most when both and are known. No Gaussian law or independent noise model is part of these assumptions.
Write for the posterior covariance matrix. The quantity is the remaining parameter uncertainty in the chosen direction. The matrix function used to measure accumulated uncertainty is
The matrix order means that is positive semidefinite. Conditional expectations of matrices are taken entrywise. The filtration can contain information beyond the actions and observations; it need not be generated by them.
The first target is the source's stochastic variance reduction inequality. For every , almost surely,
The matrix potential targets are the concavity of on the positive semidefinite cone and equation (2.2): if , then
Two scalar and covariance bounds from the proof complete the milestone list: on , and almost surely. The main target, a conditional formulation of Theorem 2.1, is
The source prints an unconditional expectation on the left although can be random. Conditioning on supplies a coherent general statement; it becomes the printed display when the initial information is trivial. The goal retains the explicit factor and the horizon inside the log determinant.
The result controls a cumulative, adaptively selected posterior quadratic form using only the initial posterior covariance, the horizon and the conditional noise bound. It permits a regret analysis of linear Thompson sampling without replacing the prior by a Gaussian model. In the source, this bound feeds the Bayesian regret theorem for that algorithm; that later theorem is outside this mission's scope. Its proof would also require formalizing the sampling policy and its action-selection law.
The formal development fixes a reusable interface for finite-dimensional posterior covariance under a filtration: a parameter, adapted actions, conditional moments of observations, and an entrywise matrix covariance. It also states the matrix potential claims separately from the probability model, so those claims can serve other analyses of covariance updates. The statements compile locally as open Lean theorems; this mission does not claim machine-checked proofs of them. The deterministic elliptical potential statement already available elsewhere uses a Gram-matrix update and does not establish this posterior result.
Posterior covariance is not pathwise decreasing. The paper's Section 2 example has an observation after which . A bound that assumes for every outcome therefore fails at the first stochastic step. The issue matters especially when actions are adapted: later actions can point toward directions whose posterior variance became large after earlier data. Conditional covariance reduction is a matrix inequality, while the target is a scalar sum of quadratic forms; its potential must remain valid across those different objects.
Lean uses vectors Fin d → ℝ and the Euclidean dot product, so the unit-ball assumptions mean . The posterior covariance is the conditional expectation of centered coordinate products. The expectation of a covariance matrix is defined entrywise; matrix order is positive semidefiniteness of the difference. The conditioning sigma-algebra for is , not merely . Every observation is explicitly square-integrable, so Lean's totalized conditional variance cannot silently return zero for a non-square-integrable input. The source's bound on the parameter already supplies its integrability.
Rounds start at ; the finite sum uses . At it is empty and both sides of the goal are zero. No positivity assumption on is imposed, since the statements use and the zero-denominator covariance correction has zero numerator. The log determinant is used on positive semidefinite covariance matrices with nonnegative scalar argument, where its determinant is positive. The paper's square-root factorization of is represented by its equal direct matrix formula. A deterministic Gram matrix in place of , an independent-observation construction in place of the conditional-moment model, or a supremum-norm ball would change the theorem. The separate matrix and probability lemmas, conditional expectation infrastructure, and finite-dimensional matrix order are the principal reusable components.
Capacitated vehicle routing asks how to serve clients from a depot with vehicles that can carry only a limited load. In the unsplittable version, one vehicle must deliver each client's entire demand. This makes the choice of routes interact with bin packing: a short tour can fail because its total demand exceeds the vehicle's capacity. Approximation algorithms are therefore useful when exact optimization is impractical, and their guarantees must account for both travel distance and capacity. Friggstad et al., arXiv:2111.08138v1, pp. 1–2.
The paper distinguishes unit-demand, splittable-demand and unsplittable-demand CVRP. Earlier tour-partitioning methods gave constant-factor guarantees, while the paper's first main result is a combinatorial algorithm with ratio , where is an approximation ratio for metric traveling salesman tours. Taking gives the paper's stated ratio. The paper also gives a separate linear-programming-based improvement, which is outside this mission. These are results already proved mathematically; the mission concerns their precise Lean statements and a machine-checked proof of the combinatorial result. Friggstad et al., arXiv:2111.08138v1, pp. 2–3.
An instance consists of a finite set of clients, a separate depot , a symmetric nonnegative metric cost , and a demand for each client. A vehicle has capacity . A route starts and ends at , visits a sequence of clients, and carries at most one unit of total demand. A feasible solution is a collection of routes in which every client appears exactly once. Its cost is the sum of its routes' travel costs, and is the least such cost. The normalization to unit capacity and the positivity of every demand are standing assumptions of §2. Friggstad et al., arXiv:2111.08138v1, p. 4, Definitions 3–4.
For a threshold , a client is small when and big when . The radial sums are
The last sum is the cost of giving each big client its own depot route. Lemma 6 says . Friggstad et al., arXiv:2111.08138v1, pp. 4–5.
Algorithm 1 fixes . It obtains one traveling-salesman tour through the small clients and another through all clients. A consecutive split partitions the visiting order of a tour into capacity-feasible routes; is the minimum cost of such a partition. The algorithm also finds a minimum-cost matching with loops on the big clients, whose one- or two-client routes cost . It returns the cheaper of a matching plus a split of , and a split of . Friggstad et al., arXiv:2111.08138v1, pp. 7–8, Algorithm 1.
The first targets are the paper's intermediate bounds: Lemma 6's radial lower bound; the TSP lower bound used in §3.1; Claims 8–9 on the probabilities of the tank events; Lemma 7's -tank cost guarantee; Lemmas 10–11 on the matching; and the two branch estimates (4)–(5). These are the mission's milestones in the order in which their results are needed. Friggstad et al., arXiv:2111.08138v1, pp. 4–8.
The goal is Theorem 1. Let be the minimum depot tour length through exactly the client set , and suppose
For the specific cost
the goal says that a feasible solution attains and, for every feasible solution ,
Quantifying over every feasible solution expresses the ratio against without relying on a default value of a real infimum. Friggstad et al., arXiv:2111.08138v1, p. 2, Theorem 1; pp. 7–8, Algorithm 1.
The theorem supplies a cost guarantee for a concrete routing algorithm with a fixed threshold and two prescribed branches. It applies to unequal, indivisible client demands, while a unit-demand model cannot express the main capacity issue. The instance obtained from a -approximate TSP routine is a directly interpretable guarantee. The stronger LP-based theorem in §4 is a separate result and is not needed to establish this one. Friggstad et al., arXiv:2111.08138v1, pp. 2, 7–9.
A completed formalization would connect the paper's demand-aware CVRP model to a reusable published metric-route module, add definitions for optimal consecutive tour splitting and loop-allowed matching, and certify the stated branch and radial inequalities. Related platform results cover unit-demand VRP and TSP bounds, but their capacity and demand conventions differ. This mission introduces the unsplittable-demand statements rather than treating those unit-demand results as interchangeable.
The direct shortcut from a TSP tour to CVRP routes does not control capacity: a segment cheap in distance may carry too much demand. The big clients are especially restrictive at , since no feasible route can contain three of them. The tank lemma has to relate a partition of a fixed visiting order to the four radial terms with the exact coefficients shown above. The final ratio depends on comparing the two algorithm branches, including both matching bounds; an arbitrary feasible solution with a small cost would not establish a guarantee for Algorithm 1. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.
Lean represents the nodes by Fin (n+1), with depot and all other nodes as clients. A route is a nonempty list of clients, and a solution is a list of routes whose concatenation contains each required client once. The metric and route-cost functions come from the published SupplyChainTheory_vrp definition module; its unit-demand feasibility predicate is not used. The number of clients may be zero. Costs and demands are real, capacity is exactly , and every client demand lies in . The value at the depot is unused.
Each optimum in the statement is a real infimum over a finite, nonempty, nonnegative cost set for a valid instance. Singleton routes make the split and matching candidate sets nonempty; an ordering exists for every finite client set. The TSP inputs list exactly their intended client sets, and their guarantees refer to the corresponding TSP optima. The explicit condition records what the paper means by an approximation ratio. Lemma 7 is stated for any client subset because Algorithm 1 applies it both to the small-client tour and the all-client tour. Display (5) is an upper bound: the printed equality replaces the tour cost by upper bounds. The running-time assertions are outside this cost formalization. Friggstad et al., arXiv:2111.08138v1, pp. 5–8.
The goal bounds the cost of the specified algorithm, including attainment by a feasible solution. Merely asserting that some feasible solution has cost at most would be trivial, since an optimal solution already does. Contributions to the finite-tour, consecutive-split, radial, matching and tank-event lemmas are useful beyond the final ratio.
Firms that disclose a product carbon footprint can lower it in two ways: by cutting the emissions they control (better materials, cleaner processes), which costs money up front, or by buying carbon offsets from a third party at a constant price per tonne. Offsets have become cheap and widely available, and the business press has repeatedly argued that cheaper offsets let firms substitute away from costly abatement (The Wall Street Journal 2008, Forbes 2020 and The Washington Post 2020, as cited by Gao and Souza, p. 14). Whether that substitution actually happens matters for climate policy: if a lower offset price always raises a firm's own emissions, cheap offsets undercut real abatement.
Gao and Souza, Carbon Offsetting with Eco-Conscious Consumers (Management Science, 2022, doi:10.1287/mnsc.2021.4293), study this question in a model where demand responds to the disclosed footprint. Their Proposition 1 shows that the conventional intuition can fail in both directions of preference correlation: a cheaper offset can make the firm cut its controllable emissions. This mission formalizes that proposition together with the lemmas of its proof.
A firm sells to consumers. It chooses a controllable emission level per unit, which determines a unit cost and a fixed cost , with , , , on and . Each unit also carries uncontrollable emissions . At the offset price the firm offsets units, and discloses the footprint .
A consumer with valuation and environmental disutility gets utility at the price , and buys if and only if . A share of consumers is eco-conscious (); the rest are eco-unconscious (). A share of eco-conscious and of eco-unconscious consumers have the high valuation ; the others have , with , . The demand is the sum of the four segment masses whose utility is nonnegative, and the firm's profit is
A best response to is a feasible maximizing .
Two special cases carry the analysis: Case N (, negative correlation between caring about function and caring about the environment) and Case P (, positive correlation). For , the segment-optimal emission is the maximizer over of : the abatement level a firm chooses when it serves a segment of size and pays per unit of footprint. The proof compares the profit of covering the whole market at with that of serving only high-value consumers at ; their difference has a least zero , the offset price at which the firm switches.
In Case N, with , , a sign change of at its least zero , and condition (1) of the proof at , there are offset prices
for every pair of best responses (which exist), with strict emissions inequality when and . In Case P the analogue holds with , , and .
Proposition 1 identifies a mechanism by which cheaper offsets complement, rather than substitute for, controllable abatement. In Case N a lower offset price lets the firm lower its footprint enough to attract low-value eco-conscious consumers; in Case P it lets the firm price down to the low-value eco-unconscious consumers while keeping eco-conscious buyers. In both cases the served volume grows, and because abatement is a fixed cost, the larger volume makes deeper abatement worthwhile (economies of scale). The paper builds its NGO-pricing results (Propositions 2 and 4) on this subgame analysis.
The result is proved in the paper by a case analysis and derivative arguments; it has no machine-checked proof. Formalizing it produces a complete, checked treatment of a discontinuous best response in a pricing model with threshold demand, and it makes several steps of the published proof precise: where the paper asserts and "" without proof, the formal statements carry them as disclosed hypotheses, and the formalization of " for some " pins both thresholds down.
The best response is not a continuous function of : demand is a step function of price and footprint, so the firm's problem splits into six regimes (Online Supplement I1), and the optimal price jumps between , and the footprint-adjusted prices. Comparative statics by differentiating first-order conditions, the method of the paper's lemmas, applies only within a regime. The obvious argument, " is decreasing in by Lemma VI1", is wrong across the switch at : there the served segment shrinks, and Lemma VI1's monotonicity in the segment size works against its monotonicity in the price. Showing that the jump in segment size dominates requires controlling the best response on both sides of , including uniqueness of the best response and the behaviour of at the ends of where the first-order condition fails.
All quantities are real. The model is one definition file, EcoOffset.Subgame.Model, with a structure Params of primitives and a predicate Params.Standing bundling the standing assumptions of §3: , , , , , of class on with the sign conditions on on the closed interval , and . Prices range over all of ; consumers buy at zero utility. A best response is a predicate, never a chosen function, and the goal quantifies over every best response at and and asserts that one exists. is defined as the maximizer, not through the paper's root of the first-order condition (which does not exist at ). The switching price is a variable pinned by and on .
Added hypotheses relative to the page, all disclosed in the statements: (the proof's unproved ""; numerical Case N instances violate it); a sign change of at (the proof's unproved ); in Case N and in Case P (divisions in , ); for the existence of in Case N; explicit interiority conditions in place of "if is large enough".
Stating the goal about the two named profiles (for example ) would reduce it to Lemma VI1 plus algebra and is ruled out: the goal is about best responses of the full profit maximization. The paper's "for some " is likewise not used, since would make it vacuous.
A complete development needs: existence, uniqueness and continuity in of the maximizer of a strictly concave function on an interval (Berge's maximum theorem in one dimension); monotone comparative statics for ; the case analysis of the step-function demand; and intermediate-value arguments for . The first two are reusable for any one-dimensional parametric optimization. Proofs of individual milestones, and of the goal from the milestones, are welcome.
Electricity systems with hydro storage, and many other resource systems, are operated over time under uncertain inflows. In a centrally planned system a single risk-averse planner chooses releases and storage to minimize a nested (time-consistent) coherent risk measure of total cost. In a deregulated system the same decisions are taken by many agents, each with its own risk attitude, who trade the product, stored resources and financial instruments at market prices. A classical question of welfare economics is when the two coincide.
For risk-neutral agents the answer is the standard welfare theorems. Ferris and Philpott, Dynamic risked equilibrium (Operations Research, 2022), extend them to a multistage setting in which each agent evaluates risk with its own polyhedral coherent risk measure on a scenario tree and can trade Arrow–Debreu securities between each node and its children. Their First Welfare Theorem (Theorem 3) says that every such risk-trading equilibrium solves a social planning problem whose risk set is the intersection of the agents' risk sets. The converse direction, that a risk-averse social planning solution can be supported as a competitive equilibrium with risk trading (a Second Welfare Theorem), was shown for multistage hydro-thermal electricity markets by Philpott, Ferris and Wets (Mathematical Programming B, 2016). The forward direction is described in the 2022 paper as newly established there.
A finite scenario tree has nodes , root , leaves ; is the parent of and its set of children. A finite set of agents acts on it. At node , agent chooses releases and storage ; it has a cost , a production , a terminal storage value , and its storage evolves as with random supply .
Each agent's risk attitude is a polyhedral risk set at every non-leaf node,
a polytope of probability vectors on the children ; the one-step risk of a cost on is . The social planning risk set is (Definition 1), assumed nonempty (Assumption 3).
Prices are for the product, for agent 's storage, and for an Arrow–Debreu security bought at that pays in child . Agent buys of them. Its one-node disbenefit is
and its problem in complementarity form is the system , (20a)–(20g). A multistage risk-trading equilibrium RTE (Definition 3) is a set of prices and actions such that every agent solves and the product, storage and security markets clear, (21)–(23). The social planning system (p. 10) is the analogous eight-line complementarity system for a single planner with stage cost and risk set .
Every RTE with prices and actions satisfies, with :
Theorem 3 says that competitive trading of risk, through a complete set of one-step Arrow–Debreu securities, leads risk-averse agents with different risk attitudes to the outcome a risk-averse planner would choose if the planner used the intersection of their risk sets. The equilibrium security prices are the planner's worst-case probability measure. The paper uses the welfare theorems to indicate how social welfare might be compromised when risk markets are incomplete or illiquid, even if agents behave as price takers; its motivating example is a cascade of hydroelectric reservoirs operated by different agents.
The result is proved on paper. As far as a search of the Prove2Me catalog shows, no risk-trading equilibrium, nested polyhedral risk measure on a tree, or welfare theorem with coherent risk measures has been formalized. The mission produces a machine-checked statement of the multistage model (the agent problem, equilibrium and planning system, written out line by line) and of the welfare theorem. It also fixes the readings of a garbled clause of the printed statement and of one gap in the printed proof (see below).
Each step of the argument is elementary, but the bookkeeping is heavy. The model is indexed by agents, nodes, children, risk-set generators and storage components, and every condition is a finite sum over children. The proof of (24) has to show that, summed over agents, all payments cancel by the complementarity conditions (21)–(23), and this cancellation uses the agents' disbenefits at the grandchildren as well. Part (iv) is the substantive step. The natural first attempt, taking the multipliers of from Lemma 1 as the printed proof does, puts all weight on one maximizing generator. That reproduces the equilibrium price only when is itself a generator, and the fifth line of needs the multipliers to reproduce exactly.
The tree is the platform's StochasticProg.Multistage.Tree ( = children n, = anc n); a leaf is a node with no children. The normal cone is the platform's FirstOrderOpt.ConvexTheory.normalCone. The definition file DynRiskEq.Welfare.Model holds the market data, the risk sets, (18), (20a)–(20g), RTE (Definition 3), (Definition 1) and (p. 10). These are the model.
Committed conventions:
EuclideanSpace ℝ (Fin d);HasGradientAt), and every normal-cone condition includes membership in its set;The hypotheses of the goal are:
Convexity of , Assumptions 1, 2 and 4 and equal leaf depth are not assumed: Theorem 3 does not use them. The closing clause of Theorem 3 is read as the link and is part of the conclusion of (iv). Without it, (iv) would not say that the equilibrium price is the social worst-case measure.
The equilibrium does not contain or the conclusion , is not defined by (24), and keeps all eight lines of p. 10. A formalization that took any of these shortcuts would make the goal trivial.
Not formalized here:
Theorem 4 is the natural follow-up mission. General lemmas about maxima of linear functions over convex hulls of finite families are reusable beyond this mission, and contributions of them are welcome.
Platforms that estimate a population quantity from individual data, such as a health service estimating the mean response to a treatment, must compensate users for the privacy they give up. Users differ in how much they value privacy, and that value is private information. Differential privacy (Dwork, McSherry, Nissim, Smith, 2006) supplies a quantitative unit of privacy loss, so the platform can trade estimation accuracy against privacy at a price. Fallah, Makhdoumi, Malekian and Ozdaglar (arXiv:2201.03968v2, Operations Research, 2024) design the cost-minimizing mechanism that elicits users' privacy sensitivities, chooses a privacy level for each user, and pays them, when the platform's estimator is a weighted mean with Laplace noise. This mission formalizes their characterization of that mechanism in the central privacy setting (Theorem 3, p. 18).
Buying privacy at auction was studied by Ghosh and Roth (2011, arXiv:1011.1375); the paper's contribution is a Bayesian mechanism in which each user receives an individual privacy level and the estimator is chosen jointly with the payments.
There are users. User holds a data point , where the are i.i.d. with mean , variance and . A randomized algorithm on datasets is -centrally differentially private for if changing user 's entry changes the probability of any measurable output event by at most a factor (Definition 1, p. 8).
The platform uses an estimator of the central class (22):
which is -centrally private (Lemma 2) and has mean square error .
Each user has a privacy sensitivity , drawn independently with density and distribution function . A direct mechanism maps the reported profile to weights , a noise parameter , privacy losses and payments . A user of type who reports bears the expected cost
and a non-participant's cost is . The platform minimizes subject to incentive compatibility (truthful reporting is optimal) and individual rationality (truthful participation costs at most ). The virtual cost is , and Assumption 1 asks that each be increasing.
Under Assumption 1, let be an optimal solution of
The mechanism with , weights , and the payments of Proposition 1 is incentive compatible, individually rational, and minimizes the platform's expected cost among all such mechanisms of class (22). The statement holds for every measurable selection of minimizers.
Theorem 3 turns a mechanism design problem over function spaces into a finite-dimensional program solved separately at each type profile. Its consequences are that users with higher virtual cost receive less weight and less privacy loss (Corollary 1), that the optimal privacy level is a continuous function of the sensitivity rather than a threshold rule, and that the program can be solved in time (Proposition 3). The same reduction underlies the paper's comparison of central and local privacy.
The result is proved in the paper; no machine-checked version exists. The mission produces a verified payment identity for a setting where the allocation enters every user's cost through a shared externality (the MSE), a verified reduction to virtual costs that does not rely on differentiability of the mechanism, and the per-user Laplace mechanism on top of Mathlib's measure theory.
The classical Myerson argument assumes a linear objective and a single-dimensional allocation. Here the objective is non-linear and non-convex in the privacy losses, the MSE couples all users, and the minimizer of (23) has kinks where a coordinate reaches zero, so the paper's first-order derivation of the payment identity, which differentiates the interim cost, does not apply to the optimal mechanism, and the identity has to hold without any differentiability. A second obstacle is monotonicity: (23) is not convex and its minimizer need not be unique, so the monotonicity required by the payment identity cannot be read off from a unique smooth solution map; it has to hold for an arbitrary measurable selection of minimizers. Finally, the comparison is over all incentive compatible, individually rational mechanisms, not over a parametric family, so the measure-theoretic bookkeeping (interim expectations, exchanges of integrals over the type law) is part of the statement's content.
All quantities are real. Users are Fin n with 0 < n. Types live in compact intervals with , and is continuous, positive and integrates to one there; the paper's and integrals to become integrals to . The type law is the product of the laws with densities , and interim expectations over are integrals of against the type law. Incentive compatibility and individual rationality quantify over types and reports in . Class (22) makes and explicit. Mechanisms are required to be measurable, with bounded privacy losses and integrable MSE and payments; differentiability (Definition 3) and nonnegative payments are not required, since the optimal mechanism has kinks and may pay negative amounts. Assumption 1 is strict monotonicity. The feasible set of (23) adds , because at Lean's would make the objective vanish. Laplace noise is the published PrivLearn.Generic.laplace.
Stating Theorem 3 as " minimizes (23)", or comparing the mechanism only with mechanisms that already use the payment rule (19), would be a trivialization; the goal compares against every admissible, incentive compatible, individually rational mechanism of class (22).
Reusable infrastructure includes heterogeneous differential privacy, the per-coordinate Laplace mechanism, the variance of Laplace noise, and a payment identity under concavity without differentiability. Proofs of any milestone, and alternative arguments for the monotonicity of the minimizer, are welcome.
A financial transaction tax (FTT) charges a fixed fraction of the value of each securities trade. The idea goes back to Keynes (1936) and to Tobin's proposal of 1972, and it became policy after 2008: France (August 2012) and Italy (March 2013) introduced taxes on equity purchases, and the European Commission has proposed a common FTT (see the introduction of the paper below, pp. 2–3). The standard objection is that such a tax reduces trading volume and market liquidity, and therefore welfare.
Dieler, Biswas, Calzolari and Castiglionesi (Management Science 69(4), 2023; accepted manuscript of January 24, 2022, SSRN 2739357) identify a channel through which a transaction tax can raise welfare. Stock prices are read by firm managers when they decide on real investment. A market can be liquid but uninformative: trade then takes place at a price that does not reveal what informed traders know, and investment is inefficient. A tax that makes this liquid equilibrium impossible can move ("tilt") the market to an equilibrium in which prices are informative. The paper's headline result, Proposition 6, says when such a tilt is optimal and identifies the optimal tax.
There are two states, , with . A single informed trader with discount factor observes and buys a quantity of the firm's stock from a unit mass of competitive uninformed traders with discount factor , where . The buyer pays a tax proportional to the purchase value . After observing the trade, the uninformed traders set the price, and the firm's manager observes the price and invests.
Firm values are when the manager invests knowing , when she invests on the prior, and when she invests as if the state were the other one. They satisfy (1), and (3), and . Write . In §5 the paper specifies , , with (23); the parameter is the value of information.
A separating equilibrium is a pair of trades that reveals the state, so the price is and the firm is worth . A pooling equilibrium is a common trade at the price , and the firm is worth . Both must satisfy the informed trader's participation and incentive constraints, including deviations to any other quantity , which the paper's off-path beliefs price as the -state. Welfare is the expected sum of traders' payoffs and tax revenue, (8). In the Pareto-optimal pooling equilibrium () it is . In the Pareto-optimal separating equilibrium (, ) it is , where .
Suppose that without a tax both a pooling and a separating equilibrium exist (Proposition 4 (ii) at , with strict participation of the low type), that , and that
where is the tax at which . Then . Moreover:
Together these say that the smallest tilting tax is the optimal FTT and that it is strictly positive.
Proposition 2 (separating equilibria and the bounds ); the monotonicity ; Proposition 3 (pooling equilibria exist iff (22)); Proposition 4 (which equilibria coexist); the welfare formulas (24)–(25); Corollary 1 (ii) (a high enough tax rules out pooling); the step and the step of the proof of Proposition 6; and the existence of parameters satisfying all hypotheses of the goal.
The result turns a qualitative policy argument into a formula. When information is valuable relative to the liquidity gains from trade, the welfare-maximizing tax is the threshold . This threshold is determined only by the discount-factor ratio and the information gap , and it is strictly positive. It does not depend on the level of pooling trade. A tax larger than only destroys more trade in the separating equilibrium. A tax at or below changes nothing.
The paper's proofs are explicit algebra. A formal development checks them, and the drafting already found several places where the printed statements are wrong at a boundary:
The mission states the corrected versions. None of these results has a machine-checked proof.
Each step is elementary real algebra, but there are many of them, and they all depend on the deviation constraint. The informed trader may deviate to any quantity , so every equilibrium condition quantifies over a continuum. In the pooling case the binding deviation is , which is excluded when . Characterizing the equilibria therefore needs a supremum argument over a punctured interval, not a finite check. The goal combines both characterizations with a sign analysis of the linear-fractional function and the order of , and . A tempting shortcut is to identify equilibria with the closed-form conditions (17) and (22). That assumes Propositions 2 and 3, which are themselves milestones.
All objects are real numbers. There is no probability space: expectations over the two states are written out as . The parameters form a structure Firm. The hypotheses are named predicates: Standing for (1), (3), , , , together with the disclosed readings and ; Spec23 for (23); and Coexist for Proposition 4 (ii). Every ratio condition is cross-multiplied, so division by zero never decides a statement. The bounds , , and the taxes , , are the printed closed forms. They are used only where their denominators are positive.
The equilibrium predicates IsSeparatingEq and IsPoolingEq encode the paper's participation and incentive constraints (14), (16), (31) and (20), (21) directly, with the deviation ranging over all of except the equilibrium trades. They are not defined through the existence conditions (17) or (22). Welfare is the bracket of (8), evaluated at the realized firm values, not the closed forms (24)–(25). These choices rule out the trivializing formalization in which the propositions hold by definition.
Not formalized:
Only Mathlib's ordered-field and calculus libraries are needed. Proofs of any milestone are welcome. The supremum lemma for punctured intervals is reusable in other signaling models with a continuum of deviations.
Dividing indivisible goods fairly is a central problem of fair division, with applications from inheritance and course allocation to the division of computing resources. Since envy-free allocations of indivisible goods need not exist (one good, two agents), the field studies relaxations. The most prominent is envy-freeness up to any good (EFX): no agent prefers another agent's bundle after removing any single good from it. Whether EFX allocations always exist for additive valuations is one of the main open questions of the area; Plaut and Roughgarden (arXiv:1707.04769) suspected that they may not exist for general valuations.
Two lines of relaxation have been pursued: weakening the envy condition by a factor , and leaving some goods unallocated ("charity").
There are agents and a finite set of goods. Agent has an additive valuation: with . A partial allocation consists of pairwise disjoint bundles ; the goods in none of them form the pool of unallocated goods.
For , is -EFX if
Fix . Agent heavily envies a set if and strongly envies if it heavily envies a proper subset of . The envy graph has an edge when ; a source is an agent nobody envies.
The rainbow cycle number (Definition 2) is the largest for which there is a directed graph whose vertex set is split into parts, each of size at most , such that every vertex has an incoming edge from every other part, but no directed cycle visits each part at most once. In the paper the parts of such a graph are indexed by low-demand unallocated goods, and the graph records which agents are "champions" for which bundles (the group champion graph).
For all , all additive valuations and all there is a partial allocation that is -EFX and leaves a pool with
For every , is finite and
equivalently, every digraph with more than parts of size at most in which every vertex has an incoming edge from every other part contains a cycle visiting each part at most once.
The milestones follow the paper's proof: the update rules U1, U2, U3 (Lemmas 8–10) and envy-cycle elimination (Lemma 6); the high-demand bound under the standing assumption (*) (Observation 12); the in-edge property of the group champion graph (Observation 13); the conversion of a rainbow cycle into a strictly Pareto-improving allocation (Lemma 14, Lemma 16); and the final count with .
The result. Theorem 1 is the first guarantee for EFX-type allocations in which the number of unallocated goods grows sublinearly in the number of agents. It shows that the relaxation by a factor can be traded for a large reduction in charity, and it isolates a purely graph-theoretic quantity, , whose improvement directly improves the bound: would give unallocated goods. For (about at ) the goal already follows from the bound of Chaudhury et al. 2020, which is posed on the platform but unproved; the content of the goal is the sublinear regime of large .
Formalizing it. The theorem is proved in the paper; it has no machine-checked proof. A formalization produces a reusable account of approximate EFX, most envious agents and the update rules, and a standalone combinatorial theorem on cycles in multipartite digraphs that can be reused independently of fair division. Sharper bounds on , or the paper's existence bound in terms of , are natural follow-ups.
The fair-division part is a potential argument: as long as one of the update rules applies, the allocation strictly improves, and the work is to show that a rule applies whenever too many goods are unallocated. The high-demand goods are counted directly. The low-demand goods are the hard part: a rule applies to them only if the group champion graph has a cycle that uses each good at most once, and nothing about a single good or a single pair of goods forces such a cycle. A Ramsey argument on the configurations between pairs of parts shows that is finite, but only with a bound exponential in , which does not give a sublinear count. The polynomial bound requires a different construction.
Agents are Fin n and goods Fin m, with all of Fin m as the set of goods; valuations are Fin n → Finset (Fin m) → ℝ with the published predicate LittleCharity.MMS.IsAdditive. Allocations, the pool, the envy graph, sources and reachability come from the published LittleCharity.EFX.Setting. The mission's own definitions are in RainbowEFX.Sublinear.Setting.
Conventions committed to:
rainbowCycleNumber d ≤ d^4 + d would hold vacuously for an unbounded set.A formalization in which the pool is an independent variable, the factor is replaced by a weaker one, or is computed as a junk supremum would trivialize the targets; the statements rule these out. The development needs basic finite combinatorics of digraphs and finite sets, and finite sums of real valuations; no measure theory or probability. Proofs of the update rules, of Theorem 3, and of any milestone independently are welcome.
A merger can give a firm access to data generated in a different market. Its effect on consumers depends on what the data do and whether firms could buy them before the merger. In Data-Driven Mergers, Alexandre de Cornière and Greg Taylor study a firm A whose customers generate data useful to two firms in a second market. Their product-improvement example has a sharp reversal: when data cannot be traded, the merger benefits consumers in both markets; when independent firms can already trade data, the merger harms consumers in both markets. This mission formalizes the latter claim, Proposition 2 of the TSE working paper.
The question matters for evaluating mergers across data-connected markets. A merger between A and one downstream firm changes who receives the returns from collecting data. The relevant comparison is therefore between two ownership structures operating under the same possibility of data trade, rather than a comparison that silently gives trade to only one side. The published article treats both the product-improvement example and a broader model of data use; the present target is the paper's explicit quality example.
Firm A is a monopolist in market A. At price it serves consumers, where . Serving consumers also produces a data set of size . A can sell this data set to one or both firms in market B, a Hotelling duopoly on the unit interval. Firm B1 is at one end and B2 at the other; transport cost per unit distance is one. Data held by firm improve its product quality to , while a firm without A's data has quality .
For data quantities held by one B firm and its rival, denotes that firm's equilibrium price and its equilibrium profit. For prices , its interior demand is
The paper's equilibrium formulas are and . Quality-adjusted price means : the price after accounting for the quality the buyer receives. Market-B consumer surplus integrates each consumer's quality less price and travel cost over the two firms' market shares. Market-A consumer surplus is .
At the first stage, A chooses its market-A price. At the second stage it can supply its data exclusively to one independent B firm or supply both. The price of one exclusive licence is ; the per-firm price of nonexclusive licences is . Under a merger, A and B1 maximize their combined returns and may still license B2. After the data allocation, B1 and B2 compete for consumers. These formulas and timing follow Sections 3–4 of the working paper.
The central target is Proposition 2. Let maximize the independent A's objective and maximize the merged A–B1 objective, each including the choice of one or two data licences. Label the independent exclusive buyer first so corresponding B firms can be compared across regimes. The claim is
The six milestones follow the paper's stated steps. Lemma 2 says a B firm's profit rises with its own data, falls with its rival's data, and consumer surplus rises with either firm's data. Lemma 1 gives the ownership-independent criterion for an exclusive allocation. Section 4.3 then says exclusive supply is optimal in the quality model and that the merged firm collects less data than independent A. The goal collects the price and welfare consequences of these comparisons. The target and milestone statements are from printed pages 6–9 of the working paper.
Under trade, independent A can earn more by collecting data that a B firm values partly because its rival lacks them. After merging with B1, A–B1 internalizes the quality benefit to B1 but faces a different return from serving an additional A customer. Proposition 2 records the outcome at optimal prices: fewer A customers are served, quality-adjusted B prices rise, and consumers lose surplus in both markets. This is a concrete merger comparison for an economy where data can already be sold, as the authors emphasize in their abstract and Section 4.3.
The result is proved in the paper but has no machine-checked proof in this mission. A completed development would certify the two-stage objective, the data-allocation decision, the comparative statics, and the two welfare calculations together. Its definitions of data prices, Hotelling demand, equilibrium price and profit, and consumer surplus can also support later work on the paper's no-trade result, Proposition 1. The more general model of Section 5 and the strategic-consumer appendix are outside this mission.
The first-stage objective is not a single smooth expression: it takes the better of an exclusive sale and a sale to both B firms. An argument that starts directly with the exclusive-sale formula skips the allocation decision that Lemma 1 and Section 4.3 establish. The comparison must also connect different optimal A prices to data quantities, then carry that change through two B-firm prices and an integral of consumer utility. The B firms' prices rise with own quality, but consumer welfare depends on quality net of those prices, so the direction of the price effect alone does not settle the welfare effect. The paper's Lemmas 1–2 and Section 4.3 state the claims used at these stages.
All prices and quantities are real; A's price ranges over all of , and the relevant data quantities satisfy . The formalized is the paper's interior linear-demand formula. The standing assumptions make the verbal requirements that market B is covered and both firms are active explicit: and for . The model assumes is differentiable everywhere and . It strengthens the paper's non-decreasing to for , because the paper states strict inequalities in Lemma 2 and Proposition 2, which fail for a constant . Footnote 11's second-derivative concavity condition is omitted; the target quantifies over any maximizers and does not require that condition.
The licence prices are the paper's equilibrium formulas. Bidding strategies and the equilibrium-selection detail in footnote 9 are not encoded. Both first-stage objectives retain the maximum over the one- and two-licence branches, so exclusive supply is a result to establish. Equality in the exclusivity test takes the nonexclusive branch; at both allocations coincide. Market-B surplus uses the paper's two integrals, and the B-firm comparison matches the data holder to the data holder. These conventions exclude an encoding in which the conclusion is true simply because exclusivity was inserted into A's objective. The reusable work includes the model definitions, the generic ownership-independent Lemma 1, and the derivative and welfare lemmas. Proofs of these statements and of the goal are welcome.
When a leveraged financial institution suffers a loss, a leverage constraint can force it to sell assets. If several institutions hold the same assets, their simultaneous sales depress prices and impose losses on everyone holding those assets. These fire-sale spillovers were a central amplification channel in the 2007–2009 financial crisis (Greenwood, Landier and Thesmar, 2015, doi:10.1016/j.jfineco.2014.11.006; Cont and Schaanning, 2017, SSRN 2541114). Regulators who monitor systemic risk care about two different quantities: how likely it is that some institution is forced to sell, and how likely it is that several are forced to sell at once.
A. Capponi and M. Weber ask how banks choose portfolios when they anticipate fire sales by others (SSRN 3345399, published in Operations Research, doi:10.1287/opre.2022.0290). In their model, banks with different leverage choose deliberately different portfolios in equilibrium. They call this systemic diversification. Its effect on the two quantities above goes in opposite directions.
There are banks and assets, each with price one at date 1. Bank has total assets , leverage ratio (debt over equity, so ) and a leverage threshold . At date 1 the bank chooses portfolio weights in the simplex .
At date 2 the asset prices change by the random vector , and bank 's return is . Its new leverage is . If , the bank sells the amount that restores the threshold:
Sales are proportional to holdings. Asset trades at a discount proportional to the total amount sold, with illiquidity parameter . The realized liquidation cost of bank is
and bank minimizes given the others' portfolios. The distance to liquidation is the smallest loss that forces a sale: bank sells exactly when , and then .
The expected cost splits as . Here is the cost bank would bear alone, and is the cost bank 's sales add. The single-bank benchmark minimizes on ; a Nash equilibrium is a profile from which no bank gains by deviating alone. The game has the potential .
The shock satisfies Assumption 3.3: is spherically symmetric, and each has a continuous density that is increasing on . Assumption 3.6 asks that be strictly convex on . Assumption 3.7 asks that every be at most a sufficiently small .
For two banks and two assets with and , the equilibrium raises the probability that at least one bank liquidates and lowers the probability that both do:
Proposition 4.4 says that heterogeneous banks move apart in equilibrium: the more leveraged bank tilts further toward the liquid asset, the other toward the illiquid one. Proposition 4.5 turns this into probabilities of distress. Lower portfolio overlap makes joint liquidation rarer, but each bank holds a less diversified portfolio, so liquidation by some bank becomes more frequent. The trade-off between individual and systemic diversification underlies the paper's welfare comparison (§5) and its discussion of Pigovian taxes (§6). It is a statement about the shape of the equilibrium, not about any particular constant.
The results are proved on paper, with arguments that are partly informal ("by continuity", "sufficiently close"). They have not been formalized anywhere. A formalization would make those steps precise: it fixes the order in which and the closeness of are chosen, and it checks the measure-theoretic interchange of derivatives and expectations. Along the way it builds a reusable model of leverage-driven fire sales and of spherically symmetric shocks in Lean.
The equilibrium has no closed form, so nothing can be computed directly. The comparison with the benchmark rests on the sign of a cross-partial of the potential, which is an expectation over the intersection of two half-planes. This sign is positive at , through an explicit integral in polar coordinates, and stays positive for small only by a uniform continuity argument. The probability comparison of Proposition 4.5 then needs the equilibrium weights to stay on the correct side of , which is where the closeness of and enters. One might try to compare equilibrium and benchmark through first-order conditions alone. That fails: both banks' conditions move together, and their joint movement is controlled only through the monotone best responses that Lemma A.2 provides.
The shock law is a probability measure on EuclideanSpace ℝ (Fin K). Spherical symmetry is invariance under every linear isometry, which is stronger than exchangeability. Each marginal has a continuous density, weakly increasing on . Portfolios are functions Fin N → Fin K → ℝ, the action set is stdSimplex ℝ (Fin K), and for two assets is written two t. Bank 1 and asset 1 are index 0.
Liquidation is the model's leverage rule, written cross-multiplied, and the amount sold solves (2.1). The closed form of Lemma A.1 is a theorem, not a definition. Every theorem that integrates a cost assumes ; without it Lean's integral of a non-integrable cost is .
The following hypotheses are added, each disclosed in its statement:
In Assumption 3.7, is chosen after the law, the illiquidities, total assets and thresholds, and before the leverages.
Results are quantified over every Nash equilibrium and every benchmark optimum. A formalization that fixes a particular equilibrium, replaces the probabilities by expected costs, or assumes the ordering of portfolio weights would be trivializing, and is ruled out.
Needed infrastructure: differentiation under the integral sign for piecewise-quadratic integrands, polar coordinates for rotation-invariant laws on , and convex-analytic facts about potential games. The first two are reusable well beyond this mission. Proofs of any milestone, and sanity lemmas showing the hypotheses are satisfiable (for instance by the standard Gaussian), are welcome.
In the principal–agent model a single agent takes a costly action on behalf of a principal who sees only the action's stochastic outcome, and pays the agent according to that outcome. Many practical relationships have one agent and several principals: a manager and the shareholders, a freelancer and several employers, a marketing agency that bids for ad space on behalf of several advertisers. Bernheim and Whinston introduced this common agency model in 1986 (Econometrica 54(4), 923–942). With several principals there are two problems at once: coordinating principals who act noncooperatively and have private valuations, and the hidden-action problem of contract design.
Lavi and Shamash (EC 2019) proposed VCG contracts for common agency when the agent's action is observable. Alon, Lavi, Shamash and Talgam-Cohen (arXiv:2105.14998, Operations Research 2024, Technical Note) extend the approach to hidden actions. They define the family of incomplete information VCG (IIVCG) contracts and show that it is the unique family that makes truthful reporting dominant for the principals and makes the agent maximize declared welfare. They also show (their Theorem 3) that an IIVCG contract need not be both limited-liability and individually rational, even with one principal. This mission formalizes their main positive result: whenever some IIVCG contract has both properties, an explicit, algorithmically defined contract ALG1 has them too.
A common agency setting has a finite set of actions with pairwise distinct costs , a finite set of outcomes, and for every action a probability distribution on . There are principals. Principal has a valuation taken from a nonempty convex domain . Write .
The principals report bids , and denotes with principal 's bid replaced by . The declared welfare of action is
and denotes the welfare-maximizing action, ties broken towards the highest cost.
A contract specifies the payment from principal to the agent when the bids are and the outcome is . The agent chooses an action maximizing . Among maximizers he takes the one of highest declared welfare, and among those the costliest. The properties studied are:
The algorithm uses four derived quantities:
Contract ALG1 (Definition 4, Algorithm 1) takes an optimal solution of the linear program defining and weights summing to one with . It then pays
and such choices exist. The polynomial-time half of Theorem 5 is not part of the target.
Theorem 5 turns an existence question into a construction. Once the setting admits any IIVCG contract with both participation guarantees, ALG1 is one, computed from three linear programs per bid profile. Combined with Proposition 1 (every IIVCG contract is truthful), ALG1 is a truthful, welfare-maximizing contract under which the agent never pays out of pocket and no truthful principal loses in expectation. Lemma 2 shows that the obstruction found in Theorem 3 is the only one: it is exactly the failure of .
The results are proved in the paper. No machine-checked version of the IIVCG theory exists. Mathlib has no contract-theory or principal–agent library, and the platform's published VCG developments concern allocation mechanisms with an observable outcome and no agent action. A complete development yields a reusable formal model of hidden-action contracts with several principals, including the agent's tie-breaking rule. It also needs a linear-programming attainment fact that is useful beyond this mission.
Definition 2 constrains only expected payments under one action, while limited liability is an outcome-by-outcome condition and the agent's incentive constraint involves every action. A first attempt adjusts the expected-payment formula outcome by outcome. That fails because the payments must also make the agent's choice under the tie-breaking rule, and this couples all principals through (Lemma 1). The two bounds then point in opposite directions. IR caps each principal's expected payment by (Claim 1), and LL with incentive compatibility forces the total to be at least (Claim 2). The contract must split the cheapest implementing payment among the principals inside both bounds at once. Two further points need care: the minima defining and range over sets that need not be compact, and the agent's choice must be pinned down through the tie-breaking rule.
Principals are Fin n, a bid profile is Fin n → O → ℝ, a contract is t b ℓ o, and is Function.update b ℓ w. Expectations are finite sums. The standing assumptions are those of §2: finite nonempty action set, finite outcome set, distinct costs, probability vectors , and nonempty convex domains of non-negative valuations. is added; with no principals the weights cannot sum to one. Convexity is kept although unused. The polynomial description of the domains and every polynomial-time claim are dropped. is the welfare maximizer of highest cost, the reading under which footnote 9 says it is unique, and the same is used in IIVCG, , and ALG1. The paper's minima are real infima over nonempty sets bounded below. ALG1 is parametrized by the choice of optimal LP solutions, and the goal quantifies over all admissible choices and asserts that one exists.
The goal must not take as its hypothesis (that is Claim 3). It must also not quantify over arbitrary contracts "with Algorithm 1's properties": ALG1 is the explicit formula of Algorithm 1, line 8. A sorry-free sanity file exhibits a setting satisfying the standing assumptions with an IIVCG contract that is LL and IR, so the goal's hypothesis is satisfiable.
Contributions are welcome on the milestones in the listed order. The LP-attainment step (Proposition 4) and the infimum bookkeeping for and are reusable.
Cake cutting is the standard model of fair division for a divisible, heterogeneous resource: the cake stands for time on a shared machine, a stretch of coastline, or bandwidth over a time window, and agents value its parts differently. The central fairness notion is envy-freeness: every agent weakly prefers its own piece to every other agent's piece. When pieces must be contiguous intervals, as with time slots or land, envy-free allocations exist under mild assumptions (Stromquist, 1980; Su, 1999), but no finite protocol finds one when the valuations are accessed through queries (Stromquist, 2008), and finding one is PPAD-hard under ordinal valuations (Deng, Qi and Saberi, 2012).
Barman and Rathi (arXiv:2006.00481, Mathematics of Operations Research, 2022) identify a structural condition from statistics and economics under which the problem becomes tractable: the monotone likelihood ratio property (MLRP). Agents' value densities can be ordered so that each consecutive ratio is nondecreasing. MLRP holds, for instance, when all densities are Gaussian with a common variance, Poisson, binomial, single-parameter exponential, or linear, and for linear translations of any log-concave density (Barman and Rathi, §1).
A cake-division instance consists of agents, and agent has a value density , bounded and integrable, normalized so that . Agent values an interval at . A contiguous allocation is given by cut points , and agent receives . It is envy-free up to if for all agents .
Access to the densities is through Robertson–Webb queries. returns a value. returns the leftmost with , or if there is none. The queries are -Lipschitz () when both functions are -Lipschitz in the -norm. Running times are measured in , and .
Under MLRP, the densities are strictly positive and, after reindexing, is nondecreasing on for every . Fixing the first cut point and requiring for determines all later cut points. The resulting last cut point is the ripple map , which is a composition of queries (recursion (1)). A -ripple division is such a chain of cut points with and positive values. BinSearch (Algorithm 1) bisects on the first cut point until of the midpoint lands in .
There is a universal such that, for every MLRP instance with -Lipschitz queries and every , BinSearch with first returns at an iteration with
and giving the leftover to agent turns its output into a contiguous allocation of that is envy-free up to . The goal fixes neither the degree nor the constant of the polynomial.
Theorem 1 marks a boundary in the complexity of contiguous envy-free division. In general there is no finite protocol and no efficient approximation is expected. Under MLRP the problem admits an algorithm that is polynomial in , and , so the precision can be made exponentially small at polynomial cost. The same ripple structure underlies the paper's further results: every envy-free allocation is Pareto optimal under MLRP, and social, egalitarian and Nash welfare can be optimized efficiently. Theorem 6 is also a structural fact in its own right. Under MLRP, envy-freeness reduces to the local equalities between neighbouring agents.
The result is proved in the paper. To our knowledge none of it is formalized: neither the cake-cutting query model nor monotone likelihood ratios of densities exist in Mathlib or on the platform. This mission produces a machine-checked model of contiguous cake division with Robertson–Webb queries and a verified complexity statement for a cake-cutting algorithm.
The algorithm is short, but its analysis combines three ingredients that do not reduce to one another. Envy-freeness of a ripple division (Theorem 6) is not a local statement. Agent is only constrained to be indifferent between its own interval and its right neighbour's, yet it must not envy any interval, far to the left or right. Bridging that gap is exactly where MLRP enters, through the interval-ratio inequalities of Lemma 1. The running-time bound needs a quantitative continuity statement for a -fold composition of queries (Proposition 1). In Lean this composition passes through the truncating Cut query, whose value is defined by an infimum and a convention. Finally, positivity of the ripple values is not assumed. It has to be extracted from the Lipschitz continuity of Cut, because the existence and complexity lemmas do not assume MLRP.
The model is one definitions file, MLRPCake.EnvyFree.Model.
Fin n; agent i is the paper's agent ). Cut points are a sequence x : ℕ → ℝ, and agent i receives [x i, x (i+1)].eval integrates over Set.Icc ℓ r and is for . cut returns the infimum of the solution set and 1 when it is empty, never Lean's sInf ∅ = 0.The goal cannot be met by an existence statement. It bounds the first stopping iteration of the algorithm as defined, with a polynomial whose constant is chosen before the instance. It certifies both that the coalesced output is an allocation of the whole cake and that it is envy-free up to . Stating only that some -envy-free allocation exists, or bounding the iterations by an instance-dependent constant, is not Theorem 1.
A complete development needs basic interval-integral calculus for densities (continuity of , attainment of the Cut infimum), the intermediate value theorem, and a binary-search invariant argument. The query model and Lemma 1 are reusable for the paper's later results (Pareto optimality, welfare maximization) and for other cake-cutting formalizations. Proofs of any milestone and of auxiliary facts about cut and rd are welcome.
Online retailers and platforms summarize the experience of past buyers for future buyers. Some show only an average rating, a single number; others show full reviews, from which a reader can tell who the reviewer was and how well the product suited them. Sellers of new products, in turn, decide whom to advertise to in the launch period, and digital advertising lets them target narrowly. These two decisions interact: the people reached by the launch campaign are the people who later write the ratings.
Fainmesser, Lauga and Ofek (Management Science, 2021) study a monopolist that launches a product of unknown quality, chooses how broadly to advertise it and how to price it, and faces a second generation of consumers who learn from the first generation's user-generated content. Their first result, Proposition 1, compares three information structures and finds that an average rating, unlike full reviews or no information at all, makes the firm advertise to fewer consumers and charge a higher launch price. The mechanism is that later consumers cannot see whom the firm targeted, so a broader campaign, which brings in buyers who like the product less, lowers the average rating and with it the quality later consumers infer.
There are two periods and two generations of consumers, each a unit mass spread uniformly on a circle of length 4 (a Salop circle). The product sits at a location known to the firm, and has quality drawn uniformly from . A consumer's utility from buying is , where is the value of quality, the cost of a unit of distance between the consumer's location and the product, and the price.
In period 1 the firm chooses a price and an advertising interval of length , , centred at , at cost . Only consumers inside the interval learn of the product; they do not see and hold a belief . First-period demand is
The mean net utility of first-generation buyers, the average rating, is
In period 2 all second-generation consumers learn of the product and the firm sets . What they learn about quality depends on the information structure:
The firm maximizes total expected profit . The solution concept is a pure-strategy perfect Bayesian equilibrium (PBE): consumers' belief equals the firm's choice ; the second-period price is optimal at every information value; and no deviation raises when consumers keep the belief .
The paper's standing assumptions are and, for the cost, , , and .
Each of the three cases has a PBE, and for any equilibria (Benchmark), (Reviews), (AR),
the second-period pricing rules of the Reviews and AR cases coincide and are strictly increasing in quality, and .
and every root of (7) in is a PBE. 4. The AR term: the expected optimal second-period profit has derivative in at . 5. Unique roots: (7) and the AR condition
each have exactly one root in , and it is interior. 6. Lemma 2 (AR, necessity): every AR PBE solves (8) with , and , . 7. Lemma 2, sufficiency: the root of (8) with these prices is an AR PBE. 8. Lemma 3 (Reviews): every Reviews PBE solves (7), coincides with the Benchmark in period 1, and every root of (7) is a Reviews PBE.
Proposition 1 is the paper's base result: Proposition 2 (average-rating dynamics), Corollary 1 (the AR/Reviews rating reversal) and Proposition 3 (welfare) are all read against the equilibria it characterizes. It gives a testable prediction, that a seller facing an average-rating system targets more narrowly and prices its launch higher than one facing full reviews, and it isolates the channel: consumers' inability to observe the firm's targeting makes the rating manipulable through the advertising decision, the classic signal-jamming structure in a marketing setting.
The result is proved in the paper, with the derivations of the demand functions in a Technical Appendix. No machine-checked proof of any part of it is known. The mission produces a checked version of the equilibrium characterization, including the existence half, which the paper establishes only in the sufficiency part of the proof of Lemma 2, and an exact statement of the interiority assumption the paper leaves qualitative.
The Benchmark and Reviews cases are routine: the second-period profit does not depend on , the first-period problem is concave, and the first-order conditions characterize the equilibrium. The AR case is not. The inferred quality is clamped to , so the expected second-period profit is only piecewise smooth in the firm's deviation , and it is convex, not concave, for upward deviations. The first-order condition (8) is therefore necessary but does not by itself show that the candidate survives large deviations; that needs the curvature bound against the convexity of the expected profit on each side of . The derivative at also has to be taken through an expectation whose integrand has a moving kink.
Everything lives in the namespace RatingsAdvert.AdInterval, built on one definition file Model.
Params with fields tau, beta and A : ℝ → ℝ. Standing bundles , , of class , , and , on , . Positivity of and the requirement are added; the page divides by and uses , .Interior: and , exactly the statement that the roots of (7) and (8) lie in . It is the quantified form of the paper's "sufficiently convex … to guarantee that the solution is interior"; without it a corner can be an equilibrium.The infrastructure needed is elementary real analysis: concavity of the first-period problem, differentiation of an interval integral with a clamped integrand, and the intermediate value theorem. Contributions of proofs of any milestone are welcome; the AR sufficiency and derivative milestones carry the main work.
Retailers run two kinds of temporary promotion on staple products. A price reduction (PR) cuts the price of every unit for a while; a buy-one-get-one (BOGO) offer leaves the price of the first unit alone and discounts a second unit bought at the same time. Both are common in grocery retail, and in practice the manufacturer sets the wholesale price before the retailer decides which promotion to run. Which promotion a retailer should prefer, and how the choice moves profit between the manufacturer and the retailer, is a basic question in the operations and marketing literature on trade promotions.
Li, Khouja, Pan and Zhou (SSRN 3561162; Management Science, 2022, doi:10.1287/mnsc.2022.4638) model this as a two-echelon Stackelberg game with consumers who value a second unit less than the first. Their headline result for the case without consumer stockpiling (Corollary 4, pp. 23–24 of the working paper) is that, whenever both promotions are adopted in equilibrium, the manufacturer is indifferent between them while BOGO gives the retailer, and the supply chain as a whole, strictly more profit. This mission formalizes that statement about the equilibria of the model.
A unit mass of consumers has valuations uniform on . In each of two periods a consumer values the first unit at , a second unit at with , and further units at nothing. A consumer buying units in period 1 and in period 2 takes the purchase option .
Each consumer picks a utility-maximizing option. At wholesale price the retailer's profit is the expected margin of the chosen options, and the demand is the expected number of units. The manufacturer, with unit cost , earns .
There are three games. In the BOGO game the retailer may set a single price or run a BOGO; in the PR game, a single price or a PR; in the NP game, only a single price. In each, the manufacturer leads: an equilibrium is a wholesale price and a retailer strategy that is a best response at every , such that maximizes . The thresholds of the paper are
Fix and with . Take equilibria of the three games and write (BOGO), (PR), (NP) for the manufacturer's and retailer's profits. Then
and for also , , , and the retailer's share of supply-chain profit is strictly largest under BOGO; at , . Across two values in the region, the price gap , the advantage and the BOGO share strictly decrease.
The corollary separates the two effects of a promotion. Because both promotions lead to the same wholesale price and the same expected demand, the manufacturer's profit does not depend on which one the retailer runs; the entire extra supply-chain profit from BOGO goes to the retailer. This is the paper's case that BOGO is a profit-reallocation device within the channel rather than a demand-creation device. The comparison with the NP benchmark shows that, in this region, both the retailer and the supply chain gain from running BOGO rather than no promotion.
The paper's working-paper version contains no proofs (they are in a supplementary file), and none of the statements has a machine-checked proof. A complete development here checks the full chain from consumer choice to the manufacturer's optimum. It also pins down the exact domain of the claims: the strict comparisons fail at , Proposition 3 as printed leaves uncovered, and Proposition 4 b) does not hold as an equilibrium statement, because the PR demand jumps at . The statements in this mission are corrected accordingly.
The closed forms of Table 3 make Corollary 4 a matter of rational-function algebra once the equilibria are known, and that is the trap: the content lies in showing that the equilibria are exactly the Table 3 outcomes. The retailer's problem is a piecewise maximization over several consumer segmentations, compared against the single-price option on the same menu. The manufacturer's problem is then a maximization against a discontinuous best response, whose thresholds , , involve square roots. In the PR game the retailer is indifferent at between two policies with different demands. Any argument that treats the best response as a continuous function of fails there.
All quantities are real numbers. Profits and demands are interval integrals over of the margin and the number of units of the option each consumer chooses. Among tied options a consumer takes the one with more units, which affects only a null set. Feasible prices are nonnegative with and ; the page's strict has no optimum at . Wholesale prices range over . The retailer's strategy is a function of the wholesale price, so the equilibrium is subgame perfect, and ties of the retailer are resolved by the strategy, not by assumption. All of Corollary 4's claims are stated for every equilibrium, so the goal cannot be discharged by substituting Table 3, and profits are defined from consumer choices, not by the paper's formulas. The strict comparisons between BOGO and PR, and the share comparisons, carry , with the equality at as its own clause, as the corollary itself states.
The development needs piecewise integration of step functions, the maximization of concave quadratics on intervals, and inequalities with square roots. The definitions file BOGOPromo.NoStockpile.Model is self-contained. Contributions of proofs of the milestones, and of auxiliary lemmas computing the retailer's profit on each consumer segmentation, are welcome.
A system of linear inequalities may have either a feasible point or a short witness that no feasible point exists. An algorithm that returns the witness is useful when a solver must explain an infeasibility decision rather than merely announce one. The standard ellipsoid method can test feasibility under suitable geometric bounds, but its ordinary output does not supply the type of algebraic certificate considered here. Lamperski, Freund, and Todd's oblivious ellipsoid algorithm (OEA) is designed to return the appropriate kind of object without knowing in advance whether the system is feasible. Its infeasible-case iteration guarantee is Theorem 7.1 of the source preprint.
The source combines a constraint-based ellipsoid representation with continually updated certificates of lower bounds. This mission targets its infeasible case. The feasible-case result, Theorem 7.2, uses a different volume estimate and lies outside this mission.
Let have columns , and let . The primal system (P) seeks such that . A type-L certificate of infeasibility is a vector satisfying , , and . Such a vector rules out a feasible : multiplying the inequalities by its nonnegative components would give , a contradiction.
The paper assumes throughout that the nonnegative cone generated by the columns of equals , and that each column has Euclidean norm one. A certified lower-bound pair consists of and a matrix whose columns certify lower bounds for the individual constraints: , entrywise, and . These are the initial data, alongside positive weights , for OEA. The mission starts at , the all-ones vector.
OEA represents an ellipsoid by the same lower-bound vector and a positive weight vector. With , its Burrell–Todd ellipsoid is
Its centre is , its scale is , and is its radius in the direction of . These quantities determine a new certified lower bound . The condition measure is the absolute value of the greatest possible minimum slack, . On an infeasible system it measures a violation that must be present at every point. The paper defines a potential from the normalized weights and to state the quantitative progress made by an update. These definitions and their source locations appear in Sections 3–7 of the preprint.
For every certified pair and every permitted run of Algorithm 4 starting from , if (P) is infeasible, OEA returns a type-L certificate. The source's displayed bound is
The formal goal records all possible choices left open by the algorithm and bounds the number of completed updates, the quantity called in the proof of Theorem 7.1. It also asserts that every reached state has a next admissible outcome and that every terminal outcome on an infeasible input is a valid type-L certificate.
The milestone list contains the paper's certificate results, the exact form of its weight update, the slab-radius bound, and the potential decrease. In particular, Lemma 7.1 states under its specified update relation. Each milestone retains the paper's own index and hypotheses.
The target strengthens an infeasibility decision with a checkable vector whose entries can be substituted directly into the original inequalities. Its finite bound is expressed using the supplied certified lower bounds and the problem's condition measure, so it quantifies how the algorithm behaves on a particular input rather than only asserting eventual termination. The published paper proves this result; the open work here is a machine-checked development of its definitions, supporting theorems, and run-level guarantee.
The development would also provide reusable finite-dimensional matrix and certificate interfaces. In particular, certified lower bounds and the conversion of a strengthened bound into a type-L witness can be used outside this algorithm. The potential and update relations remain specific to the paper's parameterization.
The main obstacle is maintaining the link between an ellipsoid update and a valid algebraic certificate. A small slab radius alone does not describe a certificate, while an algebraic lower bound alone does not control the number of updates. The algorithm can also stop at several different tests, and Procedure 2 permits choices of indices and positive step sizes. A convergence statement about an arbitrary sequence of weights satisfying a convenient update inequality would leave these algorithmic obligations unresolved.
The representation uses Fin n and Fin m for the paper's finite index sets, real matrices for and , and real-valued functions for vectors. The standing conic-spanning and unit-column conditions are explicit in every theorem. The norm in the bound is the Euclidean norm, written as a square root of a sum of squares because Lean's plain finite function space carries a sup norm. The maximin slack is represented by a real supremum, whose boundedness and attainment follow from the standing assumption; the formal statements do not assume those consequences separately.
Algorithm 4, Procedure 2, and Procedure 3 are relations over states and outcomes. The relations retain the order of each test, the normalization of at Step 3, the replacement of one column of at Steps 5–8, and all allowed choices. A completed iteration means a pass that reaches Step 12. The paper's printed wording counts an eventual stopping pass, while its proof bounds completed updates . A first-pass stop can occur with a negative value of the printed logarithmic expression, so the formal bound applies to reached states with and the first-pass case is covered by the outcome clauses. This is the interpretation used by the proof, not a new assumption on the input.
The definitions use Lean's total matrix inverse, square root, real power, logarithm, and supremum. Positive weights and positive scale guard the ellipsoid formulas in the results that use them; the algorithm tests the scale before using the radius. Needed infrastructure includes finite matrix identities, positivity of , certified lower-bound algebra, and the inequalities underlying the potential bound. Contributions that prove the listed statements or their faithful intermediate lemmas are within scope. The goal must remain about actual OEA runs; assuming its potential decrease as a property of an arbitrary input sequence would trivialize the target.
Loss aversion, the tendency to weigh a loss more heavily than a gain of the same size, is the central ingredient of reference-dependent preferences. Measured degrees of loss aversion vary widely across experiments and markets. One explanation is that the reference point is not fixed. People form it partly from their own expectations about what they will choose, and partly from an external benchmark. He and Strub (SSRN 3318295; Operations Research, 2022, doi:10.1287/opre.2022.2309) ask how this endogenization changes the loss aversion an outside observer would infer from portfolio choices in a complete market.
The relevant models have a short history. Kőszegi and Rabin (QJE 2006; AER 2007) introduced personal equilibrium: a plan that remains optimal when it serves as its own reference point. De Giorgi and Post (Management Science 2011) introduced a state-dependent version together with a partially endogenous variant, in which deviating from an exogenous benchmark carries a mental cost. They applied it to a choice among four strategies. He and Strub solve the partially endogenous model for a general portfolio problem.
An agent with initial wealth buys a prospect, a nonnegative random variable on a probability space . The market is complete with pricing kernel , integrable, so costs . The affordable prospects form .
Given a reference point (itself a prospect), the agent values by
Here is the weight of gain-loss utility and is the intrinsic degree of loss aversion. The utility satisfies Assumption 1: it is strictly increasing, strictly concave and on , with , the Inada conditions, and integrability of and for every . Reference points satisfy , and an expectation is whenever .
With an exogenous reference point , problem (4) maximizes over . Its optimum is denoted . A threshold , given by an explicit formula (6) in terms of and of , marks where stops depending on .
A mental cost , with strictly decreasing and continuous, is charged for choosing . An agent who tolerates cost at most chooses from . A partially endogenous PE is an with for all . The partially endogenous PPE maximizes among these.
Let and . Then
Here is the unique solution of . It is strictly decreasing and continuous, with limits as and as . In each case the partially endogenous PPE exists and is unique up to almost sure equality.
Theorem 3 says that partial endogenization is observationally a reduction of loss aversion. An agent with intrinsic degree and mental-cost tolerance chooses exactly what a standard agent with exogenous reference point and the lower degree would choose. The exhibited degree interpolates monotonically between the intrinsic level (capped at ) and , so empirical estimates of loss aversion confound the intrinsic parameter with the flexibility of the reference point. Theorem 2 is the other extreme: with a fully endogenous reference point and state-dependent evaluation, loss aversion has no effect at all.
The results are proved in the paper; none of them has a machine-checked proof. The mission adds a formal model of reference-dependent preferences in a complete market, with the paper's convention for expectations and utilities with . It also provides formal versions of the exogenous-reference optimum, the personal-equilibrium notions of Kőszegi–Rabin and De Giorgi–Post, and Theorem 3 itself. Three printed slips are corrected along the way: the second limit of Theorem 3 (iii), the constant in the rewrite of (18), and the budget condition in Theorem 2.
Given its inputs, the proof of Theorem 3 is short: a Lagrangian rewrite, the intermediate value theorem and a duality step. The inputs carry the weight. Theorem 1 is an existence and uniqueness result for an infinite-dimensional concave problem whose objective is not differentiable where . The optimal multiplier is defined implicitly, through continuity and monotone limits of a budget map. Proposition 1 needs essential suprema and infima that can be or . Continuity of needs dominated convergence under Assumption 1. Strict monotonicity uses Proposition 1's injectivity, and it fails to be strict at .
A first idea is to maximize directly over . This identifies the PPE only after the reduction (10) ⇔ (16) is proved, and that reduction uses through .
Everything is defined in the namespace EndoRefLA.PartialPPE, in one definitions file. Conventions:
is the optimum of (4), not formula (5), and the PPE is the De Giorgi–Post equilibrium object, not the maximizer of (16). Defining either one by the formula that a milestone proves would make the goal tautological.
A complete development needs the following, all reusable beyond this mission: pointwise maximization of concave integrands under a budget constraint; continuity and monotonicity of budget maps in a Lagrange multiplier; and properties of under the Inada conditions. Proofs of any milestone are welcome. The paper's other two models (§3.2–§3.3) are outside this mission.
A stochastic game (Shapley, 1953) is a dynamic game in which the players' actions influence the evolution of a state variable. Whether every multiplayer stochastic game admits an -equilibrium for every is open even for finitely many states and the long-run average payoff; it is open as well for the general class in which each player's payoff is an arbitrary bounded Borel-measurable function of the infinite play, introduced by Blackwell (1969). This class contains the discounted and long-run average payoffs and the winning conditions of verification (Büchi, parity, Müller).
Flesch and Solan (arXiv:2208.12096; Mathematics of Operations Research, 2024) prove a weaker, unconditional statement: every such game has a subgame that admits an -equilibrium. Their tool is the Martin function, a real-valued function on histories which reduces playing well in the stochastic game to playing well in a one-shot game at each history.
Timeline.
A stochastic game consists of
A history of stage is a finite prefix with positive transition probabilities; is the set of histories and the final state of . A behavior strategy assigns a mixed action to every history. A profile and a history determine a probability measure on runs that continue . Player 's payoff in the subgame is , and the minmax value there is
A profile is an -equilibrium in if no player gains more than by a unilateral deviation, measured by . The subgame is -solvable if it has one (Definition 4.8).
A function induces at every the one-shot game , in which player receives ; its minmax value is .
For every stochastic game as above and every ,
The history may depend on and is not required to start in a prescribed initial state.
The result. Theorem 4.9 is the strongest unconditional existence statement known for multiplayer stochastic games with general payoffs. When the payoffs are shift-invariant (long-run average, limsup, parity) the solvable subgame yields an initial state with an -equilibrium (Corollary 4.10). This recovers the results of Thuijsman and Vrieze (1991) and Vieille (2000c) for the long-run average payoff. Theorem 4.4 along the way answers a question of Simon (2016): no three-player zero-sum-on-every-play game has all minmax values strictly positive.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formalization produces:
Kernel.traj;The first idea, to play the profile of Theorem 4.4 everywhere, fails: keeps every player above the minmax value, but it is not an equilibrium, because a player may prefer some actions in the support of its own mixed action or may steer the play to histories where its own minmax value is high. Handling the first problem needs a compact set of runs on which payoffs are almost constant and a way to identify who left it. That second ingredient is the blame function of Alon, Gunby, He, Shmaya and Solan (2022), which is not available on the platform. Handling the second needs the fictitious hitting counts of (8)–(10) and a careful choice of punishment thresholds. Theorem 3.1 itself is not proved in the paper: it rests on Martin's (1998) determinacy of Blackwell games, on the multiplayer extension of Ashkenazi-Golan et al. (2022a, Theorem 3.6 and Claim 3.5, with the modification of footnote 3), and on the countable-state method of Maitra and Sudderth (1998).
Fintype with decidable equality and are nonempty. States form a nonempty Countable type, and action sets are nonempty Fintypes, the same in every state. The transition is p : S → (∀ i, A i) → PMF S.Feasible.playMeasure G σ n h is Kernel.traj of the one-stage kernel (independent mixed actions, then ) started at . Its runs begin with , so ∫ f i ∂(playMeasure G σ n h) is .⨅/⨆; they are the paper's values because payoffs and Martin functions are bounded.AGT.IsMixedNash.Kernel.traj (conditioning on the first coordinates), Lévy's upward and zero-one laws (the platform's FamousTheorems.levy_upward_theorem is Proved), and existence of Nash equilibria in finite games (AGT.nash_existence, Proved). It also needs regularity of probability measures on Polish spaces, and either a proof of Theorem 3.1 or the blame-function result of Alon et al. Contributions to any of these, and proofs of the milestones independently of one another, are welcome.In many services the customer, not the provider, decides how long to stay: a gym session, a car-wash bay, an electric-vehicle charger, a call to a help line, a slot on a shared computing resource. Such services are called discretionary. Their congestion depends on how many customers join and on how long each of them stays. Providers manage them with per-use fees, with price rates per unit of time, and with time limits, caps on the time any one customer may spend in service. Time limits are common in practice (charging stations, library computers, public parking), and the operations literature on discretionary services (Hopp, Iravani and Yuen 2007; Tong and Rajagopalan 2014; Debo and Li 2020) studies how such systems should be priced and operated.
Feldman and Segev (SSRN 3424317) ask whether a time limit is merely convenient or actually optimal. Their answer for a single-server queue is that a revenue-maximising provider who may use any incentive-compatible price and time schedule chooses to impose a time limit when congestion is high, and that this mechanism attains the first-best social welfare.
Service needs arise as a Poisson process of rate at a single server that serves in first-come-first-served order. A customer's type is her ideal time in service, uniformly distributed on with . Time in service is worth to a customer of type . Customers pay a waiting cost per unit of expected waiting time.
An allocation consists of a measurable admitted set and a measurable time function with on . Its expected waiting time is the Pollaczek–Khinchine mean wait of the resulting M/G/1 queue, which for uniform types reads
and the allocation is feasible when the queue is stable, . Its social welfare is
and an allocation is first-best if it is feasible and maximises among all feasible allocations.
A direct mechanism adds a non-negative price for . It is incentive compatible (IC) if for all , and individually rational (IR) if on . Its revenue is .
The thresholds of the paper are
For each congestion regime, take the first-best allocation of Theorem 1:
and the full-extraction price . Then is first-best, is a feasible IC and IR mechanism with , a non-admitted type gains nothing by claiming an admitted type, no IC and IR mechanism earns more revenue, and
The result. Theorem 1 shows that the welfare-optimal schedule in a discretionary M/G/1 service is an admission threshold followed, at high congestion, by a time limit. The reason is that the waiting time depends on the second moment of service times, and a time limit is the cheapest way to cut that second moment for a given total service. Theorem 8 then shows that a monopolist with unrestricted pricing loses nothing relative to the planner: the optimal mechanism reproduces the first best, time limit included, and extracts all surplus. Together they justify time limits as an optimal instrument rather than a heuristic, and they supply the benchmark () against which the paper's simpler schemes, per-use fees and price rates with or without limits, are compared in its Theorem 10.
The formalization. The results are proved in the paper, partly by "standard arguments" (the reduction to admitted intervals) and by first-order conditions whose global optimality is argued informally; two displays in the proof of Theorem 1 are misprinted. No part of the paper has been machine-checked, and the platform has no development of discretionary services, endogenous service times or mechanism design with congestion. A complete formal proof would verify the case analysis of Theorem 1, including uniqueness in its first two cases, and the full-extraction argument, which the paper does not check for the non-negativity of prices.
The hard step is Theorem 1. The first-best program is a non-convex optimisation over measurable sets and functions, in which welfare involves the ratio of the second moment to the slack . The natural approach, pointwise optimisation of the integrand, fails because every customer's time enters every other customer's waiting cost through two integrals. The paper's route goes through a reduction to intervals, a water-filling sub-problem and a three-parameter calculus problem with implicit first-order conditions, and a formal proof must justify each reduction globally, not only at stationary points. Theorem 8 on top of Theorem 1 is short, but it needs the first-best time function to leave , which follows from the optimality of the lower threshold.
Everything is real-valued, in the namespace ServTimeLimit.OptMech. Parameters are a structure with fields Lam (), c and θbar (), and every statement assumes ; is made explicit. Allocations are pairs of a set Φ : Set ℝ and a function t : ℝ → ℝ of which only the values on matter; integrals are Lebesgue integrals over .
No queueing process is modelled: the waiting time is defined by the Pollaczek–Khinchine display above, which is the paper's own formula with . The program's condition "" is read as stability, , and is part of feasibility. Welfare integrates over the admitted set, as in the proof of Theorem 1 and the program of Theorem 8; §4's display over would charge the waiting cost to customers who are not admitted. IC is stated on , as printed, and the goal adds the proof's check for excluded types. Prices must be measurable, integrable and non-negative. Uniqueness in Theorem 1 is of the threshold (and time limit) within the displayed shape; for the first best is not unique and no uniqueness is stated. The milestone for adds the stability range at .
The goal is not Theorem 8 for an arbitrary first-best allocation: that version would drop "according to Theorem 1" and reduce to milestones 7 and 8. The goal names Theorem 1's admitted sets and time functions in each regime, so a proof must establish the first-best characterisation.
A complete development needs Lebesgue integrals over intervals, a water-filling (or convexity) argument for sub-problem (4), and one-variable calculus for the first-order conditions. The sub-problem lemma, minimising under a mean and a pointwise upper constraint, is reusable beyond this paper. Contributions of any of the milestones, or of intermediate lemmas such as the reduction to admitted intervals, are welcome.
Many decision problems have set-valued outcomes rather than single numbers. Typical cases are a portfolio whose risk is a set of capital vectors, a vector optimization problem whose image is upper-bounded by an ordering cone, or a robust model whose value is the set of all achievable outcomes. Set optimization minimizes such a map . The first difficulty is how to compare two sets. In the complete lattice approach of Heyde and Löhne (2011) and of the survey by Hamel, Heyde, Löhne, Rudloff and Schrage (2015), the values are taken in a complete lattice of sets, so that infima exist. A solution is then a set of arguments that attains the infimum and consists of minimal points.
Crespi, Hamel, Rocca and Schrage (arXiv:1812.03300v1, published in Mathematics of Operations Research, 2021) generate both the set relation and the lattice from an arbitrary family of monotone scalar functions on a preordered set. The construction needs no linear structure on the image space. It covers vector orders, scalarizations by linear functionals and orders given by indicator functions. On top of it they define approximate solutions with tolerance , and prove a Weierstrass-type existence theorem: compactness of approximate minimizer sets yields exact solutions, and the approximate sets converge to the exact ones in the Hausdorff sense.
Let be a preordered set and . Let be a family of monotone functions , so that implies .
For a map on a non-empty set , the problem is
and for . For and , let if and , with .
In §4, is a separated (Hausdorff) topological linear space over .
Let and , and suppose is compact for all . Then is non-empty and compact, and for every neighbourhood of and all sufficiently small
If, additionally, every is lower semicontinuous, then is non-empty and a -solution of (P).
The theorem is the existence result of the paper's framework. It turns a compactness condition on approximate minimizer sets into an exact solution in the sense of Definition 3.7: a set of arguments that attains the lattice infimum and consists of minimizers. The Hausdorff convergence statement is a well-posedness result: approximate minimizers computed with a tolerance lie close to exact -minimizers when is small. The framework applies to vector optimization with a cone order, to set-valued risk measures and to orders given by indicator functions, all as instances of the same .
The results are proved in the paper. None of them is formalized on the platform or in Mathlib, which has neither set relations nor lattice-valued solution concepts. This mission produces machine-checked statements of the lattice of Ψ-closed sets, inf-stability, approximate solution concepts with their conventions, and the existence theorem. Later set optimization missions can build on these definitions.
The individual arguments are short. The work lies in the extended-real bookkeeping and in using the lattice structure correctly:
EReal, and the empty infimum is . carries [Preorder Z], and is a Set (Z → EReal) with every member monotone. A map into is f : X → Set Z together with the hypothesis that every value is Ψ-closed. The lattice structure is therefore Proposition 2.3, not a built-in instance.The development needs extended-real infima, lower semicontinuity into EReal, and Cantor's intersection theorem for nested compact sets in Hausdorff spaces, all available in Mathlib. The definitions of inf-extension, Ψ-hull, set relation and approximate solutions are reusable beyond this paper. Proofs of any milestone, and of alternative routes to the goal, are welcome.
Hiring decisions often rest on a recommendation from someone who knows the candidate: a thesis adviser, a former supervisor, a colleague. Referrals are a common channel of labor market matching, and their value depends on whether the recommender can be trusted. An adviser who cares about his candidate has a reason to overstate the candidate's quality, and the main check on this is the adviser's reputation: a recommendation that turns out badly costs the adviser future credibility.
Câmara, Jia and Raffiee (2023) study this trade-off in a one-period recommendation game in which reputation enters as a state variable, and ask a question about matching between advisers and firms: which firms are more likely to hire the candidates of strong-reputation advisers? Their answer is that it depends on the shape of the firm's outside market, not only on its average quality. This mission formalizes that result, together with the equilibrium characterization it rests on.
A focal candidate has skill , , high with probability ; the average skill is . An adviser with reputation privately observes and a personal bias , distributed on with a continuous CDF of full support. He sends a message (recommend or not). A firm privately observes the value of an outside candidate, distributed on with a continuously differentiable CDF , density and full support, and hires either the focal candidate (payoff equal to the candidate's skill) or the outside one (payoff ).
If the adviser recommends a high-skilled candidate who is hired, his reputation rises to ; if he recommends a low-skilled candidate who is hired, it falls to , with ; otherwise it stays at . He receives the reputation payoff of his final reputation, plus if his candidate is hired. The payoff loss from an unsuccessful hire is
and the paper's standing Assumption (A1) is : an adviser with a higher reputation has more to lose. The solution concept is perfect Bayesian equilibrium with two tie-breaks: an indifferent firm hires the focal candidate, and an indifferent adviser does not recommend a low-skilled candidate.
In equilibrium a low-skilled adviser lies (recommends) exactly when his bias exceeds a threshold , and the firm's belief after a recommendation is
The largest possible benefit from lying is . A market is top-heavy if is strictly increasing, and bottom-heavy if is strictly decreasing.
Let be the ex-ante probability that the firm hires the focal candidate in an equilibrium at reputation . For all and all equilibria at and :
and both inequalities are strict when and . Part (iii) of the proposition, assortative matching, is (i)–(ii) restated.
The result separates two notions of a firm's "strength" that are often conflated: the average quality of its outside options and the shape of their distribution. Two firms with the same average outside candidate can respond in opposite ways to an adviser's reputation. Firms with access to many strong outside candidates (top-heavy) favor candidates of high-reputation advisers; firms whose outside options are concentrated at the bottom favor candidates of low-reputation advisers. The paper uses this to explain assortative matching between strong advisers and strong firms without assuming it, and connects it to the persuasion literature, where the convexity of the sender's payoff in the receiver's posterior determines how much information the sender wants to reveal (Kamenica and Gentzkow 2011).
All results here are proved in the paper, in Appendix A. None of them has a machine-checked proof. A formal development makes precise several points the prose leaves implicit: what "increasing" means where the adviser's behavior stops responding to reputation, that the comparison holds for every equilibrium and not only for a constructed profile, and which regularity of the shape definitions need.
The obvious argument treats the threshold as a known function of and differentiates. Two steps break this. First, is defined implicitly by a fixed-point condition that couples the adviser's incentive with the firm's Bayesian belief, which itself depends on ; existence and uniqueness of the equilibrium, and the threshold form of every equilibrium (not merely of one candidate profile), have to be established before any comparative static makes sense. Second, the hiring probability is not monotone in for every : a higher threshold makes a recommendation more persuasive but rarer, and the two effects cancel exactly for linear . The sign is decided only by the curvature of , which enters through its density, so the definition of top- and bottom-heavy markets has to be related to convexity of the CDF on the support. A further subtlety is that the hiring probability is constant for reputations at which the adviser never lies, so the monotonicity is strict only from reputations with .
All quantities are real numbers. The laws of the bias and of the outside option are probability measures , on with mass one on , no atoms and strictly increasing CDFs on ; and are their CDFs, is on (not on all of , which would force and rule out top-heavy markets), and is the derivative of on . The functions , , are differentiable on , and (A1) is stated as there.
Strategies are pure and Boolean-valued: for the adviser and for the firm, as in the paper's footnotes 15–16. They are required to be measurable, which the paper leaves implicit; message and hiring probabilities are measures of the corresponding sets. Best responses are imposed for every bias in and every outside value in , so uniqueness in Proposition 1 is on those supports. Beliefs lie in and follow Bayes' rule after every message sent with positive probability. The adviser's expected utilities are eqs. (6)–(8), with in (7); the sentence leading into (7) misprints it as .
"Increasing in " in Propositions 2 and 3 is formalized as weakly monotone on together with strict monotonicity from every with ; strict monotonicity on all of is false. The goal quantifies over arbitrary equilibrium profiles at both reputations: a statement about the threshold or about a profile the theorem itself constructs would reduce the goal to milestones 1, 5 and 8 and is ruled out. The standing assumptions are satisfiable together with a top-heavy market (for instance on with uniform bias).
The development needs only Mathlib's measure theory (CDFs from measures), one-variable calculus (monotonicity from the sign of a derivative, convexity from a monotone derivative) and slope inequalities for convex functions. The general facts in milestones 7 and 8 are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Proposition 1.
Not formalized here: the second sentence of Proposition 2 (the firm's ex-ante payoff increases in ), Proposition 4 (the low-reputation trap), Propositions 5 and 6, and the extensions of §5.
Many combinatorial optimization problems are linear programs over a polytope with exponentially many facets, and one way to solve them by a polynomial-size linear program is to write the polytope as the projection of a higher-dimensional polytope with few facets. The minimum number of facets needed is the extension complexity of the polytope. It is now understood for most textbook polytopes: flows, matchings (Rothvoß 2017), arborescences, travelling-salesman tours and stable sets (Fiorini et al. 2015). Matroids are a notable exception.
For a matroid , the independence polytope is the convex hull of the characteristic vectors of the independent sets. Rothvoß showed by a counting argument that many matroids have independence polytopes of exponential extension complexity (Math. Program. 2013), so a polynomial bound can only hold for special classes. Regular matroids, those representable over every field, are the natural class: they contain the graphic and cographic matroids, and Seymour's decomposition theorem describes all of them.
Timeline:
A matroid has a finite ground set and a family of independent sets; . For , is its characteristic vector, and
An extended formulation of a set of size is a system , with exactly inequalities such that if and only if some satisfies the system. The extension complexity is the least such . The paper defines as the minimum number of facets of a polytope projecting onto , and on p. 1 it gives the extended-formulation form as an equivalent definition.
A matroid is regular if it is represented over by a totally unimodular matrix : a set is independent exactly when the corresponding columns of are linearly independent. It is binary if it is represented over . It is graphic if it is the cycle matroid of a multigraph (independent sets are forests) and cographic if its dual is graphic. A cycle is a disjoint union of circuits. For binary , the sum has ground set , and its cycles are the sets , with a cycle of , that lie in that ground set. This sum is a 1-, 2- or 3-sum when the two ground sets share zero, one or three elements, under the side conditions of p. 3. In the 3-sum case the shared set is a triangle, a 3-element circuit of both parts. A matroid is 3-connected if it is neither a 1-sum nor a 2-sum.
The constant is not fixed; the exponent is the paper's. Section 8 of the paper sketches an improvement to without proof, so the goal keeps the proved exponent.
The result. Theorem 1 shows that linear optimization over the independent sets of any regular matroid is a linear program of size polynomial in , written down without any algorithm. Regular matroids are the largest classical matroid class for which such a bound was in question, and the bound separates them from general binary matroids. The proof also gives an extended formulation for the circuit dominant of a regular matroid, a separate result that this mission does not include.
Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs a Lean theory of matroid sums (1-, 2- and 3-sums defined through cycle spaces), decompositions of regular matroids along trees, and extended formulations, with explicit bounds on how the size of an extended formulation behaves under products, intersections with hyperplanes and convex hulls of unions. Seymour's decomposition theorem enters only through Theorem 6, which can be taken as a black box while the polyhedral part is formalized.
The obvious induction fails at 3-sums. For 1- and 2-sums, the extension complexities of the parts add (Lemma 3), and an induction gives a polynomial bound. For a 3-sum, the best known symmetric formulation for has size with (p. 4). A constant larger than 1 compounded over a decomposition tree of logarithmic depth only gives a quasi-polynomial bound, and over an unbalanced tree an exponential one. So the parts of a 3-sum have to be treated differently, and the decomposition tree has to be rebalanced into a star whose leaves have at most about half the elements.
The cographic centre is a second obstacle: the formulation of the centre's part is known only when every triangle shared with a leaf is the set of edges at a degree-3 node of the underlying graph, and getting there requires the decomposition tree of Proposition 27.
Matroid α over one ambient type ; the parts of a sum share elements of (the triangle elements) that are not in . Statements that construct decompositions (Theorem 6, Proposition 27, Lemma 4) take infinite, so that fresh elements exist; otherwise "not a 2-sum" could hold for want of room.IsEFOfSize and extensionComplexity (size = number of inequalities, equations free). Every upper bound is the existence of an extended formulation of the stated size, and bounds in terms of the parts quantify over extended formulations of the parts. This rules out the trivializing reading with an infimum that is on sets with no extended formulation.A seller of a good with network externalities (a social app, a telecom plan, a game console) gains from knowing how strongly each consumer's demand depends on the consumption of others. Candogan, Bimpikis and Ozdaglar (Operations Research, 2012) showed that, on a known network, the optimal price vector of a monopolist and the resulting revenue have closed forms built from the matrix . In practice the network is estimated from data and is never known exactly. A seller who commits to prices on the basis of a forecast then faces revenue that moves with the true network .
Baron, Hu and Malekian (SSRN 3561270, 2020; published as a Technical Note in Operations Research, 2022, doi:10.1287/opre.2022.2302) ask how large that movement can be in the worst case, when the forecast error is bounded in spectral norm. Their Theorem 1 gives an exact answer depending on the network only through its largest eigenvalue. This mission formalizes that theorem, read in the SSRN version of 2020-03-25.
There are agents on a network with , and, as for any network without self-loops, . A parameter scales the peer effect, collects the agents' primary values, and is the seller's marginal cost.
The game has two stages. In the first, the seller chooses a price vector . In the second, each agent chooses a quantity , with utility
A consumption equilibrium is a profile in which each maximizes over . The seller's revenue is , and the optimal revenue is its supremum over all prices and their equilibria. Assumption 1 asks for every ; Assumption 2 asks .
The forecast error is measured by the uncertainty set
with the spectral norm. The seller fixes the price that is optimal for the forecast ; consumers then play the equilibrium on the realized , producing revenue . The revenue volatility is the supremum of the relative change over and . Finally, is the largest absolute value of an eigenvalue of .
Under Assumptions 1 and 2, for every with , every admits an interior consumption equilibrium at the seller's ex-ante price, and
The theorem turns a robustness question about an equilibrium of a game into a single spectral quantity. A seller can read off the worst-case relative revenue change from , and , and compare networks by their largest eigenvalue: denser, more central networks are more exposed to estimation error. The paper uses it to compare chains and complete networks (Proposition 3) and as the deterministic benchmark for its stochastic analysis (Theorem 2).
The result is proved on paper; no machine-checked proof exists. A formalization adds three pieces that are absent from the platform: the network pricing game stated as an equilibrium (not as a closed-form demand), the optimality of the price over all of , and the Neumann series for real matrices under .
The obvious argument substitutes Proposition 2's closed form and bounds a difference of resolvents. Two steps resist this. First, the realized network need not satisfy Assumption 1, so the existence, uniqueness and positivity of the equilibrium on must come from the spectral bound alone. Second, the bound is a supremum of a generalized Rayleigh quotient over , which must be related to the spectral norm of through a constrained-optimization argument. Tightness needs the top eigenvector, which is only non-negative in general, so the supremum is generally not attained in the open set .
The game-theoretic layer is not a formality: Proposition 2 asserts optimality over every price vector, including those at which some agents consume nothing.
Agents are Fin n; vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ. The norm is Mathlib's scoped spectral norm (Matrix.Norms.L2Operator). is the supremum of over the real spectrum (used only for symmetric matrices), and is computed from the complex spectrum. Condition (1) is written , equivalent to the printed form when , and avoiding Lean's convention .
Conventions added to the page, each disclosed in the items:
The optimal revenue and the revenue on are defined from the game (suprema over prices and equilibria), never by Proposition 2's closed form; a formalization that substitutes the closed form would make Propositions 1–2 vacuous and reduce the goal to a matrix inequality, and is ruled out.
A complete development needs: potential games with concave potentials on , linear complementarity for diagonally dominant matrices, the Neumann series and Perron–Frobenius for non-negative matrices, the spectral theorem for real symmetric matrices, and a Lagrange multiplier rule for a quadratic constraint. The Neumann series criterion and the norm–radius equality for symmetric matrices are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative decompositions of Part 3.
Classical sample-size calculations for a clinical trial fix a significance level and a power and solve for the number of patients. They do not ask what the trial is for. A value-based design asks instead: given what it costs to recruit patients and what a better adoption decision is worth to the patients treated after the trial, how long should the trial run and how fast should it recruit? Health technology assessment bodies such as NICE already decide adoption on cost-effectiveness grounds, and Bayesian decision-theoretic trial design goes back to the value-of-information literature of the 1990s and 2000s (Claxton & Posnett 1996; Chick, Forster & Pertile 2017).
Alban, Chick and Forster (Management Science 2023) make the two decisions explicit, recruitment duration and recruitment rate , and let the regulatory context decide the population that benefits after the trial. Their asymptotic result, Proposition 5, says that the optimal number of patient pairs grows as the square root of that population, and that the optimal expected net gain per post-trial patient converges to a value that does not depend on the switching costs.
A new technology N is compared with a standard S. A fraction of patients is on N before the trial. Patients are randomised in pairs; recruiting at rate for a time yields pairs. The incremental net monetary benefit of N over S has prior , each pair gives an observation , and . After pairs the posterior mean has predictive law with .
After the trial the decision maker adopts N, adopts S, or keeps the current mix, paying fixed switching costs . Without discounting, the expected net gain of a design with is
where is the cost per patient, the setup cost of recruitment capacity, and switches on rewards to trial patients. Without a trial, . The post-adoption population is either a fixed pool, , or set by a fixed horizon, , with incidence and observation delay . The paper also treats discounting at rate ; the asymptotic results take .
Problem (5) maximises over , where Table EC.1 takes and . With and , the paper distinguishes four cases: I (, fixed pool), II (, fixed horizon), III (, fixed pool), IV (, fixed horizon).
Write , for the standard normal density, for the standard normal linear loss, and
Assume and . For every selection of optimal designs, with :
with (Case I) or (Case IV). In Case II the denominator is , and in Case III (corrected, see below) it is . The goal also asserts that optimal designs exist once the population is large.
The closed form (8) of through ; existence of an optimal design (Proposition 1); the reductions to one decision variable (Propositions 2–4); and the four case lemmas EC.1–EC.4 of Appendix C.4, which together give Proposition 5. Lemma EC.4 adds the finer statement that in Case IV both and grow like .
The result turns an optimisation without a closed-form solution into a rule of thumb: for a large population, the optimal trial enrols about patients. The authors show in their ProFHER application that the approximation is accurate at realistic sizes. It also explains two qualitative facts, that fixed-pool and fixed-horizon contexts reach the same value per patient, and that switching costs become irrelevant at scale.
The paper proves these results with asymptotic arguments that are sketched in places ("by rearranging and some additional asymptotic approximations"). A formal proof makes every limit exchange explicit. The formalization also corrects a misprint: the Case III constant in Proposition 5 and the constant in (EC.4) are printed without the setup-cost term , and the proof's own optimality condition shows that it belongs there. None of these results has been machine-checked before; the platform has the normal linear loss and nothing on clinical-trial design.
The objective is not concave in , has a jump where the trial stops running, and its optimiser has no closed form. The square-root law concerns an arbitrary optimiser as the population grows. So it is not enough to differentiate an asymptotic approximation of and solve the first-order condition. One must show that every optimiser escapes every bounded set, that the exact first-order condition holds there, and that the error terms of and of the indifference points and vanish at the right rates. In Case IV two decision variables diverge at different rates, and the fixed horizon couples the trial length to the post-trial population.
All quantities are real. A design is a pair . The post-adoption term of is a Bochner integral against gaussianReal µ0 σZ², and is the published InventoryControl.normalLoss. is defined by the expectation (7) and (9), never by the closed form (8), which is a milestone. Optimality is IsOptOn f S x: and on .
Decision sets follow §3.6.1: in Cases I and II, with ; in Case III, with ; in Case IV, both are free. Under a fixed horizon, is added, because beyond it , outside the model (§2.4.1 requires ). The finite box statements use , , and a fixed pool has , as in Table EC.1. Other added hypotheses: the standing sign conditions of §2 and Table EC.1 (; ; ; ), (used in the proof of Proposition 1), and .
Limits are asserted for every selection of optimisers. A separate conjunct asserts that optimisers exist for large populations, so the statement cannot be satisfied vacuously by an empty set of optimisers. It is not about a stationary point of an approximation, and is never replaced by a formula.
Two printed slips are corrected and labelled. In Proposition 5, Case III has constant , and (EC.4) has the factor in its denominator. Both follow from the cost of pairs at fixed , which is ; at the corrected constant matches a numerical optimum to four digits, the printed one does not. The branch of Lemma EC.4, Proposition 6 (discounting) and the comparative statics of §3.5 are not formalized.
A complete development needs Gaussian expectations of piecewise-linear functions, semicontinuity arguments on a box with a jump, and asymptotic analysis of argmax sets. The Gaussian-loss identities are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the case lemmas.
The monotone complementarity problem (MCP) asks, for a continuous monotone map on the positive orthant, for a pair with , , and for every . It contains linear programming, convex quadratic programming, the monotone linear complementarity problem and the Karush–Kuhn–Tucker conditions of smooth convex programs. Interior-point methods solve it in polynomially many Newton-type steps when a strictly positive, well-centered starting point is known, but in general no such point is known, and the problem may be infeasible or feasible without any positive feasible point.
Andersen and Ye (Mathematical Programming 84, 1999) extended the homogeneous self-dual embedding of linear programming to the nonlinear MCP: one embeds the problem into a homogeneous problem that always has a trivial interior starting point, solves it by a path-following method, and reads off either a solution or a certificate of infeasibility. Section 8.4 of Ye, Interior Point Algorithms: Theory and Analysis (Wiley 1997, doi:10.1002/9781118032701) presents this construction, the convexity property of the residual set it rests on, and the analysis of one step of the algorithm. This mission formalizes that section.
Vectors are compared componentwise; is the all-ones vector, , , the Euclidean norm and the open orthant. A map is monotone if for all ; denotes its Jacobian.
The residual set is , and for the slice .
The homogeneous map on , with points written , is
The homogeneous model (HMCP) asks for with minimizing .
A map on is scaled Lipschitz with a monotone increasing if
The algorithm works in with and . At an iterate let and . The direction solves
and for a step size the new iterate is and .
Assume is scaled Lipschitz with , and let
If and , then and
The goal remains true when is only assumed differentiable on and scaled Lipschitz; this variant is posed beside the goal (see Formalization scope).
Theorem 8.29 is the one-step invariant behind the iteration bound of the homogeneous algorithm: combined with Lemma 8.28 it shows that the infeasibility residual and the complementarity gap shrink by the same factor per step while the iterates stay in a fixed neighborhood of the central path. Together with Theorem 8.25 (v)–(vi), which identifies solutions and infeasibility certificates of the MCP from maximal complementary solutions of the homogeneous model, this yields an algorithm that needs no feasible starting point and detects infeasibility. The convexity of (Theorem 8.23) is the structural fact that makes the homotopy path of the homogeneous model well defined.
These results are proved in the book (with Theorem 8.19, which Theorem 8.23 uses, left as an exercise). None of them is formalized on the platform: the existing Andersen–Ye material covers only the linear complementarity case, as a set-valued operator, and no statement about scaled Lipschitz maps or the nonlinear homogeneous map exists. A completed development gives a machine-checked analysis of an interior-point step for a nonlinear problem, with every constant explicit.
The algebra of Lemmas 8.27 and 8.28 depends on the identities and , which require differentiating a map defined through ; working with as a Fréchet derivative rather than a hand-written block matrix is part of the work. In Theorem 8.29 the nonlinearity enters only through the scaled Lipschitz bound, which applies only when , so the step must first be shown to stay well inside the orthant before the neighborhood estimate can be closed; the norms involved (, , and the scaled norms , ) must be chained in the right order. Theorem 8.23 is of a different kind: its proof passes through the homeomorphism of Theorem 8.19, whose proof the book leaves as an exercise, and a compactness argument along a homotopy.
Two points in the printed text need care. The block matrix (8.24) displayed for has a spurious transpose in its lower-left block; with the printed matrix Lemma 8.24 would fail for nonsymmetric , and the statements here use the true Jacobian. The printed proof of Theorem 8.25 (iii) (the scaled Lipschitz constant of from that of ) establishes the bound with , not the stated , and only for ; that part is not in this mission, and Theorem 8.29 assumes the scaled Lipschitz property of directly, as the book does.
Vectors are Fin N → ℝ, a point of is z : Fin (n+1) → ℝ with Fin.init z and z (Fin.last n) , and every Jacobian is Mathlib's fderiv. The standing assumptions of §8.4 are explicit hypotheses of every theorem: continuous and monotone on the open orthant , and differentiable there wherever or appears (the section assumes this silently). In the scaled Lipschitz condition, "monotone increasing" is read as nondecreasing on and ranges over . The direction is any solution of (8.42)–(8.43). The new dual iterate is defined by the first line of (8.47); its closed form is a conclusion. The book writes no in the statements of this mission: , , and are the book's explicit constants. is a total function in Lean (division by returns ), but every statement evaluates it and its derivative only at .
A trivializing formalization is excluded: the scaled Lipschitz hypothesis is not vacuous (it holds, for instance, for with any admissible ), the direction is not assumed to have any property beyond (8.42)–(8.43), and the monotonicity of and the identities (8.41) are proved milestones, not hypotheses of the goal.
Beyond the paper. One variant is posed: central_step_strong (strengthened) drops the continuity and monotonicity of from Theorem 8.29, because the scaled Lipschitz condition already forces , the only use the proof makes of monotonicity.
The development needs Fréchet derivatives of compositions with , finite-dimensional norm inequalities, and, for Theorem 8.23, invariance of domain or a direct proof of Theorem 8.19. The definitions (monotone maps on the orthant, the scaled Lipschitz condition, the homogeneous map) are reusable for the remaining parts of Theorems 8.25 and 8.26. Contributions of a proof of Theorem 8.19, and of the faithful Theorem 8.25 (iii), are welcome.