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?
Much of the trading in options, bonds and other over-the-counter products does not go through a limit order book. A client approaches several dealers, each dealer quotes a price schedule (the total price for each trade size), and the client splits the order among them. The dealers face two costs. The first is adverse selection: clients who trade large amounts tend to hold information about the asset's payoff. The second is inventory: a position that is held is risky.
Earlier models of competition in price schedules (Glosten 1989 for the monopolist; Biais, Martimort and Rochet 2000, 2013; Back and Baruch 2013) mostly use payoffs with compact support, or they impose conditions that rule out normal distributions. Herdegen, Muhle-Karbe and Stebegg (arXiv:2107.12094) study clients whose signals and inventories have log-concave densities on the whole real line, and dealers with quadratic inventory costs. They characterize the symmetric Nash equilibrium of competing dealers completely: its marginal prices are the unique solution of a nonlinear first-order ODE that has no boundary conditions.
The client receives a signal about the payoff of a risky asset, where is mean zero and independent. The client holds an initial inventory and has inventory cost . and are independent and have positive densities and , and both are log-concave, i.e. and are concave (Assumption 2.1). Only the effective type matters. Its density is , its distribution function is , its survival function is , and the payoff it predicts is the conditional mean .
There are dealers. Dealer quotes a price schedule : a continuous function with that is twice continuously differentiable away from . A client of type chooses trades to maximize
A schedule is admissible if, when all dealers quote , this problem has a unique solution for every . Schedules are compatible if the problem with has a solution for some . Dealer 1 has inventory cost , and given the client's trade her goal functional is
which is when the negative part is not integrable. is a symmetric Nash equilibrium if it is admissible and no that keeps compatible gives dealer 1 a larger goal functional.
The candidate marginal price solves the ODE (3.8). For and respectively,
where and . Assumption 3.7 asks that . Assumption 3.10 asks that on and on .
Under the standing assumptions and Assumptions 2.1, 3.7 and 3.10, let be the increasing, continuously differentiable solution of (3.8) on . Then for every ,
The statement contains both existence (the integral of is an equilibrium) and uniqueness (there is no other).
The result gives a closed description of equilibrium liquidity provision by competing dealers with unbounded types: equilibrium prices exist, are unique, and are convex, and their marginal prices are computable from a scalar ODE. It covers normal signals and inventories (Remark 3.12), which earlier conditions excluded. Lemma 3.6 and Theorem 3.8 already show that there is at most one symmetric equilibrium. The verification half shows that the first-order ODE identifies a global optimum. That is not automatic here, because the dealers' optimization problems are not convex.
The paper's results are proved on paper and none of them is machine-checked. A formalization would check the verification argument of pp. 27–30, which hinges on Assumption 3.10. It would also produce a reusable library of facts about log-concave densities on (Propositions D.1–D.3), an integration-by-parts lemma, and an existence theorem for ODEs between lower and upper solutions (Proposition C.4) that Mathlib does not yet have.
There are two difficulties.
All objects live in the namespace LiqProvision.Oligopoly, in one definition file:
dens, cdf and surv are the explicit convolution integral for and its distribution and survival functions.condMean is the Bayes ratio . The noise is dropped because .Fin K, and dealer 1 is index .EReal, with when the negative part is not integrable (footnote 5).Corrected misprints:
Trivializing formalizations are excluded:
A sorry-free check shows that the hypotheses are satisfiable: Gaussian with , , meets the standing assumptions and Assumption 2.1, and is admissible.
Contributions are welcome at every level:
Not formalized:
A majority attack lets a miner create blocks on a private branch of a permissionless blockchain and later publish that branch as the accepted transaction history. The familiar motive is a private benefit from changing the record, such as a double-spend. Gans and Halaburda show that this motive need not be present: when transactions compete for limited block space, a slower private branch can collect more fees per block. The extra mining revenue can outweigh the attacker's cost even when the private benefit is zero. Their analysis therefore makes the fee market part of the security calculation, alongside the hash power needed to overtake the public branch. This mission formalizes the Proof of Work result in Proposition 1 of the pinned preprint, pp. 13–14.
The result matters for miners deciding whether to continue honestly on the incumbent chain and for designers assessing what a given distribution of mining power actually guarantees. An active miner need not already control half of the incumbent hash power to face a profitable attack opportunity. That is the specific vulnerability established here; the model does not claim that every miner attacks or that every attack succeeds under every network rule.
Let be miner 's hash power before an attack and the incumbent total. If the intended time between blocks is , the puzzle difficulty is . A miner deploying hash power earns an expected blocks per unit of clock time. With per-block reward and mining cost per unit time, its flow profit is
For an honest block, : is the value of newly issued tokens and the expected transaction fees. A miner is active when its incumbent flow profit is nonnegative, the participation condition (1) on p. 5. The attacking branch pays per block. The token reward is the same on both branches, as §4.3 states; their expected fees can differ.
If a miner held before attacking, the paper's minimum attack-power bound is (p. 6). Let be an attained maximizer of attack-chain flow profit over nonnegative hash powers. Equation (3), p. 8, evaluates the attack at and defines its net cost over expected duration :
A miner with private attack benefit prefers not to attack only if . A no-attack equilibrium, for this mission, means that every active miner satisfies this incentive condition. These definitions follow the paper's benchmark, attack description and incentive condition in §§2–4, pp. 4–8.
In the fee model, every available transaction has unit size and a nonnegative fee. A block takes the highest fees among its available transactions. Write for the expected block fee when independent fees have a common law . For congested honest blocks and a slower attack branch, the first central target is Lemma 2, pp. 12–13:
The paper expresses congestion as , with the mean transaction arrival rate, and obtains more arrivals between attack-chain blocks when attack hash power is below . The natural counts state that comparison directly. The same law on both branches represents users leaving their fee submissions unchanged.
The economic target is Lemma 1, p. 11. When the attack-chain reward per block is greater, there is a threshold strictly below half of above which the net attack cost is negative:
The goal, Proposition 1, pp. 13–14, combines these claims. For the finite miner population, there is such that any active miner with violates the no-attack incentive condition even at . The threshold is chosen before the incumbent allocation varies. Thus it applies to genuinely sub-majority values of , including an interval below .
Strictly higher fees on the private branch make its reward per block greater even though the issued-token reward remains . Lemma 1 then identifies incumbent miners whose forgone honest profit is less than their expected attack profit. Proposition 1 states the resulting failure of the no-attack equilibrium condition. This gives a precise economic implication of congestion in the model: hash-power shares alone do not determine whether an active miner has an incentive to preserve the public chain.
The paper proves these claims informally, while the proposed Lean theorems remain open proof targets. The development contributes reusable objects beyond the final proposition: a top- sum for finite fee samples, its expectation under a product probability law, and a separate mining-profit and attack-cost model. Formal proofs would make the assumptions behind strict fee improvement and a sub-majority threshold explicit. They would also resolve the paper's informal assertions about the attack cost curve without changing its stated target.
Adding candidate transactions can never reduce the top- fee sum, but that only gives a non-strict comparison. Strictness requires a positive probability that a new transaction displaces one selected by the honest block. The common fee law must therefore have more than one possible value, the block capacity must be positive, and the expectation must be finite. These conditions are easy to overlook when replacing the paper's order-statistics prose with a real-valued integral.
The threshold statement has a different difficulty. The paper describes a break-even hash-power level and treats its behavior as evident, but the needed existence and ordering are not established in the text. A faithful formal statement must retain the existential threshold below for an entire range of incumbent powers. It cannot choose a threshold after seeing one fixed allocation, since that would lose the proposition's sub-majority content.
Hash powers, rewards, costs, time and net cost are real numbers; hash powers used by miners are nonnegative. The miner population is finite, and the goal requires . The puzzle difficulty is always with , so no division by zero is used. Attack duration is positive. The attack fee and honest fee come from the same fee law with natural arrival counts ; the goal does not assume their ordering.
The paper says mining cost is nondecreasing and weakly quasi-convex on nonnegative power. Here cost is additionally convex there, which supports the single-peaked attack-profit model used in equation (3) and Figure 1. The attack-chain maximizer is required to be attained; some otherwise admissible costs yield no finite maximizer. The fee law is a nonnegative probability distribution with a finite first moment and is not a point mass. These additions are disclosed in the theorem descriptions and are needed for the paper's strict claims. Independent fees are represented by a product measure, and block fees by a maximum over sets of at most indices; with nonnegative fees and , this is the sum of the highest fees. This representation is continuous and integrable under the stated law, so the real integral does not receive Lean's default value for a non-integrable integrand.
The paper uses as a lower bound even though it says a successful attack must exceed it. The net-cost definition follows equation (3) literally at the maximum of that bound and the unconstrained optimizer. The target concerns the paper's incentive inequality in this stated model. Contributions to the fee-order-statistic infrastructure, continuity and integrability, attack-cost comparisons, and the two numbered lemmas are all useful to this mission.
Firms are run by managers who know more about cash flows than investors do. In the dynamic agency literature that started with DeMarzo and Fishman (2007) and DeMarzo and Sannikov (2006), a manager can divert cash by under-reporting output, and investors deter diversion with a contract that promises future pay after good reports and threatens liquidation after bad ones. Liquidation destroys value, so the threat itself is costly; the gap between the firm's value under the optimal contract and its first-best value is an agency cost, and in this class of models it is also the firm's credit spread.
Fu and Trigilia ask what happens when the manager can, from time to time, produce hard evidence that a low cash flow was bad luck rather than diversion. Disclosure is voluntary: evidence can be hidden, so the contract must reward disclosing it. The question is whether better information technology, a higher probability of evidence, makes the firm more valuable and less likely to default. The paper's answer (Proposition 4(a)) is used by the rest of the paper: by the analysis of when to invest in the technology (§7) and by the claims about default risk at initiation.
A firm produces i.i.d. cash flows with and . Investors and the manager are risk neutral and discount at rate . Reporting a high cash flow as low lets the manager divert , of which the manager keeps the private benefit with . Write . Each period, with probability , the manager also receives evidence of the true cash flow, which he may disclose or hide; is the classical model without evidence.
The contract is written recursively in the manager's promised utility . At state it chooses a liquidation probability , cash payments , and continuation utilities , indexed by (evidence disclosed or not) and by the reported cash flow. Writing , it must satisfy
The firm value (total surplus) is the fixed point of the Bellman operator
over feasible policies, in the class of continuous functions on with , where is the first-best value. The credit spread is . Two thresholds organise the solution: the cash payout boundary , above which , and the first termination threshold with , below which the optimal contract liquidates with positive probability.
For , with , the firm values for and , a firm value exists for each evidence probability and
The paper states the strict inequality for every . That is false below when : there firm value is linear through the origin with slope , which does not depend on , so and coincide on . The goal is the corrected statement: weak everywhere, strict above the first termination threshold of the smaller evidence probability.
The result says that the value of a firm run under moral hazard, and its default risk, respond monotonically to the quality of information about cash flows, even though the information is controlled by the party whose incentives are the problem. It underlies the paper's analysis of when investors should pay for the information technology and how the credit spread varies with it. The correction also identifies precisely where better evidence is worthless: in the liquidation region below when , where the firm reaches the payout boundary after a single high cash flow.
These results are proved in the paper (with the gap noted above) and none has a machine-checked proof. A complete formalization gives a verified treatment of a discrete-time dynamic contracting problem: the Bellman operator of a constrained recursive contract, the shape of its fixed point, the binding incentive constraints and the closed-form optimal contract.
The value function is defined only implicitly, as the fixed point of an operator whose feasible set is not convex in the obvious variables: promise keeping multiplies the liquidation probability by the promised utility. Comparing two fixed points for different requires knowing their shape, which in turn requires the explicit optimal policy. The paper's comparative-statics argument differentiates in through an envelope condition at points where has kinks, and treats the region below by continuity; but itself moves with , so the argument does not transfer from above to below it, and the strict claim fails there for . Any proof must handle the moving threshold explicitly.
All objects are in the namespace VolDisclosure.Evidence. Parameters are a structure with fields and lam (), with the standing assumptions , , , . A policy is nine real numbers (, four cash payments, four continuation utilities). The conventions are:
The firm value must be the fixed point of (T) over all feasible policies. Defining it from Proposition 3's policy, or dropping (under which ), would make the goal trivial; the goal also asserts existence of a firm value, so it cannot hold vacuously.
Not formalized: Proposition 2's cash formula (5) and the half of definition (3) that involves the investment-option problem (F); Proposition 3's third bullet (-period thresholds); Proposition 4(b)–(d), of which (c) and (d) are misprinted; the two-period model, the investment option (§7) and the default-risk results at initiation (Proposition 7).
A complete development needs a contraction fixed-point argument on bounded continuous functions on , the shape results for the fixed point, and the explicit policy; contributions of any milestone are welcome, and the fixed-point layer is reusable for other recursive contracting models.
Supply-chain traceability depends on firms adopting a technology together. A firm may benefit only after enough other firms in a shared supply chain have adopted; a supply chain may in turn become traceable only when a threshold number of its firms participate. Selecting firms to seed therefore couples many local adoption decisions. Blaettchen, Calmon, and Hall model this coupling as a network diffusion problem and ask for a least-cost seed set that eventually activates every firm Blaettchen, Calmon, and Hall, 2024. Their model permits overlapping supply chains and firm-specific benefits and costs, so it describes more than a single threshold rule on an ordinary graph.
The paper establishes an exact linear programming reformulation whose size depends exponentially on treewidth but only linearly on the numbers of firms and supply chains, up to parameter factors Theorem 2. This mission records that mathematical claim as a cost-independent extended formulation, together with source propositions describing the diffusion correspondence and the first binary formulation.
Let contain firms and let contain supply chains. Supply chain comprises the hyperedge . Firm has an adoption cost and receives a nonnegative integral benefit from an incident supply chain once enough of that chain's firms are active. The chain's threshold satisfies . The paper assumes that each firm's total incident benefit can cover its adoption cost. A seed set is active at time zero; every later set retains the already active firms and adds a firm when
A seed set fully activates the network if at some finite time. Given real seeding costs , the optimization value is
The auxiliary graph has a firm vertex for each and a supply-chain vertex for each , joined when . Its directed weighted version sends weight from a firm to a supply-chain vertex and weight in the reverse direction. Firm thresholds are ; supply-chain thresholds are . A weighted linear-threshold update activates vertices whose total incoming weight from active vertices reaches their threshold. Proposition 1 identifies the firms active after original steps with those active after auxiliary-graph steps Proposition 1, p. 10.
A tree decomposition is a tree of vertex bags that covers every vertex, places each graph edge or hyperedge in a bag, and keeps the bags containing one vertex connected along the tree. Its width is the largest bag size minus one. Write for an upper bound on the treewidth of the original hypergraph and Definition 2, p. 13; Proposition 9, p. 18.
The target is one finite linear system , where has visible seed coordinates and auxiliary coordinates . The system is chosen from the adoption instance and is independent of . Its projection onto is exactly the convex hull of fully activating seed indicators:
Consequently, minimizing over the same LP yields for every real . One absolute constant , placed before all instances and treewidth parameters, bounds the total number of variables and constraints by
This is the form stated immediately after Theorem 2 p. 18. The source's more detailed displayed bracket is not used as the target because its fixed exponents do not match the asymptotic bound obtained from the propositions cited in the proof.
The milestones follow the proof of Theorem 2 on p. 41. Proposition 1 and Corollary 1 identify the adoption process with a weighted threshold process on . Proposition 5 gives a binary program (4) whose feasible seed vectors are exactly the fully activating seed sets. Proposition 7 replaces its global acyclicity constraints by constraints inside the bags of a tree decomposition of , formulation (5). Proposition 8 splits the long covering constraints of (5) into partial sums along a rooted binary decomposition, formulation (10). Proposition 9 bounds the treewidth of the intersection graph of (10) by , where is the width of the decomposition of . Proposition 3 gives , and Proposition 4 is the bounded-treewidth LP theorem for binary programs pp. 10–18.
An exact LP gives the same optimum for every seeding-cost vector while keeping the constraints fixed. The size guarantee explains why a structurally sparse supply-chain network can admit a formulation far smaller than a generic enumeration of seed sets. It also separates the economics of choosing from the combinatorics of diffusion: once the network formulation is built, different cost scenarios use the same feasible region Theorem 2 and §5.3.
The paper proves the theorem, citing Proposition 4 from Laurent (2009) and Bienstock and Muñoz (2018). Neither Theorem 2 nor Proposition 4 has a machine-checked proof on Prove2Me. The remaining work is to formalize the paper's chain of reformulations and the cited LP theorem. The tree decomposition definitions are already published as reusable Prove2Me objects from Robertson and Seymour. The diffusion model, the binary formulation, and their relationship to an LP extended formulation are the new formal objects here.
The first binary program represents the activation order but connects variables across many firm–supply-chain pairs. Its intersection graph has treewidth at least , even when the underlying supply-chain graph is sparse Proposition 6, p. 16. Applying a bounded-treewidth LP theorem directly to that program therefore loses the desired parameter bound. The source introduces a more local formulation tied to a tree decomposition, and controlling the intersection graph of that formulation is the central difficulty. Formulation (10) as printed is not exactly right: the bit count (6) is one bit short, so that an instance with loses its optimal seed set, and the root inequalities (10c), (10g) use an undeclared variable. The targets use the bit ranges of the integer program (11) in the proof of Proposition 8 and the partial sum at each subtree root.
The Lean instance uses Fin n for firms, Fin m for supply chains, and natural numbers for benefits, adoption costs, and thresholds. The auxiliary graph is a simple graph on the disjoint union of these two finite types; the diffusion update retains active vertices and uses the paper's weak inequality at the threshold. Hypergraph treewidth requires every entire hyperedge in some bag and uses the published Robertson–Seymour tree decomposition predicate for the primal graph. Graph treewidth for uses the corresponding published bound predicate.
The paper treats connectedness as without loss of generality. Here it means that the incidence graph is connected and is included with the other standing assumptions. The gcd normalization discussed in §3.1 is a preprocessing convention, not a hypothesis. The finite family of successful seed sets always contains the all-firm set, so OPT is a genuine finite minimum. The formulation counts both auxiliary variables and inequalities. The additive shifts in the size bound handle small values of , , , and ; they do not change the asymptotic claim. The LP is quantified before , and its projection is specified, excluding a trivial LP selected separately for each cost vector.
Formulations (4), (5) and (10) are binary feasibility predicates over natural-number variables bounded by one; the adoption inequality is written as . Constraints (5c), (5d), (10i), (10j) range over distinct vertices of a bag (with the printed (5c) would be infeasible). A rooted binary tree decomposition is a published tree decomposition together with a root, a parent map and at most two children per node; the subtree root is the node of the subtree nearest the root. The partitions , are arbitrary data with the properties stated on p. 17, which are all the proofs use. Proposition 7 is stated for every tree decomposition of ; binarity is not needed there.
The generic finite linear-system and intersection-graph definitions can be reused beyond this paper. Contributions are welcome at every milestone; Proposition 4 is a general result on binary programs and is the most widely reusable.
Optimal transport asks how cheaply several prescribed probability distributions can be coupled. Adding a divergence penalty relative to their independent product makes the problem amenable to numerical methods, but changes its value. A quantitative bound on that change tells users of regularized transport how much bias a chosen regularization parameter can introduce. Eckstein and Nutz study this question through quantization of an optimal plan. Their Theorem 3.8 gives an entropic bound and a bound for a broader family of divergence penalties when the cost has a bounded second derivative. The result concerns the value of the transport problem; it does not assert convergence of optimal couplings or dual potentials.
There are marginals. For , is a closed convex subset of a Euclidean space and is a probability measure on with finite second moment. Their product has the Euclidean product metric. A coupling is a probability measure on whose th marginal is . The reference measure makes the coordinates independent.
The transport value is the infimum of over these couplings. The cost is continuous and has growth of order two, so its integral and the value are finite in this setting. For a strictly convex, lower bounded generator with and , the -divergence integrates against when ; it is otherwise. The regularized value is
Entropic regularization has , with . A law belongs to when it is supported on at most points of . An optimal plan has quantization rate when, for each , some satisfies . Here is the Wasserstein distance for the Euclidean product norm. The rate hypothesis is on the joint optimal plan, not merely on its individual marginals.
The goal is the corrected form of Theorem 3.8. Assume is twice continuously differentiable on a neighborhood of , , , , and is an optimal plan with . The Hessian bound is two-sided and holds for every direction in the ambient product space:
For entropy and , the first target is
For two marginals, suppose on , where is nondecreasing and concave there. Write and . If is strictly increasing on , , put . The second target includes and as and, when , , and ,
The source prints in both bounds and a one-sided condition in (3.4). The squared quantization estimate requires , and the Hessian condition must control both signs in every ambient direction. The mission records these corrections explicitly rather than changing the quantization hypothesis.
The first estimate controls entropic bias at order when an optimal joint plan admits the stated quantization rate. The second expresses a rate for other divergence generators through an inverse function determined by . These are established analytical results in the cited paper, though the corrected formulation is needed for the stated constants and hypotheses. The formalization target is a machine-checked statement of those rates and their supporting cost and divergence bounds. No completed machine-checked proof of this mission's goal is claimed here.
A finite approximation of the optimal plan need not retain the prescribed marginals. Restoring them can increase cost and divergence. A direct first-order cost estimate also misses the improvement sought here: the result uses cancellation associated with martingale quantization, while the remaining cost change is quadratic in the Wasserstein error. The requested infrastructure therefore includes a transport model with actual probability couplings, finite-support quantizers on the joint space, and a divergence that keeps its infinite value outside absolute continuity.
Lean represents each marginal space by EuclideanSpace ℝ (Fin (d i)) and the product by PiLp 2, whose norm is the paper's Euclidean product metric. The paper's marginal is Lean's index i : Fin N. The formal statement requires , closed convex supports, probability marginals concentrated on those supports with finite second moments, growth of order two for , and regularity on an open neighborhood. The real value OTval is used only under those conditions; OTreg and fDiv use extended real values, so an infinite divergence cannot silently become zero. The divergence definition assigns when its density integrand is not integrable, consistent with a lower-bounded generator under a probability reference measure. The condition covers without division by zero. The function is constrained only on , allowing generators with a nonzero value at zero.
The development reuses the published WassersteinDRO.Duality.wassersteinDistance for . Its new definitions of couplings, product reference law, divergence, quantization, and martingale coupling are reusable for related finite-dimensional transport results. The milestones isolate the Taylor estimate, the marginal-restoring coupling and its data-processing bound, the corrected cost estimate, and the entropic discrete-marginal bound of Lemma 2.3(iii). Lemma 2.3(i) is not posed here because the proposed positive-argument interpretation of does not control , and its stated divergence bound then has a two-point counterexample. A valid closure must use joint-plan quantization and a two-sided Hessian bound; replacing the regularized infimum by a default real value, restricting the Hessian to directions inside , or quantizing only the marginals would change the result.
Network interdiction asks how an inspector should randomize over sets of links when a router can choose a path through a network. Link inspection probabilities and path interception probabilities describe different features of the same random choice. Specifying both sets of numbers separately does not guarantee that one distribution over inspection sets realizes them. The poset model of Dahan, Amin and Jaillet isolates this compatibility question: links become elements of a partially ordered set, and relevant paths become maximal chains. Their feasibility theorem supplies the distributions required in the equilibrium analysis of their interdiction game. This mission formalizes that theorem and its stated structural results, from the pinned preprint arXiv:1811.08516v3.
The question also stands on its own as a finite probability problem. A vector of element marginals fixes the chance of selecting each element, while a lower bound for every maximal chain fixes the chance of selecting at least one element from that chain. The two requirements interact because chains can overlap and share several splice points. Conditions that look sufficient one chain at a time can fail to support a single distribution across all chains. The paper's Example 2 on p. 9 demonstrates infeasibility when its conservation condition is absent. Dahan, Amin and Jaillet prove that the two stated conditions together are sufficient for every finite nonempty poset.
A finite poset is a finite set with a reflexive, antisymmetric and transitive order. A chain is a subset whose points are pairwise comparable; a chain is maximal when it cannot be enlarged while remaining a chain. Write for the family of maximal chains. For each , prescribe an element marginal . For each , prescribe a chain hitting target . A distribution gives a nonnegative weight to every subset , including the empty set, with total weight one. Its marginal at is the total weight of subsets containing ; its hitting probability for is the total weight of subsets meeting .
Two parameter conditions are central. Condition (2) says for every maximal chain. To state condition (3), take maximal chains and a common point . Splice them at : follows through and then above it; takes the opposite halves. The conservation law is for every such pair and every common point. The paper's §2.2 specifies these conditions and the distribution problem (D) on pp. 7–8.
The auxiliary program (Q) keeps the element marginal equalities but omits total weight one. It minimizes total assigned weight while limiting how much weight may be assigned to subsets that meet a maximal chain more than once. Its slack is , and its optimum is . The factor in its chain constraint is the real number when .
The goal is the paper's Theorem 1, p. 8: under conditions (2) and (3), some distribution satisfies all marginals and chain hitting bounds simultaneously:
Theorem 2, p. 11, is the strongest quantitative milestone. With the same standing setting, it identifies the least feasible total weight in (Q):
The intervening milestones are the paper's Lemmas 1–3 and Propositions 1–4. Lemma 2 establishes the poset generated by a splice-closed family of chains. Proposition 1 relates (D) to the bound . Propositions 2–4 state the properties, termination, feasibility and total weight of the paper's Algorithm 1.
Theorem 1 is an existence guarantee for a joint distribution, not merely separate bounds that can be met one chain at a time. It lets a model specify desired inspection marginals and path interception lower bounds while retaining a genuine probability distribution over inspection sets. In the paper, this supplies the interdiction strategies used in the network game's equilibrium characterization in §5. Theorem 2 gives the exact amount of unnormalized weight needed to meet the same constraints, which also identifies when normalization to a probability distribution is possible.
The results are already proved in the cited paper. The work here is to state their hypotheses, objects, algorithm and conclusions in Lean and then construct machine-checked proofs. The reusable output is a finite-poset interface for maximal-chain splicing, chain-generated subposets, distributions on subsets, and the auxiliary optimization problem. The game equilibrium theorem of §5 is outside this mission; a formal development of it could import the distribution theorem after it is proved.
Matching each element marginal separately does not control the probability of hitting every chain at once. If a selected subset meets a chain at two or more elements, the sum of its element marginals counts that subset more than once, while the chain hitting event counts it once. Hence condition (2), although necessary, does not alone capture all compatibility constraints. The conservation law couples overlapping maximal chains at every common splice point, and the auxiliary program records the excess count . In Algorithm 1, a chain can be removed from the active family while its constraint must remain satisfied; the paper's Lemma 3 addresses precisely that issue. Sections 2–3 of the preprint give the detailed statements.
The ground set is a nonempty finite Lean type with a partial order. Subsets and maximal chains are Finsets, and a distribution is a real-valued function on all finite subsets. The values of are stored as a function on finite subsets for convenient splicing, but all bounds and conservation equations use only maximal chains. The splice uses the first chain at and below the common point and the second at and above it. The conservation equation quantifies over every common point. This rules out a vacuous or weaker encoding that checks only one splice, drops the empty subset, or replaces probability normalization by an inequality.
The optimal value is the real infimum of feasible (Q) objective values. Under the standing assumptions it is a proper finite optimum; the statements using it retain those assumptions. The maximum in Theorem 2 ranges over all elements and maximal chains of the nonempty poset. Cardinalities in (Q) are converted to reals before subtracting one. The algorithm's Lean state zero is paper iteration one, and its output accumulates weights assigned to a subset if that subset appears in more than one iteration. This additive interpretation of step A7 is disclosed because the printed assignment does not say what happens on repetition.
The development needs Mathlib's finite posets, chains, finite sets and real-number sums, together with the paper-specific chain relation and algorithm state. Contributions proving the numbered milestones, establishing the algorithm's invariants, or providing reusable facts about chain splicing and finite distributions all advance the goal. The affine special case of §4 and the game theory of §5 are separate work.
Training a neural network means minimizing a non-convex loss over its weights. Local search methods can only certify local optimality, so a recurring question in the theory of neural network optimization is whether every local minimum of the training loss is a global minimum. A local minimum that is not global is called a sub-optimal (or bad) local minimum.
A line of positive results suggested that sufficiently wide networks have no bad local minima. Yu and Chen (IEEE Trans. Neural Networks 6(5), 1995, Theorem 3) stated that for one-hidden-layer sigmoid networks with at least as many hidden neurons as training samples, every local minimum is global; the survey of Bianchini and Gori (Neurocomputing, 1996) lists this as a main result of the area. Later work proved weaker landscape properties for deep over-parameterized networks, such as the absence of sub-optimal valleys or basins (Nguyen, Mukkamala and Hein, arXiv:1809.10749; Nguyen, arXiv:1901.07417), and Nguyen, Mukkamala and Hein conjectured that "no bad local minima" holds under mild conditions.
Timeline of related results, as attributed in the source paper:
A fully connected network with hidden layers has widths , input width and output width . Its parameters are
Given an activation and a data matrix whose columns are the samples, the post-activations are and
and the network output is , with no output bias. For targets , the empirical loss is
Two assumptions are made.
For every satisfying Assumption 1 with , every satisfying Assumption 2, any depth and any widths with , there is an output matrix such that
The data and the activation are given; only is chosen. The widths other than are unrestricted, so the statement covers arbitrarily wide and deep networks.
The theorem is a counter-example: for generic data and almost every smooth activation, increasing width or depth does not by itself remove bad local minima of the squared loss. It refutes Theorem 3 of Yu and Chen (1995) (Corollary 2 of the paper) and the conjecture of Nguyen, Mukkamala and Hein for this setting. Positive landscape results therefore need further assumptions on the data, the targets or the architecture, and the construction indicates which assumptions cannot be dropped.
The result is proved in the paper; no machine-checked proof of it is known. A formalization would verify a full counter-example for arbitrary depth, which involves a layer-by-layer second-order expansion whose bookkeeping across layers is where informal arguments of this type are most error-prone. It also provides a reusable Lean model of a deep fully connected network with biases and an arbitrary activation, which other landscape results can build on.
The output of the constructed configuration does not depend on the input, so a perturbation of changes in ways that need not be first-order: the obvious approach of checking a vanishing gradient and a positive semidefinite Hessian is inconclusive, because the loss is flat along several directions at the constructed point (for instance, changes of that keep its row sums), and the decisive effect of perturbing appears only at second order in the hidden layers. Local minimality must be shown for all nearby configurations at once, by controlling the second-order term of every layer uniformly in a neighbourhood and propagating the sign through the layers. The correlation condition must hold for every row of and every neuron simultaneously.
Fin a → Fin b → ℝ; indices of neurons and samples are 0-based. The parameter space is the full product of all weights and all hidden biases , with its usual sup-norm metric; local minimality is Mathlib's IsLocalMin. The forward pass is defined by recursion over the layers, feeding the post-activation of layer to layer (the printed eq. (2b) writes the pre-activation, a slip).Contributions welcome: proofs of the milestones, in particular a Lean development of the layer-wise Taylor expansion behind Lemma 2.
Classical ruin theory studies the Cramér–Lundberg model: an insurer's capital grows linearly through premiums and drops at the arrival epochs of a compound Poisson stream of claims. Two features of real capital processes are missing from it. Free capital earns interest, so the drift depends on the current level. And a firm may receive capital injections, upward jumps that arrive at random. Ruin with compounding assets goes back to Harrison (1977) and is surveyed in Paulsen (2008). Discounted penalties at ruin, which involve the deficit at ruin and the surplus just before it, are the subject of Gerber–Shiu theory (Kyprianou 2013).
Boxma and Mandjes (Affine storage and insurance risk models, Math. Oper. Res. 46(4), 2021) combine both features. The surplus has an affine drift and two-sided jumps. They give a closed form for the joint transform of three ruin quantities: the time of ruin, the surplus just before ruin (the undershoot) and the deficit at ruin (the overshoot). The same insurance process later drives the paper's two storage models (§3–§4), through a duality argument. This mission formalizes the insurance result, §2 of the paper, culminating in its Theorem 1.
Fix a premium rate and an interest rate . Upward jumps arrive at the epochs of a Poisson process with rate , and their sizes are i.i.d. exponential with mean . Claims arrive at the epochs of an independent Poisson process with rate . Their sizes are i.i.d. with a density on and Laplace–Stieltjes transform . Write .
Starting from , the surplus follows between jumps. It rises by at and falls by at :
The ruin time is , with if the surplus stays positive. The overshoot is and the undershoot is the left limit . Let be exponential with mean , independent of everything else. For define
So is evaluated at an initial surplus that is exponential with mean .
Put and
Let be a primitive of on . Put , and . Then let and .
For every with ,
where and
The constants and are the model's own, defined through the process, not free parameters.
The milestones follow the paper's derivation:
Theorem 1 reduces a three-dimensional joint law to one-dimensional integrals of explicit functions of the model data. Through , , and it gives the transform of the ruin time, overshoot and undershoot jointly. Inverting it numerically gives ruin probabilities before a fixed horizon. Its specialisations include discounted penalty functions of Gerber–Shiu type for a risk process with interest and capital injections. In the paper, the same analysis carries over to a reflected storage process and to the dual storage process with affine release rate.
On the formal side, no ruin-theory result for a risk process with interest is machine-checked yet. The mission produces a pathwise construction of a piecewise-deterministic jump process with level-dependent drift, and a rigorous version of the paper's heuristic derivation. The page derives Lemma 1 by an argument that assumes is differentiable. It also asserts the boundary behaviour of , and it solves the linear system (10)–(11) without checking that its determinant is nonzero. All three steps become proof obligations here.
The algebra from Proposition 1 to Theorem 1 is routine once its inputs are available. Two steps are not.
The first is analytic regularity of . Lemma 1 needs to be differentiable on . The obvious route conditions on the first event in and lets , but it presupposes that derivative. Proving it requires a first-jump decomposition along the deterministic flow, together with right-continuity of at , which is the identity .
The second is the singular point , where has a pole. The variation-of-constants formula fixes only up to separate constants on and . For , the formula (9) integrates across the pole. Its correctness there rests on , which in turn comes from the boundedness of near . The page's order, (9) before (11), hides this dependence.
All primitives (interarrival times and jump sizes of both streams) form one independent family Z : Fin 4 × ℕ → Ω → ℝ on a probability space, with the stated laws. The surplus and its left limit are defined by the closed form above. Jump counts are least indices, which agree with the true counts almost surely. The ruin time takes values in . The horizon is integrated out against expMeasure ν. is quantified over all primitives of on . At the removable point , takes its limit value .
The hypotheses , , and are added to the page's . With the denominator in (12) vanishes, with ruin is impossible, and the page itself assumes tacitly. The case (Remark 5) and the page's sharper logarithmic rates of are not formalized. Those rates need a moment of the claims that the paper does not assume; the milestones state only what holds without it.
The goal cannot be satisfied trivially. and are expectations over the pathwise process, not formulas. Theorem 1 is about these objects, not about an arbitrary bounded solution of (6). The determinant condition is part of the conclusion, so the quotient in (12) is never Lean's .
Useful infrastructure, all welcome as contributions:
The first and last are reusable beyond this mission.
A seller choosing between a first-price auction (FPA) and a second-price auction (SPA) needs to know whether the payment rule changes expected revenue. In the classical independent private-value benchmark, the two formats can be revenue equivalent. Balzer and Rosato examine a different setting: a bidder’s value depends on other bidders’ private signals, and the bidder dislikes outcomes that fall below a reference lottery formed from the bid she chooses. Their result gives a precise revenue ranking under these preferences. The paper was published online in Management Science in 2020 in its Articles in Advance pagination Balzer and Rosato.
The question matters because a payment rule changes both what a winner pays and which monetary outcomes she anticipates. In an FPA the winner pays her own bid. In an SPA she pays the highest opposing bid, so her payment varies with competitors’ signals even when she wins. Balzer and Rosato distinguish the risk of winning versus losing, which they call extensive risk, from variation in value or payment among winning outcomes, which they call intensive risk. Their analysis asks how these risks affect bidding and the seller’s expected receipts Balzer and Rosato, §§3–4.
There are bidders. Each observes a signal drawn independently from a continuously differentiable distribution on , where and the density is strictly positive. Bidder values the item at . The value is nonnegative, increasing in every signal, strictly increasing in the bidder’s own signal, twice continuously differentiable, and symmetric in opponents’ signals. The distribution of the highest of the opposing signals has cumulative distribution and density Balzer and Rosato, §2.1 and §3.1.
A realized outcome is a value-payment pair . Its comparison point is another such pair . Gain–loss utility is for and for , with denoting the item and money dimensions. Here , , and . Total utility is
For outcome lottery and reference lottery , expected utility averages this expression over an independent draw from each lottery. Under a choice-acclimating personal equilibrium (CPE), a type assesses each possible nonnegative bid against the lottery that the same bid induces. A symmetric increasing strategy is a CPE when bidding maximizes this self-referenced expected utility for every type. The paper maintains Assumption 1, , through its CPE results Balzer and Rosato, Definition 1 and Assumption 1.
The main target is Corollary 1. For any symmetric CPE strategies and in the FPA and SPA, respectively, let and be the expectation of the sum of all bidders’ payments. Then
The milestone list follows the paper’s CPE results: the direct-utility representations (10) and (12), existence and bid formulas for every symmetric equilibrium in Propositions 7 and 9, the common equilibrium-utility identity in the proof of Proposition 11, and Proposition 11’s comparison of utilities and payments. These targets retain the distinction between a lottery-based preference definition and the formulas derived from it Balzer and Rosato, pp. 10–11 and Appendix.
The corollary tells the seller which format yields more expected revenue within this model. When bidders have no loss aversion over money, the two formats yield the same revenue even though values are interdependent. With positive monetary loss aversion, the FPA yields strictly more. Proposition 11 gives the bidder-level comparison behind this statement: equilibrium utility is the same in both formats, while each type above the lowest pays more in expectation in the FPA when Balzer and Rosato, Proposition 11 and Corollary 1.
The result is proved in the paper but is not yet machine-checked in this mission. A completed formalization would connect the primitive gain–loss utility, lottery construction, CPE incentive condition, interim payment comparison, and ex ante revenue ranking. The auction data module can also support other results about independent signals and interdependent values; the loss-aversion module records the additional preference and equilibrium structure.
The expected utility of a bid changes when the bid changes because the reference lottery changes with it. Treating the comparison point as fixed would describe a different equilibrium concept. An SPA also exposes winners to variation in the payment itself, which is absent from the FPA. Thus the two formats cannot be compared merely by inserting the same bid into different payment formulas. The paper’s two direct-utility displays and its payment comparison are separate substantive targets Balzer and Rosato, §4 and proof of Proposition 11.
Lean uses real-valued signals, values, bids, and payments, and exactly bidders, so an opponent always exists. The signal law is a density-weighted measure on ; opponent and all-bidder signals use product laws. Strategies are measurable, nonnegative, and strictly increasing on the signal support. The model requires measurable values so mapped lotteries are genuine measures. A bid wins only when it strictly exceeds every opposing bid; ties have probability zero under the stated atomless signal law and strict monotonicity. Values of strategies outside the support do not affect the lotteries.
Revenue is defined directly as the expectation of the sum of payments, rather than by the payment formulas that the results seek to establish. Likewise, CPE is the incentive inequality over every nonnegative bid, and expected utility is built from the primitive outcome and reference lotteries. The direct-utility formulas are theorem targets, not definitions. The conditional value is used only when , where ; the bid formulas (11) and (13) are stated on because their displayed denominators vanish at the lower endpoint for some bidder counts.
The paper writes the intensive-risk term with a conditional density of value, although that density need not exist for private values. Lean instead uses a double expectation over the winning-signal region. The paper’s printed prefactor in (10) is inconsistent with a reference lottery induced by the deviation; the formalization uses . This correction is recorded on both representation milestones. Contributions toward the measure identities, equilibrium existence, envelope identity, and bidder-level payment comparison are all within scope.
A cryptocurrency user can attach a fee to a transaction, and a miner can choose which waiting transactions enter the next block. When the most valuable waiting transactions compete for a limited number of places, the fee rule affects both the user's bid and the amount the user expects to pay. Basu, Easley, O'Hara and Sirer study a protocol that charges every included transaction the minimum included fee. This makes the fee visible from the block itself, but it also lets a bidder affect the price when that bidder supplies the lowest winning bid. Their Result 3 asks how much this incentive matters when many users are active. Basu et al., §4 and Result 3, pp. 13–16.
The result is a useful distinction for the design of a multi-unit fee auction. Truthful bidding can fail as an exact dominant strategy even while the maximum expected benefit from deviating becomes small in a large active market. The paper treats this as one part of a proposed fee mechanism; the claims about miner payments, fill penalties and longer-run blockchain behavior are separate from Result 3. Basu et al., §4, pp. 13–16.
A block has places for transactions. There are other active users besides the bidder being studied, with . Each user's value for inclusion in the current block and each allowed bid lie in . The others' truthful bids form a vector . Write for its th highest entry, counting repeated values. The rule places the highest bids in the block. A winning bidder pays the lowest of those bids. Basu et al., §3, pp. 10–11; §4, pp. 13–16.
For a bidder with value who bids , let be the current-block payoff: value less the charged fee when included, and zero otherwise. A bid strictly above wins; the bidder then pays . A bid equal to loses under the tie convention used here. The strategic gain is the best admissible payoff minus the payoff from bidding one's value,
The model draws active users' values independently from a common continuous density on , with throughout that interval. Thus the joint law of is the product law of draws. A bidder knows their own value and the number of active users, but does not observe the other users' values or bids before choosing their own bid. The expected strategic gain therefore fixes the bid before averaging over the others' values :
The goal is Result 3. Its first clause says that truthful bidding fails to be a dominant strategy: for every admissible number of other active users, there is a valid profile and an admissible deviation with higher current-block payoff. Its second clause concerns the expected strategic gain when the others bid truthfully:
The quantifier over makes the convergence uniform across the bidder's possible values. It follows the paper's claim for “any bidder” and the value-independent upper bound stated immediately before Result 3. Basu et al., Result 3, p. 16; proof, pp. 21–22.
The milestone list records the statements in the paper's proof: an explicit profitable deviation when ; no profitable bid below the lower threshold; the two possible prices for a winning slot; the pointwise bound ; the bound ; and the assertion that this expected spacing tends to zero as grows. These are intermediate targets, not replacements for the goal about strategic gain. Basu et al., proof of Result 3, pp. 21–22.
The theorem identifies what the mechanism does and does not guarantee for a user. It rules out an exact dominant-strategy interpretation of truthful bidding for the minimum included fee protocol, while bounding the incentive to depart from truthfulness in a sufficiently large active market. Without the first clause, a claim of truthfulness would be misleading; without the second, the protocol would lack the paper's quantitative reason to expect truthful behavior to be nearly optimal when participation is high. Basu et al., §4, p. 16.
The paper gives the mathematical result and an appendix argument. This mission asks for a machine-checked account of that result, including the auction payoff, the order statistics, and the probability statement; these claims are open Lean targets in the proposed mission, not already machine-checked results. The definitions of the finite order statistic and of gain from an admissible deviation can be reused in later multi-unit auction formalizations. The density and product-law interface may also support other bounded-support order-statistic results.
A pointwise payoff comparison is not by itself an asymptotic statement. The gain depends on the entire vector of other bids through two adjacent order statistics and on a supremum over all allowed bids. Turning its bound into a statement about expectations requires those random quantities to be measurable and integrable. The spacing between the st and th highest of draws then has to vanish in expectation for the stated class of densities. Merely showing that this spacing is nonnegative or at most gives no decay with . Basu et al., proof of Result 3, p. 22.
There is also a boundary issue in the auction itself: a bid tied at the last included position requires a specified outcome. The protocol states the payment for included users but does not prescribe a complete deterministic tie rule for this one-bidder analysis. The chosen strict inclusion threshold makes every payoff a total function, and the continuous value law makes ties irrelevant to the expected-gain limit.
Lean represents the other active users as Fin m → ℝ, their th highest value as a real supremum defining kthHighest, and their i.i.d. values as Measure.pi of a density law supported on . The density assumption includes , continuity on that interval, , and total integral one. The slots satisfy : has no and the fee rule becomes a first-price case. The index is the number of other active users; the convergence is conditional on that count, matching the model's statement that bidders know how many users are active. Basu et al., §3, p. 11; Result 3, p. 16.
Bids range over . The gain is computed from the protocol payoff by a supremum over that interval; it is not defined as the adjacent order-statistic spacing or as a closed expression for the optimum. The expected gain takes the supremum over bids of expected payoffs, not the expectation of the pointwise supremum, since a bidder cannot condition a bid on the others' bids. The theorem explicitly requires integrability of the payoff of every admissible bid, so the real-valued integral cannot acquire meaning from Lean's default value for a non-integrable function. The first clause uses a concrete admissible bid profile; the second uses the product law of truthful others. The participation probability , the total potential user count , miner rewards, and the multi-block averaging parameter do not enter this conditional one-block claim. Basu et al., §3–§4, pp. 10–16.
The development needs finite order statistics, a measurable payoff and gain, probability laws from continuous densities, and integrability and convergence of adjacent order-statistic spacings. Contributions that establish those interfaces or prove the quoted intermediate claims serve the stated goal directly.
A Nash equilibrium of a two-player game is a pair of choices from which neither player can improve by changing their own choice alone. Computing one equilibrium is a central task in algorithmic game theory. For unrestricted bimatrix games, their payoff tables may encode difficult equilibrium computations. The structure of a rank-one bimatrix game gives a more specific question: can one equilibrium be found in time polynomial in the binary description of the game, even when equilibria are not isolated? Adsul, Garg, Mehta, Sohoni and von Stengel answer this with their BINSEARCH algorithm in Fast Algorithms for Rank-1 Bimatrix Games, Theorem 19. Their analysis explicitly includes degenerate games, which can have continua of equilibria (p. 5).
The paper develops a geometric account of rank reduction, parameterized linear programs, the connected set of equilibria of the auxiliary games, and the binary search procedure. The present mission targets the algorithmic result. The separately stated results on enumeration, exponentially many equilibria, and a structure theorem are outside this mission (Adsul et al., §§6–9).
An bimatrix game has payoff matrices . Player 1 chooses a row and player 2 chooses a column. A mixed strategy assigns nonnegative weights summing to one to a player's pure strategies. Write and for the two simplices. Against mixed strategies and , the payoffs are and . The pair is a Nash equilibrium when each strategy maximizes its owner's payoff against the other. These are the paper's definitions on pp. 4–5.
The games studied here have the form
The sum of the two payoff matrices is , so its rank is at most one. Zero vectors are allowed; the zero-sum case is included. A real parameter defines an auxiliary game . The set consists of triples for which is an equilibrium of that auxiliary game. The desired equilibria are the triples in that also satisfy (equations (10)–(12)).
For each , a primal linear program minimizes subject to , , and . Its dual maximizes subject to and . Their optimal solutions describe the auxiliary equilibria. The sets and identify the inequalities that can be slack or the coordinates that can be positive on the dual optimal face. They define a face of the parameterized primal polyhedron (equations (17)–(29)).
The goal is Theorem 19: for rational of combined binary length , and polynomial-time LP solvers returning extreme optimal solutions, Figure 2's BINSEARCH finds a Nash equilibrium of in polynomial time in . In the formal statement, a polynomial is chosen before the dimensions, game data, and admissible LP-selection oracle. It bounds the number of main-loop iterations, the bit length of every midpoint parameter passed to , and the bit length of every returned , including the parameter passed to the final :
for every optimal returned by the final dual LP, with the stated bound on each intermediate parameter. The ordered milestones cover best responses (Lemma 1), rank reduction (Lemma 6 and Theorem 7), primal-dual optimality (Lemma 9), preservation of the bracket (Lemma 17), the segment test (Lemma 18), and separation of distinct breakpoints (proof of Theorem 19).
The theorem gives an algorithm whose performance guarantee depends on the input's bit length, not on the number of equilibria. This matters for degenerate games: a continuum of equilibria does not by itself supply an algorithm to find one. The auxiliary LPs also connect game-theoretic best responses to ordinary finite-dimensional optimization. These claims and their precise scope are in §§4–5 of the paper.
The paper proves the theorem on paper. This mission asks for a machine-checked version of its formal statements and, ultimately, the proof. The definitions of best responses, primal and dual feasible sets, optimal faces, breakpoints, and a rational-input LP oracle are reusable in other formalizations of parametric games. The draft theorem declarations contain proof placeholders; they are targets rather than completed machine-checked proofs.
Ordinary bisection finds an interval containing an equilibrium parameter, but it can continue indefinitely when the equilibrium lies at a breakpoint: the two bounds can remain in neighboring segments. Repeated midpoints also create parameters whose bit descriptions grow with the number of iterations. Figure 2 therefore uses additional LPs that search the current optimal face and, in a strict branch, replace the answer by a breakpoint. A correctness proof must cover every permitted extreme optimal answer from these LPs, including degenerate faces, and must bound the separation of rational breakpoints (pp. 17–22).
Lean represents pure strategies by zero-based Fin m and Fin n, mixed strategies by real standard simplices, and payoffs by real matrices and vectors. The goal's input entries are rational and cast to reals for the LPs. It assumes : the paper leaves this implicit, while its minimum over the entries of and both mixed-strategy simplices require nonempty index sets. The game may be degenerate and may have rank zero.
LP optima are members of feasible sets whose objective is least or greatest on the full feasible objective image. An extreme LP solution also lies in the feasible set's extreme-point set. A selection oracle is constrained whenever an optimal extreme solution exists, and the goal asserts that every LP actually called during the run has such an answer. This excludes arbitrary values from an oracle at an infeasible or unbounded call. The initial bracket is the minimum and maximum entry of ; every branch and BR replacement follows Figure 2. The breakpoint endpoint symbols and are represented by absent optional finite endpoints in Lemma 18.
The running-time clause is an iteration bound together with a bound on the binary size of the midpoint and returned LP parameters; it does not formalize a machine model or the assumed polynomial-time LP solver. The goal is about the specified BINSEARCH run for every admissible selection oracle. Existence of some Nash equilibrium or termination for one hand-picked oracle would not express Theorem 19. Lemma 6 uses , the condition used in its printed proof; with a freely fixed , its printed implication (a) to (b) is false. A full development needs finite-dimensional LP duality, extreme-point and rational-vertex bounds, convex optimal-face geometry, and control of the run invariant. Contributions proving these components are welcome.
A bilevel program is an optimization problem in which one of the constraints is itself an optimization problem. An upper-level decision maker (a leader) chooses ; a lower-level decision maker (a follower) responds with an optimal solution of a problem parameterized by ; the leader's cost depends on both. Stackelberg games, toll setting on transportation networks, hyperparameter selection in machine learning, and many pricing and network design problems in operations research have this form. See Dempe, Foundations of Bilevel Programming (Kluwer, 2002), and Dempe and Zemkoho (eds.), Bilevel Optimization (Springer, 2020).
Necessary optimality conditions for bilevel programs are hard to obtain because the follower's optimality is not a standard constraint. The value function approach of Outrata (1990) replaces " is optimal for the lower level" by the single inequality , where is the optimal value of the lower level. This gives an equivalent single-level problem, but a well-known obstacle follows: Ye and Zhu (1995) showed that the standard nonsmooth constraint qualifications (nonsmooth MFCQ, equivalently NNAMCQ) fail at every feasible point of this reformulation. KKT-type conditions have therefore relied on calmness (Clarke 1983) or on partial calmness (Ye and Zhu 1995), both of which are strong.
Gfrerer (2013) introduced directional versions of regularity conditions, required only along one critical direction. Bai and Ye (arXiv:2004.01783, Mathematics of Operations Research 2022) carry this idea to the value function approach. They define calmness in a direction, prove a directional KKT condition for a general inequality-constrained problem under it, and apply this to the value-function reformulation of a bilevel program. This mission formalizes that chain, up to the paper's Theorem 5.1.
Let , and be continuously differentiable. For each , is the solution set of the lower level program : subject to . The bilevel program is
The value function is , and the value-function reformulation is
All norms are Euclidean, and is the open unit ball. For a direction and , the directional neighbourhood is
It is a cone of half-angle governed by around the ray through , cut at radius ; for it is the whole ball .
(VP) is calm at in direction if there are such that for every perturbation of the right-hand sides and every that satisfies the perturbed constraints. The same definition (Definition 3.1) applies to a general problem (P): s.t. .
A map is directionally Lipschitz at in direction if it is Lipschitz on for some . Its directional derivative is .
The directional limiting subdifferential collects the limits of Fréchet subgradients with , and .
The critical cone of (VP) consists of the with
Let be a local minimizer of (BP). Suppose is directionally Lipschitz and directionally differentiable at in direction , that , and that (VP) is calm at in direction . Then there exist , and with
Theorem 5.1 gives a KKT condition for bilevel programs under a regularity assumption checked in one critical direction only. Directional calmness is weaker than classical calmness, because the neighbourhood is smaller than a ball. The conclusion is also sharper than the nondirectional KKT condition: the subdifferential of is the directional one, and the multipliers satisfy the extra orthogonality conditions with and . Example 3.1 of the paper is a bilevel program in which partial calmness and calmness fail but calmness in a nonzero critical direction holds. Theorem 5.1 applies there, and the classical results do not. Section 5 of the paper derives verifiable sufficient conditions (directional quasi-normality, Theorems 5.2–5.3) from it.
The result is proved in the paper; nothing here is open mathematically. To our knowledge none of it has been machine-checked. A formal proof would check a chain that passes through Ekeland's variational principle, a Fermat rule and a chain rule for limiting subdifferentials, and a limiting argument with directional sequences. The general Theorem 3.1 is reusable for any inequality-constrained program with directionally Lipschitz constraints.
The obvious route is "calmness gives exact penalization, then Fermat's rule". For directional calmness this only says that minimizes the penalized function on the directional neighbourhood, which is not a neighbourhood of . Fermat's rule cannot be applied at itself, so the stationarity must be produced at points inside the cone that approach along the direction, and then passed to the limit. That passage needs the multipliers to be bounded and the limiting subgradients to be directional ones.
The bilevel step adds two obstacles. The constraint is nonsmooth and extended-valued, so its subdifferential has to be split exactly into and the -part of . And when the conclusion still requires an element of , which exists only because is directionally Lipschitz.
EuclideanSpace ℝ (Fin q) (E q). The pair lives in WithLp 2 (E n × E m), the Euclidean product; the bare product type would carry the sup norm. Theorem 3.1 and its milestones are stated on any finite-dimensional real inner product space, which is linearly isometric to ; this lets the goal apply Theorem 3.1 on the product.EReal-valued infimum: when the lower level is infeasible, when it is unbounded. The constraint of (VP) is evaluated in EReal. " directionally Lipschitz" includes finiteness of on , which Definition 2.4 leaves implicit because it is written for real-valued maps. Directional differentiability is that of as a real function on that set, and its value is passed explicitly and enters the critical cone.NonconvexSplitting.Shared.IsRegularSubgrad, and the directional normal cone is the published SetConstrSOC.Directional.dirLimNormal. Each is an inner product, and is . "" is stated as the existence of one that makes the sum zero, including when .A complete development needs Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle) and the Fréchet and limiting subdifferential calculus: the Fermat rule, the sum rule with a smooth function, and the chain rule for a Lipschitz composition. It also needs the fact that Lipschitz functions have bounded subgradients. These are reusable well beyond this mission. Proofs of any milestone are welcome, as are proofs of the subdifferential calculus lemmas as separate theorems.
Estimating a probability that is too small to observe often by direct simulation is a routine problem in reliability analysis and rare-event simulation. Importance sampling changes the sampling law so that the event is seen more often, then corrects each sampled outcome with a likelihood ratio. The conventional design in a large-deviations setting mixes one exponential tilt for every dominating point of the rare-event set. That design is judged by the estimator's second moment. Bai, Huang, Lam and Zhao ask whether the resulting variance requirement is stronger than what is needed for an estimate that is accurate with high probability Bai et al., 2022.
Their result concerns the case in which different parts of the rare-event set have different exponential rates. A part with a higher rate can contribute a very large likelihood ratio on the rare occasions it is sampled, making the variance large, while barely affecting an estimate from a feasible number of replications. The paper introduces probabilistic efficiency to express the sampling requirement directly through the estimator's relative error. The mission formalizes the paper's Theorem 6, which treats all ties among the most significant dominating points.
For each rarity parameter , let be a random vector in with law . Fix a Borel set . The probability to be estimated is
The scaled logarithmic moment generating function is . Assumption 1 requires a pointwise extended-real limit , an interior effective domain containing zero, differentiability there, and steepness at its boundary. Its rate function is the Legendre transform , and for a set . Assumption 2 requires to be Borel, , , and Bai et al., pp. 7–8.
A dominating set is a finite minimal collection of boundary points of . Each has an associated tilt satisfying , and the half-spaces cover . A point is more significant when it has a smaller value of . Exponential tilting toward gives a sampling law whose density relative to the original law is . A mixture gives these laws positive weights summing to one Bai et al., pp. 8–10.
For independent outputs under the mixture law , write for their mean. At tolerance , the minimal relative discrepancy is . Strong probabilistic efficiency means that one sample-size function grows subexponentially in and makes this discrepancy tend to zero for every Bai et al., p. 16.
Let contain exactly the points of having the smallest rate, including every tie. The goal is Theorem 6 Bai et al., p. 20:
for some with . The result allows the mixture to omit every dominating point with a strictly larger rate. It does not choose a fixed sample size or require a second-moment efficiency guarantee for the resulting mixture.
The milestones state the Gärtner–Ellis bounds of Theorem 1, the rate minimization of Theorem 2, full-mixture asymptotic efficiency of Proposition 1, the implication of Proposition 6, and the rare-event and tilted decay estimates used in the paper. Theorem 3 supplies a general discrepancy bound for a disjoint split of a rare event Bai et al., pp. 8–9, 17–18, 21–22.
The theorem establishes that a sampler can satisfy the paper's relative-accuracy criterion while omitting less significant dominating points. It explains why a large variance caused by rare, high-weight observations need not predict poor performance at the sample sizes in this asymptotic regime. The single-point case, Theorem 5, is included when has one member; the mission takes the more general finite-mixture claim as its goal Bai et al., pp. 19–20.
The result is proved in the cited paper. The work here is to give the assumptions, mixture law, discrepancy criterion, and rate comparisons a common Lean statement that can support a machine-checked proof. Mathlib supplies measures, product measures, integrals, Euclidean geometry and filters; the paper-specific definitions and proofs remain to be formalized.
The familiar variance test can fail for a sampler that omits a dominating point: a sample from the omitted region may receive a very large likelihood ratio even though such samples are extremely unlikely under the selected tilts. Bounding the full second moment therefore does not establish the desired criterion. The formal target must keep the probability of encountering that region separate from the behavior of the estimator on the main region. The argument also needs the large-deviation rate under each tilted law, including the strict gap between selected and omitted dominating points Bai et al., pp. 20–22.
The Lean model uses laws on EuclideanSpace ℝ (Fin d) in place of random variables on an unspecified probability space; all probabilities in the paper depend only on those laws. The functions , and use extended real values, while event probabilities and discrepancy ratios use real values. The mixture uses Mathlib's exponential tilt and fixed positive weights. The output uses the paper's explicit likelihood ratio. The sample mean uses the product law on Fin n, and is fixed before the tolerance is quantified.
The finite dominating set is enumerated injectively, and is a nonempty finite set of exactly the lowest-rate indices. The definition of asymptotic efficiency requires an eventual finite second moment; Theorem 3 also requires its variance to be genuine. Its displayed bound is stated for sufficiently large , where the denominator is positive. Theorem 3 states the sample-size and variance condition supplied by its printed asymptotic-efficiency premise. These choices exclude zero tilted measures, default zero values for nonintegrable variances, and the weaker quantifier order in which a new may be chosen for each tolerance. Theorem 1's second clause, as printed, asserts under Assumption 2 alone. This fails when contains a point on the boundary of with finite rate and zero probability. An example is a Poisson variable of mean plus an independent uniform variable on , with . The milestone therefore states that clause for sets that also have a finite dominating set, which covers every use in the paper. Definitions of the rate function, dominating set, event split, and discrepancy can be reused in later formalizations of rare-event simulation.
Exchanges increasingly operate several venues side by side: a lit pool, where the limit order book is visible, and a dark pool, where orders are hidden and trades execute at the mid-price. Liquidity on both venues is supplied largely by market makers, and exchanges steer that supply through make-take fees: rebates paid to liquidity providers and fees charged to liquidity takers. How to set such fees is a principal–agent problem. The exchange (principal) designs a remuneration contract; the market maker (agent) chooses which volumes to post where, given the contract.
B. Baldacci, I. Manziuk, T. Mastrolia and M. Rosenbaum (arXiv:1912.01129, published in Operations Research in 2023) model this situation for one market maker quoting on a lit and a dark pool of the same exchange. The approach follows the contract-theoretic treatment of make-take fees by El Euch, Mastrolia, Rosenbaum and Touzi (arXiv:1805.01145), in which the exchange's problem reduces to a Hamilton–Jacobi–Bellman (HJB) equation once the market maker's best response is substituted. In the present model the inventory lives on a finite grid and the reduced equation is a finite system of backward ordinary differential equations whose right-hand side is a supremum over incentives. The paper's main theorem asserts that this system is well posed; its numerical sections then solve it with deep reinforcement learning.
Time runs over with . The market maker posts volumes on side (ask, bid) of pool , taken from finite sets containing . The inventory is an integer between the risk limits and ; volumes are admissible at when and . Write , .
Market orders arrive with intensities driven by the lit-pool imbalances , (both when nothing is posted in the lit pool):
where is for and for . A fill of size on side of pool has intensity and moves the inventory to . A dark fill is executed at the mid-price, or at half a tick from it under latency , the latency states being weighted by . Fills carry market impact .
The exchange offers jump incentives and a price-risk incentive . The market maker's Hamiltonian (4.10) is
with risk aversion , and a best response maximizes it over admissible volumes. The exchange, with risk aversion and fees , faces
where is the market maker's certainty-equivalent gain from the fill, and .
For every best-response selection , the system
has a continuous viscosity solution, and any two continuous viscosity solutions coincide on . No growth, sign or regularity condition is imposed on the competitors.
Where , the supremum of over is attained, uniquely, at
Well-posedness of (4.15) is what licenses the rest of the paper: the reduced value is identified with the exchange's optimal utility, the optimal make-take incentives are read off the supremum in (4.15), and the neural-network scheme of §5 approximates a well-defined object. Without uniqueness, a numerical solution of (4.15) need not be the value of the design problem.
The well-posedness assertion is justified in the paper by a single citation to lecture notes on stochastic control; no argument specific to this Hamiltonian is printed. A machine-checked proof makes explicit which properties of the citation requires and that they hold here: finiteness, convexity and local Lipschitz continuity on the negative cone, and invariance of that cone under the backward flow. The result has not been formalized before; the platform has no market-making or make-take-fee model, and no viscosity notion for finite systems of backward ODEs.
is a supremum over an unbounded set of incentives and is as soon as a relevant component of is nonnegative, so the standard Lipschitz ODE theory does not apply directly. The best response is an argmax over a finite set and may jump in , so is not continuous in the incentives. Global existence requires that solutions neither reach the region where nor blow up before time . Uniqueness is claimed among all continuous viscosity solutions, not only negative ones, so a competitor must first be shown to stay in the region where is finite. Finally, viscosity solutions must be related to classical ones for a system whose coupling is nonlocal in the inventory.
Everything lives in the namespace MMDarkPool.Exchange. One definition item, Model, holds the parameters and the standing assumptions (Standing: ; ; ; ), the grid, admissible volumes, , (4.10), the best-response predicate (4.6), , , (4.16) and IsViscositySolution. Inventories are integers, cast to reals inside formulas; a solution is a function constrained on only. Jump incentives are indexed exactly by the volume sets, so the supremum ranges over .
The formalization commits to these readings, each disclosed in the items:
A real-valued supremum for (which Lean sets to on unbounded sets), a statement about an abstract convex Hamiltonian, a choice-based maximizer in place of the supremum, or one-sided tests at would each change the theorem, and are ruled out. The identity , the third sentence of Theorem 3, Theorems 1 and 2, and the numerical sections are not part of this mission: they need the stochastic model of controlled point processes, which has no substrate.
A complete development needs comparison or Picard–Lindelöf arguments for finite ODE systems with extended-real right-hand sides, and the passage from viscosity to classical solutions for time-only equations; both are reusable beyond this mission. Contributions of such lemmas as separate theorems are welcome.
Testing makes an infected person less likely to pass an infection to someone else. In a society whose contacts depend on voluntary social activity, that direct benefit changes behavior: an agent who expects fewer infections may choose more contacts. The central question is whether the added contacts can outweigh the direct benefit of testing in equilibrium. Acemoglu, Makhdoumi, Malekian, and Ozdaglar study this question in a finite random network with two values for social interaction NBER Working Paper 27483. The paper later appeared in Operations Research in 2024; the mathematical statements in this mission follow the July 2020 NBER working paper, whose numbering and page locations are used throughout.
The effect matters when testing policy and voluntary distancing operate together. A prediction made with fixed contact patterns can have the opposite direction from a prediction made after agents adjust their activity. The result targets this difference directly: in two policy regions the equilibrium infection probability of the agents who mix between activity and inactivity rises with more testing, even though infection probability at a fixed activity profile falls NBER Working Paper 27483, Proposition 1 and Theorem 1.
There are agents. Agent chooses an activity , valued at either or , where . A fixed fraction of agents is designated high value. Conditional on the activities, each unordered pair forms a contact independently with probability , with . One agent is chosen uniformly as the initial infection source. Each infected agent is tested with a probability determined by her type: for low value and for high value. Untested agents transmit across each contact with probability ; tested agents transmit with probability , where NBER Working Paper 27483, Section 2.
Write for the chance that infection reaches on a fixed contact graph , after averaging over the source, testing, and transmissions. Averaging again over the random graph formed by an activity profile gives . These are distinct probabilities: the first holds contacts fixed and the second includes how activity changes the contact network. An agent's utility is
where and is her type's testing probability. A symmetric equilibrium assigns one activity distribution to each type and permits no agent to gain by choosing any other activity in NBER Working Paper 27483, equation (1) and Definition 3.
The testing square is partitioned, with shared boundaries, into four regions by comparisons of infection probabilities at all-active and partially active profiles with the thresholds and . In both types are active. In high-value agents are active and low-value agents mix. In only high-value agents are active. In high-value agents mix and low-value agents are inactive NBER Working Paper 27483, Section 3.1 and Proposition 2.
The goal is the finite-population comparative statics in Theorem 1. For sufficiently large , compare coordinatewise ordered policies in the interior of the same region, and their symmetric equilibria. The target includes existence of an equilibrium for every policy. In the two pure-activity regions, infection weakly falls:
In the mixing regions, the mixing type's infection probability rises. For , the increase is strict for distinct ordered policies; for , it is strict when the high-type testing probability increases. The inactive low-value agents in have infection probability at both policies:
The target also includes the theorem's closing sentence: at policies on the boundaries of the four regions, equilibrium infection probabilities are continuous in the policy.
The milestone list follows the paper's activity monotonicity and concavity result, fixed-network testing result, endpoint best responses, four-region equilibrium characterization, and the mixing indifference equations (9) and (10) NBER Working Paper 27483, Lemmas 1–2, Propositions 1–2, Theorem 1.
The theorem gives a precise setting in which the direct effect of testing and the equilibrium effect of changed contacts have different signs. It distinguishes the regions where everyone or no one of a type changes activity from the regions where a type mixes. Thus a policy comparison can specify whose infection probability rises, falls, or stays at the source-infection floor , rather than claiming one direction for every agent and policy NBER Working Paper 27483, Theorem 1.
The paper presents proofs of these claims, but this mission's Lean theorems remain open. A completed formalization would provide a reusable finite independent-cascade model with shared testing coins, a random activity-dependent contact network, and equilibrium predicates that compare against all unilateral activities. Those definitions can support later work on intervention and network-formation games. The formalization also makes the finite-population qualifications explicit, including the signs of the mixing-type infection identities.
Testing monotonicity on a fixed network does not settle the equilibrium comparison, because the contact graph's law changes when agents change activity. The difficult step is the uniform, large-population equilibrium characterization in Proposition 2: the paper needs a single threshold that works across all policies and keeps the two types' incentives separated. Its proof asserts a bound on the effect of one agent's choice on another's infection probability for large without a quantitative derivation NBER Working Paper 27483, proof of Proposition 2. This is a substantive open proof obligation for solvers, not a condition assumed in the theorem.
Lean uses Fin n for agents and SimpleGraph (Fin n) for undirected contacts. All probabilities are finite sums of Bernoulli weights. A single testing coin per agent is shared by that agent's outgoing transmission arcs; ordered arcs have independent transmission coins. Infection means reflexive reachability from the uniformly selected source in the resulting live-arc graph, so even an isolated inactive agent can be infected as the source. The activity-dependent graph draws one coin per unordered pair. This is the paper's stochastic process in finite form NBER Working Paper 27483, Section 2 and proof of Proposition 1.
The high-value agents are the first members of Fin n. Policies and typewise strategies are real pairs ordered low then high. Symmetric mixed strategies are independent Bernoulli mixtures on activities , as in the proof of Proposition 2; deviations still range over every real activity in . Region interiors are taken in . The source's weak direction is used for decreases; the strict increases are restricted to policy changes that affect the mixing type. The printed high-type constancy claim in Theorem 1(b) is false in the finite model and is excluded. Two printed statements fail at degenerate inputs and are stated in corrected form. Lemma 2's claim that every best response is or fails when utility is constant in the agent's own activity, so that case is the stated exception. Proposition 2's uniqueness fails at the corner , , where low-value agents never transmit and every low-type mixing probability can be an equilibrium. That corner is excluded from parts (a)–(c) and from the continuity clause of Theorem 1. The paper's displayed formulas are corrected to , as their preceding lines require NBER Working Paper 27483, pp. 37–38.
The infection probability is defined by the cascade itself, and equilibrium is checked against every unilateral deviation. The goal includes equilibrium existence so that a universal claim over equilibria cannot hold vacuously. The definitions, finite-sum facts, and equilibrium results are welcome contributions; no closed-form infection probability is built into the model.
In a group-buying event a retailer offers a product at a discount that materializes only if enough customers sign up before a deadline. Platforms such as Taobao and JD run such events with several deal levels: the more customers join, the lower the final price. Each arriving customer must decide whether to join without knowing how many others will follow, so the sign-up decisions form a dynamic game among customers who arrive one at a time.
Much of the theory of group buying works with batch sign-ups, where all customers decide simultaneously (Anand and Aron 2003; Jing and Xie 2011), or compares simultaneous and sequential mechanisms (Hu, Shi and Wu 2013). Ming and Tunca (SSRN 3352047; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1083) model the event in continuous time with a deposit and two deal thresholds, as on Taobao. They characterize the customers' equilibrium sign-up behaviour as a function of elapsed time and the current sign-up count, and use that characterization for structural estimation on Taobao data. This mission formalizes the theoretical part: Lemma 1 and Proposition 1 of §3.
The event runs on a time window , . Customers arrive according to a Poisson process with rate . Each customer has unit demand and a reservation utility drawn from a probability law on with c.d.f. ; the outside option is worth .
A customer who joins pays a non-refundable deposit . The platform fixes two sign-up thresholds , natural numbers with . The retailer announces a base price and a deal discount , which give the deal prices
If the total number of sign-ups by time is below the price is , if it is , and if it is . After the event, a customer who joined either pays the balance or walks away and loses the deposit, so his surplus is .
A customer arriving at time sees the number of earlier sign-ups. Write for the probability that only the first deal happens, and for the probability that the second deal happens, given sign-ups on . Joining moves the count to , so the expected utility of signing up is
The customer signs up if and only if , and the sign-up probability is (2).
Conditioning on the arrival time of the next customer, which is exponential with rate , gives the conditioning equations: for ,
and the same equation (5) for when . The boundary conditions are , for , and for . A dynamic consumer equilibrium is a family of -valued measurable functions satisfying (2), (4), (5) and these boundary conditions on .
For and :
Proposition 1 turns an equilibrium of a continuous-time game, defined implicitly by the conditioning equations, into a backward recursion over the sign-up count that can be computed. The structural estimation of §4 uses this recursion: the likelihood of the observed sign-up times is built from the equilibrium intensities , so without the proposition the estimator has no well-defined object. The threshold structure of Lemma 1 also underlies the paper's discussion of drop-outs after the event.
The result is proved on paper; nothing in this model has been formalized. The paper's proof differentiates (4) without stating any regularity of or , and leaves implicit the facts that the beliefs stay in the probability simplex along the induction and that is measurable in . A machine-checked proof settles these points. Printed slips in (6) and (A.14) are corrected in the statements (see Formalization scope).
The obvious argument is the paper's: differentiate (4), solve the resulting linear ODE with an integrating factor, and induct backwards from . This argument assumes that is differentiable, which is not known a priori. Only measurability and boundedness are available, so the equivalence of (4) and (6) has to be proved at the level of integral equations: uniqueness through a Volterra-type estimate for bounded measurable solutions, and existence by checking that the closed form solves (4). The induction also has to carry two invariants that the paper does not mention. The beliefs must stay in the simplex so that Lemma 1 applies at the next step, and must be measurable so that the integrals in (4)–(6) mean anything. Lemma 1 itself is a three-branch case analysis with divisions by and .
Everything lives in the namespace GroupBuyEq.Signup; one definitions file, GroupBuyEq.Signup.Model, holds the objects.
Params holds , (lam), , , and . are derived. Standing bundles , , , , and . and are implicit on the page.NullSingletonClass). This is weaker than the paper's density assumption. is Mathlib's ProbabilityTheory.cdf μ.Not trivializations. The equilibrium is not defined by (6), which would make existence definitional, and is not defined by (7), which would bypass Lemma 1: is the -measure of .
A complete development needs:
The equivalence (4) ⇔ (6) is a generic statement about linear integral equations with an exponential kernel and is reusable beyond this mission. Contributions to any milestone are welcome.
A decision maker often receives several probability forecasts for the same binary event. The forecasters may have overlapping information, so averaging their numbers can count shared evidence more than once. Lichtendahl, Grushka-Cockayne, Jose and Winkler study the probability of the event conditional on the forecasts themselves. Their generalized probit ensemble gives this conditional probability for jointly normal information states and a broad class of response curves. It lets the information states have a general covariance matrix, which records how much information the experts share.
The question is operational: given the experts' reported probabilities, what probability should the decision maker report? Under a proper scoring rule, the conditional event probability is the optimal report. The paper first develops ensembles based on conjugate prior and likelihood pairs, then treats the normal information-state model in Proposition 4. This mission concerns that latter result, using the preprint's §3 and Appendix rather than the published article's pagination.
There are experts. Their information states form a jointly normal vector with mean and covariance matrix . The event is . A generalized linear model specifies the probability of that event after all information states are known:
Here is the cumulative distribution function of a continuous, full-support real random variable . Expert reports the conditional probability . The prior-predictive probability is , and the Bayesian aggregate is . None of these probabilities is defined by the closed formula to be proved.
Write for the distribution function of the sum of independent and , where is standard normal. The paper gives its variance parameters and in terms of and , and weights in terms of the correlations . The inverse distribution function in Proposition 4 is evaluated only at probabilities arising from the model.
Lemma 1 identifies the normal law of the full linear predictor and the conditional normal law of the predictor excluding expert , given . Equation (14) identifies an expectation of the link function under a normal law with . The proof of Proposition 4 then identifies the weights, each expert's report, and the prior-predictive probability. The five milestones are the two Gaussian laws, equation (14), the report formula, and the prior-predictive formula; the weight chain is a supporting theorem item.
The target is the paper's formula for the Bayesian aggregate, including its stated formulas for and :
The corresponding parameters are , , , and . The two other conclusions are and .
Proposition 4 expresses a forecast based on all reports using only the reports, a prior probability, the link distribution, and coefficients determined by the information-state covariance. It allows the decision maker to account for correlated expert information without reconstructing each expert's private sample. The result also states that an expert's report is calibrated under the model: if only that report is heard, its conditional event probability is the reported number.
The result is proved in the paper. The remaining task here is a machine-checked proof of the conditional Gaussian, integral, inversion, and conditioning identities behind the displayed ensemble. The formal definitions of the forecast as a conditional probability and the covariance-derived coefficients can be reused when comparing other forecast aggregation rules. No proof of Proposition 4 is claimed by this proposal; the Lean theorem is an open target.
The report is itself a conditional probability, while the aggregate conditions on the vector of these reports. Replacing either by its expected closed form at the outset would erase the central claim. A proof must instead connect the Gaussian conditional law of the unobserved states to each report, and then relate conditioning on the reports to conditioning on the full state. The inverse cdf also requires care: its real-valued representation is meaningful at probabilities strictly between zero and one, and its value outside that interval has no role in the paper's formula.
Experts are indexed by Fin k; the formulas do not require , although §2.2 discusses at least two experts. The information state is EuclideanSpace ℝ (Fin k), and its law is Mathlib's multivariate Gaussian with a positive semidefinite covariance matrix. A probability measure represents ; absolute continuity and positive measure for every nonempty open interval express the paper's continuous, entire-real-line support assumption. The cdf of is the cdf of the convolution of with a centered normal law. A generalized inverse uses the infimum of its upper level set; it is used only on the probability range .
Three nondegeneracy assumptions are stated explicitly: , , and for each expert. They make the paper's inverses, correlations, and denominators meaningful. Positive semidefiniteness gives , so conversion to Mathlib's nonnegative variance type does not clip them. The location-scale statement fixes as its standard member, with location zero and scale one.
The event is measurable, the information-state map is measurable, and its law and conditional event probability are model hypotheses. Reports and aggregate are conditional expectations of the event indicator, with identities stated almost surely because conditional probabilities are only determined up to null sets. The proposal never defines reports or the aggregate by their claimed closed formulas. Contributions may develop general Gaussian pushforward and conditional-law results, cdf convolution identities, and measure-theoretic results about conditioning on transformed reports.
Auctions in which bidders face budget constraints do not fit the classical quasi-linear theory: a bidder cannot pay more than a fixed amount, however much the goods are worth to him. For a single divisible good, Dobzinski, Lavi and Nisan showed that the adaptive clinching auction of Ausubel is incentive compatible, individually rational and Pareto optimal, and that with two bidders it is the only such mechanism (Dobzinski–Lavi–Nisan 2012). Goel, Mirrokni and Paes Leme extended clinching to supply constraints described by a polymatroid, the polyhedral clinching auction (Goel–Mirrokni–Paes Leme 2015), which covers sponsored-search and matching-type markets.
These results are one-sided: a single auctioneer sells and keeps the revenue. In markets with many sellers, such as advertising exchanges or electricity markets, sellers have their own valuations and the mechanism must also make them better off and pass payments through. For non-budgeted bilateral trade, the Myerson–Satterthwaite theorem rules out efficiency together with incentive compatibility, individual rationality and budget balance (Myerson–Satterthwaite 1983), so a positive result needs a weaker efficiency notion and sellers that report truthfully.
Timeline:
The market is a bipartite graph : buyers , sellers , and edges ; means that buyer wants the goods of seller . Write and for the edges at buyer and at seller . The goods are divisible and homogeneous.
Buyer has a valuation , a bid and a budget , all nonnegative reals. Seller has a reserve price , which he reports truthfully, and a monotone submodular function on the subsets of : , is monotone, and . The value bounds the goods transacted through , and is seller 's stock. The polymatroid of is .
An allocation is a triple of transactions , payments and revenues with for every seller and for every buyer. A mechanism maps the public information (graph, bids, budgets, reserve prices, the ) to an allocation; it does not see the true valuations. The utilities are
The five properties are: (ICb) truthful bidding is a dominant strategy for buyers; (IRb) truthful buyers get nonnegative utility; (IRs) each seller ends with utility at least ; (SBB) ; (PO) under truthful bids, no allocation with makes everyone weakly better off and someone strictly.
for every market and clock step , on inputs whose bids, reserve prices and true valuations are multiples of (Assumption 3.2).
The witness is Mechanism 2: add a virtual buyer with infinite budget and bid for each seller, run the two-sided clinching auction (Algorithm 2), and subtract the virtual buyers' payments from the revenues. The milestones follow the paper's argument:
The theorem shows that the impossibility for two-sided trade disappears when efficiency is weakened to Pareto optimality and sellers report truthfully, even with budgets and with polymatroidal transaction constraints on each seller. Mechanism 2 is implementable: each clinching step reduces to a polymatroid greedy computation (Theorem 3.6). The polymatroid layer covers matching-type markets and sellers with structured supplies.
The result is proved in the paper; no machine-checked proof of it or of the polyhedral clinching auction is known. The mission produces a formal model of budgeted two-sided markets, of ascending clock auctions as relations on runs, and of the clinching polytopes, together with the statements of the paper's main steps. Formal proofs of any milestone are welcome, including the one-sided theorem of Goel et al. (Theorem 3.3) on its own.
The obvious route, running the one-sided polyhedral clinching auction on the aggregated polymatroid , gives the buyers' quantities and payments but not who buys from whom, and not the sellers' revenues; nothing in the one-sided analysis protects a seller from selling below his reserve price. The paper's Mechanism 2 clinches edge by edge, and the central step is Theorem 3.9: a buyer's sequential edge-wise clinch in the two-sided market coincides in total with his simultaneous clinch in the reduced market, for every choice of maximal clinching vector. This needs a polymatroidal network-flow description of the remnant supply and a careful invariant on the minimizers of the associated submodular functions (§5.2). Pareto optimality requires, in addition, tracking the sellers' utilities through the virtual buyers.
Buyers are Fin n, sellers Fin m, edges a Finset (Fin n × Fin m); transactions are functions on the edges in E. All indices are 0-based. Budgets and demands that can be infinite live in WithTop ℝ; buyer utility lives in WithBot ℝ and is only compared. The properties are imposed on the inputs of Assumption 3.2 (p. 10): bids, reserve prices (the virtual buyers' bids) and true valuations are nonnegative integer multiples of ; budgets and the are unrestricted apart from the standing assumptions.
Algorithms 1 and 2 are relations: a run is a finite sequence of states, one per while-iteration, ending at the first state where all demands are , and results are stated for every run. The demand of a buyer whose clock is still and below his bid is (line 1 and Table 1, p. 16). Line 13 of Algorithm 2 updates the demand of the buyer whose clock was just increased. The polynomial-time clauses of Theorem 3.6 are not formalized.
A mechanism that reads the true valuations, a (PO) whose competitors need not be allocations, or a mechanism that is not required to output allocations would make the goal trivial; the definitions exclude all three.
Mechanism 1 (polymatroidal network flow, Theorem 3.5) and the deeper lemmas of §5 are not stated. Reusable parts: the polymatroid definitions and the one-sided Algorithm 1, stated for an arbitrary feasible set.
In most organizations the person who decides is not the person who carries the decision out. A board ratifies a product and engineers build it; a studio approves a film and a director makes it. The implementer usually also knows more, or can learn more, about which course of action will work. A long literature in organizational economics asks whether such an organization should be staffed with people who share the decision maker's preferences or with people who disagree with her: Aghion and Tirole (1997) on formal and real authority, Dessein (2002) on communication, Van den Steen (2010) on homogeneity, and Landier, Sraer and Thesmar (2009) on "optimal dissent" between a decision maker and an implementer.
Itoh and Morita add endogenous information acquisition to the decision–implementation setting of Landier et al. The implementer chooses how much effort to spend learning which project is efficient, and that choice responds to whether his preferences agree with the decision maker's. Their main result (Proposition 2) says when the principal, who only cares about success, should prefer a heterogeneous organization (one where the two agents disagree) to a homogeneous one.
A principal employs a decision maker (DM) and an implementer (IM). There are two projects and two equally likely states ; project is efficient iff . A project succeeds iff it is efficient and IM exerts implementation effort, which costs him a random with CDF and density , where , is strictly increasing on and . Success is worth to the principal.
On success, DM receives from her favourite project 1 and from project 2. IM receives from his favourite project and from the other. The organization is homogeneous if IM's favourite is project 1 and heterogeneous if it is project 2. Write and for the two biases.
Before the project is chosen, IM picks information effort at cost , . With probability he observes a signal that points to the efficient project with probability ; otherwise . The signal is public. The posterior that project is efficient is after , after , and after .
Moves are solved backwards:
Three thresholds in appear: , and , the solutions of
DM follows a signal for project 2 iff (homogeneous) or (heterogeneous). Let , and let be the least at which IM's optimal effort in organization reaches .
The paper's assumptions are:
Under Assumptions 1–3:
and for there is with
strictly for . The threshold is existential, not a formula.
In attack order:
The result. Proposition 2 identifies a channel through which disagreement between a decision maker and an implementer raises an organization's success probability: the implementer, anticipating that without information the decision maker will pick his unfavourite project, invests more in information (the paper's "ignorance-avoiding effect"). Against this, a heterogeneous implementer is less willing to execute the decision maker's default. The proposition says exactly when each force wins: never for weak signals, and above a cost threshold for informative ones. Corollary 1 and the comparative statics of Proposition 3 build on it.
Formalizing it. The result is proved in the paper; this mission formalizes the statement from the primitives (DM's argmax, IM's maximizer, success probability) rather than from the closed forms, and then the paper's chain of lemmas. Two of the paper's arguments need repair along the way: the proofs of Lemmas A2 and A3 claim the payoff difference is increasing in , which fails once the heterogeneous effort saturates at , although the lemma statements remain true. No part of this model is formalized elsewhere.
The comparison is between two maximizers of different concave programs, each built on a different branch of DM's decision rule, so the obvious argument of differentiating in has to handle kinks: the efforts are and saturate at different , and DM's choice switches at different . The single-crossing property in (one sign change of ) is not monotonicity of the difference on the whole half-line; on the interval where only the heterogeneous effort is saturated the difference is not increasing, and the sign has to be read off directly. For DM reacts in one organization and not the other, and the positivity of the relevant brackets rests on the definition of and on Assumption 3.
All quantities are real. The model is one definition file, OrgDiversity.Optimal.Model:
Standing makes this precise by requiring to be integrable on every and for . The formalization also assumes is continuous on and on .is never defined by its closed form, and optimal efforts are arbitrary maximizers of IM's payoff on , not the formula ; stating the goal about the closed forms would reduce it to elementary inequalities and is ruled out.
Contributions of any milestone are welcome; the convexity lemma for and the maximizer of a concave quadratic on are reusable beyond this mission. Corollary 1, Proposition 3, §4 and the cheap-talk extension of §5 are not part of this mission.
The Bass model describes how a new product spreads when consumers can adopt through external exposure and through contact with previous adopters. A homogeneous model assigns the same response rates to everyone. Actual networks can have consumers who respond at different rates, even when the average rate is known. For a fixed average, it is therefore useful to know whether replacing the individual rates by that average changes the expected adoption curve. Fibich and Golan study this question for a stochastic, individual-level Bass model on weighted networks Fibich and Golan, 2022.
This mission concerns heterogeneity in the external influence rates on a complete network. The paper's Theorem 3 says that, with a common total internal influence rate, heterogeneity strictly reduces the expected adopted fraction at every positive finite time. The result distinguishes the expected behavior of the individual-level process from a calculation made using only average external influence.
There are consumers, indexed by . Each is either a nonadopter or an adopter. Everyone is a nonadopter at time zero, and adoption is permanent. A nonadopter adopts at rate
where is the current set of adopters, is the external influence rate, and is the influence of adopter on . The rates are nonnegative. Thus the adopter set is a finite continuous-time Markov chain: it can move from to , for , at precisely the rate above. This is equation (5) of the pinned preprint, p. 5.
Write for the number of adopters at time . The paper studies the expected adoption fraction , equations (10)–(11) on p. 5. In this development, is evaluated from the transition matrix of the adopter-set generator . Its initial state is the empty adopter set.
On a complete network, let be the total incoming influence on consumer . The mild-heterogeneity convention divides it equally among the other consumers: when . The target case has a common . The homogeneous comparison network has the same and , and external rate at every node. These are the paper's equations (9), (12), and (34)–(35) on pp. 5–6 and 11.
For nonnegative that are not all equal, a common , and every , the goal is the strict comparison
This is Theorem 3, p. 11. Its conclusion is about the original adopter-set process, not about a substitute curve defined from a comparison theorem. In particular, no ordering of the is imposed on the goal.
If is the time between adoption and adoption , its CDF is . Lemma 5, p. 11 compares these CDFs on a complete graph when the external and total incoming influence rates are ordered together. It gives equality for and a strict heterogeneous-versus-homogeneous comparison for every later at positive .
Let be the time of adoption . Equation (60) in Appendix D, p. 26 compares adoption times of auxiliary, independently coupled waiting-time sequences. It does not compare the actual dependent adoption times in the heterogeneous network, so it is not a milestone here. Equations (32) and (61) identify adoption-time probabilities with the generator process and its expected count pp. 10 and 26. A separate milestone records Lemma 4, p. 11, the two-consumer case.
The strict inequality says that replacing unequal external adoption rates by their mean overstates the expected adopted fraction at every positive time, under the paper's complete-network and homogeneous-internal-influence assumptions. It supplies a precise direction for the bias caused by a homogeneous approximation. It does not assert a comparison for each individual consumer or for arbitrary network topology.
The theorem is stated in the cited paper, but its printed proof invokes Lemma 6, which claims independence of inter-adoption times. That claim fails for heterogeneous networks with three or more consumers. For , , and , the covariance of the second and third inter-adoption times is by exact rational calculation. The paper's printed argument therefore does not establish the required adoption-time dominance. This mission does not attribute that missing comparison to equation (60). Neither Theorem 3 nor the included milestones have a machine-checked proof here yet. A complete formalization would settle the theorem through a valid argument about the actual dependent adoption times.
The total rate after an adoption depends on which consumer adopted. Consequently, the adopter count alone does not generally form a Markov chain, and successive inter-adoption times need not be independent. Comparing the marginal CDF of each holding time does not by itself compare the sum of those times. This is exactly where the paper's argument becomes incomplete: its independence claim cannot carry the comparison from Lemma 5 to the adoption times needed for Theorem 3. The missing step is a strict comparison between mixtures of waiting-time sums over possible adoption orders.
Consumers are Fin M; adopter states are finite subsets. The Lean model uses real-valued nonnegative rates, a generator with jumps that add exactly one nonadopter, and the matrix exponential for transitions. The expected fraction is the weighted sum of transition probabilities from the empty set, divided by . A reusable finite-state jump-generator definition is separate from the paper-specific adoption rates. Complete-network weights use real division by and have zero diagonal. The goal's heterogeneity assumption implies , so that denominator is nonzero.
For the distribution milestones, an adoption order is a permutation, and a stage is numbered from zero in Lean: Lean stage corresponds to the paper's and . Each order has its jump-chain weight; conditional holding times use independent exponential measures with the corresponding positive stage rates. The stage rates appear in denominators and exponential measures, so the general generator-to-jump-chain milestone states positivity explicitly. It also carries the paper's standing assumption (7) that each consumer has positive total incoming peer influence; accordingly its network has at least two consumers. The paper's in remains one-based.
The paper does not define “heterogeneous in ” formally; Lean reads it as the existence of two unequal . Nonnegative are included because they are adoption rates. Lemma 5 additionally requires a positive initial total rate and some variation in or for its strict conclusion. The model uses the generator-defined throughout: replacing it with a sum of adoption-time CDFs in the goal would erase the bridge the mission asks solvers to establish. Contributions on finite-chain laws, jump-chain representations, strict distribution comparisons, and the two-consumer calculation all serve the listed targets.
A household can borrow against expected future income only while repayment remains preferable to default. In the baseline model of Choi, Koo, Lim and Yoo, this choice is imposed through a participation condition at every date: the household's remaining utility from its planned consumption must be at least its remaining utility after default. The constraint changes the borrowing limit from the present value of income to a smaller level that depends on the default penalty. Determining that level is useful for understanding which debts are sustainable when income fluctuates and contracts cannot force repayment. The paper gives a closed form for the limit and for optimal financial wealth in its baseline continuous-time model (Proposition 3.2, p. 11).
The result is known mathematically: it is stated and proved by the authors, with the proofs placed in an Online Appendix. This mission targets a machine-checked formalization of the baseline result. It also identifies smaller claims about the constants and the optimal multiplier that are useful independently of the stochastic verification theorem.
The household receives income with initial level . Its growth is a geometric Brownian motion driven by two independent standard Brownian motions and . The first is the source of risk priced by the traded stock; the second is the remaining income risk, which the paper assumes can be hedged. The state-price density prices future consumption. In the formal model both processes are given explicitly:
where . The rate gives the present-value benchmark for income. These are the paper's mortality-adjusted , , and discount rate ; the mortality intensity has already been absorbed into them (§2.1, pp. 4–6 of the preprint).
For risk aversion , , utility is . A consumption plan is a positive process measurable as information arrives. It is feasible from wealth when its discounted net cost satisfies and, at every , it meets the conditional participation constraint
Here is the information generated by the two Brownian motions through time , and is consumption after default. A larger means a less severe default penalty. The paper restricts and defines from its other parameters in (2.7) (pp. 6–7 of the preprint).
The endogenous credit-limit coefficient is
where , , and the positive quadratic root have exactly the formulas in (2.7) and Proposition 3.1. The first targets establish , , and . Proposition 3.4 then gives the dependence on the default fraction:
The central target is Proposition 3.2. For , the candidate consumption plan is feasible and maximizes expected utility among all feasible plans. Its optimal wealth , defined as the conditional present value of future net consumption, satisfies the closed form (3.10) and the bound
For , the feasible set is empty: the household defaults immediately. On the way, the mission states the two duality results of §3.1 that the paper's argument rests on. With a Lagrange multiplier for the budget and a non-decreasing shadow-price process , , for the participation constraints, the dual objective (3.4) is minimized by the running maximum
(Proposition 3.1, for multipliers with ), and the primal value satisfies the duality relation (Theorem 3.1). The algebraic milestones also identify the binding level and the unique admissible initial multiplier solving Proposition 3.3's equation. These targets follow §§3.1–3.2, pp. 8–12 of the preprint.
The coefficient turns a family of conditional participation conditions into a usable state-dependent debt bound. Its comparison with quantifies the difference between a limit based on priced income alone and one that lenders can sustain when the household can default. Proposition 3.4 states precisely how that bound shrinks as default becomes more attractive; at it reaches zero. The wealth formula also says where the optimal policy sits relative to the boundary at every time, rather than only at the initial date (Propositions 3.2 and 3.4 of the preprint).
Formalizing the result supplies reusable definitions for a continuous-time consumption problem with conditional participation constraints and a stochastic income stream. The constants, multiplier equation, and binding-level facts are separate theorem targets; the final theorem must additionally verify feasibility, optimality, and the conditional wealth identity. The present proposal contains open Lean statements, not verified Lean proofs.
The natural-limit calculation prices future income, but it does not establish an incentive-compatible borrowing limit: a plan can meet its time-zero budget and still violate participation at a later date. The candidate shadow price depends on the running maximum of an income-adjusted dual process, so the wealth identity involves an infinite-horizon conditional expectation of a path-dependent consumption process. The same candidate must satisfy every conditional participation condition and outperform every feasible plan. Checking only the closed formula for or defining wealth by the right side of (3.10) would leave these claims unproved. The paper places its detailed proofs in an Online Appendix unavailable with the pinned preprint.
Lean uses time , real-valued wealth and utility, and a natural uncompleted filtration generated by two Brownian coordinates. Infinite time integrals are over the real interval . Each participation condition holds almost surely for each fixed , matching conditional expectations' almost-sure meaning. The running maximum defining the shadow price ranges over ; continuous Brownian paths make that range compact. Its initial value is zero almost surely, as is the Brownian starting value, and it is nonnegative on every path. The optimization statement uses a greatest element of the feasible utility values, avoiding a real supremum with a default value on an empty or unbounded set.
The printed Problem 2.2 mentions a default time but does not define it. The formalization uses the static martingale budget that §3 prices in its Lagrangian; it represents consumption rather than the stock and futures positions. This is the form of the problem for which the goal states optimality. Plans carry the integrability needed for their budget, utility, and conditional expectations. The source leaves and a positive leading coefficient of the quadratic unstated; both are explicit because the reservation value and closed-form real powers otherwise become ill posed. Plans are strictly positive, so that utility is never evaluated at zero. The dual value is not defined as a real infimum: the duality relation is stated with least elements of the explicit set of values of the dual objective, and the integrability conditions (3.2) on shadow prices are genuine finiteness requirements, never default values. The optimal-stopping representation of the dual (Lemma 3.1) is not formalized. The initial multiplier is restricted to , the branch that makes the shadow price start at zero. The endpoint appears only in the comparative-statics result for , whose formula remains defined there.
The shared Brownian and Euclidean-state definitions are reused from the platform. The new model, candidate process, real-power calculus, conditional integrability, and stochastic verification are available as distinct contributions. The goal cannot be discharged by assuming optimality or by defining to equal (3.10): it identifies wealth through a conditional present value and proves the displayed formula separately.
In the rough Heston model of El Euch and Rosenbaum, the variance of an asset is driven by a fractional kernel with Hurst exponent , which matches the roughness observed in realized volatility. The model keeps one feature of the classical Heston model: the characteristic function of the log-price is explicit up to the solution of a deterministic equation, here a fractional Riccati equation
with complex coefficients that depend on the Fourier variable (El Euch–Rosenbaum 2019). Pricing a vanilla option by Fourier inversion requires this solution for many complex parameters, and the equation has no closed form. The standard numerical method, the fractional Adams scheme, is slow because of the memory of the fractional derivative.
Callegaro, Grasselli and Pagès (arXiv:1805.12587v4) observe that with zero initial condition the solution is a fractional power series whose coefficients obey an explicit convolution recursion. The series can be summed very fast, but only on its interval of convergence; beyond it they switch to a hybrid numerical scheme. Where the switch happens is governed by the convergence radius, and their Theorem 3.3 bounds it explicitly from below and, for parameters of equal sign, from above.
Fix and . Identifying the coefficients of the series in the Riccati equation yields the coefficient recursion (3.19)–(3.20):
where is the discrete convolution (so ). Each depends on only, so the sequence is uniquely determined; in Lean it is coeff α lam mu nu : ℕ → ℂ.
The convergence radius of is given by Hadamard's formula (3.21):
in Lean radius α (coeff α lam mu nu). With , and the Beta function , the paper introduces the constants
For :
In attack order: the Riemann-sum Lemma A.1 (A.39); Kershaw's Gamma-ratio inequalities (A.41); the coefficient upper bounds of (B.49) for and (B.51) for ; Proposition B.1 (a) (for the even coefficients vanish and solves (B.50)) and (b) (comparison ); Theorem 3.3 (c) (sign symmetry ); the lower-bound propagation of §B.1.2 (); the Riemann-sum bound (B.52) with ; and the lower-bound propagation of §B.2.2 ().
The lower bound is an explicit, parameter-dependent time up to which the series converges absolutely: on the Riccati solution, and with it the rough Heston characteristic function, can be evaluated by summing a series with no discretization error. The upper bound shows that for parameters of equal sign the radius is finite and of order , which is why the paper's hybrid scheme (series near , a numerical scheme beyond) is needed for long maturities. The two bounds together fix the scale on which the hybrid scheme switches methods.
The result is proved in the paper (Appendix B). The proof has not been machine-checked. A formal development adds a checked convergence guarantee for a recursion used in option-pricing code, and its auxiliary results (Kershaw's inequality for the Gamma function, which the pinned Mathlib does not contain, and Riemann-sum bounds for symmetric monotone functions) are reusable outside this paper. The paper prints a strict inequality ; its proof gives , which is what the goal asks. Upgrading to the strict inequality would be a sharpening beyond the paper.
The obvious approach is to bound by a geometric sequence and propagate the bound by induction through the recursion. It fails: the convolution contributes a factor that the Gamma ratio absorbs only when , and then with constants that are far from sharp. The propagated bound therefore needs a polynomial correction . That turns the convolution into a Riemann sum of , which is convex for and concave for , and controlling it takes a non-asymptotic Gamma-ratio inequality valid for every rather than Stirling asymptotics. For the upper bound on the radius, the coefficients must be bounded from below, which requires positivity, the vanishing of the even coefficients when , and a separate comparison between the cases , and .
Everything is stated about the coefficient sequence and its Hadamard radius. The fractional derivative, the Riccati equation itself and the function do not appear, as in the paper, which identifies the coefficients formally. Conventions:
coeff α lam mu nu : ℕ → ℂ, with ; the convolution at index runs over (Finset.Ico 1 j). Gamma factors are Real.Gamma of real arguments, cast to ; for every argument is at least .radius α a = liminf_{k→∞} ‖a k‖₊^{-1/(α k)} in ℝ≥0∞, with for , so vanishing coefficients (all even ones when ) do not lower the radius. Real bounds enter through ENNReal.ofReal.A trivializing formalization is excluded: the radius is Hadamard's in , not a supremum of convergence points computed in (which would be on an unbounded set), and the recursion carries the paper's and conventions, so that and, at , the coefficients are those of (), with and .
A complete development needs: real-analytic Gamma-function inequalities (log-convexity is in Mathlib; Kershaw's bounds are not); Riemann-sum estimates for symmetric monotone functions on ; the Beta integral (Mathlib has Complex.betaIntegral); and manipulations of -th roots in ℝ≥0∞. The Gamma-ratio and Riemann-sum lemmas are reusable beyond this mission. Contributions to any milestone, and alternative proofs of the radius bounds, are welcome.
Not formalized: the "Moreover" sentences of Theorem 3.3 (b) (monotonicity and blow-up of the maximal Riccati solution) and (c) (convergence at the radius), the non-homogeneous Theorem 6.1, and the numerical scheme of §4–§5.
The Colonel Blotto game, introduced by Borel in 1921, is a two-player zero-sum game of resource allocation. Two players distribute their troops over several battlefields, and each battlefield is won or scored according to the troops placed there. It models allocation contests in military planning, political campaigns (budgets across swing states), advertising and security. Computing its equilibria is the basic algorithmic question about the game. The difficulty is that the number of pure strategies is exponential in the number of battlefields.
This mission formalizes the upper bound: the polynomial-size linear formulation and the facts it rests on.
An instance has battlefields, troops for player A and troops for player B, and real payoffs : player A's payoff on battlefield when A puts troops and B puts troops there. Player B receives . A pure strategy of a player with troops is an allocation of non-negative integers with . For pure strategies and , A's payoff is . Mixed strategies are probability vectors over pure strategies, and expected payoffs are the corresponding averages. A pair of mixed strategies is a Nash equilibrium when neither player gains by deviating. is the set of A's mixed strategies that occur in some Nash equilibrium.
The marginal of a mixed strategy is the vector with . The set of Nash-equilibrium marginals of A is
The layered graph of a player with troops has vertices for and . It has an edge from to whenever . A canonical path runs from to . Through prefix sums, pure strategies correspond to canonical paths, and mixed strategies to unit flows from to .
There is a constant such that, for every instance with battlefields and at most troops per player, is the projection of a linear system with
The constant is not fixed, and the statement asserts only the order of growth. Any improvement of the constants leaves it unchanged.
The result turns equilibrium computation for discrete Colonel Blotto into a single linear program of size , which an off-the-shelf solver handles. Ahmadinejad et al. instead needed the ellipsoid method with a separation oracle that is itself an exponential-size LP. The same layered-graph formulation computes A's equilibrium marginals and, through Lemma 4.5, an equilibrium strategy with polynomial support. The paper's experiments rely on it to compare the discrete game with Roberson's continuous predictions, and its §6 extends it to several resource types. The matching lower bound (Theorem 5.6, extension complexity ) concerns the same set .
On the formal side, none of these statements has been machine-checked so far. The mission produces a checked model of discrete Colonel Blotto and of the layered-graph flow representation of allocation distributions. It also produces two general results: the characterization of Nash equilibria in finite zero-sum games by maxmin and minmax strategies, and a dynamic-programming certificate for maximum-weight paths in layered graphs. Formalizing the proof also checks the printed Linear Program 1, which has a defect in one row (see Formalization scope).
The obvious description of quantifies over all pure strategies of A, and there are of them. Projecting to marginals does not remove this. Checking whether a marginal vector comes from a probability distribution over allocations is not a local condition, and the natural description in marginal space has exponentially many facets. Lifting to the layered graph fixes the membership side, but each step needs proof. Flows must encode exactly the mixed strategies (Corollary 4.4 and the decomposition of Lemma 4.5). The exponentially many payoff constraints, one per pure strategy of B, must become a polynomial dynamic programme, and the projection must be shown to equal the equilibrium set rather than a superset. That last step needs the minimax theorem. Counting variables and constraints is routine; the equivalences are the content.
Fin K). The paper's battlefield is Lean's , and the paper's flow variable sits on the Lean edge from layer to layer . Pure strategies are maps Fin K → Fin (N+1) summing to exactly . Mixed strategies are real weight functions, non-negative with sum , not measures.U k i l is A's payoff with A's troops first. B's per-battlefield payoff is , and the payoff on a battlefield depends only on the troops placed there.Naive Bayes is one of the oldest and cheapest classifiers for text and count data: given word counts for documents in two classes, it fits one multinomial distribution per class by maximum likelihood and classifies by the likelihood ratio. Its cost is a single pass over the data. In high-dimensional applications (text, genomics) one also wants the classifier to depend on few features, both for interpretability and to discard noise. Imposing that the two class distributions differ in at most coordinates turns maximum-likelihood fitting into a cardinality-constrained, nonconvex problem.
Askari, d'Aspremont and El Ghaoui (arXiv:1905.09884, Mathematics of Operations Research, 2024) show that the Lagrangian dual of this sparse problem is a one-dimensional convex problem solvable by bisection at essentially the cost of naive Bayes itself, and that its value is within a shift of four features of the true optimum. The shift comes from a duality-gap bound for separable problems in the line of Aubin and Ekeland (1976) and Ekeland and Temam, based on the Shapley–Folkman lemma.
There are features. A nonnegative data matrix with labels enters only through the class sums (the total count of each feature in each class), assumed entrywise positive. Write and .
The sparse multinomial naive Bayes problem (SMNB) at sparsity level is
where counts the coordinates in which the two class distributions differ. Without the last constraint the problem is ordinary naive Bayes.
For a vector , is the sum of its largest entries. Let
and . The relaxation (USMNB) has value
It is a convex problem in one variable. Its dual (D) is a concave maximization over with , which plays the role of a fractional feature-selection vector.
For ,
The constant four does not depend on , or the data. Numerically it is not tight (a shift of one suffices on random instances), but the goal keeps the paper's constant.
Milestones 1–6 follow the paper's proof of Theorem 3.6; milestones 7–9, on top of 1–4, are the paper's second, constructive route to the upper bound .
The theorem certifies that a convex problem of negligible cost brackets a nonconvex, combinatorial maximum-likelihood problem: the relaxation's value at lies between the true values at and . Whenever varies slowly in , which the paper observes past the "elbow" in the number of relevant features, the duality gap is small, and Propositions 3.8–3.9 turn the relaxation's solution into a sparse classifier with at most four extra features. The paper uses this to run feature selection on data sets with millions of features.
The results are proved in the paper (Theorem 3.5 is quoted from the literature). None is formalized. Formalizing them yields the perturbation-function duality-gap bound for separable nonconvex problems as a reusable statement, a verified variational formula for top- sums, and a check of a printed formula: the dual (D) as printed carries a spurious term , and the formal statement uses the corrected objective.
The lower and middle inequalities are weak duality once the dual is computed, and computing it is a separable calculation. The upper inequality is the content: it bounds a duality gap, and nothing in the one-dimensional structure of (USMNB) gives it. The naive approach, rounding the fractional of (D) to its top coordinates, has no a priori control on the loss. Both of the paper's routes need a Shapley–Folkman type argument, in which the number of nonconvex contributions is bounded by the number of constraints plus one. The Shapley–Folkman lemma itself is not in Mathlib (it is an open goal on the platform), and Theorem 3.5 also requires conjugates of extended-valued functions and the convex envelope of a sum of separable terms.
Features are indexed by Fin m, with fp fm : Fin m → ℝ entrywise positive. This positivity is stated on p. 7 and is needed because the formulas take . The standing assumption of §3.1 is carried by every statement about (SMNB). The commitments are:
EReal-valued functions on Fin d → ℝ. The conjugate is a supremum (p. 9 prints an infimum), and finiteness of each is added in Theorem 3.5 so that is a real vector.Proposition 3.8 is stated with the additional conclusion that the constructed point's value is at least the optimum of (D). Its proof establishes this, and without it the statement is met by a maximizer of and says nothing about (D).
A complete development needs Lagrangian duality for a separable problem, the perspective of , top- sums and their LP dual, Fenchel conjugates of extended-valued functions, and a Shapley–Folkman lemma. The last three are reusable well beyond this mission, and contributions there are welcome.
Unit commitment (UC) decides, period by period, which thermal generators of a power system are switched on and how much power each produces. It is solved daily by system operators and in the bidding tools of producers, usually as a mixed-integer program, and its size makes the strength of the formulation the main computational lever. A formulation whose continuous relaxation already equals the convex hull of the feasible set closes the integrality gap of each single-unit block. Such single-unit descriptions are then combined into tighter multi-unit models.
For the single-unit problem (1UC) with linear costs, several convex-hull descriptions are known. With ramping limits and a convex, nonlinear generation cost, the question is harder, because the power output is semi-continuous: either or between the minimum and maximum output. Bacci, Frangioni, Gentile and Tavlaridis-Gyparakis (Operations Research, 2024) give a formulation built on the state-space graph of a dynamic-programming algorithm for 1UC (Frangioni and Gentile, 2006), combined with perspective reformulations (Frangioni and Gentile, 2006) of the dispatch subproblems, and prove that it describes the (closed) convex hull. The paper notes that an earlier formulation claimed to have this property was later shown false by a counterexample.
A single unit is scheduled over the periods ; denotes the periods from to , empty if . Its data are:
The state-space graph has a source , a sink , and nodes , for . Its arcs are:
Formulation (26) has a flow variable on every arc subject to the flow system (18), , , where is the node–arc incidence matrix and sends one unit from to . For every it adds a private dispatch block in variables (the arc flow), for , and :
The last line is the epigraph of the perspective of the dispatch cost. Write for this constraint set and for its mixed-integer points, those with every arc variable in .
Two general objects enter the milestones. The 1-sum of and is . For a constraint map with , the support function of a set is , and the Lagrangian dual of is . denotes the closure of the convex hull.
The continuous relaxation of (26) is the closed convex hull of its own mixed-integer points, for every unit satisfying the standing assumptions and every convex cost.
The result. Theorem 1 gives an exact convex description of 1UC with minimum up and down times, initial conditions, start-up and shut-down limits, ramping limits and a convex cost. Minimizing a linear function over solves 1UC, and the single-unit blocks of a multi-unit UC model built from (26) carry no integrality gap of their own. Lemma 1 is a composition rule for mixed-integer convex sets glued along a binary variable, which the paper presents as the nonlinear analogue of a classical composition approach for polyhedra; it applies beyond unit commitment.
Formalizing it. The result is proved on paper but not machine-checked, and no part of it is formalized on the platform. A formal proof would certify the exactness claim, which matters in a literature where a published exactness claim was refuted. The paper's proof of Lemma 1 (Appendix A) assumes that a linear objective attains its minimum over a closed convex set, which is false for non-polyhedral sets; the set identity remains true, and a formal proof has to establish it without that step. The paper's remark that Lemma 1 "clearly holds in general" without hypothesis (iv) is also false, so the formal statements keep (iv).
The inclusion is routine; the content is . The obvious attempt treats each dispatch block separately and concatenates the convex combinations. This fails because the blocks share no variables with one another but all depend on the one flow vector : the convex combination that represents one block must be compatible with those representing every other block and the flow system at once. Points of with some need care too: there the perspective term is defined by continuity, the epigraph variable is unbounded above, and the closure is genuinely needed in the general lemmas. The duality route of the paper (Proposition 1 with KKT conditions) requires a strong-duality argument for every objective, which is where the printed proof has its gap.
All values are real. Periods are natural numbers , so the paper's indices are kept; the rule is written without natural-number subtraction, and the source rules are evaluated in the integers. The ambient space of (26) is finite-dimensional: arc flows indexed by the arcs of ; for each a power vector indexed by whose coordinates outside are fixed at ; and one epigraph variable. The convex hull is closed, as in the paper's own .
Committed conventions:
The mixed-integer set is defined as the relaxation intersected with binary arc variables, and the relaxation is defined directly from the constraints; neither is defined through a convex hull, so the goal cannot hold by unfolding definitions. The correspondence between – paths and feasible schedules of the paper's 3-bin model (§4, p. 14) is asserted there without proof and is not formalized: Theorem 1 is stated in the extended space of (26).
A complete development needs convex-analysis infrastructure that is reusable beyond this mission:
Contributions to any of these are welcome, as are proofs of individual milestones.