Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A prophet inequality compares the value obtained by an online decision maker with the largest value in a sequence that could be chosen by someone who sees the entire sequence. The online decision maker observes values one at a time and must decide whether to accept the current value before seeing future values. When the common distribution of the values is known, that distribution can inform the stopping rule. This mission concerns the case in which the distribution is unknown and the rule receives no advance samples. The restriction is operational: the same rule must work across every possible common distribution of the observations. Correa, Dütting, Fischer and Schewior show that the familiar success scale of the classical secretary problem is the sharp asymptotic limit for this setting.
The result matters to online selection when historical observations are unavailable. It says that the loss from not knowing the distribution cannot be removed merely by choosing a more elaborate rule based on the values seen so far. It identifies an asymptotic ceiling that applies to every randomized stopping rule, including rules that react to exact numerical values rather than only to their ranks. The paper also studies what changes when samples are supplied; this mission isolates its zero-sample upper bound. The source paper states the result as Theorem 2 on page 6 of arXiv:1811.06114v2.
Fix a horizon . Independent observations have the same unknown law on the nonnegative real numbers. A stopping rule first receives independent samples from that law and then sees the observations in order. At time , the rule returns a number . This is its conditional probability of stopping on , given the samples, the observed prefix , and the fact that it has not already stopped. A rule with has no preliminary samples. Its behavior may depend on every observed value and may be randomized.
For fixed samples and observed values , the conditional probability that the rule stops at is
If it never stops, its payoff is . The benchmark is the prophet's maximum . A rule has approximation guarantee when for every allowed law . The paper uses this model in §2, page 5, and develops the zero-sample upper bound in §3.2, pages 6–8. Correa et al.
Two restrictions of a rule appear in the supporting results. A rule is order oblivious when rearranging distinct, nonnegative values seen before the current observation does not change its current stopping probability. A rule is value oblivious on a set when, on histories of distinct values from whose current value exceeds the earlier values, its stopping probability at time lies in for some . The depend on the time, while the interval works for every qualifying history in . These are Definitions 1 and 2 of the paper. Correa et al.
The central target is the paper's Theorem 2. For every tolerance , a single threshold works for all sufficiently long horizons and all zero-sample rules:
The adversarial law is chosen after the rule ; the threshold depends only on . The positive benchmark makes the ratio meaningful. The law in the formal target has finite support, as does the law constructed in the paper's proof.
The milestones follow the paper's stated results and displayed bounds. Lemma 2 supplies an order-oblivious rule with the same guarantee; Lemma 3 is the infinite Ramsey statement used for an infinite monochromatic set; and Lemma 1 supplies an value-oblivious rule on an infinite set. Equation (1) bounds the expected maximum for the paper's hard distribution. The pointwise display before equation (5) bounds the effect of replacing an approximately value-oblivious rule by a record rule. Equation (4) gives the asymptotic secretary upper bound for that record rule. In the formal statements, the terms in (1) and (4) have explicit finite-horizon or meanings. Correa et al., pp. 6–10
The theorem establishes a ceiling on the worst-case approximation ratio of any zero-sample rule. Its quantifier order matters: a rule may perform well on particular distributions, yet no single rule can exceed uniformly over all unknown distributions for large . Together with the paper's lower bound in Theorem 1, it identifies the sharp asymptotic guarantee without samples. It also gives a baseline against which the paper measures the value of additional samples. Correa et al., Theorems 1–2
The mathematical result is proved in the source paper; the work here is to give a machine-checkable statement and a decomposition that can support a Lean proof. The reusable pieces include a finite-law stopping model, exact conditional stopping probabilities, order and value obliviousness, a uniform-permutation success probability, and an infinite Ramsey statement. The theorem statements in this proposal remain open proof goals. Their compilation checks the representation and syntax, not their truth; solvers must still provide proofs.
The stopping rule class is large. Each can use the exact numerical values of all observations seen so far, and those values range over a continuum. The standard secretary bound concerns decisions based on relative ranks, so it does not immediately bound a value-dependent rule. The upper bound must apply to every such rule while allowing the adversarial distribution to depend on it. A finite hard distribution also produces repeated observations with positive probability, whereas the rank comparison that motivates the secretary bound is simplest on distinct observations. The milestones expose both issues as precise statements without building them into the goal as assumptions. Correa et al., §3.2–3.3
Lean represents values by real numbers and laws by a finite support in with nonnegative masses summing to one. Expectations are finite sums over independent product weights. This finite-law class strengthens the existential law in Theorem 2 and restricts the distribution-uniform guarantees in Lemmas 1 and 2; the paper's upper-bound construction has finite support. The rules themselves are arbitrary real-valued functions on real sample and observation vectors, with outputs in . They are not limited to deterministic, threshold, rank-based, or measurable rules. Indices start at zero in Lean, so Lean index is the paper's time . Failure to stop has payoff zero.
The positive-benchmark clause rules out the point mass at zero, which would satisfy the printed existential inequality as for every rule and make the target empty of content. For the same reason, the formalization uses the actual expectation of the maximum and the actual expectation selected by the rule, rather than stipulating a closed-form success bound. A set may contain zero in Lean, though the paper denotes positive integers by ; infinitude is unchanged by that one extra point. The paper's Definition 2 prints where its quantified time is ; the formalization uses . The hard instance and record rule are defined from their parameters, not supplied as unrelated variables. The convention for a zero-length maximum is Lean's real supremum default, but the hard-instance bound explicitly requires .
A complete development can use Mathlib's finite sums, finite products, permutations, real exponential, and finite-set machinery. The stochastic model and its obliviousness predicates can be reused for sample-complexity variants; the Ramsey theorem is useful independently. Contributions proving the listed milestones, strengthening the finite-law model to broader distributions, or connecting the record-rule bound to an existing secretary formalization are within scope.
A correlated equilibrium (Aumann, 1974) is a profile of strategies chosen by a mediator: the mediator draws a joint recommendation from a known distribution, tells each player only their own component, and no player can lower their expected cost by systematically deviating from what they are told. Correlated equilibria contain the Nash equilibria, are computable by linear programming in finite games, and model situations with a coordinating device such as a traffic authority or a market designer.
Mean field games (Lasry–Lions, Huang–Malhamé–Caines, 2006) describe Nash equilibria of games with a large number of symmetric players who interact only through the empirical distribution of their states. The limit model replaces the players by one representative player facing a flow of distributions. Campi and Fischer (arXiv:2004.06185) ask what the corresponding limit object is for correlated equilibria. Their answer is the correlated mean field game solution: a joint law of a recommendation and a random flow of measures, which, unlike a Nash mean field equilibrium, need not be deterministic. They prove that this notion is the right one in both directions: limits of -player correlated equilibria are correlated solutions (Theorem 6.1), and every correlated solution is approximated by -player approximate correlated equilibria (Theorem 7.1). This mission targets Theorem 6.1.
Fix a horizon , nonempty finite sets (states) and (actions), and the noise space with the uniform law . is the simplex of probability vectors on with . The model data are a system function , a running cost and a terminal cost , with measurable and bounded and measurable.
A restricted strategy is a map ; their finite set is . A strategy modification is any map .
The -player game. Given an initial law on and a correlated profile , the mediator draws , independently of the initial states and of i.i.d. noises . Player moves by
except that a deviating player uses instead of . Its cost is the expected sum of running costs plus terminal cost. is an -correlated equilibrium if for all and , and symmetric if it is invariant under permutations of the players.
The mean field game. A correlated flow is . The representative player starts from , receives jointly with a random flow , , independent of and of the noises, and moves by with cost . is a correlated solution with initial distribution (Definition 4.1) if
Assume (A1) for a measurable with as , and is -a.e. continuous for every probability on ; (A2) continuous; (A3) is a symmetric -correlated equilibrium with initial law ; (A4) ; (A5) with . Let
computed with . Then
The milestones follow the proof: the coupling bound (2.1); the appendix lemmas on weak convergence (A.1, A.2); the coupling estimates (6.3) and (6.2) and the independence of Step Three; optimality of every limit point; the conditional-law lemmas (A.5, A.4); the pre-limit consistency identity of Step Four; Lemma A.3; consistency of every limit point.
Theorem 6.1 identifies the limit model of large symmetric games played with a mediator. It shows that correlation does not disappear in the limit: the flow of measures recommended by the mediator may remain random, and the limit object must record its joint law with the recommendation. Together with Theorem 7.1 it makes correlated mean field game solutions the exact counterpart of -player correlated equilibria, as mean field equilibria are of Nash equilibria. The example of Section 5 of the paper exhibits a correlated solution with a non-deterministic flow that is not a mixture of deterministic-flow solutions.
The result is proved in the paper; to our knowledge no part of it, nor any correlated-equilibrium mean field result, has been formalized. The mission produces a machine-checked model of discrete-time finite-state mean field games with a mediator, and general-purpose lemmas absent from Mathlib: a mapping theorem for almost everywhere continuous maps that identifies limits of relations , converging together on varying probability spaces, limits of regular conditional distributions, and the conditional law of an exchangeable coordinate given the empirical measure.
Compactness is immediate because all spaces are compact. The content is in identifying the limit. Two obvious steps fail. First, the system function is discontinuous (as in Remark 6.1), so the dynamics do not pass to the limit by the continuous mapping theorem; only almost-everywhere continuity with respect to measures of the form is available. Second, a unilateral deviation by player 1 changes the empirical measures seen by all other players, and through them the whole flow, so it is not clear that the limit flow under a deviation is the limit flow without it. Third, conditional laws are not continuous under convergence in distribution, yet consistency, a statement about the conditional law of the state given the whole flow, must survive the limit.
The Lean development lives in the namespace SimpleCorrMFG.Conv. is stdSimplex ℝ X with its subspace topology and Borel σ-algebra; flows are Fin (T+1) → P(X); restricted strategies are Fin T → X → Γ; times of actions and noises are Fin T (the noise has index ); players are Fin N and the paper's player 1 is index 0; is volume on unitInterval. Probability measures on are Mathlib's ProbabilityMeasure with the topology of weak convergence, and a limit point is the limit of a subsequence with strictly increasing indices.
The paper defines costs and through "any realization" and notes that they do not depend on the choice. The formalization uses the canonical realization: the product law of initial states, recommendations (or the correlated flow) and noises, with the states computed by the recursion. The consistency condition is stated as for every , and Borel , which is the definition of a regular conditional distribution given the whole flow. (A3) is required for , where the -player game is defined.
A formalization in which the flow is conditioned only up to time , in which the costs are integrals of possibly non-integrable functions, or in which "limit point" refers to a topology other than weak convergence would prove a different and weaker statement and is excluded. The standing assumptions that is measurable and are bounded and measurable are carried explicitly, so that no expected cost or law is a junk value.
Contributions are welcome on each milestone. The appendix lemmas are independent of the game and reusable. The written proof of (6.2) uses ; since (A1) does not require , this step needs the observation that the indicator in (A1) vanishes when the two measures coincide.
Supermarkets run temporary price promotions on a large share of their assortment, and the choice of which item to discount, by how much and in which week is a recurring planning decision for category managers. Promotions on one item change the sales of the others: a discount on one brand of coffee draws customers away from a competing brand (substitution), while a discount on shampoo can raise the sales of conditioner (complementarity). Promotions also have effects over time, because customers who stockpile during a promotion buy less afterwards.
M. C. Cohen, J. J. Kalas and G. Perakis (SSRN 3061451; Management Science, 2021, doi:10.1287/mnsc.2020.3641) formulate the multi-item promotion problem as a nonlinear integer program and approximate it by a hierarchy of linear integer programs , which add up the profit contributions of promoting up to items together. Their single-item predecessor, Cohen, Leung, Panchamgam, Perakis and Smith (Operations Research, 2017), corresponds to . The main structural result of the multi-item paper, its Theorem 1, says that under a common separability assumption on demand the hierarchy collapses at level two.
There are items and a selling season of periods. The retailer has enough inventory to meet demand throughout the season, as assumed in §2.1, so inventory does not enter the model. Item has a price ladder , where is the regular price, common to all items, and the other points are promotion prices. A plan chooses a level for every item and period; the price of item at period is . Item has unit costs and a memory , and its demand at period is a function
of its own current and past prices and of the other items' current prices (Assumption 1: cross past prices do not enter). The total profit of a plan is
and the problem (Multi-POP) maximizes it over plans satisfying the business rules: at most promotions of item , at most one promotion of item in any consecutive periods, at most promotions in total and at most in period .
A pattern assigns a level to each item; its support is the set of promoted items. The pure promotion vector uses at period and the regular price everywhere else, and is the all-regular plan. The coefficient of at is the inclusion–exclusion sum
where keeps the levels of on and is regular off . With one promoted item this is , equation (5); with two it is equation (6). The App(κ) objective of a plan is
which is equation (4) for , and maximizes it over the same feasible set.
Assume the cross-item effects are additively separable,
for arbitrary functions and . Then for every and all business-rule data,
This is the chain of the paper.
The size of grows like in the number of pairwise, triple and higher variables, and has a variable for every subset of items. Theorem 1 shows that under (8) nothing is gained beyond , an integer program with a quadratic number of variables. Equation (8) covers the demand models used in practice that the paper cites, the log-linear model with linear cross terms and the linear cross-elasticities model. The rest of the paper's solution approach works with : integrality of its LP relaxation for substitutable items (Theorem 2), a rounding scheme and a parametric bound (§3); Theorem 1 is what makes the complete cross-item model under (8).
The result is proved in the paper; its appendix carries out the order-three case explicitly and the induction step in outline, with "the details … omitted for conciseness". No machine-checked proof is known to exist. A formal proof removes the omitted cancellations and isolates the combinatorial core (milestone 5), which is a fact about pseudo-Boolean functions useful beyond promotions.
The coefficients are signed sums of total profits over all items and periods, and each profit is a product of a price margin and a demand that depends on a window of past prices. The obvious idea, expanding the products directly, gives an unmanageable number of terms. Every contribution involving three or more promoted items has to cancel, including the contributions at later periods, which see a promotion only through the memory window, and the paper omits these cancellations in the general induction step. Without (8) the claim fails: the paper notes that for demand models violating it is not necessarily equal to , and a demand with a three-way cross term already has nonzero order-three coefficients.
Lean namespace PromoMulti.PairwiseExact. Items are Fin N and periods Fin T, 0-based (period of the paper is index ); prices, costs and profits are real. A plan is a function assigning a level Fin (K i + 1) to each item and period, level 0 being the regular price ; this is the binary encoding with . Prices before the first period are (the appendix evaluates ); Theorem 1 holds for any fixed history. The paper's pairwise variables are separate binaries tied by the consistency constraints (7); for integral plans (7) forces them to be products, and the App(κ) objective uses that product directly. The paper writes out only for ; for the formalization uses the inclusion–exclusion extension of (4) with the general coefficient of p. 38. The demand receives the whole current price vector; (8) reads only the coordinates . The ladder order is not imposed, nor any monotonicity, linearity or sign of and : Theorem 1 uses none. The business rules are those of (Multi-POP); the inter-item rules 2, 3 and 5 of §2.2 are not part of it.
The coefficients are defined by the closed alternating sum and the App(κ) objective sums every pattern with ; a formalization that defines App(κ) through pairs only, defines higher coefficients as zero, or defines coefficients by the recursion (16) makes the goal trivial and is ruled out. The goal does not claim that App(2) solves (Multi-POP), which is false when past prices matter.
A complete development needs finite inclusion–exclusion over Finset.powerset, the cancellation lemma of milestone 5 (reusable for any pseudo-Boolean or multi-level function that is a sum of low-arity terms), and the bookkeeping of which plan coordinates each item–period profit reads. Contributions of proofs of any milestone, of milestone 5 in greater generality, and of alternative arguments are welcome.
A discrete moment problem asks for the largest expected payoff compatible with prescribed moments of an unknown probability distribution. A decision maker may know the first few moments of demand or loss while the full distribution remains uncertain. The optimization then asks which compatible distribution makes a chosen payoff largest. Chen, He, Jiang, Ryan, and Zhang study what happens when the distribution must also obey a shape constraint. Their preprint treats discrete log-concavity and increasing failure rate as two such constraints. This mission concerns the log-concave case.
The moment constraints alone define a convex polytope of probability vectors. Requiring log-concavity changes its geometry: the feasible region is generally nonconvex. This matters because familiar descriptions of extreme points of a moment polytope no longer describe the candidate worst-case distributions. The paper's Theorem 4.1 gives a finite structural description of the optimal extreme points despite that change. Its proof uses a general result about optimization over reverse convex constraints, Theorem 3.6, which is also included as a milestone. Both statements and their setting are taken from arXiv:1708.02079v1, pages 5–15.
Fix the finite sample space . A distribution is a vector of nonnegative masses. For each integer from through , its prescribed moment is , so . The convention makes the masses sum to one. Given payoff coefficients , the discrete moment problem maximizes over the distributions satisfying these equations.
A distribution is discrete log-concave when its positive masses form one consecutive integer interval and at every interior index . In the paper's formulation (DMP-LC), the entries on are strictly positive and the other entries are zero; the feasible region is the union over all such supports. Its alternative formulation (DMP-LC′) replaces the chosen support with nonnegativity and a family of longer-range inequalities. Proposition 2.4 says that the two feasible regions coincide. The extreme points in this mission are those of the entire feasible region, including every possible support.
The paper also considers a general reverse convex program in : minimize a function subject to , , and for . Here the reverse convex condition is relative to the nonnegative orthant: the forbidden set is convex. Under the paper's continuity, quasiconcavity, differentiability, rank, and compactness assumptions, Theorem 3.6 counts the inequalities that are tight at an optimal extreme point.
The goal is the corrected mathematical content of Theorem 4.1. If (DMP-LC) is feasible, an optimal extreme point exists. Every optimal extreme point has support and can be covered by at most geometric pieces. In symbols, there are weakly increasing breakpoints and positive parameters such that
The milestone path includes the equivalence of the two feasible formulations, compact-set extreme-point results, convexity of the forbidden power regions, the reverse convex tight-constraint count, and the two structural steps in the proof of Theorem 4.1. Theorem 3.6 asserts, in particular, that at each optimal extreme point of its -row program,
The conclusion replaces an unrestricted search over feasible probability vectors with a characterization of the candidates that can be optimal extreme points. It also identifies how the number of prescribed nonzero-order moments controls the number of geometric pieces. The count in Theorem 3.6 applies to the larger class of reverse convex programs described above; it is useful independently of this distributional example. These are results proved in the cited preprint, rather than open conjectures.
The formalization target is to give the known statements a machine-checked proof in Lean. The proposed items are statements with proof placeholders; they do not yet assert that a machine-checked proof exists. The finite moment notation, the log-concave feasible region, and the reverse convex feasible region are separate definition files so the general finite-dimensional objects can be reused. Contributions to the milestone theorems, the proof of the goal, and supporting lemmas are all in scope.
The log-concavity inequalities do not make the feasible region convex, so the standard convex-polytope description of optimal extreme points does not directly apply. In addition, the chosen support may move: a vector that is extreme within one fixed-support slice need not be extreme in the full union. Existence of an optimal solution alone gives no bound on the number of geometric pieces. The challenge is to obtain enough tight constraints at every optimal extreme point, then relate those equalities to its coordinates without assuming the desired shape in the definition of feasibility.
Lean represents as Fin n → ℝ; a Fin n index with value represents the paper's position . The helper ext supplies the paper's one-based coordinates and returns zero outside . Moments use the exact weights . All feasible sets use real vectors, with nonnegativity or strict positivity stated where the paper requires it. The (DMP-LC) region is the union over supports satisfying (2b)–(2e); the goal uses extreme points of that whole set and a maximization objective. The reverse convex milestones use minimization, full row rank, and convexity of the forbidden sets inside the nonnegative orthant. Compactness and nonemptiness are explicit assumptions where the source invokes them.
Two corrections to the printed Theorem 4.1 are necessary. First, its bound is false. With , , , , and payoff , the unique maximizing extreme point is approximately , whose geometric ratio is about . The formal statement requires . Second, the printed strict chain of breakpoints fails for short supports: with , , and moments , the only feasible distribution is the point mass at . Weak breakpoints express the paper's “at most pieces” conclusion. They allow degenerate pieces; is retained and forces a point mass. The proof's closed-range wording for tight equalities is read on interior indices, and the tight count uses moment rows. These choices and the paper's typographical slips are recorded with the items.
The feasible region does not encode geometric sequences, and extremeness is never taken only within one support or within its convex hull. The development needs Mathlib's finite sums, finite-dimensional topology, convex hulls, extreme points, matrix rank, continuity, quasiconcavity, and differentiation. The finite discrete moment definition and reverse convex feasible-set definition are intended for reuse beyond this paper.
A minimum support price (MSP) guarantees farmers a unit sale price at least as high as an announced floor. It can protect farmers when the market price is low, but the same guarantee can require a government payment and can change how much crop is produced. Policy evaluation therefore needs to account for farmers, consumers, and public expenditure together. Chintapalli and Tang examine these effects when the market price is uncertain and farmers decide whether to sow before that price is known (SSRN manuscript, §§3–4). This mission takes the paper's market uncertainty model and its joint assessment of farmer net benefit and net social value. The result is already proved in the paper; the work here is to formalize its definitions and claims in Lean.
The farmer population has total mass one. Each farmer can produce one unit and has a cultivation cost uniformly distributed on . A farmer is small enough to take the eventual market price as given. At total production , the inverse demand price is , where is market potential and the shock is uniform on . The government announces an MSP before sowing. A participating farmer receives the effective price : the market price when it exceeds the guarantee and the guaranteed price otherwise (manuscript, pp. 6–8).
Farmers are risk averse according to the paper's value-at-risk participation rule. A farmer with cost finds the crop lucrative when the probability that effective price is no greater than cost is at most :
The equilibrium quantity equals the mass of farmers whose costs make cultivation lucrative when aggregate production is . The model does not prescribe this quantity in advance. Write for production without an effective guarantee and for the quantity identified by Theorem 1. The paper considers admissible MSPs : the guarantee lies between the lowest and highest possible market price at its equilibrium quantity, or (manuscript, eqs. (7) and (9), pp. 8–10).
Let be aggregate expected farmer surplus, computed from the effective sale price less each participating farmer's cost. Let be government expenditure on the positive difference between the guarantee and the market price. Let be consumer surplus, the area between inverse demand and the market price over units consumed. The paper evaluates a guarantee through net benefit and net social value (manuscript, pp. 7 and 11–12).
The milestone path first identifies individual participation and the unique equilibrium quantity, then establishes the paper's explicit formulas for , , and . Two identities in the proof of Proposition 1 summarize the resulting policy values for admissible :
The goal is Proposition 1 in full. When and , it states if and only if . It identifies an admissible maximizer of net benefit at and says net benefit is independent of in each of the regions and . It also states for every admissible and identifies an admissible maximizer at (manuscript, Proposition 1, p. 13). A maximizer is a price attaining the largest value; the proposition does not require uniqueness.
The two metrics answer different policy questions. Net benefit asks whether farmers' aggregate surplus exceeds the public cost of the support guarantee. Net social value adds consumer surplus to that accounting. Proposition 1 identifies which MSP maximizes each measure and states that the broader value remains positive throughout the admissible range. These conclusions are specific to the paper's linear inverse demand, continuous uniform cost and price shock, and risk-based sowing rule; they do not claim the same price choices for other agricultural markets (manuscript, §4.3).
Formalizing the result requires a machine-checkable account of the continuum of farmer costs, the uniformly distributed market shock, a fixed-point equilibrium, and integrals defining all three welfare components. The manuscript gives a proof; the Lean theorem files in this proposal state open proof obligations. A completed development would make the integral formulas, equilibrium characterization, and optimality claims reusable for related support-price models, while exposing exactly which modeling assumptions they need.
The farmer's sowing decision depends on the distribution of the effective price, and the effective price changes at the support threshold. At the same time, the market price depends on the aggregate number of farmers who sow. Directly inserting a guessed production quantity would skip the equilibrium question. The welfare formulas add a second layer: they must integrate the same participation rule and price guarantee, then compare policies only within the admissible set. Theorem 1's printed farmer-level biconditional also has a boundary cost that requires care, even though a single cost has zero mass under the uniform distribution (manuscript, Theorem 1 and its proof, pp. 10 and 37).
Lean represents prices, costs, probabilities, and welfare values in . The cost distribution is Lebesgue measure on ; the shock law is normalized Lebesgue measure on . The standing assumptions are , , , and . Positivity of is explicit in Lean because the uniform law and its expectation divide by . The paper treats it implicitly when it specifies a nondegenerate uniform shock. The lucrative rule uses weak inequalities on both the loss event and the probability bound, following the numbered model equations (manuscript, eqs. (1), (5), and (6)).
An MSP's admissibility is evaluated at an equilibrium quantity, not at an arbitrary guessed quantity. Equilibrium is defined as a fixed point of the mass of lucrative farmers; it is not defined to equal . Farmer surplus, expenditure, and consumer surplus are integrals, not the later closed forms. This prevents the goal from becoming a substitution exercise. Theorem 1 is restricted to admissible MSP values; its premise evaluates admissibility at the proposed equilibrium , which the theorem then identifies as the actual equilibrium. Its farmer-level clause excludes the one threshold cost at which the manuscript's biconditional is inaccurate. Aggregate equilibrium remains the same. The mission covers the single-crop market uncertainty model in §§3–4; the paper's yield uncertainty and two-crop extensions are separate results. Contributions to the fixed-point, measure, integration, and policy-optimization steps are all within scope.
Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation , TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.
The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach , nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.
Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.
A finite Markov reward process consists of a finite state space , a stochastic matrix with the probability of moving from to , transition rewards with , and a discount factor . The chain has a stationary distribution (), and the observed trajectory starts from , so it is a stationary sequence.
Each state carries a feature vector with . The steady-state feature covariance has full rank, and is its minimum eigenvalue. Value functions are compared in the steady-state seminorm .
At a transition the TD direction is . Its steady-state mean is , and the TD fixed point is the vector with . Projected TD(0) with radius starts from and iterates
where is the Euclidean projection onto the ball of radius . The averaged iterate is .
The chain mixes uniformly (Assumption 1): there are and with for all . The mixing time is . Write .
All three bounds are stated together, with the expectation over the stationary trajectory:
(a) for and ,
(b) for a constant ,
(c) for and ,
The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence (Lemma 1); the descent inequality (Lemma 3); the gradient bound (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound (Lemma 9); boundedness and Lipschitz continuity of the gradient error (Lemma 10); and the bias bound (Lemma 11).
Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning , part (b) shows exponential convergence to a neighbourhood whose radius scales with , and part (c) gives an rate. Compared with the i.i.d. bounds, the only change is a factor of order : roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.
The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.
The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses . Under Markov sampling this fails: is a function of and is correlated with the observation at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in steps, which is where the projection and the uniform gradient bound enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant (, ) tracked exactly.
Fintype. The expectation over the stationary trajectory is the finite sum , the exact law of for a finite chain started from , so no measure theory is used. The paper itself works with a finite (p. 5).EuclideanSpace ℝ (Fin d) with , so every is Euclidean.sInf over and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.Electricity end-users increasingly generate their own power with rooftop solar panels and small wind turbines. This distributed renewable energy (DRE) is usually sold under net metering: a customer who produces less than it consumes buys the shortfall from its utility at the retail price, and a customer who produces more sells the surplus back to the utility. The buy-back rate is either the retail price (the retail-based rule) or the wholesale price (the market-based rule); both are in force in different U.S. states.
The common view in the industry is that net-metered DRE hurts utilities twice: it shrinks their retail sales, and it obliges them to buy surplus energy at a rate above their procurement cost. Utilities have lobbied against net metering on this basis. Sunar and Swaminathan (SSRN 3257925; Management Science, 2021, doi:10.1287/mnsc.2020.3854) point out that this view ignores the wholesale market. A utility that meets part of its demand from a wholesale market, where generators compete in supply functions as in Klemperer and Meyer (1989) and Green and Newbery (1992), pays a market-clearing price that falls when DRE lowers the net wholesale demand. Their main result, Theorem 1, gives an exact condition under which net-metered DRE raises a utility's expected profit.
Wholesale market. There are generators. Generator submits a supply function and producing costs it , with . For a realized net wholesale demand , the market-clearing price solves . A profile is a supply function equilibrium (SFE, Definition 1) if no generator can raise its ex-post profit, for any realization of the demand, by submitting a different supply function. The symmetric profile with
is the equilibrium the paper works in; its clearing price is with .
Utilities. Utility sells at the retail price . Its net-metered customers demand and generate ; its total end-customer demand is with . It owns existing resources covering up to units at unit cost , with . and are bounded random variables, is the rest of the wholesale demand, and the net wholesale demand is
Utility 's expected profit under the rule is equation (6): retail revenue, minus the buy-back cost of the surplus at , minus the cost of buying the residual demand on the wholesale market, plus the revenue from selling any excess there. is the same profit when nobody generates ( everywhere, Definition 2). The constants , are the expected net demands of the rest of the market with and without DRE, and , are the explicit ratios (EC.16), (EC.17).
For there is a threshold such that for every ,
with the expression (EC.16)/(EC.17), which does not depend on .
Theorem 1 is the paper's headline: it reverses the industry's belief under stated conditions. It says that a market-reliant utility (small ) facing a wholesale price that is sensitive to demand (large ) earns strictly more with net-metered DRE than without it, and that this happens only under these two conditions. Corollary 1 adds that the gain from DRE is larger the more the utility relies on the market. The paper uses these results to argue that lobbying against net metering can hurt the lobbying utility.
The result has been published but not machine-checked. A formalization pins down exactly what Theorem 1 needs, and the planning analysis already found that the printed argument leaves gaps. Lemma EC.1 is false when the denominator of is not positive; a two-point counterexample is recorded in the item notes. The proof also uses an independence of region from the rest of the market that the paper does not state. Theorem 1 itself survives both gaps because its threshold is existential. A Lean proof would settle this, and would also give a reusable formal account of a supply function equilibrium with quadratic costs.
The obvious argument says that DRE lowers retail revenue and raises buy-back costs, so the utility must lose. It fails because the wholesale price is endogenous: DRE lowers and hence , which helps a utility that buys on the market and hurts one that sells. Three steps carry the weight. The first is a measure-theoretic reduction of (6), with its indicator terms, to closed forms; it needs the independence of region and the integrability of every term. The second is the sign analysis of a difference that is affine in , including the degenerate cases where 's denominator is or the slope vanishes. The third is the ex-post optimality of the symmetric supply function against every deviation , not only against differentiable or monotone ones.
Everything lives in the namespace NetMeterDRE.Profit. Two definition files: SFE (profit (EC.2), clearing (1), Definition 1, , ) and Model (utility data, standing assumptions, (5), the integrand of (6), , , , , , ). All quantities are real. Utilities are indexed by a finite type and generators by Fin N. Random primitives are measurable functions on a probability space and are almost surely bounded, so every expectation is of an integrable function. is . The wholesale price in every theorem is a function that clears the market of the symmetric profile at every demand; it is neither a free differentiable function nor a closed form.
Conventions committed to:
The goal cannot be trivialized by the formalization. is pinned to its explicit formula rather than existential, is chosen before , and is defined by (6), not by the closed forms, so milestones 3–4 are not definitional. Contributions are welcome on any milestone. Milestones 1–2 are self-contained algebra and analysis. Milestones 3–4 are the measure-theoretic core.
An innovation contest asks people outside a firm to submit solutions and promises payments according to the rank of their submissions. The firm would like a strong best submission, but a potential solver must decide whether entering is worth a fixed cost before knowing who else will enter. Paying only the winner can encourage effort while leaving the contest with no entries. Paying several ranks can make entry more attractive while spreading the reward budget across more people. Stouras, Hutchison-Krupat and Chao study that tradeoff in a model where the firm values the best solution and pays a penalty if the contest receives none (accepted SSRN version, Sections 3–5.1).
The question is operational: given a budget and entry cost, how many ranks should receive a positive reward? The paper's Theorem 2 describes regimes in which a winner-take-all allocation is optimal and regimes in which the optimum pays several ranks. Its supporting results connect the equilibrium entry threshold to the number of entrants and identify allocations that maximize participation (Theorems 1–2, pp. 10–12).
There are potential solvers, with . Their abilities are independent draws from a common distribution on with CDF and continuous, strictly positive density . A solver who exerts effort produces performance when their ability is . The marginal cost of effort is one. Entry also costs , so performance costs for a solver with (model setup, pp. 6–7).
An allocation lists rank rewards with , where is the firm's budget. Rank one is the best submission. A rank beyond the number of entrants receives no payment. The number of rewards is the count of strictly positive entries in that list, including tied positive payments at different ranks.
Given , the paper's symmetric equilibrium has an ability threshold : a solver enters precisely when . The expected rank reward determines that threshold, and the paper gives an integral expression for the resulting equilibrium performance (Proposition 1, p. 8). Both quantities depend on the entire announced allocation. The independent ability profile has the product law of the density on . If is the number entering, the failure probability is .
The firm's objective is equation (6), with failure cost :
Every allocation comparison recalculates , , and the failure probability. An optimal allocation maximizes this objective over every feasible , including allocations that spend less than the budget.
The main target is Theorem 2, including existence of an optimum. For , every positive budget and nonnegative failure cost have an optimum, and every optimum pays exactly one rank. For , the corrected statement asserts thresholds and, for each budget , a threshold such that every optimum satisfies
Here is the largest number of equal awards that maximizes participation. The same two thresholds govern both clauses. Equality at a threshold is left open because allocations can tie there. The bound is the paper's constrained-budget regime, stated in its discussion and used in its threshold proof (Theorem 1 and its discussion, p. 10; proof of Proposition 1, p. 23). At , this regime may have no multi-reward case; the conditional statement retains the paper's population range.
The milestone results include the rank-probability identity (EC.3), the binomial law for the number of entrants (Proposition 2), the equal-award participation optimum (Theorem 1), attainment of the firm's maximum, and the claim that winner take all maximizes the first, performance term of (Electronic Companion and proofs, pp. ec1, 9–10, 28).
The theorem separates the firm's two aims in a precise way: a positive entry cost and a sufficiently consequential failure can justify paying more than the top rank, while the participation-maximizing number bounds how far the firm should spread rewards. The result is a statement about all optimal feasible allocations, not merely a comparison of a few equal-split choices. It also identifies the number of entrants through a binomial law, so the failure event has an explicit probability (Proposition 2, p. 9).
The paper presents these results and their arguments, but this mission's statements still require Lean proofs. A complete formalization would connect the rank and participation formulas to the objective evaluated on independent ability profiles, and establish existence and the design regimes. The order-statistic definitions and product-measure treatment of the ability population can be reused in other contest models.
The obvious thought is to maximize performance and participation separately, then compare their best allocations. That does not settle the firm's problem because changing a reward changes the entry threshold and the performance schedule at the same time. In particular, the performance term under partial entry cannot be replaced by its guaranteed-entry counterpart: entrants are selected by ability, and the selection threshold moves with the allocation. The printed proof of Theorem 2 cites a guaranteed-entry result at this point, leaving a substantive partial-entry comparison for the mission (proof of Theorem 2, pp. 27–28; Theorem EC.2, p. ec5).
Lean uses natural-number ranks , real abilities and rewards, and the density-based measure on whose finite product gives independent solver abilities. The order-statistic CDF is a binomial sum; its empty-range value is zero. The participation threshold is the least for which expected rank reward reaches , with value one when that set is empty. The submission schedule is equation (4), and the firm's objective is the expectation in equation (6), not its later reduced integral form. A finite maximum over the solvers represents the best submission. Only positive rewards count toward ; the unused rank-zero coordinate and rewards above rank are fixed at zero. At ability zero, division by ability is avoided in the submitted definitions.
The source's proof introduces an additional constraint that , even though Theorem 2 does not require it and a large failure cost can make it impossible. The mission keeps the original feasible set with and no sign restriction on . This prevents a formally easy but vacuous optimum claim. The strict performance milestone is labelled as a strengthening of the printed maximization claim. Contributions that establish the equilibrium characterization, measure identities, continuity and attainment, or a rigorous partial-entry performance comparison are within scope.
The secretary problem asks an online decision maker to pick the best of candidates who arrive in uniformly random order, deciding irrevocably on each one at arrival. Its matroid generalization, the matroid secretary problem (MSP) of Babaioff, Immorlica and Kleinberg (SODA 2007), asks the algorithm to select an independent set of a matroid whose elements arrive in random order. The MSP models online hiring under combinatorial constraints, posted-price mechanisms for matroid-constrained markets and online bipartite matching, and the conjecture that it admits an -competitive algorithm for every matroid is still open.
Soto, Turkieltaub and Verdugo (arXiv:1802.01997; Mathematics of Operations Research, 2021) study the ordinal version, in which the algorithm only compares revealed elements and never sees weights, and introduce the strongest of several competitiveness notions, probability-competitiveness: every element of the optimum must be selected with probability at least . Their central tool is the forbidden sets technique, summarized in a single statement, the Key Lemma, which turns a combinatorial property of an algorithm into a constant competitive ratio. Every constant-ratio algorithm of the paper for a specific matroid class (transversal matroids and gammoids, graphic and hypergraphic matroids, -framed matroids, laminar matroids, semiplanar gammoids) is obtained by verifying the hypothesis of this lemma.
Timeline. Dynkin (1963) and Lindley (1961) solve the classical problem with ratio . Babaioff et al. (2007) pose the MSP. Korula and Pál (ICALP 2009) and Kesselheim, Radke, Tönnis and Vöcking (ESA 2013) analyze random-order algorithms through the reverse arrival sequence, the device the Key Lemma abstracts. Soto, Turkieltaub and Verdugo (SODA 2018, MOR 2021) state the Key Lemma and use it to improve the best known ratios for almost all studied matroid classes.
Let be a matroid on a finite ground set with , and let be a total order on , the value order. The span of is the set of elements whose addition does not increase the rank of . For , the greedy optimum is the base of obtained by scanning in decreasing value order and keeping each element that keeps the set independent; equivalently
The elements arrive in a uniformly random order , and . An algorithm draws a sample size for a fixed sampling probability , observes the arrivals, and returns a set . It has forbidden sets of size (Definition 7) if
The algorithm is probability-competitive if for every , the probability being over and the arrival order.
With
every algorithm with forbidden sets of size , run with sampling probability , satisfies
The Key Lemma separates the analysis of a random-order algorithm into a structural part (exhibit forbidden sets of size ) and a probabilistic part (the lemma itself), so the probabilistic part is done once. Its consequences in the paper include an probability-competitive algorithm for transversal matroids (the first guarantee in the probability notion for Kesselheim et al.'s matching algorithm), ratio for graphic matroids, for laminar matroids and for -framed matroids. Because probability-competitiveness implies the ordinal, utility and intersection notions, each of these also bounds the weighted problem.
The result is proved in the paper; nothing here is open. To our knowledge no part of it is formalized in Lean. A formal Key Lemma makes every forbidden-sets analysis a purely combinatorial obligation (Definition 7 for a concrete algorithm), and it fixes a precise probability model for the random-order MSP that later formalizations of the paper's algorithms, or of the classical secretary rule, can reuse.
The obvious argument, "each earlier arrival is forbidden with probability at most , so multiply", fails as stated: the forbidden set depends on the random set , so the events " is not forbidden" are not independent in the forward direction. The proof needs the reverse arrival sequence: conditioned on , the arrivals are revealed backwards, each uniform in the current prefix and independent of what was revealed after it. Making this conditioning precise over a finite uniform permutation space is the main formal work. The second difficulty is analytic: the expectation in (5) over has no closed form, and the paper bounds it by a continuous-time coupling with uniform arrival times rather than by direct summation.
All objects live in one definitions file, namespace OrdinalMSP.Forbidden.
Fintype R with DecidableEq R and a LinearOrder R; the value order is q < r. The matroid is a Mathlib Matroid R with ground set Set.univ, and the span is Matroid.closure.opt M Q), which is the greedy output.σ : Fin n ≃ R; σ i arrives at time . Times in milestone statements are the paper's 1-based ones.Real.exp 1; the powers are Real.rpow; and branch on before dividing by .Definition 7 is satisfiable (the rule "accept every element after the sample" in a free matroid satisfies it with empty forbidden sets), so the goal is not vacuous; a formalization that strengthens Definition 7, for instance by requiring the selection condition for times , or that fixes instead of drawing it from , would prove a different statement and is ruled out. The auxiliary game of the paper is a proof device and is not formalized; its milestone is a real-number inequality.
Needed infrastructure: counting over Fin n ≃ R conditioned on a prefix set (the reverse arrival sequence), binomial sums, interval integrals of , and calculus on and . The reverse-arrival counting lemmas are reusable for any random-order secretary analysis. Contributions of alternative proofs of the game bound (for example by direct summation) are welcome.
Ad blockers remove advertising from web pages, and with it the revenue that pays for free content. By the time of this paper a large share of desktop users ran one, and publishers had three responses at hand: tolerate ad blockers, block access to users who run one (an adblock wall), or move behind a paywall. The common view was that ad blockers can only hurt ad-funded platforms.
Despotakis, Ravi and Srinivasan (SSRN 3083119, version of November 28, 2017; published in Management Science in 2020, doi:10.1287/mnsc.2020.3653) model this choice as competition between two platforms and show that ad blockers can raise platform revenue. The mechanism is a segmentation effect: users who would install an ad blocker are typically the most ad-averse, and competition over them pushes ad intensities down for everyone. Letting them block ads takes them out of the ad market, so competition for the remaining users is softer. This mission formalizes the paper's first main result, Proposition 1, together with the case analysis of its proof.
Two platforms sit at the endpoints and of a Hotelling line. Users are spread uniformly on ; a user at position gets intrinsic value from platform 1 and from platform 2, plus a common value large enough that every user joins exactly one platform (full coverage). There are two user segments:
The price sensitivity of all users is . Each platform chooses a plan:
At platform 1 a non-adblock user suffers disutility under Ban and Allow and under Fee; an adblock user suffers under Ban, under Allow and under Fee. Platform 2 is symmetric. Within a segment, platform 1's share is the length of the set of users who prefer it,
where are the two disutilities, and the revenue is the sum over the segments of mass × share × payment per user.
The game has two stages. Platforms first choose plans ; then they choose decision values , and a stage-2 equilibrium is a pure Nash equilibrium of the resulting revenue game over . A plan profile with its decision values is an equilibrium if the decision values form a stage-2 equilibrium and, after any unilateral change of plan by either platform, the new subgame has a stage-2 equilibrium in which the deviator earns no more.
The benchmark is the world without ad blockers: plans are Ads (identical to Ban: everyone sees ads, the adblock-prone segment keeps sensitivity ) and Fee.
For :
then (Allow, Allow) with is an equilibrium, each platform earning ; 2. if and , then the same holds and is at least each platform's revenue in every symmetric stage-2 equilibrium of the benchmark subgames (Ads, Ads) and (Fee, Fee).
The milestones follow the numbered cases of the appendix proof: the share formula (case 1), the benchmark subgames (Ads, Ads) and (Fee, Fee) (cases 1–2), the on-path subgame (Allow, Allow) (case 5), the deviation subgames (Ban, Allow) and (Fee, Allow) (cases 8–9), and the three algebraic facts of p. 44 that turn revenue comparisons into conditions on and .
Proposition 1 is the paper's answer to whether ad blockers must hurt publishers: in a region of parameters both platforms prefer to let ad blockers in, and both earn more than without ad blockers. It underlies the paper's welfare result (Proposition 2) and the extensions with an intermediate segment, whitelisting and content investment, which all build on the same equilibrium.
The result is proved on paper by first-order conditions of interior solutions. It is not formalized anywhere. A machine-checked version has to deal with what the first-order derivation leaves out: corner responses where a platform abandons a segment, global rather than local optimality of each response, and uniqueness where it is needed. Two of the paper's intermediate claims fail as printed in parts of the parameter region (see Difficulty), and one threshold on p. 44 contains a typo; the formal statements here are the corrected versions, so a completed proof also certifies the corrected thresholds.
The obvious argument solves the first-order system in every subgame. That gives candidate points, not equilibria. With clipped shares the revenue of a platform is only piecewise quadratic in its decision, and a platform can do better by moving to a corner, for example by raising its ad intensity until it serves no adblock user at all.
This happens in exactly the region where Proposition 1 matters. In the (Ban, Allow) deviation subgame the interior point printed in the paper is not a stage-2 equilibrium for large : at the Ban platform earns about there but about by serving only non-adblock users. The proof must therefore find the right stage-2 equilibrium regime by regime and check every unilateral deviation globally over . Similarly, the benchmark (Ads, Ads) point is not an equilibrium for large , which is why the benchmark comparison quantifies over actual equilibria.
The development needs only real analysis of piecewise quadratic functions and Lebesgue measure of intervals. The model definitions (Hotelling share with full coverage, pure Nash equilibrium over nonnegative reals) are reusable for other duopoly models. Proofs of individual milestones are welcome independently; the goal follows from them by the case analysis described above.
In a communication network, file transfers ("flows") share the capacity of the links on their routes, and the bandwidth-sharing policy decides how much rate each flow receives. The connection-level model of Massoulié and Roberts (2000) treats flows as customers that arrive at random, carry a random amount of data, and leave once it is transferred. Under weighted proportional fairness (Kelly 1997; Mo and Walrand 2000), the rates maximise subject to the link capacities. Its delay performance in steady state, measured by the expected numbers of flows on the routes, is the quantity a network operator cares about.
Most heavy-traffic results for this model are diffusion approximations: Kang, Kelly, Lee and Williams (2009) under a local-traffic assumption, Ye and Yao (2012) under a full-rank routing matrix, with interchange of limits by Shah, Tsitsiklis and Zhong (2014) and Ye and Yao (2016); all assume exponential file sizes. Vlasiou, Zhang and Zwart (2014) obtained the diffusion limit for phase-type sizes. Whether the stationary flow counts depend on the file-size distribution beyond its mean (insensitivity) is the central practical question, since real file sizes are far from exponential. Wang, Maguluri, Srikant and Ying (arXiv:1808.02120, 2021; Math. Oper. Res. 2022) answer it in heavy traffic with explicit bounds, using the Lyapunov drift method instead of diffusion limits.
There are links with capacities and routes ; the routing matrix has if link is on route and otherwise, has full row rank, and every route uses some link. Flows arrive on route as a Poisson process of rate . Their sizes are i.i.d. with a phase-type law in the class : the absorption time of a Markov chain whose transient phases form Erlang blocks with pairwise distinct rates , started with positive probability in the first phase of every block. With subgenerator and initial law , the mean size is and the route load is . The class is dense in the distributions on .
Given the numbers of flows on the routes, the weighted proportionally fair allocation with weights gives each flow on route the rate solving
The state counts the flows of route in phase ; it is a continuous-time Markov chain: arrivals into phase at rate , phase changes at rate , and completions from phase at rate .
Heavy traffic. Fix on the boundary of the capacity region: for all links, with equality exactly on the nonempty set of critically loaded links, . The -th system has arrival rates , , and denotes a random vector distributed as its stationary distribution, with route totals .
The leading constants depend only on the number of critical links and the weights, not on the file-size laws in .
The proof is organised around a new inner product on the phase-level state space (67). In attack order:
The result. The bound is linear in the number of critical links, not routes, and holds without the local-traffic assumption. With equal weights the two sides coincide and give the exact heavy-traffic limit for every file-size law in : proportional fairness is heavy-traffic insensitive. As a by-product, state-space collapse yields the interchange of limits for the diffusion approximation of Vlasiou, Zhang and Zwart (Theorem 5 of the paper, not part of this mission).
Formalizing it. The paper's results are proved on paper; no part of this argument is machine-checked. A formalization yields reusable pieces beyond this paper: the continuous-time Bertsimas–Gamarnik–Tsitsiklis tail bound (Lemma 10), steady-state "zero expected drift" arguments for countable-state chains, and the matrix analysis of phase-type laws (Lemmas 5, 6, 11). The paper's own proof of Lemma 6 contains an incorrect step (a hazard-rate claim that fails for Erlang blocks), so a checked proof of that lemma is itself a contribution.
The drift method needs a Lyapunov function whose drift is negative along the directions the process actually moves. For exponential sizes the diagonal inner product of (9) suffices. With phase-type sizes the natural Euclidean or diagonal inner products fail: the rotation by produced by phase changes can make negative, so (P2') breaks. The integral construction (67) of is what restores it, and checking that is positive definite requires a controllability (PBH) argument. On the probabilistic side, every step "in steady state the expected drift is zero" requires integrability of an unbounded Lyapunov function under the stationary law of a countable-state chain, which must first be established from the tail bounds; Mathlib has no ready theory for this.
All objects are in the namespace HTInsensBW.PhaseType. A class- law is a structure (PhaseTypeD) with blocks, lengths, distinct rates and an initial law; phases are pairs (block, position), 0-based. The network (BWNetwork) carries , , , and one law per route; the standing assumptions are explicit theorem hypotheses: 0/1 entries and full row rank of , every route uses a link, , , , (7)–(8) with . The allocation is a predicate on route totals, and theorems take an allocation function satisfying it (it exists and is unique by milestone (5)). The chain's rates are exactly (60) with zero diagonal; a stationary distribution is a nonnegative, total-mass-one solution of the global balance equations (the published KellyStochasticNetworks.FullBalance), and statements hold for every such solution. and are explicit – statements with constants chosen before , and every expectation carries a summability clause.
The goal's statement uses only the model layer; , , the cone distance and the projections live in a second definitions module used by the milestones. The goal cannot be satisfied trivially: the allocation exists (milestone (5)), stationary distributions exist for every (Lemma 7), the expectation must be finite, and none of the network, the weights or the file-size laws is specialised.
Paper slips handled in the statements: Lemma 7 is stated for (the page says "nonnegative"); Lemma 8 quantifies over all with , as its proof does; is stated for critical links only, which is what its derivation shows; Lemma 9 holds for every multiplier vector, since multipliers need not be unique; the closing brackets missing in (80) are restored.
Needed infrastructure: the matrix exponential of block-bidiagonal matrices and its integrals; positive definiteness through the PBH test; countable-state continuous-time Markov chains (irreducibility, stationarity, uniformisation, zero expected drift for integrable Lyapunov functions); finite-dimensional convex optimisation with KKT conditions. Contributions to any of these, and proofs of any milestone, are welcome.
A learner wants to locate an unknown number, the true value , by asking threshold questions of a database: each query is answered by the single bit . Bisection finds to within with queries, and no strategy does better (Waeber, Frazier and Henderson, 2013). Bisection, however, reveals everything: each query is a function of the previous answers, so anyone who sees the queries can reconstruct the answers and hence .
Tsitsiklis, Xu and Xu study a learner whose queries, but not the answers, are watched by an adversary. Their motivating examples (pp. 2–3) are a firm testing prices whose surveys a competitor can observe, a consumer browsing products on a platform that sees what is browsed, and an optimizer whose test points are visible to the database it queries. The question is how many queries the learner needs if she must find accurately while keeping the adversary uncertain about it.
The model is from the authors' COLT 2018 extended abstract and Z. Xu's master's thesis (MIT, 2017); the journal version appeared in Operations Research (2021). This mission formalizes arXiv version 3 (26 Feb 2020), and all page and theorem numbers refer to it.
The learner submits queries one at a time. A random seed , uniform on , lets her randomize. A learner strategy of length consists of query maps and an estimation map (§2.1, p. 8): the -th query is , where are the responses so far, and the estimate is . The class consists of the strategies of length that submit pairwise distinct queries. Write for the queries and for the estimate when and .
The adversary knows and sees . The set of query sequences that can occur when is (eq. (1)), and the adversary's information set is
Its size is measured by the -cover number , the least number of closed intervals of length at most whose union contains (Definition 3.2, p. 10). A strategy is -private (Definition 3.3, p. 10) if
The query complexity is (eq. (5), p. 11). All logarithms are base 2 and are rounded up (footnote 1, p. 4).
For , and an integer with ,
The Opportunistic Bisection (OB) strategy first places "guesses" with fixed queries, and then runs a bisection of steps in one of the gaps. The bisection is truthful if no guess caught , and driven by the seed otherwise. The milestones are: OB is accurate; the union of guesses has (Claim 6.3); for every observable (Claim 6.4); the cover number is monotone; and OB is -private (Proposition 6.2).
For an accurate strategy, the final interval between consecutive sorted queries (with , ) has length at most (§7.1), so , the union of special intervals (display (20)). Lemma 7.1 puts queries in for some true value, and accuracy alone gives . A covering bound gives , with the number of special queries in (p. 21). Together these give for every private strategy.
Corollary 4.2 (the case ) is Theorem 4.1 specialized and is not posed separately.
The result. The theorem gives the cost of privacy in this model up to an additive constant. At the two bounds differ by at most 4 (Corollary 4.2), and the extra cost over plain bisection is at most an additive . That is much less than the non-adaptive -dense strategy, which is always private but needs about queries (§5). The lower bound also shows that the obfuscating queries cannot be shared with the queries that locate (§7, p. 19).
Formalizing it. The result is proved on paper, but Lemma 7.1 is given only an intuitive argument: the paper calls its proof "fairly standard" and omits it (p. 20). The covering step on p. 21 is argued component by component, with an exceptional component straddling . A formal development supplies both and checks the bookkeeping behind the constants , and . To our knowledge, no machine-checked proof of this theorem or of the bisection lower bound in this form exists.
The upper bound is a construction. Its delicate point is Claim 6.4. For every point of every guess one must exhibit a seed under which produces exactly the observed queries, and that seed differs according to whether the observed run was truthful or fictitious.
The lower bound is harder. Counting queries is not enough by itself, because the obvious argument conflates query values with query indices. Lemma 7.1 counts indices along a single run (a fixed true value and seed). The covering bound counts distinct values in , one of which may be the artificial point . The natural first idea, a direct counting bound on , is unavailable: is a minimum, so a lower bound must be proved for every private strategy of every length. Only the goal speaks about , where the upper bound shows the set being minimized is nonempty.
Everything lives in the namespace PrivSeqLearn.QueryComplexity, built on Mathlib with no measure theory in any statement. Conventions:
Fin Ybar with 0 < Ybar. "Positive probability" is read as "for some seed" and "probability one" as "for every seed", which is exact for a uniform seed on a finite set.List Bool, and the response to at true value is decide (q ≤ x). Queries are 0-indexed (Fin N).InPhi) requires query values on every history of length and estimate values on every history of length to lie in , and the queries to be pairwise distinct for every and seed.Fin L-indexed families of closed intervals Set.Icc. and are sInf over , which equals the minimum when the set is nonempty.⌈Real.logb 2 ·⌉ computed in , so never truncates. In the regime, all log arguments exceed 1.Trivializing encodings are ruled out:
0 < Ybar;Contributions are welcome on any milestone. The bisection lower bounds (Lemma 7.1 and the bound) and the interval-covering facts are reusable beyond this mission.
A constrained optimization problem often has an objective of the form : a smooth map describes the model, while an extended-real function gives the cost and can assign to infeasible outputs. Such a description covers polyhedral constraints, quadratic penalties on pieces, and many nonsmooth composite objectives. Solvers need to know how the local first and second order behavior of depends on the two parts of the model. The usual chain rules in Rockafellar and Wets, Variational Analysis use qualification conditions stronger than an error bound at the point of interest. Mohammadi, Mordukhovich, and Sarabi develop chain rules under a metric subregularity qualification condition (MSQC), including the second order result targeted here.
The paper was circulated as arXiv:1905.08837v2 in 2019 and published in Mathematics of Operations Research in 2022. This mission follows the pinned arXiv version, whose theorem and page numbering is used throughout. The result is known in mathematics; the open task here is its formalization in Lean. The paper also derives optimality conditions and statements about KKT systems from its second order analysis, but those later applications are outside this mission's target. Source: §§1, 5, 6, 8.
Fix finite dimensional Euclidean spaces and . An extended-real function has finite domain . Assigning outside a feasible set lets an ordinary function and a constraint be treated together. A convex piecewise linear-quadratic function (PWLQ) has a finite collection of polyhedral convex pieces whose union is its domain. On each piece its value is , where is symmetric. The separate formulas must agree where pieces meet, because all describe the same function. Source: (2.9), p. 5.
A function is fully subamenable at when it agrees with on a neighborhood of , with twice differentiable at , convex PWLQ, and MSQC satisfied there. Write . MSQC says that for some and all near , . This controls how far a nearby point is from feasibility through its residual in the outer domain. It is the paper's condition (3.5), not metric regularity. Source: Definition 3.2 and (3.5), pp. 9–10; Definition 4.2, p. 16.
The subderivative is a lower limit of first order difference quotients as positive time tends to zero and the direction tends to . Given a limiting subgradient , the second subderivative uses the quotient after subtracting the linear term and dividing by . Proper twice epi-differentiability means these quotients epi-converge to a second subderivative that never equals and is finite somewhere. The paper gives an equivalent test using recovery directions for every positive null sequence; that test is used in Lean. Source: (2.11), (2.15), (2.16), pp. 6–7.
For every , a fully subamenable is properly twice epi-differentiable at for . With
its second subderivative satisfies, for every ,
The maximum is attained; a supremum alone is a weaker claim. This is Theorem 5.2 and (5.3), p. 22.
The milestones are the paper's equality rules for first order subderivatives and subgradients (Theorems 3.4 and 3.6), its identification of critical directions with the finite domain of the second subderivative (Theorem 4.4), the PWLQ outer-function formula (4.8), the lower bound (4.10), and the parabolic limit formula (Lemma 5.1). Each names a separate mathematical claim needed to connect the composite model to the goal. Source: §§3–5.
Theorem 5.2 gives a data-level way to evaluate the second order behavior of a nonsmooth composite: the outer function contributes its own second subderivative, the inner map contributes its Hessian, and multipliers connect the two. Its properness and epi-differentiability clauses make the formula suitable for the paper's later no-gap second order optimality conditions and parametric analysis. Without those clauses, an equality of extended-real expressions alone would not establish the stability of the difference quotients. Source: Theorem 5.2 and §6.
A formal development of this result would add reusable definitions and lemmas for extended-real difference quotients, second-order tangent geometry, PWLQ functions, and local composite error bounds. The present draft contains statements and definitions that compile; it does not yet contain proofs of the open theorem items. The published limiting-subdifferential definition is reused, while the paper-specific local representation and multiplier set are defined here.
A first order expansion of does not settle the second order claim. Near a polyhedral boundary, the direction may be tangent while a fixed straight path leaves the domain; the second-order correction and the outer function's active piece matter. MSQC controls distance to feasibility but does not itself identify a feasible second-order path or a maximizing multiplier. The source therefore needs separate results about critical directions, PWLQ second subderivatives, parabolic limits, and dual attainment before the full formula can be stated with a maximum. Source: §§4–5, especially pp. 17–23.
Lean uses EuclideanSpace ℝ (Fin n) and EReal. The paper's codomain excludes ; the relevant hypotheses enforce that exclusion, while the subderivatives themselves may take either infinite value. The finite domain is defined by exclusion of . A PWLQ representation records finite closed half-space intersections, symmetric operators, and the exact quadratic coefficient. Twice differentiability includes differentiability near the base point and differentiability of the derivative at the point. The composite identity holds on a neighborhood rather than globally. MSQC uses the paper's local distance estimate with . Positive null sequences represent ; a filter lower limit represents the varying direction. The second quotient retains the paper's denominator.
The subdifferentials are the published analytic regular and limiting subdifferentials. Their use matches the paper's geometric subdifferentials at the lower semicontinuous functions in these statements. The goal computes the second subderivative from the lower-limit definition, rather than defining it by (5.3). Full subamenability retains MSQC and a genuine PWLQ representation; it is neither an empty-domain case nor a stronger metric-regularity special case. Contributions toward proofs of the milestone theorems, their needed tangent-set geometry, and the goal are in scope.
Many allocation problems divide an object whose value to the participants is uncertain at the time the division rule is designed: computing time on a shared cluster, a recurring chore, the cost of a service used jointly. If the rule must be fixed before the realizations are known, and must treat everyone fairly in expectation, the designer faces a tradeoff between ex ante fairness and ex post efficiency. Bogomolnaia, Moulin and Sandomirskiy (arXiv:1903.10361, published in Management Science, 2022) study this tradeoff for a single divisible object, in the setting of online and repeated fair division (Moulin 2019).
The paper characterizes the most efficient fair rules that need almost no knowledge of the underlying distribution. For a good the efficient fair rules form a one-parameter family; for a bad (a chore, a cost) there is a single most efficient fair rule, the Bottom-Heavy rule. This mission formalizes the bads result, Theorem 17 of the paper.
There are agents and one divisible bad. A profile lists the agents' disutilities for the whole bad; zero disutilities are allowed. Write , and . The disutility profile is random, with distribution on ; the coordinates may be correlated. A problem is normalized if for every .
A division rule maps each realized profile to a lottery ; agent bears the fraction of the bad. A rule is almost prior-independent (API) if it is a single measurable map, used for every distribution once disutilities are normalized by their means. It is symmetric if permuting agents permutes shares. It satisfies Fair Share if in every normalized problem each agent's expected disutility is at most of her expected disutility for the whole bad:
The social cost of at is , and dominates if its social cost is at most that of at every profile and strictly lower at some profile.
For , let (with ). The Bottom-Heavy rule orders agents by disutility, gives the full to the longest prefix of low-disutility agents that fits into the simplex, splits the remainder equally among the next class of tied agents, and gives nothing to the others. The canonical rule is , whose prefix shares are .
For every , is a symmetric API rule satisfying Fair Share, and for every symmetric API rule satisfying Fair Share with somewhere on ,
Theorem 17 says that, for a bad, the efficiency cost of ex ante fairness without knowledge of the prior is resolved by a single explicit rule: no fair API rule is ever cheaper ex post, at any realization, than the Bottom-Heavy rule. This is the basis of the paper's worst-case and asymptotic comparisons for bads (competitive ratio and price of fairness, §5–6), and it contrasts with goods, where the undominated fair rules form a family. Proposition 14 is of independent use: it turns a condition on all priors (Fair Share) into a pointwise inequality on the rule.
The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the model (normalized random objects, API rules, Fair Share, ex post domination) and a path of eight milestones to the main theorem. The formalization also makes precise two points the printed proof leaves implicit: the convention at and at zero disutilities, and the case of the final domination argument, which Step 3 does not cover.
The "only if" direction of Proposition 14 is the analytic core. Fair Share is a statement about expectations under every normalized distribution, and has to be turned into a bound on the rule at each profile. Testing Fair Share on finitely supported normalized laws shows that agrees with its concave majorant at ; extracting a supporting affine function there and pinning down its coefficients needs the symmetry of the rule and the boundary profiles . Mathlib has supporting-hyperplane and separation theorems but no concavification operator.
The domination steps are exchange arguments around the threshold that defines the Bottom-Heavy rule. Step 3 compares two thresholds as varies; it is proved on profiles with distinct coordinates, and ties need a separate argument (the paper invokes continuity of the total disutility, while the rule itself is discontinuous there). The natural first idea, that minimizes cost among rules satisfying (9) for , does not suffice: a fair rule may satisfy (9) only for a smaller , so the comparison across the whole family is needed, and the case (Equal Split) requires the anti-monotonicity of and Chebyshev's sum inequality.
Agents are Fin n (0-based; the paper's agent 1 is agent 0), and throughout. Profiles are vectors x : Fin n → ℝ; is 0 ≤ x and includes zero coordinates. A distribution is a measure on Fin n → ℝ, normalized meaning probability, carried by the orthant, integrable coordinates with mean . An API rule is a measurable map (Fin n → ℝ) → (Fin n → ℝ) that is simplex-valued on the orthant; values off the orthant never matter. Fair Share quantifies over all normalized laws, not only finitely supported ones. Domination is for a bad: lower social cost, weakly everywhere on the orthant and strictly somewhere.
The convention is explicit: the bound (9) is whenever , for every ; in with , agents with zero disutility split the bad equally (at this is ). The threshold is encoded at the level of values (prefix masses ) rather than by sorting. Two printed claims are posed in corrected form and disclosed in the statements: the case of Step 2 holds only on profiles with all coordinates positive, and "α ≥ 0" in the proof of Proposition 14 is .
A trivializing formalization is ruled out: the goal asserts that is itself a symmetric API rule satisfying Fair Share (so a mis-encoded , such as the cost-minimizing utilitarian rule, cannot pass), "other" means differing at some profile of the orthant, and domination includes a strict inequality.
A complete development needs: integrals of bounded measurable functions against probability measures on Fin n → ℝ; a supporting-hyperplane or concave-envelope argument for Proposition 14; finite-sum manipulations over filtered Finsets and Chebyshev's sum inequality for the domination steps; measurability of piecewise-defined maps. The model layer (normalized random objects, API rules, Fair Share, domination) is reusable for the goods half of the paper. Proofs of any milestone, and sanity checks of the definitions (Example 16 for ), are welcome.
A simple formula for the average gate fidelity of a quantum dynamical operation establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
Let be a positive integer and let be a trace-preserving quantum operation on a -dimensional quantum system . Define its average fidelity by , where is the uniform Haar probability measure on normalized pure states. Let be a -dimensional reference system, let , and define . Then
This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.
Formalization Note The frozen channel predicate supplies complete positivity, trace preservation and linearity through a normalized Kraus representation. The Haar state measure is the image of normalized full-unitary Haar measure applied to a fixed unit vector; channel integrability is established in the imported definition module. Entanglement fidelity is an overlap probability, independent of the choice of maximally entangled state.
Let be a positive integer and let be a trace-preserving quantum operation on a -dimensional quantum system . Define its average fidelity by , where is the uniform Haar probability measure on normalized pure states. Let be a -dimensional reference system, let , and define . Then
This identity converts entanglement fidelity into the average probability of preserving a uniformly distributed pure state.
Formalization Note The frozen channel predicate supplies complete positivity, trace preservation and linearity through a normalized Kraus representation. The Haar state measure is the image of normalized full-unitary Haar measure applied to a fixed unit vector; channel integrability is established in the imported definition module. Entanglement fidelity is an overlap probability, independent of the choice of maximally entangled state.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Let , let be a completely positive trace-preserving map on -dimensional matrices, and let be a unitary target. Let denote the normalized Haar average of . Then
Thus unit overlap fidelity characterizes exact implementation of the target channel, including its action on all density inputs.
Let and let be a completely positive trace-preserving map. Define its normalized unitary Haar twirl by . Then is completely positive and trace preserving, and
for every density matrix and unitary . Here is the normalized pure-state Haar overlap average, and is the normalized maximally entangled overlap with identity action on the reference register.
These properties allow the fidelity calculation to be reduced to a unitarily covariant channel.
Let and let be a completely positive trace-preserving map. Its normalized unitary Haar twirl has a real parameter , independent of the density input, such that
No additional interval constraint on is imposed. This identifies the twirl as a depolarizing channel.
Let and let be a completely positive trace-preserving map. Let be a complex operator basis consisting of unitaries with . With the overlap of the normalized maximally entangled state before and after applying to its system register,
This expresses entanglement fidelity using the channel action on an operator basis.
Let , let be a completely positive trace-preserving map, and let be a unitary target. Let be a complex operator basis of unitaries satisfying . The normalized Haar average gate overlap is
The target inverse conjugates the channel output. This is the paper's general qudit formula, with no unitality assumption.
Let be a completely positive trace-preserving map on a qubit, let be a unitary target, and let , , be the Pauli matrices, with . Then the normalized Haar gate overlap satisfies
This specializes the general operator-basis formula to three nonidentity Pauli operators; trace preservation suffices.
Let , let be a completely positive trace-preserving map, and let be a unitary target. Let be a complex operator basis of unitaries with . Let be a complex operator basis whose elements are density matrices. Define the unique complex coordinates by . Then
This gives an exact algebraic determination from the outputs on the state basis. It asserts no finite-shot accuracy or sample-cost guarantee.
These additional statements have current no-edit source review. Their formal proofs remain open; deferred results are excluded.
The precision matrix of a Gaussian random vector encodes its conditional independence structure: exactly when and are independent given the other coordinates. Estimating it is a basic step in Gaussian graphical models, portfolio selection and linear discriminant analysis. The textbook estimator, the inverse of the sample covariance matrix , fails when the number of samples is smaller than the dimension : then is singular and the maximum likelihood problem has no solution. Even for the inverse sample covariance is badly conditioned.
Nguyen, Kuhn and Mohajerin Esfahani (arXiv:1805.07194, Operations Research 2022) replace the nominal distribution in the likelihood by the worst case over all normal distributions within a type-2 Wasserstein distance of it, and show that the resulting robust problem has a closed-form solution. The solution keeps the eigenvectors of and maps its eigenvalues through an explicit nonlinear shrinkage, and it is invertible for every sample size. Shrinkage estimators of this kind had been proposed earlier for statistical reasons (Ledoit and Wolf, doi:10.1016/S0047-259X(03)00096-4); here the shrinkage follows from the robust model rather than being imposed.
Fix a dimension . Write and for the positive semidefinite and positive definite symmetric matrices, and for the trace inner product. For distributions on the type-2 Wasserstein distance is
the infimum over couplings with marginals , (Definition 1.1).
Given a sample covariance matrix (possibly singular) and a radius , the ambiguity set is
the centred normal distributions, degenerate ones included, within distance of the nominal one. The worst-case expectation is (7), and the robust estimation problem (5) is
where is the set of admissible precision matrices; without structural information .
The paper reformulates (5) through the metric on (Definition 2.3), the scalar program (8)
and the joint convex program (6), which minimizes plus the objective of (8) over , .
Let , , and with orthonormal . Then the equation
has a unique positive solution , and the unique minimizer of (5) is
The result. Theorem 3.1 gives the robust estimator in closed form up to an eigendecomposition and a scalar root, so it costs no more than the sample covariance itself. It shows that the estimator commutes with , is positive definite for every even when is singular, and depends on the data only through the eigenvalues; the paper's later sensitivity results (Proposition 3.5) and the numerical comparisons with Ledoit–Wolf shrinkage and the graphical lasso rest on this formula. Theorem 2.6 shows more generally, for sparsity-constrained , that the robust problem is a convex program although the ambiguity set is not convex.
Formalizing it. The results are proved on paper; none is machine-checked. The formalization exercises a measure-level definition of the robust problem, with the ambiguity set defined through the coupling Wasserstein distance, and connects it to matrix analysis: the Gelbrich formula for Gaussians, a semidefinite duality, continuity of optimal value functions, and a first-order optimality argument for a matrix-fractional objective. Each milestone is reusable for other Gaussian–Wasserstein robust models, of which the platform already has several (Kalman filtering, minimax mean-square-error estimation).
The obvious argument is to plug into the first-order conditions of (6). This works only when : for singular , every zero eigenvalue gives , so is singular and is not even feasible in (6). The singular case, which is the case of interest (), therefore needs continuity of the optimal value and of the worst-case expectation in , which is the content of Theorem 2.6 and Proposition 2.8. Those in turn require the reduction from distributions to covariance matrices (the Gelbrich formula, which holds for degenerate normals and is an optimal-transport theorem in its own right), a Lagrangian duality with a Lyapunov-equation inner problem, and a priori eigenvalue bounds on near-optimal that vary continuously with . Sufficiency of the first-order conditions also needs joint convexity of , which the paper cites.
is EuclideanSpace ℝ (Fin p) and matrices are Matrix (Fin p) (Fin p) ℝ with the entrywise topology. is Mathlib's multivariateGaussian 0 S, which allows singular . The Wasserstein distance is the published coupling distance WassersteinDRO.Gelbrich.wassersteinDistance 2, valued in ; the radius enters through ENNReal.ofReal ρ. The square root is the published psdSqrt, and the published WassMMSE.Sandwich.frob. The worst-case expectation, , and the values of (6) and (8) are suprema and infima in EReal. Every distribution in is Gaussian, so the integrand is integrable. Every matrix inverse sits under the constraint inside the infimum. "Unique minimizer" is stated as IsMinOn over all positive definite together with equality of every positive definite minimizer to . The eigendecomposition is an arbitrary orthonormal one, not a basis chosen by the library.
One hypothesis is added: , because for (16b) has no positive solution. Definition 2.1 prints the normal density without the factor in the exponent; the standard normal distribution is used.
The goal is stated for the measure-level problem (5). Stating it on the matrix program (6) would be a different and, for singular , false theorem. Replacing by the covariance ball or by all distributions, or computing suprema as real sSup (which returns on unbounded sets), would trivialize or change the statement.
The mission concerns the zero-mean problem (5) with for the goal; Theorem 2.6 is posed for general . Out of scope: Theorem 2.10 (the unknown-mean problem (4)), Corollary 2.9, Lemma 3.3, Proposition 3.5, the algorithm of §4, the extremal distributions of §5 (Theorem 5.1) and the experiments of §6. The Gelbrich formula (Proposition 2.2) is not posed here; it is Open on the platform as WassKF.Reform.proposition_2_2. The Open theorem WassMMSE.Sandwich.proposition_A_4_i, a covariance-level duality behind Proposition 2.8, is included for reuse. Welcome contributions: the Gelbrich formula for possibly degenerate centred normals, second moments of multivariateGaussian, continuity of optimal value functions (Berge's maximum theorem), and convexity of the matrix-fractional function.
Display advertising is sold one impression at a time, mostly through second-price auctions with reserve prices. A reserve tailored to each buyer and to the features of the impression can raise the seller's revenue considerably, but the right reserve depends on the buyers' valuations, which the seller does not know and must learn from past auctions. The buyers participate in the same exchange day after day and know that their bids feed the seller's learning, so a patient buyer may bid untruthfully today to obtain lower reserves tomorrow. Learning reserve prices from strategic buyers is therefore a joint problem of statistics and incentives.
Golrezaei, Javanmard and Mirrokni (arXiv:2002.11137, Operations Research 69(1), 2021) study this problem in a contextual model and propose the policy CORP (Contextual Robust Pricing). Earlier work on learning against strategic buyers considered a single buyer facing posted prices, without contexts: Amin, Rostamizadeh and Syed (NeurIPS 2013) introduced the discounted strategic buyer, and contextual and revenue-optimization variants followed (Amin, Rostamizadeh and Syed, NeurIPS 2014; Mohri and Muñoz Medina, NeurIPS 2015). Personalized reserves in second-price auctions were studied by Paes Leme, Pál and Vassilvitskii (2016). The present paper treats many buyers, personalized reserves, contexts in and censored observations (the seller sees who won, not the valuations).
In every period the seller observes a feature vector , drawn i.i.d. from a law supported in the unit ball. Each of buyers has the valuation
where is an unknown preference vector with and the noises are i.i.d. with a known density on , mean zero, and distribution function . Assumption 1 asks and to be log-concave on .
Each period runs a lazy second-price auction with personalized reserves : the highest bidder gets the item if and pays ; nobody else pays. The benchmark knows the and sets (4); its expected revenue against truthful buyers is (5).
CORP works in episodes with . At the start of episode it computes, for each buyer, a maximum-likelihood estimate over from the censored outcomes of episode (8)–(9). In each period of episode , with probability it explores: one uniformly chosen buyer is offered the item at a price uniform on . Otherwise it exploits with reserves (10).
Buyer 's bid may depend on his own history of valuations, bids, allocations and payments, on , on and on private randomness. His utility is with a discount factor , and buyers are utility-maximizing. The regret after periods is , worst case over and (7).
There is , depending only on , such that for all , , , all admissible and all utility-maximizing buyers,
If true, Theorem 4.1 says that a seller can learn personalized, contextual reserves from censored data at a cost logarithmic in and linear in , even when buyers manipulate their bids. The strategic term vanishes as buyers become impatient. The episodic delay between a bid and its effect on reserves, together with the random exploration prices, is what makes untruthful bidding unprofitable. The lemmas are of independent use. Proposition 3.1 and Lemma 2 concern the monopoly price under log-concave noise. Lemma 3 is a deterministic fact about second-price auctions. Corollary 18.2 is a vector concentration inequality.
Status. None of these results is machine-checked anywhere known to us. The paper's printed proof has gaps. Proposition 9.1 (p. 52), which bounds the estimation error of the MLE by the number of lies, fails as printed. With uniform noise a single lie per episode keeps the estimate a constant distance from . Its supporting Lemma 5 uses a constant that is infinite for every compactly supported (p. 71). Its curvature bound (89) also fails when a likelihood term leaves the support of . Lemma 6 (p. 76) conditions on an event the exploration lottery itself moves. A proof of Theorem 4.1, or a counterexample to it, would settle the question. The goal is stated as the paper states it, and is neither asserted nor denied here.
The natural route is the paper's. First bound the estimation error of the censored MLE in terms of the number of lies. Then bound the number of lies by comparing a lie's discounted future gain with its immediate loss under the exploration lottery. Finally sum over episodes.
The first step is where it breaks. With noise supported on , an observation whose threshold falls outside the support carries no curvature. Its likelihood term is constant or , so the minimizer of (9) is in general a set, not a point. A minimizer at the wrong end of that set can keep the reserve below the benchmark for many episodes, even with truthful buyers. Any proof must say which minimizer CORP takes, or show that all of them work. The second step must handle buyers who react to one another through their histories; the paper's proof holds the other buyers' bids fixed. The concentration steps need a vector martingale inequality and a covariance concentration bound, neither of which is in Mathlib.
Lean represents features as EuclideanSpace ℝ (Fin d) and buyers as Fin N. Periods are indexed from internally (Lean's is the paper's ), and episodes likewise (Lean's is the paper's , so ). Period always explores. The per-period randomness consists of the features, the noises, the exploration coin, the chosen buyer, the exploration price and the buyers' seeds. It is independent across periods, under Measure.infinitePi, and the play is defined by recursion over periods. The likelihood (9) takes values in with ; a real-valued Real.log would make impossible observations free and change the estimator. The estimator (8) and the reserve rule (10) are arbitrary measurable selections of the argmin and argmax, quantified universally. No tie-break or uniqueness is added. The same reserve rule defines the benchmark (4).
Standing assumptions and added hypotheses.
Ruled out. The constant comes before every instance, horizon, selection and strategy, so a bound depending on or on the instance does not count. The policy is CORP as defined, not any reserve-setting rule. The rationality hypothesis is satisfiable.
Infrastructure. A complete development needs the following.
Contributions on any milestone are welcome. So is a formal counterexample to the goal in the model as stated, for example with one truthful buyer, uniform noise and the smallest minimizer of (9).
Out of scope. CORP-II and SCORP (Theorems 5.1–5.3, Propositions 11.1–11.2) and the extensions of Appendix 8 are not part of this mission. Proposition 9.1, Lemma 5, Lemma 6 and Theorem 18.1 are not posed (see Significance).
Many proposed quantum optimization and machine-learning methods (variational quantum eigensolvers, QAOA, quantum classifiers) tune the real parameters of a circuit by gradient descent on an objective that is only accessible as a black box. Classically, a finite-difference estimate of costs on the order of evaluations of . Quantum algorithms can access coherently through a phase oracle , and the question is how many such queries are needed to learn to accuracy in the sup norm.
Timeline.
A point of is , with . The paper's is .
Grid and Jordan's algorithm. For qubits put . A bit string encoding the integer labels the grid point , and is the set of these points (Definition 17). Algorithm 2 prepares registers of qubits in uniform superposition over . It applies the phase oracle once, applies the inverse grid Fourier transform to each register, and measures the outcome .
Index sequences and analyticity. For , is the -th partial derivative along the coordinates , and (Definition 4). The function is analytic around if
(Definition 5, there at ).
Central differences. The central difference coefficients are
The degree- central difference of is , an approximation of (Definition 7).
Queries. A fractional query with counts as one query (Definitions 10–11). The algorithm of Theorem 25 has parameters and . It runs Algorithm 2 with qubits per register on the phase , where . It reads each outcome as , repeats times and outputs the coordinate-wise median. One run costs queries to .
There is an absolute constant such that for every , and some parameter choice, made before and , uses at most
queries. For every and every smooth that is analytic around with (), it outputs with with probability at least .
The result. Theorem 25 gives a quantum gradient algorithm whose query count grows like in the dimension and nearly linearly in . Jordan's original analysis gives , and classical finite differences need on the order of evaluations. Section 6 of the paper shows that cannot be beaten for a class of smooth functions, so Theorem 25 is optimal up to logarithmic factors. Section 5.5 shows that probability oracles built from parametrized circuits satisfy the derivative bound, so the theorem applies to gradient-based training of variational circuits.
Formalizing it. The theorems are proved in the paper; this mission is not aware of a machine-checked proof of any of them. A formal proof would check the explicit constants (1/1000, , , ) and the accounting of fractional queries, which are spread across the main text and Appendix A. It would also produce reusable libraries: exactness and coefficient bounds for central differences, concentration of random multilinear forms, and a phase-estimation-style analysis of Jordan's algorithm on the published Lean model.
Jordan's algorithm reads off a gradient only if the phase is almost exactly affine on the whole grid. A truncated Taylor expansion of makes the error of order- terms grow like on the cube, which destroys the scaling. The approximation is only good on most of the grid, not all of it. The guarantee therefore has to tolerate a small fraction of bad grid points inside the quantum algorithm (Lemma 20) and has to control random multilinear forms (Lemma 36). The analysis also has to keep explicit, -uniform control of the central difference coefficients, whose sizes enter both the approximation error and the query count.
Fin d → ℝ, whose norm is . is iteratedFDeriv along coordinate vectors, and functions are assumed (ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)). "Analytic" is the Taylor representation (5) at the relevant point (IsTaylorRep), not Mathlib's local AnalyticAt.QAlgorithms.gradientAlgState. Independent runs multiply.Contributions are welcome at every level. Most useful are general facts about central difference coefficients (moment identities, , the binomial ratio bounds), concentration of multilinear forms in independent symmetric variables, and the single-run analysis of gradientAlgState. These are reusable beyond this mission.
Stress testing and data-driven decision making often combine two samples: observations of the quantity of interest and additional scenarios (stress scenarios supplied by a regulator, or unlabeled data). Blanchet and Kang (arXiv:1605.01340v4, 2020; later in Operations Research, 2021) propose to measure how far the empirical distribution of the observations is from the set of distributions that live on the merged sample and satisfy a hypothesis about a parameter, such as "the mean is ". The distance is an optimal-transport (Wasserstein) cost, and the resulting statistic is the sample out-of-sample (SOS) profile function.
The construction is the transport analogue of empirical likelihood (Owen 1988), whose central result is a Wilks-type theorem (Wilks 1938): of the likelihood ratio at the true mean is asymptotically . Empirical likelihood can only reweight the observed points. The SOS function can also move mass to out-of-sample scenarios, which is what makes it usable for stress testing. Confidence regions require the asymptotic law of the statistic at the true parameter. That law is the subject of this mission: the paper's main theorem for means, Theorem 1 (pp. 15–16).
Let . Observations and scenarios are random vectors in , all mutually independent, with Lebesgue densities and . A ratio fixes the number of scenarios used with observations. The standing assumptions A1)–A4) (p. 14) are: the samples are i.i.d. with these densities; ; everywhere; and, if , are differentiable with bounded gradients.
The merged sample is . For the SOS function (Definition 1, in the linear-programming form (21)) is
It is the least squared transport cost from the empirical measure of the to a probability measure supported on with mean . The statistic of interest is at the true mean . Write and .
The limits involve a mixed exponential variable. With the rate , the variable satisfies . From one defines , , the solution of , and .
As ,
The goal is the paper's theorem in all three regimes. The case is stated with , a correction of the printed (see Formalization scope).
Theorem 1 calibrates the SOS method. Its quantiles define the radius of a confidence region for the mean, and through the paper's Theorems 2–3 for estimating equations and for stochastic programs whose uncertainty set must cover out-of-sample scenarios. Unlike empirical likelihood, the limit depends on the dimension and on the densities : more dispersed scenarios give smaller distances and smaller quantiles (§4.1.1). The theorem also shows that the scaling itself changes with , from for to for .
The result is proved in the paper; nothing here is an open problem. As far as we know, none of it has been formalized. A formal development adds:
The obvious approach is a Wilks-type expansion: take the dual of the LP, find the dual multiplier by a quadratic approximation, and read off a limit. This works only for . In higher dimensions the transport may only move mass to sample points, and the constraint for observation is controlled by the distance from to the nearest other sample point. That distance is of order , so it competes with at a dimension-dependent scale. The quadratic approximation therefore fails: the dual objective becomes, after rescaling, an average of over dependent first-arrival times, which share the same merged sample.
Three steps carry the weight. (a) The dependent array needs a uniform empirical-process bound (Lemma 1); i.i.d. tools such as the Dvoretzky–Kiefer–Wolfowitz inequality do not apply. (b) A quantitative Poisson approximation (Lemma 2) needs the bounded density gradients. (c) The random concave objective must converge to a deterministic one uniformly enough that its maximiser converges (argmax continuity). Step (c) also needs a multivariate central limit theorem for , which Mathlib does not yet provide.
Representation. Points live in EuclideanSpace ℝ (Fin l). The samples are infinite sequences on a probability space , jointly independent (iIndepFun over ), with laws volume.withDensity. The -th statistic uses the first observations and the first scenarios; is read as the floor, and is allowed. The SOS function is a real infimum over couplings of indexed families. Convergence in distribution is Mathlib's TendstoInDistribution, with limit the image of multivariateGaussian 0 Var(X) under an explicit map . The goal is a conjunction of three clauses, , , .
Conventions and disclosed readings.
Ruled out. The following are not acceptable formalizations: a feasibility hypothesis on every sample; a limit law left as a parameter or quantified existentially; , or given by closed forms rather than from the law of and the fixed-point property; the printed presented as proved; Lemma 2 with a constant uniform in ; Lemma 1 with a Bochner integral, which would be a default for a non-integrable supremum.
Infrastructure. A full proof needs: finite LP strong duality (Farkas), absent as a packaged theorem; binomial/Poisson estimates for small-ball counts; a pathwise Burkholder–Davis–Gundy inequality (Beiglböck and Siorpaes 2015) or another route to Lemma 1; dominated-convergence differentiation of ; a multivariate CLT; and argmax-continuity for random concave functions. The LP duality and the multivariate CLT are reusable well beyond this mission. Contributions to any milestone are welcome; milestones 1, 2, 6, 7 and 8 are deterministic and independent of the probabilistic core.
A clinical trial that compares several treatments for the same condition must decide, patient by patient, which treatment the next patient receives. When the treatments are related (doses of one drug, drugs of one class), an outcome observed on one arm is informative about the others, and a good allocation rule should exploit that correlation. Chick, Gans and Yapar (SSRN 3184758, version of August 31, 2020; later in Management Science) model this as Bayesian sequential sampling with a correlated Gaussian prior and propose the cPDE allocation policy, which samples the arm with the largest value of an adaptive-lookahead optimal-stopping index. Their one theorem, Theorem 1, says that cPDE is asymptotically consistent: run forever, it learns every arm's mean and identifies the best arm.
Consistency is the minimal guarantee asked of an allocation heuristic: a rule that can stop sampling an arm whose value is still uncertain may settle on the wrong treatment forever. The argument follows the consistency proof of Xie, Frazier and Chick (Operations Research 64(2):542–559, 2016; "XFC") for one-step knowledge-gradient (cKG) policies, extended to an index whose lookahead is itself an optimal stopping time.
There are arms. Arm has unknown mean ; an observation of arm is with known , independent across observations. The prior is with positive definite, and sampling arm costs . After observations the belief is ; one observation of arm updates it by Bayes' rule (8):
From a belief , imagine sampling arm alone. The predictive change after samples is a centred Gaussian with variance , ((9)–(10)). The cPDE allocation index is (EC.8):
the supremum over stopping times of the sampling of arm . The one-step index is the same expression with ((EC.6)). The cPDE policy allocates observation to an arm maximizing ; the trial never stops.
For each arm , almost surely,
and almost surely has a unique maximizer which, for all large , is also the unique maximizer of .
Theorem 1 is the only theoretical guarantee the paper gives for cPDE; the rest of the paper is computational (bounds, comparators, experiments). It also covers, through the same sandwich argument, the cheaper variants cPDELower and cPDEUpper (Corollary 1), which are not part of this mission. A consistent policy cannot lock onto a wrong treatment, which is the property a trial designer needs before comparing finite-horizon performance.
The result is proved on paper but has no machine-checked proof. Formalizing it requires a correlated-Gaussian Bayesian learning model, optimal stopping indices defined as suprema over stopping times, and the XFC consistency argument, none of which exist in Lean. The paper's proof also routes Lemma EC.4 through an upper bound that is false as printed (see below), so a checked proof replaces that step with a correct one.
The obvious route bounds above by a one-step index with a fixed lookahead , as the paper's Lemma EC.1 does. That bound fails: of (EC.11) changes under a change of currency while every index is invariant. For , , , , , the formula gives and , while the lookahead already yields a value above . Any upper bound on must instead be uniform over stopping times of unbounded length, and showing that it tends to needs along posterior covariances, not only .
The second difficulty is the "finitely sampled arms" half of the argument (Lemmas EC.3, EC.5): an arm whose variance stays positive must keep a one-step value of sampling bounded away from zero, even while correlated arms are learned. This uses almost sure convergence of the posterior means and the structure of the piecewise linear terminal reward.
Arms are Fin M (0-based) and time counts observations, being the prior. The trial lives on the canonical space times an array of standard normal noises , with law multivariateGaussian µ0 Σ0 times an infinite product of gaussianReal 0 1; the -th sample of arm is . The index is built on its own auxiliary space (a prior draw of and i.i.d. noise), not as a conditional expectation on the trial space.
Committed conventions, each a disclosed reading of the page:
sSup over stopping times of the auxiliary filtration with for some ; this has the paper's value and keeps every expectation finite.MemLp plus eLpNorm → 0.Trivializing formalizations are ruled out: is defined from , not a parameter, a fixed-lookahead index or a supremum over non-adapted times; the policy is defined, not assumed; and both come from (8); the part does not use an integral that is for non-integrable functions; iv) asserts uniqueness; and the false upper bound of Lemma EC.1 is not posed or used.
A complete development needs Gaussian conditioning for the update (8) (that ), the closed form , optional stopping for uniformly integrable martingales, measurability of the index, and the XFC argument. The Gaussian-update and optional-stopping parts are reusable for other Bayesian ranking-and-selection results; contributions of those as separate lemmas are welcome.
Many services rent out a fixed stock of units that come back after use: hotel rooms, rental cars, cloud servers, hospital beds, parking spaces. Such reusable resources differ from perishable inventory because a unit sold now returns to the stock later, so the provider's pricing problem is a queueing control problem rather than a stock-depletion problem. A provider can change its price with the number of free units (dynamic pricing), or post one price and keep it (static pricing). Static prices are simpler to run, and easier to explain to customers, but they forgo the gains of reacting to congestion. How much a single price can lose is the question.
For perishable inventory, Gallego and van Ryzin (1994) showed that under a concave revenue rate a static price loses a vanishing fraction in large systems and at most a fraction in every regime. For reusable resources the evidence for static pricing was numerical or asymptotic: Paschalidis and Tsitsiklis (2000) reported numerical results for multi-class systems, and Gans and Savin (2007) showed near-optimality of static pricing in rental systems whose offered load and capacity are both large. Besbes, Elmachtoub and Sun (arXiv:1905.00731) gave a guarantee that does not depend on the scale of the system: a constant fraction that holds for every capacity, service rate, demand curve and weighting of the provider's objectives.
A provider owns identical units. Customers arrive as a Poisson process of rate , and at price a customer buys with probability ; the effective arrival rate is . Prices and rates are in one-to-one correspondence, so the provider chooses a rate and charges . A buyer holds one unit for an exponential time of mean , pays , and costs the provider . A customer who finds every unit busy is lost.
A stationary policy is a vector of rates , with used while units are free; a static policy uses one rate in every state. The number of free units is a birth–death process with steady-state probabilities
The profit rate, market share and service level of the policy are
and the provider maximizes for weights summing to . The instance class requires the profit rate to be concave in .
For a policy , the static rate is its average rate over the states with a free unit. The proof works in the variables (with ), , and , in which the ratio of service levels of and becomes a rational function , and in a truncation used for .
For every instance of and every optimal stationary policy there is a static rate with
One price serves all three objectives at once, whatever the weights.
The theorem bounds the value of dynamic pricing for reusable resources by a universal constant: dynamic pricing can improve each objective by at most a factor , so a provider can adopt a single price at a known, bounded cost. Since the same price works for all weights, the optimal static price also earns at least of the optimal weighted objective. Section 3.2 of the paper shows that the constructed static rate attains exactly in a limit, so the analysis of that rate cannot be improved.
The result is proved in the paper (arXiv v3, 2020; Operations Research, 2022). No part of it has a machine-checked proof. Formalizing it checks a proof whose second half is a case analysis of high-degree rational functions spread over ten pages of an e-companion, and produces closed-form, reusable statements about the stationary distribution of finite birth–death chains with state-dependent rates.
Step 1 is algebra and one application of Jensen's inequality. The difficulty is in bounding for every . For the bound is coefficient matching between two explicit polynomials. For the numerator and denominator of have degree growing with , and no term-by-term comparison works uniformly; the paper's lemmas each cover a regime of and require bookkeeping that is uniform in .
A second difficulty is Lemma 1. It is a statement about the average-reward optimal policy of a controlled birth–death chain, proved in the paper by value iteration. In the formal statement optimality is a maximization over the closed-form objective, so a proof must either develop the average-reward optimality equation for this chain or argue directly on the closed form. The goal itself quantifies over every optimal policy, including any that is not monotone; the paper's combination step assumes the monotone structure that Lemma 1 provides only on reached states, so a complete proof of the goal must handle this gap.
The model is posed over stationary state-dependent pricing policies with the closed-form steady state of §2.3; the paper's reduction from general non-anticipating policies to stationary ones, and the long-run averages (1)–(2), are taken as the model and not re-proved. A policy is a function lam : ℕ → ℝ read at the states with rates in ; optimality is IsMaxOn of the weighted objective over this set, and existence of an optimal policy is not assumed. Standing assumptions (the structure Standing): ; ; with ; concave on ; strictly decreasing on .
Added hypotheses, each disclosed in its item: Theorem 1's profit bound is conditional on (the profit ratio is meaningless otherwise); Lemma 1 assumes and strict concavity, and restricts monotonicity to states of positive probability (the printed version is false without these). Lemma 2 and the combination step are stated for every nonnegative , as printed. Identities (11), (12) and the identity are stated for every stationary policy, since their derivations use no optimality.
The objectives are the closed forms above, not free functions constrained by hypotheses; ratios are cross-multiplied so that no objective is divided by a possibly zero quantity; is built into the definitions so that and never divide by zero for ; the derivative in Lemma 2 is asserted with HasDerivAt, not deriv. Every constant (, , , ) appears as stated.
Needed beyond Mathlib's finite sums and products, Nat.descFactorial, ConcaveOn and HasDerivAt: nothing. Theorem 2 (the 95.5% guarantee for two units and linear demand), its Lemmas 5–6, the tightness example of §3.2 and the numerical experiments are out of scope. Proofs of any milestone, and alternative proofs of the bound on , are welcome.
A norm measures the size of a vector. The triangle inequality says that adding two vectors cannot increase their size beyond the sum of their sizes. The Hlawka constant problem asks for a quantitative comparison between the deficit in a three-vector triangle inequality and the sum of the deficits in the three two-vector inequalities. For operator norms, the comparison constant must work in every matrix dimension. Audenaert and Kittaneh state this question in Section 8.2, Problem 7 of Problems and Conjectures in Matrix and Operator Inequalities.
This mission concerns the diagonal, or commuting, case. For a complex diagonal matrix, its Schatten p-norm equals the coordinate p-norm of its diagonal. An exact answer in this setting identifies a concrete extremal family while preserving the requirement that the constant work in every finite dimension. It does not settle the sharp constant for arbitrary noncommuting matrices.
The foundation mission formalizes the cyclic formula for real exponents at least 256. The accepted cutoff-32 theorem, recorded on 16 October 2026, lowers that threshold. The present source is Yuxuan Xu's AI-assisted research preprint, which supplies a computer-assisted argument extending the formula to all real exponents at least 21. The preprint has not undergone independent analytic review. Its new interval has numerical verification reports but no Lean proof.
For a real exponent p greater than one and a finite complex vector x, define the coordinate p-norm by
For three vectors x, y, and z in the same dimension, set
The quantity S minus T is the triple deficit. The quantity G is the sum of the three pair deficits and is nonnegative by the triangle inequality. A real number C is a uniform Hlawka constant when
for all triples and all finite complex dimensions. No equal-norm or nonzero-vector restriction is part of this property.
The candidate sharp constant is specified by an explicit scalar formula. For a real parameter t in the closed interval from one half to two, let
The ratio comes from the cyclic triple (-t,1,1), (1,-t,1), and (1,1,-t). In the exponent range of the mission its denominator is positive, and continuity makes the supremum an attained maximum. The mission imports the campaign's existing definitions of these quantities.
The goal is Theorem 1.1 of the source preprint, in the campaign's exact statement format:
Here the minimum notation includes both admissibility and leastness; existence of an admissible constant is part of the conclusion. The theorem does not assume that certificate validation, localization, or convexity already holds. It does not assert that 21 is the smallest possible exponent threshold.
Four supporting targets follow the source's two finite windows. Equation (7) and Table 1 give, on each full real interval, the scalar inequalities
Window I is [21,26], with c=273/625 and q=1011/2500. Window II is [26,32], with c=443/1000 and q=197/500. Two further targets are the unconditional real three-dimensional Hlawka inequalities on these respective windows, as concluded in Section 7 of the source. The previously proved tail for p at least 32 is included as a referenced theorem, preserving its published identity and attribution.
The proposed result would extend the known formalized range of the exact diagonal constant from p at least 32 to p at least 21. It would give one constant simultaneously for all complex dimensions and for all real exponents in that range, rather than separate statements at selected integer exponents. The cyclic witnesses also explain the obstruction to decreasing the constant itself.
Formalizing this source means closing the gap between its analytic argument and its finite computations. The release replay report records exact rational linear-dual replay and directed interval checks. Those reports support the paper's computer-assisted claim; they are not kernel-checked proofs of the mission's open statements. A completed mission must establish those statements in the platform's ordinary proof system.
The least constant is defined through a special three-dimensional family, but admissibility quantifies over arbitrary triples in arbitrary dimensions. Unequal singleton norms and degenerate triples are included. Arguments that verify only the cyclic family establish a lower bound and leave the main admissibility assertion unresolved.
The source also requires inequalities uniform in a continuously varying real exponent. Pointwise numerical optimization and dense sampling cannot establish such interval statements. Its localized convexity estimates retain norm bounds and linear coordinate-sum constraints; each retained constraint must genuinely follow from the preceding localization argument, and the averaging domain must remain convex. In particular, retaining a norm-sum equality as if it defined a convex domain would not justify the required averaging step. These issues are part of the formalization target, not additional assumptions supplied to solvers.
The environment is Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474, using Lean v4.33.1. The goal uses Fin n → ℂ, real p, the existing lpNorm, cyclicConstant, and HasHlawkaConstant, and IsLeast over real constants. Natural-number dimensions include zero. In dimension zero all coordinate norms vanish, so the inequality is harmless; triples containing zero vectors remain included in positive dimensions. All quantities must retain their foundation definitions.
The four new milestone declarations use the same scalar and coordinate definitions, including the existing scalarEnvelope. They introduce no replacement norm and no axiom saying that an external Python execution is correct. The source package contains exact certificates, two arithmetic implementations, and explicit remainder estimates for its rational interval backend. Those implementations share the mathematical model and are not independent end-to-end proofs. Independent analytic review remains pending.
Contributions may reuse the existing dimension reduction, complex transfer, cyclic sharpness, and cutoff-32 results when their hypotheses match the target range. Formalization of the new scalar bounds, exact linear-dual implications, interval arithmetic soundness, and real three-dimensional admissibility is welcome. Proof details and the proposed dependency order are available in the source paper and the milestone descriptions. The declarations uploaded with this proposal are statements to prove, with the standard by sorry placeholders; compiling them checks well-formedness only.
A tournament is a directed graph in which every two distinct vertices are joined by exactly one arc — the model of a round-robin competition, and the setting of Ramsey theory's oldest questions.
In 1982 Sands, Sauer and Woodrow asked: if the arcs of a tournament are coloured with two colours, must some vertex be reachable from every other vertex along a monochromatic path, one whose arcs all carry the same colour? They answered yes [SSW82, Corollary 2, p. 273], through a theorem on arbitrary digraphs [SSW82, Theorem 1, pp. 271–273]. That theorem is also the two-colour case of kernel theory: kernels are independent dominating sets, they exist in digraphs whose arcs split into two transitive classes, and the stable-marriage theorem is a special case [Ch26, §1].
The tournament statement is the settled case of a question of Erdős that remains open: with three colours, must either a rainbow directed triangle occur, or a vertex reach every other vertex monochromatically [SSW82, PROBLEM, p. 275]? The platform already carries that open problem as the mission "Monochromatic reachability or rainbow triangles" (OPG1808.root_problem). This mission is the two-colour theory beside it, not a duplicate: it collects the results that are known and that any attack on the three-colour question builds on.
Timeline. Sands–Sauer–Woodrow (1982) prove Theorem 1, deduce the two-colour tournament statement, exhibit a three-coloured tournament with no vertex reaching all others, and ask whether three colours force a rainbow triangle or such a vertex [SSW82]. Shen Minggang (1988) proves the theorem for any number of colours when no triangle carries three distinct colours [Mi88]. Galeana-Sánchez and Rojas-Monroy (2005) give a six-vertex four-coloured tournament with neither, so three colours is the last case of the rainbow formulation [GR05]. Bousquet, Lochet and Thomassé (2017) show that a k-coloured tournament has a dominating set of size built from monochromatic paths — bounded, but not the single vertex of the two-colour case [BLT17]. Chancelier (2026) gives the first machine-checked proof of the general theorem, in Rocq, and records that no Lean formalization exists [Ch26].
Fix a vertex type . A digraph is a relation , written ; an arc colouring assigns each ordered pair a colour in ; a colouring uses at most two colours when every arc has colour or colour . A tournament is a loopless digraph in which every two distinct vertices are joined by exactly one arc.
A monochromatic path from to has distinct vertices, consecutive ones joined by an arc, all those arcs of one colour; write when one exists, and say that monochromatically reaches . A set is monochromatically independent when no two distinct members are connected by a monochromatic path in either direction — this is not graph independence: in a tournament a single arc joins any two vertices, so such a set has at most one element. A digraph has no monochromatic infinite outward path when no injective has all arcs of one colour.
a tournament on a nonempty finite vertex type, its arcs coloured with at most two colours:
any digraph on any vertex type, arcs coloured with at most two colours, with no monochromatic infinite outward path:
The goal in the orientation of the platform's existing definition, the distinguished vertex reaching the others:
a tournament whose arcs carry three colours and whose vertices are partitioned into blocks, two vertices of different blocks always joined by a red arc and two of the same block by a blue or a green arc; then some vertex is monochromatically reached by every other.
The result. The goal settles the two-colour case of Erdős's question in the sharp form that one vertex suffices, and it is the base of the known theory: the paper's own block-coloured three-colour theorem is proved from it by iteration, and the kernel and stable-matching corollaries of the general theorem make it standard digraph theory. Without it the three-colour question has no settled case to compare against.
Formalizing it. No Lean formalization of these statements is recorded, for the corollary or for the general theorem [Ch26]; the machine-checked development that exists is in Rocq, for the general theorem, and is the first for the infinite case. This mission produces, in Lean, a classical theorem the platform does not have, together with the definitions it rests on: monochromatic reachability and monochromatic independence over an arbitrary vertex type. Status is stated per target: the goal is a theorem of the source paper, not an open question; the three-colour problem beside it remains open.
The first idea — take a longest monochromatic path and read off its end — does not close the argument. It gives monochromatic reachability only for the vertices on the path; for a vertex outside it, one knows only that the arcs from the path to that vertex cannot continue the path's colour, which yields no path back to the path's end. The source instead takes a maximal element, under a relation mixing the two colours, of a family of monochromatically independent sets — when every has , or a blue path to some with no red path back — and shows by a minimal-counterexample argument on red reachability that a maximal element is the required set. Over an arbitrary vertex type the family needs Zorn's lemma, and the no-infinite-outward-path hypothesis, not finiteness, is what bounds the argument. A second trap is definitional: because independence here is monochromatic, the tournament case collapses to one vertex; a formalization using graph independence would state a different and false theorem.
opg1808_colored_tournaments: Digraph V := V → V → Prop, ArcColoring V := V → V → Fin 3, IsTournament, and MonochromaticallyReaches, the reflexive-transitive closure of one colour's arcs. A new definition supplies monochromatic independence; prose and statements use the same notation.IsTournament. For the general digraph target loops change nothing, as the source's paths have distinct vertices.MonochromaticallyReaches uses walks; the two agree for reachability, and independence is stated through walks, so no distinctness hypothesis is needed.[Fintype V] [Nonempty V]; nonemptiness is required, the target being false on an empty vertex type. The general target is stated on an arbitrary type, and its hypothesis is vacuous in the finite case, which is the entry point for the goal.IsMonochromaticSource is the reversed orientation of the goal; the goal follows the source paper, which orients paths towards the distinguished vertex.Needed: the reused module, a definition of monochromatic independence, reachability lemmas for two colour classes, and for the general target Zorn's lemma and infinite outward paths. The reachability and independence layer is reusable by any later mission on coloured digraphs, including the three-colour problem beside this one. Contributions to any target are welcome.
Establish a separation exponent of at least between block sensitivity and sensitivity of total Boolean functions.
For every and integer , construct with and .
A multiple-life contract has payments depending on the survival of more than one individual. A joint-life pension might stop at the first death, while a last-survivor annuity continues until both lives have died. A retirement pension may continue in a smaller amount to a surviving spouse, and a policy may instead pay one capital sum on the first or second death. These arrangements arise in pension schemes, life insurance and the valuation of dependent beneficiaries. They have different claim events, beneficiaries and settlement dates. The distinction matters in actual valuation, especially when both deaths occur between scheduled pension dates.
The basic mathematical objects are laid out in Promislow's Fundamentals of Actuarial Mathematics, third edition (2015, Chapter 10), and Dickson, Hardy and Waters' Actuarial Mathematics for Life Contingent Risks, third edition (2020, Chapter 10). Both discuss joint and last-survivor states. The latter also treats dependent future lifetimes and common shocks. The mission develops event-consistent formulas from a shared joint mortality law, rather than selecting unrelated survival probabilities for different contract components.
Let two future lifetimes be represented by death-time states and on a finite grid with right-censoring horizon . For , state means the first life dies in the interval after anniversary and its death benefit is payable at tick under the annual settlement convention. The terminal state means that this death has not been observed before the horizon. The same convention applies to the second life. More finely spaced ticks can represent payment and death dates within a year, so ordering is retained when the two deaths fall in different subannual intervals.
The joint probability mass function is , with and . It determines both one-life margins and their dependence. In particular, the probability that both lives are alive at tick is . Products of the two marginal survival probabilities are valid only under an explicit independence assumption.
At a scheduled payment anniversary there are four disjoint in-force states: both alive, member only, spouse only and neither alive. The joint-life status is the both-alive state. The last-survivor status consists of all states except neither alive. The reversionary spouse status is specifically member dead and spouse alive. A reversionary pension starts once member death makes the spouse entitled and pays only when the spouse is alive at the relevant instalment date. This is contractually distinct from an unqualified joint-and-survivor pension, whose original member and survivor amounts may follow a different schedule.
Write for a discount factor taking a payment at tick to commencement, and for its gross benefit amount. A member pension may pay while the member is alive and when the member is dead but the spouse remains alive. The ratio is the spouse continuation factor. Unless stated otherwise, the status is tested at each scheduled payment date, so a spouse who dies before the first eligible instalment receives no instalment. Death lump sums use the tick immediately after their death-year state and are distinct from these scheduled pension payments.
The first group constructs the joint law, marginal survivals and four exclusive occupation states. Their probability sums and event identities must agree without assuming independent lives. Strict order events and are accompanied by the tie event ; both terminal states are right-censored and must not cause a fictitious death claim. Equal grid times are treated as genuine ties in the grid model. Physical simultaneous death in continuous time requires a separate law assigning it positive mass.
The second group gives realised annuity cashflows and expected present values for joint-life, last-survivor, member-only and reversionary spouse statuses. A key identity for identical payment dates and discounting is
The first term values any surviving life, and the second values the spouse-only reversion. These identities are valid under general dependence because all terms come from the same joint distribution. For a member pension with a separately contractual spouse continuation of , its expected value is
This formula presumes the member payment and spouse payment are evaluated at the same dates with no overlapping guarantee or independent payment entitlement. Guarantee cashflows require separate contractual events.
The third group models a unit claim on the first death, a unit claim on the second death, the member dying first, the spouse dying first and simultaneous-grid death. It also models a later death of the survivor and pure endowments contingent on joint or last-survivor survival. Payment at death and payment on a pension anniversary can differ even when the same person eventually receives a benefit. Both deaths within a year are represented with a sufficiently fine tick grid; annual year-end states alone do not identify their physical order.
The capstone values a combined pension and assurance from the realised cashflow across all death-time pairs. It then reconciles the expected value independently against single-life, reversionary and last-survivor annuity factors, together with the disjoint first- and second-death assurance values. The event partition is incorporated in the total cashflow rather than appended as an unrelated identity.
The identities provide actuarially auditable bridges between benefits administered by member and spouse status and factors calculated by conventional life-contingency methods. In Dickson, Hardy and Waters (2020, Chapter 11), pension mathematics supplies further context. They can be used to check spouse continuation calculations in defined benefit pension administration, premium valuations of first- and second-death assurances, and mortality stress tests where lives in a household may be dependent. A dependent joint law can change the joint annuity and first-death insurance values while preserving each single-life margin.
The formalisation keeps payment timing, benefit entitlement, event order and valuation date visible in the mathematics. In the published sources the classical factor relations are known results, while the present finite-grid cashflow definitions and their combined capstone are original derived formulations. Each proposed theorem remains an open formal target until independently verified by Prove2Me's authoritative remote Lean compiler and, separately, proved.
Marginal survivals do not determine joint survival or within-year death order. A spouse may become entitled before the first payable instalment, and may die between those events. Death settlement, grid ties and terminal censoring therefore require careful treatment. The capstone reconciles expected realised cashflows with independently calculated factors, preserving the same joint law, dates and entitlement rules in both valuations.
The Lean kernel uses finite double sums over one right-censored joint law. Due, arrears, subannual, deferred and guaranteed member/spouse cashflows are defined. Death timing is represented on an integer grid; periods can be made subannual by changing the tick size. Scheduled pension payments are due at their specified ticks. Lump sums are settled at the following death tick. Discount factors and benefit amounts are parameterised as schedules; no particular flat interest rate is built into the definitions.
In the guarantee kernel, is an absolute expiry tick and starts the payment window. Guaranteed member payments do not require survival to : they model an already vested obligation, not a pension conditional on reaching retirement. A guarantee lasting periods from would expire at and require a separate retirement-eligibility condition. UK defined benefit death-in-deferment and dependant entitlements are scheme-specific and outside this kernel.
The main decomposition identities do not need independence, and explicit independent/dependent finite counterexamples are staged for remote theorem proofs. Equal-tick ties are explicit. A smooth continuous-time law, arbitrary within-tick death times, integrals for immediate death settlement, changing spouse eligibility and other pension guarantee arrangements require further declarations and remote verification before the complete mission can be released. The finite model does not imply those continuous-time results. Annuity-certain or single-life results from other unpublished owner Drafts are not assumed to be importable.
Formal contributors must preserve the same probability law and the same discount and settlement conventions across all components of any identity. A vacuous statement established by assuming its intended conclusion, using inconsistent marginals or suppressing the tie event does not meet the mission's mathematical contract.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, Chapter 10, Sections 10.2–10.8, publisher-linked contents.
D. C. M. Dickson, M. R. Hardy and H. R. Waters, Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, 2020, Chapter 10, book DOI.