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?
Prizes and patents reward the first innovator to fill a market niche. How generous the reward should be depends on how often useful ideas arrive, and a policy maker rarely knows that rate. Basov, Erkal, Minehart and Scotchmer (SSRN 4628270, 2024; published in Management Science, doi:10.1287/mnsc.2023.03362) model ideas as scarce: they arrive at the times of a Poisson process, each to a different person, and an idea that is not used is lost. A reward then works as a screen. Ideas whose cost is below the reward are developed, and the rest are discarded. The planner trades the cost of the innovation against the delay before it arrives.
The question is how this trade-off changes over time when the arrival rate of ideas is unknown. Each period in which the reward goes unclaimed is evidence that ideas are scarce. The paper shows that the optimal reward rises with the delay and that expected welfare falls. The model belongs to the family of optimal stopping and real-options problems with Bayesian learning (compare Mason and Välimäki, 2011, with two possible arrival rates). Here the planner's belief is a whole density on , and the paper shows that one scalar state variable still suffices.
A niche, once filled, has social value , where is the discount rate. Each idea has an R&D cost drawn from a continuous cost density on its support , with distribution function . Throughout, . At time the planner offers a reward . An idea that arrives at time is developed exactly when its cost is at most , which happens with probability .
Ideas arrive at an unknown rate . The planner's prior is a density on , and Assumption 1 requires to be continuous and bounded, to have finite moments of every order, and to satisfy . The cumulative innovation incentive is a sufficient statistic: given that no innovation has occurred, the posterior is with . Its moments are .
The expected welfare of a reward policy from state is
The value function is , taken over all admissible policies. It satisfies the Hamilton–Jacobi–Bellman equation
There is an optimal feedback reward . It is the unique solution of
it is and strictly increasing, is strictly decreasing, and
The statement holds for every cost density and every prior satisfying Assumption 1. It assumes no parametric family.
Theorem 3 gives the shape of the optimal reward. It starts low, rises monotonically, and tends to the full social value . The rate is governed only by and the cost distribution below . Theorem 4 says that a planner who learns sets a lower reward than one who treats today's expected rate as known. The difference is the option value of the information in an unclaimed reward. These results underlie the paper's legal interpretations, such as rewards that grow with delay and the comparative statics in the cost distribution (Theorem 6).
Formalization adds three things on top of the paper. First, the moment calculus of Lemma 2 is a reusable result about exponential tilting of densities on . Second, the identification of the value function with the HJB solution and the derivation of (22) and (24) are carried out with a fixed policy class and solution concept. Third, the statements fix the welfare functional precisely: as printed, (16) multiplies by , which already contains that factor. The mission uses the functional that is the limit of the Bellman recursion (17), which the paper's own derivation uses, and the HJB milestone states that limit. None of these results has been machine-checked. The paper's proofs are informal at the limit .
The obvious route is to write down the HJB equation and read off the policy, and it skips the hard part. The paper passes from discrete time to the HJB equation in one sentence. In continuous time one needs a verification argument: every bounded differentiable solution of the HJB equation bounds the welfare of every admissible policy, and it is attained along closed-loop paths. The value function must also be shown to be differentiable before (21) can be written. A second difficulty is monotonicity. Equation (24) alone does not rule out a reward that first falls. The argument combines Lemma 3, which needs the strict Cauchy–Schwarz inequality behind Lemma 2 (iii), with a limit argument at infinity. The rate constant (not , the naive rate) comes from l'Hôpital's rule applied to (24) together with . The latter is a Laplace-type asymptotic that depends on being continuous and positive at .
The Lean development lives in the namespace ScarceIdeas. States are , and every derivative is taken within . Policies are open-loop functions of time with values in , measurable on . The value is the real supremum of the welfare over all of them. An optimal reward is a feedback rule whose closed-loop paths exist from every state, and every such path attains . The moments are defined by the quotient (31). The naive reward is the root of (56). is stated as a limit of . "Increases" and "decreases" are strict.
The value function is a supremum, not a solution of the HJB equation or of (22). Defining it by either would make the goal circular. Optimality is measured against all admissible policies, not a restricted class. Changing a feedback rule at a single state changes no closed-loop welfare. For that reason the goal pins the optimal reward pointwise through (22), and "unique solution to (22)" means uniqueness of the root at each state.
A complete development needs: differentiation under the integral sign for Laplace-type integrals, and their asymptotics at infinity; the strict Cauchy–Schwarz inequality for integrals; a verification theorem for a one-dimensional infinite-horizon discounted control problem with a bounded state-dependent hazard; and comparison arguments for scalar ODEs. The moment lemma and the verification theorem are reusable beyond this mission. Contributions toward either, and toward any milestone, are welcome.
Search engines sell the ad slots next to their results in position auctions: advertisers bid, the highest bidder gets the top slot, the second highest the next one, and so on. A slot higher on the page is clicked more often, and the ratio of click rates between slots is described by a vector of relative position values. The textbook truthful mechanism, Vickrey–Clarke–Groves (VCG), computes its prices from this vector. The auctioneer does not know the true vector; it can only estimate it, and the bidding language of a real auction (one number per bidder) cannot express the bidder's own view of it.
Dütting, Fischer and Parkes (arXiv:1602.07593v4) ask which mechanisms still reach an efficient outcome, with slots assigned in order of value, when the mechanism uses a misspecified estimate. Their answer for complete information is that the non-truthful generalized second price (GSP) auction used in practice is at least as robust as the VCG mechanism run on the same estimate.
Timeline. Varian (2007) and Edelman, Ostrovsky and Schwarz (2007) characterized the envy-free ("symmetric", "locally envy-free") equilibria of GSP when the auctioneer uses the true position values, and showed that one of them reproduces the VCG outcome. Dütting, Fischer and Parkes treat the case of an estimate α different from the true vector β: Theorem 1 (complete information) and Theorem 2 (Bayes–Nash equilibrium of the first price variant). The preprint was posted in 2016 and appeared in Mathematics of Operations Research in 2024.
There are k positions and n ≥ k bidders. Let be the set of vectors with positive, non-increasing entries, extended by for . The true relative values are , and bidder values position at with . The auctioneer uses an estimate .
A bid profile is . An allocation is a ranking of the bidders in non-increasing order of bids, with ties resolved by . Write for the -th highest bid, and for . The bidder in position pays
and its utility in position at price is . For these are the VCG and GSP auctions.
An equilibrium is a profile in which no bidder gains by raising or lowering its bid and being assigned a different position (§3.1, p.8). Moving bidder to position leaves the other bidders in their order, and the mechanism charges its price for position on the new order. The equilibrium is efficient if also orders the values. A profile is envy-free (22) if no bidder prefers another bidder's position at that bidder's current price.
For every , every and every :
The values are not sorted, ties are allowed in , and , and the rankings are existential on both sides.
The milestones are stated in the paper's sorted frame (, bidder in position ):
The theorem compares the two mechanisms over all misspecifications at once. For every pair where the α-VCG mechanism can support an efficient outcome, so can the α-GSP mechanism. §3.1 of the paper shows that the converse fails. Running the "truthful" mechanism therefore buys no robustness, which is one argument for the non-truthful auctions used in practice. The proof also goes through an envy-free α-VCG profile and a map to α-GSP bids that keeps the payments, which describes the α-GSP equilibrium explicitly.
The result is proved on paper. As far as the platform's catalog shows, no part of it, and no position auction model, has a machine-checked proof. The mission produces the model (rankings, both payment rules, deviations, envy-freeness), which other work on sponsored search auctions can reuse, and a checked version of an argument whose statement needed correcting (next section).
The obvious approach compares the equilibrium conditions of the two mechanisms inequality by inequality, as the paper does for three positions in §3.1. In general the α-GSP conditions are not implied term by term: a bidder moving up in the α-GSP auction pays the bid of the occupant it displaces, not a sum of externalities. The paper instead passes through envy-freeness, which depends only on allocation and payments. The work is index-heavy: telescoping sums over positions, a recursively defined profile (26), and boundary positions beyond and beyond , where , and the order statistics are . The goal is stated for arbitrary rankings and unsorted values, so a relabelling to the sorted frame is also needed.
The equilibrium notion. On p.6 the paper defines a Nash equilibrium with deviations to every real bid under a fixed tie-breaking rule, and efficiency as " whenever ". With that definition Theorem 1 is false. Take , , , , . The α-VCG profile has no ties and is an efficient Nash equilibrium. An efficient α-GSP equilibrium would need . Bidder 3 must not take position 2, which gives , so . Bidder 1 must not drop to position 2, which gives . With this forces , a contradiction. The paper's proof uses the position-deviation conditions (23)–(24) of p.11. Under that notion, with ties resolved by the ranking (Lemma 2 produces the tie ), the argument is sound. Here the α-GSP profile is an efficient equilibrium.
Bidders are Fin n, and positions are 0-based ranks Fin n (rank is position ). Ranks are unassigned positions, worth and priced at . Rankings are Equiv.Perm (Fin n). and are functions on that are positive and non-increasing below and from on. Bids in rank order are padded with . Bids and values are non-negative. The equilibrium is the position-deviation equilibrium in both the hypothesis and the conclusion of Theorem 1; it is the mission's one declared correction. In Lemmas 1 and 2, positive vectors in are relaxed to non-negative sorted ones.
Efficiency is part of both sides of the goal. Dropping it, or replacing the deviation price with the current price of the target position (which is envy-freeness), would change the theorem. The sanity file checks that the example above behaves as described. In the model, is an efficient α-VCG equilibrium, is an efficient α-GSP one, and is not an equilibrium.
Everything is finite: sums over ranks, one permutation, real inequalities. No library beyond Mathlib is needed. Proofs of any milestone are welcome, as are a general relabelling lemma that reduces arbitrary rankings to the sorted frame and a proof of the strengthening that keeps the ranking fixed.
In Multiway Cut one is given an edge-weighted graph and terminals, and must delete a minimum-weight set of edges so that no two terminals remain connected. Equivalently, one labels every vertex by a terminal, each terminal by itself, and pays for the edges whose endpoints get different labels. The problem is APX-hard for every fixed (Dahlhaus et al., 1994), and it is a standard test case for rounding geometric relaxations.
Timeline of the approximation ratio obtained by rounding the simplex relaxation:
An instance consists of a finite vertex set , a finite edge set of pairs , weights , and distinct terminals . A feasible labeling is with ; its cost is the total weight of the edges with .
The simplex relaxation embeds every vertex as a point of the simplex , with , and minimizes . A rounding maps the points to labels at random:
The transformation of the paper sorts the coordinates of as , forms the vectors , sets
for an explicit symmetric matrix (display (5.3) of the paper, nonzero only in its first three rows and columns and in ), and puts the values back in the original coordinate order. The cut density of a rounding at an edge that moves mass between the -th and -th largest coordinates (an -edge) is the limiting separation probability per unit .
With and the matrix (5.3), for every , every instance and every feasible embedding : both branches label the terminals correctly almost surely, and
hence for every feasible when is an optimal embedding.
The theorem shows that the barrier of Sharma and Vondrák concerns only coordinate-wise transformations: a transformation that couples the coordinates through their sorted order reaches with the two original ingredients and a proof checkable by hand. The approach (choose a feasible transformation, then bound the density by a sum of absolute values of linear forms) is a template for other partitioning relaxations.
The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. Formalizing it checks a long case analysis (the proof of Lemma 5.4 spans pp.8–11) and the reduction from cut density to the approximation ratio, which the paper calls "easy to show" and which, read with the lim sup of Definition 2.1, needs a correction (see below).
The obvious route, "bound the cut density and conclude by the Karger et al. argument", fails as stated: a bound on a pointwise does not control the separation probability of a long edge, because a labeling can jump between nearby points in a way invisible to every one-sided limit. The mission therefore states the per-edge bound with a remainder uniform over all edges, and the reduction with that hypothesis. Proving the uniform remainder for Algorithm 3 requires following along an edge exactly, not only its derivative.
The second obstacle is Lemma 5.4: removing the absolute values in (5.2) needs the chain of prefix-sum dominations of Observation 5.1 and Lemma 5.3, then a case analysis over and with exact rational arithmetic. The exponential-clocks bound (Lemma 2.1) needs the competing-exponentials computation and a coupling of two argmins.
Coordinates and terminals are Fin k, indexed from ; is stdSimplex ℝ (Fin k). The clocks' law is Measure.pi of expMeasure 1; the argmin runs over the support of by cross-multiplication (Lean's would otherwise let a zero coordinate win). CKR's law is the average over permutations of Lebesgue measure on . Probabilities are measures of events (outer measures), never integrals of indicators, so non-measurability cannot make a bound vacuous; expected costs are . "" is the eventual form "for every , eventually ratio ". The transformation uses Mathlib's Tuple.sort; its value does not depend on how ties are sorted. The matrix (5.3) is defined for every by its entry formula.
A trivializing formalization is excluded: the goal keeps the terminal clause (otherwise labeling everything costs nothing), and constants , and the matrix entries are fixed.
A complete development needs: the competing-exponentials law , the CKR union bound, the subdivision of a segment of into order-preserving steps, and exact rational arithmetic for the case analysis. The first three are reusable for any analysis of simplex-relaxation roundings. Proofs of individual milestones, and of the reduction (p.4) independently of this algorithm, are welcome.
Many allocation procedures used in practice — school choice, university admissions, course allocation — are run as one-shot direct mechanisms: every participant submits a full ranking, and an algorithm such as deferred acceptance or top trading cycles computes the assignment. Sequential alternatives, in which participants repeatedly pick one option from a menu, may see their pick rejected, and are then offered a smaller menu, have been proposed and studied for college admissions; the iterative deferred acceptance mechanism is the leading example (Bó and Hakimov, Games and Economic Behavior 135, 2022), and laboratory evidence finds more truthful behaviour under it than under its direct counterpart (Bó and Hakimov, The Economic Journal 130, 2020). Two questions arise: which allocation rules can be run this way at all, and when is it in every participant's interest to pick truthfully?
Bó and Hakimov, Pick-an-Object Mechanisms (arXiv:2012.01025v4) answer both questions for a general class of sequential procedures, and the answer is a pair of characterizations. This mission formalizes them.
is a finite set of agents and a finite set of object types containing the null object . Each agent has a strict preference over all of ; objects ranked below are unacceptable, and means or . A rule maps every preference profile to an allocation . There is no capacity constraint: feasibility is whatever the rule produces. A rule is individually rational if and strategy-proof if no agent gains by reporting another preference.
A choice history is a sequence of menus and choices ; a collective history has one per agent, and is the one in which no agent has chosen yet. A menu function assigns every agent a menu at every collective history, subject to two rules:
The pick-an-object (PAO) mechanism of runs in periods. If every menu is empty, it stops and each agent receives her last choice. Otherwise every agent with a non-empty menu picks one element, and the history grows. A straightforward agent always picks her most-preferred element of the menu. sequentializes if, for every profile , straightforward play from ends at .
The lower contour set is the set of profiles such that, for each agent , has the same objects strictly above as , in the same order. A rule satisfies monotonic discoverability if for every allocation and profile , either , or some agent has for every .
A strategy chooses an element of the current menu as a function of the agent's own choice history. Straightforward strategies form a perfect ex-post equilibrium of if, at every collective history that can produce (under arbitrary past choices) and for every profile , no agent gains by deviating to any other strategy from on. A rule is pick-an-object implementable in perfect ex-post equilibrium if some sequentializes it with straightforward strategies forming such an equilibrium.
For every individually rational rule :
and, if is PAO-implementable in perfect ex-post equilibrium, straightforward strategies form a perfect ex-post equilibrium of every menu function that sequentializes .
Theorem 1 says exactly which rules a PAO mechanism can run, and shows that the restriction is real: not every rule can be sequentialized, because a rejected choice can never be offered again. Proposition 1 of the paper (not part of this mission) places deferred acceptance, top trading cycles and the Boston mechanism inside the class. Theorem 2 adds incentives: among sequentializable rules, the strategy-proof ones are exactly those for which truthful picking is a best response after every history, against every deviation, for every preference profile — and this holds in every PAO mechanism for the rule, not in a specially designed one. For a designer this means the choice of menus can be made for simplicity or transparency without affecting incentives.
On the formal side, the mission produces a reusable model of sequential menu mechanisms for ordinal object allocation (histories, menu functions, an executable run, strategies, perfect ex-post equilibrium), which the platform does not have; existing items cover strategy-proofness of fixed algorithms (top trading cycles, deferred acceptance) and obviously strategy-proof mechanisms for scheduling. The paper's results are proved on paper only; none is machine-checked. The printed proof of Theorem 1's "if" direction relies on a canonical mechanism (§3.3) that does not sequentialize every monotonically discoverable rule (a two-agent serial dictatorship already fails), so a complete formal proof must supply a different witness.
The equilibrium part is the hard one. Perfect ex-post equilibrium is required at every history, including histories in which agents have already made arbitrary non-truthful choices. Strategy-proofness of speaks only about complete reports from , so it does not directly compare two continuations after such a history. The bridge is Lemma 1: every history of the mechanism must be rationalized by preferences (the tuples ), the continuations under truthful and deviating play must be re-expressed as straightforward play from the beginning under modified profiles, and the comparison must be made through recursive dominance. Keeping the same in both representations is essential and is where a careless argument breaks.
For Theorem 1, the natural first idea — elicit the whole preference profile with menus and then assign — is not available: menus must shrink and the agent keeps her last pick, so information about lower-ranked objects can only be obtained by permanently rejecting her current choice. The "only if" direction must turn this informational constraint into monotonic discoverability. The "if" direction needs a menu function that rejects only choices that are no longer attainable.
Object types are Option Obj for a finite type Obj, with none the null object. A strict preference is a ranking Option Obj ≃ Fin (card (Option Obj)) (rank is best), so every strict linear order is represented exactly once. Allocations are arbitrary maps . Histories are lists of (menu, choice) pairs, oldest first. The run is the -fold iterate of one period of the mechanism; with menus that strictly shrink, this is enough for the procedure to stop from any history, and a stopped history is a fixed point. Strategies are functions of the agent's own history and current menu that pick from every non-empty menu. The collective histories of are an inductive predicate: and everything reachable from it under arbitrary choices from the offered menus. The menu-shrinking constraint is not imposed at histories other than in which some agent has never faced a menu, which the mechanism never produces.
The lower contour set is corrected. The display on p.12 constrains only pairs of objects strictly above ; with it, the one-agent rule " iff " on is individually rational and sequentialized by the single menu , but fails Definition 3 at , , , so Theorem 1 would be false. The formalization uses the reading stated in the sentence under the display (same objects above , in the same order). Likewise, the canonical mechanism of §3.3 is not used as the witness for Theorem 1 and is not part of the formalization.
Restricting perfect ex-post equilibrium to histories generated by straightforward play, or allowing a deviation to "choose" an object outside the menu, would change the equilibrium notion; neither is done.
Needed infrastructure: finite permutations and rankings, list and finset manipulation, induction over reachable histories, and a determinism and termination analysis of the run. The model definitions and the representation of outcomes after arbitrary histories (Lemma 1) are reusable for other sequential mechanisms. Proofs of any milestone, a formal proof that the run's period bound suffices, and alternative witnesses for Theorem 1 are welcome.
When independent firms pool resources, they can share not only a deterministic profit but a random one, chosen through a joint decision. Cooperative models for operations management usually value such payoffs in expectation or by a concave utility, and then bargain over the expected values. Gutjahr, Kovacevic and Wozabal (author manuscript) replace this with coherent acceptability functionals in the sense of Artzner et al. (1999), the class that contains expectation and the Average Value-at-Risk, and ask which sharing rule follows from axioms alone. The classical axioms of Nash (1950) are stated for deterministic utility pairs. The relevant comparison for this mission is the splitting axiom of Hougaard (2009), which the paper carries from deterministic allocation to random payoffs.
Fix a probability space, an exponent , and a compact topological space of decisions. An instance for a finite nonempty player set consists of endowments , a profit for each decision , with continuous into with the weak topology, and coherent acceptability functionals , that is, monotone, positively homogeneous, super-additive and translation invariant. Write . The set of feasible acceptability allocations is
and is the maximum of over the same constraints, which is problem (8). A bargaining solution selects a point of for each instance. It is asked to satisfy PAR (Pareto optimality), SYM (equal treatment when all values agree and is permutation invariant) and STR (a player who splits into copies, each with endowment , receives the same total).
On the class of admissible instances, those with all for which the maximum in (8) exists, put
The goal has four clauses: (a) rule (9) is a bargaining solution; (b) a bargaining solution agreeing with (9) satisfies PAR, SYM, STR and CONT; (c) a bargaining solution with PAR, SYM, STR agrees with (9) wherever the are natural multiples of one positive real; (d) a bargaining solution with PAR, SYM, STR, CONT agrees with (9) everywhere. CONT requires to be continuous along scalings with .
The milestones are: Proposition 2 (the polytope (7)), Proposition 1 (compactness, as an equivalence with attainment), Lemma 5 ( does not depend on the endowments), invariance of and of the class under splitting, the identity under PAR, the commensurable case (clause (c)), the converse (clauses (a), (b)), and two counterexamples.
The result gives a sharing rule for risk-averse partners with a closed form: the shares depend only on the values , and the decision enters only through . So a joint decision can be separated from the division of the surplus, which is what makes the rule usable in stochastic optimization models.
The theorem has been published, but the formalization adds more than a check, because the printed statement is false in two ways, and the mission records both as machine-readable counterexamples. Nothing in this mission has a previous machine-checked proof on the platform. The two-player Nash theorem there uses different axioms and yields a different solution.
The obvious route from rational to real values fails. The printed proof treats by splitting and symmetry and then appeals to the continuity of the right-hand side of (9). That continuity says nothing about , and SYM only compares equal values while STR only divides a value by an integer, so two players with are never connected. The second obstacle is structural: Axiom STR splits one player at a time, the player type changes at every step, and no relabelling invariance of is assumed.
Corrections. Two corrections to the printed Theorem 1 are part of the statement. First, CONT is added to the characterization, and clause (c) keeps what the printed axioms give; the witness is a rule that differs from (9) at , and meets PAR, SYM, STR at every admissible instance. Second, the class requires the maximum in (8) to exist: on with the uniform probability there is a feasible instance, with , where it does not exist, is not compact, and no rule can satisfy PAR. Proposition 1 and Proposition 2 are restated accordingly. Lemma 4 of the paper is false and is not used.
Representation. is Lp ℝ p μ with p : ℝ≥0∞, 1 ≤ p (so is admitted), and is a map X → Lp ℝ p μ. Functionals are real-valued. No continuity of , no bound and no dual representation is assumed. Player sets are finite nonempty types and a rule is a family over all of them, because Axiom 3 changes the player set. A split player set is {j // j ≠ i} ⊕ Fin ℓ with ℓ : ℕ+. The real is a sSup and equals the maximum exactly on attained instances; every item mentioning assumes attainment.
Non-triviality. Clause (a) shows that the hypotheses of (c) and (d) can be met, so neither is vacuous, and the class is not empty: it contains every instance with constant endowments and expectations whose total does not exceed a constant profit. Defining through , or adding an axiom that depends only on , would assume part of the conclusion; neither happens here.
Infrastructure. The development needs coherent functionals on Lp, the polytope description of , and the split and scaling operations on instances. Coherent acceptability on is reusable for other risk-averse models. Contributions that connect these definitions to Average Value-at-Risk are welcome.
Many developing countries reserve college seats for disadvantaged students, and how large the reservation should be is a live policy question: in 1993 the Supreme Court of India capped reservations at 50% of seats. Bao, Ni and Singh (SSRN 3772113, version of May 30, 2023; published in Management Science, doi:10.1287/mnsc.2021.00249) build an equilibrium model in which higher-income students can buy private tutoring, the job market pays each group the mean ability of its admitted students, and a policymaker moves seats from one group to the other. Their closing finding answers a policy question: the transfer that eliminates the admission gap is larger than the transfer that maximizes overall student welfare, so a welfare-maximizing policymaker leaves inequality in place. The paper asserts this comparison in one line of its appendix.
A unit mass of students competes for capacity . A share is type and can pay for proprietary resources; the remaining are type and cannot. A student who exerts effort pays , and her ability is if she invests and otherwise, with and .
The college admits every student whose ability exceeds a cutoff . Write for the admission probability of a student of mean ability . An admitted student receives a reward equal to the expected ability of the admitted students of her type. Each student takes and as given and maximizes , net of if she invested. Seats clear: .
A seat transfer gives each type its own cutoff and fixes admissions: type loses exactly seats relative to the no-policy benchmark and type gains exactly . Educational inequality is , and overall welfare is .
The parameters satisfy , , and . The threshold of equation (32) is the largest cost at which type does not deviate from investing.
For , the investing benchmark equilibrium exists and is unique; every feasible transfer has a unique equilibrium ; and
is feasible, with and for every other feasible . Moreover overall welfare has a unique maximizer over feasible transfers, and
The admission probability (4) and reward (10) under uniform noise; effort at a given cutoff (11); the equilibrium cutoff (26)–(27); the investment thresholds (32) and (45); Proposition 1; the equilibrium probabilities (28) and the closed form of inequality (47); the policy cutoffs (51)–(52); Lemma 1 on effort; welfare as a concave quadratic in (55); its vertex (56); and Proposition 5, the inverted-U shape of welfare.
The result gives a closed form for the transfer that closes the admission gap and states that closing it costs welfare. The paper draws its policy advice from this: other instruments, such as better basic education and lower wage discrimination, should accompany reservation. Without the strict inequality, the conflict between the two policy goals would not be established.
The results are proved on paper, with first-order conditions and a one-line comparison. They have no machine-checked proof, and this mission adds three things. It derives (4) and (10) from the uniform measure instead of assuming them. It establishes existence and uniqueness of the equilibria the paper takes for granted. It gives a proof of on the whole parameter domain, a comparison in four real parameters that the paper does not derive. It also corrects errors in the printed statements: the effort range, the claimed equivalence of the cutoff restriction with the capacity interval, the denominator of in (57), and a misplaced bracket in . Exact-rational sampling supports the comparison, with never above about ; that is evidence, not a proof.
The closed forms follow from linear algebra once the model is reduced to first-order conditions. The work lies in the reduction: passing from the true clipped probability and a conditional expectation to the linear system, showing that a boundary effort is not a maximizer, and ruling out every other outcome. The naive route of comparing (24) with (56) symbolically fails to be routine, because (56) is the first-order solution only when positive, so , and both cases must be handled; the remaining inequality is a polynomial inequality in on a non-box domain.
Parameters are a structure of five reals with the predicate Params.Valid. The noise is the uniform law on : Lebesgue measure on scaled by . admitProb and admittedMean are the true probability and conditional mean from that measure; (4) and (10) are theorems. Equilibria are pure and symmetric within a type.
Three conventions depart from the printed text and are declared on every theorem. Effort ranges over , because equilibrium effort can exceed the page's bound of . The domain is the capacity interval above with no restriction on . Best responses range over the efforts at which the admission probability lies strictly in , the set on which (4) holds. Under this convention equilibria are exactly the solutions of the paper's first-order conditions. Against all efforts with the clipped probability they can fail: effort can pay more than the interior effort when admission chances are small, at itself for small .
The policy game is the investing branch, equation (17), and the feasible transfers are the set of p.41. The transfer in the goal is characterized as the maximizer of , never defined by (56); is characterized by what it achieves; so the goal is not algebra about named formulas. The definitions are local to this model and reusable only through the uniform law. Proofs of the milestones, in any order, are welcome.
The risk-sensitive exponential cost of a Markov chain replaces the long-run average of the one-step cost by the exponential growth rate of the expected exponential of the accumulated cost. It penalizes rare sample paths with high cost, and it goes back to Howard and Matheson (1972). For a finite chain the growth rate is the logarithm of a Perron eigenvalue (Balaji and Meyn, 2000).
Policy gradient methods for the average cost are classical: Marbach and Tsitsiklis (2001) estimate the gradient from cycles between visits to a recurrent state, and Borkar (2001) gives a sensitivity formula for the risk-sensitive cost. Moharrami, Murthy, Roy and Srikant (arXiv:2202.04157v2) give a trajectory-based algorithm for the risk-sensitive cost, updated once per cycle, and prove that it reaches a stationary point of the cost with probability 1. This mission formalizes that convergence theorem.
Let be a finite state space and a parameter. For each there is a transition matrix and a one-step cost . For a risk factor , the risk-sensitive cost is
which does not depend on under the assumptions below.
Assumption 1 asks that every matrix in the closure of be irreducible and aperiodic. Assumption 2 asks that and be bounded and twice differentiable in with bounded first and second derivatives. Assumption 3 gives bounded functions , with and .
Fix a state , and let . On a cycle from to , put . Then is the unique solution of . For , the smooth truncation is
and is the unique solution of .
The algorithm runs the chain under from the -th to the -th visit to , and then updates
where and are the cycle statistics at truncation level . A second rule projects both increments coordinatewise to fixed intervals. Assumption 5 is , and .
The goal is Theorem 1 of the paper, for both update rules.
If for all , then with probability 1
If for some and , where and (Assumption 4), then with probability 1
The milestones follow the paper's proof: uniform exponential moments of over the closure and for the twisted kernels (Lemma 1, Corollary 4), the eigenvalue and fixed-point descriptions of the cost (Proposition 2, Corollary 1), the truncation and sensitivity results of Appendix E (Corollaries 14–16, Lemmas 14–17), and the three steps of Appendix B (Lemmas 3, 4 and 11, Corollary 12).
The theorem gives a sample-path algorithm with an almost sure guarantee for an objective whose natural gradient estimator can have infinite variance. Its supporting results stand on their own: uniform return-time moments over a compact family of chains, the cycle description of the Perron eigenvalue, and differentiability of the eigenvalue with bounds uniform in the parameter.
The result is proved in the paper and, as far as the platform's catalog shows, has no machine-checked proof. This mission produces that proof. It also corrects two printed statements, recorded in their items: the twisted forms in Lemma 14 omit a factor , and the interval in Corollary 12 has a sign misprint. The proof of the growing-truncation clause has a known difficulty for non-monotone : when oscillates, can cross the same gap many times, and the telescoping use of Assumption 4 no longer applies. The statement is kept as printed, and a solver may have to close or report this gap.
The obvious route is stochastic approximation on with as the sampled statistic. It fails because for small , and because the statistic can have infinite variance for large . Truncating the sampled gradient destroys proportionality to , and a hard truncation of the cost destroys smoothness; this is why has five terms.
After smooth truncation, the estimate and the moving target remain coupled. The monotonicity argument for their difference that works for the ODE fails under noise, and the proof replaces it with alternating cycles and two families of Lyapunov functions.
The parameter lives in EuclideanSpace ℝ (Fin l), and is an arbitrary Fintype. Assumption 1 is Matrix.IsPrimitive on the closure of the range of P, and the recurrent state is a parameter, since every state of such a chain is recurrent. "Bounded" means uniformly in , and "twice differentiable" does not include continuity of the second derivative. A cycle is a finite list of states, its statistics are pathwise functions, and and take values in ℝ≥0∞, because can be .
The run is an adaptive process: IsRun states the one-step law given the whole prefix, with the policy obtained by folding the update over the prefix. is the value of the fold at the -th return. Step sizes are positive, , and is any value above 1 where the set in the supremum is empty.
Two junk values are ruled out. The goal asserts differentiability of the cost, so that gradient is not the value of a non-differentiable function, and it asserts infinitely many returns almost surely, so that is defined along the path. Corollary 14 proves that the total function truncCost is the unique root of .
A complete development needs the Perron–Frobenius theorem for primitive matrices (eigenvalue, positive eigenvector, growth of powers), first-passage decompositions over excursions, differentiation under an infinite sum, the implicit function theorem, and the martingale convergence theorem. The return-time and Perron parts are reusable beyond this mission. Proofs of any milestone, and of supporting lemmas of Appendices B and E as separate statements, are welcome. Appendix D, the MDP version, is outside the mission.
The extinction probability of a branching process is the smallest fixed point of its offspring generating function, a classical result in the theory of branching processes (Athreya and Ney, 1972). Flesch, Predtetchinski and Suomala (arXiv:2104.10528) ask what becomes of this fact when the tree is contested. Two players choose the path through a random tree, and each node is controlled by one of them. The authors study the resulting zero-sum games, whose payoffs are upper semicontinuous, and determine the distribution of their value.
The model sits between three literatures: random games, where a game is drawn from a distribution and its typical solution is studied (Goldman, 1957, on the saddle point of a random matrix); games on Galton-Watson trees (Holroyd and Martin, arXiv:1904.04150); and perfect information games with semicontinuous payoffs. The tree carries marks in the sense of Neveu's marked trees (Neveu, 1986).
A primitive distribution is a probability measure on . Its coordinates are the active player , the capacity and the number of children . Write and .
A game is an ordered tree of finite sequences of positive integers, with an active player and a capacity at each node. The set of games carries the topology generated by the sets and with rational. The measure on its Borel sets is the distribution of the game obtained by drawing a triple from independently at each node of and keeping the tree that grows from the root.
Play starts at the root. At a node that is not an end node, the active player moves to a child. Player I's payoff is the infimum of the capacities visited. Player I maximizes and Player II minimizes. The value is . The truncated game keeps the nodes of length at most , and . The value generating function is
and . In Lean these are RandomPIGame.Game, gameMeasure p, Game.value, Game.trunc and f p k.
For every primitive distribution and every ,
The result. Theorem 4.6 determines the distribution function of the value from alone, with no assumption on . If Player I controls every node and the capacity is on non-end nodes and on end nodes, it recovers the extinction probability of a Galton-Watson tree. The paper's Theorem 4.7, a criterion for , follows from it together with Lemma 4.2, and its corollaries on phase transitions rest on that criterion.
The formalization. The theorem is proved in the paper; no machine-checked proof of it is on the platform. The mission adds to the platform a space of marked ordered trees with its topology and Borel measure, the value of infinite perfect information games with these payoffs, and a fixed-point theorem for a process more general than a generation-count branching process. The published GaltonWatson.extinction_criterion is a related open target about a different object, and TheoryOfGames.PerfectInfo.strictly_determined_value covers finite game trees only.
The obvious first-step argument conditions on the root and uses that the subgames are independent copies of the whole game. Its first obstacle is that the value of an infinite game is not known to be measurable: the paper notes that the value of a Borel-parameterized infinite perfect information game need not be Borel measurable. A recursion for alone is also insufficient, because a fixed-point equation does not say which fixed point is the right one. The second obstacle is independence. The subgames are functions of disjoint sets of coordinates of only after the root's number of children is fixed, and on a random tree the bookkeeping of which coordinates each subgame reads is the core of the construction. The third is the existence of the value itself: the paper cites Martin's determinacy theorem, and Mathlib has no determinacy theorem.
ℝ≥0, and nodes are List ℕ+ with written h ++ [j].ι and γ are functions on the subtype ↥T. A game is its triple, with no junk data off the tree.gameMeasure p is (Measure.infinitePi fun _ => p).map g on the Borel σ-algebra of the topology above. Measure.map is on a non-measurable map, and measurability of g is the first clause of the first milestone.value is the real sup inf, over nonempty strategy types, with all payoffs in . A play stays at an end node once reached.d p k takes values in ℝ≥0∞, since no moment of is assumed.Game.child ω ℓ is as a total map, and its default off is never used.The conclusion of the goal is IsLeast: the weaker claim that is a fixed point would not determine it, and is often a fixed point. The event is the strict , and is arbitrary.
A complete development needs the measurable structure of , the independence of subgames under , and the value theory of the games. The marked-tree space and the measure are reusable for other tree-indexed models. Definitions, lemmas on the topology and σ-algebra of , a determinacy argument for these payoffs, and alternative proofs of any milestone are welcome.
Event timing models describe when defaults, insurance claims or component failures occur. Each event arrives at the first time its integrated hazard crosses an independent exponential threshold, and the hazard rates may depend on the history of all events (contagion). Expectations of path functionals of the event indicators have no tractable closed form beyond small , so they are computed by Monte Carlo. The standard time-scaling scheme discretizes the hazards and is biased.
Giesecke and Shkolnik (doi:10.1287/moor.2021.1156, Mathematics of Operations Research, 2022; the mission cites the authors' manuscript of January 16, 2018) remove that bias by a change of measure. Under a new measure every intensity is multiplied by a chosen process , and the estimator is reweighted by the likelihood ratio . Their Theorem 3.1 says when this measure exists. It is the theoretical foundation of their exact and nearly exact algorithms (Sections 4–5).
On a probability space there are events.
admits the -intensity when is a -martingale.
Theorem 3.1 states: if for every either or -almost surely, then is an absolutely continuous probability measure and admits the -intensity . Section 2.1 assumes that the are mutually independent and that is independent of , and asserts that is an -martingale.
Counterexample B. Take , , so . Let be the natural filtration of and that of . Take for and afterwards, and symmetrically. Every printed assumption holds, and . On one has , hence
The proof's induction step (pp.28–29) uses the independence of and under the tilted measure , but the density of involves the earlier clocks, which may depend on . A second example (counterexample A, with revealing at time ) shows that the compensator property asserted on p.5 does not follow from the setting.
The mission therefore formalizes the minimal correction: (1) sequential independence, under which each is independent of ; it implies both printed independence assumptions and equals them for ; (2) the compensator hypothesis, which assumes that is an -martingale under . The multiplier, the density, the condition and both conclusions are unchanged. The corrected theorem does not cover the paper's JAM multiplier (14), which depends on every , or the two-way contagion models (32)–(34): these violate sequential independence.
Under the setting, sequential independence and the compensator hypothesis, if for every
then is a probability measure, , and for every , is an integrable -martingale under .
They follow the paper's induction over the events, Appendix A. tilts the first events. is the density process of event , and (40) are its localization times. The milestones are: the integration-by-parts formula (41); the bound ; Fatou's bound ; the conditional survival law , the corrected step; the tail bound (42); uniform integrability with ; the Doob martingale of footnote 17; and the Girsanov–Meyer local-martingale step.
The theorem lets a simulator choose the intensities it samples under, which can be piecewise constant and thus exactly simulable, while keeping an unbiased estimator. It does so for stochastic, unbounded multipliers, where classical criteria (Novikov- or Kazamaki-type integrability of the density) do not apply. Blanchet and Ruf (2016, Theorem 4) cover bounded deterministic only.
The mission records a correction: the printed statement is false. Theorem 3.1 has no machine-checked proof, and neither have its milestones. Mathlib has filtrations, stopping times, predictable processes, local properties, martingales and conditional expectations, but no stochastic integral, no Doob–Meyer decomposition and no Girsanov theorem. No statement here needs them; their proofs may.
is a nonnegative local martingale, so is immediate. Equality is the content. Localizing by gives unit-mean martingales , but mass can escape on . Bounding it needs the conditional law of given the clock under the already-tilted measure , and that law is the point where the printed argument breaks. The density may be unbounded, so uniform integrability has to be proved directly through (42).
Time is ℝ≥0; event times and take values in WithTop ℝ≥0 with . Clocks are lower Lebesgue integrals in , evaluated at any time in . is written in product form, never with , and equals on the -null event that some . is P.withDensity. Expectations of nonnegative quantities are lower integrals. Martingales are Mathlib's Martingale with integrability stated separately. Local martingales and local boundedness use Mathlib's Locally, with localization in . is any right-continuous filtration with the listed properties; the paper's progressive enlargement is one. Completeness, total inaccessibility and distinctness of the are not assumed; the last follows from sequential independence. Under the density is identically . A non-trivial instance satisfying every hypothesis (, ) is checked in Lean, so the hypotheses are not vacuous.
Two definition modules carry the model and the measure change. Proofs of the milestones, and a direct proof of the goal by conditioning on the clocks, are welcome. Reusable infrastructure beyond this mission includes the pathwise calculus of single-jump processes, the compensator of a Cox-type event time, and change of measure for counting processes.
Retailers such as Amazon (Flex) and Walmart (Spark) use independent crowd drivers to meet on-demand delivery windows. Those drivers decide for themselves whether to work, and they are paid only while busy. A firm therefore faces two linked decisions: how much on-demand work to give the crowd, and what hourly wage to pay. A low utilization leaves drivers with too little income to participate, and a high utilization makes deliveries late. Taylor (2018) identifies driver independence and customer delay sensitivity as the defining features of such platforms.
Fatehi and Wagner (SSRN 3434625; version of record in Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2021.0973) replace probabilistic assumptions on demand, service times, tour lengths and opportunity costs with CLT-motivated uncertainty sets, in the style of robust queueing theory (Bandi, Bertsimas and Youssef, Operations Research, 2015). Their model has an explicit solution. This mission formalizes that solution.
A firm sends a fraction of its orders to the crowd and the rest to a third-party logistics carrier (3PL) at a fee per package. The crowd orders are batched first-come first-served into sets of customers, in all, and each set is one tour from the depot. drivers serve the sets, with an integer, and each is paid an hourly wage for busy time. The driver population has size .
The data are the means and standard deviations of interarrival times and of on-site times, tour speeds , a tour constant , the conservatism levels , the delivery window and a stability slack . Driver has mean opportunity cost , with a common standard deviation . Write for the order statistics, and
Problem (14) of the paper minimizes over , , where bounds the value-adding time per package. It has four constraint families: an on-time condition for each and each earlier set of the same driver; an on-time condition for each set; stability, ; and participation, . The mission states this program in full and takes it as given. The derivation of (14) from the robust queueing model (7) is not part of the mission.
From the data define the closed forms , , of the paper, and
If , and for the pairs with , then with ,
If (14) is feasible and , then with is the unique optimal solution, and the optimal value is .
Proposition 1 gives a firm a closed-form policy: the share of orders to crowdsource and the wage that makes the drivers' participation constraint bind. Its three bounds have direct meanings. says sets must form fast enough, says a driver's earlier sets must leave the driver free in time, and is stability. The paper's numerical study and managerial conclusions rest on this solution.
The result is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it adds a precise record of the statement, because the printed proposition needs repair:
The concrete instances above are stated and proved in Lean in the development's verification files.
The obvious argument treats each constraint as an upper or lower bound on and reads off an interval, and the step that fails is its sign analysis. After substituting , the first family has the shape , and which way it bounds depends on the signs of both and . The source's interval is correct only with the hypothesis above, and a formalization must track each pair through that case split. The rest of the difficulty is bookkeeping: four interacting families of 1-indexed double sums, with square roots, a ceiling, and the possibility that is empty.
Lemma 1 has a separate difficulty: the maximum over must be attained, and the candidate maximizer has to satisfy the constraint for every subset , not only for .
Everything is real-valued. The sequences are functions read on their printed 1-based ranges, drivers are Fin pop, and Params carries the data. Valid holds the standing signs: and , with replacing the paper's " smaller than any other number". No sign is imposed on , and is a primitive positive number. lives in WithTop ℝ, with value when every is empty, in particular when . The sum is defined by sorting, not as a minimum over subsets, which would pre-empt Lemma 1.
Trivializing the goal is ruled out: feasibility is the four printed families with their sums and roots, never the interval of (21), and is the closed form, not an infimum of feasible wages. The development proves that the hypotheses are satisfiable at a point where (14) is feasible and at one where it is infeasible.
Only Mathlib is needed. The uncertainty set and the order-statistic sum are the parts reusable elsewhere. Welcome contributions are proofs of the goal and milestones, and also formal links from (14) back to the model (7) through Lemmas 2–7, which this mission does not state.
Ellsberg's two-urn experiment (Ellsberg 1961) asks a decision maker to bet on the color of a ball drawn from a risky urn, with known proportion one half of red balls, or from an ambiguous urn of unknown composition. Most people bet on the risky urn whichever color they bet on, which no single prior over the ambiguous urn can explain. The maxmin expected utility model of Gilboa and Schmeidler (1989) explains it: the decision maker holds a set of priors and evaluates every bet by its worst-case expected utility.
Epstein and Ji (arXiv:1708.01890v2) ask what happens when the decision maker may first sample signals about the ambiguous urn, at a cost per unit of time, before betting. Answering this requires a model of learning under ambiguity that is dynamically consistent, so that the plan chosen at time is still optimal later. The paper uses the continuous-time recursive multiple-priors utility of Chen and Epstein (2002), adapted to learning with the weak formulation of the signal process. The question is an optimal stopping problem in which the expectation is replaced by an infimum over a set of probability laws, and the paper solves it in closed form. The classical single-prior benchmark is the Bayesian sequential testing problem of Wald and of Arrow, Blackwell and Girshick (1949), solved in continuous time by Peskir and Shiryaev (2006).
An unknown parameter , , drives the signal , with known and Brownian motion . The set of priors is with . Updating each prior by Bayes' rule gives the posterior interval for the probability of , which is an explicit function of .
On a probability space with reference measure , under which is a Brownian motion for a filtration , each prior gives a drift , the posterior mean of . A density generator is a progressively measurable process with for some prior , which may change with . The predictive priors are the laws under which is a Brownian motion. Choosing the prior separately at every date and state is what makes the resulting utility time-consistent.
There are three actions: , , and an outside option with payoff . The payoffs are . Stopping at pays
and learning costs per unit of time. The problem (9) is
over the stopping times with .
In Ellsberg's urns, is the bias towards red (), the priors give probability in ( measures ambiguity), () bets on red (blue) from the ambiguous urn and pays , and bets on the risky urn and pays .
Let , and let solve . Then:
(ii) If , let be the unique root of . Then
is optimal and positive. On stopping, the decision maker bets on red if and on blue if , and never on the risky urn. Finally, increases with on .
The milestones follow the paper's proof: the closed form of (§5.1); the indifference point (§4); the boundary maps and (38); Lemma 4.1 on the critical values (30)–(32), (36)–(37); the existence of a valid model and of the worst-case prior (41); Lemma 5.1 for the value functions (44) and (50); the drift comparison (p.27); the integrability bound (49); the identification of as the maxmin value; Theorem 4.2(a), the general solution under payoff symmetry; and the Ellsberg corollaries (26), and the monotonicity of in .
Theorem 3.1 shows that an ambiguity-averse decision maker rejects learning exactly when ambiguity is large relative to the stakes, . When some learning is optimal, the risky urn is chosen only if no learning takes place, and more ambiguity means longer sampling. Equation (26) gives the value of the option to learn in closed form. Theorem 4.2(a) solves the general two-parameter problem under payoff symmetry, with the risky option either chosen on a middle band of signals (case (a.i)) or never chosen (case (a.ii)).
The results are proved in the paper, which is published in Operations Research (2022). None of them has a machine-checked proof. The mission produces a formal statement of a continuous-time maxmin stopping problem with learning, and of its solution, on top of Mathlib's Brownian motion and stopping times. The definitions of predictive priors through density generators, and of the maxmin objective, can be reused for other robust stopping and filtering problems.
The obvious approach is to solve the classical optimal stopping problem under one fixed prior and take the worst one. This fails because is not generated by the priors in one at a time: the worst-case law switches between the upper and the lower prior when the signal crosses the indifference trajectory . The value function then consists of four pieces, joined by smooth-fit conditions at the stopping boundaries and by a smooth connection at . Showing that the value under is also the maxmin value needs a drift comparison valid for every density generator, and a bound on uniform over , so that the stochastic integral in the verification argument has zero expectation under every prior. Mathlib has no Itô integral, Itô formula or Girsanov theorem, so each of these steps needs new infrastructure.
Time is , and stopping times take values in . A valid signal model consists of , a probability , a filtration and a signal with and continuous paths, adapted to , such that is a -Brownian motion. A valid model must also satisfy the conclusion of Girsanov's theorem, which the paper asserts on p.6: every bounded progressively measurable yields a probability, equivalent to on each , under which is a -Brownian motion. This is a real condition, since it fails for a filtration augmented by all null sets of , so the milestone on the worst-case prior also asserts that a valid model exists. The filtration is any filtration with these properties, which includes the paper's when its augmentation is read so that p.6 holds. Predictive priors are characterized by this Girsanov property rather than by their density. Posteriors are given by the paper's closed form (12). The infimum and supremum in (9) range over and over , never over all measures or all random times. The goal also asserts that is nonempty, which rules out a degenerate objective.
Three printed slips are corrected, each with its evidence in the statements: the payoff in (19), the term in (34), and in place of in Theorem 4.2(a.ii). The Lean files also correct and in Lemma 5.1.
A complete development needs the Itô formula for functions with a kink, the Girsanov theorem on the Brownian filtration, optional stopping for exit times of Brownian motion with bounded drift, and a verification theorem for optimal stopping. All of these are reusable beyond this mission. Contributions to any of them are welcome, as are proofs of the deterministic milestones (closed forms, the indifference point, Lemma 4.1, (26), monotonicity of ), which need only real analysis.
Stable assignments are the standard output of centralized school choice, but insisting on stability can leave many students worse off than necessary (Faenza–Zhang, §1). Morrill (2016) proposed legality as a relaxation motivated by legal standing: a student who forms a blocking pair has a complaint only if the remedy, the assignment of that student to that school, is itself considered feasible. A set of assignments that is consistent in this sense is a von Neumann–Morgenstern stable set for a dominance relation between assignments.
Timeline:
An instance has a finite bipartite graph of students and schools , a strict ordering of the neighbours of each vertex , and quotas . Any neighbour is better than no partner. For , the subinstance keeps the vertices, the induced preferences and the quotas, and has edge set .
An assignment is a set with at most one edge at each student and at most edges at each school ; is the set of all of them, and . An edge is a blocking pair for if and either for some or . Following Morrill, an assignment blocks if some edge of is a blocking pair for . This is not the usual notion of a blocking pair alone: the blocking edge has to belong to an assignment under consideration. is stable if no edge of is a blocking pair for it; is the set of stable assignments.
For , is the set of assignments blocked by a member of . The set has the legal property if : no member blocks a member, and every non-member is blocked by a member.
There is a unique with the legal property, and for ,
The statement holds for every finite instance and has no constants.
The theorem turns a definition by a fixed-point condition over the exponentially large family into a statement about one graph: legal assignments inherit the distributive lattice structure and the algorithms of stable assignments. The source uses it to compute the set of legal edges and to speed up Kesten's mechanism with consent. Every later result of the source depends on it.
The results are proved in the source and in Morrill's report. None of the statements of this mission has a machine-checked proof on the platform, which currently has one-to-one stable marriage (the Gale–Shapley algorithm, the lattice) and a many-to-one market without edge deletion. This mission adds one-to-many stable assignments with quotas and vacancies, edge deletion with fixed preferences, von Neumann–Morgenstern stable sets of assignments, and rotations in the one-to-many setting.
The obvious route is to replace each school by seats and quote the one-to-one theory. It fails: the seat reduction is a bijection on stable assignments but does not preserve legality (Example 3.2 of the source gives an instance where the legal set of the reduced marriage instance is not the image of the legal set). A second naive idea is that a fixed point of exists by monotonicity and is therefore legal. Monotonicity gives a fixed point, but the legal property needs that every edge of is used by a member of , and this is the content of the hardest step, Lemma A.6. That step combines the proposal process, rotations and the structure of assignments that do not block each other.
Students and schools are finite types with decidable equality. Instance A B holds E : Finset (A × B), preferences prefA, prefB as strict total orders on the whole other side, and quotas q : B → ℕ, with allowed. Only comparisons among neighbours matter, and restrict changes the edge set only. Assignments are Finset (A × B), families of assignments are Set (Finset (A × B)), and an unmatched vertex is worst.
The family G.assignments is all assignments, not only maximal or stable ones, and uniqueness is among all subsets with the legal property; restricting either would trivialize the goal. Blocking keeps the vacancy clause. The rotation definitions correct the source: the source's lacks a vacancy clause and its displayed definition of a rotation lacks the condition , and without these Lemma 4.2 fails. The source does not state the Gale–Shapley procedure, so it is defined here as a step relation with an arbitrary proposer. Lemmas 3.4–3.6 state "the legal set of is " as an equivalence, with no choice function. Every difference from the source is listed at the end of the item's statement.
Definitions: Def_LegalAssign_Instance, Def_LegalAssign_legalSeq, Def_LegalAssign_Rotation, Def_LegalAssign_GaleShapley. The model and the rotation theory are reusable beyond this mission. Proofs of the milestones, and intermediate lemmas such as the seat reduction of §2.2, are welcome.
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic constraints. Binary integer programs, max-cut, and many robust and polynomial optimization problems can be written this way. Any QCQP has a lifted form in which the vector variable is replaced by the matrix ; dropping the rank constraint on gives the standard semidefinite programming (SDP) relaxation. Deciding whether this relaxation is exact is NP-hard in general (Laurent and Poljak 1995), so structural conditions that guarantee exactness are of direct interest.
Rank-one generation is the strongest such condition at the level of the feasible set: it says the SDP feasible cone is exactly the convex hull of its rank-one points, so the relaxation loses nothing for any objective with a finite SDP value. It is the semidefinite analogue of the integrality of a polyhedron in integer programming. The same property also decides when every quadratic form that is nonnegative on a real variety is "immediately" nonnegative, that is, a sum of a positive semidefinite form and a combination of the defining forms.
Prior work:
Let be the space of real symmetric matrices, the cone of positive semidefinite (PSD) matrices, and the trace inner product. For a set define
the cones cut from by linear matrix inequalities (LMIs) and by linear matrix equalities (LMEs). A closed convex cone is rank-one generated (ROG) if
For write , so that for symmetric . The zero set of the forms is .
For every and all , with ,
Both directions are part of the goal, and is unrestricted.
The milestones follow the paper's own chain:
The result. Before this theorem the only explicit characterization of the ROG property for an LMI-defined cone was the one-LMI case. Theorem 3 extends it to two LMIs and shows that exactly two mechanisms exist: a PSD aggregation of the constraints, or a common rank-two structure with a shared vector . It gives short certificates in both directions, and it implies that outside dimension , condition (i) alone decides the question.
The formalization. The theorem is proved in the source, and Theorem 5 and Lemma 16 are cited there from earlier work rather than proved. No machine-checked proof of Theorem 3 is known to this mission. A complete development also produces general results that do not depend on the two-LMI setting: the extreme-ray criterion, the behaviour of ROG under faces, a machine-checked Dines theorem, and Hildebrand's Carathéodory bound.
Sufficiency is the accessible half. The central difficulty is necessity: from the failure of (i) and (ii), one must exhibit a matrix of that is not a convex combination of rank-one points in , for every pair of matrices and every .
The natural first attempt is a rank bound on extreme rays. It settles one constraint, but with two equalities the Barvinok–Pataki bound still allows extreme rays of rank two, so it cannot separate ROG from non-ROG cones. A second natural idea is to pass freely between inequalities and equalities. This fails in general: the paper shows that both directions can destroy the ROG property, and the equivalence of Corollary 3 is special to at most two constraints. A third is to treat (i) as the whole answer, but (ii) is a genuinely separate case: it arises only when the joint range has dimension three, where the cone is ROG although no nonzero combination is PSD.
The case analysis is also not uniform in the dimension, and depends on counting the real common zeros of two quadratic forms, which is Bézout-type information that has to be made elementary in Lean.
Conventions the Lean development commits to:
Matrix (Fin n) (Fin n) ℝ. is IsSymm and is Matrix.PosSemidef. is (M * X).trace, is x ⬝ᵥ (M *ᵥ x), and is Matrix.vecMulVec x x.ROGCones.IsROG is a predicate on an arbitrary set of matrices. Every set it is applied to is a closed convex cone in , or the empty face in Lemma 3, and Lemma 1 carries the cone hypotheses explicitly.{M₁, M₂} is a Set, and is allowed; is arbitrary, including . Corollary 3 is stated for all pairs, which extends the paper's .Condition (i) requires . Without it the condition always holds and the "only if" direction is empty. Condition (ii) requires the same in both matrices, and is the symmetrized product.
A complete development needs, beyond Mathlib's PosSemidef, convexHull, IsExtreme and Matrix.rank: extreme rays of pointed closed convex cones in finite dimension, the block decomposition of PSD matrices, Dines's convexity theorem, conic Gordan–Stiemke duality for subspaces of , and Hildebrand's lemma. The definitions, extreme-ray criterion and Dines theorem are reusable beyond this mission. Contributions to any milestone are welcome, including an independent proof of a cited result. Related results already machine-checked include the S-lemma ModernConvex.SLemma.s_lemma and the rank-one witness ConvexOptimization.field_of_values_psd_witness.
Admissions to the Indian Institutes of Technology and other centrally funded technical institutions run through a single clearinghouse that allocates tens of thousands of seats each year. Seats at each program are reserved for members of the Scheduled Castes (SC), Scheduled Tribes (ST) and Other Backward Classes (OBC); the rest are open-category seats available to everyone. In Ashoka Kumar Thakur v. Union of India (2008) the Supreme Court of India ruled that OBC seats left unfilled must revert to general use. This de-reservation interacts with the reservations themselves: the deployed procedure, described by Baswana et al. (2018), re-runs the whole deferred acceptance algorithm until no OBC seat is vacant.
Aygün and Turhan (arXiv:2103.05899) show that this "multi-run DA" is inefficient and manipulable, and they propose to perform de-reservation inside each institution's choice rule instead. The resulting mechanism, DA-BT, is characterized by five axioms that formalize the legal and policy requirements. The mission formalizes that characterization.
There is a finite set of individuals and a finite set of institutions. The position categories are , with the open category, and the reserve categories are . Each individual reports a membership ; reporting a reserve membership is optional, and a GC individual is eligible only for open positions. Institution has a capacity vector and a strict priority over ; is acceptable at when . Each individual has a strict preference over .
The India Reserves rule fills the open positions with the highest-priority acceptable applicants in , then fills each reserve category with the highest-priority acceptable remaining members of , up to . The backward transfers rule runs with ; if OBC positions are vacant at iteration , it moves them to the open category and runs again, stopping at the first iteration with . Its output, with category labels, is .
An assignment gives each individual either nothing or an institution–category pair. It must respect memberships, the total capacity , and each reserve capacity ; open positions are not capped by , which leaves room for de-reservation. A mechanism maps every preference profile and membership profile to an assignment. DA-BT is applicant-proposing deferred acceptance in which each institution, at each step, holds of its held and new applicants and rejects the rest.
The five axioms are individual rationality, meritocracy (an individual who envies has lower priority than every open holder there and every holder of her own reserve category), non-wastefulness (if she envies , the positions she is eligible for there are exhausted, de-reserved OBC seats counting as open), open-first (open-or-OBC positions are filled up to , open holders outrank reserve holders, and no de-reservation is unnecessary), and incentive-compatibility (truthful reporting of the preference and the membership is a dominant strategy).
For all finite , , capacities and priorities , and every mechanism into feasible assignments,
with equality of assignments (labels included) on the whole domain of preference and membership profiles.
The "if" direction: DA-BT outputs feasible assignments and satisfies each axiom (proof of Theorem 4, pp.40–42), including Theorem 3 (incentive-compatibility), which rests on Lemma 1, substitutability and size monotonicity of , strategy-proofness for fixed memberships, Theorem 1 (the BT rule complies with the spirit of affirmative action), the improvement property of reporting, and the fact that withholding membership never helps. The "only if" direction: Lemma 2 (the four non-incentive axioms imply stability with respect to the ), Lemma 3 (DA-BT is the only stable and strategy-proof mechanism, at the level of matchings), and the statement that open-first determines the category labels.
The characterization says that, given the reservations, the de-reservation rule and the policy goal that open seats have higher cutoffs than reserve seats, there is exactly one acceptable mechanism, and it is not the deployed one. Theorem 3 removes the two manipulations of multi-run DA (misreporting preferences, withholding membership), and Theorem 2 of the paper, not part of this mission, shows that DA-BT Pareto-dominates multi-run DA.
All results are proved on paper; none is machine-checked. A formal development checks a characterization whose printed statement is false at two points (below). It also gives the platform reusable objects: many-to-one deferred acceptance under institution choice functions, category-labelled assignments, a reserve choice rule with iterated de-reservation, and the substitutability and size-monotonicity properties that drive strategy-proofness. The one-to-one strategy-proofness of the proposing side is already on the platform (AGT.male_propose_strategyproof).
The "if" direction needs strategy-proofness of deferred acceptance under substitutable, size-monotone choice functions (Hatfield and Milgrom 2005) and the respect-for-improvements theorem of Afacan (2017), specialized to . Substitutability of is not the textbook argument: adding an applicant can change how many OBC seats are de-reserved, which changes the open capacity in every later iteration. The proof controls this through Lemma 1.
The "only if" direction relies on the uniqueness of stable and strategy-proof mechanisms (Hatfield, Kominers and Westkamp 2021), which identifies only the matching. The printed proof stops there. The category labels must be recovered separately, and this is where the printed open-first axiom fails.
Individuals and institutions are arbitrary finite types, either possibly empty. Priorities and preferences are rank bijections and (rank 0 best, none for ), so every strict linear order occurs. Acceptable sets are arbitrary. Capacities are in , zero allowed. Memberships are Option Res, none being GC. , and DA-BT return labels, and DA-BT is defined by its algorithm, with explicit iteration bounds that are never reached, not as "the applicant-optimal stable matching".
Theorem 4 is corrected in two places and read in three places, each declared on the items:
A trivializing formalization is ruled out: DA-BT is computed by its algorithm, mechanisms are arbitrary functions on the full domain, and the equality is of assignments, not matchings.
A complete development needs finite-set reasoning about top- selections, an invariant-based analysis of the DA loop, and the three external theorems specialized to . Proofs of the external results in general matching-with-contracts form would be reusable beyond this mission and are welcome as supporting lemmas.
Corporate insiders are barred from trading on private information, but in the United States they may donate appreciated shares to charity. The donor deducts the shares' market value from ordinary income and never pays capital-gains tax on the appreciation. Empirical work documents that such gifts are well timed: donations by insiders predict poor future firm performance (Yermack 2009; Avci, Schipani and Seyhun, University of Pennsylvania Journal of Business Law 18(4), 2016). Arya, Mittendorf and Ramanan (SSRN 4003698, published in Management Science, 2022, doi:10.1287/mnsc.2022.4514) ask what this channel does to an equity market. Their answer is that, because a charity sells donated shares, an insider's gift is an informed order, and the market as a whole becomes more informative and more liquid. This mission formalizes the price-efficiency half of that answer.
The model extends the one-shot market of Kyle (1985), in which informed traders, noise traders and a competitive market maker interact, and its many-trader version (Fishman and Hagerty, Journal of Finance 44(3), 1989), which the paper uses as its no-donor benchmark.
A firm's value , , is learned before trading by insiders (the donors) and by informed traders. Insider holds shares and has other income ; she cannot trade, but donates shares, of which the charity immediately sells a portion . Trader sells shares. Retail investors sell . Each insider also has a private motive for giving . All these variables are independent. With tax rates (capital gains) and (ordinary income), the utilities are
A market maker observes the aggregate supply and sets . The standing assumptions are and the interior condition
A linear equilibrium is a profile of linear strategies , and a linear price such that every trader and donor maximizes expected utility for every realization of her information, and almost surely. Price efficiency is .
Under the standing assumptions and , a linear equilibrium exists, every linear equilibrium has
and this closed form satisfies
Proposition 3 makes the paper's headline claim precise: allowing insiders to donate makes prices more accurate, and an extra donor improves accuracy more than an extra informed trader. A donor weighs the price at rate against the value at rate , so her gifts load more heavily on than a trader's orders. The same comparative statics with respect to tax rates are the paper's policy content: raising either tax rate makes gifts less informative.
The results are proved in the paper by hand, and the chain has been checked symbolically, but none of it is machine-checked. Formalizing it produces a multi-agent Kyle equilibrium with heterogeneous informed parties, in which existence and uniqueness are stated against a genuine equilibrium predicate (optimality plus Mathlib's conditional expectation), not against first-order conditions. The Gaussian-projection milestone (A4) is a general statement about linear functions of independent normals and is reusable for every linear-Gaussian market model.
The closed-form algebra is routine; the work is in the probability. The obvious route takes to be the linear projection, but that identity is the content of (A4): it needs the joint Gaussianity of to turn zero covariance of the residual into independence, and then the independence property of conditional expectation. Uniqueness needs two further arguments the paper leaves implicit: that admits no equilibrium (a donor's payoff is then linear or convex in her gift, so has no maximizer), and that an almost-sure equality of two affine functions of forces equal coefficients, which uses . Every expectation is a Bochner integral, so each step also needs the integrability of quadratics in Gaussians.
The sample space is , carrying , with the product of gaussianReal laws; and (with the motives are deterministic). Strategies are linear with free, agent-specific coefficients; symmetry, and the formulas are conclusions. Optimality holds for every realization; efficiency is condExp with respect to the σ-algebra generated by , almost surely. is the functional , never the closed form.
The goal assumes . Tax rates are nonnegative, and the printed assumptions alone allow , where no equilibrium exists (for , , , , the printed is negative). The derivatives and are derivatives of the closed form in real , evaluated at the model's integers, as in (A6). The goal states existence of an equilibrium together with the formula for every equilibrium, so it cannot hold vacuously.
Needed infrastructure: moments and integrability of affine functions of independent Gaussians; the jointly Gaussian conditional expectation (Mathlib's HasGaussianLaw, condExp_indep_eq); calculus of rational functions. Contributions to any milestone, and general lemmas on Gaussian projection, are welcome.
In a classical optimal stopping problem the reward collected at the stopping time is a fixed function of the state. Many decisions do not have this shape: an agent may commit to an uncertain option whose outcome is revealed only after a random delay, and if it fails the agent is back where it started and must decide again. The reward of committing then depends on the value of the problem itself. Colaneri and De Angelis call these recursive optimal stopping problems and motivate them by a trader who sells a block of shares either on the lit exchange (certain execution at the quoted price) or in a dark pool (a better price, but an order that executes only with some probability, after a random waiting time, and otherwise has to be re-placed). The same structure appears in investment with implementation lags and in grant or tender applications that can be resubmitted.
The question this mission formalizes is the foundational one: is such a problem well posed? The value function appears on both sides of the dynamic programming equation, so neither its existence nor its uniqueness, nor the existence of an optimal stopping rule, follows from the standard theory of optimal stopping (Peskir and Shiryaev; Shiryaev).
Fix a probability space with a filtration that is right-continuous and complete, with . The state is a stochastic flow on : is the process started at , it has right-continuous paths, is -adapted, has the strong Markov property and is quasi left-continuous. Write .
The data are a discount rate , a success probability , the law of a non-negative delay , and two payoffs . For a non-negative continuous define
the supremum over all -stopping times with values in , the payoff being on . is the value of committing to the delayed option when is the value of starting afresh; is the value of choosing the best moment to take the better of the two options. Problem 2 asks for with .
Solutions are sought in the linear-growth class
Assumption 2.7 asks that be continuous almost surely; that for some the process be a supermartingale; that on compacts; that when ; and that . The finite-horizon version (Problem 2') runs on with a space-time flow , stopping times , integrated over , and Assumption 2.8: the delay law has no atom in .
For both horizons: Problem 2 (Problem 2') has a unique solution ; the first contact time
is optimal; , , is a right-continuous non-negative supermartingale; and is a right-continuous non-negative martingale, for every starting point.
In the order of the proof:
The theorem turns the recursive problem into an ordinary optimal stopping problem with a known gain , so the whole toolkit of optimal stopping (stopping sets, free boundaries, smooth fit, variational inequalities) becomes available. The paper uses it in §4 to reduce the dark-pool trading problem to one dimension and to describe its stopping region; an equivalence lemma (Lemma 2.5) transfers it to the original control-and-stopping formulation. The result places no restriction on the delay law in the infinite horizon, so it covers immediate-or-cancel orders, deterministic delays and delays capped at a cancellation time alike.
The theorem is proved in the paper; nothing in this mission is open mathematics. No machine-checked proof exists. The mission produces a formal statement of the well-posedness result at full strength, with both horizons, all three regularity clauses, and uniqueness in , and the intermediate estimates as separately provable milestones. The contraction and completeness milestones are analysis; the (super)martingale and semicontinuity milestones require optimal stopping theory for Markov processes that Mathlib does not yet have.
The contraction estimate itself is short once is known to map into itself, and that is the obstacle: the image must be continuous. Lower semicontinuity of a stopping value comes from the Feller property, but upper semicontinuity does not hold in general and is the content of Lemma 3.4; it is where the stability condition (iii) of Assumption 2.7 is needed, since nearby starting points must produce uniformly close payoffs along a whole family of near-optimal stopping times. In the finite horizon the deadline moves with the starting point, so the admissible stopping times themselves change. Lemma 3.3 itself rests on the general theory of optimal stopping for strong Markov processes (Shiryaev; Peskir–Shiryaev), including optimality of the first entry time when it is infinite with positive probability.
is EuclideanSpace ℝ (Fin d); the finite-horizon state space is . Time is ℝ≥0, stopping times take values in ℝ≥0∞ (Mathlib's IsStoppingTime), and the discounted payoff is on , the paper's convention. and are Lebesgue integrals of non-negative functions with values in , so no default value enters; the weighted norm is also -valued. is the law of the flow started at under one measure . The supermartingale on uses the filtration extended by and the value at ; finite-horizon processes are frozen at . The finite-horizon hypotheses follow the reading recorded in the items: the space-time flow exists for all times, Assumption 2.7 (i) applies to its spatial part, and (ii)–(iii) hold for starting points in .
A formalization that fixes the delay law, drops the finite horizon, restricts to bounded stopping times, or encodes expectations as Bochner integrals (which return on non-integrable functions) would state a different theorem; none of these is used.
A complete development needs: optional sampling for right-continuous supermartingales on , progressive measurability of right-continuous adapted processes, entry times of closed sets as stopping times under the usual conditions, the Snell-envelope characterization of the value of a Markovian stopping problem, and Banach's fixed-point theorem. These pieces are reusable well beyond this mission. Contributions of any of the milestones, or of general optimal stopping lemmas they rely on, are welcome.
A customer who is about to buy a new product usually reads the reviews of earlier buyers. Those reviews say something about the product's quality, which all customers share, and something about its fit with the reviewer's own taste, which only similar customers share. A platform decides how much of this to show. In the paper's examples, Apple's App Store resembles a display of reviews by cluster, and Google Play resembles a global average.
Xiao, Chen and Tang (2021) analyse this choice in a two-period pricing model with Bayesian customers. Under an association-based policy (AP) a customer sees the reviews of the own cluster, under a global policy (GP) the average over all clusters. Neither policy dominates: AP is relevant but thin, GP is plentiful but mixes tastes. The paper then proposes a joint policy (JP) that shows both numbers. The question is what JP loses against a full policy (FP), which shows the ratings of every cluster separately. The prior follows Papanastasiou and Savva (2017) and Yu et al. (2016).
A firm sells in clusters over two periods. Quality and cluster preferences are unknown, mutually independent, and . The cluster value is .
In period 1 the firm sets a price in each cluster, and sales are with . A fraction of buyers rate the product, each with perception noise of precision , so the average rating satisfies
The development uses the rating statistic with independent , so that for and when no ratings exist.
In period 2 a mass of customers arrives in each cluster. A customer of cluster observes, depending on the policy , the statistic (AP), (GP), (FP) or (JP). The customer evaluation is the posterior mean . The firm then earns in cluster . Its profit is
and is optimal for when it maximizes over .
For every parameter tuple and :
there is such that is optimal for FP and every optimum of FP equals ; moreover is optimal for JP with
and AP and GP each have optima with profit strictly below this value.
The milestones follow the paper's chain, in order: the optimal second-period price (3); the posterior means (1), (2), (11) and the JP display of p.24; the a priori laws of Lemma 1, (12) and (13); the profit as a truncated Gaussian integral (6); Lemmas 8 and 2 on the functions , and ; the order of the variances (Lemma 11); the derivatives (25)–(26) and first-order conditions (27); the symmetric variances; the equation (29); and Proposition 3.
The result gives a design rule. A platform can replace cluster-specific reviews by two numbers without any loss of optimal profit, provided the clusters are ex-ante symmetric, and it strictly gains over showing one of the two. JP provides less information than FP when , so the equality is a property of the optimum and not of the two information structures.
Formalizing it adds to the theorem base a Bayesian pricing model with Gaussian signals of sales-dependent precision, in which the zero-sales boundary is part of the domain. The published proofs are pen-and-paper. No machine-checked proof of these statements was found. Printed Lemma 11 is false on the boundary of the sales domain, so the corresponding milestone states the corrected form (strict inequalities only with positive sales); the goal needs no correction. The goal's strict inequalities and the attainment of the optima strengthen what the printed proof writes.
Mathlib has no ready formula for conditioning jointly Gaussian variables, and here the signals degenerate when some vanish, so each posterior mean must be identified as a conditional expectation directly. The tempting route of writing or the profit through the printed closed forms fails at the boundary, where these forms are . A further difficulty is that is not separable across clusters: each depends on all sales, so symmetry of the optimum does not follow from the symmetry of the objective. Finally, the strict dominance over AP and GP is not in the printed proof.
Clusters are Fin N. The prior mean is . The sample space is the canonical product of the Gaussian laws, so the profit depends only on the parameters and . Sales are real, , with no upper bound. Information is a MeasurableSpace generated by the statistics, and is a Mathlib condExp. Optima are maximizers, never a supremum over .
Three shortcuts would trivialize the statement and are ruled out by the definitions: a rating would be a perfect signal at in Lean; a profit defined through the closed forms would remove the Bayesian content; and a ⨆ over would hide attainment.
Assumption 1 of the paper is not assumed. A complete development needs a Gaussian conditioning lemma for finitely many possibly degenerate linear signals, the truncated second moment of a Normal, and conditional Jensen; the first two are reusable beyond this mission. Contributions of general Gaussian conditioning results are welcome.
Firms increasingly screen job applicants, borrowers and customers with algorithms built on observable features. Regulators and the public ask for these algorithms to be made transparent, and firms often resist, arguing that agents who know the algorithm will game it. Wang, Huang, Jasin and Singh (arXiv:2008.09283, 2020; published in Management Science, 2023) model this tension as a game between a firm and strategic agents. They separate causal features, which change an agent's productivity (education), from correlational features, which only predict it. Their first headline result, Theorem 1, says exactly when a profit-maximizing firm is better off disclosing its algorithm. The answer depends on the agents' education costs, region by region in the cost plane.
The model builds on the signaling literature, in which education is both a signal and a source of productivity (Spence, 1973; Weiss, 1983), and on strategic classification, where agents manipulate the features a classifier uses (Hardt et al., 2016).
A unit mass of agents contains a share of high-talent agents (type H) and of low-talent agents (type L). A share of H agents and a share of L agents are high on a correlational feature. Every agent may acquire education at cost (type H) or (type L), with . An agent's productivity is , and the firm pays every hired agent the wage . The standing assumptions are (Assumption 1) and two-sided bounds on and (Assumptions 2 and 3) that exclude trivial equilibria.
In the opaque game the agents do not know the correlational feature. They choose education, ending in one of four states (education 0/1 times feature 1/0), and the firm hires state with probability . In the transparent game every agent raises the disclosed feature, so only education matters (states , ). Each type plays a common mixed strategy: it improves with probability or . The firm's payoff is , where the margin is computed from the masses in state . A Nash equilibrium requires each type to best-respond, and the firm to hire an occupied state surely when and never when . In the opaque game the agents move first and coordinate on the payoff-dominant equilibrium (IsOpaqueOutcome), the one that is best for both types at once.
Let be the firm's payoff at any selected opaque outcome and its payoff at any transparent equilibrium. On seven open regions of the plane (InRegion):
with , the explicit thresholds (13)–(14). The statement also asserts that the compared equilibria exist, so no clause holds vacuously.
The milestones follow the paper's argument: the firm's thresholds (12); the opaque cases that cannot be equilibria; Lemma 1, the selected opaque outcome per region; the transparent cases that cannot be equilibria; Lemma 2, the transparent equilibrium; and the five payoff comparisons (N1–N3, (13), (14), (15), C4).
Theorem 1 overturns the common view that transparency always hurts the firm. Disclosure destroys the predictive value of the correlational feature, but it also intensifies competition on education. Where this makes the types separate (), or where education is productive enough (, ), the firm gains. The thresholds are explicit, so the result gives testable conditions for the regulatory debate.
The printed theorem is false on part of its region map. The paper rules out equilibria in which both types mix ("case 9", p.18). At , , , , and , a point of the printed region , a both-types-mixing equilibrium exists and dominates for both types. Its firm payoff is , below the transparent payoff . The printed case-4 region of Lemma 1 also reverses an inequality. The mission states the corrected theorem: the boundary between and moves to the ray , and the clause, with the same threshold , holds on the enlarged region . No machine-checked proof of any part of the paper exists. A formal proof settles the corrected region map, which so far rests on exact-rational sampling.
The algebra is elementary; the difficulty is completeness. The paper's argument checks a list of nine strategy patterns, each with a guessed hiring vector. A proof of Theorem 1 must instead classify all equilibria: every sign pattern of the four margins, every tie, and every degenerate line inside a region, where continua of equilibria appear. It must then show that the payoff-dominant one exists and has the stated payoff. The obvious shortcut is to argue that L agents cannot need a higher hiring chance than H agents. It fails because the two types sit at different values of the correlational feature: both types are indifferent in a mixed equilibrium whenever . The remaining steps are sign arguments for rational functions of under Assumptions 1–3. The hardest is the positivity of the denominator of the case-9 payoff , whose minimum approaches zero as .
All quantities are real numbers. Strategies are a common mixed strategy per type, with expected masses. Firm optimality is stated through the signed margins, never through the ratios , which are at an unoccupied state. At an unoccupied state the firm hires an educated state with probability 1 and an uneducated state with probability 0. This off-path convention is used by every equilibrium in the paper's appendix, and without it the payoff-dominance selection has no solution in region . Selection compares against every opaque equilibrium, not against the paper's list of cases. Regions are open sets read off Figure 4; boundaries are not claimed. is kept: there the opaque game has no equilibrium on , so that clause is vacuous and existence is not claimed there.
The definitions are self-contained: parameters and assumptions (Params, Standing), the two games (masses, margins, payoffs, utilities), the two equilibrium predicates, the selection, the regions and the thresholds. Contributions are welcome on each milestone. The equilibrium classifications (Lemmas 1 and 2) are the core; the five payoff comparisons are independent ordered-field exercises.
Marketplace platforms often sell their sellers a service that those sellers could otherwise buy or build. Order fulfillment is the standard example: Amazon, Walmart and Alibaba offer logistics and distribution services to third-party sellers, while other platforms have delayed or declined to offer them. Li, Pisano, Xu and Zhu (SSRN 3310484; published in Management Science, doi:10.1287/mnsc.2022.4522) ask how sellers' ability to supply such a service themselves changes the platform's decision to offer it, and the price it charges. Their finding (p.3) is that, in general, the scalability of sellers makes the platform less likely to offer the service. This mission formalizes the benchmark case with one type of seller, Proposition 1, which p.20 calls the paper's main result.
A monopoly platform hosts a unit mass of identical sellers and charges a commission rate on revenue. A seller who sells units earns revenue , with derived demand . Each sale needs an ancillary service. It costs per unit from the market. A seller can instead invest and supply it at unit cost ; the scalable scenario is the one with this option, and the non-scalable scenario the one without it. The platform can pay a fixed to offer the service at unit cost and price .
The game has three stages: the platform decides whether to offer the service and at what price; sellers choose whether to enter and which service to use; sellers choose output. A seller using a service with marginal cost and fixed fee maximizes , and its output solves . Write , , and . If sellers use the platform service at price , the platform earns
In the non-scalable scenario sellers use it when , which gives the profit function . In the scalable scenario they use it when its payoff beats own service, which gives . The investment levels at which the platform is indifferent are
For every model,
and, at an optimum of where sellers use the service and an optimum of ,
The goal also asserts that the maxima are attained, that the optimal prices are unique, and that sellers use the service at the scalable optimum whenever .
The milestones follow the paper's proof: the sellers' stage (the first-order condition, the service choice, the cutoff price and eq. (6)), the jump in at , the calculus of and ending in the quasi-concavity of , and the rewriting of , with the two comparisons behind (a) and (b).
The result separates two channels. Without the service, a platform whose sellers can scale already earns more, since . With the service, it must undercut a better outside option, so its price range shrinks from to . Both channels lower the gain from offering the service. Managerially, a platform should expect less from such an investment when its sellers are able to scale. The paper builds on this benchmark for its results with two seller types and with timing.
The result is proved on paper, and this mission does not change its conclusion. No machine-checked proof of it is known. Formalizing it adds a small platform model in which sellers' behaviour is derived from primitives, a repaired set of hypotheses, and explicit attention to attainment and uniqueness of optimal prices, which the paper leaves implicit.
The conclusion (a) is short once its inputs are available: it compares suprema over nested price sets and uses . The work is in those inputs. The output is defined only implicitly, so its derivative needs an inverse-function argument, and the second derivative of needs along that inverse. The source does not claim that is concave: the structure it uses is quasi-concavity, extracted from the sign of the derivative of . The maxima run over half-open intervals, so attainment needs the behaviour of near price . The cutoff has to be constructed by an intermediate-value argument from Assumption 1 and .
Data and conditions are separated: Params holds the data, and Model extends it with the conditions. All statements use the namespace MarketplaceScalability.
The paper's demand conditions on p.4, , , and , are unsatisfiable, so the printed result would be vacuous. A positive concave function on cannot be strictly decreasing, and a concave function on cannot tend to at . Model keeps the signs on an interval and replaces by its only use: the first-order condition is solvable on for every price in . Linear demand on is an instance. Other conventions: ; prices are positive; is Function.invFunOn, and comparisons at a platform price test first; and use sSup, with attainment proved in the goal; indifferent sellers use the platform service; (b) is weak, since strict inequalities are false.
The cutoff appears in no definition: comes from the sellers' payoff comparison, and , are computed from the primitives. A version with as a free number below and assumed would make (a) a one-line comparison of suprema, and is ruled out.
Everything needed is one-variable calculus already in Mathlib. Proofs of the milestones are welcome in any order. The inverse-function lemma for is the natural starting point, since most later steps use it.
Learning curves are a standard fact of manufacturing: unit cost falls with cumulative output, so a buyer who orders more today buys cheaper tomorrow (Yelle 1979). Procurement contracts with an outside supplier then face a second problem: the supplier knows its own cost and learning ability better than the buyer does, and it also observes privately how learning went. Gao, Nikoofal and Zhang (MSOM 2023) characterize the buyer's optimal long-term contract when cost and learning rate are private ex ante and the learning outcome is private ex post. Their rent formula has a third term, driven by post-contract information, which is absent from the analysis of Baron and Besanko (1984), where, as the paper reads it, the rent depends on pre-contract information only.
One buyer procures from one supplier over two periods with discount factor . In period the buyer sells at price . The supplier has a private type , with , unit cost () and learning rate . After producing it privately observes a learning outcome , and its period-2 unit cost is . Write , , .
The buyer commits to a contract : payments and quantities and for each reported type and outcome. A supplier of type who picks the term of earns
and . The feasible set requires nonnegative quantities, Condition (C) , where if and otherwise, individual rationality , and incentive compatibility in both the type and the outcome. The buyer maximizes her expected payoff on . This is regime .
Let be type 's first best, and let be the quantities of type : when these separate, otherwise, with fixed by the first-order condition. Under second-order and interiority hypotheses, the contract with deferred payments is optimal, , and
with . Every optimal contract has the quantities of and these rents. The printed payment to type is optimal exactly when it is feasible, and that is characterized by a rent inequality.
Lemma 1(b), Claims 1–5, the deferred payment (19)–(20), the lowest rent, the two cases of Step 2, the concavity of the reduced function and the position of the optimum, and one lemma not in the paper, on the incentive compatibility of .
The result gives the optimal transfers and output for a dynamic screening problem with two layers of private information. It shows a rent term that can have either sign, a transfer deferred to the second period, and two regimes according to whether a learned type can undercut an unlearned type . Output of type can be distorted upward. The paper's later comparisons of regimes rest on this characterization.
The proposition is proved on paper only, and the printed statement needs correction. The proof never checks the incentive constraint of type , and the printed payment to type can violate it: at , , , , one gets . The quantities, rents and value survive. Replacing by in the two learning terms of type 's payment restores feasibility. The mission therefore gives a corrected, machine-checkable form of a published result, with each departure from the page declared in its item, together with a counterexample.
The obvious route is to bind the incentive constraint of type and the participation constraint of type , solve the relaxed problem, and stop. That route leaves a gap: nothing in the relaxed problem controls type 's temptation to take type 's term, which has to be derived from the optimality of the candidate quantities. The paper's Claim 4 (that a particular second-period constraint must bind) is false as printed, because a band of transfers gives the same rent.
The reduced objective is piecewise quadratic with up to three pieces, pooled, double-deviation separating and single-deviation separating. It has a concave kink at on which the optimum can sit for an open set of parameters. Concavity of each piece has to be read off Condition (A3), and the pooled piece needs its own bound.
All objects are finite real arithmetic: Params with Params.Standing, Term and Contract, the payoffs, and Params.Feasible. The expectations are two-term weighted sums, and is a Bool. Optimality is Params.IsOptimal, membership in plus a universal bound, because without second-order conditions the supremum can be . Quantities are nonnegative and (C) is written . The second-order conditions are Params.SecondOrder: , plus (A3) if and otherwise. Params.FirstBestAdmissible and Params.Candidate hold the interiority and first-order conditions, with one-sided inequalities at the kink, so the goal does not cover corner optima. Under double deviation the separating quantities are those of App. p.7, not note 9. The slopes slopeRight, slopeGap and marginalRent are explicit formulas, not deriv, because the paper's partial derivatives hold second-period quantities fixed.
Trivializing encodings are ruled out: keeps every constraint, including (IC), and is not defined by the binding constraints or by the deferred payment. The non-vacuity of the hypotheses is checked in all four regimes (pooled, double, kink, single) on the paper's Table 5 base case. The reduced function is defined by an explicit formula, and two milestones show it is the maximum.
Proofs of any milestone are welcome. A reusable byproduct is a treatment of two-type screening with a second round of private information, which no platform definition currently covers. The general objects here are specific to this model, so no platform definition was reused.
In many consumer-goods channels the party with the best demand information is the manufacturer, which controls promotion, product launches and brand planning, while the retailer places the order. Whether manufacturers should tell retailers what they know is a question of practice as well as theory, and the answer depends on how the manufacturers compete. This mission formalizes the main threshold result of Aditya Jain's Sharing Demand Information with Retailer under Upstream Competition (SSRN:3388957; journal version doi:10.1287/mnsc.2021.4116).
The paper belongs to a literature on vertical information sharing. Li (1985) gave the signal framework with linear conditional expectations used here. Gal-Or et al. (2008) showed signaling-driven distortions in the wholesale price of a single manufacturer selling through two retailers, and Shang, Ha and Tong (2016) studied two manufacturers with a retailer holding the information. Jain's setting reverses the direction of that last model: manufacturers hold the signals and sell through a common retailer.
Two manufacturers sell substitutable products through one retailer. The inverse demand is
where is the substitution level, the mean demand level, and a zero-mean demand uncertainty with variance . Marginal costs are zero.
Each manufacturer holds a private signal with , finite and nonzero precision , and linear conditional expectations. Its accuracy is .
Before seeing its signal, each manufacturer decides whether to share it () or not (). This yields four cases: (both share), (neither), and (only shares). After signals arrive, manufacturers simultaneously set wholesale prices , and the retailer chooses orders before demand is realized. The retailer knows a shared signal, and infers an unshared one from the price through the conjectured rule . A linear separating equilibrium is a profile in which for each non-sharing manufacturer, the retailer maximizes its expected profit at every price, and no manufacturer gains by deviating to any other pricing function of its signal. The expected profit is .
Take . Let
With , define
Under , the gap is positive below a threshold , zero at it and negative above it; if fails, for all . The same holds for with and , and for with and and ; for the gap is always positive. Thresholds that exist satisfy .
The relations implied by Assumption 1; Proposition 1, the equilibrium in each sharing case as an if and only if; its reduction under full information; Proposition 6(a), for ; and clauses (a), (b), (c) of Proposition 5 separately.
The theorem says when substitutability turns the sharing preference around, and it locates the turning point exactly in . At low substitution, sharing removes a wholesale-price distortion that hurts each manufacturer. At high substitution, that distortion softens price competition, and withholding becomes attractive. Proposition 5 is the basis of the paper's analysis of equilibrium sharing patterns with equal accuracies.
The formalization adds a corrected statement. The printed clauses (a), (b) and (c) fail at some parameters, so the exact conditions state what is true: at , no threshold exists, and at , , neither nor exists. Printed Assumption 1(b) is also replaced, as it contradicts the relations derived from it. On status: the paper's proofs are in an Electronic Companion. The exact conditions were derived from the limits of the gaps and tested by exact root counts on rational grids; they are not proved for all parameters. No part of the result is known to have a machine-checked proof.
The equilibrium is the first obstacle: a non-sharing manufacturer's deviation moves both the retailer's response and its inference, so the best-response problem must be solved against all pricing functions, on and off the path, and uniqueness requires the full system of coefficients, with no assumption on the sign of .
The second obstacle is the sign analysis. A natural first idea is to compare only the part of the profits, which produces from . This fails, because the part of each gap has the same order as . The gaps are rational functions in with numerators of degree up to 11, and the claim is uniform in , in both directions of each condition. Clause (d) compares roots of different such polynomials.
The probability space is general, with . Manufacturers are indexed by Fin 2, and 1 - i stands for . is a variance. is encoded as . Assumption 1(b) reads . The relation is a hypothesis. Quantities are unconstrained in sign, as in problem (2). Manufacturer optimality is ex ante, over all measurable pricing functions in . Profits are integrals along strategies, not closed forms, and they are taken along any family of equilibria. This rules out a trivial formalization: a closed-form would detach the goal from the game, and a copy of the printed (b) would be unsatisfiable. The signal model is inhabited at every and by a finite example.
A complete development needs the moment identities of the signal model, a uniqueness argument for the quadratic game, closed-form profits, and an exact sign analysis of polynomials. The signal-model lemmas are reusable. Contributions of any of these parts are welcome, and so are alternative proofs of the conditions .
Specialty coffee roasters buy single-origin beans through direct trade: they contract acreage with a grower before harvest and take the crop that passes the quality specification. A single-origin label (SL) sells at a premium to a small connoisseur segment, while a blend label (BL) has a much larger market. Beans bought for SL can always be sold as BL, a flexibility called downward substitution. The contract is signed before two things are known: the harvest yield and the BL price.
Webster, Kazaz and Gheibi (2024) model this as a two-stage stochastic program with recourse and identify three optimal sourcing strategies: specialized (no downward substitution), diversified (consistent downward substitution) and mixed. The problem joins random-yield planning, surveyed in Yano and Lee (1995), with revenue management under the multinomial logit (MNL) choice model.
Fix a price sensitivity , nominal qualities and a post-harvest cost per normalized pound. The pre-harvest cost of normalized acres is continuous, nondecreasing and convex on , and need not be differentiable. The pair of blend price and yield has a joint law with support , where and .
Once is realized, the harvest is . Selling as SL clears the market at the MNL price
and the rest sells as BL at , with profit . The second-stage value is the maximum of over , . The first-stage problem maximizes over .
Let be the Lambert W function and . The unconstrained second-stage quantity is , and the benchmarks are
An acreage is specialized if , diversified if and mixed if . With the markups and , put , , and define the expected shadow price .
the second when an optimal acreage exists; some optimal acreage is mixed exactly when neither (11) nor (12) holds; and under uncertainty any two optimal acreages lie in the same class.
The result gives an exact test, in terms of marginal revenue and marginal cost at two explicit acreages, for which strategy a roaster should adopt, for every joint law of price and yield and every convex cost, including the piecewise linear costs the paper calls typical. It is the basis of the paper's later comparative statics.
The theorems are proved in the paper, and to our knowledge none has a machine-checked proof. Formalizing them adds a capacity-constrained MNL pricing problem, a two-stage program with recourse and random yield, and one-sided optimality conditions for a concave objective with a kinked cost. Three printed statements need corrections, each with a counterexample satisfying all of the paper's assumptions:
The phrase "is optimal" is read existentially, and a clause is added that all optimal acreages share one class under uncertainty.
The first-order condition at a benchmark does not follow from a pointwise derivative. The second-stage value has a different formula on the constrained and unconstrained realizations, and the boundary between them moves with . Differentiating under the integral therefore requires seeing that the two pieces meet with equal derivative on . The naive argument "Proposition 2 gives the optimum" also fails, because may have kinks, so that the set in Proposition 2 need not have a maximum: the conditions must be one-sided and rest on concavity. Strictness on needs mass near the corner , which is the role of the support hypothesis.
The joint law is a probability measure on . Support is encoded as with positive mass of every ball around a point of ; no density, independence or atomlessness is assumed, and the rectangle may degenerate to a point. The feasible set uses , since no finite price clears the market at . are derivWithin on Ioi and Iio. is the covariance, since is undefined for zero variance. 's integrand is explicitly where . The order of and is not assumed.
and are defined as optimal values. Defining them by Proposition 1's formula would trivialize the mission and is ruled out. The strategy classes are thresholds on , not Lemma 1's probabilities.
A complete development needs elementary facts on , the analysis of the concave second-stage objective, and differentiation under the integral on the compact support. The Lambert W definition is reusable beyond this mission. Contributions of any milestone or of auxiliary lemmas are welcome.
A bank funds its assets with two kinds of debt that a nonbank firm does not mix in the same way: insured deposits, which earn the bank a service profit but cost a risk-based insurance premium, and nondeposit debt (bonds), which carries a credit spread. Regulators close a bank whose total capital falls below a fixed fraction of its assets, and the deposit insurer charges a premium that grows with the deposits it protects. How a value-maximizing bank should split its funding between the two, given these rules, is a question about bank regulation as much as about corporate finance: the split determines how much capital stands between the bank's assets and the insurer's loss.
Sundaresan and Wang (Management Science, 2023) extend the structural capital-structure model of Leland (1994) to banks with deposit profitability, risk-based deposit insurance and a total capital requirement, and solve the bank's liability choice in closed form. Their Proposition 2 is the paper's main result: the value-maximizing bank uses nondeposit debt to place its own default boundary exactly at the regulator's closure boundary. With no deposit profit and no insurance subsidy the formula reduces to Leland's optimal leverage for a nonbank firm.
The parameters (Table 1 of the paper) are the asset volatility , the asset cash-flow rate , the risk-free rate , the deposit profitability , the debt advantage (tax rate) , the liquidation cost , the capital requirement and the insurance subsidy . The exponent (lam) is the positive root of ; the state price of the asset value falling from to a boundary is .
For an asset value , a liability structure is a pair : deposits and a nondeposit coupon . It determines:
A structure is feasible if , and , and strategic (IsStrategic) if it is feasible and maximizes over all feasible structures.
Assume the regularity assumption (4), read as with below. Let
Then for every there is exactly one strategic structure, and at it ,
The proposition gives the bank's leverage, the split between deposits and bonds, the credit spread and the insurance assessment rate as explicit functions of eight parameters. Its qualitative content is that at the optimum the bank's capital is exactly the regulatory minimum at the moment its shareholders choose to default, so the strategic structure leaves no extra capital to protect the deposit insurer. The paper's comparative statics in the capital requirement, the deposit profitability and the insurance subsidy (Propositions 5–7) and its comparison of banks with nonbank firms (Proposition 4) are read off these closed forms.
The paper's proofs are in an Online Appendix that is not part of the source artifact. The result is proved on paper but has no machine-checked proof; this mission asks for one, including the global optimality and uniqueness that the paper asserts as a "complete characterization". The model's closed forms were checked numerically before formalization: maximizing reproduces the paper's Table 2 and the closed forms (5)–(7) at random parameter vectors satisfying (4).
is not concave and not smooth: it has kinks where (the maximum in ) and where (the positive part in ), and the fair rate blows up as . A first-order condition in the region alone does not find the optimum, which sits on the kink , and global optimality over the whole two-dimensional feasible set has to be argued separately. The regularity assumption (4) cannot be dropped: for , , , , , , the assumption fails and the maximizer of has a deposit ratio of about , not the of (6).
The model is stated at the closed-form state-price level: the state price is the explicit expression (Real.rpow), not an expectation under a geometric Brownian motion. The total bank value is taken from the paper's displayed pricing equations (15)–(17) of §4.1 with no restructuring, which match the §2 description; the paper's own closed form of is in the Online Appendix. As in (2), is evaluated at even when . Assumption (4), which the paper writes for the structure-dependent rate , is read as the parameter condition ; required at every feasible it would be unsatisfiable. The insurance subsidy ranges over Table 1's (the running text says ). The point is excluded from the feasible set because (2) is undefined there. All ratios are stated for an arbitrary , not normalized.
The strategic structure is defined as a maximizer of , never by the closed forms (6); the goal asserts existence and uniqueness, so it cannot hold vacuously. The credit spread is , and the goal does not assume .
The definitions use Mathlib's real powers, square root and max only. Proofs of the milestones, and lemmas on the shape of in the regions and , are welcome.
Since Naor's 1969 model of queue joining, the literature on pricing congestible services has assumed that a customer judges a time-consuming service by its full price: the money price plus a constant multiple of the time commitment , . Revenue-maximizing and welfare-maximizing prices for queues, priority schemes and capacity choices (Afèche and Mendelson 2004; Allon and Federgruen 2007; Nazerzadeh and Randhawa 2018; Gurvich et al. 2019) are all derived under this assumption, usually with identified with a customer type such as a wage. Allon and Federgruen describe it as "tantamount to assuming that all consumers assign a specific cost value to their waiting time and that the cost of waiting is simply proportional to the total waiting time."
Li, Lariviere and Bassamboo ask when this assumption is actually implied by a consumer's own optimization. They embed the purchase decision in a Becker (1965) style allocation of time and money, and show that the full-price model is exact for consumers who choose freely how long to work at a constant wage (gig workers), while it fails for shift workers. The result gives the full-price model a microfoundation and identifies the waiting cost with the wage .
A consumer has units of time per day. She chooses a plan : leisure time , leisure consumption , work time and overhead expenditure , and a purchase decision for a discrete service with value , price and time commitment . Her problem (PC) is
Here (StandingAssumptions) is continuous, non-decreasing and concave in each argument on the closed quadrant with ; , the time spent on chores when is spent to reduce them, is decreasing and strictly convex; is the compensation function. For gig workers it is linear, (linearCompensation), with wage .
A pair is feasible (IsFeasiblePair) when the buyer's problem () has a feasible plan (IsFeasiblePlan). The buyer's leisure utility (buyerUtility) is the supremum of over the buyer's feasible plans. The consumer is a full-price decision-maker (Definition 1, IsFullPriceDecisionMaker) if there is with whenever is feasible and . An optimal plan (IsOptimalPlan) of the buyer (, ) or the non-buyer (, ) maximizes over the feasible plans of that problem. The marginal rate of substitution of time for money (mrs) is
For and :
Part 1 (buyer) and part 2 (non-buyer): at an optimal plan where is differentiable with , both constraints bind; if moreover and , then at the paper's point ; and whenever and is differentiable there.
The proposition says that, for gig workers, the purchase decision depends on only through : the iso-utility curves in the plane are parallel lines of slope . This is exactly the structure that the queueing-pricing literature assumes, with waiting cost per unit of time equal to the wage (Remark 1 of the paper recovers the standard model from it). The paper's later results (Lemma 2, Proposition 2, §4) show that shift workers are not full-price decision-makers and that pricing them as if they were loses revenue; Proposition 1 is the benchmark those comparisons are measured against.
The result is proved in the paper, not formalized anywhere. The mission adds a machine-checked version of the model and of the proposition, with a corrected first-order clause: the paper states at every optimum, but at corner optima ( or ) it is false, and also needs . The formal statement carries exactly these interiority hypotheses, each only on the equation that needs it.
The full-price part is an exact change of variables, but the obvious one fails: substituting from the time constraint gives a set that seems to depend on and separately, and the sign constraint must be shown never to bind for non-negative prices (with negative prices it does bind, and the property fails). The supremum has to be compared as a supremum: attainment is not available, since is not assumed continuous.
The first-order part requires care that the paper skips. An optimum of (PC) is a maximizer of a constrained problem, not of the paper's reduced unconstrained function; one must first show that both constraints bind at an interior optimum where , then perturb along feasible curves on which the reduced objective is differentiable, which uses only differentiability of at one point and of at one point.
All quantities are real numbers. is a function on with all assumptions imposed on the closed quadrant; "concave in both arguments" is read as concave in each argument separately (the weaker reading). The purchase decision is a real entering (PC) as and , with imposed where used. Feasibility of refers to the buyer's problem. is a supremum in EReal, so infeasible pairs give rather than a junk value. Prices and time commitments are non-negative throughout. An optimal plan is a maximizer of over all four variables with fixed; binding constraints are a conclusion, never part of the definition. is computed from the Fréchet derivative of , and every statement about it assumes differentiability and at the point, so neither fderiv's junk value nor division by zero can make a conclusion true.
A trivializing formalization would define or feasibility through the full price , or define an optimal plan as one satisfying the first-order conditions; neither is done here: is the supremum over plans satisfying the two constraints of (PC) literally.
A complete development needs elementary real analysis only: supremum manipulation in EReal, one-variable derivatives of compositions along curves, and the vanishing derivative at a local maximum. The time-allocation model is new to the platform and is reusable for the paper's shift-pay results (Lemma 2, Proposition 2). Proofs of Lemma 4 and of Proposition 1 are welcome, as are formal versions of the paper's shift-pay results.
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.