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?
We address the problem of learning an unknown unitary transformation from a finite number of examples. The problem consists in finding the learning machine that optimally emulates the examples, thus reproducing the unknown unitary maximum fidelity. Learning a unitary is equivalent to storing it in the state of a quantum memory (the memory of the learning machine), and subsequently retrieving it. We prove that, whenever the unknown unitary is drawn from a group, the optimal strategy consists in a parallel call of the available uses followed by a "measure-and-rotate" retrieving. Differing from the case of quantum cloning, where the incoherent "measure-and-prepare" strategies are typically suboptimal, in the case of learning the "measure-and-rotate" strategy is optimal even when the learning machine is asked to reproduce a single copy of the unknown unitary. We finally address the problem of the optimal inversion of an unknown unitary evolution, showing also in this case the optimality of the "measure-and-rotate" strategies and applying our result to the optimal approximate realignment of reference frames for quantum communication.
This mission is the statement-level formalization of Optimal quantum learning of a unitary transformation (arXiv:0903.0543v2). 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 Covariance without loss for a delayed learning comb (§III A, Eq.(9): covariance without loss for a learning comb, PDF p. 3). 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.
11 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper a general definition of quantum conditional entropy for infinite-dimensional systems is given based on recent work of Holevo and Shirokov arXiv:1004.2495 devoted to quantum mutual and coherent informations in the infinite-dimensional case. The properties of the conditional entropy such as monotonicity, concavity and subadditivity are also generalized to the infinite-dimensional case.
This mission is the statement-level formalization of Quantum conditional entropy for infinite-dimensional systems (arXiv:1004.4519v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Conditional entropy: monotonicity, concavity and subadditivity (§2, Proposition 1, all three clauses: monotonicity, concavity and subadditivity (7)–(9), PDF p. 3). 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.
The coding theorem for the entanglement-assisted communication via infinite-dimensional quantum channel with linear constraint is extended to a natural degree of generality. Relations between the entanglement-assisted classical capacity and the -capacity of constrained channels are obtained and conditions for their coincidence are given. Sufficient conditions for continuity of the entanglement-assisted classical capacity as a function of a channel are obtained. Some applications of the obtained results to analysis of Gaussian channels are considered. A general (continuous) version of the fundamental relation between the coherent information and the measure of privacy of classical information transmission by infinite-dimensional quantum channel is proved.
This mission is the statement-level formalization of On the entanglement-assisted classical capacity of infinite-dimensional quantum channels (arXiv:1210.6926v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, (14): general constrained entanglement-assisted coding theorem (Theorem 1, (14): general constrained entanglement-assisted coding theorem, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
A nonprofit choosing how to serve people with different needs may have two ways to use an additional dollar: offer more product variants, or deliver a larger fraction of each product. Beneficiaries can sometimes finish an incomplete product themselves, but doing so takes effort. Zhang, Atasu and Ramachandran study this choice for services such as incremental housing and temporary shelter. The question is how a limited budget changes the optimal combination of variety and completion.
The paper’s main text first models the beneficiaries’ needs and the nonprofit’s costs, then derives the allocation pattern in Lemmas 1–2 and Proposition 3. This mission targets those results in the authors’ SSRN version. The optimization is over a continuous variety level, as the paper explicitly assumes in §4.2; the integer case has a different comparative static for completion at footnote 5 on p. 13.
A variety level describes how many equally spaced variants the nonprofit offers to a unit mass of beneficiaries with uniformly distributed ideal locations. The analysis treats as a real decision variable. A completion level is the fraction of each variant the nonprofit provides. Heterogeneity reduces the utility of a complete variant with distance from a beneficiary’s ideal. Aggregating the closest variant’s utility gives §3, pp. 7–8.
Each beneficiary may complete at most of the product. With quadratic effort cost , where , optimal self-completion effort is . The nonprofit’s expenditure is , where , , and for . Its total net benefit is
At a budget , a decision is feasible when , , and . An optimal decision is a feasible decision whose value of is at least that of every other feasible decision. Without the budget constraint, the same domain , defines the unconstrained problem §3, p. 10 and §4.2, pp. 12–13.
The standing assumption that provision is worthwhile says some satisfies . Let be the unconstrained optimal variety: it is when ; otherwise it is the solution above of . Write and . These are the unconstrained completion level and the budget needed to afford that pair Lemma 1, p. 12.
Lemma 1 asserts that maximizes without a budget constraint. Lemma 2 says every optimal decision exhausts its budget below :
Proposition 3 is the goal. It asserts thresholds , a small-budget variety , and middle-regime decisions such that an optimal pair can be selected as
Both and are nondecreasing on the middle interval, using the paper’s weak meaning of “increasing.” The goal characterizes using the appendix’s function : if , and otherwise is its zero. It also requires . These conditions retain the paper’s small-budget regime and prevent an arbitrary threshold from making it empty Proposition 3, p. 13; proof, Online Appendix p. 2.
The three regimes identify when a nonprofit should spend an increment of budget solely on completion, when variety and completion should rise together, and when additional budget no longer changes its choice. Lemma 1 also says that, even with ample funds, completing the entire product need not be optimal because beneficiaries can add value through their own effort §4.2, pp. 12–14.
The paper proves these claims analytically. This mission asks for machine-checked proofs of the continuous model’s optimization statements, including the attainment and feasibility of each claimed optimum. The reusable part is a compact interface for a two-variable budget-constrained optimization problem with a beneficiary best response. There is no existing machine-checked proof of these particular claims in the platform catalog at drafting time.
The binding-budget curve crosses the point , where beneficiary effort changes formula. Thus optimizing a single smooth expression over all variety levels does not cover the problem. A stationary point calculated in one region also must be checked against feasible points in the other. The argument needs to establish global optimality and preserve the bounds as the budget changes Online Appendix pp. 2–3.
The appendix’s candidate threshold in one case can exceed when the unconstrained variety is . Proposition 3 itself asks only for a threshold , so the formal goal retains that existential form. The proof’s candidate must be capped at in that case; the middle interval can then be empty. This discrepancy is recorded for solvers, who should establish the proposition as stated rather than assume the appendix’s candidate always satisfies the bound Online Appendix p. 3.
All quantities are real. The Lean model stores , , and as separate functions and requires the two derivative identities, positive and nonnegative for . It uses the closed formula for and the minimum formula for effort. The hypotheses , , and make explicit the economic parameter and budget domains; is needed for the stated variety characterization, and is implicit in the paper’s increasing quadratic effort cost. The paper’s , , and worthwhile-provision assumption are retained.
Optimality always includes membership in the feasible set. This rules out an out-of-domain maximizer. The upper regime asserts that the displayed pair is an optimum, allowing other optima when . Division by and is used only at varieties ; the standing assumptions imply there. The goal fixes by the paper’s formula and pins down , so it cannot be discharged by choosing arbitrary empty budget ranges. Proofs of the two appendix monotonicity claims, the binding-budget lemma, and the global small-budget optimum are welcome along with the goal.
Banks and other financial institutions are notoriously hard to see into: their loan books are complex and their public reports are coarse. A long-standing policy question is whether competition among financial institutions makes them more or less transparent. One view holds that competition for funding disciplines institutions into disclosing more; another that competitive pressure rewards opacity. G. Zhang, Competition and Opacity in the Financial System (SSRN 3428683; Management Science 2020, doi:10.1287/mnsc.2019.3512), gives an answer inside a coordination model in the tradition of Morris and Shin (2002) and Angeletos and Pavan (2004): competition lowers disclosure precision exactly when investors' own private information is precise.
The model belongs to the literature on public information in beauty-contest economies, where public reports serve both as information about fundamentals and as a focal point for coordination. The paper adds a second force, competition between two institutions for the same investors, and asks how the institutions' chosen precision of public disclosure responds.
Two financial institutions (FIs) raise funds from a continuum of risk-neutral investors . FI 's project has fundamentals , independent across , with prior mean and prior precision . Its return is
where is the aggregate investment in FI and is the FI's rollover-risk exposure: the more others invest, the higher the return.
Before learning , FI commits to a disclosure precision and pays . It then publishes with . Each investor also observes private signals of precision , and invests
in FI , where is the intensity of competition (: none; : the intense case analysed in the paper's main result). Here is investor 's posterior expectation; for Gaussian signals . A linear equilibrium of the investors' game is a strategy that satisfies this rule when every investor uses it.
FI 's payoff is . A disclosure equilibrium is a pair of precisions, each a best response to the other given the investors' linear equilibrium. Write for the equilibrium precision without competition () and for the one with competition.
For sufficiently large:
The goal fixes no constants: is only asserted to exist.
Proposition 4 is the paper's main result. It separates two channels through which competition acts on disclosure: competition amplifies investors' reaction to every signal, which both reduces the coordination problem that disclosure is meant to solve and raises the value of a precise report for allocating funds between the institutions. Which effect dominates depends on the precision of private information, and the result pins this down to a single threshold. Without rollover risk the two channels vanish and competition is neutral. The paper's policy discussion of opacity in the financial sector (§3.3–§4) and its welfare analysis rest on this comparison.
The result is proved in the paper by hand computation; it has no machine-checked proof. Formalizing it requires the Gaussian payoff computation, a linear fixed-point argument for the investors' game, an optimization argument for the institutions' disclosure choice under a large-cost assumption, and a sign analysis of an explicit quartic.
The payoff is an expectation of a quadratic in four independent Gaussians whose coefficients are themselves the solution of the investors' fixed point. Differentiating it in means differentiating through the equilibrium coefficients, and at the coefficients of FI depend on both precisions; the closed form (44) holds only after cross terms cancel.
The comparison is global in . Reading off the sign of the marginal payoff at gives a condition on , not on , and itself moves with . A threshold on exists only because is monotone and the quartic changes sign once. The "sufficiently large " must be uniform in : a bound that depends on does not give a single threshold.
Fin 2 (FI 1 of the paper is 0), the other FI is i.rev. The law of is a product of Mathlib gaussianReal measures; precision is variance . At the noise is a point mass, and the equilibrium puts no weight on .Classical.epsilon; Lemma 1 and Proposition 3 show it is determined in every coefficient the payoff uses. A disclosure equilibrium is a Nash equilibrium in .Large bonuses in some industries are paid within a few weeks of each other across firms: banks in a given region announce bonuses in the same months, and top-tier US law firms announce theirs almost simultaneously. Van Wesep and Waters (SSRN 3124536, published in Management Science, 2022, doi:10.1287/mnsc.2021.4076) explain this coordination with a search model of the labor market. If many workers leave their employers at the same time of year, the labor market is deeper at that time, which makes it a better time to replace a worker who has become a poor match. Firms then have reason to make dissatisfied workers stay until that time, which a bonus at the end of the cycle achieves, and the bonuses in turn concentrate quits at that time. The question is when this self-reinforcing seasonality is an equilibrium.
The model builds on the search-theoretic labor market with an aggregate matching function (surveys: Petrongolo and Pissarides, 2001; Rogerson, Shimer and Wright, 2005) and on wage bargaining with transferable utility.
Time is discrete; periods alternate between odd (index 1) and even (index 2). A continuum of firms of mass and of workers of mass , , are either matched in pairs or searching. A match produces revenue per period. A new worker is satisfied, with per-period disutility ; at the end of each period a satisfied worker becomes dissatisfied, with disutility , with probability , and stays so; matches separate exogenously with probability ; workers may quit at the end of any period. Here and , the discount factor. The importance of match quality is
If firms and workers search, matches form, where is homogeneous of degree one, increasing in each argument, differentiable, and (Assumption A1). A vacant firm matches with probability and an unemployed worker with probability ; these depend only on the labor market depth .
In the periodic turnover plan, a dissatisfied worker quits at the end of even periods and stays at the end of odd periods. Under it the masses searching at the start of each period solve a fixed system of flow equations, which yield matching likelihoods . A newly matched pair bargains over pay with worker weight (generalized Nash bargaining); the resulting values (firm with a new hire), (vacant firm), (new hire, gross of pay), (unemployed worker) and the bargained present value of pay solve a linear system together with the Nash conditions. With and the paper defines two thresholds
A periodic equilibrium consists of a labor-market state solving the flow equations, with depth differing between odd and even periods; Nash-bargained values; Pareto optimality of the periodic plan for every newly matched pair (no other turnover plan yields a larger joint value); and a periodic contract (a signing bonus depending on the hiring period, a wage in odd and in even periods) that makes the periodic plan incentive compatible and delivers the bargained present values , .
With computed from the solution of the flow equations,
Proposition 2 is the existence result on which the paper's account of coordinated bonuses rests: the subsequent results on equilibrium contracts (that rising wage profiles, i.e. end-of-cycle bonuses, always implement the equilibrium and are sometimes necessary) and on the stylized facts of compensation in finance and law presuppose a periodic equilibrium. It shows that seasonality of labor markets can be self-sustaining, with no exogenous seasonal shock, exactly when match quality matters neither too little (then dissatisfied workers are never released) nor too much (then they are released at once).
The result is proved in the paper by hand algebra over a dozen coupled equations. No part of it is machine-checked, and the platform has no search-and-matching labor market, no aggregate matching function and no turnover contract. The mission produces a checked version of the existence characterization, of the closed forms behind it, and a reusable formal model of a two-period search market with Nash-bargained, incentive-compatible contracts.
Lemma 2's existence and ordering do not follow from monotonicity of alone: the flow equations couple both periods, and the natural scalar reduction evaluates outside its domain when , so the interval on which an intermediate-value argument runs must be chosen with care. The closed forms of Lemma 3 come from eliminating ten unknowns from a linear system whose coefficients are themselves the matching likelihoods; the paper's own equation (21) contains a typo that makes (29) false if taken literally. The thresholds of Proposition 1 require turning two inequalities on joint values into inequalities in , where the sign of each denominator has to be controlled. Finally, the equilibrium compares the periodic plan with every alternative plan through their joint-value recursions, not through the closed forms.
All quantities are real. Periods are indexed 1 (odd) and 2 (even); firm masses are derived, . Assumption A1 is stated on the closed quadrant, with "increasing" read strictly, which Lemma 2's strict inequalities require. Equation (21) is used with restored, . Nash transfers are defined as maximizers of the Nash product, not by (24)–(25). Definition D3 is imposed as . Pareto optimality compares the four turnover plans that are stationary across periods of the same parity, with satisfied workers never quitting, through their joint-value recursions. Present values of contracts are infinite sums. The goal leaves the endpoints open: the paper's statement excludes them while its proof includes them. Proposition 1's printed interval is read as , as in its proof.
The periodic equilibrium is not defined through , , conditions (i)–(ii) or the closed forms, which would make the goal a tautology; it is built from the market equations, the bargaining problem, the plan comparison and the contract.
Corollary 1, Proposition 3, Lemmas 6–7 and §5–6 are not part of this mission. Contributions to the infrastructure (Nash split, geometric tsum evaluation of periodic present values, contraction arguments for the value recursions) are welcome and reusable for other search and bargaining models.
A buyback contract lets a retailer return unsold goods to a manufacturer at an agreed returns price. The promise changes the retailer's willingness to order before demand is known. If the manufacturer may fail to honor it, the retailer must also judge how credible the promise is. Wang, Gurnani, and Subramanian study what the contract's wholesale and returns prices reveal about that credibility in a supply chain with one manufacturer and one retailer (Wang et al., 2020, §3–4). Their returns-risk result gives a precise case in which a more reliable manufacturer signals through lower prices. The direction is economically consequential because lower orders and less leftover stock accompany the signal.
This mission follows the authors' revised SSRN version, whose main-body page numbers and Electronic Companion result numbers fix the statements below. The result is a known theorem in that paper; the open work here is its Lean formalization.
The manufacturer offers a pair : a nonnegative wholesale price per unit ordered and a nonnegative returns price per unit the manufacturer accepts back. Her marginal production cost is zero. The retailer orders stock before observing demand. After demand's baseline is realized, he sets a retail price . Demand is , where the baseline is high, , with probability , or low, , with probability . Write and .
The manufacturer's type is the probability that she honors the returns promise. The less risky type has probability and the riskier type has probability . The retailer does not know the type when he sees the contract, so his perceived probability is . Demand potential is common knowledge in this mission. With , the retailer's order formula from Lemma 1, at perceived demand probability , is
The low-demand unsold quantity is half the positive-part term. The manufacturer's expected profit, with actual return probability , is equation (2):
The retailer's price-stage and ordering objectives are defined separately, so Lemma 1 connects this formula to actual optimization rather than merely repeating a definition (SSRN version, pp. 9–11 and EC p. 1).
With the type known, Lemma 2 gives the symmetric-information benchmark:
The two types earn the same . Their actual returns prices differ because the expected payment depends on .
The main target is Proposition 1. A separating equilibrium has the riskier type offer and the less risky type offer a solution of problem (4). The retailer believes at the latter contract and at every other contract. Problem (4) maximizes over , subject to the riskier type's non-mimicry constraint and the less risky type's participation constraint. A solution must actually attain that maximum; existence is part of the goal. The target comparison is
and no stock remains after high demand. The Lean goal also verifies both types' no-deviation clauses under the stated beliefs (SSRN version, p. 13, Proposition 1; EC p. 15).
The milestone list follows the paper's retailer-response and benchmark lemmas, then the Appendix B bounds on the transformed optimizer and the less risky type's off-path deviations. The transformed coordinates are and . They encode the constraints and quadratic objective in (B.4)–(B.7), rather than defining the original profit by that quadratic outside its valid region.
Under the authors' model, signaling greater reliability reduces both contract prices and the retailer's volume of trade. The comparison distinguishes the effects of information about returns risk from the symmetric-information benchmark. The paper also studies signals about demand potential and joint private information, but those are distinct results (Wang et al., 2020, §§5–6).
A complete Lean development would make the demand-stage optimization, two-type incentive constraints, existence of a maximizer, and the directional inequalities independently checkable and reusable in related contract models. The present mission states those targets; it does not claim they already have machine-checked proofs. The authors prove them in the cited paper. The objective here is to formalize that known argument or another proof of the same statements.
The less risky type chooses two continuous prices under a non-mimicry constraint that is nonlinear and changes form when the retailer stops carrying safety stock. A direct appeal to an unconstrained quadratic optimum misses the boundary and can violate the riskier type's incentive constraint. Existence also requires an attained maximum of problem (4), rather than a supremum or an assumed optimizer. The Appendix B characterization shows that the optimal transformed coordinates satisfy specific equations and strict inequalities; the no-deviation check then ranges over off-path contracts, not only local perturbations (SSRN version, EC pp. 4–15).
Lean uses real parameters for the two demand baselines, , , , and , and pairs of reals for contracts. The standing assumptions include , , , and . The strict lower bounds on and are disclosed additions: the printed model allows zero, but its returns-price benchmark divides by and Proposition 1's strict lower-price claim fails at .
The admissible action set for a type is , as in the paper's optimization problems; a deviation is checked when , following the retailer-response convention on p. 10. Beliefs range over and are pessimistic away from the less risky type's equilibrium contract. This is the paper's operational most-efficient profile from problem (4). Maximality over all possible separating equilibria and refinement by the intuitive criterion are outside this target.
For the retailer-price value, Lean takes a real supremum over the compact nonempty interval ; the objective is continuous there under the standing assumptions. Lemma 1 makes its printed order formula an optimizer only when that formula is nonnegative, correcting the negative-order edge case; it states the unsold stock as the realized leftover at every optimal retail price, and claims the low-demand amount only under the price cap of Lemma A.1, without which the printed amount can exceed the stock. Manufacturer profit remains the paper's equation (2); defining it as the Appendix B quadratic would make the target easier by changing the model. The first-stage solution predicate quantifies over every feasible contract and carries no desired sign condition. Reusable contributions include the price-stage analysis, the symmetric-information benchmark, and optimization facts for the transformed feasible set.
Asset-pricing models relate an asset's expected return to the risks it shares with the market. A familiar covariance term measures exposure to the market return, while a coskewness term measures exposure to the square of that return. Shi, Cui and Zhou ask how these two coefficients change when investors weight probabilities as well as valuing outcomes. Their 2020 working paper derives a market pricing kernel and a three-moment capital asset pricing relation from a representative investor's rank-dependent utility. The paper subsequently studies the signs of the coefficients and tests the resulting relationships with financial data; this mission concerns its theoretical pricing result, Theorem 2.
At date 0, investors choose positions in finitely many assets. At date 1, asset pays a random total return per unit invested. One asset is risk-free, so its total return is the constant . A pricing kernel is a strictly positive random variable that prices every total return by . The market return is , where the market-capitalization weights sum to one. A return rate subtracts the invested unit: and . These are the conventions of §§2–3 of the source.
The representative investor has rank-dependent utility. For a nonnegative payoff with cumulative distribution function , an outcome-utility function , and a probability-weighting function , its value is the distributional integral
The model assumes an atomless probability space; is strictly increasing and strictly concave on positive wealth, continuously differentiable there, and satisfies the Inada and asymptotic-elasticity conditions of Assumption 1; is strictly increasing and continuously differentiable on , with and . Problem (P′) asks for the largest among measurable nonnegative payoffs with . Equilibrium means that attains this value. The working paper states these assumptions and this optimization problem on pp. 8–9 and identifies equilibrium with the optimal market return in Appendix A, p. 33 (source).
Write for the CDF of and set . The paper defines the pricing function
The probability weight depends on the market distribution, while marginal utility depends on the realized total return. Their joint variation determines the pricing coefficients in Theorem 2 (source, pp. 10–11).
For an equilibrium whose market return has a continuous CDF, the goal begins with the almost-sure identity
Appendix A states an intermediate first-order form with a positive multiplier , then equation (12) determines from the risk-free asset. Both are milestones (source, pp. 33–34).
When has a continuously differentiable density , Theorem 2 gives a beta premium and a coskewness premium by the closed forms in its equations (6)–(7), with and . It states
The formal target makes the last term exact. Define , with as . The pricing identity then has remainder . The source's quadratic expansion (13), its premium identities (6)–(7), and its covariance pricing identity are the remaining milestones (source, pp. 11 and 34–35).
The kernel identity connects the market's state prices to both marginal utility and probability weighting. The three-moment relation then specifies how an asset's covariance and coskewness with the market enter its expected return. Without the kernel identity the coefficients would be free parameters; without the density and derivatives their explicit forms would be unavailable. The paper uses these coefficients to analyze beta and coskewness pricing under particular weighting functions and later compares the relationships with data (source, §§3–5).
The paper result is published in Operations Research; this mission follows the held SSRN version of June 2, 2020, whose theorem numbering and pages are pinned below. The Lean theorem statements in this proposal compile as open targets; they do not yet have machine-checked proofs. A completed development would add a reusable RDU model, a pricing-kernel characterization under equilibrium, and a precise covariance relation with a controlled remainder. The later parameter-specific propositions and empirical sections are outside this mission.
The central difficulty is the first part of the theorem. The optimality condition concerns an objective that depends on the entire payoff distribution through , so ordinary pointwise differentiation of does not identify the kernel. The paper obtains this step from an earlier result of Xia and Zhou, then uses the risk-free asset to fix the multiplier (source, Appendix A). The second part needs third derivatives of and although Assumption 1 only says they are continuously differentiable. It also uses a random-variable little-o without specifying how that term enters an expected return. These are mathematical conditions the formal statement must make explicit.
Lean represents the probability space by a probability measure and atomless by the event-splitting property: every positive-measure event has a measurable subset of strictly intermediate measure. Assets are indexed by Fin n; the risk-free asset is specified by its constant total return, and is computed from the weights and asset returns. The RDU objective is the paper's integral against the payoff law, including the CDF factor, and equilibrium is optimality for problem (P′). It is not defined through the desired kernel equation.
The Bochner RDU integral is required to be integrable for the market payoff and for compared competitors. Those competitors also have continuous CDFs and positive payoffs almost surely, so endpoint values of the two-sided derivatives and the utility at zero do not affect the comparison. This is a disclosed strengthening of the conclusion's scope: the equilibrium requirement compares fewer payoffs than the paper writes. The CAPM clause assumes local regularity of at and at , , a nonnegative density represented as the law of , and finite second and fourth moments needed for genuine covariances. Its premiums are the closed forms of (6)–(7), and its remainder is computed from , once for every asset. The kernel identity is a conclusion; an assumed kernel or an independently chosen remainder would erase the target.
The development uses Mathlib's CDF, pushforward and density measures, Bochner integrals, covariance, MemLp, derivatives, and little-o. The event-splitting predicate, priced-market interface, RDU functional, feasibility and equilibrium notions, closed-form premiums, and Taylor remainder are local definitions. Contributions to the first-order characterization, the derivative identities, the precise expansion, and the covariance step all advance the goal.
Financial constraints, the gap between what a firm could produce and what it can raise from outside investors, are a central object of corporate finance. In moral-hazard models of financing, an entrepreneur must be paid an agency rent to exert unobservable effort, and the investor can only be repaid out of what is left; the agency rent therefore fixes the entrepreneur's pledgeable income and the degree to which the entrepreneur is financially constrained (Tirole, The Theory of Corporate Finance, 2006).
J. Starmans, Technological Determinants of Financial Constraints (manuscript, February 4, 2022; published in Management Science, 2022, doi:10.1287/mnsc.2022.4421), asks how an entrepreneur's production technology, meaning which part of the cash-flow distribution the entrepreneur's effort improves, determines the agency rent, and hence which entrepreneur an investor with limited capital prefers to finance. The answer links technology, the form of the optimal security (debt, equity or a combination), and financial constraints in one model. The mission formalizes the paper's general comparison of entrepreneurs (its Proposition 6) together with the closed-form solution of the contracting problem on which it rests.
There are states with , and a project pays the cash flow in state , where . If the entrepreneur shirks, the state is drawn from a baseline distribution with for every state. An entrepreneur's type is the distribution of the state under effort. Write .
The likelihood ratio of a type is . The type set consists of the distributions such that (Assumption 1) every type creates the same expected value of effort , ; (Assumption 2) first-order stochastically dominates , with at least one strict tail inequality; and (Assumption 3) is single-peaked in the state. The cumulative likelihood ratio is
and denotes the highest state with : the upper end of the region the entrepreneur improves.
A contract pays the entrepreneur in state . Given the entrepreneur's disutility of effort , an optimal contract solves problem (1): maximize the investor's expected payoff subject to the incentive constraint , the participation constraint , limited liability , and monotonicity of both payoffs, and . The agency rent of an optimal contract is . The tranches , , partition the cash flow.
Let with . For every both have optimal contracts, and, writing for any optimal contracts at :
The threshold is existential; no constant is fixed.
In attack order: the sign facts , (Lemma A.1); the sign pattern of (Lemma 2) and of (Lemma 3); the greedy optimal contract with thresholds (Proposition 1); the closed-form agency rent, continuous, increasing, piecewise linear and convex in (Proposition 2); the bounds and with equality iff (Corollaries 2 and 3); and the two facts of the proof of Proposition 6 (p. 47): the agency rent is on when , and on an initial interval for every .
Proposition 6 says that the peak cumulative likelihood ratio, the informativeness of the most informative tranche, decides which entrepreneur is cheaper to incentivize when effort is cheap, while at high disutility of effort the entrepreneur who improves only the left tail of the distribution (whose optimal contract is equity-like) is cheaper. Its instance with the optimal equity-financed and the optimal debt-financed entrepreneurs is the paper's Proposition 5, which underlies its predictions about which firms are more financially constrained. The milestones give a complete closed-form solution of a linear contracting problem with limited liability and two-sided monotonicity under a single-peaked likelihood ratio, a setting that generalizes the monotone likelihood ratio property.
The results are proved in the paper (Appendix A). As far as a search of the Prove2Me catalog shows, none of them, and no model of security design with tranches, has a machine-checked proof. The mission produces formal proofs of the paper's results; the agency-rent formula of Proposition 2 is a reusable description of a fractional knapsack's value function.
The comparison is not a pointwise statement about two formulas: the agency rent is the value of an optimization problem over all contracts, and only the solution of that problem (Proposition 1) turns it into a piecewise-linear function. The step that does not follow from slopes alone is the comparison at : it needs the identification of the optimal contract at with (Corollaries 2 and 3), which rests on the sign structure of Lemmas 2 and 3 and therefore on Assumptions 2 and 3 together. The monotonicity constraint on the investor's payoff, , is what caps each tranche at weight one; without it (the paper's Appendix C) the agency rent is for every and the crossing in case (i) disappears.
States are Fin (n + 1); types, contracts and cash flows are vectors Fin (n + 1) → ℝ, and all expectations are finite sums. The standing assumptions , , , , are bundled in Economy.Standing; is InP, which keeps Assumption 2's strict clause as written. Tranches and positions of the ordering are indexed by Fin n, standing for the paper's indices shifted by one. is the maximum over all of , including . is defined as the highest state with ; Lemma 2 shows it is the paper's . The agency rent function is the infimum of over optimal contracts, and Proposition 2 states that every optimal contract attains it on .
Conventions disclosed in the statements: "an optimal contract from Proposition 1" in Corollaries 2–3 and in the goal is read as every optimal contract of problem (1) (all optimal contracts share one agency rent, footnote 7, p. 11); existence of optimal contracts is stated explicitly wherever a statement quantifies over them; the investor's capital and the condition (p. 8) are omitted because problem (1) drops the investor's participation constraint. Each statement carries its own range of as on its page.
The agency rent is defined through problem (1) over all feasible contracts, never by the formula of Proposition 2 or the construction of Proposition 1; a formalization that defined it by the formula, or that dropped the monotonicity constraint (1f), would make the goal arithmetic or false, and is ruled out.
A complete development needs only finite sums and elementary real analysis (one-sided slopes, convexity on an interval); Mathlib suffices. Contributions welcome: proofs of the milestones, a general lemma on fractional knapsack problems (reusable beyond this mission), and the paper's remaining results (Propositions 3–5 and 7).
A series system works only if every one of its components works. Deciding whether it works by inspecting components one at a time, in the order that minimizes the expected inspection cost, is the classic sequential testing problem for series systems (Mitten 1960; Butterworth 1972; Simon & Kadane 1975). It is solved by sorting the components by the ratio . In medical diagnosis, quality control and software testing, tests are often run in batches: a laboratory charges a fixed shipping-and-handling fee per batch on top of the per-test fees. Daldal, Gamzu, Segev & Ünlüyurt (Naval Research Logistics, 2016) introduced this sequential batch testing problem and gave a -approximation. Segev and Shaposhnik (SSRN 3277805, 2018; Operations Research) settled its approximability up to with a polynomial-time approximation scheme (PTAS).
Timeline:
Let be independent Bernoulli variables with . Testing costs , and each batch also costs a set-up cost . A testing scheme is an ordered partition of . Batch is inspected only if every earlier batch found no zero, which happens with probability . The expected cost is
and the problem is to minimize over all testing schemes.
The algorithm first scales the costs by and rounds each up to a power . The variables then fall into cost classes of equal rounded cost. A state is a vector in : it records that the lowest-probability variables of each class have been tested. is the product of their . An action costs , in normalized units. For a set of states , a -path runs through with strictly increasing states, and costs . is the least such cost.
Let be the largest class with , and let . A state is nice-looking if every class is exhausted. It is great-looking if, in addition, on each of the middle classes it holds
for some integer and non-negative integers with . Here rounds down to a power of 2. and denote these sets.
For : the dynamic program over has an optimal path. The testing scheme of any optimal path satisfies, with the original costs,
and .
The PTAS shows that batch testing of series systems can be approximated to within any factor in polynomial time for fixed , improving the earlier constant factor . Its ingredients are general tools of approximate dynamic programming: a structural ordering that turns schemes into count vectors, a collapse of the state space by exhausting cheap classes, and a rounding of the middle classes onto a coarse power-of-two grid. Local charging arguments control the error of the last two. These tools apply beyond this problem.
The result is proved on paper; nothing in it has a machine-checked proof that we know of. A formalization produces a checked chain from the testing model to the approximation guarantee, including the delicate parts: the rounding interplay in Lemma 5, the double-sum exchange in the proof of Theorem 3, and the case analysis of inequalities (8)–(12). It also makes explicit what the paper leaves as and . The resulting library of testing schemes, count-vector dynamic programs and restricted state spaces can be reused for other sequential testing models.
Restricting the dynamic program to a small set of states can only make it worse. The work is showing it is not much worse, and the obvious charging fails. Exhausting all cheap classes at once (Theorem 2) costs only a factor , but it leaves states, which is quasi-polynomial. Rounding the middle classes onto a grid shrinks the state space to polynomial size, but a per-step rounding error is not small compared with that step's own cost. It must be charged to the cost of all earlier steps. That charge is affordable only because the bucketing makes the probabilities of successive steps decrease geometrically (Lemma 4). The grid must also be nested from step to step so that rounding never forces a count to decrease (Lemma 5, which relies on the power-of-two operator ). Any single per-step argument loses a factor that does not tend to .
All objects are defined from scratch in one file in BatchTesting.PTAS. The model and its conventions:
Fin n, with standing assumptions , , and . Of these, is the paper's own (p. 8); the other three are added. Every statement also assumes ; is used in the proofs of Property A and inequality (12).Finsets, and may contain empty batches. Paths are lists of states with strictly increasing steps. Every DP statement is in path form ("for every path there is a path with cost at most …"), not as an infimum over paths.The paper's "" is the explicit of its own chain on pp. 19–20. Its "within factor " is the factor , which reaches after rescaling . The running time is not formalized: the inputs are real numbers and the exponent is . The explicit bound on stands in for it.
The statement "some testing scheme is within of optimal" is trivially true, because an optimal scheme exists. The goal therefore concerns the scheme read off an optimal path over , and it carries the state count.
A complete development needs finite products over nested Finsets, an exchange argument for the greedy order, and list manipulations of paths (removing zero actions, subsequences). The counting milestone needs a stars-and-bars bound. The testing-scheme and path layer can be reused for other sequential testing problems. Proofs of any milestone, and alternative arguments with better constants, are welcome.
Consumer electronics firms receive a steady stream of defective product returns (DPRs): units that fail shortly after purchase and are exchanged for a new unit. Many of these returns are repaired and resold as refurbished products at a discount. Refurbishing is usually studied as a cost-recovery or environmental question. Singh, Ramachandran and Subramanian ask a different question: how do defective returns interact with the firm's pricing over time when consumers are strategic, that is, when they anticipate future prices and may wait?
The relevant background is the time-inconsistency problem of a durable-goods monopolist. Coase (1972) argued that a monopolist selling a durable good over time competes with its own future sales; Bulow (1982, 1986) made this precise in a two-period model and showed that a firm that cannot commit to its second-period price earns strictly less than one that can. The paper embeds defective returns in Bulow's two-period model. Returns from the first period become the supply of a cheaper refurbished product in the second, which competes with the firm's own new product in that period. The paper finds that a higher defect rate can then raise the firm's profit.
A monopolist sells over two periods to a continuum of consumers of total mass one. A consumer's quality valuation is uniformly distributed on ; each consumer buys at most one unit.
A type- consumer's discounted utilities are
for buying new in period 1, new in period 2, refurbished in period 2, or nothing. Write and .
Without commitment. The firm sets ; consumers buy in period 1 if at the second-period prices they anticipate. After observing first-period sales , the firm chooses to maximize second-period profit subject to the returns constraint , since refurbished units come only from first-period returns. In a subgame-perfect outcome the anticipated prices are the optimal ones. is the firm's optimal discounted two-period profit.
With commitment. The firm announces at the start; each consumer picks the best of the four options, and the firm maximizes subject to the same returns constraint. is the optimal profit.
For every parameter vector satisfying the standing assumptions:
At the parameters of the paper's Figure 3 (, , , , , ):
In attack order:
The result. Under commitment, defects only add friction: replacement production, refurbishing cost and hassle all lower profit, so falls with . Without commitment, the firm's temptation to sell new units again in period 2 is what lowers its profit, as in Bulow's model. Refurbished returns compete with that second-period new product, and above the firm stops offering it. The defect rate then acts as a commitment device, and on part of the parameter space profit increases with . Without the commitment benchmark, this effect could not be separated from the direct cost of defects.
Formalizing it. Proposition 3 is proved on paper through closed forms for each candidate strategy (Tables 2, 4 and 8 of the paper) and signs of derivatives. No part of it has a machine-checked proof. The mission adds a two-period durable-goods monopoly with strategic consumers to the platform, with both its subgame-perfect and its commitment profit defined from the consumers' purchase rules. Part (ii)(b) appears here in a corrected form: as printed it is vacuous (see Formalization scope), and the mission states a non-vacuous version at the paper's own numerical parameters.
is defined through an equilibrium, not a formula. Evaluating it requires three steps:
The obvious route to part (ii)(b) is to differentiate a closed form in . It fails at the step that matters: the increase happens at the boundary between strategies and , where the equilibrium strategy switches. There the profit is not given by a single formula, and the sign must be controlled uniformly in near . Part (i) needs the commitment optimum, its regime boundaries (, ), and a strictly negative derivative inside each regime, glued across regime changes.
The Lean development lives in the namespace RefurbCommit.DefectProfit. All quantities are real.
Demands are Lebesgue measures of buyer sets defined by the purchase rules, not the closed forms (4.2), (4.4), (B.19). The closed forms omit the clipping of to . A consumer indifferent between two options counts in both buyer sets; the overlaps have measure zero.
Second period. The remaining types are . Prices are optimal if they satisfy the returns constraint and maximize among all prices that satisfy it.
is the supremum of (4.5) over subgame-perfect outcomes . In such an outcome, is the first-period demand at under the anticipation , and is optimal given . is the supremum of (B.20) over feasible committed prices. Both suprema are taken in ; the commitment set always contains .
Added hypotheses, each disclosed in the item concerned:
The paper's bound (p. 8) is not imposed.
Part (ii)(b) is pinned to the Figure 3 parameters, and is required. As printed, "there exists such that is non-monotonic when " holds vacuously with . A formalization that lets , lets depend on , reads "non-monotonic" as "not nonincreasing" only, or defines or by the paper's closed-form tables is trivial and does not capture the result.
A complete development needs the following:
The buyer-set and second-period lemmas apply to other two-period vertical-differentiation models. Contributions of any of these lemmas, of exact profit formulas proved from the definitions, and of the closed-form strategy tables as theorems are welcome.
A data center can save energy by running fewer servers when demand is low, but restarting servers costs energy and queued work delays users. A controller must choose capacity while demand arrives, with limited knowledge of future traffic. Forecasts can help, yet an inaccurate forecast can make a controller perform worse than one that ignores it. Rutten and Mukherjee study this tension in a continuous-time fluid model and give a controller whose cost improves with prediction quality while retaining a bound for arbitrary predictions (arXiv:2101.12160v2, §§2–4).
The paper’s Adaptive Balanced Capacity Scaling controller, or ABCS, joins an online controller to Adapt to the Prediction, or AP. AP starts with an offline capacity plan for predicted arrivals and reacts to arrivals missed by the forecast. ABCS uses AP as advice while changing its own response rates according to the current queue and capacity. Theorem 4.11 gives an explicit bound for both accurate and inaccurate forecasts (Rutten–Mukherjee, p. 16).
Time ranges over a known finite interval , with . An arrival rate brings divisible work into a queue. A server schedule supplies processing capacity, with . The workload is the work waiting at time . It increases when arrivals exceed service and decreases under spare service only while work is waiting. The defining equation is
The objective combines three costs. With waiting weight , activation price , and operating rate , the cost is , plus times the limiting sum of positive capacity increases, plus . The offline optimum is the infimum of total cost over feasible schedules for the actual arrivals. The infimum is attained according to Proposition 2.2 (pp. 7–8, equations (2.1)–(2.3)).
A prediction covers the same horizon. Its mean absolute error is . It is -accurate when and . An algorithm has competitive ratio at most if its cost is at most for every instance and applicable prediction. These are Definitions 3.1–3.3 (pp. 10–11).
AP adds to an offline optimum for an online response to positive underprediction . ABCS receives AP’s server schedule and the workload that schedule would produce under actual arrivals. It chooses its own schedule by an integrated form of the differential rule . The coefficients switch between and by comparing with , as specified in Algorithm 3 (pp. 13–15).
For every -accurate prediction, the goal is
The constants and are exactly the rate-dependent formulas in equation (4.14), with through defined there. The first term approaches as prediction error shrinks; the second is a uniform bound over predictions. The goal quantifies over every admissible instance, forecast, AP advice, and ABCS trajectory. It is the pointwise cost form of the paper’s competitive-ratio statement, Definition 3.3 (p. 16, Theorem 4.11).
The milestone list includes the offline minimizer, the pessimistic bound , the advice comparison , and AP’s additive prediction-error bound. It also records equations (A.32), (A.34), and (A.30), which express the cost decomposition and online-correction estimate used for AP (pp. 8, 14, 22–23, 35).
The theorem puts the quality of a forecast into the same cost units as waiting, server activation, and operation. A good forecast yields the OCR term; a poor one cannot push the bound above PCR. The constants expose how the four ABCS response rates trade closeness to advice against protection from bad advice. In the zero-confidence setting , the paper reports both ratios equal to five; for instance , gives from (4.14) (p. 16, Remark 4.14).
The paper proves the mathematical result. The present formalization supplies precise Lean statements for the model, controller rules, intermediate claims, and final bound; their proofs remain to be machine checked. A complete proof would also make the reflection workload, limiting switching cost, and potential-function inequalities reusable in continuous-time online optimization.
The comparison bounds require potential functions whose derivatives balance queueing cost, capacity increases, and power cost across several switching cases. The case analysis in Appendices A.9–A.10 depends on regularity of the trajectories and of the advice. Simply integrating a differential inequality is insufficient until absolute continuity and the behavior at switching times are established. The existence of an ABCS trajectory for general arrival processes is not proved in the paper, so it is a separate analytical issue (pp. 37–45).
The offline existence result has a different obstacle: the capacity activation term is a limsup of positive mesh increments and does not vary continuously with the schedule in an elementary function norm. The paper uses a selection argument. The AP estimate also needs the one-sided queue reflection to behave appropriately when predicted arrivals and underprediction are separated (pp. 29–30, 34–36).
Lean represents time and rates by real numbers and costs and the offline infimum by extended nonnegative reals . The workload is an implicit integral-equation predicate. Offline optimization ranges over feasible schedule–workload pairs. AP and ABCS are trajectory predicates, with the latter expressing the integrated differential equation; the statements concern every trajectory satisfying it. They do not assert general existence. The zero-arrival instance has explicit AP and ABCS trajectories in a separate sanity check.
The source assumes nonnegative arrivals and predictions, , , , and . Lean additionally requires integrability of arrival rates and relevant integrands. It uses because real division by zero would turn the paper’s infinite constants into finite Lean values. The AP correction starts at zero, as required by the server schedule’s initial value. The mesh activation sum clips its last interval at so that cost through depends only on through . These choices are recorded with the item statements.
The cost keeps explicit because ABCS reads queue values. The accuracy condition uses extended nonnegative arithmetic and expresses without dividing by a possibly infinite optimum. The formalization rules out zero-denominator constants, default values from nonintegrable Bochner integrals, dependence on schedules after the horizon, and a vacuous zero-instance controller. Contributions on workload reflection, switching-cost limits, offline attainment, controller existence, and the stated milestones are welcome.
A trade moves the price at which subsequent trades are executed. Price impact models describe this shift as a function of the signed order flow and are the basic input of optimal execution and statistical-arbitrage problems. Empirically, the immediate impact of a trade is a concave function of its size, close to a square root for large orders (Bouchaud et al. 2009; Bucci et al. 2019), while most tractable models for optimal trading assume linear impact, as in the model of Obizhaeva and Wang (2013). Muhle-Karbe, Wang and Webster (SSRN 4286108; Operations Research, 2022) connect the two: when trades are small, frequent and diffusive, a nonlinear propagator model with concave impact converges to a linear impact model whose illiquidity parameter is stochastic and moves with the volatility of order flow. This mission formalizes that scaling limit, Theorem 3.3 of the paper, together with the steps of its proof in Appendix A.1.
Fix a horizon and a filtered probability space carrying two independent -Brownian motions and . The signed order flow is an Itô process with stochastic volatility,
where are locally bounded càdlàg processes, , and .
Divide into steps of width , with grid points and increments . An impact function is odd, continuously differentiable and concave on . The nonlinear propagator model (Definition 2.1) with the diffusive scaling (3.1) is the recursion
for a decay rate : each trade shifts the price by a concave function of its size, and the shift decays exponentially.
The limit involves Gaussian averages of . With the density of the centred normal law with standard deviation ,
and .
A limit of this kind lives on an extension of the probability space, a larger filtered space with a projection preserving the law; it is very good if every -martingale remains a -martingale. Stable convergence in law of processes on to on such an extension means for every bounded measurable on and every bounded path functional that is Lipschitz for the uniform distance on .
As , the step paths converge stably in law to a solution of the linear impact model
where is a Brownian motion on a very good extension with
stably in law, with standard normal and . 3. Rescaled convergence (p. 28): stably in law.
The theorem shows that the nonlinearity of microstructure impact does not disappear in the continuous-time limit; it is absorbed into a stochastic illiquidity that is an explicit Gaussian average of at the current order-flow volatility, plus an additional noise term and a drift correction . Section 4 of the paper uses the limit to solve optimal trading problems explicitly for nonparametric signals and to derive conditions that rule out price manipulation, and Section 5 fits the resulting model to public trading data. Without the limit theorem, those linear-model results would have no stated connection to the concave impact observed in the data.
The paper proves Theorem 3.3 by reduction to a functional central limit theorem of Jacod and Protter (2012, Theorem 10.3.2(a)), outlined in Appendix A.1 rather than written out. To our knowledge none of these results has a machine-checked proof. The mission produces a precise statement of the scaling limit, including the mode of convergence and the space on which the limit lives, and a formal statement of the stable functional CLT (Theorem A.3), which is a standard tool in high-frequency statistics and reusable well beyond this paper.
The impact process is not a functional of increments of a fixed process: solves a difference equation whose coefficients depend on the grid, so a central limit theorem for sums does not apply to it directly. Even for such sums the stable CLT is needed in full: the rescaled increments are of order one, so cannot be linearized pointwise, and the limit carries both a Gaussian average of and an independent noise term. The CLT itself is the hard part. Its limit lives on an extension of the original space, the drift term arises from the correlation between the volatility increments and the increments of , and stability (joint convergence with every bounded -measurable variable) is what allows the limit to be combined with the stochastic factor and with . A naive Taylor expansion of around zero gives the wrong limit for every nonlinear .
Time is and statements read . Brownian motions are IsBrownianReal with continuous paths for every , adapted, with increments independent of the past; Itô integrals use the published relation EthierKurtz_HasBrownianItoIntegral with continuous versions, and quadratic covariation the published EthierKurtz_HasCrossVariation. Itô coefficients are progressively measurable with locally integrable drift paths. is Mathlib's gaussianPDFReal 0 (v^2), whose parameter is the variance. Stable convergence is encoded with bounded measurable times bounded functionals Lipschitz for the -valued uniform distance on ; since the limits have continuous paths this matches Skorohod-topology stable convergence, and no Skorohod space is built. The goal is existential in the extension, in and in the solution ; a universal reading would be false.
Added and disclosed conventions: the growth bound (Assumption A.2(c), p. 25, required by the paper's proof); and ; capped at for the paper's ; for the negative powers on p. 27. The printed formulas for and are kept.
The statements cannot be satisfied trivially: is a solution of the integral equation (3.2), not a definition as the limit of ; the coefficients are the Gaussian integrals themselves; and the test class of stable convergence contains non-constant functionals, so convergence of the zero process to a non-zero limit fails (checked in a sorry-free sanity file).
A complete development needs a stable functional CLT for triangular arrays, Gaussian integration by parts, existence of very good extensions carrying independent Brownian motions, and pathwise stochastic calculus for Itô processes with stochastic volatility. The extension and stable-convergence definitions and Theorem A.3 are reusable for realized-variance and high-frequency estimators. Contributions on any milestone, and on the general infrastructure, are welcome.
Most equity markets trade through a continuous limit order book (CLOB): any market order is matched immediately against the resting limit orders. Budish, Cramton and Shim (QJE 2015) argued that continuous matching creates mechanical arbitrage and a race in speed between high-frequency market makers, and proposed frequent batch auctions instead, with a lower bound of about 100 milliseconds on the auction period. Earlier work, notably Madhavan (J. Finance 1992), compared auctions and continuous markets through the quality of price formation. What neither line of work gives is a quantitative answer to the question an exchange designing a periodic auction has to settle: how long should an auction last? A longer auction gathers more liquidity before the price is fixed, but the information on which that liquidity was posted grows stale.
Jusselin, Mastrolia and Rosenbaum (arXiv:1906.01713, published in Operations Research, 2021, doi:10.1287/opre.2021.2113) model a market organized in sequential call auctions triggered by market orders, measure the quality of price formation by the mean squared distance between the clearing price and the efficient price, and give this error in semi-explicit form as a function of the auction duration (their Theorem 2.1). Minimizing the formula on Euronext data gives optimal durations of a few minutes. This mission formalizes that formula and the lemmas of its proof.
Fix constants , , , , , and an auction duration . On a probability space :
With market makers present, the clearing price solves , and the mid-price ignores the market orders:
On these are defined, and the two quality criteria are
In Lean these are E p P X h and Emid p P X h, built from Pcl, Pmid, Peff and OmegaT in AuctionDuration.ClearingError.Model.
With ,
together with the integrability of both squared errors.
The result. Theorem 2.1 turns the design question into a one-dimensional minimization: every quantity in the formula is a model parameter that can be estimated from order-book data (, , , , , ). It shows that for , quantifies the cost of market orders through , and contains the continuous order book as the case , so that the auction and the CLOB can be compared in one metric. The paper's Lemma 2.1 identifies with the almost-sure long-run average squared error over the sequence of auctions, and Section 3 feeds the formula with the imbalance produced by strategic market takers.
Formalizing it. The result is proved on paper; no part of it is machine-checked. The mission produces a formal model of a call auction with Poisson liquidity and a Brownian efficient price, a checked derivation of the error formula, and, as separable by-products, closed forms for inverse moments of a Poisson variable (Lemma A.2) and a Palm-type computation for Brownian increments sampled at Poisson points (Lemma A.1). The proof in Appendix A is a short sketch: the passage from the random clearing time to deterministic times in (8), the vanishing of cross terms, and the Palm formula step of Lemma A.1 are asserted rather than carried out.
The obvious argument conditions on everything and expands the square. The random clearing time is the obstacle: the number of market makers, their arrival epochs and the Brownian value at the clearing all depend on , and the conditioning on couples the Poisson process with the opening time, so neither can be treated as having its unconditional law. Turning (8) into a rigorous statement needs a disintegration over and measurability of Brownian motion evaluated at random times. Lemma A.1 needs the conditional uniformity of Poisson arrival epochs given their number (or the Mecke–Palm formula) combined with independence from ; neither is available off the shelf. The Lemma A.2 identities are series manipulations, but they require exchanging sums and integrals of near .
AuctionDuration.ClearingError.Model defines Params (with Standing: , ), the random objects Auction (W, interarrival times A, opening time T, noises g, imbalance J), the hypothesis bundle IsModel, and Nmm, tauCl, Peff, view, Pmid, Pcl, OmegaT, E, Emid, gFun, fFun, ellFun. Market-maker arrivals use the published definition QueueingFundamentals.Foundations.ArrivalProcess (IsExpInterarrivals, arrivalTime, countingProcess); the Brownian motion is Mathlib's IsBrownianReal.
Conventions the formalization commits to:
g k and arrivalTime A (k+1) are the paper's and . is indexed by and evaluated at t.toNNReal.P[|OmegaT X h], and , , carry the indicator as on the page. Inner integrands are at , a null set., , , and are expectations over the model, not their closed forms: defining any of them by the formulas of Theorem 2.1 or Lemmas A.1–A.2 would make the goal or a milestone true by definition, and is ruled out. Integrability conjuncts in the goal, (8) and Lemma A.1 prevent a junk Bochner value from satisfying an identity.
Useful published facts: QueueingFundamentals.Foundations.poisson_count_cdf (Proved) gives the Poisson law of countingProcess for exponential interarrival times, which reduces Lemmas A.1–A.2 at fixed to Poisson-distribution computations. Contributions of general value are welcome: conditional uniformity of Poisson epochs, a Mecke formula for the published arrival process, measurability of Brownian motion at random times, and inverse-moment identities for the Poisson law.
In a bilevel program, the decision maker chooses an upper-level variable while a second decision must solve a lower-level optimization problem. This structure occurs when a leader anticipates the response of a follower, or when an outer design problem contains an optimization problem as a constraint. A feasible upper-level decision can therefore change the lower-level solution set as its parameters move. Ordinary smooth constrained optimization tests do not directly describe that dependence. Mehlitz and Zemkoho study sufficient optimality conditions for this setting; their Theorem 5.3 gives a second-order condition ensuring a strict local minimum with quantitative growth. Mehlitz and Zemkoho, 2019
Write for the upper-level decision and for the lower-level decision. The upper-level objective is , with componentwise constraints . At each fixed , the lower-level feasible set is , and its solution set is . The bilevel feasible set is . The program minimizes over . All components of are twice continuously differentiable, as assumed on page 2 of the source. Mehlitz and Zemkoho, pp. 1–2
The lower-level value function is . It may be nonsmooth even though the data are smooth. The condition can be expressed using and , giving the value-function reformulation. For the main theorem, is locally Lipschitz near the reference point and has a second-order directional derivative . This derivative measures the second-order change along the curved path , after subtracting the first-order directional term. Mehlitz and Zemkoho, pp. 5, 8–9
At a feasible point , the paper defines a linearization cone by the active and inequalities and the linearized value-function inequality. Its critical cone adds the directions in which the first-order change of is nonpositive. The Abadie constraint qualification, abbreviated ACQ, equates the tangent cone of with its linearization cone at . It is imposed on this lower-level constraint set in the joint space. Mehlitz and Zemkoho, pp. 18–19
The goal is Theorem 5.3. At a feasible , assume ACQ for the lower-level constraint set, local Lipschitz continuity and second-order directional differentiability of , and second-order epi-regularity of . The first-order test requires on . For each nonzero , the minimax program (5.5), formed from the second-order expansions of , active , , and active , must have positive optimal value. The conclusion is
and is a strict local minimizer of the bilevel program. The milestones capture the paper's supporting results: the derivative formula, rules for a finite maximum, the Hadamard derivative and tangent-cone necessary condition, Remark 5.1 under ACQ, and Proposition 2.10 on second-order growth. Mehlitz and Zemkoho, Theorem 5.3, pp. 19–20
The theorem turns tests on first- and second-order directional behavior into a guarantee about actual feasible bilevel decisions near the reference point. The growth estimate is stronger than strict local minimality: it quantifies how the upper-level objective rises with displacement along the feasible set. It applies when the lower-level value function is nonsmooth, provided its directional derivatives and epi-regularity are available. The paper gives special cases in which these hypotheses can be checked more concretely. Mehlitz and Zemkoho, §5, pp. 18–28
The result is proved in the source paper. The open work here is a machine-checked development of its variational definitions, finite-maximum rules, and sufficient-condition argument. The mission includes open Lean statements, not completed proofs. The reusable part is the generic theory of directional derivatives, epi-regularity, and growth on finite-dimensional normed spaces; the bilevel model and cones specialize it to this paper.
Smooth Taylor expansion alone does not handle : an infimum over a parameter-dependent feasible set can be nonsmooth. First-order stationarity on the paper's linearization cone also gives no quadratic increase in directions where the first-order change vanishes. The second-order test must retain the active indices of each constraint and the dependence of on both the first- and second-order directions. ACQ matters because the tangent-cone necessary condition for does not automatically apply to every linearized lower-level direction; Example 5.2 of the paper demonstrates the failure without a constraint qualification. Mehlitz and Zemkoho, pp. 19–20
Lean uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), with zero-based Fin indices and uncurried maps on their product. Fréchet derivatives express the paper's gradient and Hessian terms. Generic preliminary results are stated on finite-dimensional real normed spaces, a generalization of the Euclidean statements. The tangent cone uses positive sequences converging to zero. Directional derivatives are named finite limits; epi-regularity uses the eventual inequality for every admissible curved path and every positive error coefficient. The value function takes values in EReal, so an empty feasible set and an unbounded-below lower-level problem are represented by and . A real representative agrees with it on a neighbourhood of , where the local Lipschitz and derivative hypotheses apply. This agreement rules out an unrelated or default-valued value function.
The theorem's growth estimate uses the sum of squared Euclidean norms printed in (5.6), not the product space's sup norm. The positive value of (5.5) is expressed by a uniform positive lower bound over every on its maximum of constraint expressions. The generic maximum rules use a nonempty finite index type. The preliminary formulation of Proposition 2.10 includes local Lipschitz continuity, used in this mission's application and disclosed as an added hypothesis relative to its printed statement. Real-valued functions and finite second-order limits are also explicit scope conventions.
Dividing indivisible goods fairly among agents with different preferences is a central problem of fair division, with uses ranging from inheritance and divorce settlements to course allocation and fair-division services such as Spliddit (Goldman–Procaccia 2014). Envy-freeness cannot always be achieved with indivisible goods (one good, two agents), so relaxations are studied. Envy-freeness up to any good (EFX), introduced by Caragiannis et al. (2019), is widely regarded as the strongest relaxation of this kind whose existence is still unsettled: whether every instance admits a complete EFX allocation is open in general, even for additive valuations.
Timeline.
There are agents and a set of indivisible items. Each agent has a valuation assigning a real number to every bundle . It is normalized, , and monotone, . Nothing else is assumed (general valuations: no additivity, submodularity or cancelability). Write for .
An allocation is a family of pairwise disjoint bundles. It is complete if every item is allocated, and partial otherwise. Agent envies if . Agent EFX envies if for some . The allocation is EFX if no agent EFX envies another, i.e.
The two-valuation setting: there are set functions such that every equals one of them. and denote the agents with valuation and .
The proof works with a vocabulary that the definition file formalizes. The terms are non-degeneracy (distinct bundles have distinct values), minimum preferred sets and , most envious agents, -champions, the champion graph and its Pareto improvable (PI) cycles, semi-EFX allocations, and the partition leximin potential . The potential lists over in increasing order, followed by over in increasing order. means that is lexicographically larger than .
Milestones 2–6 are stated for non-degenerate instances, as in the paper. The goal is not.
The result. Theorem 1 is the most general multi-agent EFX existence theorem in which the number of agents is unbounded and the valuations carry no structure beyond monotonicity. It contains the identical-valuation theorem of Plaut and Roughgarden and the two-additive-valuation theorem as special cases. The potential is the paper's tool for making progress when no Pareto-dominating EFX allocation exists. Pareto domination is the progress measure used for additive and cancelable valuations, and it fails for general ones.
Formalization. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The remaining work is to formalize the known proof: the perturbation reduction, the champion-graph machinery (minimum preferred sets, most envious agents, PI cycles), the semi-EFX repair, and the case analysis of Theorem 14. The champion-graph layer is shared with the proofs of EFX with charity and of EFX for four agents.
The obvious argument is Pareto improvement: from a partial EFX allocation, hand out an unallocated item and keep everyone at least as well off. For general valuations no Pareto-dominating EFX allocation need exist. The progress step must therefore sometimes make an agent strictly worse off, and that agent may then come to EFX envy others. Theorem 14 allows an agent of to lose value while improving the -block of . The paper repairs the resulting EFX envy, which is confined to (semi-EFX), by trimming bundles. Keeping track of which agents may envy which bundles through several reallocations is the central difficulty. The champion-graph statements are also delicate: minimum preferred sets are not unique, and the cardinality parameter takes the value .
Agents are Fin n and items Fin m, both 0-indexed. Valuations are maps Fin n → Finset (Fin m) → ℝ, assumed normalized and monotone (IsNormalized, IsMonotoneVal). Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values (IsPartialAllocation). Completeness is pool X = ∅. EFX is IsEFX, from the published definition file LittleCharity.EFX.Setting. The two valuation classes are a finset A of agents with v i = va on A and v i = vb off A; in the goal they are ∀ i, v i = va ∨ v i = vb. takes values in ℕ∞. PI cycles are indexed by Fin k: distinct vertices, edge labels Option (Fin m), unallocated champion labels, labels pairwise disjoint. is a pair of sorted lists, and is the strict List.Lex (· < ·).
Disclosed readings:
The goal assumes neither additivity nor non-degeneracy. Its only added hypothesis is , which is necessary. Every item must be allocated: the empty allocation is always EFX, so a goal without completeness would be trivial. Contributions are welcome at every level: proofs of the milestones, the champion-graph library, and the termination argument for strict lexicographic orders on finite sets.
A polynomial that is positive away from the origin can be certified by writing it as a sum of squares after multiplication by a suitable power of the squared Euclidean norm. This is the uniform denominator theorem of Reznick (1995). In polynomial optimization, the size of a sum of squares certificate is governed by the number of variables in each square. A dense certificate can therefore lose the computational advantage of a polynomial whose terms involve only small groups of variables. Mai, Magron and Lasserre establish a version of Reznick’s result in which every numerator retains its own variable block. The question addressed here is the exact algebraic statement of that certificate, including its denominators and degree bounds.
A form of degree is a homogeneous polynomial in real variables ; it is positive definite when for every . The variables are covered by nonempty blocks , with . Write for the coordinates in block and for any coordinate set . A sparse form has a decomposition , where each is a degree- form in . Individual need not be positive.
The running intersection property assigns every block an earlier parent . Its overlap with preceding blocks, , must be contained in . This condition lets the certificate keep each numerator in one block. The paper defines a polynomial by multiplying squared norms of (except at the first block) and of later overlaps whose parent is . It then sets . The set consists of finite sums of squares of polynomials in the variables with total degree at most .
A second class of objects appears in the supporting results. A continuous rational form is a continuous, homogeneous function represented by a quotient of polynomials wherever the denominator is nonzero. It is positive definite on a block when it is positive wherever the coordinates of that block are not all zero. This block condition is weaker than positivity at every nonzero point of the full ambient space, since the form ignores coordinates outside its block.
The goal is Corollary 2.1 of the pinned preprint. For a positive definite form of degree , with and each supported on , it asserts the existence of a single and blockwise sums of squares such that
This is an identity of rational functions, evaluated where its denominators are nonzero. The degree index is part of the target: leaving it free would discard the quantitative certificate. In the formal statement, every overlap with is assumed nonempty so that the printed is a nonzero polynomial.
Theorem 2.1 is the last milestone. It begins with a positive definite rational form , in which is homogeneous of degree , and yields the same blockwise degree bound with a common exponent . The polynomial goal follows by taking every . Earlier milestones state the paper’s continuity, approximation, block-splitting, and uniform denominator results.
The result supplies a certificate whose numerator for block uses only variables in that block. That is the structural property needed when a polynomial optimization problem is represented by smaller semidefinite constraints instead of one dense constraint. The running intersection hypothesis is explicit, so the theorem also records when that sparsity claim applies. The common exponent and exact bound on each numerator make the certificate suitable for a hierarchy indexed by degree, as described in the source paper.
The 2020 preprint proves these mathematical results; this mission asks for machine-checked proofs of the statements in Lean. The definitions of sparse sums of squares, rational forms on blocks, and running intersection data are reusable in other polynomial optimization formalizations. No proof of the target is claimed by the draft statements themselves.
A dense Reznick certificate does not identify numerators in individual blocks. Even if the sum is positive definite, a summand can be negative, so a separate application of a positivity theorem to each cannot establish the target. The supporting statements must express how positivity is recovered on each block while preserving both the rational representation and variable support. The denominator factors also overlap: their degree contribution depends on the parent map , so the final bound must track each factor rather than only a global degree.
Lean uses MvPolynomial (Fin n) ℝ, with blocks as finite sets of coordinate indices and a zero-based Fin p block index. The paper’s first block is index zero in Lean. The standing condition from page 3 is explicit in supporting lemmas that do not assume the running intersection property; that property already implies it for the other results. Its squared Euclidean norm is the polynomial ; the function norm on Fin n → ℝ is not used for this purpose. A sparse sum of squares is represented explicitly as a finite sum of squares whose bases lie in Mathlib’s supported subalgebra. The paper’s is encoded by its combinatorial formula, which is even under the nonempty-overlap assumption. Lemma 3.3 requires the approximating polynomials to have exact total degree , as printed.
The printed formulas divide by , although the stated running intersection property allows an empty overlap and then makes that polynomial zero. The goal and Theorem 2.1 add nonempty overlaps for later blocks; Lemma 3.6 similarly requires every denominator block to be nonempty. Lemma 3.5 adds , used by its cited continuity result. These are disclosed restrictions to the printed statements, rather than conclusions hidden in definitions. Rational identities are pointwise on the set where every displayed denominator is nonzero; at a zero denominator, Lean’s total division returns zero. The quotient in the continuity lemma takes that zero value at the origin.
The supporting statements retain the restriction that every is a sum of squares in , the fixed degree bound, and positivity on each block’s own nonzero inputs. The nonempty-overlap conditions ensure the rational identity has points where all denominators are nonzero. Work on the algebraic preordering and real spectrum, homogeneous polynomial approximation, continuous rational forms, and degree control is within scope. The paper’s other main result, its sparse Putinar–Vasilescu certificate, is a separate target and is not stated here.
A probability distribution can spread its mass while remaining inside a set of limited diameter. A bound on the diameter alone does not specify its center, shape, or number of support points. Lim and McCann ask how large a recentered moment can become under this sparse geometric information. Their answer identifies a regular simplex as the extremal configuration: in dimension two it is an equilateral triangle, and in dimension three a regular tetrahedron. This gives an exact higher-dimensional analogue of the familiar one-dimensional observation that a distribution on an interval maximizes variance by placing equal mass at the endpoints. The paper frames the question in connection with systems of particles or organisms that prefer separation from one another, where a diameter constraint limits how far their spatial distribution can spread (Lim and McCann, 2020, pp. 5–7).
The mission follows the first arXiv version of the paper. The theorem is already proved in the source. The formalization task is to express its sharp bound and its equality case precisely in Lean, together with the geometric statements that distinguish the simplex from other diameter-constrained supports.
Work in Euclidean space with its ordinary distance. For a Borel probability measure , its support is the smallest closed set carrying all its mass. The diameter of the support is the supremum of the distances between its points. A bounded diameter places no restriction on where the support sits in space: translating the distribution leaves the diameter unchanged.
For a nonnegative convex function , the generalized variance allows the center to move:
The center minimizing this integral can depend on and need not be the ordinary barycenter. For it is the barycenter and the expression is classical variance. This mission focuses on radial functions , where is convex and increasing on nonnegative radii. The paper's definition and the relation to classical variance appear in equation (1.8) and Remark 1.6 (pp. 4–5).
A regular -simplex in has vertices, and every pair of distinct vertices has the same positive distance . Its uniform vertex measure assigns mass to each vertex. Write
This is the distance from the centroid to each vertex when the simplex has side length one. The paper defines regular and unit simplices in Definition 1.8 and identifies this radius in Proposition 3.1 (pp. 6, 13).
For a Borel probability measure with , the target is
Here , so the argument belongs to the domain on which is specified. The bound fixes the optimal constant in every dimension and for each eligible radial cost (Theorem 1.10, pp. 6–7).
When and is differentiable at , equality is characterized by a regular -simplex with side length :
The source's proof uses a maximization principle for generalized variance (Theorem 1.7), a constraint placing a minimizing center inside the support's closed convex hull, the two parts of Proposition 3.1 on spherical sets, and the uniqueness of barycentric weights in Remark 3.2. Those statements are the five milestones. Their order follows the progression from the measure problem to the limiting geometry and finally to equal mass (pp. 5, 13, 15).
The bound controls every convex radial recentered moment allowed by the hypotheses using only the diameter and dimension. Its equality clause identifies the entire extremal distribution, rather than merely the value of the maximum. For squared distance, this recovers a sharp variance statement; for powers of the distance, it supplies corresponding recentered moment bounds (Example 1.11, p. 7). The geometric threshold also links the paper's result to Jung's enclosing-ball theorem, which the authors discuss separately (Theorem 1.12 and §3.1, pp. 7, 15–16).
A complete Lean proof would connect measure-theoretic optimization to finite-dimensional convex geometry. It would provide reusable formal statements for generalized variance, support-constrained probability measures, simplex geometry, and the equality mechanism. The source paper proves these results mathematically. In this mission, the Lean statements are drafted and compile with proof placeholders; they do not yet have machine-checked proofs.
The diameter restriction is imposed on the support, which need not be convex. Replacing it by a restriction on a convex set loses the particular geometry that makes the simplex extremal. The minimizing center is also part of the optimization: evaluating the integral at the barycenter would change the object for a general radial cost. In the equality case, knowing only that the support lies on a sphere is insufficient. The radius must reach exactly , the spherical support must be precisely the simplex vertices, and the mass at those vertices must be equal. Proposition 3.1 and Remark 3.2 isolate these separate assertions (pp. 13–15).
Lean represents as EuclideanSpace ℝ (Fin n), with the Euclidean norm and Borel measurable space. The support diameter in the goal is the extended metric diameter, which correctly excludes unbounded supports from a finite bound. The paper's is its smallest closed convex hull, so the statements use closedConvexHull. Probability measures supported on carry the condition . The generalized variance is the infimum over all centers ; restricting centers to the support hull or replacing the infimum by the integral at the mean would give a different and potentially easier claim.
The function is modeled on all real numbers because Lean functions are total, but every value used by the mathematical statements is at a nonnegative radius. The hypotheses require nonnegativity, convexity, and strict increase on ; the latter makes the paper's equality conclusion meaningful. The equality clause additionally assumes differentiability at . Without it, a kinked strictly increasing convex , with a change of slope at that radius, can have unequal masses attaining the same optimum. The manuscript states the clause without this condition. Theorem 1.7 explicitly assumes nonempty, and the goal explicitly records and where they are needed. Theorem 1.7's support level set follows the sign proved on p. 12, ; the printed translated set has the opposite sign.
The definitions and theorem files contain no custom probability or simplex infrastructure beyond these source objects. Contributions proving the optimization principle, the center-in-hull claim, either part of the spherical geometry proposition, or the barycentric uniqueness statement are within scope. Theorem 1.1, the paper's separate convex-envelope result, and the deduction of Jung's theorem are outside this mission.
Online retailers and service providers quote a promised delivery time and are judged on how often they meet it. Platforms increasingly publish delivery-performance information, such as on-time ratings or conformance scores, so that consumers can weigh a quoted time against the firm's record. Producing accurate information is costly: the firm must track deliveries, audit ratings and present them clearly. Whether a firm should pay for precise information, or let consumers infer its reliability from noisy signals, is a question for operations management (capacity, lead-time quotation) and for marketing (pricing, information disclosure) at once.
Leng, Becerril-Arreola, Parlar and Ferguson (MSOM 2024; the mission follows the authors' preprint of April 2nd, 2023) model a firm that jointly sets a price, a promised delivery time and an effort toward the quality of its conformance information, facing consumers who care about all three. Their central analytical result, Theorem 1, says the firm should never invest partially: the optimal effort is either none or full.
The model joins two lines of work. The first is joint price and delivery-time decisions with congestion, as in So (2000), Liu, Parlar and Zhu (2007) and Boyaci and Ray (2006), where delivery reliability enters demand. The second is logit demand from discrete-choice theory (Anderson, de Palma and Thisse 1992), where the scale parameter measures how dispersed consumers' valuations are.
A firm serves consumers at service rate . It sets a price , a promised delivery time , and an information-quality effort . The market has size . Each consumer compares the firm with an outside option of deterministic utility .
If consumers arrive at rate , the firm operates as an M/M/1 queue, and an order is delivered within the promised time with probability
The deterministic utility of buying is
where is the base value, and are the sensitivities to the conformance score and to the promised time, and scales the score. Effort narrows the dispersion of consumers' inferences: the utility shock has scale
decreasing from at to at .
The demand rate is the logit share times the market size (eqs. (8)–(9)):
Since depends on through , this is a fixed-point equation in . The firm earns
with unit cost and unit effort cost . A plan is feasible when , and . The optimal profit is the supremum of over feasible plans, and are the demand and utility at the optimal plan, and the gap
measures by how much Lemma 2's condition (19) holds. With the largest attainable market share (eq. (10)), the capacity condition (16) is .
Let . If
then is strictly decreasing on and is the unique optimum. Otherwise strictly decreases and then strictly increases, with the turn at some . In both cases
Three supporting items have no counterpart in the paper. They state that the demand fixed point is well posed, that is continuous on , and the envelope identity .
Theorem 1 is a bang-bang result. A firm choosing how much to spend on delivery-performance information should consider only two options, no effort and full effort, and condition (23) gives a closed-form test for when no effort is optimal. The paper's sensitivity results (Corollaries 1–4) and its numerical study are all built on this reduction, since they compare the two endpoint regimes using the closed forms in Table 1.
The result has an analytical proof in the paper's online appendix, but no machine-checked proof. The formalization adds a precise statement of the model's well-posedness: the demand is a fixed point, and the optimal plan exists and is unique. It also makes the comparative statics explicit. Parts of Lemma 2 as printed are false, namely the directions of and in item 1 and of and in item 2, and the mission states only the parts that hold. A complete development would certify which of the paper's conclusions survive and by which argument.
The optimal profit is the value of a two-dimensional optimization whose objective is defined through an implicit equation, since demand appears on both sides of the logit formula. Differentiating in requires an envelope argument over a constrained problem. That in turn requires knowing that the optimum is interior, unique and a smooth function of , and that the queue constraint does not bind.
The single-crossing step is the delicate one. The paper reaches it through a derivative of with respect to (eqs. (30)–(34)) whose sign claims are partly wrong. The tempting shortcut, to read the sign of off the sign of , is unsound: when (19) holds, can rise while falls.
Everything is real-valued and lives in the namespace DeliveryDisclosure.InfoEffort. A structure Params holds , and the predicate Standing bundles the standing assumptions. The paper writes but divides by them, so Standing requires , together with and condition (16) for every .
Real.sigmoid gives the logit share.is defined as a supremum over all feasible plans and uses at the optimum, which rules out a trivializing formalization: cannot be replaced by Table 1's closed forms, by profit at a fixed plan, or by a demand with the conformance frozen. Lemma 1's corner case (item 1), Claim 1, Remarks 1–5, Table 1 and Corollaries 1–4 are not formalized.
A complete development needs implicit differentiation of a fixed point, an envelope theorem for a two-variable constrained maximization, and existence of maximizers on a non-compact feasible set. These ingredients apply to other congestion-pricing and logit-demand models. Contributions toward any milestone are welcome, as are proofs of the supporting items.
Time-series momentum is the empirical regularity that an asset's recent excess return predicts its future excess return. It has been documented across equity indices, currencies, commodities and bonds (Moskowitz, Ooi & Pedersen 2012), and momentum portfolios are among the most widely traded systematic strategies. Most of that literature builds portfolios from a single signal: the average return over a look-back window. Li and Liu (Operations Research 2022) ask what a long-horizon investor who rebalances should do when expected returns really are driven by such a moving average. Their answer has a structural feature that a Markovian model such as Merton's (Merton 1971) cannot produce. The optimal weight depends on the whole recent price path, not only on the current momentum.
A risky asset has price and log price , with
where is a Brownian motion. Momentum is the equally weighted moving average of excess returns over a look-back window of length . The parameter measures how strongly momentum enters the expected return, is the unconditional risk premium, is the constant short rate and is the volatility. Because the drift depends on , the price is not Markov: the state at time is the whole path on .
An investor with constant relative risk aversion maximizes expected utility of terminal wealth at a horizon by trading the asset and a riskless bond. The mission works in the paper's short-horizon regime , with the investor standing at time , so the realized path on is known.
The paper's analysis (Appendix A.2) produces the following objects:
The Lean development names them theta0, SolvesA9, phiStar, C0, omegaHat, omega and C1 in the namespace DynMomentum.ShortHorizon.
For every solution of (A.9),
Moreover, is positive on when , strictly increasing on , and constant on . The first summand is the myopic mean-variance weight; the second, , is the hedging demand.
The result. Proposition 3.3 shows that a momentum investor who rebalances should not trade on momentum alone. The hedging demand weights past returns unequally, with more weight on recent ones, so two price paths with identical momentum lead to different optimal positions. This is the paper's explanation of why path dependence is intrinsic to optimal momentum trading. It underlies the paper's later comparisons with momentum-only strategies, the horizon extension of Proposition 6.3, and the closed-form expansions of Online Appendix III.
Formalizing it. The proof's analytic half, from (A.9) to (3.8), is summarized in the paper by the phrase "after some manipulations". Writing that step out yields a checked identity between an ODE-defined weight and an explicit integral formula. Doing so has already caught an error. The constant printed in (A.14) is wrong: it differs from the true value by a path-independent amount, and it becomes correct after deleting both occurrences of (a numerical solution of (A.9) agrees with the corrected formula to ). The proposition is proved in the paper. As far as is known, no part of it has been machine-checked.
Each milestone is a direct calculus statement; the goal is not. The obvious approach is to substitute the closed forms (A.13) into (A.11) and simplify. That leaves as a double integral of the past path against two nested exponential kernels written in the ODE's own parameterization, while (3.8) is a single integral of returns against the weight of (A.14), which is written in a different parameterization. The paper gives no derivation of the match. The path is only continuous, so no step may differentiate . Separately, the Riccati closed form divides by a quantity that vanishes for small , so every step has to track where that denominator is positive.
HasDerivWithinAt, interval integrals, Real.exp and Real.sqrt. Two lemmas are reusable well beyond this mission: the closed form of a constant-coefficient scalar Riccati equation, and variation of constants for a scalar linear ODE with merely continuous forcing. Contributions of those lemmas, of uniqueness for (A.9), and of the integration-by-parts step are welcome.A simulation may give precise answers under specified input distributions while the distributions themselves are estimated from limited data. In a queueing model, for example, arrival and service times are fitted from observations before the queue is simulated. Repeating the simulation more often reduces simulation noise, but it does not remove uncertainty in those fitted inputs. Lam and Qian study the variance attributable to that data uncertainty and an estimator that can remain relatively accurate with a simulation budget that grows much more slowly than the data size Lam and Qian, pp. 6–7, 13–17.
The paper uses a nonparametric model: an input distribution is estimated by the empirical distribution of its observations. This matters when a finite-dimensional parameterization is unavailable or would conceal sensitivity to parts of the distribution. The variance is small, of order , so an estimator with small absolute error can still have poor relative error. The mission targets relative consistency, which asks that the ratio of estimated to true input variance approach one.
There are independent input processes. Process has a true probability law on a measurable space and independent observations . Its empirical law is . A real performance functional gives the expected simulation response under a vector of input laws. The input variance is the variance over the observed data,
To estimate it, Algorithm 2 chooses a common subsample ratio and takes observations with replacement from each empirical input law. It draws independent vectors of subsamples and produces independent simulation responses for each vector. Each response has conditional mean at its resampled input laws. Let be the mean of the responses in group , the mean of the group means, and the pooled within-group sample variance. The reported proportionate subsampled variance bootstrap estimate is
The comparison quantity without simulation error is , where the star means variance over subsampling conditional on the original data. Both quantities are defined in the paper pp. 15, 17, equations (4) and (8).
Write for the average input data size. The goal is Theorem 2 p. 15: under Assumptions 1–7, as every , if
then
The milestone list follows the paper's supporting results. Proposition 1 identifies the first-order scale , with the variance of the th influence function. Theorem 7 gives in probability without Monte Carlo error. The first sentence of Lemma 1 states exact conditional unbiasedness of for . Its conditional mean squared error formula is also posed as a milestone in a labelled corrected form; the printed formula (18) omits a term when remains bounded pp. 22, 25; proof p. ec14.
The theorem makes a precise distinction between a small subsample and an inaccurate variance estimate. The subsample can be much smaller than the original data set, yet the estimate retains the correct first-order input-uncertainty scale if the stated parameter rates and regularity conditions hold. This supports the paper's later simulation-budget statements, including the possibility of a budget whose growth rate is independent of the original data size pp. 16–17.
The mathematical results are proved in the cited paper; the goal here is a machine-checked formalization of their statements and eventually their proofs. The reusable output includes empirical and resampled measure constructions, an explicit conditional simulation law, and formulations of convergence for estimators that depend on both observed data and resampling. The corrected mean squared error target records a limitation of the printed asymptotic constant rather than treating that display as a verified fact.
The input variance shrinks like , so absolute consistency alone cannot establish the ratio limit. The resampling approximation and the Monte Carlo output have different sources of error, and each must be small relative to this shrinking target. The performance functional need not be linear in its input laws: the influence-function expansion has remainders under both the original empirical laws and every mixture of empirical and resampled laws. The simulation response also has input-dependent variance and a fourth moment. Treating it as fixed-variance noise would change the conditions being formalized. The paper's first-order assumptions and its conditional moment assumptions must therefore be represented on the same asymptotic regime.
The Lean model uses one infinite independent array of observations, with a finite prefix for each data size. A theorem quantifies over arbitrary sequences of data-size vectors and algorithm parameters; every input sample size diverges, and Assumption 1 bounds ratios of sizes eventually. The paper's support is represented by a measurable full-measure set of allowed point masses. Assumption 2 quantifies over the finite convex mixtures of and Dirac laws at points of , rather than over all probability measures. Its signed-measure integral is written as a difference of ordinary integrals. Conditional bootstrap expectation is an exact finite average over with-replacement index maps. Independent simulation responses are represented by product measures of an unbiased one-replication law.
The target uses the conditional probability of a relative-error event, viewed as a random quantity over the original data. Convergence of that bounded conditional probability to zero in probability is equivalent to the paper's unconditional convergence in probability. This representation avoids a zero measure produced by a nonmeasurable total-law construction. Integrability and moment guards prevent non-integrable expectations and variances from taking Lean's default zero value. The fourth simulation moment is extended nonnegative, so an infinite value stays visible. Algorithm 2 uses and ; positive sample and subsample sizes hold eventually. The unqualified in Assumption 4 is read as . For the corrected equation (18) milestone only, the true simulation variance is assumed positive. Contributions to the influence-function assumptions, bootstrap remainder estimates, and finite-product moment identities are all within scope.
Business-interruption (BI) insurance reimburses a firm for the revenue it loses while a disruption (a flood, a fire, a supplier failure) keeps its capacity down. The 2011 Thailand floods and the Tōhoku earthquake made such losses large and visible for manufacturers, and BI cover is now a standard part of commercial property insurance. Two information problems make it hard to price. The insurer does not know how strong the firm's demand will be, and so how much revenue is really at stake (adverse selection); and once a disruption happens, the insurer does not observe how hard the firm works to restore capacity (moral hazard).
Kao, Keskin and Shang (SSRN 3184530, version of May 13, 2020; published in Management Science, 2021, doi:10.1287/mnsc.2020.3776) model both problems at once for a firm with limited production capacity. Their headline is an ordering of the optimal contracts that runs against standard screening theory: the firm with the lower demand forecast is sold the contract with more coverage and a higher premium.
A firm has capacity and sells over periods at unit price . Its early demand forecast , with , is its private type, high with probability . A forecast update , with , probability of and mean zero, arrives before selling starts. Demand in period is with i.i.d. logistic shocks of mean and scale . Expected sales from a capacity are .
In period a disruption occurs with probability and wipes out capacity. The firm then chooses a recovery effort at cost and sells from capacity for the remaining periods. It also pays a penalty per unit of the net disruption loss.
An insurance contract has premium and coverage percentage . From period on, the insurer reimburses the fraction of the expected revenue loss . Given the contract, the firm chooses the effort that maximizes its profit under disruption, and denotes its expected profit with insurance when . Without insurance the effort is and the expected profit is .
The insurer offers a menu , . It maximizes expected premiums minus expected claims, , subject to four constraints:
This is program (5.1).
Under the paper's standing conditions,
program (5.1) has an optimal menu, and every optimal menu satisfies
The goal asserts only the order of the two contracts, not their values: the optimal coverages have no closed form.
In the classical screening model (Mussa–Rosen, Maskin–Riley), the type with the higher valuation receives the higher quality, and the lower type's participation constraint binds. Here the order is reversed. The high-demand firm restores more capacity on its own and is more often capacity-bound, so a unit of coverage is worth less to it than to the low-demand firm. Proposition 4 turns this into an operational recommendation: offer the low-demand firm the richer and dearer policy. The reduction of (5.1) to two binding constraints, and the resulting first-order conditions, support the paper's comparative statics (Table 1) and its capacity-investment results (Propositions 5–6).
The results are proved in the paper by calculus on explicit closed forms. None of them has been machine-checked, and the platform has no model of BI insurance, no logistic demand law and no two-type insurance-screening program. A complete development checks every step of a chain that mixes an expectation, an envelope argument, a reverse single crossing and a constrained optimization. It also produces reusable pieces: logistic expected sales, and a template for two-type screening problems in which the binding constraints are derived rather than assumed.
Each analytic step is elementary on its own; the difficulty is the length of the chain and the places where the obvious argument does not apply.
All objects live in the namespace BIInsurance.Screening:
Logistic: the logistic density and expected sales as a Lebesgue integral;Model: the parameters, the standing assumptions, the firm's profits, the efforts and , program (5.1), , , , condition (5.5) and the left sides of (5.6)–(5.7).The formalization commits to these conventions:
A trivializing encoding is ruled out. The optimal contract is a maximizer of (5.1) with all four constraints, never the closed form of Proposition 3, and never a maximizer of the reduced objective . Expected sales are an integral, not their closed form.
The development needs:
The logistic expected-sales lemma and the redundancy argument for two-type screening are reusable beyond this mission. Contributions to any milestone are welcome.
Season-long sports competitions (the biathlon World Cup, Formula One, the motorcycle Grand Prix, golf's FedEx Cup) rank athletes by adding up points awarded for the positions they take in individual races. The same mechanism, under the name positional scoring rule, is one of the oldest objects of social choice theory: Borda's rule, plurality and antiplurality are all scoring rules, and Young (1975) characterised the class axiomatically.
Kondratev, Ianovski and Nesterov start from a concrete anomaly. In the 2013/14 IBU Biathlon World Cup (Women's Individual), Soukalová won both races; under the official points table, disqualifying her would have changed the order of the athletes behind her, with Hildebrand overtaking Skardino for third. An athlete who finished first everywhere, or last everywhere, carries no information about how the others compare, so a ranking method that reorders the others when such an athlete is dropped is open to manipulation and to disputes after disqualifications. The paper asks which scoring rules are immune to this, and its answer is a one-parameter family that contains Borda's rule and has the convex point tables used in practice as other members.
The two axioms belong to a long line of independence conditions in social choice (independence of clones, of Pareto-dominated alternatives, of irrelevant alternatives). Fishburn (1981) showed that two non-equivalent score vectors always rank some profile differently, which is the classical fact behind the paper's Proposition 4.
Let be the number of potential athletes, finite or . A scoring rule assigns to every number of athletes a vector of real scores , where is awarded for position . A race on a finite set of athletes is a strict ranking of ; a profile is a sequence of races. The total score of athlete is the sum, over all races, of for the position that takes in that race, and the overall ranking is the weak order by total score: higher totals rank higher, equal totals rank equally.
An athlete is a unanimous loser if it is last in every race, and a unanimous winner if it is first in every race. A scoring rule satisfies independence of unanimous losers if, in every profile, a unanimous loser is ranked last overall and removing it from every race (the others keep their positions, and the rule now uses the score vector for athletes) leaves the overall ranking of the remaining athletes unchanged. Independence of unanimous winners is the mirror image: a unanimous winner is ranked first overall, and removing it (every other athlete moves up one place) leaves the ranking of the others unchanged.
Two vectors and are affinely equivalent if for all , for some and some ; affinely equivalent vectors produce the same overall ranking on every profile. For a parameter the geometric scores are
and a geometric scoring rule with parameter is one whose score vector for every is affinely equivalent to . The case is Borda's rule; gives convex point tables that reward winning, concave ones that punish finishing last.
For every scoring rule and every ,
The parameter is one number for the whole rule, not one per . Nothing about the values of the scores beyond their affine class is fixed.
Theorem 6 says that two weak, individually almost costless requirements together cut the infinite-dimensional space of scoring rules down to a single parameter. Each axiom alone is satisfied by any strictly decreasing score table extended by truncation at one end; jointly they force self-similarity of the table. The rest of the paper builds on this family: Theorem 9 characterises Borda's rule within it, Theorem 10 characterises , and §5 compares geometric rules with the scores that are optimal for an organiser who wants to identify the strongest athlete. For practice, the result tells a league that wants its standings to survive disqualifications of dominant or hopeless athletes exactly which point tables it may use.
The result is proved in the paper, partly through Fishburn's (1981) theorem and partly through a constructive argument in Appendix A. No machine-checked version of Theorem 6 or Proposition 4 is known; neither Mathlib nor the platform has positional scoring rules, profiles of races or the weak ranking they induce. A formal proof would add a reusable model of positional voting, a formal version of the fact that non-equivalent score vectors are separated by some profile, and a checked proof of the characterisation for every , including .
The "if" direction is a computation: geometric vectors have geometric prefixes and suffixes with the same , and positive affine maps preserve every comparison of total scores. The difficulty is in the "only if" direction of Proposition 4. Strict monotonicity follows from single-race profiles, but affine equivalence of the vector for athletes with a prefix (or suffix) of the vector for athletes does not: the axioms only speak about rankings, so every failure of affine equivalence must be witnessed by an explicit profile of strict rankings, for arbitrary real scores, in which removing the unanimous losers (or winners) reverses a comparison. Producing such witnesses uniformly is the substantive step, and it is where the published argument leans on an external theorem (Fishburn 1981) or on a dedicated construction.
A second obstacle is uniformity of the parameter when : each with determines its own , and these must agree across all ; for the parameter is not determined at all.
Athletes form an arbitrary finite type α with Fintype.card α ≤ M, where M : ℕ∞ (⊤ encodes ). A race is a bijection α ≃ Fin (Fintype.card α), a profile is Fin n → Race α, and a scoring rule is (m : ℕ) → Fin m → ℝ. Positions are 0-based: Lean's position j is the paper's position , so the paper's exponent is m - 1 - j. The overall ranking is compared as a weak order: "unchanged" means for all remaining athletes . The removed profile is not constructed: the axioms quantify over every profile on {a // a ≠ x} satisfying the removal relation, and such a profile exists and is unique.
Two readings are fixed and disclosed. "Ranked last/first in the overall ranking" is strict (the unanimous loser has a strictly smaller total than every other athlete), as the paper's proof uses it; under a weak reading constant scores would satisfy both axioms and Proposition 4's strict inequalities would fail. Consequently the axioms range over profiles with at least one race: with no races all totals vanish and no athlete is strictly last. The parameter of a geometric scoring rule is : the limits and are multi-round generalised rules (Definition 2), not scoring rules.
The axioms are stated about profiles and the removal of athletes, never about score vectors. A formalization in which independence of unanimous losers is defined as the right-hand side of Proposition 4 would make Proposition 4 true by definition and reduce Theorem 6 to algebra on sequences; that is ruled out.
A complete development needs: sums of scores over races, the existence of removal profiles, explicit strict rankings on Fin m and profiles assembled from them, and the algebra of affine equivalence and geometric sequences. The model is reusable for the paper's later characterisations (Theorems 9–11) and for scoring-rule results in voting theory. Contributions of the "if" directions, of the recurrence, and of the separating-profile lemma as standalone results are welcome.
Online platforms (labor marketplaces, review sites, crowdsourcing services) rely on feedback from their users: did the plumber arrive on time, is this image labelled correctly. The answers cannot be checked against ground truth, so a platform that rewards feedback must reward it by comparing it with other users' answers. This is the problem of peer prediction, or information elicitation without verification. The classical mechanisms of Miller, Resnick and Zeckhauser (2005) and Prelec (2004) make truthful reporting an equilibrium, but they either need the designer to know the joint distribution of the users' observations or ask users for extra reports (predictions of others' answers). Both requirements are unrealistic on a large platform.
Kamble, Shah, Marn, Parekh and Ramchandran propose the square root agreement rule (SRA). It uses only the users' answers, needs no knowledge of the distribution, and works when users perform many statistically similar tasks. A second difficulty of peer prediction is that uninformative coordinated behavior (everyone answers "yes") is often also an equilibrium, sometimes a better-paying one. The paper's main result says that, with many tasks, SRA makes truthful reporting a strict equilibrium whose payoff is within any prescribed of the best symmetric equilibrium.
Timeline. Output agreement and the peer-prediction method (Miller, Resnick, Zeckhauser 2005) require a known prior. The Bayesian truth serum (Prelec 2004) and its robust variants ask for prediction reports. Multi-task mechanisms (Dasgupta and Ghosh 2013; Shnayder, Agarwal, Frongillo and Parkes 2016) estimate the statistics from other tasks and obtain informed truthfulness under correlation assumptions. SRA (arXiv 2015, Management Science 2023) obtains strict truthfulness for every separated model and approximate payoff dominance over symmetric equilibria.
There are evaluation tasks and agents. Agent performs the tasks ; task is performed by the agents , with . Each task concerns an entity whose type lies in a finite set ; types are i.i.d. with law . An agent observes an answer in a finite set , drawn independently from . The pair is the generating model.
A reporting strategy gives, for each observation , a distribution over reported answers. The truthful strategy reports what it observes; a fully informative strategy reports for a fixed permutation of . A profile is symmetric if all agents use the same strategy.
SRA (Mechanism 1). For every task pick two distinct agents , and let
with . On each of her tasks , agent is paid if she and her peer both report , and otherwise. Rare agreements pay more.
A profile is a Bayes–Nash equilibrium if no agent can raise her expected payment by changing her own strategies, and a strict one if every change on her tasks lowers it. With , the Cauchy–Schwarz gap is
and the model is -separated if . The square root agreement measure is , and the uninformativeness of is .
For every , and there is such that for every -separated model, every and every allocation with :
for every symmetric BNE , every permutation and every agent . No constant is hard-coded: is only asserted to exist, uniformly over all models with the same .
Theorem 1 gives a detail-free mechanism: the designer needs neither nor , and the agents need only know that the model is -separated. The guaranteed gap over observation-independent reporting lets a platform pay for effort by scaling . Theorem 2 addresses equilibrium multiplicity, the main criticism of agreement-based mechanisms: no symmetric equilibrium can pay noticeably more than truthful reporting. Proposition 5.1 is a quantitative data-processing inequality for the square root agreement measure, of independent interest.
All statements are proved in the paper (arXiv:1507.07045v5, Appendix A). None has a machine-checked proof. The mission asks for formal proofs of the stated results with uniform in the model; explicit bounds on and alternative arguments for the second claim of Theorem 2 are welcome.
The payments are inverse square roots of empirical frequencies, so their expectations do not follow from the law of large numbers alone: a bound uniform over all -separated models is required, and it must be uniform in the answer . For a general symmetric profile the agreement probability of some answer can be arbitrarily close to , so no uniform concentration bound for holds across all symmetric profiles; the obvious argument "compare the limit payoffs " therefore does not transfer to finite directly. Finally, the expectations are over a product space of types, observations and reports of all agents on all tasks, and the independence structure (payments of never read her own reports) has to be made explicit.
Types, answers, tasks and agents are Fin m, Fin k, Fin N, Fin M; all quantities are real. A strategy is q : Fin k → Fin k → ℝ with q obs ans the probability of reporting ans after observing obs; models and strategies are required to be stochastic. A Setting holds the allocation together with the mechanism's choices (peers and the pairs ), and every theorem quantifies over all legal choices after . Every (task, agent) pair carries an observation and a report; entries of agents not assigned to a task are never read by a payment and marginalize out. The expected payment is the explicit finite sum, over all types, observations and reports, of the product probability times the payment; deviations change only the deviating agent's strategies on her own tasks, and strictness is over deviations that change some strategy on her tasks. "Commonly known" has no formal content beyond computing expectations under the true model. The printed "" is read as ; Theorem 1's second claim assumes . is when , so the separated theorems are vacuous there, as the page's is undefined.
Expected payments are not defined by (31) or by the limit formulas , and never depends on the model, the population or the mechanism's choices: either shortcut would make the targets trivial or strictly weaker.
A complete development needs binomial tail bounds (Hoeffding), moment bounds for inverse square roots of binomials, Cauchy–Schwarz on finite sums and the marginalization of product measures over finite types; the last two are reusable for other multi-task peer-prediction mechanisms. Proofs of any milestone are welcome.
Investors who hold risky assets face losses from occasional jumps in prices. Such jumps are infrequent, so their frequency and size distribution can be harder to estimate than ordinary price fluctuations. Jin, Luo, and Zeng study how a portfolio changes when an investor treats both the arrival rate and the size distribution of jumps as uncertain. Their 2017 working paper combines a jump-diffusion market with an entropy penalty for departures from a reference model. Its main portfolio result separates the exposure to jump risk from a component that depends only on diffusion risk and expected returns.
The practical question is precise: when several stocks share a smaller number of jump types, which combinations of stock holdings carry jump exposure, and how should the investor allocate the remaining risk? A direct optimization in all stock weights obscures this distinction. The paper's Proposition 2 describes optimal holdings through a reduced jump-dependent problem and an explicit formula for the orthogonal component. This mission asks for a machine-checked statement and proof of that result for the pointwise robust objective used in the paper's Hamilton–Jacobi–Bellman calculation.
There are risky assets and jump types. A portfolio records the fraction of wealth invested in each risky asset; the remaining fraction is invested in a bond with rate . The risky assets have expected returns , a nonsingular diffusion matrix , and a full-column-rank jump matrix . Its column scales the effect of jump type on the stock prices. The reference arrival intensity is , and is a probability law for its jump size . The paper requires the jump exposure to lie in for each ; these constraints define an admissible portfolio in the pointwise problem. The market assumptions come from §2 of the working paper, pp. 7–8.
An alternative jump model multiplies by and replaces by , where is positive and integrates to one. Its departure from the reference model is penalized by the generalized relative-entropy integrand . The investor has constant relative risk aversion , with , and ambiguity aversion . The authors derive a pointwise robust generator from their value-function ansatz. It includes the diffusion quadratic, excess expected return, the bond rate, and a genuine infimum over alternative jump models. For jump exposure , the type- inner objective is
This is equation (A.1) of the paper, p. 33, with its term depending only on time removed. The infimum is taken for each jump type over normalized positive density and positive intensity pairs.
Proposition 1 identifies the minimizing alternative model. For , write . Its intensity and density factors are
The target says this pair is admissible and attains the inner minimum. The other milestones cover the orthogonal decomposition, the jump-exposure identity, separation of , and the explicit optimum of the diffusion component. These are the claims used for the portfolio result in Proposition 2 and Appendix A of the paper, pp. 12–15 and 33–34.
Define and . Let be the column space of and decompose into its parts in and its orthogonal complement. The goal characterizes every maximizer of the robust generator over admissible portfolios by
Here is the reduced objective in equation (A.10), including the entropy penalty of the worst-case model. The target is an equivalence between maximizers of the original and reduced problems; it leaves existence of a maximizer as a separate question. The formula for the orthogonal component is fixed, while the jump component is determined by the reduced optimization.
The result identifies which part of the asset allocation depends on jump ambiguity. In the transformed coordinates, the component orthogonal to the jump columns responds to expected excess returns and diffusion risk through . All dependence on the jump-size laws, arrival intensities, and ambiguity aversion is confined to the column-space component. Since has dimension , the jump-dependent problem is effectively smaller when . These conclusions are the content of Proposition 2, rather than a claim that every stochastic portfolio policy has been verified as optimal.
The paper supplies an analytic argument, but the stated formulas are not yet a machine-checked development in this mission. A formal proof would also give reusable statements about an unnormalized entropy-penalized jump measure, the integrability required for its exponential tilt, and the matrix projection used in the decomposition. Those pieces can support later treatments of the paper's comparative statics or related robust-control models. The goal itself is a known result from the working paper, not an open research conjecture.
The inner problem optimizes an intensity and a normalized density together. Their product is an unnormalized positive tilt, so a finite-simplex relative-entropy theorem does not directly express this problem. The displayed exponential tilt may fail to have a finite real integral for a law with sufficiently much mass near jump size , particularly when and the exposure reaches . A formal proof has to keep the real-valued expectations meaningful and show that the proposed model lies in the admissible class.
For the outer problem, the stock weights appear in both the diffusion quadratic and every jump exposure. The useful orthogonal decomposition is in the transformed coordinate , while admissibility is originally written as . Identifying the same feasible exposures after that change of coordinates is necessary for the two optimization problems to have the same maximizers. One cannot infer the portfolio statement merely by maximizing the diffusion quadratic in isolation.
Lean represents vectors as Fin m → ℝ, jump-size laws as probability measures on , and the column space as the span of the columns of . Orthogonality uses the standard real dot product. The model allows and ; neither the standing assumptions nor the target inserts a positive-jump-count or strict-dimension-gap condition. The laws give zero mass outside , so real powers on that complement do not affect the objectives.
The mission starts from the pointwise generator in (A.1), after the authors' ansatz . It does not formalize the price SDE, filtration, stochastic integral, or a verification theorem for the full dynamic control problem. The term involving is omitted because it is independent of the choices in this generator problem. The generator keeps the genuine inner infimum; replacing it with Proposition 1's closed form would remove the inner optimization that the mission is meant to formalize.
The source presupposes finiteness of the expectation defining . The development states only the needed integrability of and of its product with the CRRA jump increment for every . It also requires the combined inner-objective integrand to be integrable for an admissible alternative pair. Excluded nonintegrable pairs have extended value under the integrable lower bound and cannot improve the infimum. Positivity of , , and , together with , makes the paper's divisions and preference parameters explicit. Definitions of the admissible pair, inner objective, projection, and reduced objective are intended for reuse; contributions toward the five source milestones and the goal are welcome.
The printed objective (17) omits the entropy term retained by the proof's (A.10). Since the worst-case model varies with , the two objectives can have different maximizers. The formal target uses (A.10), which matches the robust generator. The goal's Formalization Note records this discrepancy and the added integrability hypothesis.