Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Shareholder engagement with corporate management is a public good: when a change of policy raises firm value, every shareholder gains, but only the shareholders who engage pay the cost. Since Grossman and Hart (1980) this free-rider problem has been the standard explanation for why dispersed owners under-monitor management. In practice, however, engagement campaigns are increasingly run by wolf packs: several activist funds, each holding a small block, who engage together even though none could change policy alone.
Brav, Dasgupta and Mathews ask why such packs form when each member's stake is small and most of the capital they invest belongs to outside investors. Their answer is competition for flow. Fund investors observe who engaged and move their capital toward funds that revealed skill by engaging; the fees on that capital are a private, excludable reward for engagement. The paper shows that this flow motive can sustain collective engagement over parameter ranges where it fails both for funds that manage delegated money without flows and for funds that invest only their own money.
A firm has a unit continuum of shares. There are skilled and unskilled activist funds; each holds one block of size and cash , and . A block consists of a fraction of the fund's own capital and of delegated capital, on which the fund earns a fee . The difficulty of changing policy lies in with and is public. Only skilled funds can engage, each at cost . If funds engage, engagement succeeds iff ; the firm is then worth , otherwise . Write and let be the least natural number with .
A skilled fund's payoff is , where is its reinvestment return, its proprietary fraction and the value of the delegated capital it holds at the end. Three games differ only in and :
The fee value of an engager's capital when exactly funds engage and succeed is (Definition 5)
For each the skilled funds play a finite simultaneous game, the -subgame. A maximal success equilibrium (Definition 1) picks, for every , a Nash equilibrium of the -subgame whose probability of successful engagement is maximal among all its Nash equilibria, mixed ones included.
With , for every :
the first range is always non-empty, and the second is non-empty for some when . "Succeeds" means that every maximal success equilibrium of the flow game succeeds with probability one at (and one exists); "cannot" means every Nash equilibrium of the comparison game's -subgame has success probability zero.
Propositions 2 and 3 formalize the classical underprovision result and its aggravation by delegation: since , a fund that manages other people's money has weaker incentives to bear private engagement costs. Proposition 7 shows that flows reverse this ranking, and that the reversal against the proprietary benchmark is driven by the number of funds: the larger , the more capital an engager can attract. This is the paper's explanation of why wolf packs of small funds can be more effective than a single large owner, and it underlies the paper's comparative statics in activist capital.
The results are proved in the paper (Management Science, 2022); none of them has been formalized. The mission produces a machine-checked model of threshold engagement games with three payoff regimes on top of a published finite-game vocabulary, and machine-checked proofs that also cover mixed equilibria, which the paper treats in a short argument. Two hypotheses missing from the printed Proposition 7 (, ) and one endpoint in Lemma 2 are made explicit.
Each pure-profile check is a comparison of two numbers, but three steps need care. First, the cost intervals of Lemma 2 must cover the whole half-line ; this uses that is strictly decreasing and the endpoint , which the printed lemma excludes. Second, "no engagement" above the thresholds must hold for every mixed equilibrium, so the argument has to work with expected payoffs over all pure profiles rather than with one pivotal fund. Third, a maximal success equilibrium is a family indexed by , and maximality compares it against every mixed equilibrium of each subgame. The naive reading of Proposition 7 as three interval inequalities misses all of the game theory and is not the target.
The model is one definitions file, WolfPack.FlowEngage.Model, built on the published agt_games vocabulary (AGT.IsPureNash, AGT.IsMixedNash, AGT.profileProb). Players are Fin N (the skilled funds; unskilled funds never act and enter only through in the reallocation). Actions are Bool, with true = engage. Mixed profiles are weight functions; the success probability sums over the pure profiles. is sInf over ; casts to before subtracting. The proprietary game is the model with the proprietary fraction set to , all else unchanged (p. 15, footnote 14).
Conventions and additions, all disclosed in the items:
A formalization in which "success is impossible" quantified only over pure equilibria, in which the comparison game was allowed to choose its own no-engagement equilibrium, or in which "every maximal success equilibrium" ranged over an empty set would be trivial; the goal quantifies over all mixed equilibria of the comparison games and asserts existence of a maximal success equilibrium. Not formalized: Proposition 1 (social optimum), Lemma 1, Corollaries 1–3, Propositions 5, 6, 8, the asymmetric-information extension of Appendix B, and the case . Proofs of any milestone are welcome, as are general lemmas on mixed equilibria of binary-action symmetric games.
Many service systems match heterogeneous customers to heterogeneous resources: jobs to machines in a data centre, patients to beds, orders to couriers, donors to recipients. A recurring question is whether such a system, run first-come-first-served among compatible pairs, has a stationary distribution that can be written down. Two lines of work answered it for special structures: the order-independent queue of Krzesinski (2011, cited as [20] in the paper), where the service rate of the population does not depend on the order of customers, and the multi-type job and server model of Visschers, Adan and Weiss (2012, [22]), where customers are matched to compatible servers under an assignment rule. Redundancy systems with cancel-on-completion fit the first framework and those with cancel-on-start the second (arXiv:1902.02137v1, p. 3); matching models fit the second.
Ayesta, Bodas, Dorsman and Verloop (arXiv:1902.02137v1, later published in Operations Research, 2022) introduce the token-based central queue, which contains both. Their Theorem 1 states that, under an assignment condition and an order-independent condition, the stationary distribution has a product form. The paper's performance results (generating functions of queue lengths, Laplace transforms of waiting and sojourn times) and its applications (heterogeneous M/M/K, multi-server job models, redundancy, matching) are derived from it.
There is a finite set of customer types and a finite set of tokens. Type- customers arrive in a Poisson process of rate ; . A type- customer can hold only tokens from its compatibility set and is served only while it holds one. An arrival that finds a compatible free token claims one, chosen by a randomised assignment rule; otherwise it waits at the end of a central queue as an inactive customer. When a customer leaves, its token passes to the longest-waiting compatible inactive customer, or becomes free if there is none.
The state lists the tokens held by the active customers in order of arrival and the number of inactive customers that arrived between the holders of and ; is the empty state and . With , write , and let be the rate at which arrivals claim token when is the set of busy tokens.
The holder of leaves at rate with and for ; let , so .
With and , if the series below converges, then
is a probability distribution that satisfies the global balance equations of the queue's transition rates .
The paper's proof runs through the identities below, listed in attack order: (1), the departure-rate identities (4), (5), (7), the total exit rate , the explicit form (8)–(9) of the global balance equations, the partial balance equations (12), (13), (14) with the rearrangement of and the telescoping identity (29) from Appendix A, and (9) for the product form.
The product form gives the stationary law of a multi-class, multi-server system with compatibility constraints, with a normalising constant expressed as an infinite series. The paper derives from it the joint generating function of the numbers of waiting customers per type (Theorem 2), the numbers in system (Theorem 4), and the transforms of time-till-token and sojourn time (Theorems 6, 7), and shows that the heterogeneous M/M/K queue, redundancy with cancel-on-start or cancel-on-completion and a family of matching models are special cases.
The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formal proof would check the bookkeeping of the transition structure, where the printed text has slips (below), and would give a reusable development of product-form verification by partial balance for queues with order-dependent descriptors.
The algebra of the partial balance equations is long but routine once the predecessors of a state are listed correctly. The difficulty is that list. A departure frees a token that passes to the first compatible waiting customer, so the predecessors of a state are indexed by where the departing customer stood, how the waiting customers were split around it, and whether the token was released or reclaimed. The paper's printed list of reclaiming predecessors, , is stated for and , while the balance equations sum over . The obvious reading of the printed tuple at counts customers twice. A second slip sits in Appendix A, in the rearrangement of . A proof that copies the paper's backward formulas into the balance equations proves the wrong identity: the goal is balance for the forward transition rates, from which the predecessor list has to be derived.
Fintypes with decidable equality (finitely many tokens, as in Theorem 1). A state is a list of (token, count) pairs with distinct tokens. Infeasible descriptors (a waiting customer that could have claimed a free token) are included; the weights vanish on them.transitions lists the forward transitions of §4.1 with their rates, and rate y x is the total rate from y to x. The reclaim probabilities use for a customer waiting behind . The departure rates are defined by (3), with taking the prefix .FullBalance. Proofs of any milestone are welcome, and so are general lemmas on partial balance for lists of transitions.An entrepreneur developing a venture repeatedly chooses between strategies that differ in speed, risk and cost: a safe, slow approach or a fast, risky one. Wang and Zenios model this as a drift–variance diffusion control problem (SSRN 3667132; published in Operations Research, 2021, doi:10.1287/opre.2021.2171): the controller chooses not only the drift of a Brownian state but also its variance, and pays a running cost for each choice. Earlier models in which a decision maker switches controls as a diffusion evolves, Radner and Shepp (1996) on corporate risk choice and Harrison and Sunar (2015) on multiple modes of learning, describe their optimal policies through numerical procedures; here the controller chooses drift and variance together, the trade-off between moving fast and moving reliably is the object of study, and the optimal policy is in closed form.
The paper's motivating example (p. 10) suggests that the optimal policy might be complicated: use the safe control near to avoid failure, the cheaper risky control in the middle, and the safe control again near to secure the reward. The paper's main result says this never happens.
There are two controls . Control gives drift , volatility (variance ) and costs per unit time. The state follows
on , , and stops on hitting (no payment) or (terminal cost , i.e. a reward ). The entrepreneur minimizes the expected total cost.
Write for the effective drift, for the critical cost (the cost at which control alone breaks even with no noise), and . As in the paper (p. 12), throughout.
A -interval policy (Definition 1) cuts at and uses control on , with . Its value is the function that is continuously differentiable on , satisfies , , and on each piece solves
A policy is optimal if its value lies below the value of every interval policy on .
With :
In words: an optimal policy either uses one control throughout or switches exactly once, and away from the critical point no optimal policy switches more than once.
The result reduces an infinite-dimensional control problem to a two-parameter family of candidates (which control first, and where to switch), and Theorem 2 identifies the optimum explicitly. Downstream, the paper reads managerial conclusions off the region picture: when both controls are inefficient, when to begin with the safe control and when with the risky one (§4, §8).
The theorem is proved in the paper; nothing here is open. No machine-checked version of any part of it is known. The mission produces a checked version of the analytic core: the closed-form value functions, the sign analysis of the switching functions, a one-dimensional comparison principle (the analytic content of the verification lemma), and the correction of the uniqueness half of Theorem 1 at the critical cost point.
The existence half is a long chain of explicit but delicate calculus. The slopes involve terms whose ordering (Lemma 1) is not visible from the formulas, and the switching point of the two-interval policy is the root of a function built from the derivatives of a piecewise exponential solution whose coefficients are ratios of exponential sums. Showing that keep their signs away from requires the sign facts of Lemma 22 in exactly the right region.
The uniqueness half looks immediate (two optimal policies have the same value, which cannot solve two different ODEs on an interval) but is false as printed: at the affine function solves both ODEs, and every interval policy is optimal. The correct statement must exclude that point, and its proof must show that, elsewhere, the optimal value is affine on no interval.
Mathlib has Brownian motion but no stochastic integral or Itô formula, so the problem is stated analytically, in the objects the paper's proofs manipulate. A policy's value is the unique solution of its ODE boundary-value system with pasting; the identity with the expected cost (Dynkin's formula, the second half of Lemma 12) is not formalized, and optimality is over interval policies, to which the paper restricts (p. 8). Conventions: , , , minimization; is the volatility and enters the ODE; is an explicit hypothesis; controls are a two-constructor type, policies are structures carrying , the controls, strictly increasing breakpoints from to and distinct adjacent controls.
Corrections relative to the page: Theorem 1's uniqueness half excludes ; Lemma 22 (204) is stated strictly; Lemmas 9–10 carry the hypotheses of condition (9) that their proofs use; the exclusivity claim of p. 13 is dropped (only exhaustiveness is stated); (73)'s in the control-2 equation is read as .
The encoding cannot be trivialized: the value fixes both boundary values and gluing, so no policy has arbitrarily low "values"; optimality quantifies over policies of every length and all their values at every point of ; and the policy structure forbids empty pieces and repeated adjacent controls, so is the true number of intervals.
Needed infrastructure: elementary real analysis (exponential inequalities, derivatives of explicit functions, the intermediate value theorem), a one-dimensional maximum principle for with piecewise-constant coefficients, and linear independence of . The comparison principle and the interval-policy layer are reusable for other one-dimensional switching problems. Proofs of any milestone are welcome, as is a formal Dynkin link once Mathlib has stochastic integration.
Service systems such as outpatient clinics, surgical suites and diagnostic units book requests one at a time. When a patient calls, the scheduler commits at once to a provider and a day, without knowing who will call next. Each provider has a planned working time per day, which can be stretched by overtime at a cost. Keyvanshokooh, Shi and Van Oyen (MSOM 2019; accepted manuscript SSRN 3352166) study this problem when the arrivals are adversarial, and analyse it by competitive analysis: an online policy is judged by the worst case, over all arrival sequences, of the ratio between its value and the value of an offline planner who knows the whole sequence.
The paper sits in the line of online primal-dual algorithms for packing problems: online b-matching (Kalyanasundaram and Pruhs 2000), AdWords (Mehta, Saberi, Vazirani and Vazirani 2005), ad auctions with budgets (Buchbinder, Jain and Naor 2007) and the general framework of Buchbinder and Naor 2009. In all of these, capacity is a hard limit. Overtime turns capacity into a soft limit with a price, and the algorithm must decide when to start paying it.
There are servers , days and customers , numbered in order of arrival. Server on day has a regular capacity and an overtime budget , and server pays per unit of overtime. Customer needs service time and brings reward at server , normalized so that .
The offline problem (P) chooses and overtime to maximize subject to: each customer is served at most once; ; and . Its optimal value is . The dual (D) of the LP relaxation minimizes subject to , and .
The instance parameters are
together with and .
HOOP-BOT (Algorithm 1) keeps prices (regular capacity, initially ) and (overtime, initially ). Customer is offered the server-date maximizing and is rejected if that value is negative. If it is accepted at , then:
The output may exceed capacity by one customer per threshold. The paper converts it into a feasible solution of value .
With , where
for every instance and every tie-break,
Theorem 1 is the paper's headline result: a worst-case guarantee for online scheduling in which capacity can be expanded at a price. In the proportional case and as , the paper reads it as a ratio of at least , to be compared with the upper bound of its Theorem 2. The guarantee underlies the rolling-horizon policy of §5 and the case study of §6.
The formal statements add three things. They fix the hypotheses: the page leaves , and the choice of implicit. They pin the conversion from almost-feasible to feasible solution, which the paper describes only inside a proof. And they settle the truth of the result. No part of this paper has been formalized before. The technical inequality is shared with the Buchbinder–Jain–Naor mission and is referenced from there.
The obvious argument is the usual primal-dual accounting: bound the dual increase by times the primal increase at every iteration, sum, and lose a factor when the at most two overflowing customers per server-date are dropped. The step that needs care is the first overtime iteration of a server-date. There the regular price has been capped at while the overtime price still has its initial value , so the identity that the per-iteration bound relies on is not yet in force. The initial dual value is also not a sum of per-iteration increments. Any proof of the goal has to deal with both points.
Everything is in ℝ. Indices are Fin n, Fin T and Fin m, with customers in arrival order; and are written customer first. The maxima in (1) are suprema over nonempty finite index sets. Algorithm 1 is defined step by step, exactly as printed (Steps 1–13, initially, the tests , and as printed). Its run is the fold of one step over the customers. The argmax tie-break is a parameter, and statements about the run hold for every selector that returns a maximizer.
Standing assumptions: ; ; ; ; ; (the paper's normalization); and . The page does not state the last one, but divides by , which vanishes at . depends on the whole instance, as it does in the paper.
"Admits competitive ratio " is formalized through Definition 1 and Proposition 4. There is a feasible of (P) with and , differing from in at most two customers per server-date, whose value is at least times the optimal value of (P), taken as the greatest objective value of a feasible solution. A statement about a closed-form allocation, a fixed tie-break or an initialization other than would be a different theorem and is excluded. The goal is posed exactly as printed, and the proposers record a counterexample to it. Lemma 1 and (15) are stated for the Rule (I) recursion along the customers allocated to one server-date, abstracted from the run.
Not formalized: the limit (12); Theorem 2 and Lemma 3 (the upper bound); Proposition 1, which fails as printed at the first overtime iteration; Propositions 3 and 5; and the case study. Welcome contributions include proofs of the milestones and reusable facts about multiplicative price updates.
Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to iterations earlier).
The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space . The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.
Let and be finite index sets and let , be real Hilbert spaces, with Hilbert direct sums and . For every and the data are:
The parallel sum of is . Write and . The primal problem (1.1) asks for with
Its set of solutions is . The dual problem (1.2) asks for such that some satisfies and ; its set of solutions is . The Kuhn–Tucker set (2.13) collects the pairs satisfying the first condition at and .
On the saddle operator (2.11) maps to the product of the sets , , and . It splits as (Definition 2.4), where collects the cocoercive operators.
Algorithm 3.4 runs, at iteration , over activated blocks , . For it computes a resolvent step from the delayed iterate ; for it computes , from resolvents of , at the delayed iterate . Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing , measured by a number that involves . If , it moves toward that half-space with relaxation ; otherwise the iterate stays put.
Under Assumptions 3.1–3.3 (step-size ranges tied to , and by (3.1); every block activated at least once in every consecutive iterations; delays at most ), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies
together with the analogous statements for and . There exist and with such that
In attack order:
Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of , and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with and .
The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.
The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward in . That approach fails: for the general Problem 1.1, no half-space separating the current point from can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets in the larger space . The link back to , and is Proposition 2.2.
The second difficulty is asynchrony. The half-space at iteration is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of , one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).
PiLp 2 over finite index types, and is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.Most technology startups that exit successfully are acquired by incumbents rather than taken public. A founder therefore faces a timing question: sell early, while the company is still an invention that only a few incumbents can evaluate, or wait until the invention has been developed into an innovation that every potential buyer can value, at the risk of failing before that point. Arora, Fosfuri and Rønde (SSRN 3611808, forthcoming in Management Science, 2020) model this choice as a contest between three exit strategies: commit to an early sale, commit to a late sale, or keep both options open. The paper's first main result, Proposition 1, describes which startups choose which strategy as a function of their execution capability and of the cost of seeking early offers.
The question matters to entrepreneurship and innovation economics because the answer is not monotone: the paper finds that keeping options open is chosen by startups of intermediate capability, while both weak and strong startups prefer to commit. Commitment to an early exit can be valuable even when flexibility costs nothing, because flexibility changes how early buyers bid.
A startup has execution capability , its probability of surviving to the late market on its own. It holds resources . Trying the early market costs ; the remaining is spent developing the invention, which realizes the fraction of the late-market value, where is strictly increasing and continuous on with and .
There are buyers in the early market and in the late market, with . Buyer values the startup at : a common component and an idiosyncratic component drawn independently from the uniform law on , with distribution function . Each market is a sealed-bid second-price auction. With bidders, let and be the expected highest and second-highest idiosyncratic draws, computed from the order-statistic distribution functions and and their densities and . A buyer then expects and the seller .
The three exit strategies pay:
The startup's choice maximizes the three profits; on ties it prefers the less time-consuming strategy, so early before late before flexible. Let be the type at which ; it equals .
There exist costs such that
All thresholds except are existential, as on the page, so the goal does not depend on any computed constant.
The milestones follow the paper's own proof, Online Appendix A2:
Proposition 1 is the paper's characterization of exit timing. It explains why some founders publicly commit to an early sale, and it is the input to the paper's welfare analysis (§4), which compares the equilibrium timing with the efficient one in the two polar cases (iii) and (i). Without it, the comparative statics of Proposition 2 and the inefficiency results of Propositions 3 and 4 have no equilibrium to refer to.
The paper proves Proposition 1 on paper only. This mission produces a machine-checked version of the model and its proof. That includes the order-statistic facts for uniform valuations, which are standard (Krishna, Auction Theory, 2010, Appendix C) but which have no closed-form statement on the platform. The appendix's argument relies on "calculations show" steps and on convexity claims stated without proof; checking them in Lean is the main work beyond the paper. The platform holds no formalization of this model or of startup exit timing.
The obvious argument compares three explicit profit functions, but is not explicit: its lower integration limit moves with and has a kink where it leaves . The shape of (flat, then strictly decreasing, then strictly increasing) depends on the sign of an inequality between the ratio evaluated at the moving cutoff and a linear function of , and the paper settles this inequality at by an unstated calculation valid for every and . The comparison at holds uniformly in , and the slope comparison must hold across the kink. Finally, the cost thresholds are defined implicitly, and their order follows only by combining the single crossing in with the monotonicity of .
A tempting shortcut is to define the choice through the thresholds; that would make the goal true by definition and is ruled out (see below).
All quantities are real numbers; are natural numbers with , so the paper's branches are not formalized. ranges over (the paper's ) and over . The standing assumptions are bundled in one predicate. Three choices differ from the printed page and are disclosed in each item:
The tie rule early ≻ late ≻ flexible is the page's "least time consuming" convention.
are Lemma 1's closed forms, linked to the actual order statistics of a product of uniform laws by the theorem lemma_1. and are integrals, so Lemma 3 is a theorem rather than a definition. is eq. (2) with Lemma 4's cutoff; Lemma 4 itself, the early-market bidding equilibrium, is not formalized. The choice is defined from only, never from , or , so the goal cannot hold by unfolding a definition. Proposition 2, Lemma 6, Propositions 3–4 and the Online Appendix extensions A4–A6 are outside this mission.
Contributions are welcome at every level. Particularly reusable are:
Inventory integration (or pooling) serves several markets from one stock instead of one stock per market. Its classical value is statistical: when demands are not perfectly correlated, the pooled demand is relatively less variable, so less safety stock is needed for the same service level. Eppen (Management Science, 1979) quantified this for normal demand, and it is the starting point of the risk-pooling literature.
Retailers who mark down unsold stock face a second effect. Strategic consumers who expect a clearance sale may delay their purchase, and whether they wait depends on how likely they believe a unit will still be available at the low price. Integration changes that availability and therefore changes consumer behavior. Aflaki and Swinney (SSRN 2842182, 2020; Operations Research 69(4), 2021) model this interaction as a rational-expectations game between a firm and its consumers, in the line of Su and Zhang (Management Science, 2008) and Cachon and Swinney (Management Science, 2009). They split the value of integration into an operational part and a behavioral part, and characterize when the behavioral part is positive.
A firm sells one product over two periods: at full price in period 1 and at clearance price in period 2. It orders units at cost before the season, with . Market demand is normal. In the multichannel system each of two identical markets has demand and its own stock. In the integrated system one stock serves , where is the correlation.
Consumers have valuations with density on , distribution and . A unit bought in period 2 is worth , with and , and . Consumers believe a unit is available in period 2 with probability . They buy in period 1 exactly when , where
Given the belief about this threshold, the firm faces period-1 demand and solves a newsvendor problem. Its optimal profit is , with
where and .
The second-period fill rate is expected period-2 sales divided by expected period-2 demand. Period-2 demand is , and period-2 sales are the smaller of that demand and the leftover stock .
An equilibrium (Definition 1) is a triple in which maximizes profit given , , and . Write and for the equilibrium thresholds of the two systems. The behavioral value of integration is the second term of the paper's decomposition (6):
Let , the value of at which changes sign.
The goal asserts only the shape of the answer: the set where the behavioral value is positive is an initial segment, in correlation and in variability. It fixes no formula for the thresholds.
Propositions 1–3 cover consumer thresholds, the newsvendor best response, and existence and uniqueness of the equilibrium with . Equations (8) and (14) give the fixed-point form of the equilibrium fill rate. Three further milestones are the reduction to the coefficient of variation, the deterministic endpoint (, ), and Lemma 1, continuity of a unique fixed point. The last ones are Proposition 5 (i), quasiconcavity of and in and in , and the sign rule that when and when .
The result says when pooling helps through consumer behavior: when markets are not too positively correlated and not too variable. Above either threshold, integration encourages strategic waiting enough to reduce the total value of pooling below its classical operational value. A firm that ignored this effect would overrate integration in highly correlated or highly variable markets.
The formalization adds two things. It makes the equilibrium of a rational-expectations inventory game a checked object. It also records gaps in the printed statements. First, part (iii) and the sign rule on p. 13 need : for the sign of flips the sign of . Second, footnote 4 needs . Third, under the paper's ratio fill rate with normal demand, the equilibrium fill rate can be negative, which affects (8) and (14). The result is proved on paper. To the best of current knowledge, nothing in it has been formalized.
The equilibrium is an implicit fixed point. The fill rate is the solution of (14), in which the demand ratio depends on the fill rate itself, through the threshold valuation. Comparing with means comparing the fixed points of two different equations, one per system.
A direct approach would show that is monotone in or . That fails, because the equilibrium fill rate rises and then falls in variability. Only quasiconcavity holds, and the threshold structure must come from combining quasiconcavity with the behavior at the endpoints, where demand is deterministic. Quasiconcavity of an implicitly defined fixed point needs a second-order argument on (14), which involves Gaussian integrals with variable limits.
Everything is real-valued. The multichannel system is formalized as one market , taken once, since the two markets are identical and the equilibrium is symmetric (Proposition 3). The integrated system is the market given by the law , as in Proposition 2 (ii), not as a bivariate sum. The demand law with standard deviation is the Dirac mass, which is how the deterministic endpoint is stated.
The valuation density is integrable, has total mass one, vanishes off and assigns positive probability to every nonempty interior subinterval. Three conventions and additions are disclosed:
The goal is stated about equilibria of Definition 1 and about the behavioral value. It is not stated about (14), an abstract function of the coefficient of variation, or the sign of . The thresholds range over and , so the uniqueness claim cannot be met by an unconstrained threshold.
A complete development needs Gaussian integrals of piecewise-linear functions, the newsvendor solution for normal demand, fixed-point arguments for monotone maps, and implicit differentiation of parametric integrals. The normal newsvendor and the loss-function identity are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 5 (i) that avoid differentiability assumptions on .
Many planning problems ask for a decision that varies over a time horizon and must satisfy a constraint at every instant, possibly with cumulative effects of past decisions. The applications in the source paper are a maximum-flow problem with time-varying pipeline capacities, a wireless coverage problem for a moving target region, and the approximation of Pareto curves of bi-objective semidefinite programs. Ahmadi and El Khadir (arXiv:1808.03994, Mathematics of Operations Research, 2021) model these as time-varying semidefinite programs (TV-SDPs), a common generalization of semidefinite programming and of the continuous linear programs of Bellman (1953), Tyndall (1965) and Levinson (1966), which are the case of diagonal matrices.
A TV-SDP is an infinite-dimensional problem: its variable is a function. The paper's main message is that, under a strict feasibility assumption, nothing is lost by searching only over polynomial solutions, and that the best polynomial solution of a fixed degree can be computed by an ordinary SDP through sum-of-squares certificates. The first statement, Theorem 4, is what justifies the second as a convergent approximation scheme, and it is the goal of this mission.
Fix integers . Let be the set of measurable functions that are bounded, . The data are polynomial: an objective of univariate polynomials, symmetric matrices with polynomial entries, and symmetric kernels with entries polynomial in . For define the matrix function
A function is feasible if and for almost every . The TV-SDP is
It is strictly feasible if some and satisfy for almost every . A polynomial solution is for polynomials .
The proof uses the mollifying operators , : with the bump for , otherwise, normalized so that ,
applied entrywise to vector- and matrix-valued functions. In Lean these are Ln, Sm, Data, F, Feasible, StrictlyFeasible, obj, opt, polySol, J, cJ, Mv, MvVec and MvMat in the namespace TVSDP.PolyOpt.
If the TV-SDP is strictly feasible, there are polynomial vectors such that every is feasible and
the limit taken in the extended reals, so is included.
The result. Theorem 4 says that the supremum of a strictly feasible TV-SDP over polynomial solutions equals its supremum over all bounded measurable solutions. Combined with the paper's Theorem 6, which computes the best degree- polynomial solution by an SDP, it shows that these SDP values form a nondecreasing sequence of lower bounds converging to . Without it, the polynomial restriction could have a strictly smaller value; Example 1 of the paper shows that this happens when strict feasibility fails, where the unique feasible solution is a step function.
Formalizing it. The result is proved in the paper, not formalized anywhere. A machine-checked proof also has to repair the printed argument: the operator integrates over only and is not normalized near the endpoints ( for ), so three auxiliary statements of §3.1 are false as printed (see Formalization scope), although Theorem 4 itself is true. Any complete proof therefore needs an argument that handles the endpoints, which the formal development would record.
The natural route is "perturb into the strict interior, smooth, approximate by polynomials", and each step preserves feasibility only up to a uniform error, so the margin must survive all three. The difficulty is uniformity on the closed interval: smoothing commutes with only approximately, the Volterra term couples times, and at and the mollifier of Definition 3 loses half its mass. Applying the printed Corollary 1 directly fails at the endpoints. In Lean, a further cost is the bookkeeping between "almost every " for feasibility and "every " for the smoothed and polynomial solutions.
Conventions committed to:
volume.restrict (Set.Icc 0 1)), never Lebesgue measure on .EReal supremum; the matrix inequality is positive semidefiniteness of .Trivializations ruled out: feasibility is a.e. on only, solutions in are bounded, is not a real sSup (which would be on an unbounded set), and polynomial solutions are genuine polynomials evaluated everywhere, not functions that agree with a polynomial almost everywhere.
Deliberately absent: the third sentence of Proposition 1 (uniform convergence for continuous ), Lemma 3(c) and Corollary 1. All three are false for the operator of Definition 3 because of the endpoint effect; for example, Corollary 1 fails for , at . The printed constant on p. 14 has in place of , and with it the Lipschitz display fails; milestone 6 uses the corrected constant. Measurability of is added in Lemma 3(a), where the paper uses it implicitly.
Infrastructure needed: interval mollification of bounded measurable functions, uniform convergence on , the Weierstrass approximation theorem for -valued functions (in Mathlib), and Loewner-order perturbation bounds. The mollifier and the Loewner perturbation lemma are reusable beyond this mission. Contributions of proofs for any milestone, of the missing endpoint-robust smoothing step, and of the paper's Example 1 are welcome.
A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).
The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.
A flexibility design is a set of arcs from plant to product . Plant has capacity , product has demand and margin , and units of product are made by plant . The maximum profit is the optimum of the finite linear program
Products fall into categories with margins . Write for the products with margin and for their total demand. A deterministic score in the paper's class has the form , with strictly increasing in its profit argument when category totals are fixed. Its robust score is for an uncertainty set of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).
A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to for a fixed centre . Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).
In the target system there are plants and products, , with unit plant capacities and exactly products in each of two margin classes . A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric , and every robust score in the class above,
This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).
The paper defines a dual margin group index by an integer program that assigns product dual values from the finite menu , where . The parameter counts how many products in each category receive each nonzero menu value. Its feasible set is . Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.
Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).
The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.
The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector (Wang, Wang and Zhang 2020, Appendix A).
The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category is the paper's category , and the added margin level is zero. The production variable is written x j i in Lean for the paper's . Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.
The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts to . These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The case is included.
Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.
A customer who is short of time may pay for a better place in a service queue. Unlike resale of a fixed ticket, this transaction changes the waits faced by later customers, and those customers' choices then change the value of the position being sold. Yang, Wang, and Cui study this feedback in an unobservable queue with a firm that repeatedly sells its place to arriving customers. Their single-scalper analysis identifies demand levels at which such a firm enters, rather than assuming that more customer traffic always makes entry more attractive (Yang, Wang, and Cui 2021, §§3–4).
The mission targets a precise claim about that entry decision. Low demand leaves few sales; very high demand forces more customers to balk and limits what a buyer will pay. The result is a possibly empty interval of demand volumes in which the scalper enters. The associated price and revenue results are useful milestones because they describe the economics of that interval using the same customer equilibrium as the entry theorem (Yang, Wang, and Cui 2021, Propositions 2–4).
The service system is an M/M/1 queue: potential customers arrive as a Poisson process at rate , and a single server completes service at exponential rate . Customers cannot observe the queue length or their positions. Every customer values completed service at and has a private delay cost per unit time. In this mission, is uniform on and . A queue-scalping firm may place one scalper in line. Under the head-queueing rule, the scalper can hold the first position without blocking service while waiting to sell it to a customer. After a sale, the scalper returns to the tail. The firm pays cost per unit time for the scalper and charges a nonnegative price per sale (Yang, Wang, and Cui 2021, pp. 5–9, Lemma 1).
Customers use two cutoffs. Customers below join without buying, customers from through join and buy, and customers above balk. The actual throughput is ; the share of joining customers who buy is . A customer with delay cost is indifferent between buying and not buying. A customer at can join and buy, while the corresponding utility is zero if any customers balk. These are the customer-equilibrium equations (1b)–(1d) of the paper, with , , and stable throughput (Yang, Wang, and Cui 2021, pp. 7–9).
Let be a buyer's expected delay and a nonbuyer's expected delay under the head-queueing rule. Their difference is the buyer's delay saving. Optimal revenue is the attained maximum of over nonnegative prices and compatible customer equilibria. If the firm stays out, its profit is zero. If it enters, its best profit is . At equality the model takes the no-entry decision, as in the proof's entry criterion (Yang, Wang, and Cui 2021, equation (1a), Proposition 4 and its Online Appendix proof).
For fixed , , and , Proposition 4 asserts that thresholds exist such that every positive demand volume has an optimal customer-equilibrium revenue and
The interval can be empty. The thresholds depend on the system parameters, rather than on the demand volume being tested (Yang, Wang, and Cui 2021, Proposition 4, p. 12).
Proposition 2 gives the optimal price in the all-join regime and the balking regime , and says that this price is unimodal. Proposition 3 says that optimal revenue is also unimodal, with a unique peak . The Online Appendix identifies the cutoff , reduces the pricing problem to the buying cutoff , gives the revenue expression in each regime, and shows that revenue less cost approaches at both extreme demand levels (Yang, Wang, and Cui 2021, Propositions 2–3, Online Appendix pp. 1–3).
The entry theorem classifies queue demand by the scalper's decision while allowing the equilibrium buying and balking rates to change with price. It explains why a queue with more arrivals can become less attractive to a scalper even though it offers more potential buyers. The price and revenue milestones also distinguish two operational regimes: one in which everyone joins, and one in which joining itself contracts as demand rises (Yang, Wang, and Cui 2021, §§4.1 and 9).
The paper proves these results mathematically; this mission asks for machine-checked proofs of the statements under an explicit model interface. The reusable output includes formulas for the two customer delay classes, a predicate for cutoff-based customer equilibrium, and an attained joint optimization predicate. A formal proof of entry must connect the closed-form revenue analysis to that optimization predicate. At the draft stage, the proposed theorem statements compile with sorry; they are not yet machine-checked proofs.
More arrivals directly create more opportunities to sell a place, but customer behavior also changes the number who join, the fraction who buy, and the price they will pay. Holding any one of these responses fixed gives the wrong entry question. The challenging point is to establish a single rise and fall of optimal revenue across the boundary between the all-join and balking regimes, while keeping the customer equilibrium and the price optimization tied together. The endpoint behavior matters as well: an interval theorem needs no entry at sufficiently low and sufficiently high demand, including the possibility that the entry interval is empty (Yang, Wang, and Cui 2021, Propositions 2–4 and Online Appendix A).
Lean represents as real numbers and the entry decision as either zero or one. Params.Standing records , , and . Proposition 4 additionally assumes ; the Online Appendix uses the negative limit , and at zero cost the high-demand nonentry threshold need not be finite. Statements concerning demand use . The positive cutoff makes the purchase-rate quotient meaningful, and stable throughput keeps the queue-delay denominators positive.
The delay formulas of Lemma 1 are taken as the model's delays; their underlying stationary queueing-process derivation is outside this mission. The uniform CDF is the identity on . The paper's optimization is represented by an attained maximum over prices and customer equilibria, rather than by a supremum of arbitrary real values. The entry goal includes existence of an optimizer at every positive demand, so missing feasible equilibria cannot make the result vacuous. Contributions that establish equilibrium cutoff uniqueness, exact reduction of the pricing problem, price and revenue optimality, and the resulting demand shape are all within scope. The definitions of the equilibrium and optimum can be reused in further analysis of queue position sales under the same rule.
An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).
The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.
Let decision and true outcome . The protected class has two groups, with conventionally advantaged and disadvantaged. The proxy takes values in a measurable space ; it may be categorical, continuous, or mixed. The primary marginal is , and the auxiliary marginal is . Both share one proxy distribution , as required when they arise from a common population joint law.
For each proxy value , write and . Their decision marginal is . A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set contains all measurable conditional joint arrays that couple and at each , together with the fixed . It imposes no additional assumptions on the unknown association of class and outcomes.
The demographic disparity of a compatible joint is . Its partial identification set is
This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.
For a group , decision , and proxy value , define the Fréchet–Hoeffding weight endpoints
For a class weight function , let . The goal, Proposition 7, is the equality
Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).
The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.
Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.
The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome remains in the compatible-joint model even though demographic disparity uses only . When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.
The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on and measurable, normalized, nonnegative conditional vectors and . The set consists of measurable conditional couplings for every . Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of is computed from , not inserted from the auxiliary marginal.
The theorem explicitly assumes and , since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every selects a version and does not change the attainable disparities. On a cell with , weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.
The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.
Prices of staple vegetables in India, onions above all, rise sharply at irregular intervals. When they do, governments respond with cash transfers, subsidized sales and import programmes. A recurring explanation for these price spikes is artificial shortage: traders who control a large share of the stock withhold supply early in a season, and consumers who observe the scarcity raise the amount they are willing to spend on the commodity, so the traders sell more later at a higher price. Levi, Singhvi and Zheng (SSRN 3332493; Manufacturing & Service Operations Management) give a stylized model of this mechanism. It shows that a monopolist trader facing budget-adjusting consumers creates an artificial shortage. It then asks how three common government interventions change the shortage. This mission formalizes the paper's answer for the first intervention, a cash subsidy (CS) to the poorest consumers. The question matters for policy: the paper argues that a well-intended transfer can make the hoarding worse.
A unit mass of consumers have Period-1 budgets distributed uniformly on . A monopolist trader sells over two periods.
where is the budget adjustment factor.
Under a cash subsidy , the government gives cash to the fraction of consumers with the lowest budgets, within a budget . At price :
The game is solved by backward induction:
The set of equilibrium Period-1 quantities is . An element is written , and is the no-intervention quantity.
With , there is a threshold such that
and is non-increasing in for . The equilibrium set is also nonempty for every .
Proposition 3 is the paper's verdict on cash subsidies. A small budget is absorbed without effect on the trader's behaviour, because the trader's Period-2 revenue equals its no-intervention value. A moderate budget induces a larger Period-1 release and so mitigates the shortage. A budget above makes the trader withhold more than without intervention, because subsidized consumers can pay more in Period 2. The non-monotone dependence on is the basis of the paper's policy advice against "oversubsidizing" and of its comparison with supply-allocation schemes (Proposition 4, not in this mission).
The paper prints no proofs; they are "available from the authors upon request" (p. 10). The threshold and the online appendix (Lemma O.1) are not in the published text. A machine-checked development would therefore be the first complete public proof of these statements. It would also settle Theorem 2(iv), whose printed form is false on a band of budgets and is posed here in corrected form. None of these results has a formal proof anywhere.
Every stage of the backward induction is a non-smooth optimization.
The tempting route is to differentiate the Period-1 objective and solve the first-order condition. It fails twice. It misses the jump at , where the global maximizer switches modes, and it misses the kink above , where the maximizer is not a stationary point.
All quantities are real numbers. The trader's Period-2 decision is a price with quantity equal to the explicit demand, which is equivalent to the paper's quantity form. Purchases at equality count as purchases, as in the text. The commitments are:
The goal is stated about itself. A version that substituted Theorem 2's closed forms or first-order roots for would assume the content of the theorem, and is ruled out.
The development needs the Period-2 best response of a piecewise-linear demand, the government's two-variable welfare problem (eq. (5) is a polynomial in the breakpoints), and a comparison of the two modes of the Period-1 objective. Lemmas on maximizers of piecewise-quadratic functions are reusable beyond this mission. Proofs of any milestone, and sanity lemmas on the tie-breaks, are welcome.
A seller whose customers influence one another faces a choice between two pricing policies. It can collect information about the social network and charge each customer a personalised price that reflects their position in it, or it can ignore the network and charge everyone one uniform price. Personalised pricing is never worse for the seller, but collecting network data is costly and raises privacy concerns. The question is how much profit the network information is worth.
For a fixed network the answer depends on its fine structure. Candogan, Bimpikis and Ozdaglar (Operations Research 2012) showed that with linear-quadratic utilities the optimal personalised prices are expressed through Bonacich centralities, so the gain from discrimination is a difference of discounted walk counts. Huang, Mani and Wang (SSRN 3368458; published in Management Science, 2021) study this gain, the value of price discrimination, in large random networks. Their main result for random networks, Theorem 5.1, says that in directed Erdős–Rényi networks the seller who prices uniformly loses only a vanishing fraction of the optimal profit, whatever the density of the network. This mission formalizes that theorem and the results its proof rests on.
There are consumers. The network is an matrix with non-negative entries, where is the influence of consumer on consumer . For a square matrix , is its spectral norm (the operator norm); is the all-ones vector, and is the total weight of walks of length in .
Consumer facing price chooses a consumption level to maximise
with a stand-alone utility and a network coefficient . The resulting consumption equilibrium is (eq. (1))
The seller has marginal cost and profit . The optimal profit is ; the optimal uniform price is . The regret and fractional regret of uniform pricing are
A directed Erdős–Rényi network is the random matrix whose off-diagonal entries are independent with , and whose diagonal is zero. denotes expectation over it. The constants are the same for every .
For every sequence of densities with values in ,
Both parts are stated. The goal fixes no rate and no density regime; the paper's Theorems 5.2–5.4 give exact rates in three regimes and are not part of this mission.
The paper calls the optimal uniform price "under the assumption that , according to [12]" (p. 7); milestone 2 states that optimality as part of eq. (4).
Theorem 5.1 says that in large random networks the network information has asymptotically no value to a monopolist: the uniform price does not depend on the network, yet earns a fraction of the optimal profit tending to one, for sparse, critical and dense networks alike. This separates the deterministic picture, where some networks have a large value of discrimination (Theorem 4.1 of the paper characterises those with none), from the typical random one. It supplies a benchmark against which network-based pricing, and the cost of collecting network data, can be judged.
The paper proves the theorem by hand. No part of it, and no part of the model, has been machine-checked; the platform has no network pricing model and no walk-count results for directed random graphs. A complete development would make the closed forms (3) and (4), the spectral inequalities and the Erdős–Rényi walk moments reusable. The printed proof of Theorem 5.1 bounds expectations of ratios by almost-sure statements and splits the density sequence into "maximal subsequences"; a formal proof must replace these steps by quantitative ones. The printed proof of Lemma 5.5 (i) relies on a per-walk claim that fails (a closed walk in can use four arcs of while it visits three ordered pairs), although the statement itself was checked by exhaustive enumeration for small ; that lemma needs a new argument.
The regret is a difference of two discounted walk series. Bound (29) controls it by walks of length two and the spectral norm, which suffices when the network is very sparse, but in dense networks, where and , it only gives . The dense case needs the cancellation between and for each up to a slowly growing cutoff (Lemma 5.5), together with a lower bound on the spectral norm that holds with high probability. In the critical regime , neither bound applies directly, and one needs that grows with in probability. The goal quantifies over all density sequences, so the argument must be uniform across these regimes; a proof for one regime does not suffice.
All objects live in the namespace NetPriceDisc.Random and are defined in one file. Networks are Matrix (Fin n) (Fin n) ℝ; the spectral norm is Mathlib's operator norm (Matrix.Norms.L2Operator). The consumption equilibrium is formula (1) for every price vector, with no non-negativity constraint on consumption, as in the paper's definition of . is defined as the supremum of over , and , from and ; the closed forms (3) and (4) are theorems, not definitions, so the goal cannot be discharged by unfolding formulas. Lean's convention gives the empty network no externality, hence zero regret, which is the paper's own reading of the empty network (p. 12); the empty network keeps its probability . The Erdős–Rényi expectation is the finite sum over arc sets of off-diagonal pairs with weight ; no measure theory is used. The fractional regret's expectation is the expectation of the ratio. "Any sequence of densities" is a function , with no further restriction.
Two printed statements are corrected and disclosed: Lemma 5.3 is stated for even (as printed it fails for odd ; for the star with , one gets ), and Lemma 5.5 (ii) for (at it involves the undefined ). Only the deterministic Rayleigh-quotient part of eq. (12) is stated.
Useful infrastructure includes Neumann series and Rayleigh-quotient bounds for symmetric non-negative matrices, walk moments of directed Erdős–Rényi graphs, and maximum-degree or spectral lower bounds in probability. Proofs of any milestone, and alternative routes to the goal that avoid Lemma 5.5, are welcome.
Probabilistic selling, also called opaque selling, offers a customer a product whose exact version is revealed only after purchase: a "mystery box", an unnamed hotel on a travel site, a flight whose carrier is announced after booking. The firm controls the price and the probability with which each version is delivered. The classical analyses (Fay and Xie 2008; Jerath, Netessine and Veeraraghavan 2010) assume customers know these probabilities and form rational expectations.
Huang and Yin (SSRN 3627927; Manufacturing & Service Operations Management, 2020) drop that assumption. Customers do not observe the offering probability; they infer it from a few anecdotes, which are reports of what earlier buyers received, in the spirit of the literature on the belief in small samples (Tversky and Kahneman 1971), here as a model of boundedly rational expectations. Because today's deliveries become tomorrow's anecdotes, the firm's offering decision in one period shapes demand in the next, and probabilistic selling becomes a dynamic problem. The paper's first main result, Proposition 1, solves the two-period problem when every customer draws a single anecdote.
A firm sells two versions of a product, and , over two periods . Each period has a fresh unit mass of customers. Every customer values at and at , with ; unit costs are ; and .
In period the firm posts one price for the opaque product and delivers with probability . A customer draws one anecdote and estimates the -probability as with prior , so . She buys if and only if
A period-1 anecdote is with probability . A period-2 anecdote comes from period 1 with probability and from period 2 otherwise, so it is with probability . Writing for the purchasing fraction, the firm's profit is
The price is what a customer with an anecdote is willing to pay; is what everyone pays. The alternative is transparent selling: one version at prices , bought in period iff .
Let , and . Over all feasible opaque and transparent policies:
with profit ;
In the order the paper's argument uses them:
The result says when, and how, a firm should randomize its product delivery when customers learn from anecdotes. The optimal offering probability is decreasing over time, : the firm delivers the high version generously early, so that period-1 deliveries become favourable anecdotes for period-2 customers, and then saves cost. Probabilistic selling is optimal only when both transparent margins are low, which makes it a complement to transparent selling rather than a substitute. Corollary 2 of the paper builds on Proposition 1 to show that the dynamic policy can earn up to twice the profit of the best static one.
Proposition 1 is proved in the paper's appendix (pp. 30–31), with Lemmas 1–4 proved in an online appendix. No part of it has been machine-checked. A formalization supplies the missing lemma proofs in checked form, pins down the conventions the printed statements leave implicit (tie-breaking, the price domain, the sign of ), and corrects a false part of Lemma 4 as printed. The model layer, an anecdote-based demand computed from a purchase rule, is a reusable template for other sampling-based expectation models.
The goal is a global optimality claim over a continuum of prices and offering probabilities and a second family of transparent policies. Lemma 1 reduces prices to two candidates, but each of the four resulting objectives is a non-separable quadratic in , maximized over a box. Objective (3) has seven regimes whose boundaries depend on and on the margin ratio ; the threshold is where the interior optimum's reaches zero. Comparing the regimes with each other and with transparent selling requires signed polynomial inequalities in and across regime boundaries. Checking first-order conditions is not enough: in part (iii) the claim is that no opaque policy at any price beats transparent selling, which requires bounding the box maximum of every objective, including the corner regimes.
Everything is real-valued and lives in the namespace DynOpaque.TwoPeriod. The definitions file states the model from its primitives: the anecdote estimate with and , the purchase rule (1) with equality buying, the purchasing fraction derived from them, profit (2), transparent profit from a version and two prices, the policy type with its feasibility predicate, and global optimality. The objectives (3)–(6) are separate literal definitions, so their agreement with (2) is a theorem, not a definition.
Committed conventions, each disclosed in the statements:
A formalization that optimizes only over the candidate prices , defines demand by the closed forms and , or defines the transparent value as would make Lemma 1 or part (iii) circular; the goal quantifies over every feasible price and derives demand from the purchase rule.
The general- model (Lemma 1 with binomial sums, Proposition 3), the extensions of §5, and Corollaries 1–2 are out of scope. Proofs of any milestone are welcome, and so are reusable lemmas on maximizing quadratics over a box.
Group buying sells a product at a discount once enough customers have committed to it. Groupon's "a deal a day" campaigns ran on a fixed deadline. Group buying on Pinduoduo has no preset deadline: a customer pledges, then waits until the group is complete. Most of the operations literature studies the first, fixed-duration form, in which a campaign ends at its deadline whether or not the threshold is reached. Hu, Liu and Zhai (SSRN 3242687, Manufacturing & Service Operations Management) study the flexible-duration form: the campaign stays open until customers have signed up, a batch of premium units is produced, and a new campaign starts at once.
In this form the expected waiting time of a new customer falls as the campaign fills up. A customer arriving early faces a long wait, a customer arriving late a short one. The firm can therefore use the state of the campaign itself to separate customer segments over time, which the paper calls intertemporal segmentation: high-valuation customers sign up early, and low-valuation customers join once the remaining wait is short enough. The paper's Proposition 2 says exactly when a profit-maximizing firm chooses this.
Customers arrive as a Poisson process with rate . A fraction are high-end, with valuation , and the rest are low-end, with valuation , where . The firm sells a regular product of quality at price and a group-buying premium product of quality at price . A customer who signs up for the premium product gets , where is her valuation, is her expected waiting time and is the waiting cost per unit time. Buying the regular product gives . Prices are fixed for the whole horizon, and the firm maximizes long-run average profit.
The pledge-to-go state is the number of further sign-ups the campaign still needs. In the equilibria of interest, high-end customers sign up at every state and low-end customers sign up once the state has fallen to the tipping state . The three resulting scenarios are (never tip, ), (intertemporal segmentation, ) and (always tip, ). The expected waiting time is
The firm sets . Its premium price is the largest one that keeps high-end customers signing up at state and low-end customers at state :
At only applies. The profit is revenue per expected renewal cycle.
With , and , the optimal tipping state over is
In each case the optimal price and profit also have the closed forms printed in the proof (Online Appendix pp. 4–5).
Proposition 2 is the paper's characterization of equilibrium segmentation. It shows that a flexible-duration campaign can separate customers through time alone, with one uniform price. It also shows that the separation is chosen for every large enough batch size, whatever the valuation ratio. The profit comparisons of the paper's Theorem 2, between group buying and the volume, margin and product-line strategies, are built on these closed forms.
The proof is a printed calculation on Online Appendix pp. 3–5, and no part of it has been machine-checked. A formalization checks three things: the case analysis over the whole interval , including the junction at and the endpoint ; the closed forms, notably ; and the threshold algebra.
The calculations are elementary, but is piecewise. The price switches branch at , and at it is not given by the minimum formula at all. A proof must compare the maxima of both branches with the value at . In case (ii-1) with , the late branch is decreasing and its supremum is approached as without being attained. Only the jump of the price at makes optimal there. The obvious argument, "each branch is monotone, so compare endpoints", has to handle this endpoint carefully.
Params with a predicate Standing (, , , , ). The batch size is a natural number .Defining or case by case, or maximizing over only, would trivialize the goal. Both are ruled out: is the binding-constraint minimum, and the maximum ranges over the whole interval.
Only Mathlib's real analysis (HasDerivAt, monotonicity from derivatives) is needed. Proofs of any milestone are welcome. The model definition is specific to this paper.
Optimization problems often require a smooth objective to be minimized subject to membership in a set. When that set is convex, established second-order conditions describe how curvature of the objective and constraints limits a local solution. Complementarity constraints and related models lead to nonconvex constraint sets. The tangent sets needed for a second-order condition can then be nonconvex as well, so a condition expressed only through ordinary convex support functions does not cover the general case. Gfrerer, Ye, and Zhou study this setting and state a directional necessary condition that permits a nonconvex set and a directional form of metric subregularity. Their result is Theorem 2 of arXiv:1911.04076v2, on printed page 16.
The mission concerns the first of the paper's two approaches to second-order necessary conditions. It targets the theorem that uses a lower generalized support function. The paper also develops conditions through convex duality under a stronger directional qualification; those results have different hypotheses and are outside this mission's target. The theorem here is a proved mathematical result whose statement and supporting definitions remain to be formalized and proved in Lean.
Fix natural dimensions and . A problem consists of twice continuously differentiable maps and , together with a closed set . Its feasible region is . A point is a local solution if no sufficiently nearby feasible point has a smaller value of .
For a set and a point , the contingent cone collects limits of directions of feasible displacements as . Given a direction , the outer second-order tangent set collects limits of for displacements . It can be empty and need not be convex. The regular normal cone describes vectors whose inner product with nearby displacements into is negligible to first order. Limits of these normals form the limiting normal cone ; restricting their approach to direction gives the directional limiting normal cone .
The critical cone at is . Directional metric subregularity requires an error bound near within a neighborhood of the ray in direction : distance to is at most a positive constant times distance from to . The neighborhood is precisely from Definition 6, including the zero direction.
The Lagrangian is . A directional M-multiplier at satisfies and . For a set and a subset , the lower generalized support function is the lower limit, as , of the infimum of over with . Write when is the whole space. The paper's Definition 7 assigns to the unrestricted function when is empty.
Let and let . The main target is Theorem 2, equations (17) and (18): if is a local solution, , directional metric subregularity holds along , and is nonempty, then one directional M-multiplier works for every :
The same multiplier gives the unrestricted conclusion . The goal retains the order “there exists such that for every .” The milestones state the paper's supporting results: the distance and outer-limit identity, the tangent and second-order tangent chain rules, their error bound and nonemptiness consequence, the primal second-order necessary condition, the critical-direction derivative condition, and the inclusion of limiting normals to a second-order tangent set.
The result supplies a directional dual necessary condition for a local minimizer without assuming that is convex. Its multiplier belongs to a directional normal cone, which can be smaller than the ordinary limiting normal cone. The set also lets the condition retain information about which second-order constraint perturbations arise from feasible displacements. The paper explains that taking gives a more tractable but weaker condition, while gives the strongest member of this family on page 17.
A complete formalization would provide checked interfaces for second-order tangent sets, directional normals, directional metric subregularity, and lower generalized support. Those objects can be reused in later work on nonconvex constrained optimization. This mission supplies statements and definitions; the published mathematical argument still needs a Lean proof. The local draft's compilation checks statement well-formedness, not the theorems' truth.
At a local minimum, ordinary first-order information constrains derivatives along contingent directions. The second-order tangent set is harder: it may be empty, and even when the original set is convex it need not be convex. The usual convex-support interpretation therefore cannot simply be applied to it. In addition, the error bound for the original constraint system must remain valid in the second-order linearized setting before normal-cone information can be transferred. These are the substantive points represented by Proposition 5 and Lemma 3 in the milestone list.
The Lean development uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so both dimensions are finite and may be zero. The standing assumptions of are explicit: both maps are and is closed. The contingent and second-order tangent sets use positive sequences tending to zero; a monotonically decreasing sequence can be selected from one of these. Tangent sets and normal cones are empty when their base point is outside the underlying set, matching the domain stated in Definitions 1, 3 and 4. Second derivatives are Fréchet derivatives applied twice to . A local minimum is stated together with feasibility.
Distances to possibly empty second-order tangent sets or outer limits use extended nonnegative reals, with distance to the empty set equal to . The lower generalized support function uses extended reals, where an empty infimum is ; the goal compares its value with the real Hessian value embedded in that order. This expresses the paper's “Hessian minus support is nonnegative” without undefined extended-real subtraction. Directional metric subregularity requires positive constants and the exact neighborhood in Definition 6, including ; it cannot be satisfied by making that neighborhood empty. Likewise the lower generalized support function is computed from limiting normals and is not assigned a constant extreme value.
The paper's is represented by and . The “modulus ” in Proposition 5 is represented by an admissible constant in the defining error bound. Equations (11), (12), and Corollary 1 contain printed slips in the point or derivative notation; their Lean statements use and as their surrounding formulas and proofs require. Equation (18) uses the same multiplier as (17), by taking to be the whole space. Contributions to the definitions, chain rules, error bound, normal-cone inclusion, and final theorem are all within scope.
Dividing a set of indivisible goods among agents with different preferences is a basic problem of fair division, with applications to inheritance, course allocation and the division of shared assets. With indivisible goods, envy-freeness and proportionality cannot always be achieved: a single good and two agents already rule both out. Budish (The combinatorial assignment problem, J. Political Economy, 2011) proposed the maxmin share as a benchmark that adapts to indivisibility: each agent is guaranteed what it could secure by partitioning all goods into bundles and receiving the worst one.
Whether every agent can receive its maxmin share at once has a short history.
This mission formalizes the additive result of the last paper.
There are agents and a finite set of goods (items) . Agent has a valuation on sets of goods. It is additive when
For a set function and , the -maxmin share of a set is
the maximum over all partitions of into disjoint parts, and is the maxmin share of agent .
An allocation gives each good to exactly one agent; is the set agent receives. It is -MMS if for every agent.
The paper's proof works with instances , a set of agents and a set of goods. An instance is -reducible (Definition 2.1) if some non-empty set of agents can be given a set of goods so that each agent of gets at least and every other agent keeps its share in the smaller instance, ; otherwise it is -irreducible. The proof also uses bipartite graphs between goods and agents, maximum matchings, the set of vertices not reachable by alternating paths (Definition 3.5), maximum cardinality maximum weight matchings (MCMWM), and an envy relation among agents holding partial bundles (Definitions 3.9–3.12).
For every and all additive valuations on there is an allocation of with
Table 1 of the paper (p. 5) lists this existential statement as Theorem 3.39; the sentence printed under that number on p. 30 is the claim that the paper's algorithm satisfies every agent before it stops. The goal fixes no normalization of the valuations.
The milestones are the statements of §2 and §3.2–§3.3 that the existence proof uses, in attack order.
The result. The factor broke a barrier at that several earlier techniques could not pass. It shows that the structural properties of the maxmin share known before were not the limit of what can be guaranteed, and its reducibility argument and double-counting techniques were reused in later improvements of the constant. The value of the best possible constant remains open: Feige, Sapir and Tauber (WINE 2021) showed it is at most .
Formalizing it. The theorem is proved on paper, in a long case analysis spread over about forty pages of the paper and its appendices. To our knowledge no part of it has a machine-checked proof. A formal development would check the case analysis and would provide reusable statements about maxmin shares under removal of goods and agents, about alternating-path structure in bipartite matchings, and about maximum weight matchings. These are used across the fair-division literature.
The obvious approach is to fill bags greedily: give an agent a bag as soon as it reaches of its share. This works when all goods are small, but large goods break it. A bag closed by a large good can be worth far more than to the agent who takes it, and the goods left over may no longer be worth enough to the remaining agents. Reducibility removes the very large goods (Lemmas 3.1–3.3), but goods worth between roughly and remain. Assigning them requires clustering the agents through matchings (Lemmas 3.6–3.13) and a careful order in which the clusters are served. The final counting argument, which shows that the leftover goods suffice for the agents not yet served, is the step that depends on all the earlier structure.
Agents are Fin n and goods Fin m. Valuations are v : Fin n → Finset (Fin m) → ℝ with the published LittleCharity.MMS.IsAdditive (sum of singleton values, non-negative). The paper's printed additivity identity on p. 12 contains a sign slip; the paper uses only the sum form. The maxmin share is the published LittleCharity.MMS.mms (v i) k S, a maximum over labelled, possibly empty -partitions. An allocation is a map A : Fin m → Fin n; agent receives the goods mapped to . Instances are pairs of finite sets of the ambient agents and goods, so sub-instances need no re-indexing.
The following conventions are added or chosen, each disclosed in the item's Formalization Note:
Bipartite graphs are two finite vertex sets with an edge set . Alternating-path reachability is an inductive predicate.
The goal is the unconditional existence statement. A formalization that assumes or irreducibility in the goal, or that drops the requirement that every good be allocated, does not state the paper's theorem. Neither does one that lets the reducing set be empty, which would make every irreducibility hypothesis unsatisfiable. The paper's Algorithms 1–3, the running-time statement of Theorem 3.40, and the algorithm-state Lemmas 3.36–3.38 are not posed.
A complete development needs basic facts about maxmin shares (monotonicity in the number of parts, removal of goods), Hall's theorem and Berge's augmenting-path characterization for bipartite matchings, and the exchange arguments for MCMWMs. The matching and maxmin-share lemmas are reusable beyond this mission. Proofs of any milestone, and of auxiliary facts about mms, are welcome.
An intervention inside a continuing system can change what happens after the moment at which it is assigned. In a search service, for example, an action shown now can alter the system state that later users encounter. A simple randomized experiment therefore mixes two effects: the immediate reward of treatment and the change in the distribution of future states. Farias, Li, Peng and Zheng model this setting as a finite Markov decision process and study how to estimate the long-run effect of always using the intervention from data collected while treatment is randomized Farias et al., 2022.
The paper calls the difference between treatment and control averages the Naive estimator. It can be biased at first order in the intervention's effect on transitions, because both averages use the state distribution generated by the randomized experiment. The differences-in-Q estimator uses state-action values instead of immediate rewards. Theorem 1 asserts that its population bias is at most second order in that transition effect under a geometric mixing assumption Farias et al., 2022, Theorem 1.
Let be a finite state space. At each time, the system takes one of two actions: is control and is intervention. An action at state earns a real reward and moves to the next state according to the row of a stochastic matrix . The control policy always selects ; the intervention policy always selects . The experiment policy selects each action with probability one half independently at each decision, so its transition matrix and expected reward vector are
Write , and for stationary probability distributions of these three matrices. The average treatment effect is the difference between the long-run average rewards under always intervening and always controlling:
For the experiment policy, is the expected excess reward when action is taken first at state and the experiment policy is followed thereafter. Excess means reward relative to the experiment's stationary average reward . The idealized differences-in-Q value is
This is the population quantity whose bias Theorem 1 bounds. It is distinct from the finite-sample estimator calculated from a trajectory Farias et al., 2022, §3.1–3.2.
The mixing condition, Assumption 1, says that for every state and time , the total-variation distance between the -step experiment law and its stationary law is at most . The intervention impact is measured by a second total-variation bound, for every Farias et al., 2022, Assumption 1 and Theorem 1.
The goal is Theorem 1. With , it asks for one polynomial , valid uniformly over all finite models and all admissible , and , such that
This formalizes the paper's statement that the unspecified constant depends polynomially on . The polynomial is quantified before the state space and the model, so its coefficients cannot be chosen from a particular example.
Five subtargets record the paper's route to this statement: Lemma 1's stationary-distribution perturbation identity; the corrected norm bound of Appendix F, Lemma 2; the corrected average-treatment-effect expansion in Eq. (6); the identification of the experiment's relative value with a group-inverse expression; and the identity that makes the first-order truncation Farias et al., 2022, pp. 13–15, 41. The goal and these milestones concern the idealized population estimator. Asymptotic normality and finite-sample estimation from Theorem 2 are outside this mission.
The result quantifies what the DQ adjustment buys in a dynamic experiment. When action-dependent transitions differ by at most in total variation, the population bias scales as , with an explicit dependence on the experiment chain's mixing rate and the reward bound. This provides a statement against which variants of the estimator and sharper constants can be compared Farias et al., 2022, Theorem 1.
The theorem is proved in the cited paper; the task here is to give its claim and the supporting identities machine-checkable proofs. The finite-chain definitions, perturbation identity and group-inverse bound can be reused in other average-reward Markov-chain arguments. No machine-checked proof of this theorem or these milestones was found in the local Prove2Me catalog search for this mission.
The immediate-reward difference averages under , whereas the treatment effect compares rewards under and . Replacing both stationary laws by therefore loses a term of order in general. The relative-value and Q-function expressions account for that term, but their definitions involve infinite excess-reward series. A formal proof must establish their convergence from mixing and reconcile them with the matrix group inverse. It must also control the norm of that inverse with the paper's precise row norm; using a generic matrix norm would change the claim.
The state type is finite, actions are Fin 2, and reward vectors take real values. The matrices and are row stochastic. Primitivity represents the §2 standing ergodicity convention for the control and intervention policies. A stationary distribution is a nonnegative vector summing to one, so an empty state space cannot satisfy the theorem's hypotheses. Total variation is half the rowwise distance. The paper's is the maximum absolute row sum, and is a rank-one matrix. The group inverse is represented by , used under hypotheses making the inverse valid Farias et al., 2022, Appendix A.
The relative value and action value are sums of expected excess rewards, matching the reading of the paper's expectation formulas used in §3.3. They are not defined by the group inverse: the equivalence is a milestone. The idealized DQ value averages their action difference under ; the ATE uses the stationary-distribution form stated on p. 13. The goal assumes , as required by the mixing expression and the denominator. Its polynomial constant is uniform over all instances. These choices exclude an instance-dependent constant or a definition that builds the desired equality into .
The Appendix F version of Lemma 2 is corrected with : without it, the one-state case permits a negative stated upper bound. Its premise bounds the maximum row norm. The p. 14 total-variation version omits the factor of two needed to convert to that norm. Accordingly, the remainder inequality and Eq. (6) milestones use the corrected Appendix F premise; their verbatim fields preserve what the paper prints Farias et al., 2022, pp. 14, 41. Contributions that establish these identities and bounds under the stated hypotheses, including reusable finite-chain matrix results and summability facts, are within scope.
A prophet inequality compares the value obtained by an online decision maker with the largest value in a sequence that could be chosen by someone who sees the entire sequence. The online decision maker observes values one at a time and must decide whether to accept the current value before seeing future values. When the common distribution of the values is known, that distribution can inform the stopping rule. This mission concerns the case in which the distribution is unknown and the rule receives no advance samples. The restriction is operational: the same rule must work across every possible common distribution of the observations. Correa, Dütting, Fischer and Schewior show that the familiar success scale of the classical secretary problem is the sharp asymptotic limit for this setting.
The result matters to online selection when historical observations are unavailable. It says that the loss from not knowing the distribution cannot be removed merely by choosing a more elaborate rule based on the values seen so far. It identifies an asymptotic ceiling that applies to every randomized stopping rule, including rules that react to exact numerical values rather than only to their ranks. The paper also studies what changes when samples are supplied; this mission isolates its zero-sample upper bound. The source paper states the result as Theorem 2 on page 6 of arXiv:1811.06114v2.
Fix a horizon . Independent observations have the same unknown law on the nonnegative real numbers. A stopping rule first receives independent samples from that law and then sees the observations in order. At time , the rule returns a number . This is its conditional probability of stopping on , given the samples, the observed prefix , and the fact that it has not already stopped. A rule with has no preliminary samples. Its behavior may depend on every observed value and may be randomized.
For fixed samples and observed values , the conditional probability that the rule stops at is
If it never stops, its payoff is . The benchmark is the prophet's maximum . A rule has approximation guarantee when for every allowed law . The paper uses this model in §2, page 5, and develops the zero-sample upper bound in §3.2, pages 6–8. Correa et al.
Two restrictions of a rule appear in the supporting results. A rule is order oblivious when rearranging distinct, nonnegative values seen before the current observation does not change its current stopping probability. A rule is value oblivious on a set when, on histories of distinct values from whose current value exceeds the earlier values, its stopping probability at time lies in for some . The depend on the time, while the interval works for every qualifying history in . These are Definitions 1 and 2 of the paper. Correa et al.
The central target is the paper's Theorem 2. For every tolerance , a single threshold works for all sufficiently long horizons and all zero-sample rules:
The adversarial law is chosen after the rule ; the threshold depends only on . The positive benchmark makes the ratio meaningful. The law in the formal target has finite support, as does the law constructed in the paper's proof.
The milestones follow the paper's stated results and displayed bounds. Lemma 2 supplies an order-oblivious rule with the same guarantee; Lemma 3 is the infinite Ramsey statement used for an infinite monochromatic set; and Lemma 1 supplies an value-oblivious rule on an infinite set. Equation (1) bounds the expected maximum for the paper's hard distribution. The pointwise display before equation (5) bounds the effect of replacing an approximately value-oblivious rule by a record rule. Equation (4) gives the asymptotic secretary upper bound for that record rule. In the formal statements, the terms in (1) and (4) have explicit finite-horizon or meanings. Correa et al., pp. 6–10
The theorem establishes a ceiling on the worst-case approximation ratio of any zero-sample rule. Its quantifier order matters: a rule may perform well on particular distributions, yet no single rule can exceed uniformly over all unknown distributions for large . Together with the paper's lower bound in Theorem 1, it identifies the sharp asymptotic guarantee without samples. It also gives a baseline against which the paper measures the value of additional samples. Correa et al., Theorems 1–2
The mathematical result is proved in the source paper; the work here is to give a machine-checkable statement and a decomposition that can support a Lean proof. The reusable pieces include a finite-law stopping model, exact conditional stopping probabilities, order and value obliviousness, a uniform-permutation success probability, and an infinite Ramsey statement. The theorem statements in this proposal remain open proof goals. Their compilation checks the representation and syntax, not their truth; solvers must still provide proofs.
The stopping rule class is large. Each can use the exact numerical values of all observations seen so far, and those values range over a continuum. The standard secretary bound concerns decisions based on relative ranks, so it does not immediately bound a value-dependent rule. The upper bound must apply to every such rule while allowing the adversarial distribution to depend on it. A finite hard distribution also produces repeated observations with positive probability, whereas the rank comparison that motivates the secretary bound is simplest on distinct observations. The milestones expose both issues as precise statements without building them into the goal as assumptions. Correa et al., §3.2–3.3
Lean represents values by real numbers and laws by a finite support in with nonnegative masses summing to one. Expectations are finite sums over independent product weights. This finite-law class strengthens the existential law in Theorem 2 and restricts the distribution-uniform guarantees in Lemmas 1 and 2; the paper's upper-bound construction has finite support. The rules themselves are arbitrary real-valued functions on real sample and observation vectors, with outputs in . They are not limited to deterministic, threshold, rank-based, or measurable rules. Indices start at zero in Lean, so Lean index is the paper's time . Failure to stop has payoff zero.
The positive-benchmark clause rules out the point mass at zero, which would satisfy the printed existential inequality as for every rule and make the target empty of content. For the same reason, the formalization uses the actual expectation of the maximum and the actual expectation selected by the rule, rather than stipulating a closed-form success bound. A set may contain zero in Lean, though the paper denotes positive integers by ; infinitude is unchanged by that one extra point. The paper's Definition 2 prints where its quantified time is ; the formalization uses . The hard instance and record rule are defined from their parameters, not supplied as unrelated variables. The convention for a zero-length maximum is Lean's real supremum default, but the hard-instance bound explicitly requires .
A complete development can use Mathlib's finite sums, finite products, permutations, real exponential, and finite-set machinery. The stochastic model and its obliviousness predicates can be reused for sample-complexity variants; the Ramsey theorem is useful independently. Contributions proving the listed milestones, strengthening the finite-law model to broader distributions, or connecting the record-rule bound to an existing secretary formalization are within scope.
A correlated equilibrium (Aumann, 1974) is a profile of strategies chosen by a mediator: the mediator draws a joint recommendation from a known distribution, tells each player only their own component, and no player can lower their expected cost by systematically deviating from what they are told. Correlated equilibria contain the Nash equilibria, are computable by linear programming in finite games, and model situations with a coordinating device such as a traffic authority or a market designer.
Mean field games (Lasry–Lions, Huang–Malhamé–Caines, 2006) describe Nash equilibria of games with a large number of symmetric players who interact only through the empirical distribution of their states. The limit model replaces the players by one representative player facing a flow of distributions. Campi and Fischer (arXiv:2004.06185) ask what the corresponding limit object is for correlated equilibria. Their answer is the correlated mean field game solution: a joint law of a recommendation and a random flow of measures, which, unlike a Nash mean field equilibrium, need not be deterministic. They prove that this notion is the right one in both directions: limits of -player correlated equilibria are correlated solutions (Theorem 6.1), and every correlated solution is approximated by -player approximate correlated equilibria (Theorem 7.1). This mission targets Theorem 6.1.
Fix a horizon , nonempty finite sets (states) and (actions), and the noise space with the uniform law . is the simplex of probability vectors on with . The model data are a system function , a running cost and a terminal cost , with measurable and bounded and measurable.
A restricted strategy is a map ; their finite set is . A strategy modification is any map .
The -player game. Given an initial law on and a correlated profile , the mediator draws , independently of the initial states and of i.i.d. noises . Player moves by
except that a deviating player uses instead of . Its cost is the expected sum of running costs plus terminal cost. is an -correlated equilibrium if for all and , and symmetric if it is invariant under permutations of the players.
The mean field game. A correlated flow is . The representative player starts from , receives jointly with a random flow , , independent of and of the noises, and moves by with cost . is a correlated solution with initial distribution (Definition 4.1) if
Assume (A1) for a measurable with as , and is -a.e. continuous for every probability on ; (A2) continuous; (A3) is a symmetric -correlated equilibrium with initial law ; (A4) ; (A5) with . Let
computed with . Then
The milestones follow the proof: the coupling bound (2.1); the appendix lemmas on weak convergence (A.1, A.2); the coupling estimates (6.3) and (6.2) and the independence of Step Three; optimality of every limit point; the conditional-law lemmas (A.5, A.4); the pre-limit consistency identity of Step Four; Lemma A.3; consistency of every limit point.
Theorem 6.1 identifies the limit model of large symmetric games played with a mediator. It shows that correlation does not disappear in the limit: the flow of measures recommended by the mediator may remain random, and the limit object must record its joint law with the recommendation. Together with Theorem 7.1 it makes correlated mean field game solutions the exact counterpart of -player correlated equilibria, as mean field equilibria are of Nash equilibria. The example of Section 5 of the paper exhibits a correlated solution with a non-deterministic flow that is not a mixture of deterministic-flow solutions.
The result is proved in the paper; to our knowledge no part of it, nor any correlated-equilibrium mean field result, has been formalized. The mission produces a machine-checked model of discrete-time finite-state mean field games with a mediator, and general-purpose lemmas absent from Mathlib: a mapping theorem for almost everywhere continuous maps that identifies limits of relations , converging together on varying probability spaces, limits of regular conditional distributions, and the conditional law of an exchangeable coordinate given the empirical measure.
Compactness is immediate because all spaces are compact. The content is in identifying the limit. Two obvious steps fail. First, the system function is discontinuous (as in Remark 6.1), so the dynamics do not pass to the limit by the continuous mapping theorem; only almost-everywhere continuity with respect to measures of the form is available. Second, a unilateral deviation by player 1 changes the empirical measures seen by all other players, and through them the whole flow, so it is not clear that the limit flow under a deviation is the limit flow without it. Third, conditional laws are not continuous under convergence in distribution, yet consistency, a statement about the conditional law of the state given the whole flow, must survive the limit.
The Lean development lives in the namespace SimpleCorrMFG.Conv. is stdSimplex ℝ X with its subspace topology and Borel σ-algebra; flows are Fin (T+1) → P(X); restricted strategies are Fin T → X → Γ; times of actions and noises are Fin T (the noise has index ); players are Fin N and the paper's player 1 is index 0; is volume on unitInterval. Probability measures on are Mathlib's ProbabilityMeasure with the topology of weak convergence, and a limit point is the limit of a subsequence with strictly increasing indices.
The paper defines costs and through "any realization" and notes that they do not depend on the choice. The formalization uses the canonical realization: the product law of initial states, recommendations (or the correlated flow) and noises, with the states computed by the recursion. The consistency condition is stated as for every , and Borel , which is the definition of a regular conditional distribution given the whole flow. (A3) is required for , where the -player game is defined.
A formalization in which the flow is conditioned only up to time , in which the costs are integrals of possibly non-integrable functions, or in which "limit point" refers to a topology other than weak convergence would prove a different and weaker statement and is excluded. The standing assumptions that is measurable and are bounded and measurable are carried explicitly, so that no expected cost or law is a junk value.
Contributions are welcome on each milestone. The appendix lemmas are independent of the game and reusable. The written proof of (6.2) uses ; since (A1) does not require , this step needs the observation that the indicator in (A1) vanishes when the two measures coincide.
Supermarkets run temporary price promotions on a large share of their assortment, and the choice of which item to discount, by how much and in which week is a recurring planning decision for category managers. Promotions on one item change the sales of the others: a discount on one brand of coffee draws customers away from a competing brand (substitution), while a discount on shampoo can raise the sales of conditioner (complementarity). Promotions also have effects over time, because customers who stockpile during a promotion buy less afterwards.
M. C. Cohen, J. J. Kalas and G. Perakis (SSRN 3061451; Management Science, 2021, doi:10.1287/mnsc.2020.3641) formulate the multi-item promotion problem as a nonlinear integer program and approximate it by a hierarchy of linear integer programs , which add up the profit contributions of promoting up to items together. Their single-item predecessor, Cohen, Leung, Panchamgam, Perakis and Smith (Operations Research, 2017), corresponds to . The main structural result of the multi-item paper, its Theorem 1, says that under a common separability assumption on demand the hierarchy collapses at level two.
There are items and a selling season of periods. The retailer has enough inventory to meet demand throughout the season, as assumed in §2.1, so inventory does not enter the model. Item has a price ladder , where is the regular price, common to all items, and the other points are promotion prices. A plan chooses a level for every item and period; the price of item at period is . Item has unit costs and a memory , and its demand at period is a function
of its own current and past prices and of the other items' current prices (Assumption 1: cross past prices do not enter). The total profit of a plan is
and the problem (Multi-POP) maximizes it over plans satisfying the business rules: at most promotions of item , at most one promotion of item in any consecutive periods, at most promotions in total and at most in period .
A pattern assigns a level to each item; its support is the set of promoted items. The pure promotion vector uses at period and the regular price everywhere else, and is the all-regular plan. The coefficient of at is the inclusion–exclusion sum
where keeps the levels of on and is regular off . With one promoted item this is , equation (5); with two it is equation (6). The App(κ) objective of a plan is
which is equation (4) for , and maximizes it over the same feasible set.
Assume the cross-item effects are additively separable,
for arbitrary functions and . Then for every and all business-rule data,
This is the chain of the paper.
The size of grows like in the number of pairwise, triple and higher variables, and has a variable for every subset of items. Theorem 1 shows that under (8) nothing is gained beyond , an integer program with a quadratic number of variables. Equation (8) covers the demand models used in practice that the paper cites, the log-linear model with linear cross terms and the linear cross-elasticities model. The rest of the paper's solution approach works with : integrality of its LP relaxation for substitutable items (Theorem 2), a rounding scheme and a parametric bound (§3); Theorem 1 is what makes the complete cross-item model under (8).
The result is proved in the paper; its appendix carries out the order-three case explicitly and the induction step in outline, with "the details … omitted for conciseness". No machine-checked proof is known to exist. A formal proof removes the omitted cancellations and isolates the combinatorial core (milestone 5), which is a fact about pseudo-Boolean functions useful beyond promotions.
The coefficients are signed sums of total profits over all items and periods, and each profit is a product of a price margin and a demand that depends on a window of past prices. The obvious idea, expanding the products directly, gives an unmanageable number of terms. Every contribution involving three or more promoted items has to cancel, including the contributions at later periods, which see a promotion only through the memory window, and the paper omits these cancellations in the general induction step. Without (8) the claim fails: the paper notes that for demand models violating it is not necessarily equal to , and a demand with a three-way cross term already has nonzero order-three coefficients.
Lean namespace PromoMulti.PairwiseExact. Items are Fin N and periods Fin T, 0-based (period of the paper is index ); prices, costs and profits are real. A plan is a function assigning a level Fin (K i + 1) to each item and period, level 0 being the regular price ; this is the binary encoding with . Prices before the first period are (the appendix evaluates ); Theorem 1 holds for any fixed history. The paper's pairwise variables are separate binaries tied by the consistency constraints (7); for integral plans (7) forces them to be products, and the App(κ) objective uses that product directly. The paper writes out only for ; for the formalization uses the inclusion–exclusion extension of (4) with the general coefficient of p. 38. The demand receives the whole current price vector; (8) reads only the coordinates . The ladder order is not imposed, nor any monotonicity, linearity or sign of and : Theorem 1 uses none. The business rules are those of (Multi-POP); the inter-item rules 2, 3 and 5 of §2.2 are not part of it.
The coefficients are defined by the closed alternating sum and the App(κ) objective sums every pattern with ; a formalization that defines App(κ) through pairs only, defines higher coefficients as zero, or defines coefficients by the recursion (16) makes the goal trivial and is ruled out. The goal does not claim that App(2) solves (Multi-POP), which is false when past prices matter.
A complete development needs finite inclusion–exclusion over Finset.powerset, the cancellation lemma of milestone 5 (reusable for any pseudo-Boolean or multi-level function that is a sum of low-arity terms), and the bookkeeping of which plan coordinates each item–period profit reads. Contributions of proofs of any milestone, of milestone 5 in greater generality, and of alternative arguments are welcome.
A discrete moment problem asks for the largest expected payoff compatible with prescribed moments of an unknown probability distribution. A decision maker may know the first few moments of demand or loss while the full distribution remains uncertain. The optimization then asks which compatible distribution makes a chosen payoff largest. Chen, He, Jiang, Ryan, and Zhang study what happens when the distribution must also obey a shape constraint. Their preprint treats discrete log-concavity and increasing failure rate as two such constraints. This mission concerns the log-concave case.
The moment constraints alone define a convex polytope of probability vectors. Requiring log-concavity changes its geometry: the feasible region is generally nonconvex. This matters because familiar descriptions of extreme points of a moment polytope no longer describe the candidate worst-case distributions. The paper's Theorem 4.1 gives a finite structural description of the optimal extreme points despite that change. Its proof uses a general result about optimization over reverse convex constraints, Theorem 3.6, which is also included as a milestone. Both statements and their setting are taken from arXiv:1708.02079v1, pages 5–15.
Fix the finite sample space . A distribution is a vector of nonnegative masses. For each integer from through , its prescribed moment is , so . The convention makes the masses sum to one. Given payoff coefficients , the discrete moment problem maximizes over the distributions satisfying these equations.
A distribution is discrete log-concave when its positive masses form one consecutive integer interval and at every interior index . In the paper's formulation (DMP-LC), the entries on are strictly positive and the other entries are zero; the feasible region is the union over all such supports. Its alternative formulation (DMP-LC′) replaces the chosen support with nonnegativity and a family of longer-range inequalities. Proposition 2.4 says that the two feasible regions coincide. The extreme points in this mission are those of the entire feasible region, including every possible support.
The paper also considers a general reverse convex program in : minimize a function subject to , , and for . Here the reverse convex condition is relative to the nonnegative orthant: the forbidden set is convex. Under the paper's continuity, quasiconcavity, differentiability, rank, and compactness assumptions, Theorem 3.6 counts the inequalities that are tight at an optimal extreme point.
The goal is the corrected mathematical content of Theorem 4.1. If (DMP-LC) is feasible, an optimal extreme point exists. Every optimal extreme point has support and can be covered by at most geometric pieces. In symbols, there are weakly increasing breakpoints and positive parameters such that
The milestone path includes the equivalence of the two feasible formulations, compact-set extreme-point results, convexity of the forbidden power regions, the reverse convex tight-constraint count, and the two structural steps in the proof of Theorem 4.1. Theorem 3.6 asserts, in particular, that at each optimal extreme point of its -row program,
The conclusion replaces an unrestricted search over feasible probability vectors with a characterization of the candidates that can be optimal extreme points. It also identifies how the number of prescribed nonzero-order moments controls the number of geometric pieces. The count in Theorem 3.6 applies to the larger class of reverse convex programs described above; it is useful independently of this distributional example. These are results proved in the cited preprint, rather than open conjectures.
The formalization target is to give the known statements a machine-checked proof in Lean. The proposed items are statements with proof placeholders; they do not yet assert that a machine-checked proof exists. The finite moment notation, the log-concave feasible region, and the reverse convex feasible region are separate definition files so the general finite-dimensional objects can be reused. Contributions to the milestone theorems, the proof of the goal, and supporting lemmas are all in scope.
The log-concavity inequalities do not make the feasible region convex, so the standard convex-polytope description of optimal extreme points does not directly apply. In addition, the chosen support may move: a vector that is extreme within one fixed-support slice need not be extreme in the full union. Existence of an optimal solution alone gives no bound on the number of geometric pieces. The challenge is to obtain enough tight constraints at every optimal extreme point, then relate those equalities to its coordinates without assuming the desired shape in the definition of feasibility.
Lean represents as Fin n → ℝ; a Fin n index with value represents the paper's position . The helper ext supplies the paper's one-based coordinates and returns zero outside . Moments use the exact weights . All feasible sets use real vectors, with nonnegativity or strict positivity stated where the paper requires it. The (DMP-LC) region is the union over supports satisfying (2b)–(2e); the goal uses extreme points of that whole set and a maximization objective. The reverse convex milestones use minimization, full row rank, and convexity of the forbidden sets inside the nonnegative orthant. Compactness and nonemptiness are explicit assumptions where the source invokes them.
Two corrections to the printed Theorem 4.1 are necessary. First, its bound is false. With , , , , and payoff , the unique maximizing extreme point is approximately , whose geometric ratio is about . The formal statement requires . Second, the printed strict chain of breakpoints fails for short supports: with , , and moments , the only feasible distribution is the point mass at . Weak breakpoints express the paper's “at most pieces” conclusion. They allow degenerate pieces; is retained and forces a point mass. The proof's closed-range wording for tight equalities is read on interior indices, and the tight count uses moment rows. These choices and the paper's typographical slips are recorded with the items.
The feasible region does not encode geometric sequences, and extremeness is never taken only within one support or within its convex hull. The development needs Mathlib's finite sums, finite-dimensional topology, convex hulls, extreme points, matrix rank, continuity, quasiconcavity, and differentiation. The finite discrete moment definition and reverse convex feasible-set definition are intended for reuse beyond this paper.
A minimum support price (MSP) guarantees farmers a unit sale price at least as high as an announced floor. It can protect farmers when the market price is low, but the same guarantee can require a government payment and can change how much crop is produced. Policy evaluation therefore needs to account for farmers, consumers, and public expenditure together. Chintapalli and Tang examine these effects when the market price is uncertain and farmers decide whether to sow before that price is known (SSRN manuscript, §§3–4). This mission takes the paper's market uncertainty model and its joint assessment of farmer net benefit and net social value. The result is already proved in the paper; the work here is to formalize its definitions and claims in Lean.
The farmer population has total mass one. Each farmer can produce one unit and has a cultivation cost uniformly distributed on . A farmer is small enough to take the eventual market price as given. At total production , the inverse demand price is , where is market potential and the shock is uniform on . The government announces an MSP before sowing. A participating farmer receives the effective price : the market price when it exceeds the guarantee and the guaranteed price otherwise (manuscript, pp. 6–8).
Farmers are risk averse according to the paper's value-at-risk participation rule. A farmer with cost finds the crop lucrative when the probability that effective price is no greater than cost is at most :
The equilibrium quantity equals the mass of farmers whose costs make cultivation lucrative when aggregate production is . The model does not prescribe this quantity in advance. Write for production without an effective guarantee and for the quantity identified by Theorem 1. The paper considers admissible MSPs : the guarantee lies between the lowest and highest possible market price at its equilibrium quantity, or (manuscript, eqs. (7) and (9), pp. 8–10).
Let be aggregate expected farmer surplus, computed from the effective sale price less each participating farmer's cost. Let be government expenditure on the positive difference between the guarantee and the market price. Let be consumer surplus, the area between inverse demand and the market price over units consumed. The paper evaluates a guarantee through net benefit and net social value (manuscript, pp. 7 and 11–12).
The milestone path first identifies individual participation and the unique equilibrium quantity, then establishes the paper's explicit formulas for , , and . Two identities in the proof of Proposition 1 summarize the resulting policy values for admissible :
The goal is Proposition 1 in full. When and , it states if and only if . It identifies an admissible maximizer of net benefit at and says net benefit is independent of in each of the regions and . It also states for every admissible and identifies an admissible maximizer at (manuscript, Proposition 1, p. 13). A maximizer is a price attaining the largest value; the proposition does not require uniqueness.
The two metrics answer different policy questions. Net benefit asks whether farmers' aggregate surplus exceeds the public cost of the support guarantee. Net social value adds consumer surplus to that accounting. Proposition 1 identifies which MSP maximizes each measure and states that the broader value remains positive throughout the admissible range. These conclusions are specific to the paper's linear inverse demand, continuous uniform cost and price shock, and risk-based sowing rule; they do not claim the same price choices for other agricultural markets (manuscript, §4.3).
Formalizing the result requires a machine-checkable account of the continuum of farmer costs, the uniformly distributed market shock, a fixed-point equilibrium, and integrals defining all three welfare components. The manuscript gives a proof; the Lean theorem files in this proposal state open proof obligations. A completed development would make the integral formulas, equilibrium characterization, and optimality claims reusable for related support-price models, while exposing exactly which modeling assumptions they need.
The farmer's sowing decision depends on the distribution of the effective price, and the effective price changes at the support threshold. At the same time, the market price depends on the aggregate number of farmers who sow. Directly inserting a guessed production quantity would skip the equilibrium question. The welfare formulas add a second layer: they must integrate the same participation rule and price guarantee, then compare policies only within the admissible set. Theorem 1's printed farmer-level biconditional also has a boundary cost that requires care, even though a single cost has zero mass under the uniform distribution (manuscript, Theorem 1 and its proof, pp. 10 and 37).
Lean represents prices, costs, probabilities, and welfare values in . The cost distribution is Lebesgue measure on ; the shock law is normalized Lebesgue measure on . The standing assumptions are , , , and . Positivity of is explicit in Lean because the uniform law and its expectation divide by . The paper treats it implicitly when it specifies a nondegenerate uniform shock. The lucrative rule uses weak inequalities on both the loss event and the probability bound, following the numbered model equations (manuscript, eqs. (1), (5), and (6)).
An MSP's admissibility is evaluated at an equilibrium quantity, not at an arbitrary guessed quantity. Equilibrium is defined as a fixed point of the mass of lucrative farmers; it is not defined to equal . Farmer surplus, expenditure, and consumer surplus are integrals, not the later closed forms. This prevents the goal from becoming a substitution exercise. Theorem 1 is restricted to admissible MSP values; its premise evaluates admissibility at the proposed equilibrium , which the theorem then identifies as the actual equilibrium. Its farmer-level clause excludes the one threshold cost at which the manuscript's biconditional is inaccurate. Aggregate equilibrium remains the same. The mission covers the single-crop market uncertainty model in §§3–4; the paper's yield uncertainty and two-crop extensions are separate results. Contributions to the fixed-point, measure, integration, and policy-optimization steps are all within scope.
Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation , TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.
The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach , nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.
Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.
A finite Markov reward process consists of a finite state space , a stochastic matrix with the probability of moving from to , transition rewards with , and a discount factor . The chain has a stationary distribution (), and the observed trajectory starts from , so it is a stationary sequence.
Each state carries a feature vector with . The steady-state feature covariance has full rank, and is its minimum eigenvalue. Value functions are compared in the steady-state seminorm .
At a transition the TD direction is . Its steady-state mean is , and the TD fixed point is the vector with . Projected TD(0) with radius starts from and iterates
where is the Euclidean projection onto the ball of radius . The averaged iterate is .
The chain mixes uniformly (Assumption 1): there are and with for all . The mixing time is . Write .
All three bounds are stated together, with the expectation over the stationary trajectory:
(a) for and ,
(b) for a constant ,
(c) for and ,
The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence (Lemma 1); the descent inequality (Lemma 3); the gradient bound (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound (Lemma 9); boundedness and Lipschitz continuity of the gradient error (Lemma 10); and the bias bound (Lemma 11).
Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning , part (b) shows exponential convergence to a neighbourhood whose radius scales with , and part (c) gives an rate. Compared with the i.i.d. bounds, the only change is a factor of order : roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.
The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.
The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses . Under Markov sampling this fails: is a function of and is correlated with the observation at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in steps, which is where the projection and the uniform gradient bound enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant (, ) tracked exactly.
Fintype. The expectation over the stationary trajectory is the finite sum , the exact law of for a finite chain started from , so no measure theory is used. The paper itself works with a finite (p. 5).EuclideanSpace ℝ (Fin d) with , so every is Euclidean.sInf over and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.Electricity end-users increasingly generate their own power with rooftop solar panels and small wind turbines. This distributed renewable energy (DRE) is usually sold under net metering: a customer who produces less than it consumes buys the shortfall from its utility at the retail price, and a customer who produces more sells the surplus back to the utility. The buy-back rate is either the retail price (the retail-based rule) or the wholesale price (the market-based rule); both are in force in different U.S. states.
The common view in the industry is that net-metered DRE hurts utilities twice: it shrinks their retail sales, and it obliges them to buy surplus energy at a rate above their procurement cost. Utilities have lobbied against net metering on this basis. Sunar and Swaminathan (SSRN 3257925; Management Science, 2021, doi:10.1287/mnsc.2020.3854) point out that this view ignores the wholesale market. A utility that meets part of its demand from a wholesale market, where generators compete in supply functions as in Klemperer and Meyer (1989) and Green and Newbery (1992), pays a market-clearing price that falls when DRE lowers the net wholesale demand. Their main result, Theorem 1, gives an exact condition under which net-metered DRE raises a utility's expected profit.
Wholesale market. There are generators. Generator submits a supply function and producing costs it , with . For a realized net wholesale demand , the market-clearing price solves . A profile is a supply function equilibrium (SFE, Definition 1) if no generator can raise its ex-post profit, for any realization of the demand, by submitting a different supply function. The symmetric profile with
is the equilibrium the paper works in; its clearing price is with .
Utilities. Utility sells at the retail price . Its net-metered customers demand and generate ; its total end-customer demand is with . It owns existing resources covering up to units at unit cost , with . and are bounded random variables, is the rest of the wholesale demand, and the net wholesale demand is
Utility 's expected profit under the rule is equation (6): retail revenue, minus the buy-back cost of the surplus at , minus the cost of buying the residual demand on the wholesale market, plus the revenue from selling any excess there. is the same profit when nobody generates ( everywhere, Definition 2). The constants , are the expected net demands of the rest of the market with and without DRE, and , are the explicit ratios (EC.16), (EC.17).
For there is a threshold such that for every ,
with the expression (EC.16)/(EC.17), which does not depend on .
Theorem 1 is the paper's headline: it reverses the industry's belief under stated conditions. It says that a market-reliant utility (small ) facing a wholesale price that is sensitive to demand (large ) earns strictly more with net-metered DRE than without it, and that this happens only under these two conditions. Corollary 1 adds that the gain from DRE is larger the more the utility relies on the market. The paper uses these results to argue that lobbying against net metering can hurt the lobbying utility.
The result has been published but not machine-checked. A formalization pins down exactly what Theorem 1 needs, and the planning analysis already found that the printed argument leaves gaps. Lemma EC.1 is false when the denominator of is not positive; a two-point counterexample is recorded in the item notes. The proof also uses an independence of region from the rest of the market that the paper does not state. Theorem 1 itself survives both gaps because its threshold is existential. A Lean proof would settle this, and would also give a reusable formal account of a supply function equilibrium with quadratic costs.
The obvious argument says that DRE lowers retail revenue and raises buy-back costs, so the utility must lose. It fails because the wholesale price is endogenous: DRE lowers and hence , which helps a utility that buys on the market and hurts one that sells. Three steps carry the weight. The first is a measure-theoretic reduction of (6), with its indicator terms, to closed forms; it needs the independence of region and the integrability of every term. The second is the sign analysis of a difference that is affine in , including the degenerate cases where 's denominator is or the slope vanishes. The third is the ex-post optimality of the symmetric supply function against every deviation , not only against differentiable or monotone ones.
Everything lives in the namespace NetMeterDRE.Profit. Two definition files: SFE (profit (EC.2), clearing (1), Definition 1, , ) and Model (utility data, standing assumptions, (5), the integrand of (6), , , , , , ). All quantities are real. Utilities are indexed by a finite type and generators by Fin N. Random primitives are measurable functions on a probability space and are almost surely bounded, so every expectation is of an integrable function. is . The wholesale price in every theorem is a function that clears the market of the symmetric profile at every demand; it is neither a free differentiable function nor a closed form.
Conventions committed to:
The goal cannot be trivialized by the formalization. is pinned to its explicit formula rather than existential, is chosen before , and is defined by (6), not by the closed forms, so milestones 3–4 are not definitional. Contributions are welcome on any milestone. Milestones 1–2 are self-contained algebra and analysis. Milestones 3–4 are the measure-theoretic core.