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?
A bank's failure can make its creditors fail, and those failures can cause further defaults. The final number of failures depends on the network of exposures as well as on each bank's ability to absorb losses. Amini, Cao and Sulem study this question in a directed random network whose banks may have different degrees and different default thresholds. Their limit theorems separate the case in which nearly every bank eventually defaults from the case in which the final counts have Gaussian fluctuations around explicit deterministic values. Those distinctions matter when a systemic-risk calculation depends on the distribution of a cascade's final size, rather than only on its expected size (Amini, Cao and Sulem, arXiv:2104.00248v1, §§2–4).
The paper was first available as the pinned 2021 preprint used here and was published in Mathematics of Operations Research in 2024. This mission follows the preprint's section, page and theorem numbering throughout. Its target is Theorem 3.7 on preprint page 13.
An economy has banks, each assigned a characteristic from a countable set . A type specifies an incoming degree , an outgoing degree , and a default threshold . The threshold is the number of defaulted incoming counterparties that bank can tolerate before it becomes insolvent. For a bank of type , has probability law on . The fraction of banks of type is . As the economies grow, the type fractions and threshold laws approach and .
The paper represents exposures as incoming and outgoing half-edges. Its balls-and-bins death process gives every incoming ball an independent exponential lifetime of mean one. A bank is solvent at time while fewer than of its incoming balls have died. Threshold-zero banks are therefore defaulted at the start. The process tracks five quantities: solvent banks , defaulted banks , alive incoming balls of solvent banks , alive incoming balls of defaulted banks , and white infected outgoing balls . If is the total number of alive incoming balls and the outgoing balls of solvent banks, the paper's initial recolouring convention gives . The final time is the first nonnegative time at which becomes negative (§2.4, pp. 8–9).
For , let be a binomial probability and its upper tail. The paper's functions describe the deterministic scale of the five counts at time after setting . Write for their vector, and for the same formulas with finite-economy parameters. The final-size parameter is the largest zero
and is the corresponding largest zero of . A zero is stable when . The class count records solvent banks of type , threshold , and dead incoming balls, with (§3, pp. 9–13).
The goal is both parts of Theorem 3.7. If , the final default fraction tends to one in probability:
If and , then and the five final counts converge jointly:
Here is an explicit covariance formed by drawing a threshold and an independent binomial number of surviving incoming balls for each type. The theorem also gives a one-dimensional Gaussian limit for every admissible , centred at its finite-economy value. The milestones are Lemma A.4, the largest-zero claim in the proof of Theorem 3.7, and the process limits Theorems 3.5 and 3.6. They cover uniform derivatives, zero location and the Gaussian process limits in the stronger moment regime of Assumption 3b. The paper's Theorem 3.1, Lemma 3.2 and Theorem 3.3 are omitted as milestones because their printed weaker Assumption 3a allows outgoing degree mass to escape to rarer types; the formalization notes give a counterexample.
The stable regime supplies a distributional approximation for the final number of solvent and defaulted banks and for the numbers of healthy and infected links. It also quantifies fluctuations of a specified type-threshold class. The degenerate regime identifies a qualitatively different outcome: almost all banks default. The paper uses these counts as inputs to systemic-risk aggregates in its following section (§4, pp. 13–15).
The results are proved in the paper, but the goal and its four curated source results were not found as matching formal statements in the Prove2Me catalog during preparation. Formalizing them would provide reusable statements about first-passage times, countably typed death processes and vector-valued process limits. The cited Glivenko–Cantelli theorem is already proved on the platform, while a general martingale functional central limit theorem is posed there as an open goal; neither is substituted for a paper-specific milestone. Solvers can contribute the probability infrastructure as well as proofs of the listed statements.
The fixed-time counts are sums over many bank types, but the type space can be infinite and degrees need not be uniformly bounded. Pointwise convergence for each type does not by itself control the total process or all derivatives of its fluid functions. More importantly, the cascade ends at the random time , while the process limit is indexed by deterministic time. Substituting directly into a fixed-time Gaussian limit loses the fluctuation of the stopping time and produces the wrong final covariance. A proof must retain the joint process fluctuations and the behaviour of the largest finite-economy zero near the stable limit.
Lean uses Fin n for banks, a countable type space , real time , and a single probability space for the sequence of economies; no dependence across different is assumed. It orders the five coordinates as , represents each in-ball by an index , and uses ordinary real derivatives. The threshold laws are supported on , thresholds and actual in-ball lifetimes are jointly independent within each economy, and the incoming and outgoing degree sums agree for every . These conditions make explicit requirements used by the paper's formulas and proofs. The finite and fluid functions use , the finite mean degree, where the preprint prints (p. 12).
The printed lifetime variance in equations (24) and (39) is too small by a factor of two. The limit here uses the corrected per-bank covariance ; for a single incoming ball the Bernoulli variance is , rather than . The statement concerns the balls-and-bins death process of §2.4, on which the paper's §3 states its theorems; the equivalence with the default cascade on the configuration model, asserted in §2.4, is not formalized.
The explicit covariance, the joint five-coordinate law, and evaluation at the random rule out an unspecified or existential covariance, separate marginal limits, and substitution of the deterministic . The degree moment and probability assumptions exclude junk Gaussian, derivative and infinite-sum values. The model definitions, the corrected covariance and the path-convergence reference are reusable beyond this mission. Theorem 4.1 and later systemic-risk aggregates are outside this final-size target.
A seller who can inspect a buyer's true value after receiving a bid can use the bid as a refundable deposit. A truthful buyer may receive a reward, while a buyer whose report is false forfeits the deposit. This changes the incentive constraint: a buyer who considers reporting compares her truthful utility with , not with the payoff from a conventional payment schedule at the false report. Alaei, Belloni, Makhdoumi, and Malekian study the revenue-maximizing design for this setting in Optimal Auction Design with Deferred Inspection and Reward, §§2–3.
The single-agent problem is a useful test of how inspection affects mechanism design. The paper gives an explicit bid function, allocation rule, and payment rule for a general positive differentiable value density. The mission asks for a formal statement and proof of that characterization, including the claim that the proposed auction is optimal among every feasible deferred-inspection mechanism. The source used here is the SSRN copy dated 2022-03-22; all page and result numbers refer to that copy.
The buyer has a private value in . Its density is differentiable and strictly positive on , and integrates to one. The seller allocates one object with probability after report . The buyer pays the report as a deposit. After inspection reveals the true value, a truthful report may earn a nonnegative reward; a false report earns none. Write for the seller's net payment when the buyer reports truthfully.
A pair is incentive compatible and individually rational when, for every ,
The first inequality includes the forfeited deposit . Expected revenue is . Feasibility also requires to be integrable, so this real-valued objective represents an expectation. These are Problem (7)–(9) on p. 7 of the source.
For a fixed allocation, (10) defines its greatest compatible payment
The best-alternative bid is the largest report attaining that minimum, when an attaining report exists. The paper also considers allocations that are strictly concave and differentiable up to a threshold and equal to one thereafter. It calls this class SCD. Those concepts are represented directly in the mission's definition module.
The goal is Theorem 2 on p. 12. Put
The theorem asserts that thresholds exist with and with the integral branch of the proposed allocation reaching one at . The allocation is above and
where . Its payment is at or below , between the thresholds, and at or above . The formal goal says this explicit pair is feasible and that for every feasible pair . It also asserts that a threshold pair exists.
The milestones follow the paper's route: Proposition 2 identifies ; Lemma 1 records payment improvements from removing allocation decreases, changing endpoints, and taking the concave hull; Lemma 2 supplies smooth strictly concave approximations with convergent revenue; and the sound part of Proposition 3 concerns best-alternative bids. The final two targets are the differential identity for in the proof of Theorem 2 and the threshold equation (15). Their source wording, page, and PDF hash are attached to each milestone.
The result replaces an optimization over pairs of functions subject to all pairwise incentive inequalities with explicit rules calculated from the value density. It determines both the allocation probabilities and the payments in the inspection model. For the uniform density, Example 2 on pp. 13–14 gives a continuous allocation and revenue about , compared with for the standard no-inspection benchmark in that example; see the source. The difference comes from the seller's ability to retain the deposit after a false report.
The paper has a published mathematical argument, but these exact statements have no machine-checked proofs in this mission. A completed formalization would provide reusable definitions for truthful reporting with forfeited deposits, the optimal-payment operator, and the inverse weighted distribution . It would also resolve proof gaps visible in the source rather than silently taking them as assumptions. Theorem 1 of the SSRN copy is false as printed for its stated bid class and is deliberately absent from the formal targets; the mission's goal is Theorem 2 itself.
The main obstacle is global optimality. Checking a derivative or a local incentive condition does not compare the proposed auction against every feasible mechanism. Every type can contemplate every false report, so a local condition alone does not settle incentive compatibility. The appendix derives the proposed bid through variations of an allocation-dependent functional, including Dirac-delta perturbations and an unconstrained reformulation in Theorem 1. Its admissible bids do not all correspond to feasible allocations satisfying the endpoint condition. A proof of Theorem 2 must establish the global revenue comparison without treating that reformulation as an already valid equivalence.
The boundary is also mathematically delicate. The derivative becomes singular as approaches from above, although the allocation integral remains meaningful for the intended positive threshold. Formula (15) must have a genuine solution; merely quantifying over thresholds satisfying an equation would make the optimality clause empty if no such pair existed.
Lean represents values by real numbers and restricts every value and report quantifier to . The density carries exactly Assumption 1's differentiability, positivity, and unit integral; the absence of point masses follows from the density representation. Allocation and payment functions are total real functions whose values outside the value interval have no economic role. Expected payment is a real interval integral, and feasible mechanisms require integrability of .
The inverse is the lower inverse on , formed with a real infimum. Its intended calls are within the range of . The displayed allocation uses the ordinary derivative of the explicit bid on its open differentiability interval; the singular endpoint does not affect the integral. The equation is read through the integral branch, not through the constant-one branch, because it determines the threshold by continuity. The goal states existence of thresholds and optimality over all feasible mechanisms. In particular, the incentive condition is not replaced by the classical , and comparison is not restricted to SCD, concave, or monotone allocations.
Proposition 2 and Lemma 1 are expressed as payment-improvement statements, since pointwise assertions about every revenue optimum fail after null-set changes. Proposition 3 keeps the unique minimizer and monotonicity claims but narrows strict increase to the region before the bid reaches ; the printed full-interval claim admits a flat segment. The derivative identity is stated on , where its terms are defined. Contributions that prove these precise statements, construct the threshold solution, or establish the final global comparison are within scope.
A transformation achieving the optimal symmetric N-to-M cloning of coherent states is presented. Its implementation only requires a phase-insensitive linear amplifier and a network of beam splitters. An experimental demonstration of this continuous-variable cloner should therefore be in the scope of current technology. The link between optimal quantum cloning and optimal amplification of quantum states is also pointed out.
This mission is the statement-level formalization of Optimal cloning of coherent states with a linear amplifier and beam splitters (arXiv:quant-ph/0012046v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal coherent-state cloning by concentration, amplification, and distribution (Unnumbered main result; Eqs.(10)–(12), PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
We consider two examples of dynamical semigroups obtained by singular perturbations of a standard generator which are special case of unbounded completely positive perturbations studied in detail in [10]. In the section 2 we propose a generalization of an example from [1] aimed to give a positive answer to a conjecture of Arveson. In the section 3 we consider in greater detail an improved and simplified construction of a nonstandard dynamical semigroup outlined in our short communication [13].
This mission is the statement-level formalization of On singular perturbations of quantum dynamical semigroups (arXiv:1706.04866v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Rebound diffusion is conservative and nonstandard (§3.2, unnumbered main result: the rebound diffusion is nonstandard, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
An expression is derived characterizing the set of admissible rate pairs for simultaneous transmission of classical and quantum information over a given quantum channel, generalizing both the classical and quantum capacities of the channel. Although our formula involves regularization, i.e. taking a limit over many copies of the channel, it reduces to a single-letter expression in the case of generalized dephasing channels. Analogous formulae are conjectured for the simultaneous public-private capacity of a quantum channel and for the simultaneously 1-way distillable common randomness and entanglement of a bipartite quantum state.
This mission is the statement-level formalization of The capacity of a quantum channel for simultaneous transmission of classical and quantum information (arXiv:quant-ph/0311131v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: simultaneous capacity region and alphabet bound (Theorem 1: simultaneous capacity region and alphabet bound, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
4 results of the paper are not stated yet, because the library lacks an interface they need:
We present a generalized version of classical geometric invariant theory `a la Mumford where we consider an affine algebraic group acting on a specific affine algebraic variety . We define the notions of linearly reductive and of unipotent action in terms of the fixed point functor in the category of --modules. In the case that we recuperate the concept of lineraly reductive and of unipotent group. We prove in our "relative" context some of the classical results of GIT such as: existence of quotients, finite generation of invariants, Kostant--Rosenlicht's theorem and Matsushima's criterion. We also present a partial description of the geometry of such linearly reductive actions.
This mission is the statement-level formalization of Reductive and unipotent actions of affine groups (arXiv:1406.4446v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Extensions of subgroup translation actions and normalized twisted cocycles (Observation 5.4, equations (4)–(7), PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
45 results of the paper are not stated yet, because the library lacks an interface they need:
The concept of translation of an operator allows to consider the analogous of shift-invariant subspaces in the class of Hilbert-Schmidt operators. Thus, we extend the concept of average sampling to this new setting, and we obtain the corresponding sampling formulas. The key point here is the use of the Weyl transform, a unitary mapping between the space of square integrable functions in the phase space and the Hilbert space of Hilbert-Schmidt operators on , which permits to take advantage of some well established sampling results.
This mission is the statement-level formalization of Average sampling in certain subspaces of Hilbert-Schmidt operators on (arXiv:2011.05871v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §3, Eq. (3), unnumbered: average sampling of one-generator HS subspaces (§3, Eq. (3), unnumbered: average sampling of one-generator HS subspaces, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Paired-comparison data (which of two items a user clicked, which of two players won a game, which of two products a respondent preferred) are summarised by ranking scores, one real number per item. The Bradley–Terry model (Bradley and Terry, 1952) is the standard statistical model for such scores, and its parameters are estimated by maximum likelihood or by maximum a posteriori (MAP) estimation. The workhorse for both is the MM algorithm (minorize–maximize), systematised for the Bradley–Terry family by Hunter (2004); the MAP version with a Gamma prior is due to Caron and Doucet (2012).
Vojnović, Yun and Zhou (arXiv:1901.00150v3) give the first rate-of-convergence analysis of these algorithms that depends on the structure of the comparison data. They find that the classic MAP iteration can be arbitrarily slow when the prior is weak, and that a simple rescaling of each iterate removes the slowdown. This mission formalizes the rate of the rescaled MM algorithm, the paper's Corollary 4.2.
There are items. For , is the number of comparisons in which item beat item . The co-occurrence matrix has entries for and . Three quantities of enter the rate:
The parameter is , with item strengths , and item beats item with probability . The log-likelihood and the log-prior of independent priors on the are
The log-a posteriori function is , and the MAP estimate maximizes it. The MM algorithm maximizes, at each step, the surrogate , where
lies below and touches it at . The rescaling is with . It shifts all scores by a common constant so that . The rescaled MM algorithm (Algorithm 1) is with a maximizer of . Finally and .
If the MAP point , the iterate (an output of ) and the virtual gradient point all lie in , then
The milestones follow the structure of the paper:
Without rescaling, the MAP rate of MM (the paper's Corollary 3.4) is , and the paper shows this is tight on two items. For a weak prior, which is the usual choice in practice, convergence is therefore arbitrarily slow. The rescaled rate replaces by . It thus recovers, as , the maximum-likelihood rate governed by the algebraic connectivity of the comparison graph, at the cost of one normalisation per step. This explains the many-orders-of-magnitude speed-ups that the paper reports on real datasets.
The framework of §4.1 is stated for any objective, any surrogate and any map satisfying (F1), (F2), (P1), (P2). It applies to other generalized Bradley–Terry models (Rao–Kupper, Luce, Plackett–Luce) and to gradient descent. The results are proved on paper; none of them, and none of the Bradley–Terry objects, has a machine-checked proof that we know of. A formalization would also settle the points the printed statements leave implicit (see below).
The objective is not strongly convex with a useful constant on all of : its curvature in the direction comes only from the prior and is of order . The natural argument (strong convexity of gives a PL inequality, and the PL inequality gives a linear rate) therefore yields only the slow -dependent rate. The faster rate needs a PL inequality that holds only on the points where (Lemma 4.1). This uses the fact that the Hessian bound does not couple with its orthogonal complement. The rescaling must then keep every iterate in that set without decreasing .
All curvature bounds hold only on the box , because is unbounded. The MM step is compared with a virtual gradient step, and that step must stay in the box.
Parameters live in EuclideanSpace ℝ (Fin n) (items are 0-based); is the Euclidean norm and uses the sup norm. Counts are natural numbers and every sum runs over . Eigenvalues come from Mathlib's eigenvalues₀, and is by convention for . Gradients are Mathlib's gradient; the Hessian forms are second iterated Fréchet derivatives. The framework minimizes , exactly as the paper does.
The goal fixes these points, relative to the printed statement:
Theorem 4.2 is stated with rate ; the page prints , which does not match its own proof or Corollary 4.2.
The goal does not assume (F1), (F2), (P1) or the surrogate bound for . Those are milestones about the concrete model. Stating Corollary 4.2 with any of them as a hypothesis, or with or the MM step replaced by an abstract map, would be a different and weaker theorem.
A complete development needs, besides the model file, a descent lemma for functions with Lipschitz gradient on a convex set and the variational characterisation of of a symmetric matrix. It also needs Gershgorin's theorem and second-order calculus for log-sum-exp functions; these are reusable well beyond this mission. Proofs of any milestone, including the general Lemma 4.1 and Theorem 4.2 independently of the Bradley–Terry model, are welcome.
During an epidemic a government knows more about the severity of the disease than the public, and what it chooses to say changes how many people stay at home. Isolation is cheap for some and expensive for others. A person who cannot work from home loses income, and people facing different costs answer the same message in different ways. de Véricourt, Gurkan and Wang (ESMT Working Paper 20-03, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2021.4016) model this as a problem of information design (Bayesian persuasion, Kamenica and Gentzkow 2011). The receivers are a continuum of individuals who play a game among themselves, because each active person raises everyone else's infection risk.
The paper's main finding links economic inequality to misinformation. As the spread of isolation costs grows, the optimal policy exaggerates the severity of the epidemic less often and less strongly, and downplays it more. This mission formalizes that result, Theorem 2, together with the chain of statements on which its proof rests.
A unit mass of individuals each choose : isolate () or interact (). An isolated individual pays an economic cost , uniformly distributed on with mean and standard deviation , where . Write for the width of . An active individual pays the health risk . Here is the perceived infectiousness, the mass of active individuals and the healthcare cost of an infection.
A profile is a Bayesian Nash equilibrium (BNE) if, for every and every type , minimizes , where is the active population the profile induces.
The infectiousness is with ; it is high with prior probability , and the prior mean is . The paper also assumes . The government commits to an information policy , a law of messages given the state. Message moves the public to the posterior mean by Bayes' rule. For a weight on the economy, the government's cost is
An optimal policy minimizes over all policies and all their BNE profiles. On the binary message space the paper names four kinds of policy:
In equilibrium (Proposition 1), every type below the threshold isolates. The reduced cost at posterior mean is , and is its lower convex envelope on . The functions of (equations (23)–(25)) define thresholds for the ratio . Explicit rational functions of the parameters, and ((13)–(16)), are the second posteriors of the optimal exaggerating and downplaying policies.
Let , every other parameter fixed and admissible at both levels. Then
When exaggerating is optimal at both levels (, ), the exaggeration probabilities of optimal exaggerating policies satisfy
When downplaying is optimal at both levels (, ), the downplaying probabilities satisfy
The probabilities belong to policies that are optimal for the government's problem over all finite-message policies and BNE profiles.
Theorem 2 is the paper's answer to its question. Inequality in the economic cost of isolation pushes the government's message toward downplaying the epidemic, whatever weight the government puts on health. Theorem 1, the full characterization of the optimal policy, is a complete solution of a persuasion problem whose receivers play a congestion-type game, and Theorem 2 is a comparative-statics statement about that solution.
To our knowledge none of these results has a machine-checked proof. The mission produces:
The proofs in the paper are calculus on explicit functions, but they are long and contain sign slips. The proofs of Lemma 3 Parts C and D swap "convex" and "concave". The proof of Theorem 2 attaches the downplaying and exaggerating probabilities to the wrong -intervals. A closed form printed for in the proof of Lemma 2 does not equal its definition . A formal proof settles these points.
The obvious argument goes through the closed forms (17)–(18) of the optimal probabilities and differentiates them in . That argument needs, first, that the optimal policies are those forms. This rests on Theorem 1, the convex-envelope reduction and the curvature analysis of . The reduced cost is neither convex nor concave, and its shape changes across seven parameter regimes. Second, the derivatives of and in are rational expressions whose signs follow only from the regime bounds and . These bounds involve square roots. Third, the step from the equilibrium game to the reduced problem must handle the indifferent type and arbitrary BNE profiles, not only the threshold profile.
Params holds . The predicate Standing collects the assumptions of §2: , , , , and .Fin 2 (0 ). Message spaces are finite types; with a binary state, two messages suffice for the optimum.BiconvexProg.BranchBound.convexEnvelope.Theorem 2 must not be stated about the closed forms (17)–(18). It quantifies over policies that are optimal for (6), so a proof has to go through Theorem 1. The government's cost must also not be defined as , which would skip Proposition 1. A sorry-free check in the workspace exhibits two parameter pairs (one exaggerating, one downplaying) that satisfy the regime hypotheses of the goal at both inequality levels.
Contributions to every milestone are welcome. The general pieces are reusable beyond this paper:
Banks that can sell loans after origination may face different incentives to screen them before lending. A buyer that has invested in screening can inspect a seller's loan and buy it when its quality is high. That opportunity can make screening more valuable and reduce the equity a buyer needs to commit. At the same time, a seller may prefer to avoid the screening cost and rely on a later sale. Song and Thakor study when these two choices coexist in an interbank market, even though banks begin with the same opportunities and information (Song and Thakor, SSRN 3667175). The resulting question concerns the capital structure of banks and whether a trading market opens a region of heterogeneous behavior between two homogeneous regimes.
The paper's Proposition 2 is a result about this transition as the chance of a boom changes. It also compares the width of the heterogeneous region across market efficiencies. The mission formalizes that result from the authors' specified model and their preprint's assumptions. The preprint describes the paper as forthcoming in Management Science; the DOI record identifies the associated journal work.
A good loan pays at its final date. A medium loan pays in a boom and zero in a recession. Both require an initial investment . The probability of a boom is , with , so a medium loan is not creditworthy on its own. Before a bank screens, each type has probability one half. Screening costs and reveals the type. A bank can finance the loan with deposits and equity; supplying one unit of equity costs insiders per unit. Default also loses the bank its charter value . The paper restricts , and by Assumptions 1–4 and fixes the matching technology by Assumption 5 (preprint, pp. 7–12); is increasing and concave.
Without loan trading, the minimum screening equity is , the profit from screening is , and the profit without screening is . Their difference, , is the screening advantage. The paper writes each quantity as an explicit real-valued function of in equations (8)–(11). A cutoff separates the choices when the loan market is closed (Proposition 1, p. 15).
With trading, some banks can be buyers that screen, while others are sellers that do not. If buyers have mass and sellers mass , market tightness is . A seller meets a buyer with probability ; a buyer meets a seller with probability . Here measures matching efficiency. The buyer's bargaining weight is , and the price for a verified good loan is . Trading reduces the buyer's required equity to (Assumption 5, equation (13), and Lemma 1; the matching function follows Kiyotaki and Wright (1993)).
The main target is Proposition 2, p. 21. Under the paper's assumptions and its endpoint conditions, there are cutoffs . Every bank screens below ; none screens above ; between them, buyers and sellers coexist. In the interior the buyer/seller ratio is determined by
The two cutoffs solve the paper's equations (A4) and (A7). The mission also targets uniqueness of the equilibrium in every regime, expansion of the heterogeneous region when a larger feasible is used, and falling and as rises within that region. The milestone list covers the matching identities of Assumption 5, the Nash price (13), Lemma 1's equity threshold, the monotonicity of (footnote 19), the sign form of the cost condition (A1), the strict concavity of , the closed-market cutoff of Proposition 1, the two trading cutoffs (A4) and (A7), the interior indifference equation (A9)/(15), and the monotonicity in of the left side of (15) (Appendix A, pp. 34–37).
The result identifies a region in which banks that started alike choose different capital structures and screening decisions. A loan-trading market changes the relative payoffs of screening and not screening, and the boom probability determines which choice can survive a unilateral switch. The cutoffs show precisely where the market moves from all-screening to mixed behavior and then to no-screening. The market-efficiency comparison says when the mixed region widens. These distinctions matter for the paper's subsequent welfare comparison and its discussion of capital requirements (Song and Thakor, §§3–4).
The result is proved in the source paper. The remaining work is a machine-checked proof of the model-specific statements and their consequences, including the bargaining maximum, incentive threshold, cutoff existence and uniqueness, and comparative statics. The definitions are reusable for further formal work on the paper's welfare and capital-requirement results; this mission does not assert that those extensions have been formalized.
The equilibrium claim joins several regimes in one statement. The homogeneous corners are governed by whether a single bank would gain by changing its behavior, whereas the interior is governed by equality of buyer and seller profits. A root of the displayed equation alone does not establish an equilibrium: the cutoff and no-switch conditions must also hold, and the root must be unique. Moreover, the source's claimed global negative derivative for is not implied by its assumptions. The cutoff argument must therefore use a valid shape condition without importing that false assertion. The charter-value function is concave but otherwise general, so reasoning cannot rely on a particular polynomial example.
Lean represents all expectations by the closed-form real expressions in equations (7)–(15); there is no probability space. The parameter structure fixes , and . All five numbered assumptions remain explicit, including Assumption 4. The formalization reads screening cost and equity cost as positive, reads the paper's smooth as differentiable on , and requires for an open market. The bargaining price is optimized over . The buyer meeting probability uses its continuous value at . Proposition 1 uses a reduced closed-market outcome that records screening and equity; at its profit tie, footnote 21 selects no screening. The open-market equilibrium variable is the buyer share , with only in the interior; the all-buyer corner uses the sole-seller limit instead. Price and buyer equity are constructed from the paper's equations, and are never arbitrary choices. The cutoffs are required to satisfy , so all three regimes are nonempty; a version in which the equilibrium is any root of (15), or in which price or buyer equity are free variables, would be a different and weaker statement and is excluded. The hypotheses are jointly satisfiable, but only for small market efficiency (numerical searches find ); an explicit rational instance is checked in Lean.
The preprint prints a plus sign in (A6) where its preceding deviation inequality requires a minus sign; the Lean condition uses the latter. The paper also claims that the absolute sensitivity of to falls with , but that claim is false under its hypotheses, so the mission does not include either sensitivity clause of Proposition 2. The paper's unsupported global first-derivative bound for is excluded. The milestone from the proof of Proposition 5 states its displayed second-derivative identity wherever exists, and states strict concavity throughout the interval. Any further result should keep these corrections explicit. Contributions to the bargaining, real-analysis, and equilibrium lemmas are welcome; proofs of the milestone statements can then support the capstone theorem.
Rooftop solar changes both a household's electricity bill and the utility's cost of serving its customers. A tariff that encourages an aggregate amount of solar generation can still leave one customer tier paying more than before. Regulators therefore face a joint design question: can they induce a chosen adoption pattern while meeting the solar supplier's and utility's profit requirements and protecting every customer tier? Singh and Scheller-Wolf formulate this question for a solar company that sells generation through a power purchase agreement, a regulated utility, and households grouped into tiers. Their SSRN paper studies several tariff families; Proposition 5 identifies a tiered tariff that can implement the selected outcome and, when the customers' aggregate financial gain is nonnegative, avoid cross-subsidization.
The selected outcome is assumed to have been chosen for social welfare reasons. The result concerns the next task: implementing it through the tariff while customers decide whether to adopt and the solar company chooses its price. That distinction matters because a tariff that appears to allocate enough money to all parties may change the solar company's preferred price, and therefore change which households adopt.
There are finitely many customer tiers . Tier contains households. Each household has annual electricity demand , potential solar generation , and excess generation . If it adopts solar, it draws from the grid and sells back. The target adopting set identifies the tiers whose households install solar. Let be baseline utility demand, the target rooftop generation, and net utility demand. The paper restricts attention to outcomes with at least one adopting tier and (§3, pp. 10–11).
The regulator sets a tariff , a customer's utility bill based on grid draw , electricity sold to the grid , and adoption indicator . For tier , the two relevant bills are and . A solar company chooses a single price per unit generated by adopting households and pays unit cost when its sales volume is . Each customer adopts when its adopter bill plus is no larger than its nonadopter bill. With ties favoring adoption, this is , where . Thus the solar company's price determines both its sales volume and its unit cost (§§3–4, pp. 10–13).
The regulator's P2 objective is the largest increase in a tier household's cash outflow relative to the baseline rate . A nonpositive objective means no tier is financially worse off, which the paper calls cross-subsidization free. P2 also requires a specified solar-company profit and utility profit change . Write for the financial welfare improvement of the whole system and for customers' aggregate financial gain (§4, pp. 12–15).
Tariffs of type charge nonadopters and adopters , where is a common rate and a tier-specific adopter charge. The paper constructs one such tariff, , from the target outcome. At its prescribed price , the target tiers adopt, the solar company earns and earns strictly less at every other price, and the utility receives its specified profit change :
This is the feasibility claim of Proposition 5(a), p. 18.
When the aggregate customer gain is nonnegative, has a nonpositive P2 objective:
If a tier with the smallest demand does not adopt, Proposition 5(b) further says minimizes this objective among feasible tariffs. Both clauses belong to the combined goal theorem. The milestone list also includes the customer threshold, the welfare identity, the threshold formula, Proposition 5(a), Lemma 1, the retail-rate identity for , and the cross-subsidization clause (p. 18 and proof on p. S.3).
Proposition 5 gives a tariff implementation for any admissible target adoption set without relying on control of the solar company's price. Its equity guarantee has a clear limit: it requires nonnegative aggregate customer gain. Within the paper's family, the additional lowest-demand condition gives an exact minimax result for customers' bill changes (Proposition 5, p. 18). This distinguishes the existence of an implementing tariff from its distributional performance.
The mathematical result is already proved in the paper; this mission asks for a machine-checked development of its model, construction, and claims. The reusable pieces include finite-tier induced-adoption sets, price-dependent sales volume, and the accounting identities between company profits and customer outflows. The statements in this proposal are proof targets and do not claim an existing Lean proof.
Setting each customer's adoption threshold to produce is insufficient by itself. The solar company chooses to maximize profit, and a change in price can change both the adopting set and the unit cost . The prescribed price must beat every alternative real price strictly. The utility's required profit change constrains the same tier fees used to set thresholds. Finally, a nonnegative total customer gain does not by itself imply that every tier benefits; P2 asks about the largest individual tier increase. These coupled requirements are visible in the paper's P2 formulation and in the proof of Proposition 5 (pp. 13–14, 18, S.3).
Lean represents tiers by a finite type and outcomes by finite sets of tiers. All demands, prices, bills, costs, volumes, and profit changes are real. The tier type is unordered: the paper relabels tiers during 's construction. A tariff is represented by its two bills per tier, the evaluations P2 uses. For , fees are indexed by tier, consistent with the paper's statement that the utility can infer a solar customer's tier from grid draw (p. 17). Adoption ties go to adoption, and the solar company's price ranges over all real numbers. P2 feasibility includes the induced adopter set, the firm's unique best response, and the utility constraint.
The standing assumptions state , , nonincreasing , and . Positivity of is implicit in the paper and makes the displayed volume and price divisions valid. The target set is nonempty and satisfies . The utility's total generation cost is outside the household sum in its accounting constraint; this is the reading consistent with the paper's welfare identity. The printed indexing slips in (17) and (19) are avoided by expressing the induced equilibrium directly. Customer aggregate gain is computed from , rather than defined from the desired conclusion. The optimality quantifier covers feasible tariffs, the family studied in §4.3. Contributions may develop the equilibrium argument, the accounting lemmas, the rate identity, or the complete optimality proof.
A Nash equilibrium problem (NEP) asks for strategies of several players such that no player can lower its own cost by deviating while the others keep theirs fixed. NEPs model competition in electricity markets, environmental agreements, and the training of generative adversarial networks. When the players' problems are nonconvex, an equilibrium requires every player's strategy to be a global minimizer of a nonconvex problem, and even the special case of multilinear objectives over simplices is PPAD-complete (Daskalakis, Goldberg, Papadimitriou 2009). A second, less studied question is how to certify that a NEP has no equilibrium at all.
Nie and Tang treat NEPs in which all data are polynomials. They replace the equilibrium conditions by a polynomial system built from Lagrange multiplier expressions (Nie 2019), minimize a positive definite quadratic over it, and cut off candidates that are not equilibria. Their Theorem 3.3 states that for generic polynomial data this procedure stops after finitely many loops, either with an equilibrium or with a certificate that none exists. The paper also notes that a player problem (3.8) may have no minimizer, leaving the next cut undefined. This mission formalizes the finite loop bound and makes the attainment condition for an answer explicit.
There are players. Player chooses ; the joint strategy is , , and is with block replaced by . Player solves
with , and . Its feasible set is . A Nash equilibrium is a point with for all and all ; is the set of all of them.
Let be the polynomial matrix whose column is above , and . If a matrix polynomial satisfies , the multiplier expressions are . The set consists of the with
Algorithm 3.1 fixes a positive definite and cut sets . It repeatedly minimizes , , over the points of satisfying for all (problem (3.10)). If (3.10) is infeasible it reports that there is no equilibrium. Otherwise it tests the minimizer : it stops if is an equilibrium, and else adds to optimizers of for every player that can improve, and loops.
Generic data: fix degrees of in the block and degrees of ; the input is the vector of all coefficients, and a property is generic if it holds for all outside a Lebesgue-null set.
For positive degrees , for almost every , for all labels , all with and all positive definite :
At the end of every run, infeasibility of (3.10) implies while feasibility implies that (3.10) has a minimizer. If (3.8) attains a minimum for every player at every candidate in , each partial run extends to a terminal run within the same loop bound, ending with an equilibrium or a correct infeasibility report. This qualification corrects the paper's unconditional answer claim.
Theorem 3.3 is the termination guarantee for a method that computes Nash equilibria of nonconvex polynomial games and certifies their nonexistence; outside convex or special structured classes such guarantees are rare. Its two ingredients are of independent use. Theorem 3.2 bounds the loop count of a cutting-plane scheme by the number of KKT points that are not equilibria. Theorem A.1 is a generic finiteness result for multi-player KKT systems, the type of statement behind finite convergence of Moment-SOS hierarchies.
None of these results has a machine-checked proof. The mission provides a Lean model of polynomial NEPs, KKT points, multiplier expressions and nondeterministic algorithm runs, and a measure-theoretic notion of genericity for polynomial data, all reusable for the paper's companion results (Algorithm 3.7 for finding all equilibria, generalized NEPs).
The combinatorial part (Theorem 3.2) is short: each loop removes its candidate from a finite set. The difficulty lies in genericity. Milestone 7 needs Theorem A.1 for every sub-tuple of active constraints. Theorem A.1 is a dimension count in a product of projective spaces: the paper intersects a codimension- variety with determinantal varieties and argues through birational maps and generic hyperplane sections. Converting "codimension " into "finitely many points outside a Lebesgue-null set of real coefficients" requires showing that the bad coefficient set lies in a proper algebraic subset, and that such a subset is null. The naive route, a Bézout count, does not apply directly: the multipliers enter bilinearly and the system is not square in the usual sense when . Milestone 1 needs KKT necessity for mixed equality and inequality constraints under LICQ, derived from .
Step38Solvable requires a minimizer of (3.8) for every player at every point of ; under it, every partial run has a terminal extension that preserves its earlier candidates and cut sets.Monte Carlo tree search repeatedly chooses actions using estimates built from earlier simulations. The rewards attached to an action need not form an independent, identically distributed sequence: deeper parts of the search tree change as the search proceeds. Shah, Xie and Xu isolate this difficulty in a non-stationary multi-armed bandit and study a version of upper confidence bound selection with a polynomial exploration bonus. Their bandit theorem is the concentration result used in their subsequent analysis of tree search; it is a distinct finite-sample result with explicit assumptions and constants. Shah, Xie and Xu, §5–§7
The mission concerns Theorem 3 of arXiv:1902.05213v4, including both its expected-reward bound and its two-sided concentration bound. It provides the bandit foundation for the paper's later Monte Carlo tree search statements. The latter require a separate model of the search tree and are outside this mission. Shah, Xie and Xu, Theorems 1 and 3
A reward table has arms and random variables , where is the reward obtained on the th play of arm . Every reward lies in for a fixed . The arm's empirical mean after plays is , and the expectations of these means converge to . Rewards may depend on earlier rewards, including rewards from other arms. The model imposes no independence or identical-distribution assumption. Shah, Xie and Xu, §5, equation (12)
The per-arm concentration assumption fixes , , and . For every , both tails of beyond have probability at most . This describes each arm's complete reward sequence without specifying a filtration or a sampling law. The limiting optimal arm has mean ; each other arm has gap . Shah, Xie and Xu, §5, equation (13)
A run chooses arm at round . Its count records how many rounds through chose arm , and its average reward is . The polynomial UCB index is for , with . At round , the run maximizes the index formed using counts and bonus time . An unplayed arm has infinite priority, and ties among eligible arms are arbitrary. Shah, Xie and Xu, §5.1–§5.2, equations (14)–(16)
Theorem 3.A bounds the gap between expected run reward and the best limiting arm mean. With a positive lower bound for every , and , the target for is
The first term is the optimal arm's own finite-sample bias. The remaining term is explicit in the bandit parameters. Lemma 2 and the displayed decomposition on page 18 are the curated targets for this part. Shah, Xie and Xu, Theorem 3.A and §6
Theorem 3.B states that one constant , depending only on , bounds both tails for every admissible reward table, measurable UCB run, horizon , and :
The tuning parameter satisfies and . Lemma 1, the event inclusion (34), the play-count tail (36), and Lemma 3 are the curated targets for this part. The same theorem statement carries parts A and B. Shah, Xie and Xu, Theorem 3 and §6.1–§6.3
The expected-reward bound relates the run's finite-horizon mean to the optimal arm's own mean and to an explicit penalty for sampling other arms. The concentration bound says that the run's cumulative reward inherits polynomial two-sided tails at a derived exponent. Together these claims let the paper apply a bandit guarantee in its analysis of Monte Carlo tree search, where an action's reward process changes as the search continues. Shah, Xie and Xu, §6–§7
The result is proved in the cited paper; the mission seeks a machine-checked Lean development of that known result. Its reward-table model and finite-sample count estimates may be reused when a sequential choice rule is analyzed without independent arm rewards. The mission currently provides compiled definitions and theorem statements as proof targets, not verified proofs of those targets.
A standard stationary-bandit analysis would replace each arm's history by independent draws from a fixed law. Here the assumptions give only convergence of expected arm means and polynomial per-arm concentration. A run also samples arms adaptively, so the random number of observed rewards on an arm cannot simply be inserted into a fixed-sample tail inequality. The finite-sample guarantee has to retain the exact dependence on the bonus, arm gaps, pull counts, and the tuning window. The paper's intermediate results identify the required count and tail statements. Shah, Xie and Xu, §6.1–§6.3
Lean uses a probability space , a table , and a run . Play numbers begin at one; index zero is unused. The model makes reward measurability, boundedness, limiting expected means, and both concentration inequalities explicit. The run requires measurable arm-selection events so that its probabilities and bounded expectations are genuine. The model does not add independence, an identical-distribution condition, or a filtration.
The real index is compared only when every arm under comparison has a positive count; a separate clause gives unplayed arms the paper's priority. The time argument of the index at round is . The thresholds and use the paper's closed ceiling formulas. The paper's is represented by a positive lower bound on all suboptimality gaps; setting recovers the printed statement when that minimum is defined. Theorem 3 explicitly requires and . The existential precedes the probability space, rewards, run, , and , so it cannot change with an instance or horizon. Both parts of Theorem 3 are present, and the model's hypotheses are satisfiable for ordinary bounded bandits.
The mission needs reusable definitions for reward tables, empirical and run averages, pull counts, measurable runs, UCB selection and polynomial play thresholds. Contributions proving the six curated milestones, connecting them to the goal, or establishing reusable measurability and finite-sum facts are in scope. The pathwise two-sided reward decomposition is also posed as a supporting theorem.
Sequential packing matters when an item's size is known statistically before placement but revealed only afterward. A connection request has uncertain bandwidth, a shipment has uncertain final weight, and a virtual machine has uncertain resource use. In each example, exceeding capacity can have a separate cost from opening another container. Perez-Salazar, Singh, and Toriello formulate this as adaptive bin packing with overflow and analyze policies that respond to observed sizes without seeing future outcomes (paper, §1.1–1.2).
The paper's i.i.d. result gives a fixed numerical guarantee for a simple online rule, even against the best adaptive policy that knows how many items will arrive. This mission formalizes that theorem and the policy comparisons on which its statement depends. The source is the pinned preprint arXiv:2007.11532v2; all page and result numbers below refer to that version.
There are items with independent, nonnegative random sizes . Each bin has unit capacity. Before placing item , a policy knows its distribution and the realized sizes and assignments of earlier items, but it does not know . Its choice is irrevocable. A bin becomes unavailable after its accumulated load becomes strictly greater than one. Opening a bin costs one, and breaking a bin adds penalty . A policy here is deterministic, nonanticipative, measurable, and feasible: it never puts an item into an already overflowed bin (paper, §1.2 and §3.1).
Let count bins opened by policy , and let count bins whose final load exceeds one. The policy's objective is
For a bin with current load , placing item incurs overflow risk . The risk of a bin is the sum of these quantities over items assigned to it. A policy is risk-budgeted at level if every bin's risk is at most . These terms are properties of the realized history before each assignment, not substitutes for the actual count .
Budgeted Greedy, the paper's Algorithm 1, uses risk budget with . At a round it considers an opened bin if its load is at most one and the new item's risk would keep total risk within the budget. It uses an eligible bin if one exists and opens a new bin otherwise. The paper leaves ties arbitrary; the formal rule chooses the lowest indexed eligible bin. When an item has , it cannot fit the budget even in a fresh bin. The algorithm still opens a new bin for it, so a separate heavy-item case is needed in the performance theorem (paper, §3.2 and Theorem 4.4).
The central target is Theorem 4.4, also stated in Theorem 1.2. For i.i.d. nonnegative items and , Budgeted Greedy is an admissible policy and, for every admissible policy ,
The comparison with every is deliberate. The paper explains that an exact minimizer need not exist for continuous distributions; its notation includes arbitrarily good approximations. The universal inequality therefore expresses the same guarantee without presuming that an optimum is attained (paper, p. 8 and Theorem 4.4).
The milestone list follows the paper's stated intermediate results. Proposition 3.1 identifies expected broken-bin count with expected accumulated risk. Lemma 3.4 and Corollary 3.5 turn the risk budget into an expected cost bound. Theorem 4.1 states that every policy has a controlled-cost counterpart that isolates high-risk items and budgets every other bin. Lemma 4.3 compares the expected bin openings of Budgeted Greedy with all budgeted policies for i.i.d. items. The heavy-item estimates are taken directly from the proof of Theorem 4.4. An initial milestone states that the online algorithm actually induces a policy (paper, pp. 4, 8–14).
The theorem supplies an explicit bound for an online packing algorithm when overflow has a monetary penalty. Its comparator may adapt to past observations and know the finite horizon, so the guarantee concerns a strong benchmark rather than a fixed packing plan. The structural milestones are also useful separately: the risk identity describes how individual placement probabilities account for broken bins, while Theorem 4.1 connects arbitrary policies to the risk-budgeted class (paper, Theorem 1.1, Proposition 3.1, Theorem 1.2).
The mathematical result is proved in the cited paper. This mission supplies Lean statements and definitions but does not claim machine-checked proofs of the milestones or the goal. A completed development would give a reusable interface for adaptive bin assignments, product laws for independent sizes, measurable policy costs, and per-bin risk accounting. Those definitions could support later statements about other distributions or packing rules from the same paper.
An item's overflow event is revealed after its bin has been chosen, while the bin choice can depend on all earlier sizes. Consequently, multiplying an unconditional overflow probability by a simple occupancy count does not directly give the cost: the assignment and current load are random. The risk identity must account for this dependence. The comparison with an arbitrary adaptive policy is harder because that policy can interleave work across bins, whereas Budgeted Greedy follows a narrower budget rule. The i.i.d. assumption supports the expected-opening comparison, but does not make the random policy histories disappear (paper, §§3–4).
Items and bins are Fin n, indexed from zero. This provides at most bins, enough for a sequence of items. The item laws form a product probability measure on real-valued outcome vectors; nonnegativity is a separate support hypothesis. In the i.i.d. statements every coordinate uses one law . A bin breaks at load , not at equality. The algorithm's risk test uses the exact real probability of . All costs are integrals of the bin-opening and bin-breaking counts, rather than definitions in terms of risk.
The model makes policy measurability explicit so these real integrals do not acquire Lean's default value for nonintegrable or nonmeasurable inputs. Policy feasibility is required on every outcome vector, including vectors outside the nonnegative support; this is a chosen extension of the paper's reachable-history convention. The model also fixes a lowest-index tie break. Algorithm 1 line 3 omits the load-at-most-one test stated in its preceding prose; the formal algorithm includes it. Lemma 4.3 is stated under , the condition needed for Budgeted Greedy itself to be budgeted and the case in which the paper uses that lemma. These choices are disclosed in the item descriptions and moderation notes (paper, pp. 9–10, 13–14).
The representation must retain the two actual random counts and ; defining cost from the risk sum would erase Proposition 3.1's content. The finite indexing, product measure, measurable sets, and Bochner integrals use Mathlib. Useful contributions include proofs of policy measurability, the per-bin expectation identity, the risk-budget comparisons, and the final approximation bound.
In reinforcement learning, each policy update may require new interaction with an environment. When interaction is costly, an optimizer can retain past trajectories and use them again, provided it corrects for the different policy that generated them. Lin, Wang, and Zhou study this idea for natural policy gradient, using importance weights to reuse earlier state-action samples. Their rate result identifies how reuse changes the covariance of the optimization error, rather than measuring progress solely by the number of iterations. The result appears as Theorem 2 of their 2025 preprint, subsequently published in Operations Research.
The question is subtle because the reused data are correlated with the sequence of policies. A fresh sample drawn at iteration has the current occupancy distribution, while an old sample was drawn under an earlier policy and receives a likelihood ratio that depends on the current iterate. The inverse Fisher-information estimate adds another random factor. The covariance therefore has separate terms for gradient sampling and for the interaction between gradient sampling and the inverse-information estimate. The paper's §4 and Theorem 2 quantify both.
A discounted Markov decision process has states , actions , transition probabilities , rewards , an initial-state law , and a discount factor . A parameter specifies a stochastic policy . Its objective is the expected sum of discounted rewards. The discounted occupancy distribution is the probability of observing when the time is geometrically distributed with parameter . It is this distribution, rather than the one-step transition law, that supplies the algorithm's samples.
At each iteration, the method draws state-action pairs from . Its gradient estimate combines the current batch with earlier batches. A reused pair from iteration is weighted by . The preconditioner is the inverse of a regularized empirical Fisher information matrix. The iterate moves in that preconditioned gradient direction and is projected back onto the feasible set . The source's equations (3)–(6) and Algorithm 1 define these operations; the paper fixes reuse to the gradient estimate alone for its convergence analysis in §3, p. 7.
Write for the single-sample policy-gradient contribution, for the score outer product, for the mean regularized inverse Fisher estimate, and for the covariance of . The two matrices governing the rate are
where averages over a fresh Fisher batch. All three matrices are derived from the MDP and policy; none is supplied as a free covariance parameter.
Suppose the RNPG iterates converge almost surely to , the paper's regularity and step-size conditions hold, and the linearization of the mean natural-gradient field at is a Hurwitz matrix . For the normalized error , the goal is the marginal central limit conclusion of Theorem 2, p. 11:
Here stacks matrix columns and is the Kronecker sum. The milestone list follows Lemmas 4–8 and display (10), pp. 12–13: three conditional covariance limits for the fresh-gradient and random-preconditioner terms, their combined covariance, then two limits for the fixed-state memory process. The formulas retain the paper's factors , , , and .
The limit law gives a quantitative description of the parameter error when the step size is small: the covariance is to first order. In the noise matrix, the contribution is divided by , exposing the benefit of reusing gradient samples under the paper's assumptions. It also recovers the single-batch regime at , where the memory terms vanish. These are claims about the algorithm's asymptotic statistical behavior, not guarantees that every finite run improves.
The paper proves the theorem analytically. This mission presents Lean statements and definitions; the open task is to give machine-checked proofs of those statements. A completed development would supply reusable finite-MDP occupancy and importance-weighted sampling interfaces, plus conditional-moment tools for stochastic approximation with finite memory. The marginal convergence claim is the goal; the source's additional process-level weak convergence to a stationary stochastic differential equation remains outside this mission.
Treating the gradient batches as independent at every iteration gives the wrong covariance. An old batch appears in several successive estimates, and each reuse weight depends on the changing policy. Even the random inverse Fisher estimate cannot simply be replaced by its mean inside a covariance. The paper distinguishes the conditional fluctuation from the term carried by the stored history; the two have different limits, and a cross term survives in the accounting. The required result is a joint limit over a late starting time and a long averaging window, not a one-step variance calculation. This dependence is the central obstacle for the milestone chain in §4 and Appendix A.7–A.11.
Lean uses finite, nonempty state and action types with discrete measurable structures, real rewards and parameters in a Euclidean space of positive dimension. All state-action and batch expectations are finite weighted sums. The objective itself is the unnormalized infinite discounted return from equation (1); occupancy is normalized. The policy family is defined on all of , while the bounds in Assumption 1 are imposed on . The theorem additionally requires : at a boundary limit a projected iterate can have a one-sided normalized error, contradicting a nondegenerate centered Gaussian. The paper discusses the interior case just below Assumption 2 on p. 10.
The run draws separate independent gradient and Fisher batches, realizing Assumption 1(A.1.7). Before batches exist, its gradient estimate averages all batches available. A general filtration records the past; conditional matrix expectations are taken entrywise. The fixed-state lemmas condition on a stored-memory process whose future batches follow the occupancy law at fixed . The finite model writes the distributional continuity of Assumption 2(A.2.4) as pointwise continuity of the finite sample functions. The complete process-level SDE claim of Theorem 2, the separate almost-sure convergence Theorem 1, and the numerical examples are not formalized here.
The covariance matrices and limit law are computed from the policy, MDP, and RNPG run. An arbitrary covariance inserted as an extra hypothesis would erase the paper's main claim. Work on the published goal and the six paper-indexed milestones is welcome, as are supporting results for occupancy positivity, score identities, conditional expectations, and finite-memory stochastic approximation.
A standard-essential patent is a patent that an implementer must use to make a product compliant with a technical standard. Its owner may demand a royalty from firms using the standard. Whether a patent is truly essential can be disputed, yet licensing offers and investment decisions are made before a court resolves that dispute. Standard-setting organizations can commission essentiality checks that certify patents before licensing. Better checks identify more patents that are not essential, but they also change what an implementer believes about a patent that passes the check. Schuett and Wipusanawan study how those two effects interact with litigation and research investment in their TILEC discussion paper, §§2–5.
A common policy intuition is that a more accurate check should save litigation costs by excluding weak patent claims. The paper identifies a countervailing effect in a model where an innovator chooses research effort before it knows whether its patent will be essential. The question here is local: when a small increase in check accuracy leaves each state's licensing regime unchanged, how does equilibrium welfare change if the patent owner faces no effective cap on royalties? The paper's Proposition 1 answers this question, building on its licensing, investment, and welfare formulas Schuett and Wipusanawan, pp. 16–25.
An upstream firm chooses research effort at cost . Research succeeds with probability . Following success, the standard uses the firm's technology, its patent is essential, and the commercial value is one of finitely many values with probabilities . Following failure, the standard uses a status-quo technology, the patent is not essential, and value occurs with probability . The separate distribution for the unsuccessful upstream technology enters the paper's assumption that the status quo has higher expected value than that technology. The model requires Assumption 1, p. 10.
An essentiality check certifies an essential patent correctly. It also certifies a non-essential patent in error with probability , where is accuracy. After observing certification and value, the upstream firm offers a royalty fraction bounded by . The downstream firm can accept or litigate. Litigation costs each firm ; the court determines essentiality correctly. A non-certified patent earns the upstream firm no licensing revenue in this model. The paper assumes Assumption 2, p. 12.
A certified patent can produce a hybrid licensing outcome, in which the unsuccessful firm sometimes offers a low royalty and the downstream firm sometimes litigates a high offer, or a pooling outcome, in which both types offer the maximum royalty. Write and for the sets of states with those outcomes. The implementer's belief that a certified patent is essential, , depends on expected effort , accuracy , and the value distributions. In equilibrium, . The paper derives a private investment wedge from the difference between expected licensing revenues after success and failure, and a social wedge from expected value less both parties' litigation costs equations (1)–(7), pp. 16–22.
The main target is Proposition 1. With an ineffective royalty cap, , fix where no positive-probability state lies exactly at the hybrid–pooling boundary. Along a continuous path of nearby equilibrium efforts , the right derivative of welfare satisfies
The inequality is weak because the paper concludes Proposition 1 and its proof, pp. 24–25. The target concerns a marginal increase that preserves the licensing regimes; it makes no claim about a large change that moves states between and .
The milestone statements cover the regime condition (4), the private revenue wedge (5), the welfare identity (6), Lemma 2's positive response of research effort to accuracy, and Lemma 3's comparison of private and social investment incentives. Their order exposes the quantities the goal uses without replacing Proposition 1 with a narrower fixed-regime statement.
Within this model, the result says that improved screening can lower welfare when unconstrained licensing already induces too much research investment. It identifies a limit on an intervention aimed at reducing disputes over essentiality: even a check that detects more non-essential patents may change the incentives of firms whose patents pass. This is a statement about the model's local equilibrium, not a claim that every real-world checking program lowers welfare. The paper separately examines changes large enough to alter licensing regimes and the case of an effective royalty cap Schuett and Wipusanawan, §§5–6.
The economic theorem is proved in the cited paper. This mission asks for a machine-checked account of its finite-state model and the local welfare claim; the displayed Lean statements are open proof targets. The shared definitions of certification beliefs, licensing outcomes, revenue, and welfare are useful for checking later variants of the model, including alternative certification errors or royalty caps. No machine-checked proof of this paper's proposition is claimed here.
The local comparison crosses three choices. Accuracy changes the chance that a failed innovator is certified. Certification changes the downstream firm's belief when it sees a high royalty. The resulting licensing outcome affects the innovator's incentive to invest, and effort feeds back into the belief. Simply holding effort fixed misses the welfare effect in Proposition 1. Treating the hybrid and pooling sets as fixed for all accuracy levels is also too broad: the paper restricts the result to a neighborhood where the regime condition does not meet equality. At a boundary, the relevant formulas can switch and the local derivative need not have the same form pp. 20, 24–25.
The Lean model uses real values and probabilities on a finite state type Fin n. Each of , , and is a nonnegative probability vector. Assumptions 1 and 2, , and the paper's increasing convex research cost with and as are explicit standing conditions. The cost is represented by a real function twice continuously differentiable on , which covers the effort domain below one. Equilibrium effort is interior and satisfies the private first-order condition with the implementer's belief equal to effort.
Three premises used in the paper's argument are made explicit. Litigation costs satisfy . The second derivative at the equilibrium effort satisfies , as required by the displayed denominator in Lemma 2; convexity alone gives only nonnegativity. A right-continuous equilibrium-effort path supplies nearby equilibria for the local comparison. The derivative is one-sided because the target concerns an increase from , including . Strictness of the regime condition is demanded only for states with positive probability under or ; an absent state cannot affect welfare or investment.
The belief formula is the paper's ratio when its denominator is positive. Its value at a zero-probability state is immaterial to the weighted outcome; the regime milestone also gives a cross-multiplied condition there. Uncertified patents give the upstream firm zero revenue, and the downstream firm retains value without litigation. Welfare is assembled from the two firms' payoffs in every certification and licensing outcome, then related to equation (6). Defining welfare directly by (6), fixing in the goal, or assuming the derivative of would remove the main work of the proposition. Contributions to the finite-state payoff model, the regime and welfare identities, and the local derivative and wedge comparison are all within scope.
Multistage stochastic optimization chooses a sequence of decisions while information arrives over time. A decision at time may depend on the observations available by then, but not on later outcomes. That information restriction, called nonanticipativity, links decisions across scenarios. Dual variables for it are useful because they express how an information constraint affects the optimum and because they lead to conditions that can be checked scenario by scenario. The paper studies this question for convex objectives on spaces of random variables broad enough to include strategies without integrability restrictions. Earlier duality models often worked on a smaller space or required multipliers in a full topological dual whose elements are not always random variables. Pennanen and Perkkiö, 2022 ask when the dual optimum can instead be attained by random-variable multipliers.
The distinction matters even if the two dual problems have equal values. A strong dual solution can include a singular functional that cannot be expressed as integration against a random variable. A numerical or economic interpretation of a dual multiplier usually needs the latter representation. The paper's result therefore includes both equality of values and actual attainment in the ordinary dual. Its final optimality condition concerns the original problem over all adapted measurable strategies, not merely the locally convex space used to construct the dual.
Let be a probability space with a finite filtration . A process is adapted when each is measurable using information at time . Write for the linear space of adapted processes. The objective is the integral of a convex normal integrand : each scenario has a closed convex extended-real objective, and the epigraphs vary measurably with the scenario. The paper assigns to the integral when the positive part is not integrable. A fixed random parameter gives the original problem : minimize over . These conventions and the model are stated on pages 1–3 of the pinned preprint.
For duality the paper uses locally convex spaces and of random variables, with and . The associated problem minimizes over . Its value function allows the nonanticipativity constraint to be shifted by . The spaces and are solid and decomposable, and they pair by expected dot product with random-variable spaces and . Strong Fréchet topologies give larger topological duals and ; each splits uniquely into a random-variable part and a singular part.
The ordinary dual maximizes over and . Here integrates the pointwise conjugate , while consists of members of annihilating every adapted element of . The strong dual maximizes over the full topological duals. Their distinction is the central object of the mission.
The goal is Theorem 27 on page 20. Under Assumption 23 and closed linearity of , it gives
and an attaining pair in . Assumption 23 has two parts: the positive hull of is a closed linear space, and a feasible point can be replaced by another feasible point whose coordinates through time equal their conditional expectations. The paper's displayed formula repeats “” in the second position; the distinct restricted problem defined on page 2 supplies the reading used here.
For a feasible adapted strategy with finite objective, the goal also identifies primal optimality with a dual feasible pair satisfying
The supporting targets are Lemma 13, which separates the regular and singular pieces of an approximate integral-functional subgradient; Theorem 18, which establishes strong dual attainment; Lemma 24, which controls a support function after conditional expectation; Theorem 25, which supplies ordinary dual variables; and Theorem 26, which compares the two dual values and their attainment. Theorem 14's conjugate and subgradient formulas are included as a supporting theorem item, with its lower-semicontinuity equivalence left outside this mission.
The equality between and says that constructing duality in the locally convex space has not changed the value of the unrestricted adapted problem. Equality with and attainment then provide actual random-variable multipliers rather than only a supremum or singular dual solutions. The pointwise subgradient condition converts an optimality claim about a coupled stochastic program into conditions on the scenario integrand. These are the consequences asserted in the source's Theorem 27.
The result is proved in the source, but this mission's Lean statements are open proof obligations. A completed development would add a reusable treatment of convex integral functionals with extended-real values, singular dual decompositions, adapted almost-everywhere classes and support functions under conditional expectation. The definitions are shared across the goal and milestones so that a proof of one result addresses the same objects used by the others.
Strong duality alone does not supply the ordinary dual variables. The strong topological duals may contain singular functionals, so an optimizer of need not lie in . The source must show that under Assumption 23 those singular components can be removed without worsening the dual objective. Conditional expectation interacts with the time structure of a process and the domain of ; this is where a direct appeal to an abstract convex-duality theorem stops short of Theorem 27. Separately, the original primal problem permits adapted strategies outside , so its value cannot be identified with by definition.
Lean represents random variables as classes modulo almost-everywhere equality. Each Euclidean process block is flattened to coordinates indexed by a finite type, with a time stamp recording its filtration stage. Adaptedness means that every coordinate has an -measurable representative. Strong topologies live on the types and embedded into those classes; the regular dual partners remain submodules of random-variable classes. The setting explicitly states their Fréchet properties, solidity, decomposability, separating pairings, integrability of pairing products, and unique regular–singular dual decompositions. Continuity of each regular pairing expresses the source's Mackey-strength condition. Conditional expectation closure is a separate section-four hypothesis.
Primal and dual values, conjugates and support functions take values in the extended reals. The ordinary dual uses the integral of the pointwise conjugate and ranges over ; ranges over all adapted measurable classes. Thus neither problem can become true merely by restricting to or redefining the ordinary objective with . The positive-part integral convention uses the previously published expectation definition.
Two source qualifications are recorded in the formal statements. The proofs of Lemma 24 and Theorems 25–27 need proper and lower semicontinuous in the strong product topology, as Theorem 18 states. In the forward direction of Theorem 27's optimality equivalence, is also required: with value , primal optimality need not give a finite pointwise subgradient. The reverse direction has no such added guard. These repairs and the duplicated “” display are documented in the mission notes.
Bundle methods minimize a convex objective while using local supporting affine functions to represent a component that may be nonsmooth. Their iterations can spend time improving the model without moving the current proximal center, so a bound on useful center changes alone does not bound the total work. Liang and Monteiro study a common generic proximal bundle (GPB) framework for several model update rules and give one explicit iteration bound that covers every rule admitted by its bundle update blackbox. The result is a proved theorem in their paper, rather than an open complexity conjecture.
The framework matters when a convex objective combines a component supplied through subgradients with another component whose proximal subproblems can be handled directly. One-cut, two-cut, and multiple-cut bundle updates fit the same abstract requirements in the paper. A common statement makes their guarantees comparable without identifying a specific update formula as canonical.
The problem is to minimize hybrid convex composite objective over . The effective domain is nonempty and contained in the domain of . The function is lower semicontinuous and -convex, for : its convexity inequality gains the quadratic term . For each , a chosen subgradient defines a supporting affine cut
The hybrid oracle condition allows both a constant and a distance-dependent part:
where . For tolerance , the pair minimizes among all nonnegative pairs satisfying the same condition. An optimal point nearest the initial point exists under the paper's assumptions, and .
A GPB run is an infinite sequence of points , best-so-far points , centers , and convex bundle models . At a serious update, the next center is the current point and the next model lies between and . At a null update, the center stays fixed and a bundle update blackbox selects the next model. Its output must dominate a mixture of a fresh cut and an auxiliary model that agrees with the previous model at and has as its proximal minimizer. Every new minimizes its model plus the squared distance to its center divided by . The best-so-far point minimizes the observed objective values. The gap compares with the proximal model value; a step is serious when .
The goal is Proposition 4.9, an explicit total iteration bound for every run admitted by GPB when is set by equation (38). Put and
There is an index with and
Here is the minimum of the two serious-iteration expressions in (61), with the paper's limiting convention at . The milestones follow the two quantities in this product: Corollary B.2 and Lemma 4.2 yield the serious-iteration estimate; Proposition 4.3 packages it. Equation (7), Lemmas 4.6, A.3, and 4.7 bound the behavior within each cycle; Proposition 4.8 bounds the cycle length. The goal combines the two bounds without selecting one concrete bundle update.
The theorem gives a finite tolerance certificate with a numerical bound on all iterations, including those that only improve the bundle model. The bound depends on the oracle parameters, curvature, initial distance to the solution set, tolerance, and proximal stepsize. It therefore states what an implementation gains by satisfying the BU conditions even when its internal model construction differs from another implementation. The broader paper also analyzes particular update schemes and an adaptive method, but the target here is the common GPB result Liang and Monteiro, §3–4.
The mathematical result is already proved in the source. This mission asks for machine-checked definitions and proofs of its explicit bound and the selected supporting statements. No machine-checked proof is supplied by these open theorem items. The definitions of the hybrid oracle, proximal model, and abstract GPB run can be reused to formalize the paper's concrete update schemes later.
Counting serious steps does not count intervening null steps. A null step can leave the center fixed while the model changes, and the BU condition permits many such models. The main obstacle is to obtain a uniform bound for a complete cycle from conditions that are local to one model update. The separate analytic obstacle is the hybrid descent estimate (7): the oracle bound contains both a constant term and a term proportional to distance, and the needed quadratic coefficient is , not the easier . The source's auxiliary proximal displacement estimate also depends on lower semicontinuity so that its minimizers exist.
The Lean space is EuclideanSpace ℝ (Fin n), with its usual norm and real inner product. The function domain stands for ; , , and each bundle model are real-valued on , with an extended value off when lower semicontinuity is stated. All model inequalities and proximal minimizations are over . This represents the paper's extended-valued functions without ambiguous arithmetic at . The selected subgradient inequality is also required only on . The source's lower semicontinuity of and of the BU auxiliary model is omitted, which strengthens the resulting claims; lower semicontinuity of and of each generated model remains. The abstract serious-iterate sequences explicitly keep their auxiliary points in .
Index zero is initialization and counts as serious because ; subsequent indices are natural numbers. The GPB run predicate retains the existential auxiliary model in every null update, so it covers every admissible variant. The goal concludes existence of a successful bounded index. It assumes so equation (38) defines . For , the serious-step formula uses the limiting value rather than real division by zero. The printed cycle and total bounds omit an integer rounding and can be too small; the formal targets use a ceiling and a nonnegative logarithm. Lemma 4.2(c), Lemma A.3, and Lemma 4.7 carry the additional qualifications needed by their printed proofs, disclosed beside their statements.
The development needs Mathlib's finite-dimensional Euclidean spaces, convexity, lower semicontinuity, and real logarithm, plus real-sequence and finite-index estimates. Contributions proving the milestones, the goal, or reusable facts about the GPB model are within scope. A proof for one fixed update formula alone does not establish the goal over the BU blackbox.
Retirement timing is an optimal stopping decision: continuing work earns income but incurs labor cost, while stopping removes both. In the investment model of Jang, Xu and Zheng, the decision also interacts with asset returns and with consumption of basic and luxury goods. The paper separates the retirement decision from the individual's utility specification by moving to a dual state. The resulting free boundary says which dual states favor immediate retirement. A rigorous account of that boundary is useful whenever one wants to compare retirement timing across income, labor-cost or market scenarios without solving a new utility-specific stopping problem.
This mission concerns the near-terminal shape of the boundary in the arXiv:2008.00392v2 version. The paper states that the boundary increases as mandatory retirement approaches and converges to the contemporaneous ratio of labor cost to income. Its printed argument shifts time in a differential operator that the model permits to vary with time. The target below includes the additional condition that makes that shift valid. The original time-dependent claim is therefore not represented as an unconditional theorem.
There are risky assets and two horizons: the mandatory retirement age and a later consumption horizon . The deterministic coefficients on are the interest rate , discount rate , income , labor cost , excess-return vector and volatility matrix . The market price of risk solves . The scalar coefficients and each component of are positive, continuous and bounded; is continuous and uniformly elliptic in the sense that is bounded above and below by positive multiples of the identity. These are the standing model assumptions on p. 7, supplemented by the relation defining on p. 12 of the source.
For a dual state at time , let solve the dual state equation
The noise term is represented by the scalar process . Its increments are independent of the past and Gaussian with variance . These properties determine the stopping model used here.
The dual stopping value is the largest expected discounted net gain from continuing until a stopping time :
This is equation (26), started at , with the absolute-time discount in equation (25). On , the retirement region is and the working region is . The free boundary is , with .
Proposition 16 describes the two regions by and , and says that higher income or lower labor cost lowers the boundary. Proposition 17 gives the preterminal bound
The proof-level milestones state that is nondecreasing in and, under the aged-window conditions below, nonincreasing in . These statements follow the labels and proof passages in the source, pp. 17 and 39–40.
Assumption 18 fixes an aged interval , where , and asks
The corrected goal also asks that and be constant on that interval. It then states that is nondecreasing there and
The left limit is essential: under the paper's empty-set convention, even though the limit from earlier times is finite.
The boundary turns a stopping-time optimization into a time-and-state decision rule. The upper bound and the terminal ratio supply observable scales for that rule. The comparative-statics statement identifies the direction of change when income rises or labor cost falls while the investment environment stays fixed. Near , the goal says that the threshold moves monotonically toward a ratio involving only the two labor coefficients, despite the stochastic dual state. These are the retirement-region claims of Propositions 16–17 and Theorem 19.
The paper presents analytic arguments for these results; this mission asks for machine-checked Lean proofs of the stated stopping-model claims. The current draft contains definitions and open theorem statements, not verified proofs. It also records two corrections explicitly, so that a future proof cannot silently rely on the false terminal endpoint of Proposition 17 or on time invariance absent from the printed Theorem 19.
The boundary is an infimum of a strict-positive-value region rather than an explicit formula. Showing monotonicity of the value alone does not automatically settle the boundary at points where the value is zero, and a limit of the boundaries needs control of behavior close to the terminal time. The time-dependent generator is a separate obstacle: changing the starting time also changes the future drift and volatility schedule, so the printed time-shift comparison is unavailable without a condition that fixes the generator on the aged interval. Stopping-time suprema add measurability, integrability and finite-value obligations before any order comparison is meaningful.
Time and the dual state are real-valued. The market has finitely many assets, ; the retirement horizon is strictly before the coefficient horizon . Income and labor cost are positive, so is defined throughout the relevant interval. The deterministic -dimensional Wiener integral is encoded by a continuous adapted scalar process with independent Gaussian increments of variance . This retains the law and filtration properties the stopping value uses.
The value is the stopping representation of (25)–(26), not the Sobolev/PDE definition (24). The two differ only through the paper's identification of those formulations. Appendix F's discount from instead of zero is a positive rescaling and leaves the zero regions and boundary unchanged. Each stopping payoff is required to be integrable within the value's defining set; for the paper's bounded coefficients and lognormal state this is expected for every admissible stopping time. The supremum is taken over actual admissible stopping times and is nonempty because immediate stopping gives zero. Its upper bound is finite under the same model. The formal proof must establish these facts rather than exploit a default value of a real supremum.
The boundary takes values in the extended reals so an empty working set gives . The additional constancy of and on appears only in the corrected Theorem 19 and its time-comparison milestone. Assumption 18 uses derivatives within that closed interval, including one-sided endpoint derivatives. The paper's utility and wealth-control layer, the verification theorems, and the variational-inequality comparison theorem are outside this stopping-model mission. Reusable contributions include the Gaussian-increment model, integrability and boundedness results for the stopping value, and general facts about thresholds formed from positive-value regions. The claim cannot be discharged by assigning a convenient boundary or by restricting to a constant stopping time: is computed from the full stopping-time supremum.
Large language models answer reasoning questions better when they are allowed to write out a chain of thought (CoT) before the final answer, but every generated token costs time and money. A large body of recent work therefore asks models to "think less": prompts such as "be concise" or "use at most 10 words", and training methods that shorten the reasoning trace. These methods trade accuracy for length, and the natural question is how good such a trade can possibly be.
Lee, Che and Peng (2025) study this question empirically on MATH-500, GSM8K and MMLU-Pro Math with 31 prompts and several frontier models. Their key observation is that, question by question, correctness is almost a threshold function of the response length: a model solves a question if and only if its chain of thought is at least as long as a question-specific token complexity. Under this hypothesis they derive the best possible accuracy–length tradeoff over all prompts, and show that existing prompting strategies are far from it (Table 4 of the paper). This mission formalizes that derivation: Theorem 1 of the paper and the steps of its proof in Appendix D.
Fix one language model and a dataset of questions . A prompt determines, for each question , a chain of thought of token length and a correctness indicator . The accuracy and the average token length of a prompt are
The two optimal tradeoff curves are the optimal accuracy at average budget and the minimal average length for accuracy :
Assumption 1 (token complexity hypothesis). There are numbers , the token complexities, such that for every prompt and question ,
The value marks a question the model never solves. The paper also assumes the prompts are rich: every vector of token counts is produced by some prompt. The answer is expressed through the empirical quantities
where is the largest accuracy any prompt can reach.
Assume Assumption 1, rich prompts, and pairwise distinct finite token complexities. Let be the largest finite with and the smallest finite with . Then for every and every ,
with both optima attained. As printed, the theorem defines , which does not depend on , and , which overshoots the quantile; both readings give wrong values on one- and two-question examples. The goal uses the thresholds that the proof and the text describe ("the highest value of τ that the LLM puts into the knapsack", "the α-quantile of the empirical distribution").
Milestones 4 and 5 allow ties among the token complexities; the goal's closed form does not.
Theorem 1 turns an optimization over all conceivable prompting strategies, an infinite and unstructured set, into a formula in the empirical distribution of numbers. Its consequence, Corollary 1, is that , the average token complexity of the solvable questions, is a lower bound on the average length of any lossless compression of the chain of thought; the paper's Table 4 uses it to show that current concise prompts leave a 3–11× reduction unrealized. The same characterization explains why adaptive strategies, which spend more tokens on harder questions, are necessary to approach the frontier.
The result has a pen-and-paper proof of a few lines in Appendix D; the prior-art search found no machine-checked version. Formalizing it adds a correct statement: the printed definitions of and are wrong, eq. (8) has a reversed inequality, and the closed form silently needs distinct token complexities. The mission records the correct versions with the counterexamples to the printed ones, and separates the tie-robust greedy form (milestones 4–5) from the CDF form (the goal).
The individual steps are elementary, but the obvious argument skips three points. First, passing from prompts to token vectors uses richness in both directions: an optimal prompt must be matched by a token vector and conversely, and the optima must be shown attained, not merely bounded. Second, the reduction to must handle questions with , which can never be selected. Third, the greedy claim is a statement about every feasible selection, not only the sorted ones, and translating the greedy count into the threshold forms and is exactly where ties break the formula, so distinctness must be used at that step and nowhere else.
Fin n; prompts are an arbitrary type; a Benchmark gives token lengths len : Prompt → Fin n → ℕ and correctness correct : Prompt → Fin n → Bool. Each (prompt, question) pair yields one deterministic chain of thought.ℕ∞-valued; is ⊤. Assumption 1 is correct P i = true ↔ τ i ≤ len P i ("above" read as , as the displayed formula on p. 5 shows). Every count or sum over filters on before converting to a natural number.IsGreatest/IsLeast predicates over the set of values achieved by prompts, never sSup/sInf, so empty or unbounded feasible sets cannot produce a junk value.The definitions (benchmark, empirical CDF over an ℕ∞-valued family, sorted prefix sums) are self-contained. A proof of the greedy milestones gives a reusable fact about unit-reward knapsacks. Proofs of any milestone and of the goal are welcome, as is a formalization of Corollary 1 on top of the goal.
An entrepreneur deciding whether to continue a project may value continued control even when liquidation would generate more cash. The project has a known liquidation value, but its final cash flow is uncertain. An accounting signal changes what the entrepreneur expects from continuation and can therefore change the decision. A regulator who cares about total cash flow can choose how much the signal reveals. Jiang and Yang ask which accounting rule best corrects the entrepreneur's excessive willingness to continue and show that the answer has a precise threshold form (Jiang and Yang 2023, §§2–3). The mission formalizes their main threshold characterization for the regulator's reduced problem.
The question belongs to information design: a decision maker chooses a signal before the state is known, anticipating how another party will act after observing it. The result gives a concrete instance in which the optimal signal is neither arbitrary disclosure nor full disclosure. It also identifies a parameter range in which the regulator can obtain the same liquidation decisions as if the entrepreneur had no private benefit.
At date 1 a project can be liquidated for or continued to produce a random date 2 cash flow . The prior law of has a density and full interval support , where . The entrepreneur receives an additional private benefit from continuation. The regulator counts the project's cash flow, not that private benefit. These assumptions and the common prior are from §2 of Jiang and Yang.
An accounting rule reveals information about . The signal induces a posterior probability distribution and hence a posterior mean . Under decision rule (4), the entrepreneur continues exactly when ; on equality they terminate, following the paper's tie rule. The regulator's payoff after that posterior is
The formal representation of a rule is a distribution over posteriors. It is Bayes plausible when its average posterior equals the prior ; the regulator's value is . This posterior representation is the one used in the paper's Appendix A.1 and is consistent with the general Bayesian persuasion framework of Kamenica and Gentzkow 2011. For an event of positive prior probability, denotes .
A threshold rule at sends a high signal precisely on . It sends the low signal when . The strict boundary agrees with Proposition 2; because the prior has a density, the single boundary state has probability zero.
For and , the goal is the corrected endpoint form of Proposition 2. There is a threshold whose reveal policy attains at least the value of every Bayes-plausible accounting rule. Its two cases are
The interior solution is unique. The entrepreneur follows the signal: continuation after the high signal and termination after the low signal. The first case gives the first-best liquidation decision, which continues precisely for .
The milestone list follows the source's Appendix A.1: reduction from Bayes-plausible posterior rules to a binary signal probability ; the relation between the two binary mean constraints (A.1) and (A.2) in each prior-mean regime; the threshold shape associated with the appendix's multiplier; the first-best case; existence, uniqueness, and optimality of the interior threshold; and the closing implication that joins the low-prior-mean case to the first-best case. Together these statements connect the general accounting-rule problem (5) to the threshold formula (6).
The theorem specifies when disclosure can neutralize the private continuation benefit and when a more conservative threshold is required. In the latter case the low signal must put the entrepreneur exactly at the continuation indifference point. The threshold characterization also underlies the paper's claims about full disclosure and how the optimal rule changes with and (Jiang and Yang 2023, Corollaries 1–2). Those corollaries are consequences of the present target, not assumptions of it.
The paper proves Proposition 2 mathematically; the Lean goal and milestone statements here remain open for machine-checked proofs. A complete development would provide a reusable posterior-to-binary reduction for a payoff with two linear segments, plus formal results about conditional means under full interval support. The referenced Bayes-plausibility definition is already published on Prove2Me. Proposition 1 of the paper concerns financing contracts and is outside this reduced regulator problem; its proof is in an online appendix not held with the cited PDF.
The regulator ranges over every Bayes-plausible distribution over posteriors, while the proposed optimum uses only two signals. Checking that a given threshold is best among threshold rules leaves this larger comparison unresolved. The regulator's payoff also switches formula at the entrepreneur's indifference mean, so a direct global smoothness argument does not apply. Finally, the conditional mean below a moving threshold must reach at one and only one interior point under the prior's support conditions. The binary reduction and these boundary properties are substantial parts of the formalization.
Lean uses real cash flows and a probability measure on with , mass one on , and positive mass on every open subinterval. A published definition supplies Bayes-plausible measures on the Giry space of posterior measures and the two-cell reveal policy. The strict high cell is ; equality goes to the low cell and termination. Conditional means are ratios of restricted integrals to event probabilities, and every event used by the theorem has positive prior mass. Bounded support makes the relevant posterior means finite almost everywhere under a Bayes-plausible rule.
Two endpoint guards repair the source's literal Proposition 2. At , its asserted interval is empty. At , the interior equation need not have a solution: with uniform on and , its left side is positive for every positive threshold. The goal therefore assumes and . The paper's assumption (1), involving investor reservation value, is absent from the reduced problem (5), and Appendix A.1 treats a prior-mean case that assumption would exclude; it is not imposed here.
The comparison in the goal covers all Bayes-plausible accounting rules. The payoff uses the entrepreneur's posterior-mean response, including the tie rule. A development that compares only threshold rules or fixes the entrepreneur's action to the signal would not establish this target. Contributions to the binary reduction, conditional-mean continuity and uniqueness, and optimality of the two threshold cases are directly reusable.
Service firms with idle capacity often turn away customers while a nearby competitor sits idle, and the reverse happens an hour later. Sharing capacity would help both, but contracting on every transfer is costly, and monitoring the partner's state is usually impossible. Informal arrangements in which favors are returned rather than paid for are a natural alternative, and the economics literature on favor exchange (Abdulkadiroğlu and Bagwell 2013) studies when such reciprocity is self-enforcing.
Hu and Caldentey (2023) model this as a dynamic game between two firms that can only observe the running balance of favors. They ask when a self-enforcing, payment-free exchange of capacity can be sustained in equilibrium. Their answer is an explicit condition on the primitives of the model. This mission formalizes that answer, Proposition 5 of the paper, together with the chain of lemmas the proof uses.
Two firms each serve their own stream of customers. Type- customers arrive at firm according to a Poisson process with rate . Each firm is a single server without a queue: its state is (idle or busy), and service times are exponential with rate .
The firms do not see each other's state. They only observe the favor balance , the net number of transfers firm 1 has accepted from firm 2. A transfer of a type-2 customer moves to , a transfer of a type-1 customer moves to .
A trading-favors strategy profile is with , where means that firm accepts a transfer at balance . Under the state is a continuous-time Markov chain on . Firm 's expected discounted payoff from state , written with its own state first, is , and .
A firm that is idle when the partner requests a favor compares accepting with refusing. This gives condition (4):
A trading-favors equilibrium (TFE) is a profile satisfying (4) for both firms. The no-collaboration profile (always refuse) is one. The family of interest is , : firm 1 accepts exactly when , and firm 2 accepts exactly when . Its core region is .
Two constants enter the answer. The modified traffic intensity is . The factors are entries of the inverse of a matrix from the balance equations of the chain (Lemmas 2–3 of the paper): when only firm 1 accepts at , and when only firm 2 accepts. They are discount factors of first passages out of a cluster of states.
A non-trivial TFE with exists if and only if
Each inequality says that the discounted value of a favor being returned exceeds the immediate service cost plus the discounted opportunity cost of being busy.
Proposition 5 turns an equilibrium question over infinitely many states into two inequalities in the primitives. It tells a manager whether informal capacity sharing can work at all, and how it responds to load, margins and patience. With Lemma 4 it also yields the largest sustainable core region, which the paper uses to compare the trading-favors arrangement with a central planner and with perfect monitoring (§5).
The result is proved on paper. No part of it, and no part of its model, has a machine-checked proof. Formalizing it requires a discounted-reward theory for a countable-state uniformized Markov chain, its balance equations, first-passage discounting and a one-shot-deviation comparison. These pieces are reusable well beyond this game. The formalization also settles the right reading of the equilibrium notion, which the printed text leaves ambiguous (see the scope section).
The obvious route is to solve the balance equations (5) explicitly. That fails: the system is infinite, and an explicit solution is available only cluster by cluster, through a matrix inverse whose entries have no simple closed form.
The sufficiency half of Lemma 4 is the hard step. To show that (14) makes an equilibrium, one must check (4) at every balance in the core, not only at the new boundary. This compares with a shifted through first-passage decompositions (Lemma A.3) and the strict part of Lemma A.1. Monotonicity of payoffs in (Proposition 4) solves the second-order recursion (9) and needs the bounds of Lemma A.2. Each of these steps is an inequality between expectations over an infinite state space.
All quantities are real numbers. Parameters are bundled in a structure with the standing assumptions , and . The paper states the conditions on , (after normalizing the per-rejection cost to ) and . Positivity of is added: these are rates of a Poisson process and an exponential law, and fails without them.
Conventions.
Fin 2, with 0 meaning "accept".The core-region reading. Definition 1 asks (4) at every . Under that reading Proposition 5 is false. At the paper's own Table 2 parameters, (15) holds, yet firm 1 strictly prefers to accept at , just outside the core of , so no with is a TFE. The paper's proofs check (4) only on the core region. Proposition 4, Lemma 4 and Proposition 5 are therefore stated with (4) on , and their titles say so. With this reading, the paper's Tables 2 and 3 are reproduced exactly. Proposition 1 keeps the literal definition. Lemma A.1 assumes (4) on a set containing the deviation balance, which is what its proof uses.
Ruling out trivial readings. A formalization that defines the payoff as "some solution of (5)", defines by a closed form, or defines the core-region equilibrium by (14) would make the milestones definitional. None of these is used. The equilibrium predicate is satisfiable: at the Table 2 parameters is a core-region TFE for .
Not formalized. Theorem 1 (finite core region of a general TFE), Propositions 2–3 and 6–8, Lemma 1, Corollary 1 and the numerical study are outside this mission.
Contributions welcome: summability and the Bellman identity for the uniformized discounted series, a policy-improvement lemma for one-state deviations, and first-passage decompositions on .
Directed network design asks which connections can be bought under a limited budget when traffic follows the directions of arcs. In directed tree orienteering, the reward comes from vertices reached by a rooted directed tree. The submodular version allows the reward of a new vertex to depend on which vertices have already been reached. This captures diminishing returns, including coverage rewards, while preserving a single cost constraint. Ghuge and Nagarajan use this problem to obtain results for directed Steiner tree and other directed network design problems; the connection is explained in their introduction and applications.
The target here is the paper's main algorithmic theorem. Its distinguishing claim combines an approximation ratio that improves with the optimal solution size and a quasi-polynomial bound on the algorithm's work. Both parts matter: an approximation statement about an unspecified algorithm would leave the computational content of the result open. The paper develops recursive greedy search, a value-guided budget search, and a version that groups several recursion levels. The main theorem reports the combined guarantee.
An instance has a finite vertex set of size , a root , a nonnegative integral cost for every directed arc, and a budget . A rooted arborescence is a set of directed arcs in which each selected non-root vertex has one incoming arc and every selected vertex is reachable from . Its cost is the sum of its arc costs. The complete directed graph is used because the source reduces to that representation; loops have no role.
A value oracle supplies for every vertex set . The reward is monotone: enlarging a set cannot lower its value. It is submodular: . In this mission, values are natural numbers and satisfy for a fixed exponent . This makes the integer thresholds used in the binary-search version explicit. The reward of an edge set is evaluated on , which includes the root. For an already selected set , the marginal reward is .
The algorithm also receives a responsibility set , a budget, and a depth . A successful output must reach every vertex in and respect the budget. A compatible comparison arborescence has the same root, responsibility and budget conditions, together with the depth's vertex cap. The paper's counts vertices in a comparison solution, including its root. The target assumes so its double logarithm is positive.
The main target is Theorem 1.1, p. 1. For every and polynomial reward exponent , one constant works for every eligible instance. The specified grouped recursive greedy algorithm returns a feasible solution such that every feasible rooted arborescence with at most vertices obeys
The milestone statements are the rooted separator Fact 2.2 in the corrected edge-count form, the guarantee for basic recursive greedy in Lemma 2.5, the same guarantee with binary-search budget guesses in Lemma 2.8, and the grouped recursion guarantee in Lemma 2.10. Their original wording and page locations accompany the individual milestones. These statements isolate the size reduction and the three approximation regimes on which the target depends.
The theorem supplies a directed, budget-constrained optimization guarantee for a class of rewards broader than additive vertex prizes. If an optimal solution has vertices, the approximation factor grows as , while the reported work grows quasi-polynomially in the input parameters. The paper applies the result to directed tree orienteering and derives consequences for directed Steiner tree and other network design settings. The mission concentrates on the submodular tree orienteering theorem itself, so those later reductions remain separate statements in the source.
This is a known paper result, not an open conjecture. The formalization work is to state and eventually prove the theorem for an explicit algorithm and a concrete step counter. A machine-checked proof would also settle the paper's boundary cases in a representation that subsequent results can import: reachability in directed edge sets, compatible subproblems, and value-threshold budget search. The statements here are draft targets; a successful Lean build checks that they are well formed, not that the advertised bounds have already been proved.
A recursion that guesses a separator and divides responsibilities must coordinate the two subcalls: the second uses vertices already found by the first, and its remaining budget depends on the first guess. A direct transcription of the printed pseudocode can return an empty edge set despite unmet responsibilities. It also omits zero as a left-subtree budget even though the paper permits zero-cost arcs. Either issue can break feasibility or the approximation claim on small instances. The grouped version must preserve the approximation bound when its depth counts several levels at once. In particular, its depth-one call must handle every compatible tree with at most non-root vertices. Its binary searches and grouped-base candidates must be included in the runtime accounting. A value-only guarantee does not establish the theorem's time bound.
Vertices are Fin n; arcs are ordered pairs and algorithms return an optional finite arc set with a natural-number step count. none represents infeasibility. The output's reachability, cost and responsibilities are asserted separately because a union of recursive outputs need not itself have the unique-parent property of an arborescence. The target also requires a rooted arborescence contained in that output on the same vertex set. Marginal rewards use real subtraction, avoiding truncated natural-number subtraction. The paper's submodularity predicate is reused from the published NonmonotoneSubmod.Shared.Submodular definition.
The concrete algorithm searches budgets from zero through the remaining budget and carries infeasibility through subcalls. Its grouped depth-one call examines all feasible arborescences up to the source's cap. Binary search records every recursive probe, and the step count records each candidate value evaluation and each grouped-base edge tuple. The logarithmic base uses , making the statement meaningful for budgets zero and one. No triangle inequality is assumed: the source invokes metric completion without loss of generality, while these statements work directly with the complete cost table. These choices, along with the corrected rooted interpretation of Fact 2.2, are recorded in the moderation notes.
The target names this algorithm and its recorded steps; an existence claim about some algorithm would miss its computational assertion. Useful contributions include the separator theorem, the three approximation lemmas, and reusable properties of the budget search, reachability and step counter. The source's length-constrained and deadline extensions, and its later application reductions, are outside this mission.
Firms that disclose a product carbon footprint can lower it in two ways: by cutting the emissions they control (better materials, cleaner processes), which costs money up front, or by buying carbon offsets from a third party at a constant price per tonne. Offsets have become cheap and widely available, and the business press has repeatedly argued that cheaper offsets let firms substitute away from costly abatement (The Wall Street Journal 2008, Forbes 2020 and The Washington Post 2020, as cited by Gao and Souza, p. 14). Whether that substitution actually happens matters for climate policy: if a lower offset price always raises a firm's own emissions, cheap offsets undercut real abatement.
Gao and Souza, Carbon Offsetting with Eco-Conscious Consumers (Management Science, 2022, doi:10.1287/mnsc.2021.4293), study this question in a model where demand responds to the disclosed footprint. Their Proposition 1 shows that the conventional intuition can fail in both directions of preference correlation: a cheaper offset can make the firm cut its controllable emissions. This mission formalizes that proposition together with the lemmas of its proof.
A firm sells to consumers. It chooses a controllable emission level per unit, which determines a unit cost and a fixed cost , with , , , on and . Each unit also carries uncontrollable emissions . At the offset price the firm offsets units, and discloses the footprint .
A consumer with valuation and environmental disutility gets utility at the price , and buys if and only if . A share of consumers is eco-conscious (); the rest are eco-unconscious (). A share of eco-conscious and of eco-unconscious consumers have the high valuation ; the others have , with , . The demand is the sum of the four segment masses whose utility is nonnegative, and the firm's profit is
A best response to is a feasible maximizing .
Two special cases carry the analysis: Case N (, negative correlation between caring about function and caring about the environment) and Case P (, positive correlation). For , the segment-optimal emission is the maximizer over of : the abatement level a firm chooses when it serves a segment of size and pays per unit of footprint. The proof compares the profit of covering the whole market at with that of serving only high-value consumers at ; their difference has a least zero , the offset price at which the firm switches.
In Case N, with , , a sign change of at its least zero , and condition (1) of the proof at , there are offset prices
for every pair of best responses (which exist), with strict emissions inequality when and . In Case P the analogue holds with , , and .
Proposition 1 identifies a mechanism by which cheaper offsets complement, rather than substitute for, controllable abatement. In Case N a lower offset price lets the firm lower its footprint enough to attract low-value eco-conscious consumers; in Case P it lets the firm price down to the low-value eco-unconscious consumers while keeping eco-conscious buyers. In both cases the served volume grows, and because abatement is a fixed cost, the larger volume makes deeper abatement worthwhile (economies of scale). The paper builds its NGO-pricing results (Propositions 2 and 4) on this subgame analysis.
The result is proved in the paper by a case analysis and derivative arguments; it has no machine-checked proof. Formalizing it produces a complete, checked treatment of a discontinuous best response in a pricing model with threshold demand, and it makes several steps of the published proof precise: where the paper asserts and "" without proof, the formal statements carry them as disclosed hypotheses, and the formalization of " for some " pins both thresholds down.
The best response is not a continuous function of : demand is a step function of price and footprint, so the firm's problem splits into six regimes (Online Supplement I1), and the optimal price jumps between , and the footprint-adjusted prices. Comparative statics by differentiating first-order conditions, the method of the paper's lemmas, applies only within a regime. The obvious argument, " is decreasing in by Lemma VI1", is wrong across the switch at : there the served segment shrinks, and Lemma VI1's monotonicity in the segment size works against its monotonicity in the price. Showing that the jump in segment size dominates requires controlling the best response on both sides of , including uniqueness of the best response and the behaviour of at the ends of where the first-order condition fails.
All quantities are real. The model is one definition file, EcoOffset.Subgame.Model, with a structure Params of primitives and a predicate Params.Standing bundling the standing assumptions of §3: , , , , , of class on with the sign conditions on on the closed interval , and . Prices range over all of ; consumers buy at zero utility. A best response is a predicate, never a chosen function, and the goal quantifies over every best response at and and asserts that one exists. is defined as the maximizer, not through the paper's root of the first-order condition (which does not exist at ). The switching price is a variable pinned by and on .
Added hypotheses relative to the page, all disclosed in the statements: (the proof's unproved ""; numerical Case N instances violate it); a sign change of at (the proof's unproved ); in Case N and in Case P (divisions in , ); for the existence of in Case N; explicit interiority conditions in place of "if is large enough".
Stating the goal about the two named profiles (for example ) would reduce it to Lemma VI1 plus algebra and is ruled out: the goal is about best responses of the full profit maximization. The paper's "for some " is likewise not used, since would make it vacuous.
A complete development needs: existence, uniqueness and continuity in of the maximizer of a strictly concave function on an interval (Berge's maximum theorem in one dimension); monotone comparative statics for ; the case analysis of the step-function demand; and intermediate-value arguments for . The first two are reusable for any one-dimensional parametric optimization. Proofs of individual milestones, and of the goal from the milestones, are welcome.
Electricity systems with hydro storage, and many other resource systems, are operated over time under uncertain inflows. In a centrally planned system a single risk-averse planner chooses releases and storage to minimize a nested (time-consistent) coherent risk measure of total cost. In a deregulated system the same decisions are taken by many agents, each with its own risk attitude, who trade the product, stored resources and financial instruments at market prices. A classical question of welfare economics is when the two coincide.
For risk-neutral agents the answer is the standard welfare theorems. Ferris and Philpott, Dynamic risked equilibrium (Operations Research, 2022), extend them to a multistage setting in which each agent evaluates risk with its own polyhedral coherent risk measure on a scenario tree and can trade Arrow–Debreu securities between each node and its children. Their First Welfare Theorem (Theorem 3) says that every such risk-trading equilibrium solves a social planning problem whose risk set is the intersection of the agents' risk sets. The converse direction, that a risk-averse social planning solution can be supported as a competitive equilibrium with risk trading (a Second Welfare Theorem), was shown for multistage hydro-thermal electricity markets by Philpott, Ferris and Wets (Mathematical Programming B, 2016). The forward direction is described in the 2022 paper as newly established there.
A finite scenario tree has nodes , root , leaves ; is the parent of and its set of children. A finite set of agents acts on it. At node , agent chooses releases and storage ; it has a cost , a production , a terminal storage value , and its storage evolves as with random supply .
Each agent's risk attitude is a polyhedral risk set at every non-leaf node,
a polytope of probability vectors on the children ; the one-step risk of a cost on is . The social planning risk set is (Definition 1), assumed nonempty (Assumption 3).
Prices are for the product, for agent 's storage, and for an Arrow–Debreu security bought at that pays in child . Agent buys of them. Its one-node disbenefit is
and its problem in complementarity form is the system , (20a)–(20g). A multistage risk-trading equilibrium RTE (Definition 3) is a set of prices and actions such that every agent solves and the product, storage and security markets clear, (21)–(23). The social planning system (p. 10) is the analogous eight-line complementarity system for a single planner with stage cost and risk set .
Every RTE with prices and actions satisfies, with :
Theorem 3 says that competitive trading of risk, through a complete set of one-step Arrow–Debreu securities, leads risk-averse agents with different risk attitudes to the outcome a risk-averse planner would choose if the planner used the intersection of their risk sets. The equilibrium security prices are the planner's worst-case probability measure. The paper uses the welfare theorems to indicate how social welfare might be compromised when risk markets are incomplete or illiquid, even if agents behave as price takers; its motivating example is a cascade of hydroelectric reservoirs operated by different agents.
The result is proved on paper. As far as a search of the Prove2Me catalog shows, no risk-trading equilibrium, nested polyhedral risk measure on a tree, or welfare theorem with coherent risk measures has been formalized. The mission produces a machine-checked statement of the multistage model (the agent problem, equilibrium and planning system, written out line by line) and of the welfare theorem. It also fixes the readings of a garbled clause of the printed statement and of one gap in the printed proof (see below).
Each step of the argument is elementary, but the bookkeeping is heavy. The model is indexed by agents, nodes, children, risk-set generators and storage components, and every condition is a finite sum over children. The proof of (24) has to show that, summed over agents, all payments cancel by the complementarity conditions (21)–(23), and this cancellation uses the agents' disbenefits at the grandchildren as well. Part (iv) is the substantive step. The natural first attempt, taking the multipliers of from Lemma 1 as the printed proof does, puts all weight on one maximizing generator. That reproduces the equilibrium price only when is itself a generator, and the fifth line of needs the multipliers to reproduce exactly.
The tree is the platform's StochasticProg.Multistage.Tree ( = children n, = anc n); a leaf is a node with no children. The normal cone is the platform's FirstOrderOpt.ConvexTheory.normalCone. The definition file DynRiskEq.Welfare.Model holds the market data, the risk sets, (18), (20a)–(20g), RTE (Definition 3), (Definition 1) and (p. 10). These are the model.
Committed conventions:
EuclideanSpace ℝ (Fin d);HasGradientAt), and every normal-cone condition includes membership in its set;The hypotheses of the goal are:
Convexity of , Assumptions 1, 2 and 4 and equal leaf depth are not assumed: Theorem 3 does not use them. The closing clause of Theorem 3 is read as the link and is part of the conclusion of (iv). Without it, (iv) would not say that the equilibrium price is the social worst-case measure.
The equilibrium does not contain or the conclusion , is not defined by (24), and keeps all eight lines of p. 10. A formalization that took any of these shortcuts would make the goal trivial.
Not formalized here:
Theorem 4 is the natural follow-up mission. General lemmas about maxima of linear functions over convex hulls of finite families are reusable beyond this mission, and contributions of them are welcome.