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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Many dynamic programs are solved faster after the Bellman equation has been rewritten. The Q-factor form of reinforcement learning moves the maximization inside an expectation over state-action pairs; Rust's expected value function for discrete choice models (Rust 1987) integrates out the next state before maximizing; optimal stopping problems are routinely solved through a continuation value instead of the value function. Each such transformation changes the space on which fixed-point iteration runs, often to a lower-dimensional one, and each comes with its own ad hoc argument that the transformed equation still yields optimal policies.
Ma and Stachurski (arXiv:1811.01940v2, published in Operations Research in 2021) give one abstract framework covering all of these transformations, the plan factorization, and state conditions under which a transformed Bellman equation keeps its link to optimality. The framework builds on the abstract dynamic programming of Bertsekas (Abstract Dynamic Programming, Athena Scientific, 2013), and applies to models with recursive or risk-sensitive preferences, where the standard theory does not apply directly.
A dynamic program consists of a nonempty state space , a nonempty action space , a nonempty-valued feasible correspondence with state-action pairs , a set of candidate value functions, and a state-action aggregator . The Bellman operator is .
A feasible policy is a selection satisfying a regularity condition; is the set of feasible policies. Given , is -greedy if for all . Assumption 2.1 fixes a set that maps into itself and on which greedy policies exist. Assumption 2.2 asks that each have exactly one -value function , . The value function is , and is optimal if .
A plan factorization is a pair with on for every . With and this gives . Rotating the cycle gives the refactored Bellman operator on , and the refactored -value operators on . The fixed point of is the refactored -value function, is the refactored value function, and is -greedy if .
Let be a Hausdorff topology on under which the pointwise order is closed. If and are monotone, is asymptotically stable on (a unique fixed point to which all iterates converge under ) and every is asymptotically stable on , then
an optimal policy exists, and a feasible policy is optimal if and only if it is -greedy.
Theorem 3.3 is a sufficient condition for computing with the refactored equation: it says that value iteration with converges to the refactored value function and that a policy read off from is optimal, without ever computing . The paper's applications (consumer bankruptcy, optimal stopping) use it to replace iteration over state functions by iteration over a smaller space and report large speed gains; Theorem 3.6 on refactored optimistic policy iteration builds on it.
All results are proved in the paper. No machine-checked version exists: related Prove2Me results cover finite MDPs (SuttonBartoRL.FiniteMDP.bellman_optimality, FoundationsRL.RLBasics.bellman_optimality) and Bertsekas- or Denardo-style abstract models with monotone or contracting (MonotoneDP.Decrease.prop6_bellman_equation, DenardoDP.NStage.theorem4, BertsekasShreve.Generalized.prop6_4_contraction_fixed_point). This mission formalizes the plan-factorization theory itself, under the paper's weak assumptions: no monotonicity of , no contraction, arbitrary state and action sets.
The monotonicity hypothesis is where a naive transfer argument fails. Lemma 6.1 moves fixed points between and without any order structure, so one might expect and to coincide in general. They do not: the paper's Section 6.4 shows dynamic programs with , with but , and with the converse. The proof of Theorem 3.2 compares with and with , which needs monotonicity of at every and of at every , not only on and . Theorem 3.3 then needs a limit argument: for all passes to only because the order is closed under , and the iterates leave .
DPDeconstructed.DynProg X A with arbitrary types X, A (no finiteness, no measurability), Γ : X → Set A, 𝒱 : Set (X → ℝ), and H valued in EReal with H ≠ ⊤ on . is a subtype of X × A; feasible policies form a subtype of X → A.EReal. "" and "" mean that a real function in (resp. ) equals (resp. ) pointwise. applies toReal to , which is real on ; is only applied to elements of .MonotoneOn W₀ 𝒱 and MonotoneOn W₁ 𝒢. This corrects the paper, whose p.14 takes monotonicity on , and : on those sets alone Theorems 3.2 and 3.3 are false (a one-state counterexample is recorded in the items), and the paper's own proofs use the wider domains.Proofs of the milestones in any order are welcome, as are the companion results not in this mission (Propositions 2.1–2.2, Proposition 3.4's contraction criterion, Theorems 3.5–3.6). The rotation lemmas and the abstract dynamic program are reusable for any transformed Bellman equation.
A brand-name product sold through a supplier and a retailer suffers from double marginalization: each firm adds its own margin, so the retail price is too high and both firms earn less than an integrated firm would. Anand, Anupindi and Bassok (Management Science 2008) showed that, in a two-period channel where the supplier sets each period's wholesale price at the start of that period, the retailer buys more than she sells in period 1 and carries the surplus forward. This strategic inventory is carried not to meet demand but to weaken the supplier's period-2 pricing power, and it raises the supplier's profit as well. Without competitors it exists exactly when the unit holding cost satisfies .
Successful products attract copycats: lower-quality imitations that enter after the brand has proven itself (Pun and DeYong, MSOM 2017). Jin, Wu and Chen (SSRN 3826955, 2023; MSOM 2023) ask what copycat entry does to strategic inventory. Their Proposition 2 answers it with a closed-form subgame-perfect equilibrium: copycats lower the holding-cost cutoff below which strategic inventory survives, and they remove it entirely once their quality is high enough.
Timeline: Anand et al. (2008) solve the channel without copycats (cutoff , dynamic contract only). Jin, Wu and Chen (2023) add a Stackelberg copycat entrant in period 2 and obtain the cutoff of this mission.
There are two selling periods. In each, a unit mass of short-lived customers arrives; a customer's valuation of the brand-name product is uniform on , and each buys at most one unit, in its own period. In period 1 the brand is alone: a customer buys iff . In period 2 copycats enter, and a customer values the copycat at , with copycat quality ; she buys the brand iff and , and the copycat iff and . Demands , , are the Lebesgue measures of these sets of .
The supplier charges wholesale prices . The retailer orders , sets prices , sells , carries the inventory at unit cost , and sells ; the copycats sell . Profits are , and . There is no network externality ().
Two contracts fix the move order. Under the commitment contract the supplier announces , the retailer chooses , and the copycats, seeing , choose . Under the dynamic contract the supplier announces , the retailer chooses , the supplier, seeing and , announces , the retailer chooses , and the copycats choose . The solution concept is subgame-perfect equilibrium (SPE). The benchmark means that period-1 leftovers cannot be carried.
With and
for every and : under the commitment contract an SPE exists and every SPE has the Table 1 outcome; under the dynamic contract an SPE exists, and every SPE has the Table 2 outcome with if and , and the Table 1 outcome with if or ; on the boundary both outcomes occur. Moreover on and is strictly decreasing on .
Three rows of the printed Table 2 are corrected. The -term of has the wrong sign: the table's own rows give , and at , the printed value is against . The rows and are inconsistent with the table's own and : the copycat demand there is , and must equal . At the printed and , against and . The corrected rows agree with Table 1's identities and with Anand et al. at .
The result shows that external competition reaches inside the channel. Copycat entry lowers the brand's period-2 demand, which weakens the retailer's reason to hold inventory against the supplier: the range of holding costs with strategic inventory shrinks as grows and is empty for . At the cutoff the supplier switches from tolerating inventory to pricing it away. His profit is continuous across the switch, while the retailer's profit jumps down. Under the commitment contract nothing of this happens for any . These facts are the basis of the paper's contract comparisons.
The paper states the result with proofs in an online supplement, which this mission does not use. Nothing in it has been formalized. The mission produces a machine-checked equilibrium analysis of a two-period vertical channel with inventory carry-over and a Stackelberg entrant, from the customer model up.
Each subgame is elementary, but the equilibrium must hold at every history, including off-path ones: large inventories, zero prices, retailer stock-outs. The copycat's best response must be derived from the demand sets before the retailer's period-2 problem becomes a linear-quadratic program. The supplier's period-1 problem is not concave: his reduced profit in has a concave piece with inventory and a concave piece without, meeting at a convex kink. The global maximum is a comparison of two local maxima, and is the root of the resulting quadratic indifference equation. The naive plan of solving the first-order conditions once yields only Table 2 and misses the switch, and the tie at (including the point , ) admits two equilibria. Uniqueness of the outcome has to be proved over all equilibria, not only for one constructed profile.
The Lean development is in the namespace CopycatSI. Model defines the demands as volume of subsets of (as reals), sales, inventory, holding cost and profits; Holding.infinite is the paper's . Game defines strategy profiles of both contracts as functions of observed histories, IsSPE (optimality at every history), and the on-path outcome. ClosedForms defines , and the predicates MatchesTable1, MatchesTable2. The tables appear only as right-hand sides; equilibria are never defined by them.
Conventions: throughout; zero production costs; the copycats observe only, and their demand is not rationed by the retailer's stock; prices and orders are non-negative; customers indifferent between the products buy the brand (a null set). The copycat rows are asserted for only, since at every copycat price earns zero. Under the commitment contract no inventory value is asserted, because at the timing of purchases is undetermined.
Every theorem asserts existence of an equilibrium, so no statement holds vacuously.
Contributions welcome: the copycat best-response lemma, the period-2 subgame solution for arbitrary inventory, the supplier's piecewise problem, and the real-analysis lemmas on . The game layer (contracts, histories, SPE) is reusable for other two-period channel models.
New drugs, medical devices and patented technologies reach the market only after a phase of costly testing, and they can be withdrawn later when evidence of harm accumulates. Societies control this process with three instruments: an approval standard (how strong the evidence must be before adoption), a withdrawal standard (how bad the evidence must become before the product is pulled), and liability (a payment the firm owes when the product turns out to be harmful). Viscusi, Vernon and Harrington (1995) point out that these instruments interact and that liability can chill research. Henry, Loseto and Ottaviani build a model in which the firm learns from the same public signal before and after approval, and ask which mix of the three instruments a regulator should use. Their main result (Proposition 6, called "our main result" on pp.4 and 26 of the working paper) is the goal of this mission.
The state is good () or bad (). Beliefs are written as log-odds , where is the probability of , so . Information is a Brownian signal with drift and variance ; with the log-odds belief has drift and variance . Phase is ex ante experimentation, which costs per unit of time and ends with rejection (payoff ) or adoption. Phase is ex post learning on the market, which is free and ends with withdrawal. Payoffs are discounted at rate .
On the market the planner earns per unit of time in state and in state . The firm earns in both states, minus a liability in state . Here is the externality rate: the share of the social gain that the firm does not capture.
Policies are standards: a rejection standard , an adoption standard and a withdrawal standard . With , a player with flows who adopts at belief and withdraws at gets the ex post value
From a prior the ex ante value is the expected discounted payoff of experimenting until the belief reaches or . It is written with the closed-form hitting kernels of the paper's footnote 37 and the roots . Welfare is , computed with the planner's flows.
The planner's first best (Proposition 1) is a triple with . In the regulated game the planner commits to and the firm chooses only its rejection standard , as a best reply. An optimal mix maximizes welfare over commitments and the firm's best replies.
For first-best standards there is , independent of the prior, such that for every and every prior :
The printed statement needs three minimal corrections:
Proposition 6 says that liability is used only to discourage research, never to encourage it. When the externality is small, the firm experiments too much, and liability brings it back to the social optimum. When the externality is large, the firm experiments too little; the regulator then drops liability and becomes more lenient at both ends, approving sooner and withdrawing later. This matches the observed pattern that liability and ex post regulation are rarely used together, and that regulators depart from first-best standards in the direction of leniency. Proposition 7 (costly lying) of the paper follows from this result.
The paper's proof is heuristic: it argues "by continuity" and through a second-order/first-order trade-off. The statement as printed has the slips listed above, and no machine-checked proof exists. The mission states the corrected result over the paper's explicit closed forms. A proof will settle whether the corrected statement holds in full, including the strict leniency of Step 3.
Every object is an explicit combination of exponentials, so the statements are elementary. The proofs are not:
Beliefs, standards and the prior are real log-odds. Values are the paper's closed forms for threshold policies (footnote 17 defines the first best this way). The Brownian layer and the paper's reduction to thresholds (Lemmas 1–2) are not formalized. The closed forms are extended by the stopping rules at the boundary: immediate rejection when , immediate adoption when , immediate withdrawal () when .
Further conventions:
The goal is not vacuous: the prior interval is non-empty for the true first best. Comparing optimal mixes only against mixes with the same , or letting depend on , would change the theorem and is excluded.
The development needs only Real.exp, Real.log and Real.sqrt. Lemmas on the hitting kernels (positivity, monotonicity, ) and on single crossing are reusable for other Wald-type problems. Contributions on any milestone are welcome, as are sketches of the Proposition 1 verification argument.
Mean-field control (MFC) models a large population of identical, cooperating agents through a single representative agent whose transitions and rewards depend on the distribution of the whole population. It is the limit of cooperative -agent problems as , and it is used for systems such as ride-sharing fleets, resource allocation and equilibrium pricing, where interactions pass through aggregate quantities. When the transition law and the reward are unknown and must be learned, the natural tool is reinforcement learning, and the first question is which Q function obeys a Bellman equation.
The classical Q function on states and actions does not: Example 3.1 of Gu, Guo, Wei and Xu shows it is time inconsistent for MFC. The paper lifts the problem to the space of state distributions, with local policies as actions, and proves the dynamic programming principle (DPP) for the resulting integrated Q (IQ) function.
Timeline. Laurière and Pironneau (2014) and Pham and Wei (2016) proved DPPs for the value function of McKean–Vlasov control with strict controls over a finite horizon, by enlarging the state space; Pham and Wei work in discrete time. Djete, Possamaï and Tan (2019) proved one in a more general framework. Gu, Guo, Wei and Xu (arXiv 2019, v6 2022) gave the DPP for the IQ function with relaxed controls and stochastic rewards over an infinite horizon, the first for MFC with learning.
Let and be the state and action spaces and the probability measures on . A model consists of a transition law , a reward law , both measurable in , and a discount factor .
An admissible control is a sequence of measurable maps (relaxed feedback controls). Under the representative agent follows the McKean–Vlasov dynamics (2.7)
where and are the laws of and themselves. The value of from is , and .
A local policy is a measurable map . With , the lifted transition and integrated reward are
The IQ function is , where is the expected discounted reward when , and for . Throughout, Outstanding Assumption (A) holds: for every , .
The DPP says that mean-field control with learning is a reinforcement-learning problem whose state is the population distribution and whose action is a local policy. It justifies Q-learning on , which the paper uses to design its learning algorithms for MFC (Algorithms 1–2). It is the necessary condition; the paper's verification theorem (Theorem 3.2) is the sufficient one and is not part of this mission.
The result is proved in the paper, with the proof given in outline ("we highlight the key step"). This mission formalizes it, with no machine-checked version existing before. The formal development adds a discrete-time McKean–Vlasov control layer with a genuine path law, built on Mathlib's Ionescu-Tulcea construction, and states the law-invariance lemmas for every realization of the dynamics, which the paper asserts with a short sketch.
The DPP is short once the problem is known to be a deterministic control problem on . Establishing that is the work. The population laws enter the kernels, so a path law cannot be written down before the flow of laws is known. One must show that the flow fed into the kernels is the flow the kernels produce (Lemma 2.1), and that every process satisfying (2.7) has that flow. Lemma 2.2 then exchanges expectation and an infinite series under (A), which bounds in expectation for each but not uniformly. The remaining steps are supremum arguments at fixed : an -optimal tail control is joined to a first-step local policy. Since the flow is deterministic, no measurable selection is needed.
and are arbitrary measurable spaces (the paper's compact separable metric spaces are an instance; no metric is used), and is ProbabilityMeasure X with the Giry -algebra. , , local policies and controls are Markov kernels; is a law on , so rewards are stochastic. is encoded by -indexed controls shifted by one, with the value of the control that plays first and then .
and are Bochner integrals of under the canonical path law (Kernel.trajMeasure). They are not defined as : with that definition Lemmas 2.1–2.2 become tautologies and the goal is bookkeeping. (A) is a lintegral with inside the sum. All suprema are real; under (A) they are bounded, which milestone (3.7) states.
The paper also asserts that , and are measurable on without naming a -algebra on . For uncountable this fails for every -algebra on (a diagonal argument). The milestones therefore state measurability in for fixed , and joint measurability for countable ; the goal does not claim measurability of , and its proof does not use it.
Needed infrastructure: kernel composition and products, the Ionescu-Tulcea trajectory measure, lintegral_tsum and integral_tsum. A reusable lemma identifying finite-dimensional marginals of trajMeasure with time-dependent kernels would serve other discrete-time McKean–Vlasov and MDP missions. Proofs of the milestones in any order are welcome.
On public blockchains, pending transactions wait in a public mempool before a block includes them. Anyone who sees a profitable transaction there can send a competing one with a higher fee and have it executed first. This is front running. It is a large, measured source of losses on decentralized exchanges and in other smart contracts (Daian et al., 2020). A standard defence is the commit-reveal protocol. The user first publishes a hash of her message, which hides its content, and reveals the message one block later. The contract executes a revealed message only if it matches an earlier commitment from the same address.
Canidio and Danos (arXiv:2301.13785v3) model this protocol as a game between a victim and an attacker. They ask when the protocol removes front running. Their answer is a threshold: compare the cost of a commit message with the value of a guess the attacker must commit to before seeing anything. This mission formalizes that threshold result, Proposition 2, together with the lemmas of §3.1 that lead to it.
A state of the world is drawn from a prior and observed only by player (Alice). Messages range over . Both and are finite and non-empty.
The protocol has two blocks.
Strategies are behavior strategies. For : probabilities and . For : a lottery over his commit options and firing probabilities . An equilibrium is a Nash equilibrium of the ex-ante expected payoffs. Write for , eq. (3). The value of a blind guess is
The front-running threat of 's strategy is . It is the probability that fires at 's message in the states where she has one to send.
So an equilibrium free of front running exists if and only if .
The printed proposition reads: "If , then there is no front-running in equilibrium. If instead , front running occurs with strictly positive probability in equilibrium." Both sentences fail under their natural readings, for any model satisfying every assumption of §§2–3.
Both counterexamples are checked as Lean proofs.
The threshold measures how much the protocol protects. The attacker must commit before seeing the victim's message, so his relevant information is the prior, not the message. Attacks that rely mostly on observing the victim, where guessing is hard, are removed. Attacks in which the attacker would profit anyway are not. Section 4 of the paper builds its comparison of attackers with legitimate competitors, and of hidden commitments, on this threshold.
A formal proof settles which version of the claim holds. The printed proposition mixes "some equilibrium" with "every equilibrium" and on-path behavior with threats. The corrected statement separates these. Its two halves together give a sharp characterization. No part of this paper has been machine-checked before.
The obvious argument fixes the "no front running" profile and checks deviations. That gives clause 2. It does not give clause 3, and the obvious converse is false. When guessing is easy, the attacker's threat can keep the victim out entirely, so nothing happens on path. Clause 3 instead argues by contradiction from an equilibrium with zero threat. In that case the victim must commit exactly where , which is where the interval assumption enters. Then a committed guess earns the attacker .
Ex-ante Nash equilibrium places no constraint on zero-probability states or information sets. Every per-state statement must be weighted by its probability, and handling this is a large part of the work.
Existence is Nash's theorem for this finite game, in behavior strategies. It can be proved from the normal form, or directly with Kakutani's fixed point theorem on the product of simplices.
The formalization commits to the following conventions:
Fintypes with DecidableEq and Nonempty, and the prior is a real vector summing to , possibly with zeros.Equilibrium is the plain Nash condition over all unilateral deviations. It is not defined through the paper's answer, and 's firing and 's revealing are free probabilities, so the milestones are not true by definition.
Everything is finite sums over finite types; no measure theory is needed. Mathlib's simplices and Brouwer/Kakutani-type fixed points, or the platform's AGT.nash_existence for finite normal-form games, are possible routes to existence. Proofs of any milestone are welcome.
A credit default swap (CDS) insures a lender against the default of a borrower: the protection buyer (the lender) pays an upfront premium, and the protection seller (a dealer) pays the insured amount if a credit event occurs. Because the payment depends on whether the firm is liquidated, both sides of the contract have a stake in how a distressed firm is resolved. Practitioners call the resulting interventions CDS activism: an insured lender who demands better terms in a debt restructuring (the "empty creditor" problem of Bolton and Oehmke, 2011), or a dealer who injects capital into a distressed firm to avoid paying on the CDS (Norske Skog, RadioShack, McClatchy). The legal literature disagrees on whether such interventions should be restricted.
Danis and Gamba (2024) build a closed-form model that compares a world where only the CDS buyer can intervene with one where the seller can intervene as well. Their Proposition 1 says that an intervening seller raises ex ante firm value, that the lender then hedges fully although the firm is never liquidated, and that the CDS premium is positive although no credit event ever occurs. This mission formalizes that proposition and the backward-induction chain behind it.
A firm owned by an entrepreneur chooses capital and the face value of a zero-coupon bond. At the end of the period the asset value is
where the profit shock is uniform, with , and expectations are . Corporate tax is levied at rate on the equity payoff, and the risk-free rate is zero.
The lender buys CDS protection on a fraction (the hedge ratio) of the face value. After is drawn, the equity holders, facing face value , either repay ( to equity), renegotiate (feasible iff ; the lender's outside option makes the renegotiated payment , leaving ), or liquidate (everything is lost; the dealer pays ). They take the best action, ties broken repay, renegotiate, liquidate.
Model 1 (active CDS buyer). The owner picks , the lender picks , the shock is drawn, the equity holders decide. The CDS is priced fairly: its price is the expected payment . The value of debt is the lender's expected payoff net of that price, and the firm value is .
Model 2 (active CDS seller). As above with , but after the shock the dealer makes a take-it-or-leave-it offer : inject to cut the debt to , in return for an equity stake . The owner accepts iff times her equity under is at least her equity under . The premium is fair, meaning zero NPV for the dealer: it equals minus the dealer's expected ex-post payoff, injection included.
In both models a subgame-perfect equilibrium is a profile of strategies optimal after every history: the dealer's offer after every (model 2), the lender's hedge ratio after every , and the owner's . Its value is .
For , , , both models have equilibria, and for all equilibria of model 1 and of model 2,
Model 2 has an equilibrium with , zero probability of liquidation and a positive premium; when every equilibrium of model 2 has , zero probability of liquidation and a positive premium. The printed (a) says "increases"; at both values are first best, hence the corrected form.
The proposition isolates a mechanism: the lender's large hedge raises his outside option in renegotiation, which alone would make liquidation more likely (model 1), but it also gives the dealer a reason to recapitalize the firm in distress. With both interventions the three frictions of the model (lack of commitment, liquidation costs, taxes) stop constraining investment, and the firm invests at the first-best level. The testable predictions of the paper (§2.1, Table 4), on yield spreads and liquidation probabilities when regulators restrict dealer intervention, rest on this comparison.
The result is proved in the paper by closed-form calculation; it has no machine-checked proof. A formalization adds two things. First, the paper solves each stage under conjectures (, ) and at the equilibrium values; the formal statements quantify over every equilibrium, so the conjectures must be discharged. Second, it pins down where the printed statement needs care: at the value comparison is an equality, and other equilibria with no hedging exist.
Each lemma is elementary; the difficulty is that equilibria are defined by optimality after every history, not by the closed forms. The obvious route, "substitute Lemma 3 into the payoffs", is not available: the dealer's strategy is any optimizer, and it is not unique (the dealer is indifferent at , and at , ). The value of debt must be shown independent of these choices, which holds because the choices at , give every player the same payoff and the others concern a null set of states. The lender's problem must be solved over all , including the region that the paper never visits, and the owner's problem over all , including the corner where every hedge ratio is a best response.
Lean represents the shock by Lebesgue measure on scaled by , and every paper integral by a set integral over a subset of , so a threshold above gives an empty region. is Real.rpow. Ties are broken as in the paper: repay over renegotiate over liquidate, and the owner accepts an offer when indifferent. The renegotiated payment is with the original , even after a reduction to . The hedge ratio lies in in model 1 and in in model 2. Equilibria are structures carrying strategies and optimality proofs; the goal asserts their existence, so the clauses over all equilibria are not vacuous.
A trivializing formalization would define the dealer's offer by Lemma 3 or the firm value by (15); the definitions here use only optimality predicates, so these are theorems.
A complete development needs integrals of piecewise linear functions under the uniform law, maximization of concave quadratics on intervals, and the a.e. independence of payoffs from the dealer's tie-breaks. Proofs of the milestones, alternative arguments, and lemmas on uniform expectations of truncated linear functions are welcome.
The maximum-entropy sampling problem (MESP) asks, for an covariance matrix of Gaussian random variables and an integer , for the variables of largest joint differential entropy:
where is the natural logarithm of the determinant. It arises in the design of environmental monitoring networks and other sensor-placement problems, and it is NP-hard (Ko, Lee, Queyranne 1995). Exact algorithms are branch-and-bound methods, and their performance rests on the quality of upper bounds on .
Two generic devices can tighten such bounds. Scaling uses for ; most bounds are not invariant under it, so the scaling parameter can be optimized. Masking uses that for every correlation matrix (Hadamard product ), so a bound for is a bound for (introduced in full generality by Anstreicher and Lee, 2004, for the eigenvalue bound; see §1 of the paper).
Timeline. Anstreicher introduced the linx bound (Anstreicher 2020), a concave relaxation that is among the strongest known bounds for MESP. Chen, Fampa, Lambert and Lee showed that the linx bound is convex in , so a locally optimal scaling parameter is globally optimal (CFLL 2021). Chen, Fampa and Lee (arXiv:2106.02980v1, 2021; Operations Research 2024) studied masking for the linx bound and proved that masking can improve it by an amount linear in , both without scaling (their Theorem 2.12) and, with a smaller constant, when both bounds are optimally scaled (Theorem 4.1, the goal of this mission).
Let be a finite index set with , , and the all-ones vector. The feasible set is
For a real symmetric matrix and the scaled linx objective is
with on matrices that are not positive definite, and the scaled linx bound is
The unscaled bound is . A mask is a positive semidefinite matrix with unit diagonal, and the scaled and masked linx bound is . An optimal scaling parameter is a with . In Lean these are MaskedLinx.feasibleSet, linxMatrix, linxObjective, linx and IsOptimalSolution; the identity mask enters as C ⊙ 1.
There are and positive semidefinite of order , with positive diagonal and , such that for every even both minima below are attained, both are finite, and
The paper states the theorem for the even integers; is false (no matrix gives a positive gap), so the index set is every even , which contains the multiples of the paper's proof uses.
In the order of the paper's argument:
The theorem shows that the benefit of masking for the linx bound is not an artifact of a poorly chosen scaling: even after each bound has been optimally scaled, the identity mask can lower the bound by . This justifies the search for good masks as a separate optimization layer in branch-and-bound for MESP, which the paper proposes as further work. The milestones are reusable on their own: Proposition 1.1 and Proposition 3.1 give closed-form optimal scalings, Theorem 2.8 solves the linx relaxation for diagonal matrices exactly, and Theorem 3.6 with Corollary 3.7 settles when an optimal scaling parameter exists.
None of these results has a machine-checked proof. The paper's last numerical step is slightly off: its closing expression evaluates to , just below the stated . The statement itself remains true, since the witnesses of the proof give a gap of , but a formal proof has to supply a sharper lower bound than the paper's final display.
The masked side is easy once the witnesses are chosen with unit diagonal: , and Proposition 3.1 gives the minimum at . The difficulty is the unmasked side, which needs a lower bound on valid for every , together with attainment of the minimum over . The natural route evaluates the objective at the uniform point (Lemma 2.9 applied to ), but that point alone yields only , short of the constant. Attainment needs the limits of Theorem 3.6 and continuity of , which is a supremum of a family of extended-real functions. The case is not covered by the paper's construction and needs its own witnesses.
Indices are Fin n (0-based; the paper's is d ⟨s - 1, _⟩), matrices are Matrix (Fin n) (Fin n) ℝ, and is a natural number. The objective is EReal-valued, with whenever the matrix is not positive definite, so the convention never scores a singular point as . The bound is the EReal supremum over , which is attained. Eigenvalues are Mathlib's IsHermitian.eigenvalues, and rank is Matrix.rank over . In the goal is natural-number division on even , and the minima are explicit minimizers with real minimum values , so neither an -valued infimum nor EReal subtraction can make the statement trivial. The witness matrices must be PSD with positive diagonal and rank at least , which excludes degenerate choices.
A complete development needs determinants of block-diagonal and Schur-complement matrices, the log-determinant of at points, spectral calculus for PSD matrices, and continuity of the linx bound in . The diagonal-case results (Lemma 2.3, Theorem 2.8, Proposition 3.1) and the existence results (Theorem 3.6, Corollary 3.7) can be developed independently and are useful for any later work on scaled MESP bounds. Proofs of any milestone, and alternative arguments for the goal's unmasked lower bound, are welcome.
A one-dimensional Brownian motion can be viewed as reflecting Brownian motion whose excursions away from receive independent random signs. The spider process, also called Walsh Brownian motion, replaces the sign by a uniformly random choice among rays meeting at the origin (Walsh 1978; Barlow, Pitman and Yor 1988). It is the basic diffusion on a star graph.
Lester Dubins asked how much of the spider's state space a stopping time can cover for a given expected running time: find the best with , where is the total length visited. The answer is known for (, Dubins and Schwarz 1988) and (, Dubins, Gilat and Meilijson 2009); according to the paper, no other case had been answered (Ernst 2016 discusses ).
Bednarz, Ernst and Osękowski (arXiv:2105.15202v2), published in Mathematics of Operations Research in 2024, solve the variant in which size is measured by the diameter in the British rail metric: the two longest visited segments on distinct rays. For they identify the best constant through an explicit solution of a three-dimensional optimal stopping problem.
Fix and rays in . On a probability space take a Brownian motion and an independent i.i.d. sequence , uniform over the rays. Number the excursions of away from and let be the number of the excursion straddling . The spider is
For a time , the trajectory is . The rib on ray is the length , and the diameter is
Stopping times are those of the filtration generated by the spider.
The analysis runs through a process with state space . Here is the longest rib and the second longest, so . The coordinate is the distance of from the origin, with a plus sign when lies on the running longest rib and a minus sign otherwise. Thus is a -skew Brownian motion that jumps from to when the second longest rib overtakes the longest. With the gain , the value function is , the supremum over integrable stopping times.
The explicit candidate is built from
and its inverse boundary ( for , otherwise). It is given by formula (3.8), by Corollary 3.5 and by formulas (3.12)–(3.13) of the paper.
For every , the least constant such that
is
Both halves are required: the inequality holds with , and fails for every smaller constant. Numerically , and .
The milestones follow the paper's order.
Theorem 1.1 gives the first sharp constant in a Dubins-type coverage inequality for the spider with rays. The constant is given by an integral of an implicitly defined boundary; numerically it increases slowly with from about at . The method is also of interest. A process on a star graph is reduced to a skew Brownian motion with jumps, and the optimal stopping problem in three variables is solved with a free boundary given by an ODE. Both reductions apply to other functionals of Walsh Brownian motion.
The result is proved in the paper. Nothing in this mission is formalized yet, and the substrate it needs (excursion theory, skew Brownian motion, local times) is largely absent from Mathlib.
Two statements of the preprint are corrected here.
The goal uses the corrected constant.
The upper bound needs Lemma 4.2. The candidate is not , is a skew Brownian motion, and jumps. The proof therefore applies the Itô–Tanaka formula between successive hitting times and uses the symmetry of Remark 3.7 to cancel the jumps. A direct Itô argument on the spider fails because has kinks along the free boundaries and at .
The lower bound needs the value of an explicit strategy. Its expected gain must be computed region by region, from the hitting law of Lemma 3.2 and the ODE for the boundary , and then shown to equal the explicit .
The scaling step is elementary. Defining the constant through would make it free, which is why the goal fixes it as the explicit integral.
IsBrownianReal, in its continuous version: every path is continuous and starts at . Rays are indexed by Fin n from . Excursions are numbered by the first rational time, in a fixed enumeration, that they contain. The spider takes values in .No trivial encoding of the constant is possible, because is a fixed explicit function.
Needed infrastructure, reusable beyond this mission:
Contributions toward any milestone, or toward that infrastructure, are welcome.
Many online services (social platforms, question-and-answer sites, collaboration tools) become more valuable to a user the more that user's contacts use them. A firm launching such a service commonly offers it for free at first, to let usage grow through these local network effects, and starts charging later. Alizamir, Chen, Kim and Manshadi (SSRN 3236225; published in Mathematics of Operations Research, doi:10.1287/moor.2021.1197) model this as a pricing problem on a weighted network and ask how the structure of the network affects the firm's best policy and revenue.
Their second structural result separates two features of a network: the strength of the interactions, summarized by the average degree, and their heterogeneity, the spread of the individual degrees. Holding the strength fixed, the paper shows that homogeneity is the worst case for the firm. This mission formalizes that result, Theorem 2 of the paper, together with the chain of lemmas its proof rests on.
There are consumers. A network is a real symmetric matrix with and ; measures how strongly consumers and influence each other. The weighted degree of consumer is , the average degree is , and the network is balanced if for every .
Time is discrete. With habit coefficient , utility coefficients and price in period , consumption follows the linear rule
where . A policy offers the service for free in periods and charges afterwards. With discount factor its revenue is
and the firm's optimal revenue is the maximum over all policies. Throughout, the paper imposes Assumption 1: every eigenvalue of satisfies , and for the largest eigenvalue .
Fix , , , , , and consider all networks on consumers with average degree that satisfy Assumption 1.
(i) For any two balanced networks of the class and every policy ,
so the two networks have the same optimal revenue and the same optimal policies.
(ii) For every balanced and every in the class, and every policy ,
The goal contains both the printed clauses (equal optimal policies and revenue; lowest optimal revenue) and the per-policy statements the proof establishes.
Part (i) says that, for this pricing problem, a balanced network is summarized entirely by and : a firm that knows its users interact homogeneously needs no further information about who interacts with whom. It also extends the paper's comparative statics for complete graphs (Proposition 2) to all balanced networks. Part (ii) says that, at a fixed average degree, every departure from balance weakly increases the revenue of every policy, because heterogeneous networks generate more walks of each length and hence faster consumption growth. Together they identify the second-order (degree heterogeneity) effect of a network on monetization.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it yields a checked closed form for the revenue of linear consumption dynamics on networks, and a formal Blakley–Roy inequality for nonnegative symmetric matrices, which is not in Mathlib and is of independent use in spectral graph theory. Fact 6 is printed without a nonnegativity hypothesis it needs; the mission states the corrected version.
Part (i) is close to elementary once one notices that consumption stays a multiple of on a balanced network. The difficulty is part (ii). The obvious approach compares the two consumption trajectories period by period. Equal average degree controls only walks of length one: total consumption agrees on the two networks in period 2, and from period 3 on the comparison depends on the number of walks of every length. What is needed is the Blakley–Roy inequality, a genuinely nontrivial matrix inequality whose classical proofs are not short. A second obstacle is analytic: the revenue is an infinite series, and rewriting it as a nonnegative combination of walk counts requires absolute convergence, which in turn needs the Perron–Frobenius bound together with Assumption 1.
Consumers are Fin n; a network is a Matrix (Fin n) (Fin n) ℝ with IsSymm, nonnegative entries and zero diagonal. Time is shifted to ℕ with x 0 = 0. A policy is ℕ × Set.Icc 0 (α/β): the free-offering length may be , and prices are restricted to , the range on which the paper's linear consumption rule is valid. The revenue of a policy is a real tsum, the optimal revenue a real supremum over policies; under Assumption 1 the series converges and the revenues are bounded, so neither takes a junk value. Assumption 1 is stated for every eigenvalue of Matrix.toLin' M, part 2 in the multiplied form , which keeps the network , in the class instead of excluding it through Lean's . Eigen-data in the milestones are arbitrary orthonormal eigenbases of (OrthonormalBasis (Fin n) ℝ (EuclideanSpace ℝ (Fin n))), with .
The goal cannot be trivialized: the class is nonempty and contains both balanced and unbalanced networks (the star and complete networks of the paper's Example 2 both satisfy Assumption 1 with , ), and part (ii) quantifies over all networks of the class, not only balanced ones.
A complete development needs the spectral theorem for real symmetric matrices (in Mathlib), geometric series of matrices, a Perron–Frobenius bound for nonnegative symmetric matrices, and the Blakley–Roy inequality; the last two are reusable beyond this mission. Contributions are welcome on any milestone, in particular a direct proof of Fact 8, and alternative routes to the goal that avoid the spectral decomposition (for example, comparing walk counts in the consumption recursion directly).
A wireless service provider (WSP) that sells phones with a customer warranty must replace a device that fails while that warranty is in force. Replacements come from an inventory of refurbished devices, each still carrying what is left of its OEM warranty, the manufacturer's warranty under which the WSP can return a failed device for free repair. When a customer whose warranty ends at date receives, in period , a device whose OEM warranty ends at date , the WSP is exposed for periods: a further failure in that window is repaired at the WSP's own cost. Calmon, Graves and Lemmens (SSRN 3357683; published in Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0889) study how the matching of devices to claims drives this uncovered warranty time, using data from a large WSP that stores refurbished devices unsorted and assigns them at random.
The question this mission formalizes is how bad random assignment can be when nothing is known about the termination-date distributions except that they change slowly from one period to the next.
Periods and warranty termination dates are integers. is the warranty length and the repair lead time. The cost (1) of assigning a device with OEM termination date to a customer with termination date in period is
and the uncovered time is the case .
On a probability space , is the customer-warranty termination date of a randomly chosen customer filing a claim in period . The standing model up to period asks that the , , are independent integer random variables with almost surely, and that their laws satisfy the Kolmogorov–Smirnov drift condition (6),
With demand and inventory per period, a device in stock is used with probability each period, so its time in inventory is a geometric number of trials: , . Because warranties are matched when a device is first sold, a device in stock at carries the date of the customer who returned it, so random assignment hands the period- customer a device with date .
With and , and independent of the dates,
and, for every , with independent inventory times and ,
Moreover, if , and ( or ), the first bound is attained. The printed proposition claims that "this bound is tight, i.e., there is a distribution of that achieves this bound" for all parameters. That is false: given the cost is at most , which is below once . At , , the bound is and the cost at most , and for , , , the geometric tail makes the inequality always strict. The goal keeps the claim on exactly the parameters where the paper's two-point argument (p.ec5) works.
The bound needs only the per-period drift , which the WSP estimates at per day (p.12), and no model of the termination-date distributions themselves. It turns the operational parameters (lead time, inventory-to-demand ratio, warranty length) into a worst-case figure for the uncovered time caused by random assignment, which is the benchmark against which the paper evaluates the sorting policies YOF and OOF. The bound grows with , the mean age of a reassigned device, and with , the variance of that age, so holding more inventory relative to demand raises the worst case.
The result is proved in the paper; it has not been machine-checked. Formalizing it checks a proof whose central lemma has a gap (below), and produces two reusable pieces: an extremal inequality for under a Kolmogorov–Smirnov constraint, and a clean stochastic model of a closed-loop warranty system with geometric inventory times.
The core is Lemma EC.1. The printed proof first reduces to laws supported on by "splitting" the mass at each interior point between the endpoints, and claims the KS constraints survive. They need not: for , , , , splitting the mass at produces a CDF difference of . The lemma itself survives every numerical test. A correct route uses convexity, on , and, for integer variables, , where is the CDF of .
The second difficulty is bookkeeping: is a random index into an infinite family, so the conditioning on must be done over a countable partition, with the joint independence of and the family, and the support bound must be transported to the window after replacing by .
The dates are a family D : ℤ → Ω → ℤ indexed by all integers, because reaches arbitrarily far back when ; t - l - Z ω is integer subtraction. Independence is iIndepFun on the indices , and is independent of that family as an IndepFun. takes values in with , which is the convention fixed by ; Mathlib's geometricMeasure counts failures and starts at . The drift condition ranges over all . No lower bound and no identical distribution is assumed; are reals. Positive parts are max (·) 0 on , cast to . and are the Bochner integral and Mathlib's variance, never their closed forms, and every theorem that uses a second moment states its integrability, so no conclusion rests on Lean's convention that a non-integrable function has integral . The support bound is the one the proof states at the current period (p.ec4); it is implied by the sharper and, unlike that bound imposed on the whole past, it admits stationary laws, so the model has instances for every .
Lemma EC.1 is stated on probability vectors with the double-sum objective of (EC.1), which is for independent ; without independence the lemma is false. The substrate is Mathlib: independence, Bochner integrals, variance, ConvexOn. Proofs of Lemma EC.1 and of the conditioning step are welcome as standalone contributions; Lemma EC.1 is reusable for any KS-constrained worst-case analysis.
A buyer facing uncertain demand often secures supply in two stages: it first reserves capacity from several suppliers, and after demand is observed it decides how much of the reserved capacity to use. Electricity procurement (reserve markets), contract manufacturing and logistics all have this shape. In practice each supplier quotes a reservation price for capacity and an execution price for delivered quantity, and the buyer pays as bid. How suppliers should price in such a market, and whether competition leads to an efficient outcome, are the questions of Anderson, Chen and Shao (arXiv:1905.11084), published in Operations Research (2022).
The answer connects procurement with mechanism design. In a Vickrey–Clarke–Groves (VCG) auction each bidder is paid its marginal contribution to total welfare, and truthful bidding is an equilibrium (Vickrey 1961). The paper shows that a pay-as-bid capacity game, under a submodularity condition, has an equilibrium with the same VCG profit split, reached by suppliers marking up their costs by exactly their marginal contributions.
There is a finite set of suppliers. The buyer reserves a capacity vector with , where each is compact and contains ; write and for the suppliers used. A random demand with a known distribution is then observed, and the buyer picks an execution vector , where is compact and whenever . The buyer earns revenue ; supplier incurs a capacity cost and an execution cost , both zero when is unused.
A bid of supplier is a pair of payment functions that vanish when is unused. Given bids and a buyer choice , the buyer's profit, supplier 's profit and the supply chain profit are
For , is the largest supply chain profit over choices with . The contributing suppliers are , and is supplier 's marginal contribution.
The buyer maximizes and breaks ties toward the largest supply chain profit (Assumption 1). Assumption 2 asks that all supply-chain-optimal choices use the same suppliers. Assumption 3 is submodularity of in the form
A family is consistent with the costs if adding to the costs, for , changes neither the optimal value nor the optimal solution, for every .
Let consist of the bids for and otherwise, with
Under Assumptions 1–3, for every consistent : is a Nash equilibrium; every buyer choice under is supply chain optimal; and
In the order the proof uses them: the profit identity (3); the equivalence of consistency (8) with conditions (a) and (9); Lemma 1, ; the bound (A-2) on the buyer's profit under ; the support identity (5); Lemma 2, ; the identity (A-3) ; and the deviation bound of p.30, after any unilateral change of bid.
The theorem shows that pay-as-bid procurement with two-part bids coordinates the supply chain in equilibrium: the buyer's choice maximizes total expected profit, without contracts designed for that purpose. It also pins down the profit split: each supplier keeps its marginal contribution, suppliers outside earn nothing, and the buyer keeps the rest, which is nonnegative by Lemma 1. Since payments are as bid, the equilibrium avoids some of the practical difficulties of VCG auctions that the paper reviews (§2, p.6). Corollary 2 of the paper specializes the result to function bids, and Proposition 1 builds equilibria in power-function bids from it.
The result is proved in the paper, with an appendix proof. No machine-checked version exists on the platform. The mission produces a formal statement of the general capacity game and of the equilibrium claim, the two set-function lemmas (stated for any function satisfying the submodularity inequalities, so reusable for other marginal-contribution arguments), and the profit identities of the proof.
The arithmetic of each profit identity is short. The central difficulty is the deviation step: for an arbitrary new bid of supplier and an arbitrary optimal response of the buyer, the deviator's profit must be bounded by . The natural first idea, comparing the buyer's new choice with the supply chain optimum , does not work: after a deviation the buyer may use a different set of suppliers , the other suppliers' margins are then paid on that different set, and the supply chain value of that set can lie anywhere between and . The bound must hold uniformly over all such sets, and the margins and the attainment of every optimal value enter at every subset, not only at . Suppliers outside are handled by a separate argument in the paper.
Suppliers form a finite type N and vectors are functions N → ℝ. The demand set is a measurable space with a probability measure, and expectations are Bochner integrals. A choice is feasible only if the functions , and (for given bids) are integrable; without this the integral of a non-integrable function is and the profit identities fail. is a supremum. The paper's semicontinuity assumptions (a)–(c) serve only to make every attained; they are not imposed. In Theorem 2 attainment is part of consistency (8) with , and the support identity (5) assumes it directly. The buyer's maxima under are concluded, not assumed. Submodularity is stated in the local form (6), not the union–intersection form.
"Nash equilibrium" is not defined in the paper. Here a bid set is a Nash equilibrium if its bids are allowed (vanishing at zero capacity, resp. execution), the buyer has an optimal choice under the tie-breaking rule of Assumption 1, and for every supplier , every allowed bid , every buyer choice before and every buyer choice after the deviation, supplier 's profit does not increase. The deviation clause is vacuous for a deviation under which the buyer has no optimal choice; the milestone on p.30 covers every deviation without that caveat. Consistency (8) is read as attainment at some supply chain optimal choice, and is indexed by all of .
A trivializing formalization is ruled out: the buyer's choice is defined by optimality and tie-breaking, not by supply chain optimality, so clause 2 is not assumed; and a proved sanity instance (one supplier, deterministic demand) satisfies all hypotheses with buyer profit and supplier profit .
Needed infrastructure: linearity of the integral over a probability space, suprema over feasible sets, finite sums over subsets, and Function.update for unilateral deviations. Contributions are welcome on the two set-function lemmas, which need no measure theory, and on the profit identities (3), (A-2) and (A-3).
Alaska allocates scarce big-game hunting permits through a draw in which each applicant may buy up to six tickets and spread them across the permit lotteries of her choice; an applicant drawn in several lotteries keeps the permit she ranks highest. Designs of this kind, parallel lotteries, are simple to run and give applicants freedom to express intensity of preference, but they are not efficient: two applicants could sometimes gain by swapping their chances in two lotteries. Arnosti and Randolph (SSRN 3370605; published as Parallel Lotteries: Insights from Alaskan Hunting Permit Allocation, Management Science 2021, doi:10.1287/mnsc.2021.4120) model these draws as -ticket lotteries and ask how much welfare such ex-ante trades could add. Their answer, Theorem 2, bounds the possible gain by the factor . The question sits next to the classical pseudo-market of Hylland and Zeckhauser (1979) and parallels the approximate-efficiency bound for raffles of Immorlica et al. (2017).
There are item types with quantities and a mass of unit-demand agents. An agent's type lists her values for the items; the outside option is worth . Types are distributed according to a probability measure on , absolutely continuous with respect to Lebesgue measure.
A strategy consists of a ticket vector with and a strict ranking of the items; is the finite set of strategies. Each ticket in lottery is drawn independently with probability , and an agent receives her highest-ranked item among those for which one of her tickets was drawn. Her probability of receiving item is
and her expected welfare is . A -ticket equilibrium is a pair of a measurable strategy profile and win probabilities such that maximizes for every type , and is consistent with supply: for every , with equality when . Its allocation is .
A feasible allocation is a measurable with and . It is a trade reallocation of if : agents only exchange probability shares, and the total quantity of each item handed out is unchanged.
For every , every equilibrium with allocation , and every trade reallocation of , if then
and if then . The hypothesis set includes that -almost every type values positively some item in positive supply, which makes the ratio of the paper's Definition 9 defined almost everywhere.
The clause is a correction. Definition 9 with asks for no trade reallocation with ratio for all , which fails for every allocation because is a trade reallocation of . The corrected clause says that no trade makes almost every agent strictly better off. For the statement is the printed one in its almost-everywhere form, which is stronger than "not for all ".
Theorem 2 says that a parallel lottery is within a constant factor of trade efficiency for every number of tickets: whatever ex-ante exchange of probability shares the agents agree on, some positive mass of them gains less than the factor . Together with the companion bound that -ticket lotteries are -wasteful (Theorem 3, not part of this mission), it quantifies the trade-off a designer faces in choosing : more tickets reduce waste and cost at most a bounded loss in trade efficiency.
The theorem is proved in the paper (App. D.2). No machine-checked proof exists. The mission produces a formal model of lottery-based allocation to a continuum of agents (strategies, win probabilities, consistency with supply, ex-ante trade), which other results of the same paper and related raffle and lottery mechanisms can reuse, and a checked proof of the bound, including the corrected case.
The equilibrium allocation is not given in closed form; the proof uses only optimality of each agent's strategy and the prices . Comparing with agent by agent fails, because a trade can make some agents arbitrarily better off. The argument must first find the positive-measure set of agents whose traded bundle is affordable (50), then bound the best affordable bundle through a linear program with two non-box constraints, and finally reduce to an explicit two-variable function whose supremum is approached but, for , not attained. The strict inequality requires the strict convexity of , which the paper's Lemma 8 states only in the weak form.
Items are Fin n; types are Fin n → ℝ with Lebesgue measure volume; is a probability measure with volume. A ranking is encoded as a permutation giving each item its position, ticket counts lie in , and is a finite type with the discrete σ-algebra. Optimality is required for every type, as in Definition 1. Consistency uses the printed finite sum over . Allocations are measurable, so their integrals are genuine (a non-integrable function would integrate to in Lean). The welfare ratio is stated multiplicatively. The cost sums over items with , is set to its limit , and Lemma 7 is stated on .
The trivial readings are ruled out: the trade constraint is about integrals of measurable bounded functions, the equilibrium is the paper's Definition 3 (not a greedy algorithm or a cost bound), and proved sanity checks show that the hypotheses of Theorem 2 are satisfiable for every (a one-item example with uniform on ).
Needed infrastructure: finite sums and products over Fin n, the Bochner integral, convexity of real functions on intervals (ConvexOn, StrictConvexOn), and an LP vertex argument for the two-support claim. Contributions are welcome on every milestone; the convexity of and the LP support lemma are reusable outside this mission.
A server, storage unit or production machine can serve a customer and then become available again. Offering it now earns revenue but may prevent serving a later customer while it remains occupied. Online assortment optimization with reusable resources studies these decisions when each customer chooses among the products offered and an outside option. The customer types may arrive in an adversarial order, and the seller learns each choice model only on arrival. Gong, Goyal, Iyengar, Simchi-Levi, Udwani and Wang study whether a policy that optimizes the immediate offer can compete with a seller who knows the entire future input sequence (supplied manuscript, §§1–2).
The distinction between knowing inputs and knowing random outcomes matters. The benchmark knows which customers will arrive and when, but it cannot see their future choices or the realized lengths of future rentals. The question therefore compares two adaptive stochastic policies operating under different information about fixed inputs.
Let be a finite product set, with arbitrary finite capacities . An assortment is a subset of , so multiple available units do not create multiple appearances of the same product in an offer. A fixed family describes feasible assortments. The empty assortment is available for rejection. No downward-closure assumption is imposed.
Customer arrives at epoch with type . The finite sequence of epochs is nondecreasing and can have arbitrary real spacing. Conditional on the offer , the customer selects with probability , or makes no purchase. These probabilities sum to one and vanish on unoffered products. The source's regularity assumption says that whenever (Assumption 1, p. 4).
Every new rental of product uses a fresh duration with law , independent of earlier rental samples and the choice draw. The law depends on the product, not the customer. Its duration may be zero, unbounded, or infinite. A rental begun at with duration occupies one unit until . The product is available if fewer than units remain occupied. Its full rental fee is a measurable integrable real function , with nonnegative finite mean . Full fees are counted even when the rental extends past the last arrival (model, p. 5).
Write . The myopic policy chooses a feasible available assortment maximizing this quantity at every arrival. Let be the expected sum of these conditional revenues under the operational law of policy . Let be the supremum over all measurable randomized history policies that know the fixed input sequence and duration laws, but not future draws. The main target retains the exact printed assertion:
This is Theorem 1 of the supplied manuscript, printed/PDF p. 11. Three source milestones accompany it. Proposition 1 states that replacing each unit by a labeled product preserves both OPT and the corresponding ALG value. Lemma 1 states that the FIFO duration coupling supplies the comparator with its product-specific i.i.d. usage laws. Lemma 2 asserts
where is ALG's available set and is the comparator's actual full offer. All three statements retain the standing model assumptions (pp. 9–13).
A valid one-half guarantee would quantify the revenue cost of using only current demand information, without requiring large capacities, a special choice model, or a parametric duration distribution. A precise formalization makes the benchmark, information constraints and feasibility assumptions independently inspectable.
The printed domain has a concrete counterexample. With two unit-capacity products, feasible offers only and , fees one, arrival epochs , and deterministic durations for and for , let the first customer choose and every later customer choose whenever offered. These laws are regular on all subsets. ALG earns one; a clairvoyant policy rejects the first customer and earns three. Thus . The target preserves the printed claim, and the finding is recorded separately; the mission does not insert downward closure as a repair. The declarations are compiled statements awaiting proofs or disproofs, not machine-checked proofs of the source.
Reusable inventory can increase after a return, and the return times depend on earlier random allocations. Policies can therefore face different available sets even on the same customer sequence. General duration laws also prevent replacing the process with a finite collection of possible rental lengths. Clipping durations would change duration-dependent fees.
The source's FIFO construction raises a separate conditional-law question: a sample already observed in one execution is reused in another. Its validity concerns the second policy's own information, not independence from the full joint history. An additional finding concerns a displayed equality in Lemma 2's proof: the probability of selecting a product from a reduced offer need not equal the indicator expectation for a choice made from the full offer. The feasibility counterexample and the proof-equality discrepancy are documented with numerical evidence, without replacing the printed targets.
The definition layer separates finite choice laws, measurable randomized decision rules and FIFO operations from the physical rental model. Independent uniform seeds and general Borel duration measures generate a genuine finite product probability space. A sequential run computes offers and rentals from histories; it never takes a revenue guarantee as input. No finite-support restriction is placed on durations or fees.
Arrival indices and clone labels start at zero. Time can be translated to nonnegative epochs without changing returns. Durations are revealed after allocation, returns at the current epoch precede the next ordered offer, and an empty offer gives no sale. Arbitrary measurable maximizing tie selections are represented. Zero-product, zero-horizon, zero-capacity and zero-mean-fee cases are included and disclosed as extensions. The comparator class contains rejection and has a finite uniform revenue bound, so its real supremum has its intended meaning.
Contributions can establish the operational measure identities, resolve the source milestones, or formally certify the recorded counterexample. General decision-rule and sampling infrastructure can be reused independently of this assortment model. The later independent audit is separate from this local statement-drafting pass.
published citation basis are retained; the revision year and final journal pagination have not been verified. Source SHA-256: 010bfd31379607cd3116a6d2cf07a54f6a3c648d23304d77ff19aad293efc9ac. Printed manuscript pages and PDF pages agree.In complementary sourcing, a product's value depends on the efforts of both a supplier and a manufacturer, and each firm's effort raises the marginal value of the other's. Chip lithography is a standard example: an equipment maker and a chip maker each invest heavily, and neither investment pays without the other. When firms invest in sequence, the classical result of Gal-Or (1985) applies: if the firms' choices are strategic complements, the second mover has the advantage, because it can under-invest and free ride on the first mover's commitment. This first-mover disadvantage predicts that neither firm wants to invest first.
Wang, Yin, Chen and Webster (2022) ask whether that prediction survives two features of practice: the first mover invests before knowing the state of the market, and it can set the wholesale price. Their answer is that market risk, which looks like one more burden on the first mover, can reverse the disadvantage. The published version is in Manufacturing & Service Operations Management. This mission formalizes the reversal theorem of the SSRN version.
Two firms contribute efforts , at quadratic cost each. Demand is
where measures complementarity, scales the market, and is the market risk, a cap on what performance can sell. The market risk takes the values and with probability each, with and . Each unit sold yields profit , split as to the supplier and to the manufacturer.
In Model (M) the manufacturer moves first: it chooses and before is known. The supplier then observes and the realized , and chooses to maximize . The manufacturer maximizes its expected margin net of its one-time cost:
In Model (S) the roles are exchanged: the supplier chooses and first, and the manufacturer responds to the realized . Write and for the two firms' expected profits at an equilibrium of each model. Equilibrium means subgame perfection: the second mover best-responds to every feasible first move in every realization.
If and , then for every equilibrium of each model,
Both firms strictly prefer to move first, for every .
The result itself. Theorem 2 says that the classical ranking of the two positions is not a structural feature of complementary efforts: under a two-point market risk and an endogenous wholesale price, it reverses on an explicit region of parameters. The reversal covers both firms and every complementarity . In the paper's benchmark without market risk the first-mover disadvantage largely persists, so the risk term is what changes the conclusion. Corollary 3 adds that the total expected profit of the chain is the same in both models, so the choice of leader only redistributes profit.
Formalizing it. The result is proved in the paper, with the details omitted and delegated to a general discrete case. None of it has a machine-checked proof. The mission produces a complete solution of a two-stage game with a kinked payoff, not only its final inequality, and it records one step the page leaves implicit: the strict inequality the goal needs, where the page's sufficient step is non-strict.
The second-stage problem is an easy concave maximization. The obstacle is the first stage. The manufacturer's expected profit is piecewise in , with regions cut by against and by the user experience against the two caps, and it is neither concave nor differentiable on the whole feasible set. Maximizing the uncapped expression and clipping the answer does not work, since the optimum sits on a kink. The equilibrium statements also ask for the unique global optimum, so a comparison of candidate values is not enough.
A second trap is the transfer to Model (S). The paper obtains it from the substitution , but here Model (S) is a separate definition, so the correspondence between the two games has to be proved.
Efforts and prices are real numbers. The feasible sets are and , and the expectation is the explicit sum with weights . A general leader–follower game with a revealed state is its own definition (StackelbergGame), with IsFollowerStrategy and IsEquilibrium, and Model (M) and Model (S) are instances of it. The second mover's strategy is a function of the first move and the state, so off-path behaviour is part of the equilibrium. Best responses are maximizer predicates, never the closed form. The candidates are reals constrained by their defining equations, which Lemma 3 pins down. The index takes values in Fin 2.
The goal is not trivialized by these choices. It quantifies over all equilibria of definitions that are satisfiable: the instance , , , , has explicit equilibria in both models, and the condition excludes the degenerate case in which Lean's would admit a game with zero profit.
Only Mathlib's real analysis is needed. The StackelbergGame layer is reusable for other sequential supply-chain models. The general discrete case of the paper (Theorem A1 for any ) and the fixed-price, persistent-risk and endogenous-retail-price variants are outside this mission. Proofs of the milestones and alternative routes to the goal are welcome, as is a removal of the hypothesis , which numerical checks suggest is unnecessary.
A firm that enters a new market first does not know how profitable that market is, and neither does its rival. The rival watches the first mover's earnings, learns from them, and decides when to follow and how large to enter. The first mover therefore controls not only its own profit but also what its competitor learns: a small investment caps its earnings and censors the signal the rival observes. Sunar, Yu and Kulkarni (SSRN 3408260; published in Operations Research, 2021, doi:10.1287/opre.2020.2080) model this as a continuous-time leader–follower game with Bayesian learning, in which both the follower's entry time and both firms' investment sizes are decisions.
The earlier literature on investment games under incomplete information (Kwon 2010, Kwon and Lippman 2011, Kwon et al. 2015) models a firm's earnings as a Brownian motion with an unknown drift, with no size decision. The size decision is what makes the leader's investment an information-design tool, and it produces the result this mission formalizes: in some markets, a more optimistic prior makes the leader worse off in equilibrium.
The market is favorable () or unfavorable (); both firms start from the prior . The parameters are a discount rate , unit investment costs , and earning potentials of firm after entry, with , (Params, Params.Standing).
The leader invests a size at time , at cost . Until the follower enters, its cumulative earnings are
with and volatility . The follower observes , updates its posterior belief , and chooses a stopping time and a size , paying at . After entry the drifts become and , with independent noises. The follower maximizes its expected discounted profit (7). The leader maximizes (8) knowing the follower's best response, and its equilibrium value is
where (15) is the leader's profit against the follower's optimal policy (leaderPayoff, V1).
The signal quality is zero for : a small leader reveals nothing. For the follower uses a two-threshold policy: it waits while and then invests or .
Assume the standing assumptions, , and
Then there is such that for every there is with
for every selection of follower best responses, whose existence is part of the claim.
Theorem 4 is the paper's headline: under conditions (30), which favor the follower, the leader's equilibrium profit strictly decreases in the prior near . As the market looks better, the leader enlarges its investment to sharpen the signal and delay the follower, and that costs more than the delay gains. Optimism is costly to a first mover when the follower's prospects are strong.
The printed theorem is false without a relation between the costs. With , , , , , , , every standing assumption and (30) hold, with the proof's constants. Yet for the size earns , while every earns at most plus a pre-entry gain that vanishes as by Proposition 3(a). So for large , near and . The proof's Step C asserts that the leader's equilibrium size at exceeds , which needs . The mission adds the minimal hypothesis (the paper's Figure 2 uses ). Lemma EC.8(b) is also corrected: at the maximizer of is not unique.
Nothing in this paper has a machine-checked proof. The paper's own proof of Theorem 4 is an envelope-theorem argument. It assumes is differentiable, takes limits of -dependent maximizers, and sets aside a parameter set of measure zero, which the stated goal does not exclude. A formal proof would settle the corrected theorem, and the milestones (a Bayesian filter for a binary drift, a verification theorem for a two-threshold stopping problem) are reusable well beyond this model.
The obvious route to Theorem 4 is to write as the maximum (26) of the closed forms , and differentiate. That route fails in several places. The thresholds have no closed form; they are defined implicitly by smooth pasting. The maximizer is not known explicitly. Its limit as is not shown to exist. is a supremum of functions, so it is differentiable only where the envelope argument applies. Below the goal, Propositions 1–2 are a verification theorem for optimal stopping of the belief diffusion . They need Itô's formula for , piecewise functions, which Mathlib does not yet have, and the existence of the smooth-pasting thresholds is an intermediate-value argument on a two-parameter family of ODE solutions.
IsBrownianReal, unit variance, measurable, continuous paths) and an independent uniform . The market state is , so every prior lives on one space and is a function of .discInt), equal to the Itô integral for this deterministic integrand. .WithTop ℝ≥0. Sizes are -measurable and nonnegative.sSup. The goal holds for every selection of follower best responses and asserts that best responses exist, so it is not vacuous. Statements about hold for every pair of optimal thresholds (IsOptimalThresholds).The infrastructure is reusable: a likelihood-ratio filter for a Brownian motion with binary drift, the hitting time of a closed set by a continuous adapted process as a stopping time, and a verification theorem for discounted optimal stopping of a one-dimensional diffusion. Contributions to any of these, or proofs of the closed-form milestones (EC.2)–(EC.4), (EC.79) and Lemma EC.8, are welcome.
A multi-objective optimization problem minimizes several objective functions over one feasible set. The objectives rarely share a minimizer, so the usual targets are Pareto points, where no objective can be improved without worsening another, and weakly Pareto points, where the objectives cannot all be improved at once. Such problems arise in economics, finance, medical science and machine learning; the introduction of the paper below gives references, and Ehrgott's Multicriteria Optimization (Springer, 2005) is a standard account.
Nie and Yang (arXiv:2108.04336v2) study the case in which all functions are polynomials. Their first contribution is geometric: the set of Pareto values is described as the boundary of a convex set given by moments. The description matters because Moment-SOS methods can optimize over moments, while the image of the feasible set is usually not accessible directly.
Fix real polynomials in , and polynomials (), () indexed by disjoint finite label sets. The problem (1.1) is
Its feasible set is . A point is a Pareto point if no has for all and for some . It is a weakly Pareto point if no has for all . A Pareto value or weakly Pareto value is for such a point. The epigraph set is
Write . A truncated multisequence of degree is a vector . It acts on polynomials of degree at most by . The moment cone is
for Borel measures on and . The nonnegative polynomial cone is the set of polynomials of degree at most that are nonnegative on . With the maximum degree of the objectives,
Assume has nonempty interior. Then
and, when is convex, a vector is a weakly Pareto value if and only if lies on the boundary of . Both clauses are one statement.
The milestones follow the paper's proof. They give the orthant form of and the nonnegativity of supporting normals; Proposition 3.1(i)–(ii); the linear program (3.2) with value and its dual (3.3) with value ; the identification of as the dual cone of ; nonempty interior of ; the equality ; the equivalence between in (3.3) and ; the description of by ; and the passage from the boundary of to the boundary of .
The result. Theorem 3.2 replaces the image , which has no usable description, by moment conditions that are linear in . Under SOS convexity the moment cone can then be replaced by a semidefinite representation (Theorem 3.3 of the paper), so the front becomes the boundary of a spectrahedral shadow.
The formalization. The theorem is proved on paper; no machine-checked proof is known to exist. The mission adds the first definitions of the moment cone, the truncated pairing, and Pareto values for polynomial problems to the platform, together with a checked proof.
One sentence of the printed proof needs repair. The proof says that lies in if and only if no supporting hyperplane for passes through . By the definition on p.6 a supporting hyperplane through needs , so the sentence fails outside . For , , and , no supporting hyperplane passes through , and is not interior. What the argument needs is a weakly separating hyperplane, and the conclusion the paper draws from the sentence is true for every . The milestone on states that conclusion and is marked as corrected. The goal is unaffected, as Theorem 3.2 holds as printed.
The core is a conic duality between a cone of polynomials and a cone of moment vectors. The moment cone need not be closed when is unbounded, so the dual program (3.3) lives over , and must be recovered with in the cone itself. A point of the closure need not have a representing measure. Mathlib has separation theorems and the bipolar theorem for cones, but no Slater theorem for conic programs, so the zero duality gap must be derived from separation. The obvious shortcut of identifying with moment means runs into the same closure: a mean of under a measure lies in the closure of , not obviously in the set itself. Unbounded and non-compact are the general case.
is Fin n → ℝ, and the data of (1.1) is a structure MOP n m E I with finite types E, I for the disjoint label sets. Neither nor is bounded in the goal. The index set is the finite subtype of Fin n →₀ ℕ of degree at most , and a tms is a function on it, with the product topology. The degree in is computed from the objectives. The moment cone requires that each monomial of degree at most be -integrable; without this, Lean's value for non-integrable functions would change . The optimal values , are a supremum and an infimum in EReal, so that "negative or infeasible" is exactly . The programs (3.2), (3.3) are taken for every , as the proof uses them, and the milestones about them assume , since (3.3) is meaningless at .
Convexity of is a hypothesis on . It is not replaced by convexity of the and , which the paper notes is sufficient but not necessary. Nothing is defined through , because that would hide the theorem.
The moment cone, the pairing and the dual-cone identity are reusable for polynomial optimization beyond this mission. Contributions are welcome on any milestone. A proof of the goal that avoids strong duality is welcome as well, and the moment-cone lemmas it would need are of independent use. The hypothesis that has nonempty interior is kept as the paper states it, though it forces every equality constraint to vanish identically.
In the classical secretary problem a known number of candidates is interviewed in uniformly random order, and each candidate must be accepted or rejected on the spot; the goal is to hire the best one. Its optimal rule (reject the first candidates, then accept the first one better than all before) and its success probability are classical (Dynkin 1963; Gilbert and Mosteller 1966; survey by Ferguson 1989).
Many online selection problems in operations research, such as hiring, job scheduling and online marketplaces, do not force an immediate decision: a candidate stays for some time and the decision can be postponed until the candidate is about to leave. Kesselheim, Psomas and Vardi introduce the stochastic departure secretary problem, in which candidates arrive at random times and leave after random waiting times, and the decision on a candidate is taken when the candidate departs. Earlier variants with recall or sliding windows (Goldys 1978; Ho and Krishnan 2015; Vardi 2015; all cited in the paper's §1.4) all have optimal rules that depend only on the number of candidates seen. With stochastic departures the time of the decision matters as well.
There are candidates. Each candidate has an arrival time , drawn independently from an arrival distribution on , and a non-negative waiting time , drawn i.i.d. from a waiting time distribution . Its departure time is . The candidates are totally ordered, the order is uniformly random and independent of the times, and the goal is to select the best candidate.
At time the history consists of the arrival times of the candidates that have arrived by , their departure times if they have departed by , and their relative order. is the number of candidates that have arrived by , and the best-so-far candidate at is the best among them. Whenever a candidate departs, a policy must irrevocably accept or reject it, based only on the history until that time. The policy succeeds if the candidate it accepts is the best overall.
A policy is bivariate (Definition 3) if there is a function such that a departing candidate is accepted iff it is the best-so-far and .
There is a function such that
It holds for every , every arrival distribution on (atoms allowed) and every waiting time distribution on , and optimality is against every admissible policy.
Theorem 1 reduces the search for an optimal policy, a priori a function of the whole history (arrival times, departure times, relative ranks), to a function of two numbers. This makes the optimal policy computable by a two-dimensional dynamic program, and it is the starting point of the paper's second result (Theorem 2, not part of this mission): for continuous arrivals a single time threshold, independent of , is asymptotically optimal. The paper's examples show that both arguments of are needed, and that monotonicity in time can fail for non-uniform arrivals.
The results are proved in the paper; none of them has a machine-checked proof. The mission produces a formal model of continuous-time online selection with random arrivals and departures, histories and nonanticipating randomized policies, which is reusable for other stochastic secretary and prophet variants.
The class of competitors is the hard part. An admissible policy may depend on the entire history, including arrival and departure times of candidates who are still present or have left. The obvious argument, "the future depends only on and ", does not settle the matter: it must be shown that no information in the history (for instance, that some earlier candidate has not yet departed) changes the continuation value. The paper does this by a coupling and simulation argument that rewrites one history coordinate at a time, resampling a waiting time conditionally when a departure is erased.
Monotonicity in requires comparing continuation problems with different numbers of remaining arrivals; the paper simulates a phantom candidate. Monotonicity in time uses a linear rescaling of onto that preserves uniform arrivals but stretches waiting times, which is why it holds only for uniform . Conditioning on the event that a best-so-far candidate departs at exactly time has probability zero for continuous distributions, so every conditional probability in the paper has to be given a measure-theoretic meaning.
The sample space is : arrival times and waiting times indexed by fixed labels , a uniformly random permutation ( is the best), and a uniform seed available for randomized policies, all independent. Departure times are capped at , so simultaneous departures at time are generic; a decision names at most one candidate per instant and only the first acceptance counts. counts arrivals at time itself. Histories are an equivalence relation on outcomes, and a policy is admissible if its decision at is constant on history classes and its acceptance events are measurable. Optimality is stated against all admissible policies, not through a supremum. The value of rejecting is a supremum of success probabilities conditioned on over policies that never accept a candidate arrived by , and it equals at states of probability zero.
Restricting the comparison class to bivariate or threshold policies would make the optimality clause trivial and is ruled out: the goal quantifies over every admissible policy, including randomized and label-aware ones.
A complete development needs product measures and conditional measures (Mathlib), exchangeability of the uniform order, a measurable-selection or dynamic-programming argument for the lazy policy, and the coupling constructions of Lemmas 9, 10 and 12. Contributions are welcome on any milestone and on general lemmas about the model (for example, that the history until determines the history until every ).
Proof-of-work blockchains such as Bitcoin pay a reward to whoever first solves a hashing puzzle. The protocol adjusts the difficulty so that rewards arrive at a roughly constant rate for the system as a whole, about one every ten minutes, and a miner's chance of winning the next reward is proportional to its share of the total hash rate. Mining is costly (hardware and electricity), so each miner trades a higher reward rate against a higher running cost, and the trade-off depends on what everyone else does. How much computing power such a market attracts, and whether richer miners crowd out poorer ones, are questions about the equilibrium of this game.
Li, Reppen and Sircar (arXiv:1912.01952v2, 2022; Management Science, 2024) model the miners as a continuum in a mean field game in which each miner controls the intensity of its own reward process. For exponential (CARA) utility they solve the game in closed form, which they describe as one of the few explicit mean field game equilibria outside the linear-quadratic setting (p.5). This mission formalizes that solution, Proposition 3.1.
The model has a system reward intensity , a cost per unit of hash rate per unit of time, a reward value , a risk aversion , a number of other miners ( miners in total) and a period . Utility of terminal wealth is , and
A mean hash rate is a measurable function of time, positive on . A miner who uses hash rate receives rewards at the jumps of a counting process with intensity
and its wealth evolves as . A control is a non-anticipating rule giving the hash rate at time after rewards received at times . The counting process is built from i.i.d. clocks: the next reward comes when the accumulated intensity since the last one reaches the next clock.
The value function is
over all controls of the miner started at time with wealth . With and , the optimal hash rate (2.6) is
Given a law of initial wealth at , is an equilibrium mean hash rate (2.8) if is differentiable, some family of controls realizes the feedback along almost every path, and for every , where is the law of the closed-loop wealth .
With :
and the constant hash rate attains this supremum.
The proposition gives a complete, wealth-independent description of the market under exponential utility. Every miner hashes at the same rate, total hashing is at most whatever the reward size (Remark 3.3), and each miner's reward rate is discounted by competition to . The paper uses the explicit solution to benchmark its numerical method (§3.1.3) and as the contrast case for power utility, where wealth effects and a hashing cutoff appear (Proposition 3.5).
The paper's proof guesses the product form of , assumes that is a classical solution of the HJB equation, and solves an ODE. It never proves that the HJB solution is the value of the control problem, and it shows uniqueness only within the class of value functions of product form (p.12: "the unique equilibrium (in a given class)"). The mission states the result for the genuine stochastic control problem over history-dependent controls and claims uniqueness among all equilibria. Both strengthenings are true, and both need proofs that the paper does not give. No machine-checked version of this result is known to exist.
The algebra (the maximizer, the fixed point , the ODE for ) is elementary. The difficulty is the stochastic control layer:
All objects live in the namespace CryptoMiningMFG.
Model bundles with positivity and . is real.Control) are measurable, locally integrable, nonnegative rules of time and the miner's own reward history. They do not depend on the starting wealth. The reward process (RewardProcess) uses the clock law Measure.infinitePi (fun _ => expMeasure 1), and the intensity is (2.2) literally, including its branch, during the mining period (it is outside it).costExp is as a lower Lebesgue integral in , set to on the null event of infinitely many rewards by . value is times the real part of its infimum over controls, which is at most and so finite. No Bochner integral of is used: it would return for non-integrable controls and beat every genuine control.optRate is (2.6) on value, with deriv for . IsEquilibrium contains the differentiability clause, the realized feedback (almost every path, almost every time) and the consistency condition (2.8) against the law of under independent of the clocks. is any probability measure.A complete development needs a compensator or martingale toolkit for counting processes driven by exponential clocks, which is reusable for other intensity-control problems (dynamic pricing, queueing control). Proofs of any milestone, alternative verification arguments, and lemmas on the reward process (non-explosion, , the Poisson law under a constant rate) are welcome.
Manufacturers of phones, appliances and packaging increasingly take back used products and remanufacture them, paying consumers a recycling reward (a trade-in credit or gift card). Whether a consumer returns a used product depends not only on money and effort but on social feelings: the pride of recycling when others do not, and the guilt of not recycling when others do. Operations management has studied closed-loop supply chains with exogenous return rates since Savaskan, Bhattacharya and Van Wassenhove (Management Science 2004). Huang, Nguyen, Tseng, Chen and Kirshner (M&SOM 2024) make the return rate endogenous. It is the evolutionarily stable outcome of a game among consumers, following the social-comparison model of Mai and Hu (2023). They then ask how stronger pride or stronger guilt changes the manufacturer's optimal profit. The answer is not monotone in guilt, and this mission formalizes it.
A consumer either recycles or not. With recycling reward , recycling cost , intrinsic pride and intrinsic guilt , and with social pride and social guilt felt when meeting a consumer of the other type, the expected utilities at recycling rate are
A rate is a stable equilibrium (Definition 1) if and , or and , or with and . With and the indifference rate , Lemma 1 gives the equilibrium rate . It is for low rewards, for high ones and in between when . When , the initial share decides between and .
The manufacturer sets a price and the reward . The consumers' average equilibrium utility enters the demand
New units cost and remanufactured units . With , the profit is
The benchmark without remanufacturing has demand and optimal profit , and the paper assumes . The optimal profit is
The quantity is the difficulty of remanufacturing. The region
forces . There the optimum induces the interior rate (Proposition 5).
At every point of under the standing assumptions, has partial derivatives in and , and
The Lean statement keeps each branch of (ii) and (iii) as an implication, as printed, and each "i.e." as an equivalence. The thresholds are explicit expressions in the parameters.
Theorem 2 is the paper's main managerial result. Pride always helps a remanufacturer whose products are moderately hard to recycle. Guilt helps only once the induced recycling rate is high enough relative to how strongly consumers' utility drives demand (). This is the basis for the paper's advice on when to advertise the pride of recycling and when to stress the guilt of not recycling.
Neither the paper nor any platform item machine-checks these results. The proofs (Appendix A) are in the journal's e-companion. The mission formalizes the whole chain: the equilibrium analysis, the optimization of a three-branch piecewise objective, and the comparative statics of an optimal value. Together they give the platform a first evolutionary-game recycling model and an explicitly solved closed-loop supply chain pricing problem.
The obvious argument differentiates the closed form (10) and reads off the signs. That covers only the last step. Theorem 2 is about the optimal value , a supremum over of a profit that is piecewise in through . Three things must be shown on the open set . The inner supremum over under nonnegative demand has a closed form. The interior branch of beats both boundary branches. And the resulting value equals (10) on a neighborhood, so that the partial derivatives of are those of (10). The boundary branches compare differently depending on whether or , and may be negative. Finally, the sign conditions are rational inequalities in that have to be matched exactly with the thresholds on .
All parameters are real numbers, bundled as PrideGuilt.Params, and the standing assumptions are PrideGuilt.Standing. These are , , , , and . Each theorem adds (and where the region does not imply it). and are explicit arguments of every function, and the partial derivatives are deriv of one-variable sections of optProfit. Differentiability is part of the conclusion, so Lean's default value of deriv cannot satisfy the sign claims vacuously.
The demand constraint in the supremum is a correction of (5). As printed, (5) is an unconstrained maximum. A negative demand times a negative margin then counts as profit, which makes the maximum and Theorem 2 false. A counterexample in is , , , , , , , . The paper itself requires feasible demand (footnote 4, p.13). Prices and rewards range over all of . is the Lemma 1 formula. Lemma 1 is corrected at the two endpoints where Definition 1 admits no stable equilibrium.
The development needs only Mathlib real analysis (sSup, IsGreatest, deriv). Proofs of any milestone are welcome, as are lemmas on the inner optimum over prices with nonnegative demand. That optimum is reusable for any linear-demand pricing model.
In a game of incomplete information each player learns a private type and then acts. Two equilibrium notions coexist. A Bayesian (interim) equilibrium asks every type of every player to best-respond given its beliefs. A Harsányi (ex ante) equilibrium asks each player to choose a strategy for all of their types at once that is optimal on average under their prior. With finitely many states the two coincide (Harsanyi 1967). With a continuum of states they can come apart: Simon (2003) built a game with no measurable Bayesian equilibrium, and Hellman (2014) one with no measurable Bayesian ε-equilibrium for small ε.
Hellman and Levy locate the divergence precisely in the hierarchy of countable Borel equivalence relations (CBERs), applied to the common knowledge relation of the game.
A Borel relation on a standard Borel space is one whose graph is a measurable subset of . A CBER is a Borel equivalence relation all of whose classes are countable. A CBER is smooth if a Borel map satisfies , and hyperfinite if for an increasing sequence of Borel equivalence relations with finite classes.
A purely atomic Bayesian game has a finite non-empty set of players, a standard Borel state space , finite non-empty action sets , and for each player :
The common knowledge relation ckRel B is the equivalence relation generated by . A strategy is Borel and constant on -classes. With the payoff of type (eq. (3.1)), the gain from deviating at is .
A graphical game has a Borel graph of countable degree on , an action set , and bounded payoffs that depend only on the actions of and its neighbours, are continuous in the Tychonoff topology, and are Borel along Borel profiles. Each Bayesian game with a common action set has an associated graphical game on the type space with measure .
If ckRel B is hyperfinite, then for every there is a strategy profile with
Action sets may differ between players, and each player has their own prior.
Three printed statements are false as stated and are formalized in corrected form:
The theorem shows that hyperfiniteness, the rung just above smoothness, is not an obstacle to ex ante approximate equilibrium, although it is an obstacle to measurable interim ε-equilibrium (Hellman 2014). Together with the smooth case it fixes the first two rungs of a correspondence between descriptive set theory and equilibrium existence, and it makes treeability the open frontier. The graphical-game results (Propositions 4.10 and 4.11) also stand on their own: they are existence theorems for games played by a continuum of players on a Borel network.
The result is proved in the paper. As far as is known, none of it is formalized. A complete development would give machine-checked proofs of the main theorem and of every milestone. It would also check the steps the paper leaves informal: the reduction to a common action set, which the paper says it omits, and the measurability claims called "immediate".
The obvious route is to find a Bayesian ε-equilibrium, which is itself a Harsányi ε-equilibrium. That route is closed: Hellman (2014) gives a hyperfinite game with no measurable one. A Harsányi equilibrium must instead trade off types against each other, and nothing in the game singles out which types to sacrifice. Hyperfiniteness only says the common knowledge relation is a limit of finite relations, while each player's payoff may still depend on infinitely many other types. The difficulty is to connect the finite approximations to the original game while keeping the strategies Borel at every stage. Lusin–Novikov uniformization is used repeatedly for this.
Lean conventions: state and vertex spaces are standard Borel (Polish spaces with their Borel σ-algebras are a special case). carries the Giry σ-algebra. Mixed actions are PMFs. Smoothness uses a Borel map into , and hyperfiniteness is the increasing-union form, with no measure and no null sets. The conditional payoff is an integral against the type, which equals the paper's countable sum. Every "" carries an integrability clause, so a non-integrable gain cannot pass with Bochner integral . Strategies must be both Borel and constant on knowledge classes. Dropping either requirement trivializes the notion: without invariance a strategy can read the state, and without measurability the non-measurable equilibria of Simon and Hellman become admissible. The strong Bayesian notion uses one exceptional set for all players. The graphical measures in Propositions 4.10–4.11 may be any finite measure.
A complete development needs a Borel CBER library (smooth, hyperfinite, quotients, finite subrelations) that is reusable well beyond game theory. It also needs the Lusin–Novikov theorems: LusinNovikov.exists_measurable_uniformization_of_countable_sections and LusinNovikov.exists_disjoint_injOn_fst_iUnion_eq_of_countable_sections are already proved on the platform. Further pieces are measurability of integrals against product measures over countably many coordinates, and Theorem 3.5, which is cited and may be proved or taken as a separate target. Contributions to any of these layers are welcome, as are proofs of individual milestones.
Probability distortion models the empirical tendency, documented by Kahneman and Tversky and central to rank-dependent utility and cumulative prospect theory, to overweight small probabilities and underweight large ones. A distortion function is applied to the survival function of a payoff, and the distorted expectation
replaces the ordinary expectation . This nonlinear expectation is neither sub- nor super-additive, so it lies outside Peng's framework of sublinear expectations.
The difficulty appears in dynamic problems. The naive conditional version violates the tower property already on a two-period binomial tree (Example 2.7 of the paper). This is the time-inconsistency that drives the literature on precommitment and equilibrium strategies under distortion (Ekeland–Lazrak, Björk–Murgoci, Hu–Jin–Zhou). Ma, Wong and Zhang (arXiv:1809.08262, Math. Oper. Res. 2021) follow the dynamic-utility idea of Karnam–Ma–Zhang: let the distortion depend on the current time, the horizon and the current state, and ask whether it can be chosen so that the tower property holds while the time- expectation is the prescribed distorted one. This mission formalizes their discrete-time answer.
Distortion function. A map that is continuous, strictly increasing, with , . The class consists of the functions that are bounded, continuous and (non-strictly) increasing.
The tree. Fix and times . At time the process takes values ; from it moves to with probability and to with probability , where . The filtration is the one generated by . Distortion functions are given, describing the time- perception of events at each future time, and .
Survival probabilities and the distorted probability. , , and
is the probability under which moves up from with probability . The standing condition (3.14) is .
Dynamic distortion function. A map , for in the time set, , , that is jointly Lebesgue measurable in and a distortion function in . Its conditional nonlinear expectation is
and is time-consistent if for all and .
Under (3.14) there exists a time-consistent dynamic distortion function with for such that, for all , , ,
and for (3.12). Conversely, every time-consistent dynamic distortion function with the same initial condition satisfies (3.17) and (3.12): it is unique at the conditional survival probabilities. The goal is the discrete main result of the paper; its continuous-time counterpart, Theorem 4.7, is not part of this mission.
The theorem gives a conditional expectation under probability distortion that equals the distorted expectation at time , obeys the tower property, and is linear on : it is the ordinary conditional expectation under the explicit measure . Dynamic programming arguments under distortion can therefore be run as linear backward recursions under , which is the starting point of the paper's continuous-time PDE characterization. Uniqueness shows that no other time-consistent choice with the same time- perception exists on the tree, so is forced, not chosen.
The result is proved in the paper; no machine-checked proof exists. A formal proof would supply the details the paper calls "obvious" or "straightforward" (the Markov computation of , the interpolation, and the separation of node weights by functions in ) and a reusable layer for distorted expectations of finitely valued random variables.
The obvious construction, a fixed distortion applied to conditional probabilities, is time-inconsistent, so the dynamic distortion must be built from both the - and the -survival functions. Existence needs three facts to fit together: reproduces the distorted survival function at every time (3.18), the conditional survival probabilities under and have the same order and the same zeros and ones at each node, and the inner expectation is again an increasing function of , so that time-consistency, which is only required on , applies to it. Uniqueness has to extract the one-step distortions from the tower property tested on all of , which requires functions in that separate the weights of consecutive nodes. The recombining structure and the monotonicity of the nodes are essential: Example 3.2 of the paper shows that on a tree with crossing edges no time-consistent exists in general.
The tree is realized on the canonical path space Fin N → Bool (true is an up-move); where is the number of up-moves before , and a path has probability . Times are indices . is generated by the sets of paths that agree in the first moves, and conditioning on at is conditioning on . Identities between random variables are stated at every path; every path has positive probability. The integrals (1.2) and (2.11) are Bochner integrals over , finite for the bounded variables they are applied to. Lebesgue measurability in Definition 2.8 is null-measurability for the Lebesgue measure on . The given family is indexed by , and is built in.
The uniqueness clause quantifies over all time-consistent dynamic distortion functions with the initial condition; it does not assume (3.17), so it is not tautological, and the existence clause asserts the existence of without naming the interpolant. Proposition 2.5(i)'s formula (2.3) is stated for real-valued , because the proof of Theorem 3.4 applies it to , whose nodes may be negative.
A complete development needs finite sums over paths, the Markov property of the path weights, a layer-cake computation of the Bochner integral for step functions, and piecewise-linear interpolation of finitely many points. The distorted-expectation layer (Proposition 2.5(i)) is reusable for rank-dependent utility and distortion risk measures. Proofs of any milestone, and alternative routes to uniqueness, are welcome.
Mean-field games (MFGs) approximate stochastic games with many identical, interchangeable players by a single representative player who interacts with the distribution of the population (Huang, Malhamé, Caines 2006; Lasry, Lions 2007). In applications such as online ad auctions the reward and the dynamics are not known in closed form, and the equilibrium has to be learned from a simulator. Guo, Hu, Xu and Zhang (arXiv:2003.06069v3) set up a general mean-field game (GMFG), in which reward and transition depend on the joint state-action distribution of the population, and give a learning algorithm with a convergence and sample-complexity guarantee. Its stabilizing devices, softmax smoothing and projection onto a finite net, have been taken up in later work on learning in MFGs, for example by Cui and Koeppl and by Anahtarcı et al. (cited on p.3 of the paper).
The state space and the action space are compact metric spaces with their Borel -fields; is the set of Borel probability measures on . A population state-action law is , with state marginal . A GMFG has a measurable transition law , a measurable mean reward , and a discount factor .
A policy is a measurable map . For fixed , the value is with and . A stationary Nash equilibrium (Definition 1) is a pair such that maximizes at every state, and the state-action law of the player who starts from and plays equals at every time.
Distances between laws are measured by the Wasserstein distance : the infimum of the expected transport cost over couplings. On the cost is the product distance . Policies are compared by .
The equilibrium is a fixed point of a composite map. selects one optimal policy against ; is the state-action law after one step of play from ; and . Assumption 1 asks , and Assumption 2 asks to be -Lipschitz in the policy and -Lipschitz in the law.
For finite , is the optimal Q-function of the MDP with transition and reward , and , the uniform law on the maximizing actions. The algorithm GMF-V (Algorithm 2) starts from any . At step it obtains an estimate of from a learner, plays for a smoothed argmax (Lipschitz with constant , within of argmax-e when the gap is ), and sets . Here is a finite -net in total variation whose points have action gap at least .
Let , , , and
There is , depending only on the model and , such that if each estimate fails with probability , then
where . In the same item, the total sample count satisfies
Theorem 1 gives existence and uniqueness of the equilibrium selected by under a contraction condition. Theorem 2 says that any single-agent Q-learner with a polynomial sample guarantee becomes, after smoothing and projection, an algorithm that finds that equilibrium to accuracy with high probability, at a polynomial total sample cost. The constant does not depend on , , or the temperatures. Lemma 2 and Corollary 1 of the paper instantiate the learner with Q-learning.
The results are proved in the paper, not formalized; no machine-checked proof of these statements or of the GMFG layer is known. Several printed statements are false as written and are corrected minimally here, each with a counterexample in the item's difference list. The equilibrium in Theorems 1 and 2 must be the one selected by . must use , because vanishes with a single action. The bound (23) holds without its factor and for . The printed Bellman equation has its maximum outside the sum, and only the equation with the maximum inside has the optimal Q-function as its solution. The hypotheses of Lemmas 6 and 7 are also corrected: the first must be two-sided, and the second has the wrong inequality direction.
The obvious proof of Theorem 1 is "contraction plus Banach". It needs to be a complete metric space for the product cost on general compact metric spaces. That requires the gluing lemma for the triangle inequality and weak compactness for completeness, and Mathlib has neither for this . For Theorem 2, the naive per-step bound fails at the first iterate: is not in the net, so no action gap controls the smoothing error there. The geometric recursion must also be summed with the exponent and tail sums of . Finally, the union bound over iterations has to work with failure events that need not be measurable.
is ProbabilityMeasure X with the Giry -algebra. is a real infimum over couplings with an explicit cost; the product coupling makes it genuine. The model stores the mean reward rather than the reward law. is a discounted sum over state laws built by kernel composition. is the solution of the Bellman optimality equation, which exists and is unique (proved in the verification file). The learner enters Theorem 2 only through the per-iteration failure hypothesis, for random estimates on any probability space; the failure event of the conclusion is bounded in outer measure. is quantified over fixed points of , and precedes every algorithmic parameter. Requiring to lie in the net would make the first step free, and the statement does not assume it.
A complete development needs the metric and completeness theory of on compact metric spaces, the softmax Lipschitz and approximation bounds, and the finite – comparison. The first is reusable well beyond this mission. Contributions of any milestone, and of alternative proofs of the smoothing lemmas, are welcome.
Scenario planning asks a decision maker to consider several possible futures side by side: a world in which a technology matures, one in which regulation tightens, one shaped by a dramatic event. Decision analysts who support such exercises want to run a Bayesian analysis inside each scenario, but the classical foundations of subjective expected utility (Savage; Anscombe–Aumann; DeGroot's qualitative-probability route) axiomatize a single "small world" whose events can be freely combined. In scenario work the worlds may be unrelated, their states and consequences different, and the beliefs and values attached to them held by different stakeholders.
Simon French, Axiomatising the Bayesian Paradigm in Parallel Small Worlds (accepted manuscript of the Operations Research article, doi:10.1287/opre.2019.1896), gives an axiom system for parallel small worlds. Its one shared ingredient is a reference experiment, a uniform randomiser such as a probability wheel. Every likelihood judgement in every world is a comparison with an event of that randomiser, and every utility is elicited by a standard gamble on it. The paper argues that this is how probabilities are elicited in practice, and that it makes probabilities, but not utilities, comparable across scenarios.
For each world there is a set of states , a field of events on , a set of consequences , and a set of acts , functions .
The reference events are the Borel subsets of (RefEvents), the same in every world. A likelihood relation compares elements of the set union : events of the world with each other, reference events with each other, and events with reference events, but never mixed unions of the two.
A simple distribution over has finite support and weights summing to one (SimpleDist); is the point mass at , and gives probability to and to . Compound gambles have prizes that are consequences or simple distributions (Gamble). A preference on consequences extends to on consequences and gambles, and ranks acts. All of these relations are primitive.
Sixteen axioms constrain them: PSW1–PSW6 make a weak order that is a qualitative probability on each of and , uniform on intervals, and consistently comparable across the two (LikelihoodAxioms); PSW7 is monotone continuity, PSW8 governs conditional likelihood; PSW9–PSW15 are von Neumann–Morgenstern-type axioms for (UtilityAxioms); PSW16 says an act is valued as the simple distribution over consequences it induces.
The calibrated probability of an event is
(calib), the length of the reference arc held equally likely to . The subjective expected utility of an act is (actEU).
In every world, under PSW1–PSW6 and PSW9–PSW16 (with the two corrections below), is a finitely additive probability agreeing with , and there is , unique up to positive affine transformations, with
Under PSW7, is countably additive; under PSW8, conditional likelihood is represented by .
The theorem gives a constructive subjective expected utility representation: the probability is the calibration against the reference experiment, and the utility is the standard-gamble probability. Because every world uses the same reference experiment, a probability of means the same degree of belief in every scenario; utilities carry no such common scale (p.33 of the manuscript). This is the property scenario-focused decision analysis needs to compare judgements across scenarios.
Formalization adds three reusable results with explicit hypotheses: a qualitative-probability representation calibrated by a uniform reference experiment (Lemma 1), a von Neumann–Morgenstern expected-utility theorem with uniqueness for simple lotteries (Lemma 2), and the combination into an act-level representation. The paper's proofs are outlines. Checking them exposed two places where a printed axiom is weaker than what the proof uses; both are recorded below with counterexamples. No machine-checked version of these results is on the platform.
The argument is elementary but long, and the obvious shortcuts fail. Showing that exists needs the connectedness of together with the closedness axiom PSW6; the closedness is not decoration. Additivity cannot be read off qualitative probability on alone: it comes from comparing with the half-open reference interval , which is not an interval PSW2 speaks about, so its likelihood has to be derived from PSW2 and PSW4, and the comparison needs the strict form of PSW5(b). Countable additivity needs continuity at the empty set. On the utility side, reducing a simple distribution to one standard gamble needs one substitution (PSW14) per consequence and a single reduction (PSW15), with distinct consequences possibly receiving equal standard-gamble probabilities. The uniqueness of up to positive affine transformations is a separate argument in both directions.
Each world is a SmallWorld Θ C. Events of and reference events are kept apart in Set Θ ⊕ Set ℝ; the paper's single empty set is restored by requiring . PSW2 is imposed for open and closed intervals only, as printed. Probabilities are elements of unitInterval. Compound gambles are one level deep. Every act is assumed to have finite range and events as fibres, which covers both cases of the paper's standing finiteness assumption. The goal is stated for a family of worlds indexed by an arbitrary type.
Two corrections are explicit, separate hypotheses. C1 (CorrectionC1): PSW5(b) also holds with strict conclusions when one premise is strict, as the proof of additivity uses; without it, a two-state example satisfying PSW1–PSW8 as printed has . C2 (CorrectionC2): , as the proof of Lemma 2 uses; without it, a lexicographic order satisfies PSW9–PSW15 and has no utility representation. Lemma 1's uniqueness is stated among probabilities calibrated on the reference experiment, since uniqueness among all agreeing probabilities is false.
The probability in the goal is the definition calib, not "some probability agreeing with ", and none of the relations is defined from a measure or a utility; either shortcut would make the goal a different theorem. A verification file exhibits a world satisfying every hypothesis of the goal.
Proofs of the milestones, alternative arguments for Lemma 2, and an extension to Theorem 2 (infinite consequence spaces, not part of this mission) are welcome.
Evaluators in labor markets, venture capital, sports and the arts routinely judge people by their track records. A common intuition holds that two successes are better evidence of talent than one. Another, equally common intuition celebrates the underdog: the agent who succeeds after an initial failure, against the odds. Denrell, Liu and Maslach (Management Science, 2023) ask when the second intuition is correct as a matter of Bayesian inference, that is, when a rational evaluator should regard success after failure as stronger evidence of high quality than two successes.
Their answer turns on how past outcomes change the difficulty of future tasks. Success brings resources (money, attention, social capital) and failure depletes them, so the second outcome is drawn under different conditions depending on the first. The paper identifies a condition on the interaction between quality and resources under which success after failure can be the more impressive record, and shows that this condition is necessary but not sufficient. This mission formalizes that claim together with the Bayes computations it rests on.
An agent has one of two qualities, high or low , each with prior probability . In each of two periods the agent succeeds () or fails (). The two-period model has six parameters:
The joint law on gives the outcome probability . The posterior is the conditional probability under of high quality given the ordered pair of outcomes. Order matters: conditions on failure first and success second.
In the resource model, success probability is a function of quality and resources , with low and high quality levels . Agents start with resources ; success raises them to and failure lowers them to . This induces , , and likewise for . Condition (6) says that more resources help low-quality agents proportionally more:
taken at , .
In the Lean development these objects are Quality, Params, Params.Standing, Params.mass, Params.jointLaw, Params.posteriorHigh, ofResource and Condition6.
for every success function with first-period values in , second-period values in and ;
with valued in and strictly increasing in both arguments.
The result separates two effects that a naive reading conflates. An initial failure makes a later success more diagnostic only when resources narrow the gap between low- and high-quality agents, i.e. when quality and resources are substitutes in the proportional sense of condition (6). Even then, the gain in diagnosticity must outweigh the evidence carried by the initial success itself, which is why the condition is not sufficient. In terms of expected quality, , so the same comparison governs expected-quality judgements. The paper builds on this analysis to explain when "one-hit wonders" and underdogs should be rated above consistent performers, and tests the predictions on hockey and music-market data.
The paper proves necessity in Appendix B by a short algebraic argument and asserts non-sufficiency with a numerical example (Figure 1). Neither part has a machine-checked proof. This mission formalizes both parts against a measure-theoretic definition of the posterior, so the Bayes computations of Appendix A are proved rather than assumed.
The mathematics is elementary; the difficulty is fidelity. The posterior is defined by conditioning, so the closed forms of Appendix A have to be derived from the joint law on a finite sample space, with care at the conditioning events. The ordered pair must not be confused with : the two posteriors differ in general. Non-sufficiency needs a single function on all of , valued in and strictly increasing in each argument, that passes through prescribed values at the grid ; choosing six numbers is not enough.
Qualities are a two-element type; outcomes are booleans with true for success, in time order. The joint law is a finite sum of Dirac measures weighted by , and the posterior is Mathlib's conditional measure μ[|s], converted to a real. The standing domain puts in and the four second-period probabilities in , which excludes exactly the values where a formula of the paper divides by zero. No ordering of the six parameters is assumed in the six-parameter model.
Defining the posterior by its Appendix A closed form would make the milestones definitional and the goal a statement about a formula; that encoding is ruled out. Reading condition (6) as holding for all would make necessity false; it is taken at , as Appendix B does. The necessity clause assumes only , which the paper's monotonicity assumptions imply.
The development needs Bayes' rule on a finite space (Mathlib's ProbabilityTheory.cond_apply) and real-arithmetic rearrangements. Contributions are welcome on each milestone, on the explicit witness for non-sufficiency, and on the mirror statements of the paper (eqs. (3) and (5)), which are not part of this mission.
Patent offices, grant agencies and journals screen proposals with limited reviewer time. A reviewer who cannot find concrete evidence about a proposal leaves the decision maker with a choice: reject it and possibly lose a good idea, or give it the benefit of the doubt and possibly fund a bad one. Figueroa and Lemus (SSRN 3840423, version of April 4, 2022) show that the second option has a further cost. An applicant who knows that an idea is bad gains from a report that finds nothing, and so has a reason to make the proposal harder to read. The paper calls this strategic obfuscation.
The policy question is direct. Concerns about insufficient examination time (Frakes and Wasserman, 2017) led the United States Patent and Trademark Office to give examiners more resources. If applicants respond strategically, more resources need not help. The model's communication technology follows Dewatripont and Tirole (2005), in which the sender can affect how likely a message is to get through. The published version of the paper appeared as The Benefit of the Doubt: Patent Examination Under Strategic Obfuscation in Management Science (doi:10.1287/mnsc.2023.00140). This mission uses the numbering of the SSRN version only.
An idea has value with prior , and its value is known to the applicant. The sponsor pays to fund any idea, with , and the applicant receives if funded. The applicant chooses obfuscation effort at cost . A reviewer with fixed resources finds hard evidence of with probability , where increases in , decreases in , and for . The function is submodular: more effort lowers the marginal value of resources (Assumption 1). Without evidence the proposal is uncertified. The sponsor then holds a posterior and funds with probability . Certified ideas are funded, rejected ones are not, and good applicants do not obfuscate.
A bad applicant's best response solves
An equilibrium at is with , given by Bayes' rule, and maximizing . The sponsor's payoff is
The threshold is the largest below which vanishes. With , the benefit minus the cost of funding at maximal effort, the threshold is the largest with .
For , every detection probability , every effort selection and every equilibrium family, is strictly increasing on if , and on and if . At each where and are differentiable,
Some instance and equilibrium family have in with .
The result. Proposition 2 says that the value of examination resources is not monotone. A sponsor comparing budgets has to know the prior quality of ideas and the current level of resources, because near the middle of the range a larger budget buys detection that induced obfuscation more than cancels. This is the first policy finding of the paper. Propositions 3 to 7, on investment in knowledge and on competition, are built on the same equilibrium analysis.
The formalization. The results are proved on paper and, as far as the platform's catalog shows, have not been machine-checked. The mission produces a complete treatment of all equilibria of a screening game with costly obfuscation, including non-unique equilibria and off-path beliefs. It also records the corrections needed for the printed statements. Proposition 2 fails at and at . Step a.2 of the proof of Proposition 1 draws a conclusion about that does not follow. The Claim needs , and , and its inequality (3) holds strictly below .
The paper's proof reads the sign of directly from two payoff formulas and treats as differentiable. That argument does not close in the generality stated. Effort is an arbitrary selection of an argmax and can jump, has a kink at , and the mixing regime starts at , where the two payoff formulas meet. The iff therefore has to be decided at the boundary points and , where the formula on one side tells nothing about the derivative. Equilibrium need not be unique at a given , so a statement about one chosen branch would not be Proposition 2. The monotonicity of , which the paper derives by differentiating, has to hold with no derivative of available.
The Lean development works with functions read on and ; no hypothesis looks outside those sets. Assumption 1 is stated in difference form (IsDetection), which contains the paper's class and its own example, whose is flat for . A fixed selection of (1) is used consistently in the equilibrium and in both thresholds. Bayes' rule (2) and equation (4) are cross-multiplied, so that an off-path report at , leaves free instead of inheriting . The thresholds are suprema, which agree with the paper's definitions for continuous and keep the goal free of continuity hypotheses. The partial of in is a derivative within . Continuity appears only in the location of and in the existence of a solution of (4).
A trivializing reading is ruled out: the goal is a conditional on an equilibrium at every , and its last clause supplies an instance with such a family and a real fall in payoff.
No new infrastructure is needed beyond one-variable real analysis in Mathlib. The two-point revealed-preference comparisons of milestone 1 are reusable for other games with an argmax selection. Proofs of milestones in any order are welcome. Propositions 3 to 8 are outside this mission.