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?
Barberis' casino gambling model (Barberis 2012) asks when a gambler with cumulative prospect theory (CPT) preferences should leave a casino. At each of the times the gambler either stops or bets $1 on a fair coin. The value of a stopping strategy depends on it only through the law of the gain at exit, . Probability weighting makes the problem time-inconsistent, so dynamic programming does not apply. Barberis solved small horizons by enumerating Markovian strategies, which does not scale: the paper reports 27 hours of computation for .
Hu, Obłój and Zhou (arXiv:2102.03157v1, published in Management Science 2023) take the law of as the decision variable. This works only with a description of the set of laws that stopping before time can produce, and of a stopping rule that produces a given law. Their Theorem 3.1 gives both. It is a finite-horizon Skorokhod embedding theorem for the simple symmetric random walk.
Timeline:
A casino space is a filtered probability space carrying a standard symmetric random walk and a variable . Here , each is -measurable, and each increment is , fair, and independent of . The variable is -measurable and uniform on . The variable lets a gambler randomize: from it one can build countably many independent biased coins. The admissible strategies are all -stopping times ; they may depend on the whole path and on the coins.
is the set of probability laws on the integers with a finite first moment and mean zero. The potential of is
For a stopping time , is the potential of the law of . The evolutional functions are defined on the integers by
A randomized Root stopping time has three ingredients:
It is
Let and let satisfy . Then some has if and only if
In that case, some randomized Root stopping time has .
The theorem makes the time-inconsistent stopping problem an optimisation over finitely many probabilities . The constraints are explicit: (8) together with . The paper builds its mathematical program (§4) and its algorithm on this reduction, replacing exhaustive search over strategies. The "moreover" clause shows that randomized Markovian barrier rules are as good as any path-dependent or randomized strategy for every law-invariant objective. This is a structural statement about optimal behaviour, not specific to CPT.
Formalizing the statement produces a machine-checked discrete Skorokhod embedding with a time bound. As far as a search of the platform shows, it would be the first formal treatment of Root-type stopping times. It also produces a potential-function toolkit for integer laws: identities (5), uniqueness, and the recursion (17) for stopped walks. That toolkit is reusable for other random-walk embedding and martingale optimal transport results. The result is proved in the paper; none of it is formalized.
The "only if" direction must hold for every stopping time on every casino space, including path-dependent, randomized and non-Markovian ones. A natural first idea is to prove it for Markovian or Root rules and argue that these are without loss of generality. That is exactly the content of the theorem, so it cannot be assumed. The bound must hold for an arbitrary that embeds , and the parity structure of the walk enters it in an essential way.
The "if" direction must construct the coins on the given space from the single uniform variable . The constructed stopping time must be bounded by , not merely almost surely finite. And condition (8) constrains only the odd or even sites, depending on ; showing that this partial condition forces at every integer needs convexity of and the parity identities of the evolutional functions.
All objects live in the namespace CasinoCPT.Embedding and in one definitions module.
IsCasinoSpace P F S ξ on an arbitrary measurable space. Every statement quantifies over all such spaces; no conclusion chooses the space.ℕ∞-valued IsStoppingTime, and means a stopping time with for every .stoppedValue S σ, a measure on .false meaning "stop". They are -measurable and mutually independent, with the three laws of (7).The Root clause of the goal asserts that a barrier, boundary probabilities and a coin family exist whose Root time lies in and embeds .
A trivializing formalization is ruled out: is not restricted to Root times, Markovian rules or a linear program on the binomial tree. The definition of is literally (7), with the infimum of the empty set equal to .
A complete development needs:
Proofs of individual milestones are welcome independently. Propositions A.2 (i)–(iii) and the equivalence (8) ⇔ need no probability space.
A portfolio can look attractive on average and still perform poorly when the financial system is under stress. Capponi and Rubtsov's Systemic Risk Driven Portfolio Selection asks an investor to choose asset weights using the portfolio return expected in a specified system stress state, rather than using only an unconditional mean or variance. The question is concrete: when the system return is at a low quantile, which portfolio has the highest expected return among outcomes below its own conditional low quantile? This mission formalizes the paper's closed-form answer for the Gaussian case, Proposition 2 of the May 25, 2019 working paper.
The paper distinguishes a system fixed at its value-at-risk level from a system lying anywhere below that level. The former has an explicit optimizer under a technical condition; the latter leads to a different criterion and is outside this mission. The distinction matters because conditioning on one exact system return and conditioning on a tail event produce different laws and different portfolio problems. The working paper, pp. 5–14, develops both settings.
There are risky assets and no risk-free asset. Their random return vector has mean and covariance matrix . A portfolio is a real weight vector satisfying ; the paper imposes no nonnegative-weight or no-short-sale constraint. Its return has mean and standard deviation . The system return has mean and standard deviation , and denotes the vector of covariances between each asset and the system. Thus the portfolio-system correlation is .
For a law on the real line, value at risk at level is its lower -quantile, . Let and be quantile levels strictly between zero and one half, as in the paper's stress convention. The conditional value at risk is the -quantile of the conditional law of when . The performance criterion is the co-expected return
Under Assumption 2, is bivariate Gaussian, with the means, standard deviations and correlation above. The proof of Proposition 2 uses the joint covariance of all asset returns and the system, . The working paper, pp. 5–7 and 28, gives these definitions and parameters.
The first targets identify the Gaussian quantile and lower-tail mean, then the conditional Gaussian law. They yield the paper's CoVaR display and the closed form for in Proposition 1:
Here and are the standard normal cumulative distribution and density. Define , , and . The paper's Appendix partitions and after asset to obtain and . Proposition 2 gives a particular inverse-matrix expression and states that, provided , it maximizes over all weights summing to one. The goal includes feasibility and uniqueness:
with equality only for . The exact is part of the Lean definitions and reproduces the formula printed in Proposition 2, including its last-asset partition and transpose on . The draft theorem chain covers the paper's displayed results (A.1)–(A.4), Proposition 1 (2.4), and the optimization step (A.7)–(A.8); the mission's milestones mark the conditional law, CoVaR, CoER=, the vector formula, and the optimizer. The working paper, pp. 7, 9 and 27–29, states them.
The result gives an explicit portfolio choice for a stress-sensitive objective, subject only to the full-investment constraint. Its condition identifies the regime in which the finite optimizer exists; when the condition fails, the paper notes that portfolios with arbitrarily high objective values can be constructed. The conditional-return formula also separates ordinary expected return, exposure to the system, and variance left after accounting for that exposure. This permits a precise comparison with a mean-variance portfolio using the same covariance data. The working paper, pp. 7–10, gives the comparison and its numerical illustration.
The paper proves these claims analytically. Here the Lean declarations compile as statements with open proofs; this mission does not claim a machine-checked proof of Proposition 2. A completed formalization would connect the conditional-density meaning of CoER= to the Gaussian formulas and then verify the optimizer for the full class of feasible weights. The quantile, conditional Gaussian, and quadratic objective interfaces are reusable in other risk and stochastic optimization results.
The event has probability zero for a nondegenerate Gaussian. An ordinary ratio of event probabilities therefore does not define the conditional law at that exact point. The paper relies on the bivariate density to specify it. Even after its Gaussian form is known, the objective contains a square root of a covariance quadratic form, and the feasible set is an unbounded affine hyperplane because weights may be negative. A first-order stationary calculation alone does not establish a global, unique maximizer or exclude unbounded cases. The condition in Proposition 2 addresses that boundary.
Vectors use Fin (m + 1) → ℝ with ; the final asset is Fin.last m. Matrices are finite real Mathlib matrices. The formal model builds , and from asset and system parameters, and builds CoER= from the conditional law for every weight vector. It does not replace CoVaR or CoER= by their later closed forms. This prevents the Gaussian and portfolio milestones from becoming restatements of definitions.
The conditional law at an exact system value is the density ratio of the bivariate Gaussian, fixing the continuous version needed at a null event. VaR is a left quantile; is the same construction for the standard normal law. Gaussian variances use nonnegative reals, while portfolio quantities and matrix algebra use reals. Expectations are set integrals under the conditional law, divided by the actual conditional probability of the lower-tail event.
The standing assumptions include positive definiteness of the joint asset-system covariance and . Positive definiteness makes all conditional Gaussian variances positive and supplies the nonsingular matrices required by the printed inverse formula. In particular, the mission excludes degenerate covariance matrices for which Lean's total inverse or square root could silently return a default value. The formalization needs finite-matrix positive-definiteness and Schur-complement facts, Gaussian density and quantile facts, set-integral facts, and a constrained optimization theorem for the square-root quadratic objective. Contributions proving any of those faithful milestones or reusable supporting lemmas are within scope.
A financial network can contain firms or other agents that owe money to one another. Each agent's capacity to pay depends on what it receives from the others, so a payment decision at one agent can change the resources available elsewhere in the network. A clearing payment matrix describes a set of payments consistent with those interdependent resources and with the rules by which each agent divides its available estate among claimants. Whether that matrix is unique matters when the network is used to assign final payments and equity: several clearing matrices can imply different payments even for the same liabilities and endowments. Csóka and Herings study this question for general monotonic division rules, including rules that prioritize some claimants over others. Their working paper gives an explicit example with positive endowments and two clearing matrices, then identifies conditions on the network's liability cycles that guarantee uniqueness. Csóka and Herings, 2021.
A financial network is , where is a finite set of agents, is agent 's endowment, and is the liability owed by to . There are no self-liabilities: . The total liability of is . A division rule assigns payments to each claimant when agent has an estate . Payments are nonnegative, do not exceed individual claims, and sum to . Every rule is coordinatewise nondecreasing as the estate grows. The model permits and permits an agent to have no creditors. Csóka and Herings, 2021, §2.
A payment matrix has nonnegative entries and zero diagonal. Its entry is the payment from to . Agent has asset value and equity . A row is feasible when it equals for some . Definition 2.2 calls clearing when every row is feasible, every agent has nonnegative equity, and every agent paying strictly less than its liability row has zero equity. Here means coordinatewise with at least one strict inequality; is a row, while is a number. Theorem 3.1 establishes that this economic definition is equivalent to the payment equations . Csóka and Herings, 2021, pp. 7–9.
Positive liabilities define a directed graph. Let be the strongly connected component containing . An agent is cyclical when has at least two members; is the set of such agents. A component has no successors when no positive liability leads from one of its members to an agent outside it. For a positive claim , the threshold marks the estate at which begins paying . A rule is strictly monotonic if each positive-claim payment rises strictly whenever the estate rises within . It is positive monotonic if the same holds once the estate reaches . Csóka and Herings, 2021, Definition 2.1 and §4.
The intermediate targets establish that monotonic division rules are continuous, characterize clearing through the payment equations, show that the clearing matrices form a complete lattice, and show that every clearing matrix gives the same equity vector. The later milestones track what happens when a row differs between the least and greatest clearing matrices and isolate agreement on cyclical rows. These are the statements used by the paper on its route to Theorem 4.5. Csóka and Herings, 2021, §§2–4.
The goal is existence and uniqueness under the paper's three conditions:
The first condition is over components, so stating it for every agent's component makes no difference. No extra monotonicity condition is placed on non-cyclical agents beyond the network's standing assumptions. Csóka and Herings, 2021, Theorem 4.5.
The theorem gives a network-level criterion for a unique payment outcome under general division rules. It is stronger than merely selecting a least or greatest clearing matrix: those extremal matrices exist even when payments are multiple. The paper uses its criterion to relate earlier uniqueness results for more specialized network and division-rule models, and later studies how uniqueness relates to continuity of a bankruptcy rule. Those later statements are outside this mission. Csóka and Herings, 2021, §§5–7.
The result is proved in the cited paper. This mission asks for a machine-checked Lean development of that known theorem and its listed intermediate results. The prior-art search for this proposal found only special-case clearing models and no published formalization of these exact statements with arbitrary monotonic division rules and zero endowments. The network, division-rule, and clearing definitions would also support formal work on the paper's later bankruptcy-rule results.
Monotonicity of the payment system gives a least and a greatest clearing matrix, but does not force them to coincide. The paper's priority-rule example has all endowments positive and still has distinct clearing matrices. An argument that only invokes a monotone fixed-point theorem therefore cannot settle uniqueness. The difficult distinction is between payment differences that can persist around liability cycles and those that cannot: positive and strict monotonicity are needed at different agents, and the endowment condition concerns only successor-free cycles. Csóka and Herings, 2021, Example 4.1 and Theorem 4.5.
Agents are an arbitrary finite type, including the empty type. Matrices are functions with entrywise order. Endowments and liabilities are nonnegative, and all division-rule conditions apply on ; a rule's value at negative is irrelevant. The clearing predicate is Definition 2.2's three conditions. The payment equations are a theorem, not its definition. This distinction prevents uniqueness from being built into the model. The conclusion quantifies over all payment matrices and asserts both existence and uniqueness.
The threshold is represented by the supremum of the nonnegative estates with and is used only for positive claims, where the standing assumptions make that supremum meaningful. Reachability uses positive-liability walks; between distinct agents these have the same endpoints as the paper's paths of distinct agents. A component includes its named agent, and successor-free means that no positive-liability edge leaves it. The least and greatest clearing matrices in intermediate statements are characterized by order properties, not chosen objects.
A complete development needs finite-sum and real-order facts, continuity of monotone division rules under their sum constraint, complete-lattice fixed-point infrastructure, and finite directed-graph reasoning for strongly connected components. The general network and clearing definitions are reusable. Contributions toward any of the listed milestones, including supporting results about these definitions, are within scope.
In information design (Bayesian persuasion), a designer commits to a signal about an unknown state, and every signal induces a distribution over the receiver's posterior beliefs. Kamenica and Gentzkow (2011) showed that the distributions a signal can induce are exactly the Bayes-plausible ones, those whose mean posterior is the prior, and that the designer's optimal value is the concave hull (concavification) of the designer's objective, evaluated at the prior. This reduces the design problem to a computation in convex analysis, and it is the basic tool of the information design literature.
Many applications add constraints on the distribution of posteriors: a capacity or cost constraint on information (rational inattention), participation or incentive constraints when the designer is a mechanism designer with limited commitment, or a bound on the probability of a given action. Le Treust and Tomala (2019) treated one inequality constraint for finitely supported distributions. Doval and Skreta (arXiv:1811.03588v3, Mathematics of Operations Research, 2024) allow any finite number of inequality and equality constraints, and an arbitrary Borel distribution over posteriors. Their first main result, Theorem 3.1, shows that the value is still a concave hull, of a function of more variables.
Let be a finite set of states and the simplex of beliefs. The data are measurable functions on : an objective , inequality constraint functions and equality constraint functions , with .
For a prior , is the set of Borel probability measures on with mean . The constrained information design problem (CID) at a parameter , , is
component-wise, with when no is feasible. The feasibility set (Definition 2.2) is the set of at which (CID) is feasible.
The pointwise set collects the parameters at which the constraints hold for the degenerate distribution at . The modified objective (3.1) is
equal to on and off . For a function on , the hypograph is and the concave hull (Definition 2.1) is
In the Lean development these are IsBayesPlausible, IsConstraintFeasible, value, feasibleSet, pointwiseSet, modObj, hypo and cav, in the namespace ConstrInfoDesign.Cav.
For every ,
The statement fixes no constants and assumes nothing beyond measurability; it covers infeasible parameters, where both sides are , and unbounded objectives, where both sides may be .
Theorem 3.1 gives the value function of (CID) in closed form as a single concave hull. Its consequences in the paper are a bound on the number of posteriors an optimal design needs (Corollary 3.1), a refinement to with binding constraints (Corollary 3.2), and, combined with Lagrangian duality, the characterization of optimal designs in applications such as mechanism design with limited commitment and persuasion of a privately informed receiver. The result also explains when the feasibility set is the convex hull of the pointwise set (Lemma A.1), which is the geometric reason the constrained problem behaves like an unconstrained one in coordinates.
The result is proved in the paper; to the best of current knowledge none of it is formalized. Mathlib has convex hulls, Carathéodory's theorem, measures, supports and Bochner integrals, but neither the concavification theorem of Kamenica and Gentzkow nor the Rubin–Wesler theorem that the mean of an integrable random vector lies in the convex hull (not only its closure) of a set carrying it. A complete development would give machine-checked versions of both, reusable by any formalization of Bayesian persuasion with finitely many states.
The obvious argument for says that the mean of the vector under lies in the convex hull of its range. Mathlib's tools (Convex.integral_mem) only give membership in a closed convex set, and the range of an integrable, possibly unbounded and discontinuous is not closed; the closure gives the concave closure of , which differs from the concave hull on the boundary of its domain (Example D.1 of the paper). The Rubin–Wesler theorem closes this gap, but it needs its own argument by induction on dimension.
In Proposition A.2, Carathéodory's theorem in gives points of the hypograph; the claimed bound needs the extra observation that a point of the hypograph can be moved up to the graph. The remaining steps are bookkeeping in the extended reals: shifting thresholds so that each point of a convex combination lies in , and approximation arguments when the suprema are infinite.
States are Fin N; beliefs are points of Fin N → ℝ and is stdSimplex ℝ (Fin N). The parameter space is the product (Fin N → ℝ) × ((Fin I → ℝ) × (Fin E → ℝ)). The functions , are total on Fin N → ℝ; their values off the simplex never matter. A distribution over posteriors is a Borel probability measure on Fin N → ℝ that gives the complement of the simplex measure zero, and its mean is the Bochner integral of the identity.
Conventions committed to:
EReal; suprema are sSup in EReal, so the empty supremum is .Trivializing formalizations are ruled out: is not taken over finitely supported distributions only (which would make Proposition A.1 empty), cav is Definition 2.1 and not the sum formula of Proposition A.2, is Definition 2.2 and not , integrals of non-integrable maps are excluded rather than counted as , and no supremum is taken in .
The development needs the Rubin–Wesler theorem in finite dimensions, a Carathéodory variant for hypographs, and the finite-dimensional facts that a measure on a second-countable space is carried by its support and that finite sums of Dirac masses are probability measures with the expected integrals. The Rubin–Wesler theorem and Proposition A.2 are reusable beyond this mission. Proofs of the milestones and of the goal, and alternative arguments, are welcome.
Passive funds hold a market index rather than selecting individual stocks. In the model of Baruch and Zhang (2022), this difference matters for what prices reveal. An investor who studies individual stocks can bring information about their payoffs into trading; an investor restricted to the market portfolio cannot make the same stock-by-stock trades. The paper asks how the mix of these investors changes the information about future asset payoffs that can be inferred from market prices. Its answer separates the market portfolio from every other stock portfolio: indexing preserves the former's price efficiency while reducing the latter's, at an increasing rate. This mission targets that price-efficiency result, Theorem 3 on p. 6226.
The question matters to asset-pricing models that use prices as information. A price can be informative even when it is affected by many other forces; here the paper gives a controlled Gaussian economy in which the effect of replacing active investors with indexers can be isolated. The target is a theorem about conditional variances, not an empirical estimate of the effect of real index funds. The equilibrium interpretation comes from the paper's earlier price construction; the formal statements here use the public statistic that the paper proves equivalent for this purpose (15)–(16), p. 6224.
There are risky assets and investors. The random payoff vector is , with multivariate normal law . Investor sees a private signal , where . The payoff and all noise vectors are mutually independent, and the two covariance matrices are positive definite. A stock portfolio pays . The all-ones vector is the market portfolio. These are the assumptions and terms introduced in §2, p. 6221.
The investors are partitioned into indexers , who hold the market portfolio, and nonindexers . Both kinds are present: , with p. 6222. Equation (3) sets . Equation (4) combines the nonindexers' average signal and a scalar statistic of all signals into the public statistic
The first component has coordinates; the second has one. The paper identifies the conditional variance given this statistic with the variance given equilibrium prices (16), p. 6224. In this mission, means the conditional variance of given . It is initially a random variable, and equation (20) asserts that it is almost surely a deterministic matrix expression under the Gaussian model.
The goal is Theorem 3, p. 6226, stated for all admissible nonindexer sets on the same probability space. For any real , market-portfolio multiples have unchanged conditional variance:
For every other portfolio, fewer nonindexers, equivalently more indexers, strictly raise conditional variance. The rate also grows: whenever and ,
The six milestones are the identities and statements used in the paper's development: the cross-covariance in (7), the covariance of in (8), Gaussian conditioning in (20), the characterization of market portfolios in Lemma 2, the first derivative in (21), and the second-derivative conclusion in §6.1, p. 6227. They make the model-to-goal path explicit without changing the goal's three clauses.
The result specifies which price information survives a shift toward passive investing in this economy. It says that market-portfolio payoff information is preserved while information about every portfolio outside the span of is lost, with an accelerating loss across successive increases in indexer count. The distinction is used later in the paper to discuss asset-price comovement and a conditional CAPM measure §6.2–6.3, pp. 6227–6228.
Baruch and Zhang proved the theorem in 2022. The formalization work is to represent their Gaussian model, its public statistic, the conditional-variance identity, and the comparative-statics claims in Lean, then supply machine-checked proofs. The current proposal contains checked statements and definitions with open theorem proofs; it does not claim that those proofs already exist. The model interface and covariance identities could also support later formalizations of the paper's price and comovement results.
The target compares conditional variances arising from different information sets. Their equality or ordering cannot be read directly from the definitions of conditional expectation. The Gaussian assumption turns the conditional variance into a matrix expression, but the derivation must preserve the dependence structure of all signals and the special scalar coordinate of . The boundary makes redundant and its covariance singular, so the inverse formula requires the paper's standing condition that both investor types are present.
The rate claim requires more than the sign of the first derivative. The printed second-derivative argument on p. 6227 omits the minus sign in the derivative of a matrix inverse; the nonnegativity conclusion survives, but its formal statement records the corrected derivative value. The strict increasing-rate clause in the goal is stronger than the non-strict inequality displayed in that proof. These distinctions must be established for every portfolio outside the market span, including edge dimensions, rather than inferred from a numerical example.
Assets are indexed by Fin n and investors by Fin m, both starting at zero. The final coordinate of is represented by the Unit side of Fin n ⊕ Unit. Mathlib's multivariate Gaussian law lives on a Euclidean space; a SignalModel bundles the Gaussian laws, positive definiteness, mutual independence, and measurability of payoffs and noises. Joint normality follows from these model assumptions. The measurability fields ensure that is a sub-σ-algebra of the ambient one.
The conditional variance in the goal is Mathlib's conditional variance of given , compared almost surely across choices of . It is not defined by the Schur-complement formula: milestone (20) asserts that identity. The matrix and the coefficients in (19) use a real variable in the derivative milestones, extending the integer count used by the economy. Positive definiteness and rule out the junk inverse and zero-denominator cases. The strict discrete-increment statement expresses “increasing rate” in the goal.
The equilibrium prices and their equivalence with in (16), Theorems 1–2, and the later comovement and CAPM results are outside this mission. Contributions are welcome on Gaussian conditioning, covariance identities, matrix inverse differentiation, and the comparison of successive portfolio variances. General Gaussian and matrix lemmas can be reused beyond this paper.
Shoppers judge products differently inside a store than outside it. Lighting, the color of price tags, the position of a product on the shelf, the presence of a decoy: each of these can change how much weight a consumer puts on quality or on price at the moment of purchase. A large literature in behavioral economics documents such effects and models them. Examples are the salience model of Bordalo, Gennaioli and Shleifer, the focusing model of Kőszegi and Szeidl, and relative thinking in the sense of Bushong, Rabin and Schwartzstein. Retail practice exploits the same effects: loss leaders draw customers in, and the sale is then steered towards a different product (up-selling to a pricier, higher-quality item, or down-selling to a cheaper, lower-quality one).
A. Apffelstaedt and L. Mechtenberg (Competition for Context-Sensitive Consumers, MPRA Paper No. 99509, 2016; published in Management Science, 2021) ask what happens to such tactics under perfect competition. Consumers choose a store on the basis of the product they expect to buy. Inside the store, the context may change their mind. Consumers may misjudge how strongly it does so. The paper shows that when consumers underestimate their sensitivity to context, competition does not remove the distortion. Instead it pins down a specific fooling strategy in every equilibrium: a loss-leading attraction product and a target sold at cost. The store context is used to up-sell or down-sell from one to the other.
A product has a quality , a price and a store context : no distortion, quality-inflating or price-inflating. Outside a store a consumer values it at the undistorted surplus ; the outside option of not buying is worth . Inside a store, a consumer with context sensitivity values it at
The true sensitivity is . Each consumer has a type , her belief about , drawn from a distribution with a density and supported in . Types with are optimists. A product is acceptable if and , for a minimum quality and a maximum price .
There are firms. Each firm commits to a finite menu of products with their contexts. Consumers then move in two stages:
Selling a product of quality costs the firm . The cost satisfies , , . The cost-efficient qualities solve . The paper assumes and .
Fooling (Definition 3) is a pair: an attraction product , which a type expects to buy, and a target , which she buys. It requires (IC) and (PCC), with one of the two strict.
A competitive equilibrium is a profile of menus with three properties:
The two context technologies are store-wide (one context for all products of a store) and product-specific (one context per product). Write
Assume all types are optimists. With store-wide contexts, a competitive equilibrium exists. In every one, at least two firms have positive demand and all others offer nothing. Each active firm offers exactly two products, a target and an attraction product :
When , each active firm offers one of the two menus.
With product-specific contexts, a competitive equilibrium exists. In every one, each active firm uses with
In all cases : the attraction product is a loss leader.
The proposition shows how a behavioral bias survives perfect competition. Zero profits do not mean undistorted choices. Competition passes the gains from fooling on to consumers through the attraction product, and the store context does the selling. Which context arises (quality inflation with up-selling, or price inflation with down-selling) is decided by comparing two explicit switching surpluses. A planner can read welfare comparisons and policy predictions directly off the explicit equilibrium menus. Later results of the paper build on this one: Proposition 3 implements the contexts with one decoy under salience, focusing or relative thinking, and Proposition 4 treats mixed populations.
The result is proved in the paper; no machine-checked proof of it, or of any part of the model, is known to exist. The mission produces three things:
The formalization also records three slips in the printed proof:
The pair-level bounds are elementary inequalities. The difficulty is the market argument. The paper first derives best responses for a single type with a fixed outside option, then argues that in equilibrium every type faces the same outside surplus. Turning this into a proof requires several steps:
The naive approach treats each firm as facing a single type. That step does not carry over: demand is a positive-measure condition on a continuum of types, and uniqueness must hold for all of them.
All quantities are real numbers.
(q, p, θ) and a menu is a Finset of products; the context is carried by each product. Firms are indexed by Fin K.Proposition 2 must be stated about equilibrium profiles of firms with arbitrary finite menus. It must not be stated about the candidate menus or about two-product menus. Without footnote 4's conditions it is false (padding menus), and with a literal lexicographic cost it is vacuous (no equilibrium exists).
Contributions are welcome at every level: the pair-level inequalities (Lemmas 2–3, the best-response bounds), the market argument (at least two active firms, uniqueness of the outside option), and the existence proofs. The model file, two-stage choice under a continuum of types with a firm-favourable tie rule, is reusable for other behavioral industrial-organization results.
Influenza vaccine is made in fertilized chicken eggs, and how many doses an egg yields is not known until production is under way. By the time the season begins, the realized supply can fall short of, or exceed, what a planner would want. Two inefficiencies then compound. On the supply side, a manufacturer paid a wholesale price per dose sold carries all the yield risk and plans too little. On the demand side, vaccination protects others as well as the vaccinated person, so self-interested individuals vaccinate too little when supply is ample. When supply is scarce, high-risk individuals compete with low-risk ones under random rationing, and from society's point of view too many low-cost individuals seek the vaccine. Earlier work coordinated one side at a time: Chick, Mamani and Simchi-Levi (Operations Research 56(6), 2008) designed cost-sharing contracts between a government and a manufacturer, and Mamani, Adida and Dey (IIE Transactions on Healthcare Systems Engineering 2, 2012) studied subsidies that coordinate the vaccine market.
Arifoğlu and Tang (2022) design one program for both sides at once: a vaccination incentive for individuals and a transfer payment for the manufacturer, both contingent on the realized supply . A lump-sum tax completes it. The mission formalizes the paper's headline: this modified program attains the social optimum, balances the planner's budget in expectation, and lets the planner divide the optimal welfare between individuals and manufacturer at will.
The manufacturer plans an input quantity . The realized supply is , where the yield is random with law and finite mean, the wholesale price is , the cost per planned unit is , and .
A unit mass of individuals have infection costs uniform on , so and . A healthy individual enjoys , and vaccination costs . If a fraction is vaccinated, an unvaccinated individual is infected with probability and a vaccinated one with probability . The zero-risk fraction is the least at which the population risk vanishes (or ), and Assumption 1 of the paper imposes monotonicity, convexity and concavity conditions on and below .
When only individuals with cost above a threshold seek vaccination, the vaccinated fraction is , the fill rate under random rationing is , and the ex-post welfare is minus vaccination costs minus the expected infection losses. The planner's threshold maximizes ; its demand is
where is determined by the sign of the marginal social benefit . The planner's ex-ante problem is , with maximizer .
Without a program, individuals use the equilibrium threshold : the least cost at which the marginal individual strictly gains from seeking vaccination, , given the fraction that threshold induces. With an incentive , the right side becomes , giving . The program is
with a free constant . The planner's net payment is , and the constant is evaluated at .
With :
In addition, the manufacturer's profit-maximizing quantities are socially optimal, makes the manufacturer better off than without a program, and makes the individuals better off. Here and are computed at any equilibrium production of the chain without a program.
Proposition 7 says a planner can implement the first-best vaccination outcome under random yield with no expected subsidy. Any division of the first-best welfare is also achievable, which is what makes the program implementable: it can be tuned so that both the manufacturer and the population prefer it to the status quo. Propositions 5 and 6 isolate the two halves. The incentive aligns individual thresholds with the social optimum supply by supply, and the transfer makes the manufacturer's profit equal to social welfare up to a constant.
The results are proved in the paper and its Online Supplement; none is formalized anywhere. The mission adds three things. First, a machine-checked model of a supply chain with a consumer externality and an equilibrium threshold, which no existing formal library has. Second, corrected statements where the printed ones fail: Lemma A.1(ii) needs strict convexity, and Proposition 1's uniqueness fails at and at . Third, an explicit equilibrium concept, the least-strict-gain threshold used in the proofs, under which the coordination claim holds.
The algebra of Proposition 7 is short once coordination is known: pointwise, , and the individuals' utility collapses to . The difficulty is in coordination itself, Proposition 5(i). The marginal individual's gain must vanish exactly at and be positive above it. Above that rests on Assumption 1(iv) holding strictly. Below , where the induced fraction is capped by supply rather than by demand, a separate argument is needed. Under the fixed-point reading of equilibrium, every individual is indifferent at and coordination fails, so the threshold rule must be used exactly. Proposition 1 needs a piecewise analysis of across the point where demand meets supply, with derivatives taken one-sided at and through the kink at . Proposition 2 needs differentiation under the integral with a moving upper limit.
The model is a structure of data (, , , , , , and the law of , a measure on ) plus a predicate Standing bundling every standing condition:
The formalization commits to these conventions:
derivWithin on , and Assumption 1(ii) is imposed on ;Two corrections carry added hypotheses: strict convexity in Assumption 1(iii) for Lemma A.1(ii) and the uniqueness part of Proposition 1, and a density of for the first-order condition (10).
Trivializing formalizations are ruled out. The thresholds , and are computed from the primitives, never passed in as parameters. The manufacturer's choice under the program is concluded, not assumed. The infimum defining is over a nonempty set, and is inserted into the threshold set, so no junk value of or of a division by zero enters a statement.
A complete development needs one-sided derivatives of convex functions, piecewise monotonicity arguments, and dominated differentiation under the integral sign. The threshold-equilibrium layer is reusable for other vaccination and rationing models. Proofs of any milestone are welcome, as are formalizations of the decentralized results the mission omits: Proposition 3 (decentralized demand) and Proposition 4 ().
Spare parts for capital goods (aircraft, defence systems, industrial machinery) are slow-moving and expensive to stock, and an unplanned stock-out idles the equipment they serve. Industrial additive manufacturing (3D printing) lets a part be produced close to where it is used, with short lead times and small batches. An original equipment manufacturer (OEM) that owns the design can therefore sell an IP license to its buyers instead of the parts themselves, letting each buyer print locally through a third-party printing service provider. The US Army's directive on advanced manufacturing (Department of Defense 2019) and commercial digital-inventory platforms are examples of this practice.
Zhang, Westerweel, Basten and Song (MSOM 2022) model the OEM's choice of license terms when buyers decide rationally between the two channels. The license has two classical components from the licensing literature (Kamien and Tauman 1986): a fixed annual fee and a per-unit royalty. The paper's main finding is about a single standard license offered to buyers of different sizes. A positive royalty can then be optimal under symmetric information, and all three supply chain configurations arise: centralized, decentralized and hybrid.
There are buyers . Buyer has Poisson demand with annual rate . All buyers share a holding-cost rate and a safety factor .
Traditional channel. The buyer orders from the OEM at wholesale price , with fixed ordering cost and lead time . Its expected annual cost is
The OEM produces at unit cost and earns from this buyer.
Licensing channel. Under a license with fixed fee and royalty , the buyer prints at price , with fixed ordering cost and lead time . Its expected annual cost is
and the OEM earns from it.
Surplus and choice. The surplus of buyer is , and its maximum surplus is . The licensees are ; the others stay in the traditional channel. The OEM's profit is
For two buyers with and , two kinds of royalty matter. The maximum royalty fees solve . The equalizing royalty solves .
Let be the least upper bound of . In each of the three cases of Table 1, is the largest profit in that case's column:
Each listed license realizes its profit and channel selection. Row iv of Case I is reached only as a limit . Any license that leaves both buyers with negative surplus earns . The optimal value is nondecreasing in .
In the paper's order, the milestones are:
The result gives a closed characterization of the optimal standard license for two nonidentical buyers. Three features follow from it. A royalty-only or mixed license can beat a fixed fee, unlike the identical-buyer case. The larger buyer can be deliberately kept in the traditional channel. The OEM's optimal profit rises with the wholesale price. These are the paper's managerial conclusions about distributed 3D printing, and the numerical study in §5 builds on them.
The result is proved in the paper (appendix, pp. 2699–2701), with several steps described as straightforward and Cases II and III left to the reader. As far as is known, none of it has been formalized. A machine-checked proof would supply the omitted cases and pin down the boundary behaviour. On the boundary, two entries of Table 1's channel-selection column need strict inequalities that the table does not print. The formalization adds the platform's first IP-licensing model, built on closed-form inventory costs.
The surplus is an explicit function, but the optimization is over a two-dimensional license space. The licensee set changes discontinuously across the curves and . One might reduce the problem to comparing a handful of candidate licenses evaluated at their formulas. That reduction is exactly what has to be proved: every license must be shown to be dominated by one of the candidates, region by region. In one region the supremum is approached and never attained, so no maximizer exists. The single-crossing property behind depends on a sign of a mixed derivative that fails without . The final claim, monotonicity of in , must hold across changes of case as moves, while itself moves with .
Fin n. For two buyers, the paper's Buyer 1 is index 0 and Buyer 2 is index 1. All parameters are real.IsLUB), never through sSup, whose value on an unbounded set is a junk . The royalties , and are bound by their defining equations, not left free. "" means any license under which every buyer has negative surplus.A cryptocurrency launched through an initial coin offering is often sold before the platform it serves has users. Its value to a buyer then depends on who else buys: a token that gives access to a trading network is worth more when many households with large endowments join. Sockin and Xiong (preliminary draft, March 2018, later published in Management Science) build a tractable rational-expectations model of this complementarity, in which the price of the currency is pinned down jointly by households who buy memberships and by miners who supply them. The perfect-information benchmark of the paper, in which the platform fundamental and the mining-cost shock are publicly observed, already shows the central phenomenon: the market can have two self-confirming equilibria, one with a high price and broad adoption and one with a low price and narrow adoption, and they respond to fundamentals in opposite directions.
The model belongs to the literature on multiple equilibria from strategic complementarities (Morris and Shin 1998) and on search models of money (Kiyotaki and Wright 1993), applied to a market in which the supply side is a population of miners with heterogeneous costs.
There are two dates. A continuum of households has endowment exponents with , where is the platform fundamental. At a household is randomly matched with another; if both own the currency, they trade, and with Cobb–Douglas utility
the competitive allocation of the matched pair gives household the realized utility . A household that does not trade gets zero utility.
At each household decides whether to buy one unit of the currency at price . It buys exactly when its expected utility , the expectation over its partner's of on the event that the partner also buys, is at least . Miners have productivity with , receive a share of the proceeds, and mine exactly when . The developer keeps the share , so its revenue is times the mass of buyers. The ex ante utility is .
An equilibrium at is a measurable purchase set of endowment exponents and a price such that the households in are exactly those whose expected utility, computed with partners drawn from , is at least , and the -mass of equals the mass of miners who mine at . In the Lean development these are IsEquilibrium P A xi B price and equilibria P A xi, in the namespace CryptoMembership.PerfectInfo.
There is a threshold such that there are exactly two equilibria when , one when , and none when . Moreover:
The milestones follow the proof in Appendix A: the matched-pair allocation and utility of Proposition 1; the closed forms of and ; optimality of cutoff strategies; market clearing as equation (13); the reduction of equilibria to the roots of equation (15); the log-concave bell shape of the left side of (15); the two–one–none root count; and the opposite movement of the two roots as the right side falls.
Proposition 2 is the paper's characterization of adoption equilibria with observable fundamentals. It explains why a token market can sustain both a high-price, broad-adoption outcome and a low-price, narrow-adoption one, why the latter reacts perversely to good news about the platform, and why a platform below a fundamental threshold attracts no buyers at all. The later sections of the paper build the unobservable-fundamentals analysis on the same equation.
Formalizing it produces a complete, checked equilibrium analysis of a nonlinear rational-expectations model: the equilibrium is defined from optimization and market clearing over arbitrary measurable purchase sets, and the count of equilibria is stated as an exact trichotomy rather than "generically". As far as is known, no part of this paper has been formalized. The development also requires facts about the Gaussian distribution that are reusable elsewhere, notably strict log-concavity of the standard normal cdf and truncated Gaussian moment generating functions.
The reduction to a scalar equation is mechanical once one knows that equilibria are cutoff sets; that step must be proved for an arbitrary measurable purchase set rather than assumed, as the paper does when it announces the cutoff form as a conjecture on p. 15. The equilibrium count rests on strict log-concavity of , which is not in Mathlib, and on the tail behaviour of against an exponential. The comparative statics of are not a direct consequence of the root statics: depends on both the price and the cutoff, and its monotonicity in the low-price equilibrium has to be established without the sign error in the paper's own derivative computation.
All quantities are real. Normal laws are Mathlib's gaussianReal with variances and , and is the cdf of gaussianReal 0 1. The standing assumptions , , , are bundled in Params.Standing. Ties are broken as on the page: a household buys when expected utility equals the price, and a miner mines when its revenue equals its cost. The mining cost is as in (4); display (5) prints , which yields the same mass of miners. Prices are positive. Equilibria are counted with Set.encard over pairs (purchase set, price). The high- and low-price equilibria are the cutoff equilibria with the smallest and largest cutoff. "No household buys" is stated as "no equilibrium exists", since with a positive price the miner mass is positive and the empty purchase set cannot clear. Part 3 is stated as printed in the proposition, not as the proof's final display, which has the wrong sign for the low-price equilibrium.
The equilibrium is not defined as a root of equation (6): defining it that way would make part 1 empty. Purchase sets range over all measurable sets.
A complete development needs Gaussian integrals of exponentials over half-lines, strict log-concavity and tail limits of , and a two-root lemma for strictly log-concave functions vanishing at both ends. These are reusable beyond this mission. Contributions to any milestone, or to these Gaussian facts as separate lemmas, are welcome. The unobservable-fundamentals setting (Proposition 3) is not part of this mission.
A neural network can change its behavior substantially when both its width and its training duration grow. For a network with two hidden layers, the parameters of the layers interact during training, so a large-width description must account for the output of the actual optimization algorithm. Sirignano and Spiliopoulos study this question for online stochastic gradient descent (SGD) under a mean-field normalization. Their Theorem 2.3 identifies the limit of the trained network when the first hidden layer grows, followed by the second, and gives a rate for the intermediate second-layer approximation. The result concerns a trained network: all three families of weights evolve at every SGD step.
The normalization matters. Each hidden layer contributes an average, with factors and for the first and second widths. The learning rates depend on those widths, so the output can continue changing on the time scale of SGD steps. The paper notes that a different scaling may lead to a different limiting equation or to no nontrivial training behavior at large width. A precise statement therefore needs the finite network and its SGD updates alongside the limiting equations, not merely a claim about an abstract mean-field flow.
Let be an input dimension and an input. A two-hidden-layer network has first-layer units and second-layer units. Its parameters are output weights , first-layer vectors , and second-layer weights . With an activation , its output is
Training samples are independent draws from a probability law supported on a compact product . The three initial weight families are mutually independent and identically distributed within each family, with laws , , and . Each law has a continuous density and compact support. The activation is twice continuously differentiable and, as the paper's notation requires, it and its first two derivatives are bounded. These are the standing conditions of Assumption 2.1.
At each step, SGD updates all parameters from the same previous parameter state and the same sample. The learning rates in equation (2.1) are , , and , applied with the step-size denominators in equation (1.4). The output at time is the output after updates. For fixed , the first-width limit is described by an -particle system. Its first-layer particle retains both its initial first-layer vector and the full vector of its second-layer initial weights, because its dynamics depend on all of them. The second-width limit is a limiting integro-differential system for representative paths , , and .
For and , the target is the existence and uniqueness of the limiting system (2.6), together with
The order is fixed: grows first while is held fixed. The goal states the entire Theorem 2.3, including the existence clause; without existence, convergence quantified only over solutions would have no content.
For the particle output , the same theorem gives a constant such that
The attack path records the finite-particle well-posedness of Lemma A.5; the first-width output limit stated after Lemma 2.2; the uniform particle bound (5.5); the sampling-variance estimate (5.9); the mean squared particle-error estimate (5.15); the output rate from Section 5.8; and uniqueness from Lemma 6.1. Each is a stated result or displayed assertion in the source. The rate and uniqueness milestones are also conclusions of the goal theorem.
The theorem specifies what the output of this trained network approaches, rather than only describing the parameters of a network at initialization. It connects the discrete SGD recursion to a finite particle system and then to a deterministic output from a limiting system. The bound makes the second-width approximation quantitative, while uniqueness makes the limiting output independent of the choice of representative solution. These claims provide the basis for the paper's later discussion of global convergence under stronger assumptions; they do not themselves assert that training reaches a global minimum.
The paper proves the first-width and error estimates and gives a uniqueness argument for the limiting system. It asserts existence of a solution to (2.6) in Theorem 2.3, although a separate existence proof is not supplied there. A complete machine-checked development must account for that clause as well as the known arguments. No proof of this mission's goal or milestones is currently included in the draft Lean statements; they are targets for solvers. The network model, initialization law, and particle equations can also serve as reusable interfaces for further formal work on trained wide networks.
A direct large-width argument cannot treat the two widths as one undifferentiated limit. With fixed, the shared first-layer weights couple all second-layer units. The first limit is a stochastic statement about the SGD iterates and a particle system whose state includes a vector of initial second-layer weights. Only after that limit can the fluctuations be controlled. The second stage must bound both the sampling fluctuation of the representative output and the discrepancy between the particle paths and the limiting paths. The source's existence assertion also needs a mathematical justification in the specified continuous-solution class. Simply taking a pointwise limit of the network formula leaves all of these issues unresolved.
Lean uses EuclideanSpace ℝ (Fin d) for inputs, Fin N_1 and Fin N_2 for neuron indices, and Measure.pi or Measure.infinitePi for independent initial weights and data. The arrays of all widths live on one probability space with the stated product law. The SGD recursion is the simultaneous update (1.4), with the exact factors from (2.1), and time uses . The representative and particle systems are written in integral form. Solutions are jointly continuous on times the compact supports of their initial states; this supplies the regularity needed for the integrals and matches the class used in Lemma 6.1. No nonempty-input-set assumption or monotonicity assumption on is added.
The inner probability limit in the goal uses a limsup in . Footnote 2 writes an inner limit but does not assert its existence at every probability threshold; the limsup version implies its claim whenever that inner limit exists. A single rate constant works for all , all positive , and all . The particle state includes the full vector of initial values, and the conditional expectation defining its second-layer preactivation is an integral over their product law at fixed initial values. The finite network, particle system, and limiting system must be connected by the stated results; an arbitrary output function with the desired limit would not formalize this theorem.
A complete development needs probability measures on product spaces, integrals of continuous functions on compact supports, convergence in measure, finite-sample variance estimates, and existence and uniqueness theory for the coupled integral systems. Contributions to these pieces and to the stated milestone theorems are within scope. The measure-valued Skorokhod-space statement of Lemma 2.2, numerical experiments, and the paper's separate global-convergence theorem are outside this mission.
When a new durable product is launched, demand typically follows a diffusion curve. A few innovators buy on their own, and later buyers, the imitators, are drawn in by word of mouth from earlier adopters. Bass's diffusion model (Bass 1969) is the standard description of this process and is used throughout marketing and operations to forecast the sales of new products.
In a closed-loop supply chain the producer also collects products returned at the end of their use, remanufactures them and resells them, often at a higher unit margin than new items. Returns arrive only after units have been sold and used, so early in the life cycle there are few of them. Nadar, Kaya and Güler (MSOM 2021) ask whether a producer can gain by deliberately rejecting part of the demand early on. Rejection slows diffusion, but backlogged customers return later, when accumulated returns allow them to be served with higher-margin remanufactured units. Their Theorem 1 gives conditions under which this partial fulfillment is optimal, and conditions under which it is not.
This mission formalizes the second kind of condition, a sufficient condition for immediate fulfillment (meeting all demand in every period) to be optimal, together with the model it is stated in and the diffusion comparisons it rests on.
A producer sells over periods . A sales plan chooses new-item sales and remanufactured-item sales , with total sales and cumulative sales , .
Diffusion. Only satisfied customers spread word of mouth. With market size , coefficient of innovation and coefficient of imitation , the diffusion demand in period is
When all demand is met, and (1) is the original Bass process .
Segments and backlogs. A fraction of arriving customers wants only new items. The remaining fraction buys remanufactured items when available and new ones otherwise. A fraction of unmet demand is backlogged one period and the rest is lost. The backlogs of the two segments follow the two-case recursion (4) of the paper.
Returns. A fraction of the units sold in period comes back in period . The return volume available for remanufacturing is , (6).
The producer's problem. Maximize subject to
The standing assumptions are , , , and .
Immediate fulfillment. The immediate-fulfillment plan meets all demand and serves remanufactured-item demand from returns as far as possible. Its return volume is , and it sells
If for , then is feasible, and every feasible plan satisfies
The condition says that, under immediate fulfillment, returns never exceed remanufactured-item demand, so there is never a surplus of returns that delayed customers could absorb.
The result separates the two forces in the paper. Lemma 2 says that rejection always costs diffusion, so its only possible benefit is a better use of returns. The goal shows that this benefit disappears when returns are scarce in every period. Theorem 1(b) and Corollary 1 then show that partial fulfillment can win when returns become abundant before the horizon ends. Together these results give a threshold structure that producers in fast-clockspeed industries, such as smartphones in the paper's numerical study, can check from the immediate-fulfillment trajectory alone.
The results are proved in the paper, with every proof in an online appendix. This mission produces machine-checked statements and, eventually, proofs of the fully posed part of Theorem 1 and of the diffusion comparisons beneath it. No part of this model has been formalized before. The discrete Bass process and the sales-dependent diffusion recursion are reusable for other diffusion-based sales-planning models.
The obvious argument compares profits period by period, and it fails. A feasible plan that rejects demand in some period can sell more than in later periods, because backlogged customers return and because can be positive. Profit is therefore not dominated termwise. The comparison has to be made over cumulative quantities. One must control cumulative sales against the Bass trajectory along the whole horizon, through the nonlinear recursion (1). One must also control total remanufactured sales through the return recursion (6), whose lags couple every pair of periods. The backlog recursion (4) branches on the plan, which rules out a closed form.
Params with real m p q alpha gamma2 pn cn pr cr, a horizon T : ℕ and beta : ℕ → ℝ. The standing assumptions are a predicate Standing.n r : ℕ → ℝ, read only on periods .Finset.Icc/Finset.Ico, induction along the recursions, and monotonicity of on . Contributions of auxiliary lemmas, such as nonnegativity of the Bass trajectory and , are welcome.A manufacturer that sells through an independent retailer charges a wholesale price above cost, and the retailer then adds its own margin: the double marginalization problem of vertical contracting. Anand, Anupindi and Bassok (Management Science 2008) showed that in a two-period monopoly chain the retailer can blunt this by buying more than it sells in the first period and carrying the excess into the second. This strategic inventory makes the retailer less dependent on the manufacturer's next wholesale price, which forces that price down, and in their model both firms gain.
Li, Li and Chen (SSRN 3003887; Manufacturing & Service Operations Management, 2021) ask whether the conclusion survives when two such chains compete. Their answer is that strategic inventory still arises, but under fierce enough competition it hurts every firm. The mission formalizes that result.
There are two supply chains ; denotes the rival chain. Each consists of a manufacturer with zero production cost and an exclusive retailer. There are two periods . In period the demand for product is
where is retailer 's price and measures the intensity of chain-to-chain competition.
The game has four stages. In stage 1 each manufacturer sets a wholesale price . In stage 2 each retailer sets and orders enough to cover demand plus a carryover , held into period 2 at unit holding cost . In stage 3 each manufacturer sets . In stage 4 each retailer sets and orders whatever demand its carryover does not cover; unsold units are worthless.
Contracts are unobservable: firms of chain see neither , nor the orders of chain , nor . The equilibrium is a perfect Bayesian equilibrium with passive beliefs. At every history of its own chain, a firm keeps believing that the rival charges its equilibrium-path prices , and acts optimally given that belief and the continuation play of its own chain.
Two games are compared. In the SI game each chain may carry any . In the NI benchmark, "a manufacturer only delivers whatever its downstream retailer can sell", so . Manufacturer 's profit is . Retailer 's profit is its revenue minus its wholesale bills minus .
Let . There is with such that for every , every SI equilibrium and every NI equilibrium satisfy
and equilibria of both games exist. Conversely, if or , no strategic inventory is carried in any SI equilibrium. The goal leaves unspecified, as the paper does: it asserts the shape of the comparison, not a numerical threshold.
The result. Proposition 2 overturns the monopoly-chain conclusion. Carryover still lowers the second-period wholesale price, but under competition that lower price feeds a fiercer price war between the chains, and the gain from softened double marginalization is lost. Because contracts are unobservable, no chain can commit to holding no inventory, so the firms end up in a situation every one of them would prefer to avoid. Proposition 3 sharpens the point: near the threshold a higher holding cost raises every firm's profit. A carrying cost, normally a pure loss, here acts as a commitment device.
Formalizing it. The paper's proofs are in an online appendix, which is not part of the source; the equilibrium notion is named on p. 8 but not written out. A machine-checked proof would supply both. It would pin down the equilibrium concept: what a passive-beliefs perfect Bayesian equilibrium of a two-chain, four-stage game is. It would establish that Table 1 is the unique equilibrium outcome, including against asymmetric profiles. It would derive the retailer's SI profit, which the page does not print. None of these results has a machine-checked proof.
Each stage payoff is piecewise quadratic, with kinks where demand reaches zero and where carryover covers period-2 demand. Table 1 must be shown optimal against all deviations, not only local ones, at every off-path history of a chain: a retailer that deviates in its carryover changes its own manufacturer's second-period price, and that response has to be the equilibrium one there too. The tempting shortcut is to solve the first-order conditions of a symmetric profile and stop. It establishes neither global optimality nor that asymmetric equilibria share Table 1's outcome. The goal quantifies over every equilibrium of both games, so both are needed.
The model is a single definitions file, ChainCompSI.Backfire.Model. It has the following parts:
demand, and sales ;Hist and pure profiles Profile with one strategy per stage;IsEq θ h si E, where si : Fin 2 → Bool selects SI or NI per chain;w1, p1, inv, w2', p2', D1, D2;mfrProfit () and retProfit ().Chains are Fin 2, with rival 1 - i. All quantities are real.
The formalization commits to the following conventions, each disclosed in the items:
Every statement of the form "in equilibrium, …" also asserts that an equilibrium exists, so none holds vacuously. The goal is stated about equilibria of the games, not with Table 1's closed forms substituted. A version comparing the two columns' rational functions would be a lemma of the proof, not Proposition 2.
Not formalized:
si flag leaves room to pose it later;Contributions welcome:
An online platform can know more about a product than a customer arriving for a short sales campaign. It sees earlier customers' purchase decisions and the messages it sent them, while a new customer sees only her own message and private assessment. Choosing what to disclose can raise immediate sales, but a customer's response can also reveal information that improves later messages. Küçükgül, Özer and Wang study this tension for a fixed-price campaign and reduce the platform's dynamic information-design problem to a linear program in their submission manuscript, §§3–4, pp. 7–18.
The mission concerns that reduction, stated as Proposition 5 and equations (9)–(11) of the November 2019 submission manuscript. Its original problem permits a message distribution that depends on the full private history. Its optimization variables after reformulation instead track an integer summary and three possible recommendations. The gap between those two descriptions is the main mathematical content that a formal proof must justify.
A time-locked sales campaign has customers arriving one after another at a fixed price . The product value is either or , with common prior . Customer observes a private signal ; conditional on , signals are independent, and for . She receives one message from the platform, then buys when her posterior value reaches , with equality resolved in favor of buying. These are the primitives of §3 and equations (1)–(2) of the manuscript.
An information provision policy selects a distribution over messages using the platform's history of earlier messages and purchase decisions. The customer does not see that history. The platform's expected revenue is . The target value is the best revenue over all such policies in equation (3), not a value assigned by the reduced program.
Two belief thresholds determine how a message affects buying: and . A recommendation policy uses messages , , and to recommend buying, following the private signal, and declining. The net purchase position counts purchases minus non-purchases among customers given the neutral recommendation. Section 4 defines and . This turns the history distribution into masses and the message probabilities into , where . The linear-program variables are their products ; see Propositions 1–5, pp. 11–18.
For parameters in the paper's focus region , the goal states a common value for the original policy problem, recommendation formulation (9), and LP (11):
The goal also says that every LP optimum recovers an optimum of (9) through equation (10), taking any probability vector of recommendations where . The first two maxima include attainment. The original-policy value is expressed as a supremum because the manuscript's weak incentive inequalities permit endpoint ties that may change the customer's actual response under (2); this reading is disclosed in the paper's Proposition 5 and proof, pp. 18, 42–43.
The milestones trace the source's claims: Proposition 1 classifies buying behavior; Proposition 2 restricts attention to recommendations; Proposition 3 identifies the net purchase position as a sufficient statistic; equation (9) states the original-to-reduced value identity; and equations (B.17)–(B.18) express the two directions between (9) and (11). Proposition 4's random-walk identity remains in the definition of feasibility for (9) and (11), though it is not a separate milestone in this proposal.
Proposition 5 replaces a search over history-dependent information policies with a finite linear program whose variables have the interpretation of joint state-and-recommendation probabilities. For a fixed campaign length, the LP has variables before redundant positions are removed. This gives the computational representation used in the paper's later numerical comparison and recommendation-policy examples; see §4.3, pp. 18–20.
The result is proved in the authors' manuscript. The local Lean files for this mission compile as statements with proof placeholders; they do not yet contain machine-checked proofs. Completing the mission would provide a checked bridge from a sequential Bayesian policy model to its reduced finite-state program and LP, with reusable definitions for the joint law, Bayesian response, and state evolution.
The change of variables is only the final step. The difficult claim is that optimizing over full proprietary histories and arbitrary messages gives the value of a program whose policy uses only three recommendations and the integer . A receiver's choice is endogenous: the message affects what she believes, her private signal affects whether she buys, and the platform observes the resulting decision. Defining customer behavior as automatic obedience would erase that difficulty. The paper's endpoint inequalities add another issue: at equality a nominal recommendation can differ from the purchase rule, so value comparison must keep the tie convention visible. These are the distinctions between equations (2), (3), (9), and (11) of the manuscript.
The Lean model uses real probabilities, a Boolean product value, Boolean signals and purchase decisions, and SignType for the three recommendations. It builds the joint distribution of and the proprietary history one customer at a time. Every customer buys by the joint-probability form of rule (2), including a tie; obedience is a property checked on realized signal–message pairs. Histories of length precede paper customer , while (9) and (11) keep the source's one-based time index. The state range is , with zero mass outside and zero boundary terms in the recursions.
The policy class has an arbitrary finite message type. This matches the sums over histories in Appendix B and includes the three-message policies. The assumptions retain , , and when allowed by the stated region; the definition of uses a two-sided product expression so a negative exponent never acts on zero. The reduced programs use exactly the four printed weak incentive inequalities. State masses are nonnegative, as required by their meaning as probabilities. Real-number maxima are stated with IsGreatest, and the original-policy supremum with IsLUB; no default value of a real sSup is used.
The original-policy value is taken over all information policies with Bayesian response, rather than being defined by (9). The source's correction at , the interpretation of recommendation obedience, the finite-message restriction, and the supremum reading are explicit audit points. A full development needs finite probability calculations, conditional belief identities, and equivalence between histories and net positions. The model and these supporting lemmas can be reused for later formal work on sequential persuasion in the same paper.
A blockchain miner pays for electricity and equipment while block rewards arrive at irregular times. A strategy that raises the average reward can still expose a miner with limited capital to ruin before those rewards arrive. Albrecher and Goffard study this tension for a simplified selfish mining strategy in which the miner temporarily withholds a discovered block. Their model connects the block discovery process to a dual risk process: capital falls continuously as costs accrue and jumps upward when the miner collects block rewards. The quantity of interest is the miner's expected remaining capital at a random evaluation time, counting paths that have already reached ruin as zero. The paper derives a closed expression for this quantity when the miner begins with no withheld block. Albrecher and Goffard, arXiv:2010.12577v1, §§2–3.
Network blocks are discovered at Poisson rate . The miner has a share of computing power, pays operating costs at rate , and receives per block for which the strategy earns a reward. On each discovery, records whether the miner found the block. If the miner has produced a fork and another participant finds the next block, records whether that participant extends the miner's branch; its probability is .
The state just before discovery records an empty buffer, one withheld block, or a public fork. From state , the miner withholds a newly found block and earns nothing. From state , a further miner discovery pays for two blocks and returns to ; a competing discovery creates a fork. From , the next discovery resolves the fork and returns to . It pays two rewards if the miner finds the block, one reward if another miner extends the miner's branch, and no reward otherwise. These cases define the reward count and the surplus
where is initial capital and is the number of network discoveries by time . The ruin time is . For initial state , the fixed-horizon value is . The paper replaces a fixed horizon by an independent exponential time of mean and defines . Thus the exponential law has rate . Source, equations (15), (16), and (19).
The goal is Theorem 3.1 for the initially empty buffer. Let be the parameter expressions in the paper's equation (22). Let and be precisely the roots with negative real part of
For satisfying the corrected boundary system (23), the target is, for all ,
The paper prints the third right-hand side of (23) as . Its boundary condition (33), together with its own coefficients (24), requires . The mission states this correction explicitly. Source, Theorem 3.1 and equations (23), (24), (33).
The three curated targets are the corrected advanced differential system (29) for the three starting states; Lemma A.1, which counts three characteristic roots in the left half-plane when ; and the explicit function in (39)–(40), including its corrected boundary equations. These are statements made in Appendix A and used in the discussion of Theorem 3.1. The root-count lemma has the narrower hypothesis that the authors print; the main result permits and while specifying the root set. Source, Appendix A.
The formula gives expected remaining capital for a specific block-withholding policy while accounting for the event of ruin before the evaluation horizon. It allows the model's cost rate, reward size, hash share, connectivity, and initial reserve to be compared through the same value function. The result addresses the limited-capital question that an average revenue rate alone does not answer. Its use is within this simplified strategy and the paper's Poisson and independent-mark assumptions. Source, §§3–4.
The result is presented in the paper, but a machine-checked proof of this corrected statement is still to be supplied. A complete development would establish the expectation's measurability and integrability, the differential properties of the three state-dependent value functions, the complex root count, and the identification of the explicit function with the expectation. The stochastic model and its value function can also support separate formalizations of the paper's ruin-probability and honest-miner results.
The reward at a discovery depends on withheld-block state, so the surplus alone does not describe the next reward. The value functions for all three states are coupled, and the resulting differential equations evaluate the empty-buffer function at larger reserves and . Those advanced terms prevent a direct application of ordinary differential-equation uniqueness results. The root count is a statement about a transcendental complex equation, and its left-half-plane roots must be isolated exactly.
Appendix A says that it constructs a solution of the advanced equation and assumes uniqueness, observing that simulations can check the result. That assumption leaves an identification step between the displayed candidate and the stochastic expectation that the paper does not prove. It remains part of the goal, without an invented source milestone. Source, p. 25.
Lean represents the network process through independent exponential interarrival times of rate and independent Bernoulli marks. Marks begin at index zero in code, corresponding to the paper's first block at index one. The state transition and reward map encode the cases of (16). The ruin time is extended nonnegative, so an empty set of ruin times has infimum . On the null event of infinitely many arrivals in finite time, the cardinality-based block count has Lean's default value zero; the model law excludes that event almost surely.
The horizon average uses the first expression in (19), integrating against the exponential measure of rate . The expected surplus must be obtained from this stochastic construction; defining it by the closed formula or by a differential equation would erase the target. The roots and coefficients are constrained by the characteristic equation and corrected boundary system, and integral defaults on nonintegrable inputs cannot establish the result. No net-profit condition is imposed on Theorem 3.1.
The paper-specific definitions, the three curated milestones, and the main theorem are open to contributions. General infrastructure for marked Poisson processes, extended ruin times, integration of stopped surplus, and complex root counting would be reusable beyond this case. The four printed discrepancies affecting (23), (29), (31), and (40) are recorded in the local moderation notes; this mission's Lean statements use the mathematically corrected forms.
Firms increasingly price with algorithms they do not write themselves. A retailer, a hotel or a gas station often licenses its pricing software from a third-party vendor, and competing firms may license the same product. Competition authorities have asked whether this matters: if the vendor designs its algorithm knowing that the algorithm may end up setting the prices of rival firms, the design may soften competition even when no firm intends to collude. Earlier work on algorithmic collusion asks whether learning algorithms that firms run on their own discover collusive strategies (Calvano, Calzolari, Denicolò and Pastorello, AER 2020). Harrington's paper asks a different question about the design incentive of a single vendor, in a static model with no learning and no repeated interaction.
The paper (working paper Third Party Pricing Algorithms and the Intensity of Competition, 3 November 2020; published as The Effect of Outsourcing Pricing Algorithms on Market Competition, Management Science, 2022, doi:10.1287/mnsc.2021.4241) shows that the vendor's own objective is enough to raise prices. This mission formalizes the general-demand result of its Section 4.
Two firms sell differentiated products at a common constant marginal cost . Firm 1's demand is , where is firm 's price and is a demand state. Demand is symmetric: firm 2's demand is . Profits are
Prices lie in . Demand is twice continuously differentiable, falls in the own price, and rises in the rival's price and in (2). The own-price derivative is non-decreasing in the rival's price and in (3). Each firm's profit has a negative own-price second derivative (5), and is strictly concave in its own price. The joint profit is strictly concave, with maximizer non-decreasing in , and .
The demand state changes faster than a firm can reprice by hand. Firms share a prior with continuous density on . A firm that prices on its own cannot condition on . A pricing algorithm , sold by the third party, can. Given that one firm adopts the algorithm, both adopt with probability . The third party designs to maximize the adopter's expected profit,
where is the price of a non-adopting rival. With weight , the algorithm faces a copy of itself.
An equilibrium , (11), is an algorithm and a non-adopter price such that:
Equilibria are ordered by . The minimal equilibrium is the one with the least .
For each lowest state there is such that, whenever , for every density on , a minimal equilibrium exists for every , and for
The goal asserts only the direction of the effect. It fixes no constants and needs no closed form for the equilibrium.
Theorem 2 identifies a channel through which outsourcing raises prices. A vendor whose product may compete against itself has an incentive to internalize part of the competition between its clients. It does so without coordinating the firms and without conditioning on whether the rival adopted. The non-adopting rival responds to the higher algorithmic prices by raising its own price, because prices are strategic complements. In Section 5 of the paper (linear demand), the same mechanism yields prices above the competitive level even when only one firm adopts. Theorem 2 is the general-demand statement that this direction of effect does not depend on linearity.
The paper proves the result on paper; it has no machine-checked proof. Formalizing it requires a library for parametric optimization on an interval: continuity and strict monotonicity of the maximizer of a strictly concave objective in a parameter, with derivative conditions on sections. It also requires least fixed points of monotone self-maps of an interval, and comparative statics of those least fixed points when the map moves with a parameter. These pieces recur across oligopoly theory and the theory of supermodular games.
The standard tool for "least equilibria rise with a parameter" is Milgrom and Roberts' theorem: if the fixed-point map is increasing in both the price and the parameter, its least fixed point is increasing in the parameter. That theorem cannot be applied here. The author notes he could not show that the non-adopter's best response is increasing in for all . The algorithm's price rises with only below the joint-profit price . Above it, the extra weight on facing itself pulls the price down. The argument therefore has to locate the minimal equilibrium below uniformly over the support, which is why Theorem 2 assumes a small spread . It must then show that the needed monotonicity in holds on the region where the least fixed point lives. The paper proves Lemma 4 at each point (an at each ), and the theorem needs it over a whole interval of .
All statements live in the namespace ThirdPartyPricing.General and import one definitions file, ThirdPartyPricing.General.Model.
SymmetricDuopoly holds , , and (D). The paper-specific Primitives extends it with an ambient range of demand states and (pM).Standing collects them, with partial derivatives written as deriv of one-variable sections, and is on .IsDensity) replaces the cdf . Expectations are interval integrals.IsEquilibrium is the pointwise form (11), which the paper states is equivalent to (10). IsMinimalEquilibrium and IsMaximalEquilibrium order equilibria by .Conventions that differ from a literal reading of the page:
The goal quantifies over every pair satisfying (11) and asserts that minimal equilibria exist, so it cannot hold vacuously. It does not use the closed forms (12)–(13) of the linear case. The full-information benchmarks , , the moments , and the linear-demand Properties 1–3 are not part of this mission.
Contributions are welcome at every level: proofs of the milestones, general lemmas on parametric maximizers of strictly concave functions on an interval, and least-fixed-point comparative statics.
We formalize the task of unitary Schur sampling -- an extension of weak Schur sampling -- which is the process of measuring the Young label and the unitary group register of an input qudit state. Intuitively, this task is equivalent to applying the Schur transform, projecting onto the isotypic subspaces of the unitary and symmetric groups indexed by the Young labels, and discarding of the permutation register. As such unitary Schur sampling is the natural task in processes such as quantum state tomography or spectrum estimation. We generalize this task to unitary mixed Schur sampling to account for the recently introduced mixed Schur-Weyl transform. We provide a streaming algorithm which achieves an exponential reduction in the memory complexity and a polynomial reduction in the gate complexity over na"ive algorithms for the task of unitary (mixed) Schur sampling. Further, we show that if the input state has limited rank, the gate and memory complexities of our streaming algorithm as well as the algorithms for the full Schur and mixed Schur transforms are further reduced. Our work generalizes and improves on the results in arXiv2309.11947.
This mission is the statement-level formalization of A memory and gate efficient algorithm for unitary mixed Schur sampling (arXiv:2410.15793v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Four properties of homogeneous Littlewood–Richardson coefficients (Lemma 11, PDF p. 32). 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We study and solve the problem of distilling secret key from quantum states representing correlation between two parties (Alice and Bob) and an eavesdropper (Eve) via one-way public discussion: we prove a coding theorem to achieve the "wire-tapper" bound, the difference of the mutual information Alice-Bob and that of Alice-Eve, for so-called cqq-correlations, via one-way public communication. This result yields information--theoretic formulas for the distillable secret key, giving ``ultimate'' key rate bounds if Eve is assumed to possess a purification of Alice and Bob's joint state. Specialising our protocol somewhat and making it coherent leads us to a protocol of entanglement distillation via one-way LOCC (local operations and classical communication) which is asymptotically optimal: in fact we prove the so-called "hashing inequality" which says that the coherent information (i.e., the negative conditional von Neumann entropy) is an achievable EPR rate. This result is well--known to imply a whole set of distillation and capacity formulas which we briefly review.
This mission is the statement-level formalization of Distillation of secret key and entanglement from quantum states (arXiv:quant-ph/0306078v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: one-way secret-key coding theorem (Theorem 1, PDF p. 2). 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.
Online advertising exchanges sell most impressions through second-price auctions with reserve prices. A seller who has logged the bids of many past auctions wants reserves that would have earned the most revenue on that history. When the bids are drawn i.i.d. from a distribution, the revenue-optimal reserves on a large sample approximate the revenue-optimal reserves for the distribution (Morgenstern–Roughgarden 2015, cited in the paper's §2). This makes the data-driven problem the computational core of reserve optimization.
With one reserve per buyer (personalized reserves) in the eager second-price auction, the data-driven problem is APX-hard (Roughgarden–Wang 2016). A -approximation was given by Paes Leme, Pál, Vassilvitskii 2016, and the best factor previously known was the of Roughgarden and Wang. Derakhshan, Golrezaei and Paes Leme give a linear-programming relaxation and a randomized rounding that earn a fraction of the optimum (arXiv:1905.01526; Management Science 2022). They also show that the analysis is tight and that the integrality gap of the relaxation is at least .
There is a finite set of auctions and a finite set of buyers. Buyer bids in auction . Two auxiliary buyers bid everywhere. Given a reserve vector , auction proceeds in two steps:
If , then . The eager second-price problem is
Let be the candidate reserves. A valid profile of auction is a tuple with , , and . Its revenue is . The set of valid profiles of auction is , and contains the profiles that give buyer reserve .
Profile-LP has variables (a distribution over profiles of auction ) and (a distribution over reserves of buyer ):
Pro-LPR solves Profile-LP and draws a reserve for each buyer independently with . It then outputs whichever of and the zero vector earns more.
The analysis passes through the nonlinear program (10). For buyers, is the maximum of over with and .
Profile-LP has an optimal solution, and every optimal solution satisfies
The milestones follow the paper's proof:
Lemma 5.4 remains a supporting draft item for Lemma 5.3.
The theorem shows that eager personalized reserves can be approximated beyond the factor by a polynomial-size LP. The LP has only profile variables, whereas the search space has reserve vectors. Lemma 5.1 shows that the rounding can be analyzed auction by auction, and the paper's tightness example shows the constant cannot be improved for this algorithm.
The paper's proof is complete on paper except at one point. Corollary 5.6 relies on Lemma 5.5, a KKT claim that is false as printed: , , satisfies the stated KKT system with two unequal interior coordinates. The corollary itself agrees with numerical optimization, but it currently lacks a correct proof. The paper also checks Lemma 5.7 numerically for . A machine-checked development would close both gaps and certify the constant. No part of this result is formalized elsewhere.
Lemma 4.3 and Lemma 5.2 are close to direct counting arguments. The difficulty lies in Lemma 5.3 and the bound on . Lemma 5.3 must compare the LP's profile mass with the probability that independently rounded reserves produce two cleared bids above . The LP couples buyers only through the marginals , and the comparison must hold for every optimal solution.
Bounding is a nonconvex optimization over the simplex-like region of (10), for every . The printed reduction to two symmetric families uses a KKT argument that does not hold, so a different argument is needed: a symmetrization or smoothing argument, or a direct inequality. Lemma 5.7 is tight at , , so its bound leaves no slack, and the paper's numerical range of has to be covered by analysis.
All statements live in the namespace ReserveLP.ProLPR and share one definition file, ReserveLP.ProLPR.Model. The formalization fixes these conventions:
The goal includes the existence of an optimal LP solution, so the guarantee is not vacuous. The goal compares against every reserve vector, not against the LP value. It uses the expectation of the per-realization better vector, not the larger of the two expectations. It uses the exact constant , not .
A complete development needs several ingredients:
The layer-cake sums and the product-measure marginals are reusable beyond this mission. Contributions are welcome on any milestone, especially a correct proof of Corollary 5.6.
In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.
Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).
A network is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. is the number of edges of a longest - path.
Time is discrete, . Agents form a set , possibly infinite. At each time finitely many agents enter. Agent enters at time at his origin and follows a fixed route, a nonempty - path. The tail of each edge holds a buffer. Two rules govern the dynamics:
No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).
Fix a focal agent with entry time . is the subnetwork formed by all - paths. For an integer time :
An agent exits when he reaches the head of the last edge of his route lying in .
For every admissible run and every integer : if no agent of exits before exits , then
where is the exit time of .
When is still inside at , the proof follows tokens: imaginary markers that produces from time on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with :
The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With and no later entrants on , it gives Corollary 1: the residence time of is at most . Example 1 (p. 8) shows that the bound can be attained. The freedom in is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.
Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.
The obvious argument is wrong. One might reason that travels at most edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay more than times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.
Formally, the hard parts are:
Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in ; it is a maximum wherever it is used.
Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in for the -th edge of 's route, numbered from . IsADR states that:
Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time ), as in the paper, so the theorem also asserts that exits.
Derived objects. Exit times, , , and the exit time from are definitions computed from the run, never free parameters. is Set.ncard of a set that is finite under IsADR.
Tokens. The token milestones assume that is inside at , as §3.1 requires when starting the construction. Tokens are indexed from . A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over , e.g. , which is the same inequality over the integers.
Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.
Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).
We characterize the bath resources needed to supply repeated uses of a fixed finite-dimensional quantum channel in a closed device. For each horizon , one bath, one initial state and one repeated unitary are fixed before the user. Each output is returned before the next input arrives; no reset, discard, fresh ancilla or uncounted controller is available. Approximation error must vanish against arbitrary adaptive users with quantum memory and references. Writing for the bath dimension rate and for the actual initial entropy rate, we prove that the achievable region is exactly , and . Here is maximum entropy exchange and is a smoothed independent-reference extension cost, with the zero-error limit taken before the supremum over full-rank inputs. Its exact fixed-input form is an affine transform of the zero-leakage quantum privacy funnel. The minimum dimension rate is . The proof combines entropy converses, a bath-dimension-independent support repair, and a closed adaptive implementation of encoder-only fully quantum Slepian--Wolf recycling. All seeds, clocks, workspace and retained residues are counted. Worked examples include dephasing, pure replacement and a qubit channel with . No computability of or efficient circuit synthesis is claimed. △ Less
This mission is the statement-level formalization of Bath dimension and initial entropy for closed repeated use of a quantum channel (arXiv:2609.18267v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.1: uniform collision gain (Theorem 3.1, PDF p. 6). 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.
13 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we fill the gap in previous works by proving the formula for entanglement-assisted capacity of quantum channel with additive constraint (such as bosonic Gaussian channel). The main tools are the coding theorem for classical-quantum constrained channels and a finite dimensional approximation of the input density operators for entanglement-assisted capacity. The new version contains improved formulation of sufficient conditions under which suprema in the capacity formulas are attained.
This mission is the statement-level formalization of Entanglement-assisted capacity of constrained quantum channel (arXiv:quant-ph/0211170v2). 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 Trace-norm compactness of an energy sublevel (§3, unnumbered Lemma (proof on PDF p.11), PDF p. 10). 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.
9 results of the paper are not stated yet, because the library lacks an interface they need:
The Schur transform, which block-diagonalizes the tensor representation of the unitary group on qudits, is an important primitive in quantum information and theoretical physics. We give a generalization of its quantum circuit implementation due to Bacon, Chuang, and Harrow (SODA 2007) to the case of mixed tensor , where is the dual representation. This representation is the symmetry of unitary-equivariant channels, which find various applications in quantum majority vote, multiport-based teleportation, asymmetric state cloning, black-box unitary transformations, etc. The "mixed" Schur transform contains several natural extensions of the representation theory used in the Schur transform, in which the main ingredient is a duality between the mixed tensor representations and the walled Brauer algebra. Another element is an efficient implementation of a "dual" Clebsch-Gordan transform for . The overall circuit has complexity . Finally, we show how the mixed Schur transform enables efficient implementation of unitary-equivariant channels in various settings and discuss other potential applications, including an extension of permutational quantum computing that includes partial transposes.
This mission is the statement-level formalization of The mixed Schur transform: efficient quantum circuit and applications (arXiv:2310.01613v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-input conclusive teleportation: exact success and corrected output (Section 5.1.1: two-input conclusive teleportation success, PDF p. 29). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
The maximum rates for reliably transmitting classical information over Bosonic multiple-access channels (MACs) are derived when the transmitters are restricted to coherent-state encodings. Inner and outer bounds for the ultimate capacity region of the Bosonic MAC are also presented. It is shown that the sum-rate upper bound is achievable with a coherent-state encoding and that the entire region is asymptotically achievable in the limit of large mean input photon numbers.
This mission is the statement-level formalization of Multiple-Access Bosonic Communications (arXiv:quant-ph/0506171v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational homodyne and heterodyne coherent-state MAC regions (§II.B, (5)–(8): single-mode homodyne/heterodyne capacity regions, PDF p. 2). 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.
18 results of the paper are not stated yet, because the library lacks an interface they need:
An optimal stopping game asks two players to choose when to stop a shared process. The first player receives one payoff if they stop first and another if the second player stops first. Such a game changes when one player knows a parameter that the other can only infer from observations. The informed player can reveal information through the timing of a stop, and can conceal it by randomising. De Angelis, Ekström and Glover study this interaction for a diffusion with one of two possible drifts. Their preprint gives a verification theorem for general payoffs and solves a linear geometric Brownian example explicitly. This mission targets the latter result, Theorem 6.10. The result is proved in the paper; the work here is to express its model, strategy classes, supporting results and conclusion in Lean.
The asset value starts at and evolves as a geometric Brownian motion , where , , and the hidden type selects the drift. Initially ; write for the initial odds. Player 1 sees the history of and chooses an almost surely finite stopping time for its augmented observation filtration . Player 2 also knows and chooses an adapted, nondecreasing control for the augmented filtration . An independent uniform variable turns this control into the randomised stopping time . The initial value may be positive, representing a jump at time zero.
If , Player 1 receives ; if , Player 1 receives . Thus a finite tie pays . The expected payoff is . Player 1 maximises it and Player 2 minimises it. A saddle point satisfies for every admissible pair . In the linear example and , where .
The uninformed player's posterior probability is expressed through the posterior odds . The informed strategy is a pair , one control for each type. Conditional laws define the interim payoffs . The scaled ex-ante payoff is . These quantities permit both an ex-ante saddle-point statement and the agent-form equilibrium statement of Proposition 3.6.
The supporting targets begin with the filtering and payoff identities of Section 3, the quasi-variational verification result of Theorem 5.1, and the reflected-likelihood and boundary-value facts of Section 6. They culminate in the explicit linear-game equilibrium. Two real numbers are determined by equations (90) and (93); piecewise power functions are defined by (89) and (91), extended by (94)–(97), and . The type-one control keeps the adjusted odds below , while Player 1 stops at .
The goal is Theorem 6.10: is a saddle point, and for every ,
The mission's milestone list follows the paper's stated results. It includes the payoff reductions, Theorem 5.1, reflection at , the ODE bounds, the unique ratio , and the verification of the explicit value functions.
The theorem identifies actual strategies for both players, rather than only showing that the game's upper and lower values coincide. It specifies how the informed player's randomisation depends on the unobserved type and how the uninformed player responds to the adjusted odds. It also gives the ex-ante and both type-conditional payoffs. Without the saddle inequalities over the full strategy classes, the formulas would describe candidate strategies rather than an equilibrium.
A Lean development must capture the paper's information restrictions and time-zero behaviour before the analytical proof can be meaningful. Reusable components include a model-independent two-filtration randomised Dynkin frame, the augmented observation filtrations, randomised stopping times, nonnegative extended payoffs, conditional-law decomposition, and Stieltjes integration with an initial jump. The paper has a written proof; the statements here are open Lean goals, not machine-checked proofs.
The verification theorem couples a partial differential inequality to a singular control and a stopping time. The adjusted odds can jump when the control jumps, so ordinary continuous-path differential conditions do not by themselves describe the admissible action. The support conditions and transversality limits in Theorem 5.1 are needed to connect the analytic candidate values to payoffs for strategies that can stop at any time. In the linear example, obtaining the power-function candidates is only one part of the target: their free boundaries must be valid, the reflected control must be admissible, and the saddle inequalities must hold against all admissible alternatives.
The Lean model uses the explicit strong solution of the §6 GBM on a complete probability space carrying a Brownian motion and independent uniform devices . It sets . Paths of the chosen Brownian modification are continuous. Player 1's filtration is generated by plus null sets; Player 2's also contains ; neither contains . Stopping times live in , with Player 1 required to stop almost surely. Payoffs are nonnegative extended integrals and equal zero if both stopping times are infinite. The Stieltjes convention counts .
The posterior odds use the GBM closed form. The running-maximum formula defines and permits its initial jump. The tilted law used in Lemma 6.5 is represented by an equivalent likelihood-path law. Theorem 5.1 is stated for the GBM instance with general continuous and relative closures inside . Its localisation integral retains the factor printed in the preprint. The explicit boundaries, controls and values in the goal are definitions, never free variables or hypotheses; the saddle inequalities quantify over the full player strategy classes.
There is a normalization slip in the paper's (23): it prints on , although and a Radon–Nikodym derivative at time zero equals one. Equations (20)–(21) give . The formal filtering item uses that corrected identity. Equation (50) similarly identifies the ex-ante value with the scaled payoff; the formal target records and states the payoff identities without confusing the two. The source's domain in Theorem 6.10 is read as , as required by the model. These readings are documented in the local moderation notes.
Residential solar panels can reach customers through a purchase, a lease, or a power purchase agreement (PPA), under which the customer pays for the electricity the panels generate. These arrangements allocate panel ownership, subsidy receipts, and generation risk differently. A company choosing prices for all three therefore also chooses which customers adopt each arrangement. Agrawal, Toktay and Yücel study that choice in a model with net-metered electricity, investment and generation subsidies, and customers who differ in expected solar generation. Their main structural result identifies the company's optimal mix as panel cost and the investment subsidy change. The subsequent results about subsidy effects, renewable adoption, and restrictions on leasing use this mix as their starting point. Agrawal, Toktay and Yücel (2022).
One solar power company sets a normalized monthly sales price , a monthly lease fee , and a PPA price per unit of generation. A customer can choose sale , lease , PPA , or continued electricity supply from the utility . The customer has expected monthly solar generation and expected electricity demand . The retail electricity price is ; is the fraction of panel investment cost covered by an investment subsidy, is the generation subsidy per unit, is the company's PPA monitoring cost per unit, and is its normalized panel cost. Under net metering, the customer's utility bill is when usage is and generation is . The paper's expected monthly costs of the four choices are
The customer chooses a least-cost option. Expected generation is uniform on and independent of expected demand, whose distribution has positive support. Let be the population share choosing option and the total expected generation among those customers. An option is offered when its share is positive. The company's expected monthly profit, equation (1) of the source, is
These amounts come from actual customer choices, so their adoption shares are nonnegative by definition. The sales-only benchmark, in which customers choose between and , yields the panel-cost bound . The source restricts its main analysis to . Agrawal, Toktay and Yücel (2022), §§3–4 and Online Appendix A.
The goal is Proposition 1, the global choice of business models. Write . When , there are panel-cost thresholds such that every profit-maximizing price triple has the offer set
When , a threshold separates for from for . The same thresholds apply as and the admissible demand distribution vary, and a maximizing price triple exists for each admissible . A zero-width middle regime is allowed when . The equality points at are excluded because the appendix's candidate cases become degenerate or have tied global optima there, so the printed assignment at those points does not hold for every maximizer. Agrawal, Toktay and Yücel (2022), Proposition 1 and proof.
The milestones establish the common optimal electricity usage of Lemma 1, customer segmentation by in Lemma 2, and the sales-only profitability limit of Lemma A.1. They then identify the best profits in the regions and and compare those profits across the investment-subsidy regimes. The mission follows the author's source indices and case names, including the appendix's closed-form candidate prices and values. Agrawal, Toktay and Yücel (2022), pp. 11, 14 and OA1–OA8.
The proposition states when a company can profitably maintain PPA, leasing, and sales side by side, and when it optimally drops one or both non-ownership models. This matters for the paper's later claims: a change in a subsidy or a legal restriction may alter not only prices within one model but which models serve customers at all. The paper's comparisons of total adoption, generation, and utility-firm profit therefore depend on the equilibrium classification. Agrawal, Toktay and Yücel (2022), Propositions 2–6.
The mathematical result is already proved in the source. This mission supplies compiled Lean statements for its model and central claims; the theorem proofs remain open. Completing them would provide a machine-checked route from individual cost comparisons and population integrals to the global pricing decision. The customer-choice and adoption definitions can also support formal work on the paper's later subsidy and restriction results. No machine-checked proof of these draft theorems is claimed here.
Comparing customer costs at a fixed price triple gives generation intervals, but it does not by itself identify the company's best prices. The company optimizes three prices while the adopting population changes at interval boundaries. In the appendix, the resulting problem has distinct candidates when and , and its preferred candidate changes with both and . A direct comparison of two displayed candidate profits is therefore insufficient unless the candidate is optimal throughout its stated region and all boundary cases are accounted for. At a cost where two regional values agree, different maximizing price triples can have different offer sets. Agrawal, Toktay and Yücel (2022), proof of Proposition 1, OA4–OA8.
Lean represents prices by three real coordinates and parameters by one structure. The standing conditions are , , , , , and , where is the paper's concavity threshold. Lemma 2 and Lemma A.1, which the paper states before introducing and on p. 15, assume only the §3 conditions (and for Lemma A.1). The goal also assumes . Its demand distribution is an arbitrary probability measure concentrated on , which generalizes the paper's density without changing the claims, because the choice comparisons do not depend on . Generation uses the uniform probability law on and integrates over the actual choice sets.
The four realized and expected costs are defined separately. Ties among use a fixed priority order; is selected only if strictly cheaper than all three solar options. This implements the appendix's allocation to PPA at , where PPA and utility costs tie on a set of positive mass. The theorem ranges over all real price triples. Its offer set is calculated from positive adoption at a maximizer, and it asserts existence of that maximizer; neither the offer regime nor optimality is assigned by a case label. The cost thresholds are chosen before quantifying over the demand distribution and . A milestone using requires , and the closed-form denominators are used only under the stated parameter conditions. Population measures are finite, and the choice regions are measurable; these facts matter when converting adoption mass to a real number and integrating generation. The sales-only benchmark and the appendix formulas are separate definitions, not substitutes for equation (1).
Contributions are welcome on customer-choice measurability, integral identities for adoption and generation, the regional maximization claims, and the algebraic value comparisons. Propositions 2–6 and the Technical Appendix's alternative policy models are outside this mission.