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?
Round-Robin is the simplest procedure for dividing indivisible goods: agents take turns, in a fixed cyclic order, each picking a favourite among the goods still available. When agents have additive valuations and pick truthfully, the resulting allocation is envy-free up to one good (EF1): no agent prefers another agent's bundle once a single good is removed from it. The procedure is used in practice (course allocation, sports drafts, the division of estates) and is the standard baseline in fair division.
The guarantee assumes truthful picking. Round-Robin is not truthful: an agent can gain by delaying a good that nobody else wants. Viewing the reported rankings as strategies turns the mechanism into a game, and two questions follow: does the game have (approximate) pure Nash equilibria, and are the allocations at equilibrium still fair with respect to the agents' true valuations? Round-Robin is the only known fair-division algorithm for more than two agents whose game is known to have equilibria (Aziz, Goldberg and Walsh, ADT 2017), and for additive valuations its exact pure Nash equilibria give EF1 allocations with respect to the true valuations (Amanatidis et al., WINE 2021). G. Amanatidis, G. Birmpas, P. Lazos, S. Leonardi and R. Reiffenhäuser (arXiv:2301.13652, Mathematics of Operations Research 2025) extend both questions beyond additive agents. This mission formalizes their fairness result for subadditive cancelable valuations, Theorem 4.5.
There are agents and a finite set of goods. Agent has a valuation with that is non-decreasing. The marginal value of with respect to is . A valuation is
Additive, budget-additive () and unit-demand () valuations are subadditive and cancelable.
Each agent reports a preference ranking , a total order on . Round-Robin (Mechanism 1) runs rounds; in each round agents in turn receive the -best good still available. It returns bundles ; the mechanism sees only the rankings. Write for the profile in which agent replaces her ranking by .
For and subadditive cancelable valuations , every -approximate PNE of Round-Robin satisfies: for all with there is with
Fix agents , let be a strict truthful ranking of (it puts before whenever ), let be the good receives in round of , list by allocation time in that run, and split into and , , each renamed by Algorithm 3 (p. 11).
The proof also uses three results of the same paper that are formalized in sibling missions of this series: Lemma 3.3 (p. 8, a pointwise-domination lemma for cancelable valuations), Lemma 4.6 and Lemma 4.7 (p. 19, counting the goods that the deviation can displace), and the parity split of (p. 20). They are not restated here.
The result. Theorem 4.5 says that strategic reporting costs Round-Robin at most a factor in fairness, for a class that contains the additive, budget-additive and unit-demand valuations; at exact equilibria () the allocation is -EF1. Companion results of the paper give the existence of exact equilibria for cancelable valuations (Theorem 3.2), so the guarantee is not vacuous, and show that for two additive agents the right factor is and is tight (Theorem 4.3). Since additive valuations are subadditive and cancelable, the best possible factor for this class lies between and .
Formalizing it. The theorem is proved on paper; no machine-checked version exists. A formal proof requires making precise the coupling of two runs of Round-Robin — the equilibrium run and the run where one agent deviates — which the paper handles in prose. In the course of this formalization a step of the paper's argument was found to need repair (see Formalization scope), so a complete formal proof would also certify the statement itself.
The deviation of agent changes what every other agent receives, so (from the equilibrium run) and (from the deviated run) live in different executions and may share goods. Comparing them good by good requires controlling which goods were still available to at each of her turns in the deviated run; this is the content of Lemmas 4.6–4.7 and the parity split. The tempting step from the marginal comparison (2) to a comparison of singleton values, , via cancelability, fails when is one of : then its marginal value is and (2) carries no information about its singleton value. Algorithm 3 places such shared goods last, where this happens. A two-agent instance with additive valuations and eight goods exhibits the failure. The set inequality of milestone 2 has to be reached another way.
Agents are Fin n with n ≥ 1; goods a finite type M with decidable equality; a valuation is a real function on Finset M, required to be normalized and non-decreasing. Rankings are duplicate-free lists containing every good, most preferred first; Round-Robin is defined step by step (step belongs to agent ), and agents' bundles collect the picks of their steps among the first . The paper's standing assumption (p. 7, justified there by adding dummy goods) is a hypothesis of every theorem; the reduction is not formalized. The hypotheses are those of the page. Algorithm 3 is encoded relationally (every tie-breaking is admitted), and strict truthful rankings admit every order among goods of equal singleton value; both choices make the milestones at least as strong as the paper's lexicographic versions. Milestones 1 and 2 do not assume the equilibrium (the paper does not use it there).
The formal statements rule out the trivializing readings: deviations in the equilibrium hypothesis range over total orders only (not arbitrary lists), is excluded, EF1 is measured with the true valuations and not with the reports, and both subadditivity and cancelability are required of every agent.
On milestone 2. The page derives it through the intermediate claim , which is false in general (see Difficulty); the intermediate claim is therefore not posed. The set inequality itself held in every instance tested (400 000 random two-agent instances with additive and budget-additive valuations, and 26 000 random instances with two or three agents and additive, budget-additive, unit-demand and square-root-of-additive valuations), but the page's derivation of it is incomplete. Theorem 4.5 is not known to be affected.
Needed infrastructure: the Round-Robin execution (allocation sets after each step, the picks, bundles), lemmas relating two runs that differ in one ranking, and Lemma 2.2 (cancelable functions cancel any common disjoint set). The Round-Robin layer is shared with the sibling missions on Theorems 3.2, 3.7 and 4.4 and reusable for any picking-sequence mechanism. Contributions of any of these lemmas, of a repaired proof of milestone 2, or of a counterexample to it are welcome.
A retailer often knows more about her own demand than the supplier who must produce for her. In a decentralized supply chain the supplier sets a production quantity before demand is realized, and an under-informed supplier produces too little or too much. The retailer can shape what the supplier believes by committing in advance to a disclosure policy, a rule that maps what she knows to messages she sends. This is the Bayesian persuasion or information design framework of Kamenica and Gentzkow (2011), applied by Candogan and Gurkan (2024) to a newsvendor supplier.
The natural expectation is that the retailer either tells the supplier everything or nothing. The paper shows the answer depends on the supplier's critical ratio, and that it can be non-monotone. For nested demand supports (the setting of the first missions in this series) partial disclosure appears for low critical ratios. This mission formalizes the paper's §4 extension to supports that overlap without being nested. There, under an explicit condition on the supports, the optimal policy moves from partial disclosure to no disclosure to full disclosure as the critical ratio rises.
The state is with prior . In state the retailer's demand is uniform on . The supports intersect:
Write , , ; all three are positive.
The supplier holds a belief and chooses a quantity that minimizes the newsvendor cost (2),
where is the critical ratio of the shortage cost and the excess cost . A best-response profile assigns an optimal quantity to every belief .
A policy consists of a finite message space and probabilities . After message the supplier's belief is the Bayes posterior (1),
The retailer orders the realized demand and bears only the shortage. Her design problem (3) minimizes, over policies and best-response profiles , the expected shortage
where is the induced posterior. Full disclosure reveals . No disclosure sends one uninformative message. The function
of (B.1) is the retailer's cost when the posterior is , and denotes its lower convex envelope on .
Assume and . Let and . Then:
where has two messages, sends in state with probability 1, and sends in state with probability .
The result. With nested supports, more information can only hurt the retailer at low critical ratios. With overlapping supports, Proposition 3 shows the regimes of full, no and partial disclosure can occur in a different order. It also gives a sufficient condition on the shape of the supports for that pattern. Together with the paper's Theorem 1 (nested) and Theorem 3 (disjoint), it gives the optimal policy for the main configurations of two uniform supports. The explicit thresholds tell a practitioner which disclosure regime applies from four interval endpoints and a cost ratio.
Formalizing it. The paper's argument is in its Online Appendix (C.1, pp. 30–35). It cites Kamenica–Gentzkow for the value of the design problem and proves the envelope lemma through second-derivative sign computations. None of this is machine-checked. A complete development yields a formal concavification theorem for a finite-state persuasion problem over all finite message spaces, which is reusable well beyond this paper. It also yields a checked closed form for the newsvendor quantile under a two-uniform mixture. The goal and every milestone are open on the platform; only the published convex-envelope definition is reused.
The obvious argument compares full disclosure, no disclosure and one candidate partial policy, and picks the best of the three. That proves nothing, because optimality is claimed against every policy on every finite message space. The reduction to the convex envelope (milestone 2) is what makes the comparison finite, and it is itself a theorem about splitting a prior into posteriors.
The envelope of is the second obstacle. is piecewise rational in , with two regime boundaries that move with . Its curvature changes sign across the boundaries, and the sign of its second derivative depends on relative to . Verifying that the claimed is convex at the kink requires a one-sided slope inequality whose sign rests on the hypotheses on . The equivalence of milestone 3 is where those hypotheses enter.
All objects live in the namespace SCInfoDesign.Intersecting. States are Fin 2; is the state with demand on , and beliefs are always . The uniform expectation is . Policies are stochastic maps from Fin 2 to any finite type; the paper does not bound the message space, and finite spaces are the standard Kamenica–Gentzkow setting. The supplier's cost is normalized by , which leaves its minimizers unchanged, so is the only cost parameter. A message of probability zero carries the default posterior and weight . No disclosure is the one-message policy. uses the largest optimal quantity, which is the unique one here. The envelope is the published BiconvexProg.BranchBound.convexEnvelope on .
Standing assumptions, added and disclosed because the paper uses them implicitly: ; (nonnegative demand, so the constraint never binds); . Nondegeneracy follows from the support ordering. Two printed slips are corrected in the statements and quoted as printed in the milestones: for in the display, and the label for on p. 32. The overlapping indicators of (C.2) at are read piecewise.
Trivializing encodings are excluded. Optimality is over all finite policies and all best-response profiles, not over the three named policies. The supplier's response is an argmin of (2), never the closed form (6), which is a milestone. Each named policy is also asserted to be a policy.
Contributions are welcome on any milestone. The concavification theorem (milestone 2) and the uniform-mixture newsvendor quantile (milestone 1) are the reusable pieces. Proposition 5 (shift case) and the second-derivative display (C.3) are not posed here.
A retailer usually knows more about her future demand than the supplier who has to produce for her. If the supplier must commit to a production quantity before the order arrives, the retailer bears the cost of every unit he fails to produce. She cannot pay him or contract on quantities, but she can decide how much of her demand information to share, and she can commit to that disclosure rule in advance. Which information should she share?
Candogan and Gurkan (Management Science, 2024; preprint SSRN 4378997) answer this question in a two-state model with uniform demand, using the Bayesian persuasion framework of Kamenica and Gentzkow (2011). Their main text treats nested demand supports. This mission formalizes their extension to disjoint supports, where the high-demand state's support lies entirely above the low-demand state's (Theorem 3). It is the fourth of four missions on the paper; the others cover nested supports (Theorem 1), the value of information (Theorem 2) and intersecting supports (Proposition 3).
There are two states with prior . In state the retailer's demand is with and . Here the supports are disjoint, , so state is the high-demand state.
A disclosure policy is a finite message space and, for each state , a probability distribution on . The retailer commits to , observes , and sends a message . Message has probability , and the supplier's posterior is given by Bayes' rule (1):
The supplier has unit shortage cost and unit excess cost , with critical ratio . At belief he solves the newsvendor problem (2), here normalized by :
A best-response profile assigns to every belief an optimal quantity ; the set of them is .
The retailer's cost at belief and quantity is her expected shortage . Her design problem (3) is
A policy is optimal if, paired with some best-response profile, it attains this minimum against every finite-message policy and every best-response profile. Full disclosure sends exactly in state ; no disclosure sends one message. The retailer's cost function (B.1) is , where is the largest optimal quantity at , and is its lower convex envelope on , the greatest convex function on below .
Let . For every :
where has messages with and (8). The paper writes "there exists " and then gives its value; the goal states the value.
The result shows that the shape of the optimal disclosure policy is decided by the relative width of the two supports and, below a threshold, by the prior alone: when the high-demand support is at least half as wide as the low-demand one, the retailer reveals everything, whatever the supplier's cost structure. Otherwise the critical ratio enters only through , and the optimal partial policy pools the high state with part of the low state so that the supplier's posterior lands exactly at . Together with the nested and intersecting cases, it shows that the non-monotone dependence of informativeness on found under nested supports is not universal.
The paper proves the result in its Online Appendix (App. C.2, pp. 37–40), by citation of Kamenica–Gentzkow for the reduction to a convex envelope and by a case analysis for the envelope. To our knowledge none of it is machine-checked. This mission produces a formal model of persuasion with a newsvendor receiver, a formal proof of the concavification step for finite message spaces, and the envelope computation. Formalization also pins down a boundary case the printed proof leaves implicit (see Formalization scope).
The reduction to the envelope is cited from Kamenica and Gentzkow in the paper, so it has to be established from scratch for this model, with its joint choice of policy and best response and its finite message spaces. The envelope itself requires handling a function that is concave on , convex on and discontinuous at , where it jumps down. The obvious argument — treat as continuous and compare one-sided derivatives — fails at that point, and the jump is what makes the chord to admissible.
The newsvendor step is not just the critical-fractile formula: at the mixture c.d.f. is flat at level on , so the supplier's best response is not unique there.
The Lean development lives in the namespace SCInfoDesign.Disjoint. Conventions:
Fin 2, beliefs are , and uniform expectations are interval integrals divided by the interval length.The formalization is not trivial by construction: the supplier's response is an argmin of (2), not the closed form of Proposition 6, and optimality quantifies over every finite policy with every best response, not over the three named policies.
Infrastructure needed: interval integrals of piecewise-linear functions, the convex envelope (the published BiconvexProg.BranchBound.convexEnvelope), and a Jensen/splitting argument for Bayes-plausible posteriors. The concavification step and the newsvendor argmin for uniform mixtures are reusable beyond this mission, by the three sibling missions in particular. Proofs of any milestone are welcome.
Service providers such as hospitals or retail stores each fit a predictive model on their own data, and many of them have few observations. The models of different providers are usually similar but not identical: most coefficients agree, while each provider deviates from the common model in a few features of its own. Multitask learning asks how data from all providers can be pooled to estimate every provider's model better than it could estimate alone, without being misled by the providers that differ.
Xu and Bastani (arXiv:2112.14233v5) model this with sparse heterogeneity: every task parameter is a shared vector plus a sparse deviation. They propose the robust multitask estimator (RMEstimator), which combines per-task least-squares estimates by a coordinatewise trimmed mean and then corrects each task by a LASSO regression centred at that shared estimate. Their main fixed-design guarantee, Proposition 5, is a high-probability bound on the estimation error of each task. The same estimator drives the paper's multitask contextual bandit algorithm (§5), whose regret analysis rests on this bound. The approach builds on transfer learning with a single proxy model (Bastani 2021) and on the robustness of the trimmed mean to corrupted samples (Lugosi and Mendelson 2021).
There are tasks. Task has observations, a fixed design matrix whose columns satisfy the normalization (equation (1)), and responses
The noise terms are mutually independent across all tasks and observations, and each is -subgaussian with mean zero: for all . Assumption 1 asks that the sample covariance matrices satisfy .
Given a trimming level and regularization levels , Algorithm 1 computes:
A coordinate is -poorly-aligned, , if fewer than a fraction of the tasks satisfy ; otherwise it is -well-aligned (Definition 2).
For every constant , every , every , every task and every , every output of Algorithm 1 with satisfies
with probability at least .
The printed Proposition 5 (p. 17) has where this statement has . The proof on pp. 41–43 ends with and combines it with (16), whose coefficient is , so it establishes the bound with . The goal is the bound the proof supports.
Proposition 5 separates two error sources: a LASSO term of order , which depends only on the task's own sample size, and a trimmed-mean term that shrinks with the number of tasks through . With the hyperparameters of Appendix A.2 it yields Theorem 1, an error of order up to logarithmic factors, against for a single task alone. The same decomposition underlies the paper's data-poor guarantee (Proposition 8) and the regret bounds of its multitask bandit algorithm.
The result is proved on paper; none of it has been machine-checked. A formal development checks the constant bookkeeping, including the factor 4 that the printed statement omits, and the use of the trimmed mean for samples that are independent but not identically distributed, which is where this paper departs from the classical i.i.d. robust-statistics results. Proposition 4 and Lemma 1 are reusable on their own: a corruption-robust concentration bound for the trimmed mean and a noise bound for fixed-design LASSO.
The obvious estimator of the shared parameter, the average of the per-task estimates, converges to the average of the , which differs from in up to coordinates, so the LASSO correction would have to undo a dense bias. The trimmed mean avoids this only on poorly-aligned coordinates, and only with high probability. The proof of Proposition 4 must control the samples that survive trimming even though they are not identically distributed and trimming biases the conditional means; that step needs a moment bound for subgaussian variables and a Hoeffding argument on a random index set. The LASSO step needs the cone inequality with a support that is not the support of , and the counting bound (6) to control its size.
Fin N, Fin d, Fin (n j); paper index is Lean i − 1. Designs are deterministic matrices; only the noise is random.HasSubgaussianMGF with variance proxy , . Independence of all noise terms is iIndepFun over the pairs .A formalization that drops Assumption 1 (making the OLS inverse a junk zero), lets the corrupted samples of Proposition 4 be independent or well-behaved, fixes a single existentially, or reads a junk minimizer from Classical.choose, does not state the paper's result.
The development needs least-squares algebra for fixed designs, a Hoeffding bound for independent bounded variables, moment bounds for subgaussian variables, and the LASSO basic inequality. Proofs of any milestone are welcome, and so are alternative arguments for Proposition 4 with better constants.
Personalized decisions — which drug to prescribe, which product to recommend, which price to quote — are made one user at a time, from user features observed on arrival, and the effect of each decision is learned only from the users it was applied to. This is the contextual (covariate) bandit. In electronic records and online platforms the feature vector is high-dimensional, often with more coordinates than there will ever be users, while the outcome is binary or count-valued, so a linear reward model is a poor fit. Wang, Wei and Yao (arXiv:1812.02962, published in Management Science, 2025) combine three ingredients: a generalized linear model (GLM) for rewards, sparsity of the parameter vectors, and the minimax concave penalty (MCP) of Zhang (2010) for estimation.
Timeline. Goldenshluger and Zeevi (2013) obtained regret for a two-armed linear bandit with low-dimensional covariates, under a margin condition, and showed it is the right order. Bastani and Bayati (2020) extended the setting to high-dimensional sparse linear rewards with the LASSO, obtaining regret. Wang, Wei and Yao (2018 preprint) treat GLM rewards with the MCP and claim , recovering the order in the high-dimensional setting.
At each time a user with covariate vector arrives; the are i.i.d. with an unknown law . The decision-maker chooses a decision , , and observes only the reward of that decision.
The reward of decision at covariate has law , where is a known base measure on , a known density, and an unknown sparse parameter: its support has at most elements. Write and , so the expected reward is . The Bernoulli–logistic model is , .
The cumulative regret compares the decisions with the oracle that knows every :
The G-MCP-Bandit algorithm has inputs . At time , with probability it explores: it plays a uniformly random decision (ε-decay random sampling). Otherwise it forms a shortlist of the decisions whose estimated mean reward, under the random-sample estimates (trained on exploration data only), is within of the best; it then plays the decision of with the largest estimated mean under the whole-sample estimates (trained on all data of ). Both estimates are computed by the 2-step weighted Lasso (2sWL): an -penalized maximum likelihood fit with weights , then a refit whose weights are the MCP derivatives at the first fit, both over the ball , with the anytime schedules and .
The paper assumes A.1 (bounded covariates, rewards and parameters; lower-bounds the nonzero coefficients), A.2 (margin: ), A.3 (every decision is either -suboptimal everywhere or -optimal on a region of probability at least ), A.4 (a restricted eigenvalue condition with constant for samples in ) and A.5 (smoothness and convexity of with derivative bounds ).
For every there are constants and , independent of , such that with , , , for every ,
The goal keeps every explicit coefficient of the page and leaves the constants the paper calls "independent of " existential.
In the order the proof of Theorem 1 (pp. ec5–ec8) uses them:
Theorem 1 says that, under the stated assumptions, learning with high-dimensional GLM rewards costs regret logarithmic in the horizon, the order known to be unavoidable already for low-dimensional linear bandits. It improves the of the LASSO bandit and shows how a non-convex penalty, computed by two convex weighted-Lasso solves, can be analysed under the non-i.i.d. sampling that a bandit induces. Propositions 4 and 6 are estimation results of independent interest: tail bounds for an MCP estimator trained on random and on adaptively collected samples.
The result is proved on paper; it is not formalized anywhere. The mission produces a machine-checked statement of the full algorithm and its regret, and the milestones isolate reusable facts: an exploration-count bound for ε-decay sampling, a Lipschitz bound for GLM means, and the estimator tail bounds. Alternative arguments and sharper constants are welcome as separate theorems.
The whole-sample data are not i.i.d.: which samples decision receives depends on the past estimates. Standard high-dimensional estimation results (restricted eigenvalue arguments for the Lasso or MCP) assume i.i.d. designs, and so does the analysis of the oracle estimator. The obvious argument — apply the i.i.d. result to — fails at this step. The paper instead extracts an i.i.d. subsample, the exploration samples in , and controls the rest through a martingale count. A second difficulty is that the MCP objective is non-convex; the 2sWL estimate must be shown to coincide with the oracle estimator, which requires a minimum signal strength and a sufficiently large .
Covariates are Fin d → ℝ with , decisions are Fin K with (the paper's decision is k.val + 1), times are . Norms are explicit sums. Pinned readings, all disclosed in the items:
ContDiff ℝ ∞.Trivializing formalizations are ruled out: the estimates are minimizers of the stated objective over (not arbitrary functions), the selection and tie-breaking rules are measurable (otherwise every expectation would be the junk value ), and every existential constant comes before the probability space, the rules and , so that and cannot depend on the horizon. The trailing and the explicit lower bound on are not formalized.
A complete development needs a measurable argmin selection over a compact ball, Chernoff bounds for sums of independent non-identical Bernoulli variables, differentiation under the integral for GLM means, a restricted-eigenvalue oracle inequality for the weighted Lasso with GLM loss, and a martingale concentration bound. The first three are reusable beyond this mission. Contributions on any milestone are welcome.
Firms that hold purchase-history data can treat past customers and a rival's customers differently. The economics of behavior-based pricing (BBP), charging different prices to the two groups, is well developed: in a symmetric duopoly, poaching the rival's customers with discounts intensifies competition and usually lowers profits (Fudenberg and Tirole 2000; Villas-Boas 1999). The same data can also target information. A firm launching a new product of uncertain quality can disclose that quality (free samples, demonstrations, trials) at a cost per customer reached, and it may disclose to one segment and not the other. This is behavior-based quality disclosure (BBD).
Zhang and Li (Management Science 71(10), 2025) combine costly voluntary disclosure in the style of Jovanovic (1982) with BBP in a two-period Hotelling duopoly. Their Proposition 1 answers two questions about the second period: to which segment should a firm disclose more readily, and does the option to target disclosure help or hurt profits? This mission formalizes that proposition and the displayed formulas from which it is derived.
Two firms, A at and B at , face a unit mass of consumers spread uniformly over , with unit transportation cost and a base value high enough that every consumer buys in every period. The first-period purchase splits the line at a share : A's turf consists of A's old customers, B's turf of B's.
In period 2 firm launches a product of quality ; and are independent and uniform on , and consumers do not observe them. Disclosing to the consumers in an interval of length costs , where is the unit disclosure cost. A firm discloses to a segment exactly when its quality exceeds a disclosure threshold ; consumers who see no disclosure infer and hold the belief . The updated belief is therefore if and otherwise.
In both regimes firms then set four prices: on A's turf and on B's turf. On A's turf, with beliefs , the consumers who stay with A are with , clamped to the turf; B's turf is symmetric. A second-period equilibrium is a profile of thresholds and turf price strategies such that, for every belief pair, the turf prices are a Nash equilibrium among nonnegative prices, and every threshold is a best response: disclosing is optimal above it and withholding below it. The ex ante second-period profit is A's expected revenue minus expected disclosure cost, over .
For , at the symmetric first-period share : equilibria exist under both regimes; in every BBD equilibrium
in every BBD equilibrium and for every realization , at the induced beliefs, each firm charges the rival's customers less than its own,
and for every BBD equilibrium and every uniform-disclosure equilibrium, each firm's ex ante second-period profit is strictly higher under BBD:
The goal asserts the shape of the result (an order of thresholds, of prices and of profits) and no closed form.
The result. Part (a) says that disclosure should be retention focused: a firm reveals quality to its own customers over a wider range of qualities than to the rival's. This is the opposite of the acquisition focus BBP prescribes for prices, so the two instruments built on the same data pull in different directions. Part (b) records that prices stay acquisition focused: the rival's customers get the lower price. Part (c) says that targeted disclosure raises second-period profits, in contrast with the classical finding that targeted pricing lowers them. Under uniform disclosure a single threshold over-discloses to the rival's customers and under-discloses to one's own; BBD separates the two, and the paper locates the gain in the expected disclosure cost in (5) against in (14).
Formalizing it. The paper's proofs are in an Online Appendix; the main text shows the displayed formulas only. A formal proof checks the whole chain from the clamped price games, through the best-response conditions, to the closed forms of Table 1 and the final comparison. The comparison in (c) is delicate: the profit difference is positive on all of but tends to as (about at ), so a numerical check does not settle it. The mission also gives the platform its first Hotelling duopoly, its first behavior-based pricing model and its first costly-disclosure model.
There are three nested equilibrium notions: Nash prices in each turf for every belief pair, best-response thresholds given those prices, and expectations of piecewise-defined profits over the belief support. Lemma 2's prices solve first-order conditions only in the interior; uniqueness among nonnegative prices requires ruling out the corners where one firm sells nothing on a turf. Each threshold is characterized by a best-response condition rather than an equation, so obtaining (4) or (13) requires showing that the disclosure gain is monotone in quality and crosses the cost exactly once inside . The expected profits integrate squares of linear functions of beliefs that switch at the thresholds. Finally, (c) is a sign statement about a difference of algebraic functions of with three different square roots that vanishes at ; plugging in endpoints or bounding term by term loses the sign near .
The Lean development lives in the namespace BBDisclosure.Stage2. Conventions:
A formalization in which thresholds or prices are pinned to their closed forms, or in which the equilibrium predicate is unsatisfiable, would make the goal trivial; the goal therefore quantifies over equilibria of the game itself and includes existence of an equilibrium in both regimes. "Firms'" is stated for both A and B rather than assumed by symmetry.
Needed infrastructure: piecewise-quadratic optimization on a half-line (the clamped turf games), interval integrals of piecewise polynomials, and sign analysis of algebraic expressions in , , . The turf-game analysis is reusable for any Hotelling model with behavior-based pricing. Contributions to any milestone, or to intermediate statements such as the conditional profits (3) and (12), are welcome.
Many-server queues are the basic model of call centres and hospital wards, and the Halfin–Whitt regime (the number of servers grows while the traffic intensity approaches one at rate ) is where such systems operate efficiently and with short delays. In this regime the centred and scaled queue process of a queue (general arrivals, phase-type service, servers, generally distributed patience) converges to a -dimensional diffusion, being the number of service phases (Dai, He and Tezcan, Ann. Appl. Probab. 2010). For queues the stationary distribution of the queue converges to the invariant measure of that diffusion (Dai, Dieker and Gao, Queueing Systems 2014). So is the object one would like to compute.
With exponential service the diffusion is one-dimensional and is explicit. With phase-type service it is multidimensional with a piecewise-linear drift; Dieker and Gao (Ann. Appl. Probab. 2013) proved that it is exponentially ergodic with a unique , but no closed form is known, and the characterization of multidimensional piecewise-linear diffusions was left open in Browne and Whitt (1995). Jin, Pang, Xu and Xu (arXiv:2209.07361) approximate by the invariant measure of the Euler–Maruyama discretization and give an explicit error rate in the Wasserstein-1 distance.
Fix , a patience rate , a slack , a probability vector , service rates and a sub-stochastic phase-transition matrix with and invertible. Let , , and assume the phase-type distribution has mean one, . The drift is the piecewise-linear map
Let be a matrix with for some (in the queueing model has an explicit formula in terms of the arrival variability , , , ; only the ellipticity is used). The limiting diffusion is
with a standard -dimensional Brownian motion; is the law of started at , and is a probability measure with for all .
The Euler–Maruyama chain with step is
with independent standard Gaussian ; its one-step kernel is , and denotes an invariant probability measure of it. The Wasserstein-1 distance is taken in its dual form
where is the set of with .
There is such that for every there is , depending on but not on , such that for every the chain has a unique invariant probability measure and
The constants are left unspecified, so the goal survives any improvement of them.
In the order the proof uses them:
The theorem gives a computable approximation of the stationary distribution of the diffusion limit, with an explicit rate. Combined with the convergence of the scaled queue's stationary distribution to at rate for queues (Braverman and Dai), it yields an approximation of the steady state of the queue itself, by simulating the chain for steps (Remark 2.3 of the paper). Proposition 2.1 also shows that the explicit Euler scheme does not blow up for this non-gradient, non-differentiable drift, which is not automatic: the Euler scheme of an ergodic SDE may blow up.
The result is proved in the paper; nothing here is open mathematically, though Lemma 2.2 is imported from Gurvich's regularity theory rather than proved there. To our knowledge none of it is formalized. A formalization provides the first machine-checked Wasserstein bound between the invariant measures of a multidimensional diffusion and its discretization, and on the way the Lyapunov and Harris-type ergodicity theory of Euler–Maruyama chains.
Standard error analyses of Euler schemes for invariant measures assume a gradient drift, strong dissipativity, or several bounded derivatives; none holds here. The drift is not differentiable on the hyperplane and is dissipative only in the Lyapunov sense of Dieker and Gao, so contraction-based couplings do not apply. The Stein argument instead needs second derivatives of the Stein solution that are Hölder continuous with polynomially growing constants; this is where the loss comes from, and it rests on elliptic regularity for an operator with only Lipschitz coefficients. The ergodicity of the chain must also hold with constants uniform in , which the classical Lyapunov criteria do not give directly.
EuclideanSpace ℝ (Fin d), so is the Euclidean norm; matrices act by the usual product, and .EthierKurtz.IsStandardBrownian (time ℝ≥0). The diffusion is a pathwise integral equation with continuous paths, so no Itô integral is needed. The transition function is characterized by: on every probability space, every solution from has law at time . is a hypothesis (an invariant probability measure of ), never assumed smooth or with moments.stdGaussian under ; starts at .Trivializing encodings are excluded: the existence and uniqueness of is a conclusion, not a hypothesis, and the distance is infinite rather than zero when moments fail.
A complete development needs Brownian motion with Gaussian increments, a pathwise SDE solution theory for Lipschitz drift, Itô's formula (or Dynkin's formula) for functions of additive-noise diffusions, Harris-type ergodic theorems for Feller chains and diffusions, and elliptic regularity for the Stein equation. The Harris theorems and Wasserstein machinery are reusable well beyond this mission. Contributions to any milestone, and to general infrastructure for Euler–Maruyama chains, are welcome.
Bibliographic data as in the reference list of arXiv:2209.07361v1, pp. 35–37.
In a many-server queue with servers, the Halfin–Whitt (quality-and-efficiency-driven) regime lets while the arrival rate approaches capacity at rate . In this regime the centred and scaled number of customers in each service phase of a queue (general arrivals, phase-type service, general patience) converges to a -dimensional diffusion with a piecewise-linear drift (Dai, He and Tezcan, Ann. Appl. Probab. 2010). This diffusion is exponentially ergodic with a unique invariant measure (Dieker and Gao, Ann. Appl. Probab. 2013), but for no explicit formula for is known.
Since is not explicit, its averages are estimated by simulation, for example by the time average of along one long trajectory. The second main result of Jin, Pang, Xu and Xu (arXiv:2209.07361) is a central limit theorem for these time averages. It gives the rate of convergence, for every starting point, and identifies the limiting variance through the solution of a Stein (Poisson) equation.
A model consists of , a patience rate , , a probability vector , service rates , a sub-stochastic matrix with and invertible, and a matrix . Put and . The phase distribution has mean one, , and is uniformly elliptic: for some . The drift is
and the limiting diffusion solves, for a standard Brownian motion ,
Its semigroup is and is its invariant probability measure. For bounded measurable , the empirical average is . The Stein solution is
which solves for the generator . Here is the essential supremum of .
There is such that for every bounded measurable , is differentiable, , and for every
The theorem gives the rate and the asymptotic variance of the standard ergodic-average estimator of , which yields asymptotic confidence intervals for steady-state performance measures of the queue approximated by the diffusion. The function need only be bounded and measurable, so indicator functions are included, for example the probability that the total queue exceeds a level. The same variance governs the moderate deviation principle (Theorem 1.4 of the paper), which is a planned follow-up.
The result is proved in the source paper. None of it is formalized. Formalizing it requires Lean infrastructure that does not exist yet and is reusable beyond queueing: Stein/Poisson equations for non-smooth drifts, a Bismut–Elworthy–Li formula, derivative flows of diffusions, and a continuous-time martingale CLT.
The obvious argument applies Itô's formula to the Stein solution : the time average becomes a martingale plus a boundary term, and a martingale CLT finishes the proof. That argument needs with polynomial growth of . For bounded measurable , classical regularity results for Stein equations do not apply, and the drift is not differentiable on the hyperplane , so the diffusion cannot be differentiated in its starting point directly. The central difficulty is Proposition 3.1, a gradient bound for when neither nor is differentiable.
EuclideanSpace ℝ (Fin d) with the Euclidean norm. Matrices act through Matrix.toEuclideanCLM, whose norm is the operator norm.ℝ≥0. Brownian motion is the published predicate EthierKurtz.IsStandardBrownian. The diffusion is the pathwise solution of the integral equation above, for every .Restricting to smooth or Lipschitz functions, starting in , taking or a diagonal , or dropping the differentiability of each makes the statement weaker or trivial, and none of them is the theorem.
Welcome contributions include a general Itô integral and Itô formula for additive-noise diffusions, a martingale CLT in continuous time, exponential ergodicity of this diffusion (Lemma A.1 of the paper, posed in the companion mission on the Euler–Maruyama scheme), and any of the milestones.
A retailer often knows more about her own demand than the supplier who produces for her. When the supplier must commit to a production quantity before demand is realized, what the retailer tells him shapes how much he produces, and therefore how much demand she can serve. Information design (Bayesian persuasion, Kamenica and Gentzkow, 2011) asks how a sender should commit in advance to a randomized disclosure rule to steer a receiver's action.
O. Candogan and H. Gurkan, The Value of Information Design in Supply Chain Management (SSRN 4378997; Management Science, 2024, DOI 10.1287/mnsc.2023.03004) solve this problem for a supplier facing a newsvendor problem with uniform demand. Their Theorem 1 identifies the retailer's optimal policy: full disclosure, no disclosure, or an explicit two-message partial disclosure, according to thresholds on the critical ratio. Their Theorem 2, the goal of this mission, quantifies how much the optimal policy is worth compared with the two naive policies a practitioner would use by default, and how this gain moves with the retailer's prior and the supplier's cost structure.
The state is with prior . Demand is in state and in state , with nested supports .
Supplier. At belief the supplier chooses to minimize the expected newsvendor cost
where is the critical ratio of the unit shortage cost to the total unit cost .
Retailer. The retailer learns and sends a message from a finite set according to a committed policy . Message has probability and induces the posterior . The supplier best-responds with an optimal quantity , and the retailer pays her expected shortage
Her optimal expected cost is the infimum of over all finite message sets, all policies and all best responses of the supplier.
Naive policies. Under no disclosure the supplier keeps the prior, and the retailer pays . Under full disclosure he learns , and she pays . The values of information are
Thresholds. , , and .
In the partial-disclosure regime , with :
For fixed the regime is ; for fixed it is .
The result. Theorem 2 tells a retailer when designing information is worth the effort. Against no disclosure, the gain is largest at the intermediate prior and shrinks as shortages become relatively more expensive for the supplier. Against full disclosure, the gain shrinks as the prior probability of the wide-support state grows and peaks at the intermediate critical ratio . These comparative statics are what the paper's managerial discussion (pp. 13–14, Figures 4–5) rests on.
Formalizing it. The result is proved in the paper (Online Appendix B, pp. 24–30), by citing Kamenica–Gentzkow for the reduction to the convex envelope and by explicit calculus. No part of it is machine-checked. A complete formalization would contain a self-contained proof of the concavification reduction for a two-state sender–receiver game with finite message sets, the newsvendor quantile of a uniform mixture, and an exact convex-envelope computation, each reusable beyond this paper.
The derivative formulas are routine once and are known in closed form. The work lies upstream. The optimal cost is an infimum over all finite policies and all best responses, and turning it into requires the Kamenica–Gentzkow argument: Jensen's inequality over Bayes-plausible posterior distributions for the lower bound, and a two-point splitting for attainment. itself is a supremum over all convex minorants, and identifying it requires showing that is convex below and concave above, and that the chord from to is supporting. Finally, is defined through an argmin, so its closed form needs the uniqueness of the newsvendor quantile. A solver who differentiates the closed forms of p. 28 directly proves only the last step.
All objects live in the namespace SCInfoDesign.ValueInfo. The supports are bundled in a structure Params. The critical ratio is an explicit argument of every object, because Theorem 2 varies it.
Conventions.
Fin n).BiconvexProg.BranchBound.convexEnvelope on .Added hypotheses. These are the paper's implicit standing assumptions: and , nonnegative demand (, ), and . The goal and the derivative displays also assume : otherwise the regime is empty and is .
Ruled out. The optimal cost is not the cost of the paper's policy , and the supplier's response is an argmin of (2), not the closed form of Proposition 1. Theorem 2 is therefore a statement about the game, not about a formula.
Infrastructure. A complete development needs the concavification theorem for finite policies (milestone 2, reusable for every two-state persuasion model), the uniform-mixture newsvendor quantile (milestone 1), the exact computation of a convex envelope (milestone 4) and one-variable calculus. Contributions of any milestone, of general lemmas on convex envelopes on an interval, or of the Kamenica–Gentzkow reduction in general form are welcome. The proofs of the paper are in its Online Appendix.
A retailer who sees her own demand before her supplier does can decide how much of that knowledge to pass upstream. Sharing everything is not obviously best: the supplier uses the information to set his production quantity for his own benefit, and the retailer bears a cost when he under-produces. Candogan and Gurkan (SSRN 4378997; published in Management Science, 2024, doi:10.1287/mnsc.2023.03004) treat this as a Bayesian persuasion (information design) problem in the sense of Kamenica and Gentzkow (AER 2011): the retailer commits in advance to a signalling policy, and the supplier best-responds to the posterior belief that each signal induces. The paper characterizes the retailer's optimal policy in closed form for uniform demand. This mission covers its first main result, the case where one demand support is nested inside the other.
The question links the supply-chain literature on information sharing between firms, where sharing is usually all-or-nothing, with the persuasion literature, where optimal signals are typically partial.
The state is , with prior . Demand is , where is uniform on and is uniform on . The supports are nested: and .
A disclosure policy is a finite message space and conditional probabilities . After message the supplier holds the posterior
Full disclosure sends message exactly in state ; no disclosure sends the same message in both states.
At belief the supplier solves the newsvendor problem
where is his critical ratio (shortage cost , excess cost ). A best-response profile picks an optimal quantity for every belief . The retailer pays the expected shortage at the induced posterior. Her design problem (3) minimizes the expectation of this cost over the random posterior, jointly over policies and best-response profiles . The function of (B.1) is her cost when both parties hold belief .
The thresholds are
For every prior :
The result shows that the optimal amount of disclosure depends on the critical ratio. When is high the retailer reveals everything; in an intermediate band she reveals nothing; when is low she uses a two-message policy that always reveals the narrow-support state ( always sends ) but pools part of the wide-support state with it. Corollaries 1–4 of the paper read the thresholds off this theorem (independence of the prior for large , full disclosure when , never full disclosure when ), and Theorem 2 of the paper, on the value of information design relative to full and no disclosure, is built on Lemma 1 and (B.5).
The paper proves the result in its Online Appendix, citing Kamenica and Gentzkow for the reduction to a convex envelope. None of it has been machine-checked. A formalization would make the persuasion reduction explicit for finite message spaces and best-response profiles, and would check the case analysis of the envelope, where the paper prints one overlapping-indicator slip (Lemma 1, case 3).
The obvious argument is to compare the three named policies and pick the cheapest. That is not a proof: optimality is over every policy on every finite message space, and it is only the convex-envelope reduction that cuts the comparison down to splittings of the prior into posteriors. The reduction itself requires showing that the attainable expected costs are exactly the convex combinations of values of at Bayes-plausible posteriors. The envelope computation then needs the shape of : the supplier's quantity is piecewise defined, so is a piecewise rational function of whose convexity changes across the boundaries and . In the low- regime is neither convex nor concave on , so its greatest convex minorant is a genuine mixture of itself and a line segment, whose junction point has to be located exactly.
States are Fin 2; a policy on a finite type is a map with nonnegative entries and rows summing to . The paper does not bound ; finite message spaces are a convention, and binary spaces already attain the optimum. Uniform expectations are interval integrals divided by the length. The supplier's cost is normalized by and parameterized by , which leaves its minimizers unchanged. A message of probability zero is given posterior and weight .
The supplier's response is defined as an argmin of (2), never by the closed form of Proposition 1, and optimality quantifies over all finite policies and all best-response profiles, never over the three named policies; a formalization that hard-codes either would make the goal a statement about a formula. is evaluated at the largest optimal quantity, which is the unique one under the mission's hypotheses. The envelope is the published definition BiconvexProg.BranchBound.convexEnvelope (greatest convex minorant) on .
Standing hypotheses, stated in every theorem: , , , , and nesting , . The hypotheses , are added: demand is nonnegative, and without them the constraint can bind. Equal supports are allowed; the threshold is then in Lean and the goal remains true. Lemma 1's third case is formalized as the piecewise function its two indicators intend.
A complete development needs: the convex-envelope (concavification) theorem for finite-support distributions on , the newsvendor quantile characterization for a mixture of uniforms, and calculus for piecewise rational functions. The first two are reusable beyond this mission. Contributions to any milestone are welcome.
Large retail platforms both host independent sellers and sell their own products, and they control the order in which products appear in search results. When the platform ranks its own product first regardless of relevance, it engages in self-preferencing. Regulators have treated this as a competition problem: the European Commission opened a second antitrust investigation into Amazon's treatment of its own retail offers in 2020 (CNBC, 2020), and search neutrality, the requirement that results be ranked by relevance alone, is the remedy most often proposed.
Zou and Zhou ask whether such a rule helps consumers once prices respond to it. Their model builds on the economics of prominence in consumer search (Armstrong, Vickers and Zhou, 2009), in which the product shown first is searched first and so enjoys a demand advantage. The answer they obtain is negative in an identifiable region: when the two competing products are similarly popular, search neutrality strictly lowers consumer surplus. This mission formalizes that result and the equilibrium analysis on which it rests.
A platform sells its own product and hosts a third-party seller of a competing product ; marginal costs are zero. A unit mass of consumers has unit demand. A product either matches a consumer (value ) or not (value ).
Under Condition 1 there are thresholds , depending only on , with
such that for every , consumer surplus in every equilibrium with search neutrality is strictly smaller than in every equilibrium without it:
The equilibria without neutrality: the price order when is prominent for all (Appendix, p. 42); the closed-form equilibrium of that pricing game (cases (A)–(B), pp. 42–43); the statement of Lemma A1 (p. 42); Proposition 1 (p. 16) and the uniqueness claim before it. The equilibria with neutrality: the price order by (pp. 44–45); cases (A2), (A3)/(B3) and (B2) (pp. 45–46); Proposition 2 (pp. 17–18). The two consumer-surplus displays (pp. 43–44 and 46). Proposition 3(2) and Corollary 1 are included as companion statements.
The result. Proposition 3(1) shows that a relevance-based ranking rule can backfire. Under self-preferencing the third-party product is never prominent, so its seller prices low to invite search, and this disciplines the platform's own price. Under neutrality each seller is prominent for the consumers who like its product best, and for similarly popular products both sellers charge the maximal price ; on consumer surplus with neutrality is exactly zero. The goal makes this precise and shows that the harmful region strictly contains that interval. It is the paper's central short-term finding and the basis of its policy discussion.
Formalizing it. No part of this analysis is machine-checked anywhere, and the platform has no model of consumer search with prominence. The source file contains the equilibrium derivations of §4.1 in its Appendix, but the proofs of Propositions 1–3 and of Lemma A1 are in an online appendix that is not part of the source; a formal proof would supply them. Several of the Appendix's closed forms are misprinted (the interior prices of cases (A1) and (B1), the thresholds and ), and the threshold misclassifies the boundary when ; the formal statements fix what is actually true.
The profits are piecewise quadratic with a kink at , so first-order conditions do not characterize equilibria: every candidate must be checked against global deviations across the kink. Without neutrality, a deviation can also change the platform's ranking, so the deviating seller faces a different demand system; this is the content of Lemma A1 and the reason Condition 1 is needed. The obvious argument for the goal, "consumer surplus with neutrality is zero on and positive without it", proves only the closed interval. The strict extension to requires controlling the neutral equilibrium just outside that interval, in the regions (A2) and (B2), where it is no longer at the corner.
A complete development needs elementary real analysis only: piecewise quadratic optimization on , the integral , and continuity of the neutral equilibrium in . The model definitions are shared, with the same names, with the companion mission on equal popularity and the commission rate. Proofs of any milestone are welcome, as are proofs of Lemma A1 and of uniqueness, whose arguments are not in the source.
Large retail platforms such as Amazon both host independent sellers and sell their own products in competition with them. The platform also controls the search ranking, the order in which products are shown to a consumer. The European Commission and the US Federal Trade Commission have examined whether platforms rank their own products ahead of rivals' (self-preferencing), and proposals of search neutrality would oblige a platform to rank products by relevance alone. The intuitive case for such a rule is that it protects consumers and third-party sellers.
T. Zou and B. Zhou, Self-Preferencing and Search Neutrality in Online Retail Platforms (Management Science, DOI 10.1287/mnsc.2022.01795), study this intuition in a duopoly model with consumer search and find that it can fail: when consumers see prices before searching, a platform free to steer consumers forces the third-party seller to cut its price to attract search, and neutrality removes that pressure. This mission formalizes their §4.2, which isolates the role of the commission rate the platform charges the third-party seller, at equal popularity of the two products.
A platform sells its own product and hosts a third-party seller of product ; production costs are zero. A unit mass of consumers has unit demand. A consumer of type values a product at if it matches her taste and at otherwise. A type- consumer is matched by with probability and by with probability ; for a type- consumer the roles are swapped. Throughout, . In this mission the two types have equal mass, .
Sellers set prices . The platform keeps a fraction of the third-party seller's revenue, so the profits are
where is the demand for product .
For each consumer type the platform shows one product first: the prominent product. A consumer sees both prices before searching, learns whether the prominent product matches for free, and pays a search cost , uniform on , to inspect the other product. Optimal search yields the per-type demands (1)–(2) of the paper and a consumer surplus equal to the expected payoff of optimal search, averaged over types and over .
Under search neutrality the ranking is fixed: is prominent for type and for type . An equilibrium with neutrality is a pair of prices from which neither seller gains by a unilateral change. Without neutrality, the sellers set prices first and the platform then chooses, at whatever prices it sees, the ranking that maximizes its own profit from each consumer. An equilibrium is a pair of prices together with an optimal ranking rule , mapping prices to rankings, such that neither seller gains by changing its price, given that the ranking will respond.
At :
The result separates two regimes of a single policy question. With a high commission the platform already earns most of the revenue of product and has no incentive to steer; neutrality is then moot. With a low commission the platform steers every consumer to ; the third-party seller responds by pricing below to make search worthwhile, and consumers benefit from this competition. Imposing neutrality removes it, prices rise to , and consumer surplus falls to zero, while the third-party seller gains. For high match probabilities the platform gains as well, which makes neutrality a commitment device a platform might accept voluntarily. Proposition 5 is the equal-popularity version of the paper's main short-term finding (Proposition 3, under a low commission), now valid for every commission rate.
The paper proves Proposition 5, Proposition 4 and Lemma 1 in an online appendix that is not part of the manuscript used here; the manuscript's own Appendix contains only the equilibrium derivations for the game with a fixed ranking. None of these results is machine-checked. A formalization would produce the first verified treatment of a pricing game with an endogenous, profit-maximizing ranking stage and of a consumer-surplus integral over search costs; the definitions are reusable for the companion mission on the low-commission regime and for other prominence models.
The demands are piecewise quadratic with a kink where the two prices cross, so profits are not concave on , and first-order conditions only locate candidates. The central difficulty is the ranking stage. A seller's deviation can change the platform's ranking: the third-party seller may raise its price to make prominence for type worthwhile to the platform, and the platform as a seller may cut its price to undercut. Checking an equilibrium therefore requires comparing profits across ranking regimes at every deviation price, not only inside the regime of the candidate. The uniqueness claims require excluding equilibria in every regime, including those supported by an unusual tie-break of the ranking rule. The comparison of platform profits in part 3 compares the explicit interior prices of Proposition 4(2), a rational function of , with ; the paper gives no explicit threshold .
SearchNeutrality.Commission.Model; the closed-form prices and surplus in SearchNeutrality.Commission.ClosedForms. These duplicate, with the same names, the definitions of the companion mission SearchNeutrality.ShortTerm.Heavy-traffic analysis is the standard tool for scheduling queues whose servers are almost always busy: after diffusion scaling, a multiclass queue is approximated by a reflected Brownian motion, and asymptotically optimal policies are read off a limiting control problem. Classical results of this kind, such as the asymptotic optimality of the cµ rule (serve the class with the largest holding cost times service rate first; van Mieghem, 1995), assume that the job-size distributions are known.
In practice the first moments of service times are usually estimated well, while their variability is not. Atar, Castiel and Shadmi study a high-uncertainty regime: the means of the job-size distributions are pinned down to within , but their variances are uncertain at order one, and an adversary chooses them job by job with full knowledge of the past. The scheduler wants to minimize, and the adversary to maximize, a discounted holding cost. The paper solves this game asymptotically: the nonpreemptive cµ policy is asymptotically optimal against every adversary, and the value of the game converges to the value at of a one-dimensional Hamilton–Jacobi–Bellman (HJB) equation.
There are job types and one server. In the -th system one job of each type arrives at each time , , and the server works at rate , so that a job of size occupies it for time units. The system starts empty.
Adversary. For each and type an uncertainty class , a nonempty closed set of probability distributions on , is given. At each epoch the adversary chooses for every , based on the past job sizes, and the job sizes are then drawn independently across types from these distributions. The set of such controls is .
Scheduler. The scheduler chooses the cumulative effort devoted to each type, an -dimensional Lipschitz path whose increments over lie in . An admissible strategy is a measurable, non-anticipating, work-conserving map from the adversary's control path to such an effort path that never serves more work than has arrived.
Cost and value. With , the workload is , the queue length is the number of arrived type- jobs not yet completed, and hats denote scaling by . For holding costs ,
Assumptions. With the mean and half the variance of , and , the sets converge in the Hausdorff distance to compact sets ; fourth moments are uniformly bounded; (heavy traffic); and types are labelled so that , with .
HJB equation. With ,
for the classical solution of the HJB equation. The paper states with the value of a martingale control problem; the goal uses the form, which leaves the martingale problem out of the statement.
The result gives the first-order asymptotics of a scheduling game with model uncertainty: the scheduler loses nothing by ignoring the adversary and using the cµ rule, and the adversary's best response is a state-feedback choice of drift and variance determined by and . Theorem 1 is a robustness statement for one of the most widely used scheduling rules; Theorem 2 reduces a game on path space to a scalar nonlinear ODE.
The paper's proofs are complete, so the remaining work is formalization. No part of this result, and none of its objects (heavy-traffic queues with adversarial service distributions, the nonpreemptive cµ policy as a map on path space, the HJB equation of a reflected controlled diffusion), has a known machine-checked statement or proof.
The statement is a limit of a real sequence, but each term is an infimum over measurable, causal, work-conserving maps on path space of a supremum over feedback choices of distributions. The proofs (§§4–7 and the appendix) use uniform C-tightness of prelimit processes, weak convergence in , the existence theory for fully nonlinear uniformly elliptic equations (Gilbarg–Trudinger, Thm 17.18), martingale characterizations of limits (Jacod–Shiryaev, Cor. VI.6.30; Karatzas–Shreve, Thm 5.5.15), measurable selection (Budhiraja–Dupuis, Lemma 8.10), and Taylor expansion of along the prelimit workload. The obvious route through the uncontrolled diffusion limit fails because the adversary's variance choice is state dependent, so no single limiting Brownian motion describes all adversaries; the limit is a control problem, not a process.
The Lean development lives in the namespace HighUncertHT.Game. Types are Fin L, 0-based (the paper's type 1 is index 0). Distributions are ProbabilityMeasure ℝ with no mass on , with the weak topology. Systems are indexed by ; the class at is required to satisfy the same conditions so that control sequences indexed by exist. Costs and values are in (lower Lebesgue integrals), sup norms are in , the Hausdorff distance is the extended one, and derivatives of are one-sided on .
An adversary control is encoded by its feedback map from past job sizes to distributions and the measurable Markov kernel it induces; its law is the Ionescu–Tulcea trajectory measure. By (5), the Doob–Dynkin lemma and (7), this has the same laws, hence the same costs, as the paper's . Strategies are measurable for the product σ-algebras. The cµ strategy is defined explicitly by an event recursion over service decisions.
The standing assumptions (Assumptions 1–2, labelling (14), ) are fields of the Setting and hold in every statement. Corrected printed slips: the priority rule serves the highest index (p. 9 prints "lowest", contradicting the cµ rule and Lemma 5); the departure count is capped at the number of arrived jobs (p. 6); "→ 0 in probability" for processes is read as convergence of the sup norm on compact intervals (Lemma 5); (55) is stated for the control (61), not (15).
Trivializing formalizations are ruled out: is nonempty because is a milestone; the HJB has a classical solution (Proposition 1.1), so the goal is not vacuous; no expectation is a Bochner integral that could vanish for non-integrable integrands; is not a junk deriv; and (55) asserts that its feedback control exists.
Needed infrastructure: diffusion-scaled processes and their tightness in , the one-dimensional Skorokhod map and its Lipschitz property, martingale estimates for sums of conditionally centred job sizes, and the existence theory for the HJB equation. The Skorokhod map, the queue primitives and the cµ policy are reusable for other heavy-traffic missions. Contributions on any milestone, or on general lemmas they need, are welcome. Not included: Lemmas 1, 6, 7, 8, Proposition 1.2, Proposition 2, Theorem 2.3 and the martingale control problem.
Large data centers and cloud platforms route a stream of incoming tasks to many server pools, each pool able to serve several tasks at once. A dispatcher that sends each task to the least loaded pool (join-the-shortest-queue, JSQ) balances the load best, but it needs the exact number of tasks at every pool, which is costly to maintain at scale. A threshold dispatching rule needs much less information: it only needs to know which pools hold fewer than tasks, or fewer than tasks. For constant arrival rates and exponential service it has the same fluid and diffusion limits as JSQ when and the threshold equals , where is the offered load per pool (Goldsztajn, Borst, van Leeuwaarden, Mukherjee and Whiting, INFORMS Journal on Computing 34(1), 2022, reference [15] of arXiv:2012.10142v3).
The difficulty is that the right threshold depends on , which the dispatcher does not know. Goldsztajn, Borst and van Leeuwaarden (arXiv:2012.10142v3) let the dispatcher learn it online. This mission concerns their second main result: with Coxian service times, which are dense among all service-time distributions, and the basic learning scheme, the threshold settles at the optimal value and the load becomes nearly balanced, almost surely in the many-server limit. (The first main result, for exponential service with a time-varying arrival rate and a refined learning scheme, is the subject of a companion mission.)
There are server pools. Tasks arrive as a Poisson process of rate , . A task passes through at most phases: it starts in phase , phase lasts an exponential time of rate , and after phase the task moves to phase with probability or leaves with probability , with and for . The mean service time follows from these data, and .
A pool has profile if it holds tasks in phase . The occupancy state is the fraction of pools with profile , a point of , and is the fraction of pools with at least tasks.
Dispatching. With threshold and for an integer , an arriving task goes to a uniformly random pool with fewer than tasks if there is one; otherwise to a uniformly random pool with fewer than tasks if there is one; otherwise to a uniformly random pool.
Basic learning. , where is the number of tasks divided by and .
All systems, for every , are built on one probability space from independent unit-rate Poisson processes , i.i.d. uniform selection variables and random initial states , through the equations (21a)–(21b) of §6.1.1. Initial states converge, , and for a fixed .
If , there are constants , independent of the horizon , such that almost surely
The constants are left unspecified, as in the paper; what is fixed is the shape: the threshold equals after time , the first columns are asymptotically full, and the excess mass decays exponentially.
In the order the proof uses them: well-posedness of the coupled construction (§6.1.1); relative compactness of the occupancy and counting processes (Proposition 14); a uniform bound on occupancy and threshold over (Lemma 15); the set of nice sample paths (Proposition 16); the almost-sure law of large numbers for the total mass, with the infinite-server fluid function built from the residual-service survival functions (Proposition 17); and differential inequalities for the limits of the mass processes while the threshold is (Proposition 18).
Theorem 3 says that a dispatcher that knows nothing about the load except the current number of tasks reaches the threshold JSQ-like balancing needs, and then balances the load: with , the fraction of pools with fewer than tasks vanishes and the fraction with more than tasks is , where is a lower bound on the service hazard rate. Because Coxian laws are dense among service-time distributions, the result is evidence that threshold-based learning works beyond exponential service. Proposition 17 is also a statement of independent interest: the fluid law of large numbers for an infinite-server system with Coxian service, known to hold weakly, holds almost surely under this coupling.
The results are proved in the paper (arXiv:2012.10142v3, 2024). No part of them is formalized. The mission produces a machine-checked model of the coupled many-server construction with phase-type service, which no Lean library has, and a complete formal proof of the paper's almost-sure fluid-limit argument.
The statements are almost sure and pathwise, about one coupled sequence of jump processes with a countable state space , so weak-convergence arguments do not suffice. The natural first idea, to read off Theorem 3 from Proposition 17 alone, settles only (8a): and force eventually, but they say nothing about how the mass is distributed across the pools. Statements (8b) and (8c) require tracking the column masses through subsequential fluid limits that are only known to be Lipschitz, with dispatching decisions that depend discontinuously on the state. The phases complicate this: a pool's departure rate depends on the phases of its tasks, which the column picture ignores, and only the lower bound on the hazard rate controls the decay. The hypothesis cannot be dropped: when is a multiple of , the threshold can oscillate between and .
Fin r; profiles are Fin r → ℕ; a fixed enumeration of is a parameter. is computed as , equal to (1) on .BesbesZeevi.Parametric.PoissonProcess for every driving process, their mutual independence, i.i.d. uniforms, independent initial conditions with ), plus processes that almost surely solve (21a)–(21b) for every and all , are càdlàg, -valued and have finitely many tasks. Left limits are Function.leftLim; and are guarded, never truncated. The dispatching indicators are defined for all , and the endpoints of are corrected so that the intervals partition as the text states.The reflected random walk is the waiting-time sequence of the single-server queue (Lindley's recursion). Additive functionals measure accumulated congestion. For this is the total waiting time, the area under the workload curve.
Existing general results on sample-path large deviations for additive functionals of Markov chains (in the Donsker–Varadhan line) assume the function to be bounded. They therefore do not cover the cumulative waiting time of a single-server queue. For the relevant rare events are not produced by a small, uniform tilt of the whole trajectory but by a few busy periods of exceptional size, and the speed is sublinear.
Bazhba, Blanchet, Rhee and Zwart (arXiv:2003.14381, Mathematics of Operations Research, 2025) prove that the scaled partial-sum process satisfies a large deviation principle at the sublinear speed . They also identify the rate function through a variational problem over paths of bounded variation.
Related work on large deviations of the area under a busy period either treats queue-length functionals (Blanchet–Glynn–Meyn, 2013) or assumes a moment generating function that is finite everywhere (Duffy–Meyn, 2014). Neither obtains a sample-path result. The present paper assumes only that the moment generating function of the increment is finite near the origin. It relies on the sample-path large deviations for light-tailed random walk trajectories of Borovkov and Mogulskii (II, III) and of Vysotsky (ALEA, 2021), and on the authors' earlier work in the topology (Bazhba et al., 2020).
Let be i.i.d. copies of a real random variable with . Let and be the supremum and infimum of . The paper assumes:
The chain is , . Fix and let . The object of study is
The busy periods are delimited by the return times , . The busy-period areas are , and the long-run mean of is .
lives in the Skorokhod space of càdlàg paths. This space carries the metric (Definitions 2.1–2.2). It compares parametrizations of the extended completed graph, which joins each jump by a vertical segment and also joins to at the origin ().
The rate function involves the variational problem
Here is the set of paths of bounded variation on compacts with whose reflected area up to the first return time of to zero is at least . is the reflection map. The cost is
where is the Legendre transform of and are the absolutely continuous, upward singular and downward singular parts of .
satisfies the large deviation principle in with speed and rate function
where is the set of paths with a non-decreasing pure jump path, .
The result. The theorem gives the full large deviation behaviour of , not only its one-dimensional tail. It identifies the mechanism of rare events: one or a few busy periods of area of order , each contributing times its area to the power . In the rate function, a busy period in progress at the end of the horizon is indistinguishable from a completed one; the paper's Theorem 2.3 and Proposition 4.3 make this precise. By contraction the theorem yields tail asymptotics for any -continuous functional of the cumulative cost process.
The formalization. The result is proved on paper. No part of it has been machine-checked, and the platform has no Skorokhod metric and no large deviation principle at a sublinear speed. A complete development would supply the first formal metric on and a sample-path LDP for a heavy-tailed regime. It would also provide a formal treatment of variational problems over paths of bounded variation with singular parts.
The obvious route is the contraction principle applied to the sample-path LDP for the scaled random walk , followed by the map that sends the walk to the area under its reflection up to its first return to zero. That map is not continuous: the first passage time is discontinuous in every Skorokhod topology. The paper replaces the random horizon by a large fixed horizon , but then must show that the variational problems over and over have the same value (Lemma 4.4). It must also prove uniform continuity of the area functional on level sets of the rate function (Lemma 4.5).
A second difficulty is the class of admissible paths. Because may be finite, optimal paths could a priori contain jumps or singular parts. Lemma 4.1 rules this out. Finally, the passage from the finite-dimensional LDP to the topology requires the busy period in progress at time to be handled separately. The mere existence of the limit in Theorem 2.3 relies on a time-reversal argument and on the decay rate of the stationary distribution.
U : ℕ → Ω → ℝ, measurable, independent and identically distributed, with U i the paper's . Moments are lower Lebesgue integrals in , never Mathlib's mgf. .ENNReal.log with ; liminf and limsup are taken in EReal. Probabilities of possibly non-measurable events are outer measures.Contributions to any milestone, and formalizations of the cited Results B.1–B.3, are welcome.
Global sensitivity analysis asks how much of the uncertainty in a model output is due to an input . Borgonovo, Figalli, Plischke and Savaré (Management Science, 2025) propose a family of indicators built on optimal transport: the expected optimal transport cost between the marginal law of and the law of conditioned on the information carried by . The family contains the variance-based and -based indices used in practice as special or limiting cases, and it applies to multivariate outputs.
In applications these indicators are never computed from the true joint law of . They are computed from a sample, by splitting the range of into cells, estimating the law of on each cell, and solving one optimal transport problem per cell (the estimator (76) of the paper). Whether this procedure converges to the quantity it is meant to estimate is the question of consistency, settled by Theorem 21 of the paper. This mission formalizes Theorem 21 and the steps of its proof.
Let and be Polish spaces with their Borel -algebras. A cost is a continuous function with exactly when . The optimal transport cost between probability measures on is
the infimum over couplings with marginals and .
Let be the joint law of on , with marginals (of ) and (of ). For a -algebra on , a version of the conditional distribution of given is a Markov kernel , -measurable in , with for . The OT-based sensitivity measure (Definition 1) is
written when is the Borel -algebra.
Estimation setting. A sequence of joint laws on (for instance empirical laws of a sample of size ) converges weakly to ; are its marginals. The cost has bounded separate costs: with continuous, and with ,
A sequence of finite measurable partitions of generates -algebras with
The quantities of interest are (finite ) and .
Under (73) and (75), the iterated limit exists and
The statement fixes no rate and no constant; it asserts only that refining the partition after the sample size has grown recovers the sensitivity measure.
The last step of the paper's proof, , is the continuity of along increasing -algebras, Theorem 9 of the paper. It is posed in the companion mission of this series (part 2, on information continuity) and is not restated here.
Theorem 21 is what licenses the partition estimator: without it, the number computed by solving one transport problem per cell of a sample has no proven relation to the sensitivity measure. The result is deterministic in the laws, so it applies to any sampling scheme whose empirical laws converge weakly with converging -moments, not only to i.i.d. samples. The finite case covers categorical inputs directly.
On the formal side, no part of this argument is machine-checked. A complete development produces reusable pieces beyond this paper: the conditional law on a cell of null boundary as a continuous functional of the joint law, uniform integrability from convergence of moments under weak convergence, and the stability of optimal transport costs under weak convergence of the marginals with uniformly integrable cost bounds. The last is a standard theorem of optimal transport (Villani 2009, Theorem 5.20 and its proof) that the paper invokes without proof in (86).
The naive argument passes to the limit term by term in the finite sum (83). Two steps of it fail without further work. First, the optimal transport cost is only lower semicontinuous under weak convergence in general; convergence of needs the cost to be dominated by functions whose integrals converge, which is why (73) is assumed and why uniform integrability (85) must be transferred from to the cell laws. Second, cells of zero limiting mass may carry positive empirical mass for every , and their conditional laws need not converge at all; their contribution must be shown to vanish through the product , not through the cell laws. Finally, the two limits do not commute in general, so the order matters.
Fintype with the discrete topology, so .ProbabilityMeasure.RWPI.SqrtLasso.transportCost; all of , and the integrals take values in .IsCondDistrib.lim.A trivializing formalization is ruled out: is not assumed bounded, the laws are not assumed eventually equal to , the conditional laws are not assumed to converge, and cells of zero mass are allowed.
Contributions are welcome on each milestone separately, in particular on the stability of transport costs (86), which is reusable well beyond sensitivity analysis.
Place distinct points on the unit sphere in to minimise the Coulomb energy
Good configurations are easy to find numerically, but proving that one is the global minimum is hard. Rigorous proofs exist for only a few :
The shared lemmas (the distance formula, two-point positivity behind the Delsarte–Yudin bound, and three-point positivity behind the Bachoc–Vallentin and Cohn–Woo bounds) are stated once for reuse, along with well-posedness of each configuration.
Many businesses are run by an agent on behalf of an owner who cannot see everything the agent does. Two frictions arise together. The agent may shirk, saving the cost of the effort that brings customers in, and the agent may divert cash, pocketing the fee of a customer the owner never sees: a plumbing franchise whose offline jobs bypass the head office, or a home-services platform whose providers are paid off-platform by returning clients. Each friction alone is a classical object of dynamic contract theory: DeMarzo and Sannikov (2006) study cash diversion, and Sun and Tian (2018) study effort incentives with Poisson arrivals. Tian, Astashkina and Duenyas (SSRN 4249177; Management Science, 2024, doi:10.1287/mnsc.2022.01169) solve the problem with both frictions present, in a model where customers arrive by a Poisson process whose rate the agent controls. This mission formalizes the baseline model of their Section 2 and its main result, Theorem 1.
Customers arrive at rate while the agent exerts effort (, at flow cost ) and do not arrive while the agent shirks (). Each arriving customer independently uses the unobservable channel with probability , paying the fee , or the observable channel with probability , paying . The counting processes and count the arrivals by channel. The principal observes and the agent's reports of the -arrivals; an unreported -arrival is cash the agent keeps. Both parties discount at rate .
A contract consists of a nondecreasing cumulative payment (limited liability: payments are never negative) and a termination time , both functions of what the principal observes. The agent's utility (2.1) and the principal's utility (2.2) are
A contract is incentive compatible, , if always working and always reporting truthfully (, ) is optimal for the agent against every alternative effort process and reporting rule. Write , , , and assume the standing condition (2.5), .
The candidate optimal contracts , , track a promised utility that starts at , drifts by , jumps up at rewarded arrivals, triggers termination when it reaches , and is capped at a tenure threshold , with the excess paid out: with jumps at reported -arrivals only (Definition 1); with jumps and (Definition 2); with jump at every arrival (Definition 3). The principal's value function solves a differential equation with advanced arguments, for instance in the first scenario
extended by beyond the threshold.
With (2.14), the optimal contract in is
meaning and for every .
The theorem shows that three simple contracts, each a probation period followed by termination or tenure, solve a two-dimensional moral hazard problem, and it tells which incentive constraint binds: truth-telling alone when , both when , effort alone when . Section 2.4 of the paper extends optimality to contracts that may let the agent shirk, and Sections 3 to 5 build monitoring, dynamic pricing and continuous effort on the same baseline, so the definitions here are the substrate for those results.
The result is proved in the paper, with two of the three scenarios of Lemma 4 and Proposition 1 left to the reader. It has not been formalized. A complete development would give a machine-checked account of a continuous-time contracting model driven by a controlled point process, which no library currently provides.
Three steps resist a direct transcription of the paper's argument. First, the value-function equations are not ordinary differential equations: they evaluate at , , , so existence, uniqueness and concavity come from a backward induction over intervals of length starting at the tenure threshold, and concavity holds only under (2.5). Second, the upper bound for an arbitrary incentive compatible contract needs the promise-keeping representation of the agent's continuation utility, a martingale representation for point-process filtrations, and a verification argument through Itô's formula for jump processes; the paper's proof uses the terminal condition and a martingale property without addressing or integrability. Third, the characterization of incentive compatibility by the jump conditions and is argued in the paper by a one-deviation heuristic, whereas (IC) quantifies over all joint deviations in effort and reporting.
The arrival process is built from an i.i.d. sequence of standard exponential clocks and Bernoulli() channel marks: the next arrival occurs when times the effort time accumulated since the last arrival reaches the next clock. Strategies (effort and reporting) and contracts (cumulative payment and termination rule) are functions of the relevant history: the agent's full arrival history for strategies, the principal's observed history for contracts, which is the general form of predictable and adapted processes for a marked point process. Effort at time depends only on arrivals strictly before ; reports can hide -arrivals but never invent them. Utilities are expectations in of nonnegative pathwise terms, payments enter as a Lebesgue–Stieltjes integral over , and is real-valued on contracts with finite expected payments, which requires. (IC) quantifies over every measurable strategy.
The value functions are pinned by solution classes: continuity on , the slope extension beyond , differentiability and the equation on , and . The printed (2.11) has a stray on its right-hand side; the formalization uses the equation obtained from the HJB equation (2.7), which is the one the proofs use. Proposition 2 is stated for every promised utility (the page says ), which is what the optimality argument (2.15) needs. The bound (B.12)–(B.16) adds the condition , since is defined on .
The formalization does not trivialize: is not shrunk by restricting deviations, contracts react to reports so that hiding an arrival changes what the agent is paid, carries no junk value on , and the goal quantifies over solutions of the value-function equations rather than over arbitrary concave functions; Lemma 4 is what makes that quantification non-vacuous.
Out of scope: Theorem 2 (optimality in the larger space , whose shirking payoffs are defined only inside its proof), Lemma 5, Sections 3 to 5, and as separate items Lemmas 1 to 3, Lemma 14 and the equivalence of (IC) with the two jump conditions, which need a promised-utility process with left limits built from conditional expectations. Contributions of that infrastructure (point-process martingale representation, Itô's formula for finite-variation jump processes, a verification theorem for discounted optimal control) are welcome and reusable beyond this mission.
Approximate policy iteration is the template behind most practical reinforcement-learning systems for large state spaces: alternate between choosing a policy that looks good under the current value estimate and estimating the value of that policy, with errors in both steps. Game-playing systems such as AlphaZero add two ingredients to this template: a multi-step lookahead (tree search) when choosing the policy, and a linear or neural value-function approximation fitted from a few evaluated states. Classical error bounds for approximate policy iteration (Bertsekas and Tsitsiklis, 1996) assume that each evaluation error is bounded by a fixed ; Efroni, Dalal, Scherrer and Mannor (2019) extended them to -step lookahead policies. Neither analysis asks whether a fitted value function actually meets such a bound.
Winnicki, Lubars, Livesay and Srikant (arXiv:2109.13419, Operations Research, 2025) show that it need not: with least-squares fitting on a subset of states, the iterates of approximate policy iteration can diverge (their Section 3.2). They then prove that sufficient lookahead and rollout length restore convergence, with an explicit finite-time error bound. This mission formalizes that bound.
A Markov decision process has a finite set of states , a finite set of actions , transition probabilities of moving from state to state under action , mean rewards , and a discount factor . A deterministic policy is a map . Its value is the expected discounted reward
and the optimal reward-to-go is . Vectors are compared in the sup norm . The policy operator and the Bellman operator are
Each state has a feature vector ; is the matrix with rows . For a set of states , keeps the rows indexed by and selects the entries of a vector indexed by .
Algorithm 2 starts from an arbitrary and, at iteration , (i) picks a policy with (an inexact -step lookahead); (ii) forms the noisy return on an evaluation set ; (iii) fits by least squares on and sets . Assumption 1 asks that the features of have rank for every and that . Under it the fit is linear, with , and the paper defines
If , then under Assumption 1 every run of Algorithm 2 satisfies, for every ,
In the order the proof uses them:
Theorem 1 states a sufficient condition for convergence that does not depend on the size of the state space: lookahead plus rollout depth must exceed , where depends only on the features and the evaluation sets. Paired with the divergence example of Section 3.2, it shows that lookahead is not merely a heuristic improvement but can be what makes approximate policy iteration with linear function approximation stable. Proposition 1 is a reusable interface: any policy-evaluation scheme whose errors satisfy a geometric-plus-floor bound inherits the same convergence guarantee; the paper's gradient-descent variant is obtained this way.
The result is proved on paper; it has not been machine-checked. The Prove2Me platform has the finite-MDP layer used here (transition kernels, policy values as discounted series, the Bellman optimality operator), exact modified policy iteration, and a one-step bound for greedy approximate policy iteration with -functions (, no lookahead error). It has no lookahead bound, no least-squares value-function fit, and no finite-time bound for approximate policy iteration with function approximation. A complete development would add the Bellman equations for deterministic policies, the lookahead step (15), the least-squares projection identity, and the error recursion, all of which are reusable for other analyses of approximate dynamic programming.
The obvious argument fails at the evaluation step. Classical analyses treat as given; here the error is produced by the algorithm and fed back: the fitted is the input of the next lookahead, and the least-squares operator can amplify sup-norm errors by a factor , which is at least whenever . The error recursion therefore contracts only when . A second point is the lookahead step (15), which must hold for an arbitrary previous policy and an inexact lookahead, and rests on the increase of in rather than on contraction alone. Finally, combining the geometric decay of the evaluation errors with the -contraction of (15) requires a convolution estimate that yields the factor .
States and actions are finite nonempty types; the transition kernel is the published IsTransitionKernel, is the published PolicyValue (a discounted series of expected rewards, not a fixed point of ) of the point-mass policy at , is the published BellmanOperator, and is the maximum of over the finitely many deterministic policies. Rewards enter only through their means . Vectors are functions with the sup norm; matrix norms are Mathlib's operator norm (maximum absolute row sum). The rank condition of Assumption 1 is for every ; Lean's matrix inverse is zero on singular matrices, so no statement relies on it without this hypothesis.
Conventions fixed where the page is loose: Algorithms 2 and 3 are predicates on whole runs, quantified over every admissible lookahead policy, noise and minimiser. , which Algorithm 2 never produces, is free, so every bound holds for every deterministic . is the operator of (eq. (6) calls it ; the suprema agree). is the supremum over all and all deterministic policies. Algorithm 3 is stated with , the index of (15) and Appendix B, and without the representation , which Proposition 1 does not use. Proposition 1's first display divides by and is stated for ; the other results take . The noise bound is imposed on the whole vector instead of setting off ; off it constrains only entries the run never reads. The limsup is stated as "for every , eventually bound ". The hypothesis of Theorem 1 is kept with the real logarithm as printed; for it is equivalent to , and when (possible only if ) it reads .
A formalization that fixes the lookahead policy to an exact argmax, the noise to zero, or to a convenient policy proves a special case and is ruled out; so is defining or as a fixed point, which would make eq. (2) definitional.
Contributions welcome: proofs of the Section 2 milestones from the series definition of , the least-squares identity (6), the lookahead step (15), and the recursions of Proposition 1 and Appendix B. Theorem 2 of the paper (gradient-descent fitting) is not part of this mission: its Assumption 2 places no lower bound on the step size, and the statement fails for negative step sizes.
In stochastic multi-armed bandits, a robust way to explore is action elimination: keep confidence intervals for every arm, discard an arm once its upper confidence bound falls below another arm's lower confidence bound, and sample uniformly among the arms that survive. Uniform sampling is what makes the first corruption-robust bandit algorithm work (Lykouris, Mirrokni & Paes Leme, STOC 2018): an adversary that corrupts a few rounds cannot steer a learner whose choice among surviving arms is random.
Lykouris, Simchowitz, Slivkins and Sun (arXiv:1911.08689v4, Mathematics of Operations Research) extend corruption-robust exploration to episodic reinforcement learning. Their algorithm also maintains active sets of actions, but it does not play uniformly among them; it follows an optimistic (UCB) policy restricted to the active sets. Section 7 of the paper explains why: Theorem 7.1 shows that the bandit recipe, transplanted verbatim to episodic MDPs, suffers linear regret for exponentially many episodes, even when every confidence statement it makes is correct. This mission formalizes that lower bound.
An episodic environment has a finite state set , a finite action set with , and a horizon . A stochastic problem instance on it fixes an initial state law , a transition kernel (the same at every stage), and reward laws on with means . The optimal Q-function and value are defined backwards from by and ; the optimal actions are , and .
A Q-supervisor holds estimates , active sets , and a policy greedy for . It is confidence-admissible for (Definition 4.1) if and everywhere. Its plausible sets are
An algorithm is uniformly action-eliminating if before each episode it outputs a Q-supervisor , possibly at random and depending on everything observed so far, and at each stage plays uniformly at random from , independently across stages. It is uniformly admissible for if for every instance on its Q-supervisors are confidence-admissible with probability at least . The regret over episodes is , with the uniformly-at-random policy of episode .
For every and there is an instance on an environment with and such that every uniformly action-eliminating, uniformly admissible algorithm satisfies
The witness is the combination lock : states , action advances , any other action falls into the sink , and the only reward is for action at . Its twin has the same transitions and zero rewards. The milestones are the steps of the paper's proof:
The theorem separates two exploration principles that coincide in bandits. For episodes of uniform elimination the regret is until is of order , while optimistic exploration over the same confidence sets attains regret polynomial in , , and (Azar, Osband & Munos, ICML 2017). It is the reason the paper's SuperVIsed.C algorithm combines active sets with a UCB policy rather than sampling uniformly, and it applies to any uniformly admissible construction of the confidence bounds, so better estimators do not escape it.
The result is proved in the paper (Appendix A); it is not formalized anywhere. A machine-checked version adds a precise account of what "algorithm" means here (a learner that may use all past observations and internal randomness), of the probability space of a whole run, and of the change-of-instance argument (A.1), which is the template for many reinforcement-learning lower bounds.
The arithmetic of the final step is elementary. The work is in the probability space: the run of an adaptive learner over episodes is a sequential composition of the learner's choice of supervisor, the episode's states, actions and rewards, and the learner's update. Equation (A.1) needs a likelihood argument on this composed law: on histories that never play , every factor of the two run laws agrees, because the two instances differ only at a state–action pair such histories never visit. Equation (A.2) needs that, conditionally on the supervisor of episode , the episode's actions are independent and uniform. Neither can be read off the per-episode description; both require induction over episodes on the run law.
A tempting shortcut is to apply admissibility one episode at a time. It does not suffice: the proof needs the joint event to have probability at least (see the scope section).
Fin (H+1), actions Fin A; the paper's action is 0, the sink is state 0. Stages and episodes are 0-based. Transitions, initial laws, rewards, supervisor laws and action laws are PMFs. The value is the backward recursion on p. 8, written on the number of remaining stages since the kernel is stage-independent.Welcome contributions: lemmas on the run law of an adaptive learner (marginals of the -th supervisor, conditional independence of episode given its supervisor), which are reusable for other episodic lower bounds.
Reinforcement-learning algorithms with regret guarantees, such as UCBVI (Azar, Osband & Munos 2017), assume that every episode is generated by the same Markov decision process. In practice a fraction of episodes can be generated by something else: fraudulent users of a recommender, sensor faults, a strategic participant. Corruption-robust learning asks for regret that degrades gracefully with the number of corrupted episodes, without knowing in advance.
Timeline. For stochastic multi-armed bandits, Lykouris, Mirrokni & Paes Leme (STOC 2018) introduced the corruption model and a multi-layer active arm elimination algorithm whose regret grows linearly in ; Gupta, Koren & Talwar (COLT 2019) improved the dependence to additive. For episodic reinforcement learning, Lykouris, Simchowitz, Slivkins & Sun (abstract at COLT 2021; Mathematics of Operations Research 2025) gave SuperVIsed.C, the first algorithm with sublinear regret under any deviation from i.i.d. episodes in this setting: in tabular MDPs with steps its regret is of order up to logarithmic factors and lower-order terms (their Theorem 2.1), with an analogous bound for linear MDPs, without knowing . Their analysis isolates a deterministic regret guarantee, Theorem 4.1, from which the headline bounds follow by concentration.
An episodic tabular MDP has a finite state set , a finite nonempty action set and a horizon . The nominal MDP consists of an initial distribution , stage-independent transition probabilities and mean rewards . With , the optimal values are and , and . A randomized Markovian policy is a probability distribution over finitely many deterministic Markov policies, and is its expected total reward.
A Q-supervisor holds upper and lower estimates of , active sets of actions, and a UCB policy maximizing over the active set. It is confidence-admissible if and every optimal action is active. A policy is Q-supervised if it plays only plausible actions, those with for all active . The Bellman errors are and . A policy has UCB visitation ratio at most if switching to at any stage multiplies the probability of any later state-action pair by at most . A model-estimate is valid if the bonus bounds .
SuperVIsed.C runs base learners. Learner runs a two-estimate value iteration, UCBVI-BASE, with a global model-estimate (all data, bonus inflated by ) and a subsampled one, inside the active sets handed down by learner ; it returns its base policy and the active sets for learner . In each episode a nondecreasing random layer schedule decides whose base policy is played at each stage; the master policy is the resulting mixture, and , are its conditionings on the final layer, with probabilities , .
With and expected bonus sums (subsampled, along ) and (global, along ): if the global and subsampled model-estimates of every learner are valid in every episode, then
The left side is the paper's upper bound (2.2) on the regret. The statement leaves the estimates arbitrary apart from their ranges and validity, so it holds for every data realization.
The milestones follow the proof: the value decomposition over final layers (Lemma 4.4), admissibility from validity (Lemma 4.6), supervision of the master policies (Lemma 4.5), the Bellman-error decompositions (Lemma D.1, Propositions 4.1 and 4.2), the bonus bound on Bellman errors (Lemma 4.7), and the schedule estimates (Claims 4.8, 4.9 and Lemma 4.10).
Theorem 4.1 is the explicit core of the paper's results: Theorems 2.1 and 2.2, stated only up to constant and logarithmic factors, follow from it by bounding the bonus sums. Its proof architecture, which supervises less robust learners with more robust ones and bounds their mismatch through the visitation ratio, is independent of the tabular setting; the paper applies it to linear MDPs as well.
The result is proved in the paper; no machine-checked proof exists. Formalizing it requires a fully explicit account of the master policy as a mixture over schedules, of concatenated policies, and of the step of Proposition 4.2 from fictitious trajectories to real ones. Several printed constants and statements need correction, which the formal statements record (see the scope section).
The obvious argument, optimism plus the Bellman-error decomposition of UCBVI, fails because the master policy does not play the UCB policy of any single learner. The regret of a supervised but non-greedy policy is controlled only along fictitious trajectories that switch to the UCB policy (Proposition 4.1), and turning those back into the policy's own trajectories needs a bound on the visitation ratio that holds for every schedule prefix of a mixture, not only for marginal layer probabilities. A second difficulty is bookkeeping: nested active sets, two estimates per learner, and conditioning the schedule on its final layer.
X, A with [Nonempty A]; stages 0-based (the paper's stage is Lean's h - 1, terminal values at index H); policies ℕ → X → A; randomized policies as finite weighted families of deterministic ones; trajectory laws as finite products, values and occupancies as finite sums; schedules Fin H → Fin ℓmax. Rewards enter through their mean ; the regret is the bound (2.2). Logarithms are base 2.In many sequential decision problems the state of a system is not observed for free. A controller monitoring a machine, a patient or an inventory must pay to inspect it, and between inspections it acts on a belief rather than on the state. The observation cost model (OCM) makes this precise for a finite Markov chain: at each time the controller either pays a fixed cost to observe the state and choose a new action, or keeps the previous action without observing. Reisinger and Tam (arXiv:2201.07908v3, published in Mathematics of Operations Research, 2025) show that, after augmenting the state with the time elapsed since the last observation, the dynamic programming equation of the discounted OCM is a discrete quasi-variational inequality (QVI): an obstacle problem whose obstacle depends on the unknown itself.
Earlier work on the OCM (Anderson and Friedman, 1977; Hajek, Mitzel and Yang, 2008) treated fixed dynamics of the underlying chain. Discrete QVIs with interconnected obstacles and their penalty approximation were analysed by Reisinger and Zhang (2019) for switching problems, with the identity matrix in place of the transition operator . The paper recasts the OCM QVI in an abstract form and proves it is well-posed.
Let be a finite state space and a finite nonempty action set. The unknown is a function with components . A driver is a family , ; its third argument is the vector and its fourth the whole function . Given a sequence of substochastic matrices on (nonnegative entries, row sums at most ) and a vector , the inspection operator is
It reads only at time and couples all actions. The QVI (3.1) is
Assumption 3.2 asks for a constant with whenever are bounded and , together with boundedness in and uniform continuity in . Assumption 3.12 asks that depend on only through finitely many values. For the OCM, .
For the computation the paper truncates time to , giving a finite QVI (3.7) for a map with the monotonicity property (3.5), and replaces it by the penalised problem (3.8), , with a continuous non-decreasing penalty vanishing exactly on .
Under Assumptions 3.2 and 3.12, a uniform bound , and :
The well-posedness theorem identifies the value function of the discounted observation cost model as the unique bounded solution of a QVI, which is what justifies computing it: truncating time and penalising the obstacle gives a sequence of finite nonlinear systems whose solutions converge to it, and these systems are solved in practice by semismooth Newton iterations. The abstract framework covers other models with a non-local, action-coupling obstacle, such as discretised switching problems.
The results are proved in the paper, partly by reference: existence of the penalised solutions and the convergence are delegated to Reisinger and Zhang (2019, Theorems 2.5 and 2.6), and Lemma 3.11 is stated as "a direct adaptation" of a lemma there. None of the results is formalized. A formal development makes the delegated steps explicit and fixes the hypotheses under which the statements hold (see Formalization scope).
The comparison principle (Proposition 3.3) is a maximum principle on an infinite index set: the supremum of need not be attained, so the argument works along maximising sequences and needs the uniform continuity of the driver in . In the obstacle branch, the inspection operator transports the maximum to time , and excluding that case uses through a chain argument over the finite set ; with comparison fails.
Existence is harder. A direct fixed-point argument fails because the driver is only monotone, not a contraction, and the obstacle depends on the unknown. The paper's route goes through two limits, and , each requiring bounds uniform in the other parameter and a passage to the limit in a nonlinear, non-local equation; the limit uses Assumption 3.12 to localise the dependence on .
Everything is finite-dimensional or a function on the discrete set ; no measure theory is involved. Unknowns are curried as u n x a , costs as c a x. Time in (3.1) ranges over all of , including , and is u 1. The truncated time set is Fin N with the index standing for time , so is u 0. Substochastic means nonnegative entries with row sums at most ; and are componentwise; norms are sup norms, written out entrywise. Bounded sets of in Assumption 3.2.2 are cubes.
Two additions to the paper's hypotheses are made, each because the statement is false without it. The goal assumes : Assumption 3.2.2 only bounds for each fixed , and the driver satisfies both assumptions yet has no bounded solution. Corollary 3.4 is stated for bounded solutions of (2.11). The truncated QVI is stated without Problem 3.6's time boundary condition , which (3.8) does not encode. The continuity of the restricted driver claimed in Lemma 3.5 is not part of that milestone; the truncated part of Theorem 3.13 takes continuity of an abstract as a hypothesis.
The clause of Theorem 3.13 (", monotone from below") is not stated: the paper does not define the truncated operator beyond time , and with the zero extension the monotonicity in fails. The goal keeps the clause's well-defined content, existence and uniqueness of the bounded solution. A goal asserting only uniqueness (Proposition 3.3), or existence with the uniform bound hidden inside a definition, would be a different theorem; the bound is an explicit hypothesis.
A complete development needs solvability of finite-dimensional monotone nonlinear systems (the existence result cited from Reisinger and Zhang), monotone convergence in finite dimensions, and maximum-principle arguments on . The comparison principles and the a-priori bound are reusable for other monotone schemes. Proofs of any milestone, and alternative existence arguments for the goal, are welcome.
A Markov decision process (MDP) models sequential decisions under uncertainty: in each state a decision maker picks an action, collects a reward, and the system moves to a random next state according to a transition kernel. In applications the kernel is estimated from data, and an optimal policy for the estimated kernel can perform poorly under a slightly different one. Robust MDPs replace the single kernel by an uncertainty set and maximize the worst-case discounted reward over that set (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013).
Goyal and Grand-Clément (arXiv:1811.00215v8) introduce r-rectangular uncertainty sets, in which transitions are mixtures of a small number of uncertain factors chosen independently by an adversary. Beyond the algorithmic results (the subject of the first mission of this series), they prove two structural properties of optimal robust policies in this model: a robust maximum principle and robust Blackwell optimality.
In a classical MDP, a policy is Blackwell optimal if it is optimal for every discount factor close enough to (Blackwell 1962; Puterman 1994, §10.1.2). Blackwell optimal policies are optimal for the long-run average reward and for every finer -discount criterion, so they connect discounted and average-reward control. For two-player perfect-information zero-sum stochastic games the existence of Blackwell optimal strategies is due to Gaubert and Gunawardena (1998). Goyal and Grand-Clément establish the analogous statement for robust MDPs with r-rectangular uncertainty, under the assumption that the factor sets have finitely many extreme points, as polyhedral factor sets do.
Let and be finite sets of states and actions, with rewards , an initial distribution , and a discount factor . Fix coefficients , , with . A factor matrix has probability vectors as columns and induces the kernel
The adversary chooses from a nonempty convex compact set . Its projections are the factor sets , and is r-rectangular when .
A stationary policy picks in each state; it is deterministic when each is a point mass. With and , the value function and the expected reward are
The worst-case value of is . A pair is an optimal solution of the robust MDP problem (1.2) at discount when maximizes over and attains . The Lean development uses this notation: value, R, z, IsRobustSolution, IsRRect, factorSet, IsDeterministic.
If is r-rectangular and every factor set has finitely many extreme points, there exist a deterministic policy , a factor matrix and with
The pair is fixed before and does not depend on . The statement fixes no constant and no rate.
Under the same hypotheses there are and, for each , a single deterministic pair optimal for every .
The result. Robust Blackwell optimality says that, for polyhedral r-rectangular uncertainty, a decision maker who is patient enough does not need to know the discount factor exactly: one deterministic policy is robust-optimal for all discounts near , and the adversary has one matching worst-case factor matrix. This is the robust counterpart of the classical bridge from discounted to average-reward criteria, and it is the natural entry point for a theory of robust MDPs under the long-run average criterion, for which the paper notes no results were known. The robust maximum principle states that an optimal robust policy has the highest worst-case value from every starting state, a comparison that has been used to derive structural properties of robust policies in a healthcare setting (Grand-Clément et al. 2020, cited on p. 13 of the paper).
Formalizing it. The results are proved in the paper; none has a machine-checked proof. The nominal analogues (Blackwell 1962, Theorem 5, and the rationality of the discounted value) are posed on Prove2Me as open targets on a different, nominal model and are not reused here. The formalization also corrects two printed statements: Proposition 6.1 is false for an initial distribution with a zero entry and is posed with , and the claim in Appendix G.1 that the factor matrix of a solution is an extreme point is posed in its existential form, the form the proof uses.
The obvious argument for the goal is a pigeonhole over the finitely many candidate pairs (deterministic policies and extreme factor matrices): some pair is optimal for discounts . The step that fails is passing from this sequence to a whole interval. Optimality of a pair is not a comparison between two fixed rational functions of : the worst-case value is a minimum over , and optimality quantifies over all randomized policies. A comparison of worst-case values at one discount does not by itself give a comparison of value functions that can be propagated to other discounts. The paper bridges this gap with the robust maximum principle, which turns a worst-case comparison into a statewise comparison of two value functions, each rational in . The maximum principle itself rests on the saddle-point structure of r-rectangular robust MDPs (Theorem 4.2 and Lemma 4.3 of the paper), which a solver must develop.
All objects live in the definition FactorRMDP.Blackwell.Model. States and actions are finite types, with nonempty. Factors are indexed by Fin r, i.e. 0-based. A factor matrix is a function Fin r → S → ℝ. is a nonempty convex compact set of factor matrices with stochastic factors. Its factor sets are its projections, and r-rectangularity is the predicate IsRRect, not built into the structure. Rewards are nonnegative and . The value function is the discounted series, not a fixed point, so no Bellman identity holds by definition. Minima and maxima are stated with IsLeast/IsGreatest, and statements at a fixed discount assume . Optimality in (1.2) is over stationary randomized policies, as in the paper's proof, and requires both halves: maximizes and attains . "Finitely many extreme points" is Mathlib's Set.extremePoints of each factor set. The second sentence of Assumption 2.4 (an optimization oracle) is not formalized.
Explicit choices relative to the printed text:
A goal in which the pair may depend on would only restate milestone 3 and is not robust Blackwell optimality; the pair is quantified before .
A complete development needs the saddle-point theory of r-rectangular robust MDPs (shared with the first mission of this series), Neumann series and Cramer's rule for , extreme points of products of compact convex sets, and the finiteness of zeros of a nonzero polynomial. The rationality of discounted values and the extreme-point lemmas are reusable for nominal Blackwell optimality and for other robust models. Proofs of any milestone, of the optional Proposition 6.3, and auxiliary lemmas are welcome.
Finitely many rotations of the sphere generate a group whose orbits are typically dense. A basic quantitative question is how fast those orbits fill the sphere: after words of length in the generators, how uniformly are the points spread? The answer is controlled by the spectral gap of an averaging operator built from the generators. The question goes back to the Banach–Ruziewicz problem (uniqueness of rotation-invariant finitely additive measures on spheres), was studied by Lubotzky, Phillips and Sarnak in their work on distributing points on (LPS 1987), and was formulated as a conjecture about random generators by Gamburd, Jakobson and Sarnak. It also matters in quantum computing: a spectral gap for a gate set gives efficient approximation of every single-qubit gate by short gate sequences (Sawicki–Karnas 2017).
Timeline.
The tuples with algebraic entries form a Haar-null set, so the conjecture for random tuples remains open.
Let be the group of complex matrices with and , a compact group with its normalized Haar measure (the unique left-invariant Borel probability measure). For the Hecke operator acts on functions by
On it is bounded and self-adjoint, constants are eigenfunctions with eigenvalue , and it preserves the space of mean-zero functions. Writing for the supremum of the spectrum of on , one always has , and (or the tuple ) has a spectral gap when
For , each acts on the sphere by rotations, and is the operator of the source.
For every , if are chosen independently and uniformly (Haar) at random in , then with probability
By Fisher's law, the goal follows once a spectral gap is shown on a set of positive Haar measure.
A spectral gap for means that random walks driven by equidistribute in (and orbits equidistribute on ) at an exponential rate, and that the action of the generated group on is strongly ergodic. In quantum computation it says that a universal single-qubit gate set is automatically efficiently universal. The conjecture asserts that this holds for a typical gate set, not just for the arithmetically special ones covered by Bourgain–Gamburd.
On the formal side, the milestones are proved theorems (Fisher; Bourgain–Gamburd) that have, to the knowledge of this proposal, no machine-checked proofs. Formalizing any of them requires substantial new libraries: Haar measure and harmonic analysis on , ergodicity of on (Goldman), and the arithmetic-combinatorial machinery of Bourgain–Gamburd. The goal itself is an open problem.
Spectral gap is not detected by density alone: every tuple generating a dense subgroup gives an ergodic action, but ergodicity only shows is not an eigenvalue, not that it is bounded away from . Known proofs need either arithmetic structure (automorphic forms, or the algebraic entries used by Bourgain–Gamburd to rule out short relations that come too close to the identity) or rigidity (property (T)). A generic tuple has neither.
Matrix.specialUnitaryGroup (Fin d) ℂ with the subspace topology and its Borel σ-algebra; it is shown to be a compact topological group, and haarSU d is the Haar measure normalized to total mass .Useful reusable contributions include: basic harmonic analysis on compact groups (translation invariance in , self-adjointness of ), the Peter–Weyl decomposition of , conjugation invariance of the gap, and monotonicity of the gap in the generating set.
This mission develops Chapter 31 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the running-time bound for adiabatic optimization with a linear interpolation schedule.
Let be a cost function on -bit strings and let
be the problem Hamiltonian. Let be a beginning Hamiltonian on qubits and let for . Assume that is Hermitian and has a nondegenerate ground state for every . Write for the gap between the ground and first excited energies of , and . Norms of operators are operator norms.
There are absolute constants (the constants of the first- and second-order perturbation bounds used in the adiabatic theorem, Theorem 30.1) such that the following holds for every such , , . Let and suppose
If solves the Schrödinger equation on and is a unit-norm ground state of , then there is a unit-norm ground state of with
The bound reduces the question of how long the adiabatic algorithm must run to a spectral question: if is polynomially bounded and is polynomially bounded in , the running time is polynomial.
Formalization Note The ground state of is determined only up to a global phase, so the conclusion asserts the existence of some unit ground state of within distance . The constants are quantified existentially before all other data, as in the source, where they are introduced as "some constants". The minimum gap is the infimum of the gap over .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.