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?
Many decisions are made by assigning one of several actions to an individual on the basis of observed features: which of drugs to prescribe, which of several promotions to show, which job-training programme to offer. Experimentation is often costly or unethical, while historical records of past assignments and their outcomes are plentiful. Offline policy learning asks for a rule that maps features to actions, chosen from such observational records, whose expected outcome is close to that of the best rule in a prescribed class. The binary-action case was settled by Kitagawa and Tetenov (2018) with known propensities and by Athey and Wager (2021) with estimated ones; Zhou, Athey and Wager extend the doubly robust approach to actions. This mission formalizes the statistical half of that paper: the regret guarantee of its cross-fitted learner.
Timeline. Robins, Rotnitzky and Zhao (1994) introduced augmented inverse-propensity weighting (AIPW). Dudík, Langford and Li (2011) used doubly robust scores for multi-action policy evaluation and optimization. Chernozhukov et al. (2018) showed that cross-fitting removes the bias of flexible nuisance estimates in semiparametric estimation. Athey and Wager proved -rate regret for binary actions with VC classes. Zhou, Athey and Wager (arXiv 2018; Operations Research, 2023) treat actions with a Hamming entropy integral as the complexity measure.
There are actions, written and identified with the standard basis vectors of , so that for the inner product is the coordinate . A draw consists of features , potential outcomes and a logged action ; only the triple with is observed. The data are iid draws.
The model consists of a law of the features and two conditional laws given : one for the outcome vector, one for the action. Given the two are independent (unconfoundedness). The propensity is and the mean reward is . A policy is a map from a class . Its value is and its regret is .
The learner, CAIPWL (Algorithm 1), divides the sample into evenly sized folds. For each fold it fits estimators , on the observed data outside fold , forms the cross-fitted AIPW score
and returns a maximizer over of . The oracle score is the same expression with the true and ; it gives . Write , , for the differences , , , and
The complexity of is measured through the Hamming distance on points . The covering number is the supremum over all finite point sequences of the least number of policies of that -cover in . The entropy integral is .
The assumptions are: overlap, ; bounded rewards, ; Assumption 2, ; and Assumption 3, with .
read per : for every there are and with for all . This is the paper's own "simpler way of stating the regret bound in Theorem 3". It fixes the rate and the dependence on and , but no constants.
The theorem shows that a learner can use flexible machine-learning estimates of the propensities and outcome regressions, each converging more slowly than , and still attain the regret rate of an oracle that knows them, provided the product of their errors is . This doubly robust rate condition is what makes cross-fitted AIPW scores usable for policy learning with random forests, boosting or neural-network nuisances. The dependence on only through covers the multi-action classes the paper uses later, such as depth- decision trees.
On formalization: the result is proved on paper, with explicit constants that are not established as printed. No machine-checked proof of any part of it is known. A complete development would give a checked doubly robust policy-learning guarantee with the hypotheses a correct proof needs, stated explicitly. It would also deliver, as by-products, a checked uniform-entropy bound for empirical processes indexed by policy differences and a cross-fitting lemma with fold-wise conditional independence.
Two parts are hard. The oracle concentration needs a chaining (Dudley-type) bound for the empirical process , indexed by pairs of policies, in which the covering numbers are uniform over point sets and the entropy integrand uses . Bounding one fixed pair by a central limit theorem is not enough, because the supremum over is the whole point. Lemma 3 needs the conditional independence that cross-fitting creates: given the data outside fold , the terms of fold are iid with conditional mean zero in the first two error terms of (17). The uniform bound then comes from a localized chaining argument whose radius shrinks with the nuisance errors. A naive argument conditioning on all the data at once loses the mean-zero structure.
Actions are Fin d; policies are deterministic maps X → Fin d (endnote 3, p. 45), and a class is Pol : Set (X → Fin d). The model is a probability measure PX with two Markov kernels κY, κA, and the joint law is PX ⊗ₘ (κY ×ₖ κA). This builds unconfoundedness into the law. The sample of size is the product measure on Fin n → Draw X d. Estimators of fold are functions of the observed triples indexed by {i // fold n i ≠ k}, so they cannot see fold or unobserved potential outcomes. The regret uses in place of . is an ℝ≥0∞ lower integral, finite under Assumption 3. and are read for each separately: Definition 8's " with probability " presupposes one probability space for all . Bounded support is stated for each under κY x.
Hypotheses added to the printed ones:
Without (ii) and (iii), Lean's integrals of non-measurable functions are and Assumption 2 would be vacuous. The hypotheses are satisfiable: the oracle estimators , meet every estimator condition, and a finite class of constant policies meets Assumption 3 and permissibility. The degenerate cases or force zero regret, so the goal is not trivialized there.
Needed infrastructure: product measures and kernels (Mathlib), and Hamming covering numbers (local, Definition 4). Still to build: uniform-entropy chaining for bounded classes, and Talagrand/Bousquet-type concentration. Contributions are welcome on the chaining bound, the cross-fitting conditional-independence lemma, and the elementary items (48), (17) and Lemma 1(1). These are reusable in any doubly robust estimation mission.
A firm that relies on employees to process transactions can lose money when errors remain undetected. Inspection catches errors, but each inspection costs money, and employees may change their care when they know when an inspection will occur. These effects make the timing of inspections part of a contract design problem, not just a scheduling choice. Kim and Xu study that problem in a continuous-time principal–agent model of operational risk. Their SSRN preprint proves that the ranking of two common inspection policies changes with the cost of inspection: periodic inspection is better at low cost, while random inspection is better at high cost (Proposition 4, p. 17). This mission targets that result in the authors' July 2023 preprint, whose numbering is used throughout.
The comparison matters because neither inspection policy has an unconditional advantage in the model. A periodic schedule fixes the time until the next inspection; a random schedule makes that time uncertain. The agent responds to the schedule through effort, while the firm pays both for inspections and for errors left unresolved. Choosing a policy by its inspection frequency alone therefore misses a change in the agent's response and in the duration of losses. The paper develops both policies' optimal contracts before comparing their payoffs Kim and Xu, §§3–4.
The principal is a firm and the agent is an employee. The firm earns base profit at rate . The agent chooses a nonnegative effort path , where is time since the last inspection, at unit cost . Errors arrive at aggregate rate , with . Each unresolved error causes expected loss per unit time until the next inspection finds and corrects it. The paper begins with several error classes, then uses their aggregate arrival rate and rate-weighted mean loss for the remainder of the analysis (7), p. 10.
The firm chooses an inspection frequency , a penalty charged to the employee per error found, and a wage . Under the random policy , the time between inspections is exponentially distributed with rate ; under the periodic policy , it equals . The employee chooses a best response to the announced policy and contract. The employee must receive at least the reservation payoff . Both parties discount future payoffs at rate . An inspection costs the firm per cycle. Equations (1) and (3) specify their discounted payoffs; equation (6) gives the firm's reduced payoff when participation binds §3, pp. 8–10.
The standing Assumption 1 is and , with . The first inequality excludes the paper's degenerate no-effort regime; the second ensures that the adjusted base profit exceeds the expected operational loss of the uninspected benchmark (7), p. 10. In the formalization, all six parameters are also positive, as stated in §3.
The goal is Proposition 4. For fixed model parameters there is one inspection-cost threshold , independent of the particular positive cost , such that
Here and are optimal feasible strategies under the respective inspection laws. The paper does not specify which policy is better at , and the formal goal does not add an equality claim there Proposition 4, p. 17.
The milestones first connect binding participation to the firm's reduced payoff in (6). Lemma 3 identifies constant optimal effort under random inspections and its threshold ; Lemma 4 identifies the time-dependent effort under periodic inspections and its threshold . The two statements in §4.2 then express the firm's reduced payoff through the explicit random branches of (EC.2) and periodic branches of (EC.4) pp. 10, 13–14 and ec5–ec6. These targets fix the model and its regime changes before solvers address the policy-level optimization.
The result distinguishes regimes in which a predictable inspection date pays off from regimes in which an uncertain one pays off, after each policy's frequency, penalty, wage and induced effort are optimized. It is a claim about the principal's optimal payoff under complete contracts in the paper's model. It does not assert that either schedule dominates for every fixed frequency or penalty. The strict comparisons matter: they identify a genuine reversal rather than a weak inclusion of one policy's feasible strategies in another's Proposition 4, p. 17.
Kim and Xu proved this proposition in the cited preprint; the open work in this mission is to give its stated model, supporting results and comparison a machine-checked Lean proof. The definitions of inspection laws, achievable payoffs and discounted cycle quantities can also support the paper's separate hybrid-policy comparison and future formal work on continuous-time inspection contracts. The closed-form payoff branches provide testable interfaces between the economic model and the optimization results. The mission does not claim that any of these proofs is already machine checked.
The direct intuition that unpredictable inspections should always restrain delayed effort fails as a policy comparison. Under a periodic schedule, the employee can increase effort near the known inspection time, but earlier inspection also shortens the time that errors remain costly. The relative effect depends on and on which effort regime is optimal. An argument based only on the employee's response at a fixed cannot determine the ranking of the principal's optimized payoffs. The paper's characterization of each policy includes both effort inducement and error correction modes, with different closed forms and cost thresholds §4.2, pp. 14–15; proof of Proposition 4, pp. ec30–ec33.
Lean represents an effort path as a real-valued function of time since the last inspection. It is measurable, nonnegative and bounded. The last condition is a disclosed modelling pin: it ensures that the real-valued expected effort and error terms do not acquire Lean's default zero value for a nonintegrable function. The random interval law is Mathlib's exponential measure; the periodic law is a Dirac measure at . The error classes are aggregated using and , and expected errors are . This starts at the discounted cycle payoff equations (1) and (3), rather than reconstructing the underlying Poisson and Brownian processes §3 and Appendix EC.4.1.
Feasible principal strategies require , , a best-responding agent and the participation constraint. This makes the formulas meaningful. The agent's best-response test sets , because wage enters payoff additively and cannot change which effort is optimal. A policy comparison uses achievable payoffs: it asserts an achievable payoff for the better policy exceeding every achievable payoff of the worse policy. That formulation avoids default values of a real supremum over an empty or unbounded set. It also prevents an empty feasible set from satisfying a comparison vacuously. The threshold is quantified before , and the source does not explicitly require it to be positive. Formulas dividing by are invoked only when ; the zero-penalty case has a separate statement.
This initial mission includes the model, the effort lemmas, the two payoff-regime statements and Proposition 4. Characterizing the globally optimal random and periodic contracts and their comparisons remains welcome solver work; their long closed-form optimization results have not been weakened into easier draft milestones. Reusable contributions include integration facts for the exponential and Dirac laws, best-response characterizations up to almost-everywhere equality, and analytic properties of the payoff branches.
Graph alignment asks for the correspondence between the vertex sets of two graphs that are noisy copies of each other. It underlies the de-anonymisation of social networks, where an anonymised graph is matched to a public one (Narayanan, Shmatikov 2009), the comparison of protein–protein interaction networks across species, and matching problems in computer vision. The standard random model for studying when alignment is possible is the correlated Erdős–Rényi model (Pedarsani, Grossglauser 2011).
In that model, exact recovery of the hidden correspondence and almost exact recovery (all but a vanishing fraction of vertices) have sharp thresholds: exact recovery by Cullina, Kiyavash 2016 and 2017; almost exact recovery when by Cullina, Kiyavash, Mittal and Poor (arXiv:1809.03553). Hall and Massoulié (arXiv:2007.00533v5, Operations Research 2023) study partial recovery, the recovery of a constant fraction of the correspondence, in the sparse regime , where almost exact recovery is impossible. This mission formalizes their possibility result, Theorem 2.3. Its companion mission (Partial Recovery in the Graph Alignment Problem I) formalizes the impossibility result, Theorem 2.1.
Fix and parameters with . A parent graph on includes each edge independently with probability . Two copies are made, and each copy keeps every edge independently with probability . The resulting graphs and have adjacency matrices and . For each unordered pair of distinct vertices, has the law of display (3):
independently over the pairs. The covariance of and is (display (2)), which is positive when .
A planted permutation relabels into the observed graph : . An algorithm sees and returns a permutation . Its quality is the overlap
For , a permutation is good (Definition 2) if at least vertices have degree at least in the intersection of with relabelled by :
In Lean, these objects are pLaw, Config, cfgProb, prob, A, B', B, overlap, good and Cond6 in GraphAlignment.Possible.
Let and let , be sequences. Suppose there exist such that, for all large ,
Then some algorithm returns with
The result. Theorem 2.3 shows that partial alignment is information-theoretically achievable in the sparse regime , provided is above an explicit constant depending on . Together with Theorem 2.1, it locates partial recovery between a necessary condition stated through the divergence and a sufficient condition stated through . It complements the almost-exact-recovery results for , which do not apply when stays bounded. The moment generating function computation of Lemma B.2 and the inequality of Lemma B.1 were reused for the sharp exact-recovery threshold by Wu, Xu, Yu (p. 9 of the source).
Formalizing it. The theorem is proved on paper; no part of it is machine-checked. The paper's route to Proposition 4.2 applies a -core theorem for with fixed and an integer, at and , which vary with and need not be integers. The statement of Proposition 4.2 remains true, but a formal proof needs a different argument. Proposition 4.4's union bound contains two repairable gaps: an infimum taken over instead of , and the bound . A formal development would settle the theorem under exactly the conditions (6).
The natural first step is to compute for a fixed wrong permutation and take a union bound over all permutations. The difficulty is that for the terms are not independent: an edge variable enters several terms along the cycles that induces on vertex pairs. A Chernoff bound therefore needs the moment generating function of a sum over each cycle of pairs. That is a transfer-matrix computation, and the per-cycle bounds must then be recombined uniformly in the cycle lengths. The resulting exponent must beat . This is where the sparsity conditions and , and the constant , enter. Proposition 4.2 is a concentration statement for the number of vertices of degree at least in the intersection graph, an Erdős–Rényi graph , when is only a large constant.
Everything is finite. Vertices are Fin n and permutations are Equiv.Perm (Fin n). A configuration assigns Bool × Bool to each non-diagonal element of Sym2 (Fin n), and probabilities are finite sums of the product weights. They are not taken against a free measure, so the model is a genuine probability space whenever . The standing assumptions for every (p. 5 and the running assumption on p. 7) are hypotheses of the asymptotic statements. The paper's remark "we assume " (p. 6) is used by neither result and is not imposed. Logarithms are natural, "" is a limit along , and the thresholds and are real numbers, not floored.
In the goal, an algorithm is a family of maps from the observed pair to a permutation. It is chosen before the planted permutations and may depend on , , , , but never on . This rules out the trivial algorithm "output ". The theorem does not say how is drawn, so the limit is required for every sequence of planted permutations, which covers the uniform case. "Exponential time" is not formalized.
Three statements are posed in a corrected reading, each disclosed in its Formalization Note. In Lemma 4.3, and : the paper allows and , where and (13) are undefined, and Lean's convention would make the bound trivial. Display (10) is stated for an arbitrary permutation . Only the "in particular" clause of Lemma A.2 is stated, because the paper's proof of the general normal-approximation bound does not hold as written. Lemma 4.1 (a -core theorem of Pittel, Spencer and Wormald) is not posed.
A complete development needs: Chernoff bounds for finite sums of dependent Bernoulli variables via the transfer-matrix formula, binomial and Poisson tail estimates, and the cycle decomposition of the action of a permutation on unordered pairs. Lemmas B.1, B.3 and 4.3 are general-purpose and reusable. Proofs of any milestone, and alternative proofs of Proposition 4.2 that avoid -cores, are welcome.
The source is the arXiv preprint v5, whose appendices contain the proofs that the main text defers to an electronic companion.
Online platforms such as ride-hailing, delivery and advertising marketplaces routinely test new pricing or matching policies on a single market. Randomizing over users is often impossible there: every rider and driver in a city shares one supply pool, so treating some users and not others contaminates the control group. The standard alternative is a switchback experiment: the whole market alternates between the new policy (treatment) and the current one (control) over time, and the effect is estimated from the time series of outcomes. Switchbacks are in production use at ride-hailing and delivery firms (see the industry references in Bojinov, Simchi-Levi and Zhao, 2023).
The design question is when to switch. Switching often produces many nearly independent observations, but a policy change has carryover effects: an outcome is affected by the policy of the last few periods, not only the current one, so frequent switching leaves few periods whose recent history is purely treated or purely control. Bojinov, Simchi-Levi and Zhao formalize this trade-off in a design-based, minimax framework and solve it in closed form. This mission formalizes that solution.
Time is divided into periods . An assignment path is , with meaning treatment. For every period and every path there is a fixed, unknown potential outcome ; the collection is . Randomness comes only from the random path .
Three assumptions restrict :
The set of outcomes satisfying all three is . Under 1–2, and denote the outcome after consecutive treatments, respectively controls. The estimand is the average lag- effect
A regular switchback design fixes randomization points , , and probabilities . At each an independent coin with success probability is flipped, and its outcome is applied to the periods (with ). The Horvitz–Thompson estimator weights the outcome of each period whose window is all ones (all zeros) by the inverse probability of that event. Its risk is the mean squared error
where the expectation is over the law of the path. A design is minimax optimal if it minimizes the worst-case risk over all regular designs.
The goal asserts both existence and uniqueness, and it compares against every regular design with arbitrary probabilities in .
In attack order:
(Lemma EC.2), and fair coins (Theorem 1). 5. The fair-coin moments (Lemma EC.6). 6. The structure of optimal point sets (Lemmas EC.7 and EC.8). 7. The closed-form risk (EC.8) (Lemma EC.9). 8. The integer optimum of the subset selection objective (7) at :
attained only at .
These are not milestones:
The result. Theorem 2 turns a design question into a rule: randomize once every periods, except that the first and the last epoch last periods. The rule depends only on the carryover order , not on or on the outcome model. A practitioner who chooses the period length close to the carryover duration gets a design that is robust to a short carryover, since the optimal designs for and nearly coincide. The fair-coin result (Theorem 1) keeps the inverse-probability weights at powers of , which avoids the instability of Horvitz–Thompson estimators with extreme propensities. The same design underlies the paper's asymptotic normality result and its confidence intervals (mission 2 of this series).
Formalizing it. The results are proved in the paper; none of them is machine-checked. The formalization has to make the paper's finite-sample expansion of the risk exact, establish its integer optimum, and connect it to a genuine minimax statement over all regular designs, not only over fair-coin designs. It also pins down where the printed statements need hypotheses. As printed, the first sentence of Theorem 2 and Lemma EC.7 fail for short horizons (at , the minimax-optimal point sets are and , while (7) is minimized by ). Their corrected forms are stated here. The strictness part of Lemma 1 fails at (with , , fair coins, outcomes in period 1 and in period 2 tie with ); it is stated for .
The risk is a quadratic form in the reduced outcomes whose coefficients depend on the combinatorics of the point set. The coefficients are products of inverse probabilities over the determining randomization points of each window and over the overlaps of two windows. Writing the risk in closed form requires a case analysis of how windows of length meet the blocks of the design. The paper's closed form (EC.8) holds only under three structural conditions on the points. Showing that every optimal design satisfies them (Lemmas EC.7, EC.8) needs exchange arguments that remove or move a point while keeping the design regular, and these break down at short horizons.
The step from the closed form to the explicit optimum is an integer program. The paper solves its continuous relaxation and observes that the relaxed optimum is integral. A formal proof must handle every point set, including those that violate the structural conditions and for which (EC.8) is not the risk. The obvious approach of minimizing (EC.8) directly is therefore not enough: the minimax optimum must also be compared with designs outside the class where (EC.8) applies.
Lean represents a path as a function of which only the indices are read, potential outcomes as a function of the period and the whole path, and the point set as a Finset ℕ. Probabilities are indexed by the randomization point (). The expectation under the law of a regular design is the finite sum over the coin vectors.
Committed conventions:
Minimax optimality is the statement "for every regular design and every admissible there is an admissible whose risk under the other design is at least the risk of under this one". No supremum over outcome functions is ever taken. are the constant outcome functions .
Added hypotheses.
Not a trivialization. The goal mentions neither the objective (7) nor the structural conditions, nor the closed form (EC.8). It is stated against the full class of regular designs and asserts existence. A proof cannot replace it by " minimizes (7)" (that is a milestone), and Theorem 1 is not vacuous because the goal asserts that optimal designs exist.
A complete development needs finite expectations over independent coin flips, the risk expansion as a quadratic form, and an integer optimization argument. The first two are reusable for the second mission of this series and for other design-based analyses of Horvitz–Thompson estimators. Proofs of any milestone, and of the companion statements, are welcome independently.
The quantum approximate optimization algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits, indexed by an integer depth , that prepare states whose computational-basis measurements are biased toward good solutions of a combinatorial optimization problem. It became the standard candidate for optimization on near-term quantum hardware, and its performance on MaxCut is the benchmark against which later analyses and experiments are measured.
The original paper proves one concrete performance guarantee: at depth , on 3-regular graphs, the algorithm achieves an approximation ratio of at least . Short timeline:
A graph has vertex set , and 3-regular means every vertex has exactly three neighbours. Each vertex carries a qubit; a computational basis state is a bit string . For an edge the clause is if and otherwise, and the cut objective is
the number of edges cut by the bipartition defines. As an operator, is diagonal in the computational basis.
Let and let . For angles , the depth-one QAOA state and its expected cut are
The angles may be restricted to , by periodicity.
Two kinds of small subgraphs govern the analysis. A crossed square is a set of four vertices spanning exactly five edges (a 4-cycle with one diagonal). An isolated triangle is a triangle whose three outgoing edges end on three distinct vertices. and denote their numbers in . Finally, for an edge the subgraph type is the shape of the edge together with its adjacent edges; in a 3-regular graph there are three types , according as and have two, one or no common neighbours. Each type defines a function , the expectation of the clause of the central edge in the depth-one QAOA state of the subgraph alone.
For every connected 3-regular graph there are angles , with
that is, . The constant is exactly the paper's , and is included.
The paper's argument passes through the following claims, each a milestone:
The result is the first rigorous worst-case guarantee for the QAOA, and the method behind it (the expected objective is a sum of local terms, each depending only on a bounded neighbourhood of an edge) is the template for every later analysis of fixed-depth QAOA on bounded-degree graphs. It shows that a depth-one circuit, of depth independent of , achieves a constant approximation ratio uniformly over an infinite class of graphs.
The paper's proof is complete apart from one numerical step: the minimization of (35) is reported as a numerical evaluation. No machine-checked version of the result exists. A formal proof requires an exact evaluation of the three subgraph functions at suitable angles, an exact combinatorial count of edge types, and a certified inequality in place of the numerical minimization. The margin is small: the exact minimum is , about above the paper's constant.
The light-cone reduction (milestone 1) is the conceptual step: one must show that conjugating a two-qubit clause by and leaves an operator that involves only the qubits adjacent to the edge, and that the remaining qubits contribute a factor of one. In matrix form on -dimensional space this is a statement about tensor-product structure that the definitions do not make visible. The combinatorial count (milestones 2–4) needs a careful case analysis of how triangles sit in a cubic graph, including the exceptional graph , where the count fails. The final inequality (milestone 6) has a margin of order , so crude bounds on the trigonometric functions do not suffice.
Qubits n = Fin n → Bool from the published QAlgorithms layer, with true the bit . States are vectors in EuclideanSpace ℂ (Qubits n); , as a diagonal operator, and the QAOA unitary are the published definitions uniformState, problemHamiltonian, qaoaMixer, qaoaUnitary. The latter takes mixer angles before phase angles.SimpleGraph (Fin n) with decidable adjacency; "3-regular" is IsRegularOfDegree 3. The cut counts each edge once. is defined as , which equals because is diagonal. The constant is the exact rational .Platform markets often feature a Superstar: a single complement whose presence moves consumers, such as a blockbuster game on a console or a star streamer on a video platform. Whether such a Superstar signs an exclusive deal with one platform or stays available on both is a recurring question for competition authorities and for platform managers. Empirical work documents both sides of the effect. Exclusive titles help small consoles challenge incumbents (Lee 2013). Superstar apps generate demand-discovery spillovers for small developers (Ershov 2020, NET Institute working paper). When a star streamer switched platforms, viewers followed and other content producers repositioned (Förderer & Gutt 2021, working paper).
Carroni, Madio & Shekhar (Management Science, 2024) build a two-sided Hotelling model with three groups of agents: consumers, a fringe of small complementors, and the Superstar. The model asks how Superstar exclusivity changes prices, participation and welfare. This mission formalizes the paper's analysis of the complementor side under vertical separation. The analysis runs through the equilibrium prices (Lemmas 1–3) and the sorting of complementors into multihomers, singlehomers and inactive firms (Proposition 1). It ends in the welfare result that exclusivity raises complementors' total surplus (Proposition 3).
Two platforms and sit at the ends of a Hotelling line. A unit mass of consumers has types , distributed with cumulative distribution function and density . The type measures the preference for platform over platform . The Superstar is worth to a consumer of a platform that hosts it, and records its presence on platform . A consumer of type joins platform rather than when
where are the consumer prices, the masses of complementors on the platforms, and the value of a unit mass of complementors to a consumer. Platform 's consumer share is and platform 's is .
Complementors have an opportunity cost of joining each platform, distributed with mass function and density . A complementor receives per unit mass of consumers, so it joins platform if and only if , and . A complementor that joins both platforms pays twice.
Expectations are fulfilled: the share solves the fixed-point equation
Platforms choose prices simultaneously to maximise gross profit . Under exclusivity the Superstar is on platform only (); under non-exclusivity it is on both (). The paper's standing assumptions are smoothness and symmetry of , a positive nondecreasing density , and Assumption 3: , which keeps cross-group externalities below the differentiation parameter. The complementors' total surplus at shares is
For , let be platform 's share in the selected exclusivity equilibrium and the share in the symmetric non-exclusive equilibrium. Then
The statement fixes no functional forms and no constants. It holds for every model satisfying the assumptions and every .
The result says that a Superstar's exclusive contract, usually discussed as a tool of foreclosure against the rival platform, benefits the fringe of complementors taken as a whole. Some complementors stop paying for a second platform. Others, inactive without exclusivity, enter on the favoured platform. The comparison feeds into the paper's welfare analysis (consumer surplus, Proposition 4) and into its account of when the Superstar chooses exclusivity (Proposition 5). It supplies a theoretical counterpart to the empirical spillover findings cited above.
The paper's proofs are informal in places that matter. Equilibrium selection under fulfilled expectations is described in words only, and the derivative argument for Lemma 3 tracks an equilibrium as a function of without saying which one. A formal development has to fix these choices, and this mission fixes them explicitly (see Formalization scope). None of these results has been machine-checked before. The fixed-point and first-order machinery for two-sided fulfilled-expectations demand would also serve other platform-competition models in the Armstrong (2006) tradition.
The surplus comparison itself is elementary once the equilibrium shares are known. The work lies in the equilibrium shares. Fulfilled-expectations demand is defined by a fixed point that can have several solutions, so neither the share at a deviation price nor the equilibrium share is a priori a function of prices. The obvious first step, "impose symmetry", does not prove that the non-exclusive share is . One must show that is the only interior fixed point at equal prices. Likewise, the exclusive share exceeds only for the equilibrium reached continuously from the symmetric one. Coordination on the disfavoured platform is a fulfilled-expectations outcome the model does not exclude. Lemma 1 needs a differentiable local branch of the fixed point at a deviation, which is where Assumption 3 enters.
Everything is real-valued. The model is a structure with , functions , and the following hypotheses:
Several conventions depart from the paper's wording:
Fulfilled-expectations demand is a relation, not a chosen function. A price equilibrium is a Nash equilibrium in prices in which no deviation is profitable for any fulfilled-expectations share it induces. Lemma 1's formulas are a theorem about this equilibrium, not its definition. The symmetric non-exclusive outcome is the interior equilibrium at equal prices. The exclusive outcome is the end point, at value , of a continuous path of interior equilibria of the games with Superstar value , starting from equal prices at . Platform 's share is always .
The goal must not be posed with , or as a hypothesis: since is strictly convex and symmetric about , any of these would reduce it to a calculus exercise. The price ranking in Lemma 3 is not part of the mission. Its proof rests on bounds on that the paper states only as functions of unspecified equilibrium arguments.
The needed infrastructure is the implicit function theorem in one variable, interval integrals of continuous functions, and the intermediate value theorem. Contributions are welcome on any milestone, on alternative proofs of the goal, and on reusable lemmas about uniqueness of fulfilled-expectations fixed points.
Experiments that prepare many-body entangled states (GHZ, W, stabilizer, cluster and matrix product states) need a way to check that the device produced the intended state. Full quantum state tomography answers the question but its cost grows with the dimension of an -qubit system: a reconstruction needs on the order of measurement settings. Entanglement witnesses are cheap but exist only for special states.
Direct fidelity estimation (S. T. Flammia and Y.-K. Liu, arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011; the same idea appears in M. P. da Silva, O. Landon-Cardinal and D. Poulin, arXiv:1104.3835) estimates only the one number the experimentalist needs, the fidelity of the prepared state to the target pure state . It measures a constant number of randomly chosen Pauli observables, independent of , and needs only single-qubit measurements. The method has since become a standard benchmarking tool in experimental quantum information.
Consider qubits, . Let , ranging over the labels in , be the -fold tensor products of the single-qubit matrices . The characteristic function of a matrix is
The target is a pure state, with ; the prepared is an arbitrary state (positive semidefinite, trace one). For pure the fidelity is , and .
Given an additive error and a failure probability , the protocol runs in two stages.
copies of . Each measurement gives an outcome with mean , independently. The output is
For every , every pure , every state and every ,
the probability being over both stages of the protocol.
The guarantee says that Pauli settings suffice to estimate the fidelity of any -qubit state to any pure target, whatever . The number of copies of is in expectation in the worst case and constant for stabilizer states, while the paper's lower bounds show that full tomography with Pauli measurements needs a number of copies polynomial in . The same scheme, applied to the Choi state, certifies unitary channels and Clifford circuits.
The result is proved on paper but has not been machine-checked. A formal proof requires the Pauli-basis machinery (orthogonality and completeness of the -qubit Pauli operators), the Born-rule model of repeated Pauli measurements, and the combination of a second-moment bound with a sub-Gaussian bound through a two-stage union bound. The formalization also corrects a printed slip: the paper's equality (13) holds only as an inequality (see the milestone's note), which does not affect the result.
Each individual step is classical: Chebyshev's inequality for the first stage, Hoeffding's inequality for the second. The difficulty lies in the bookkeeping that the informal proof leaves implicit. The first-stage estimator involves , which is undefined at labels the sampling never produces, so every probability must be weighted by . The second-stage bound holds conditionally on the labels, and its sample sizes depend on them, so the two stages cannot be treated as one product of independent variables. The constant in Hoeffding's bound must be tracked through the factors of and of , and through the ceiling in . Finally, the Pauli expansion (2) requires the trace orthogonality of -fold tensor products, which is not in Mathlib.
Q n := Fin n → Fin 2, Pauli labels P n := Fin n → Fin 4; matrices are Matrix (Q n) (Q n) ℂ, and is the entrywise product . is the real number .WildeQIT.IsDensityOperator (positive semidefinite, trace one), referenced from the platform; purity is with .Nat.ceil, the natural logarithm.A complete development needs the Pauli-basis lemmas (Hermiticity, , trace orthogonality and the expansion of a matrix in the Pauli basis), a Born-rule lemma for observables, and Hoeffding and Chebyshev bounds specialised to finite product measures. The Pauli-basis lemmas are reusable well beyond this mission (stabilizer formalism, shadow tomography, randomized benchmarking). Proofs of any milestone, and of auxiliary Pauli-basis facts, are welcome.
A secretary problem asks a decision maker to choose one candidate from a sequence, without being able to recall a rejected candidate. Each arrival reveals how the candidate compares with those seen earlier, but the decision maker does not know the candidate's final rank. A classifier can provide an additional Yes or No signal about whether the current candidate is the best overall. The natural performance question is how much this signal improves the chance of selecting the best candidate when the number of arrivals grows. Dütting, Lattanzi, Paes Leme and Vassilvitskii give an exact finite linear program for this setting and an explicit asymptotic value. This mission makes the limit and its finite prerequisites precise.
The classifier's quality has two parameters with different meanings. Recall is the probability of a Yes signal for the top candidate. Specificity is the probability of a No signal for any other candidate. Both lie in , as in Example 5 of the paper. At the signal conveys no information, while is perfect advice. These endpoints matter to the statement rather than being omitted as special cases. Example 5, pp. 7–8.
There are arrivals, indexed by . Their ranks form a uniformly random permutation; the maximum rank is the candidate to select. At each arrival, the observer sees the relative ranking of candidates already seen and a signal from the classifier. An admissible decision can depend on this observed history and may use a stopping probability. It cannot inspect a candidate's hidden final rank. The paper shows that, for this signal model, the optimal stopping probability is characterized by a finite primal linear program. Sections 2 and 6.
For each round and signal, is a primal variable. Put . The program has constraints , and its objective is . Write for its optimal value. The constraints account for the chance that an earlier candidate has already been selected; the objective weights winning selections by the signal probabilities of the top candidate. This is the of Section 6, rather than a value defined by an asymptotic formula. Section 6, p. 20.
The paper also considers a rescaled dual with variables and an associated pair of thresholds . The thresholds are the first rounds at which the corresponding greedy dual coordinate is positive. In the finite formalization, records a signal whose coordinate is never positive. Proof of Theorem 20, p. 21.
The main target is the limiting primal optimum for every :
The finite milestones identify the primal optimum with the greedy dual objective, give the exact late dual coordinates and the exact range of the early recursion, and establish . The asymptotic milestones state
A separate companion target gives the finite lower bound , where denotes the displayed limit. Theorem 20 states the corresponding infimum inequality but does not separately prove it. Theorem 20 and its proof, pp. 20–22.
The limit quantifies the benefit of advice across the whole parameter square, including asymmetric classifiers. It recovers the classical value when , and gives value for perfect advice. The two threshold limits say when each signal begins to justify stopping as the horizon grows. Thus the result specifies both the achievable success probability and the scale of the optimal decisions. Theorem 20, p. 20.
The paper already proves threshold optimality through its linear program and presents the limit calculation. The formalization work here is to establish a full Lean limit theorem from an exact finite LP, including the two endpoint regimes and a finite dual characterization. The nearby classical secretary threshold limit on Prove2Me uses a different rank-based model; it does not state this classifier result. Definitions of the primal feasible set and the backward dual sequence can support later results about other advice distributions.
The source uses approximations throughout its asymptotic argument and explicitly omits terms that vanish as grows. Those omissions cannot be carried into an exact finite statement: the recursion, for example, fails at the round immediately before the threshold because the next dual coordinate is then present. A complete argument has to keep the discrete threshold boundaries and the harmonic sums under control while passing to a limit. The source's displayed theorem also contains an exponent inconsistent with the last equation of its proof; the corrected expression must be checked uniformly, including zero base at . Proof of Theorem 20, pp. 21–22.
Lean represents time by natural numbers , matching the paper's displayed LP, and signals by Bool, with true meaning . The primal optimum is the real supremum of objective values over exactly the feasible LP variables. For and , the zero assignment is feasible and the objective is bounded, so this supremum has its ordinary optimization meaning. Values of a variable array outside are ignored. The greedy dual is a backward finite recursion, not the definition of ; otherwise the central LP-to-dual milestone would disappear.
The formal thresholds are first positive greedy dual coordinates. If there is no positive coordinate, ; this occurs when and has the same normalized limit as the paper's informal convention at perfect advice. Real powers use Lean's , yielding the correct endpoint. All theorems quantify explicitly over where finite rounds are used, and over . The limit uses Filter.Tendsto at infinity. The chapter does not formalize the algorithmic running time, Figures 3 and 7, or the policy-level threshold optimality addressed by the series' preceding mission. Contributions to finite LP duality, harmonic asymptotics, and endpoint analysis are within scope. Sections 6 and Appendix C.
The classical secretary problem asks a decision maker to choose the best of candidates arriving in random order. A decision must be made when each candidate arrives, before later candidates are seen. In the classical model the decision maker sees only comparisons with earlier candidates. In hiring and selection, a prediction system may also classify an arriving candidate as promising or unpromising. The question is then whether the entire history of comparisons and predictions must be retained to make an optimal decision. Dütting, Lattanzi, Paes Leme, and Vassilvitskii study this question for several advice models in Secretaries with Advice. This mission concerns their binary-classifier model and the structural conclusion of Theorem 19: two signal-dependent time thresholds suffice.
The no-information secretary problem is a special case in which the signal says and with equal probability regardless of candidate quality. A separate classical cutoff-rule problem on Prove2Me addresses a deterministic rule for that special case; the present target covers informative and uninformative classifiers and compares with randomized policies that may use all observed history. The result is known mathematically in the cited paper. The task here is to give its probability model and the structural theorem precise, checkable statements in Lean.
There are candidates. Their ranks are a uniformly random permutation of , with rank uniquely best. At round , the decision maker learns how candidate compares with all earlier candidates and receives a binary signal . The classifier has recall : the best candidate receives with probability . It has specificity : every other candidate receives with probability . Both parameters lie in . Conditional on the ranks, signals across candidates are independent, as used by the paper's calculation of the signal-history distribution in Example 5 and Section 2.2. The decision maker never observes absolute ranks.
A policy assigns a stopping probability between zero and one to every possible information state at every round. Its information consists of all relative comparisons among candidates seen so far and all signals seen so far. Once it stops, it cannot act again. It wins if it stops at the unique candidate of rank . The winning probability therefore includes the probability of continuing through all earlier rounds. A candidate is best so far when its rank is at least that of every previously seen candidate.
A threshold policy chooses two rounds . It accepts the first best-so-far candidate arriving at or after if the current signal is , or at or after if it is . A policy can finish without selecting anyone; that outcome loses. Thresholds govern when a signal becomes acceptable, while the best-so-far condition still depends on the observed comparisons.
The goal is Theorem 19. For every positive and every , there are thresholds such that, for every valid randomized history-dependent policy ,
\Pr(\text{win under }q) \leq \Pr(\text{win under threshold}$t_Y,t_N$).The thresholds are chosen once for the model, before the competing policy . Their order is not constrained by this theorem. The later asymptotic result, Theorem 20, studies the positions and relative order of thresholds and belongs to a separate mission.
The supporting targets follow the paper's route to this conclusion. Section 2.2 computes the chance that the current candidate is globally best after an observed information state. Section 6 identifies the binary model's factor-revealing linear program. Appendix C asserts that its backward-defined dual vector is monotone in time and optimal among dual-feasible vectors. Proposition 12 converts those dual properties into an optimal threshold policy. Each statement concerns the same model fixed above.
The theorem reduces an optimization over policies that can use every past comparison and signal to a search over two time thresholds. It says that remembering the earlier signals and relative-order pattern cannot increase the achievable chance of selecting the best candidate once the two thresholds are chosen. This is a structural result about policy form; it does not give the numerical values of the best thresholds or their large- performance. The paper treats those questions separately in Theorem 20.
A formal development would also give reusable finite objects: a joint rank-and-signal probability model, the information available to an online policy, an exact winning-probability expression, and the primal and dual programs for binary advice. The target theorems in this proposal are open Lean statements with sorry; compilation checks their types, not their proofs. The paper supplies mathematical arguments, while the machine-checked proofs remain work for solvers. The local published uniform-average definition for rank permutations is relevant prior art, but this model uses its own weighted outcome sum because it also averages over the dependent signal law.
The available history is much larger than a pair of thresholds: it includes all earlier classifier outputs and the complete relative order observed so far. A direct comparison of a given policy with a threshold policy must account for the chance that the policy would already have stopped at an earlier round. Simply comparing the current stopping probabilities does not preserve the winning probability. The paper organizes those reach probabilities through a finite linear program and examines a dual vector defined backward from the last round. The remaining difficulty is to connect the properties of that vector to a policy with the claimed stopping behavior, including parameter values where some constraints are tight at equality.
Lean uses Fin n for rounds and ranks. Its index zero is the paper's round one; formulas containing (1/i) use a natural round number in . Bool.true represents . Every rank order is a permutation, so there are no ties. Each outcome weight is (1/n!) times the product of the conditional signal likelihoods. All expectations and event masses are finite sums, and conditional-probability claims are stated by cross-multiplying event masses, including at information states of zero probability. The LP is indexed only by positive rounds, so its divisions by and have the intended values.
The universal competitor in Theorem 19 is a randomized policy whose input contains only observed comparisons and signals. Its winning probability has an explicit product of continuation probabilities over earlier rounds. This restriction and product prevent the result from becoming trivial by allowing the policy to see the future, identify the global best rank, or stop more than once. The parameter interval and are explicit hypotheses. The printed conditional-probability fractions in Section 2.2 omit a factor of the current round ; the formal milestone uses the corrected value and records the discrepancy. The classifier's is recall as defined in Example 5, despite a later use of the word “precision” in Section 6.
The scope includes the finite probability model, its LP coefficients, the greedy dual vector, and the optimality bridge. Solvers can contribute proofs of the event identities, dual feasibility and optimality, and the threshold conclusion. Running-time claims for an LP algorithm, plots, and Theorem 20's asymptotic limit are outside this mission.
In the classical secretary problem, candidates with distinct qualities arrive in uniformly random order; after each arrival one sees only how the current candidate compares with those already seen, and must irrevocably accept or reject. The goal is to accept the best candidate. Dynkin's rule (skip roughly candidates, then accept the first one better than all before it) succeeds with probability about , and nothing does better.
A natural question in online decision-making with data is how much prior samples help. Kaplan, Naori and Raz (SODA 2020) introduced a model in which an adversary writes down numbers, a uniformly random of them are revealed in advance as samples, and the remaining arrive online in random order. Correa et al. (SODA 2021) studied the probability of selecting the maximum in a related independent-sampling model. Dütting, Lattanzi, Paes Leme and Vassilvitskii (arXiv:2011.06726, Mathematics of Operations Research 2024) place this model inside a general framework of secretaries with advice, where each arrival carries a signal, and prove that with samples the optimal policy has a simple threshold form.
Timeline:
Fix integers and . Only the relative order of the numbers matters, so an outcome is a uniformly random permutation of positions, read as position value rank. The first positions are the samples; position holds the secretary of round .
The proof passes through a linear program with variables and coefficients
its dual with variables , and the greedy dual solution (8), computed backwards from .
The goal asserts only the shape of the optimal policy, not the thresholds' values or the optimal winning probability. The milestones follow the paper's proof:
The result. Theorem 16 reduces an optimal stopping problem over all history-dependent randomized policies, whose information is a full relative order of up to items, to choosing integers. The greedy dual recursion computes them in polynomial time, which makes the optimal success probability computable for every and and underlies the numerical curves of the paper. For the theorem recovers the optimality of Dynkin-type cutoff rules.
Formalizing it. The theorem is proved in the paper (main text plus Appendix A), but no machine-checked version exists. A formalization produces a verified LP characterization of a secretary problem with signals, a reusable discrete-integration lemma, and a checked instance of the general principle "greedy dual optimal and monotone implies threshold optimal". The classical special case is posed separately on the platform as the open item ClassicalSecretary.exists_optimal_cutoffRule (deterministic rank-only rules, ). This mission does not restate it.
The obvious approach is backward induction over information states: compute the value of continuing and compare it with the probability that the current secretary is best. The difficulty is that the information is a relative order of the samples and all secretaries seen so far, and showing that the stop region is an upper set in for each signal requires controlling continuation values across exponentially many states. The paper avoids this through a linear program. The hard steps are the exact probability computations behind and (and behind Non-Filtering and History-Irrelevance) and the optimality of the greedy dual. The perturbation argument for that optimality needs the closed form of and a telescoping sum (Lemma 15). Monotonicity of the greedy solution does not follow from monotonicity of the coefficients alone, because the recursion subtracts a sum over later rounds.
Equiv.Perm (Fin (k + n)), read as position ↦ value rank, with the uniform distribution. Probabilities are finite counts divided by , never integrals. The adversary's numbers are taken distinct.Fin n): Lean round is the paper's round . The LP and its objects use 1-based natural indices and signals , as printed.Firms that own data increasingly sell it as a product: market research panels, consulting reports, datasets for training demand models. A common commercial practice is to hand out a free sample of the data before quoting a price for the rest. Under standard Bayesian reasoning this practice looks self-defeating. Every free data point reduces the buyer's uncertainty, which reduces what the remaining data are worth to her. This is a holdup problem: once information is revealed, it cannot be sold.
Drakopoulos and Makhdoumi (Providing Data Samples for Free, SSRN 3611003; Management Science, 2022, doi:10.1287/mnsc.2022.4534) identify when free samples nevertheless raise the seller's revenue. The mechanism is disagreement about the prior. When the seller believes the buyer's initial estimate is biased, she expects the free data to move the buyer's belief toward states in which the buyer values the remaining data more. The paper calls this the persuasion benefit, and it can outweigh the holdup cost. This mission formalizes the paper's main theorem, Theorem 1(a), together with the lemmas its proof rests on.
An unknown real parameter determines a buyer's payoff from an action . The Buyer holds the prior with . The Seller believes is a biased estimate, with bias distributed as and . Her prior is with , and it is taken to be the correct one.
Data arrive continuously. The first samples are equivalent to the signal
where is a standard Brownian motion independent of and is the noise variance. Both parties agree on this law of the data given (they are concordant) and disagree only on the prior. The information after samples is .
The Buyer's posterior after samples is , with and . The Seller's posterior is given by the same formulas from her own prior. The Seller's estimate of the Buyer's error is , and .
With belief , the Buyer's best expected utility is . Her Bayes risk
is the value to her of learning exactly. Its second argument is a variance, and , and denote its partial derivatives.
A free-sample policy gives data for free up to a stopping amount , a stopping time of , and then sells the remainder. Once the free samples stop, the best price for the remainder is (Lemma 3). The Seller's expected revenue is therefore , computed under her prior. Selling in one round is , with revenue .
If the Seller-side drift of the Bayes risk is positive at the start,
then some free-sample policy satisfies
The goal has no constants. It asserts only that the optimal free-sample policy strictly beats every one-round policy.
Theorem 1 splits the drift of the Bayes risk from the Seller's viewpoint into a holdup cost, , which is the drift the Buyer herself expects, and a persuasion benefit, . Part (a) turns the sign of this drift at the start into a revenue comparison. In the paper's pricing example (unknown demand elasticity, ), condition (4) reduces to : a sufficiently biased Buyer should be given free data. In the estimation example () part (b) applies and one-round selling is optimal. The theorem is the basis of the paper's later results on myopic stopping rules and on the comparison with dynamic pricing.
The theorem is proved in the paper, in -notation and through Itô's lemma and the optional stopping theorem. It has not been machine-checked. A formal proof requires Gaussian conjugacy with respect to a Brownian filtration, moment computations for the posterior mean, an Itô-type expansion for a function of the belief, and control of the integrability of the stopped Bayes risk. Each of these is reusable for other continuous-time Bayesian learning models.
The informal argument reads off Lemma 4 that is a Seller-submartingale near the start, and then stops it. The -identities of Lemmas 1 and 4 are statements about conditional expectations at every time. Made rigorous, they require integrability of the Bayes risk and its derivatives along the belief path, and an exchange of differentiation and expectation. Neither is given by the paper's hypotheses on . The Gaussian conjugacy itself must also be established for conditioning on the whole path , not only on .
All objects are defined in one file, FreeSamples.Revenue.Setting, on top of Mathlib's gaussianReal, IsBrownianReal, Filtration.natural and IsStoppingTime. Committed conventions:
gaussianReal m v.toNNReal. and take the variance, not the standard deviation, as their second argument.Trivializing formalizations are ruled out. Every revenue in a conclusion is asserted integrable, so a junk-zero integral cannot satisfy it. The maxima in and are assumed attained, so no real supremum takes its junk value. The goal is stated for the Gaussian–Brownian model and its posterior map, not for an arbitrary process with a postulated drift. Its conclusion exhibits a policy instead of comparing a supremum over policies.
Not posed: the stochastic differential equation of Lemma 1, Lemma 2, Proposition 2 (its free boundary is part of the hypothesis), Corollaries 1–3, and Appendix B. Contributions are welcome on the conjugacy computation (Proposition 1), on the Gaussian moment estimates (Lemma 1), and on a reusable Itô-type expansion of for functions of exponential growth.
Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution from the transitions they have observed out of the state–action pair . Their regret analyses then need to know how far the empirical distribution can be from the true one . The standard tool is an bound on , as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order in the number of states . What the analysis actually uses, however, is the deviation along one direction: the projection onto a bias (or value) vector whose entries differ by at most the MDP's diameter .
S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on whose leading term is governed by a variance of under , written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.
Fix a number of states and order them . A probability vector has and . A multinoulli trial with parameter is a random state with . Draw independent trials and let
be the empirical probability vector, the average of the one-hot outcomes. For and a vector define the stick-breaking quantities
Thus is the mean of under conditioned on the states after , and compares with it. The sum equals the variance of for . In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.
Let satisfy for all , let and . Then, with probability at least ,
together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): for . 4. The predictable variance (proof, p. 21): . 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance : for , , with probability greater than ,
The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along with constant probability. Because the bound is stated along a single direction and is weighted by the variance of rather than by alone, it avoids the loss that an bound would incur, which is part of how the paper's regret bound improves on UCRL2's . The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.
Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in and its algorithm's parameters are given as . Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.
Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as ; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.
A known subtlety: the paper's proof, through Corollary B.1, yields the second term , while the statement prints the smaller . The printed statement is still true for iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.
Fin S with its natural order, 0-based; the paper's range is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to (Lean's convention), which gives the values the identities need; no positivity of is assumed.cat p ; trials have the product law trialsLaw n p Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability " is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than " is strict. is Real.log.The goal cannot be satisfied by a degenerate reading: is built from the sample, the measure is the -fold product of the categorical law , the event is the good event itself (not a complement bound), and the variance term is not identically zero (for , it equals ).
Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.
Quantum search starts with a state that has some overlap with a desired target. Standard Grover iterations can increase that overlap quickly, but their success probability oscillates with the number of iterations. If the initial overlap is unknown, a sequence chosen for one value can pass the target and perform poorly at another. Earlier fixed-point constructions avoided this oscillation but lost the quadratic improvement in query count. Yoder, Low, and Chuang gave a sequence of adjustable phase reflections with both a specified failure tolerance and a query count proportional to the inverse square root of the initial target probability Yoder, Low, and Chuang (2014).
The result concerns amplitude amplification, a reusable procedure in which a quantum algorithm prepares a state, a target test identifies the useful component, and repeated operations increase the chance of measuring that component. The paper's exact success formula is useful because it says what happens at every initial overlap, rather than only at a single guessed overlap or in an asymptotic regime. Its polynomial form also explains why the interval with a guaranteed error bound grows as the sequence becomes longer Yoder, Low, and Chuang (2014), pp. 1–2.
Let and be unit vectors in a finite-dimensional complex state space. The target overlap is . The parameter sets the desired upper bound on failure probability. A generalized reflection about a unit state changes its phase while leaving the orthogonal directions unchanged. The two reflections used here are
Their Grover iterate is . For , the sequence is , so the iterate with index acts first. The phases are those in Eq. (11) of the paper: , where Yoder, Low, and Chuang (2014), pp. 2–3.
Here is the degree- Chebyshev polynomial of the first kind. For the fractional order at an argument at least one, means the positive real continuation . This convention gives . The paper also uses a two-dimensional coordinate system spanned by the prepared state and target state, with basis order and Yoder, Low, and Chuang (2014), Eqs. (4), (6)–(7).
The goal is the paper's Eq. (1), for the phase sequence of Eq. (11):
This equality determines the entire response curve, including the one-step case . It is stated for arbitrary finite dimension, rather than only after fixing two coordinates. The milestones cover the paper's two-dimensional reduction, the reflection and rotation formulas, the equatorial-rotation sequence, its amplitude recurrence, and the Chebyshev identity used to finish the calculation Yoder, Low, and Chuang (2014), Eqs. (1), (4), (6)–(15).
The same exact formula gives a fixed-point interval. With , the desired success bound holds whenever :
The draft also states that decreases as the odd length increases, the sufficient length bound of Eq. (3), and the nesting identity for success-probability functions in Eq. (18) Yoder, Low, and Chuang (2014), pp. 2, 4.
The exact formula gives a sequence that can be selected from a lower bound on the target overlap and a chosen failure tolerance. Increasing its length extends the interval on which the tolerance is met; an already adequate state therefore stays within the bounded-error regime at greater odd lengths. The sufficient length bound records the quadratic query scaling in the overlap parameter. The nesting identity shows that the same family of probability functions is closed under the paper's specified composition of tolerances Yoder, Low, and Chuang (2014), pp. 2, 4.
The mathematical result is proved in the 2014 paper. This mission asks for machine-checked proofs of its exact operator-level equality and the cited intermediate identities; the statements here are currently draft targets, not already machine-checked results. A completed development would leave reusable finite-dimensional phase-reflection and Chebyshev tools for subsequent amplitude-amplification arguments. The paper's oracle implementation is separate from these operator identities Yoder, Low, and Chuang (2014), Fig. 2.
The obvious idea of repeating a fixed phase pair produces the familiar Grover oscillation. Adjusting phases removes that simple repeated-power description, while the target amplitude must still be controlled exactly across all allowed overlaps. A proof must keep the complex phase conventions and multiplication order aligned with the Chebyshev expression. The fractional-order parameter also lies outside the usual cosine formula's interval when ; replacing the polynomial by a clamped arccosine expression changes the target formula. The unnumbered Chebyshev-amplitude assertion after Eq. (15) is the central algebraic gap left for formalization Yoder, Low, and Chuang (2014), p. 3.
States are functions Fin N → ℂ, and operators are complex N × N matrices. Inner products conjugate the first vector. The theorem binds to the squared target overlap and requires both states to have norm one; it does not take an unrelated free success parameter. The goal permits every for which its hypotheses can hold, and every . The rotation milestones use Fin 2 with index for and index for . The operator has the same rank-one projector as the paper's phase-adjusted . Matrix exponentials define the rotations, and is Mathlib's polynomial, evaluated even outside .
The scope assumes . At , the displayed expression involves division by zero and the paper treats its limit separately. The inverse cotangent is , a branch whose changes by leave the reflection phases unchanged. The product order is fixed by the recursion defining . The mission formalizes Eqs. (6)–(7) as operators; the ancilla and oracle gates of Fig. 2 are outside this mission. The goal retains the full equality and cannot be reduced to the easier lower bound .
The milestone for printed Eq. (12) uses a free output rotation and a unit global phase. The printed outer rotations do not give the claimed state for the stated phases; this corrected form preserves the coordinate magnitudes needed for Eq. (1). The milestone for Eq. (15) states the displayed amplitude recurrence but does not restate the page's incompatible intermediate sentence. These corrections are identified in the item descriptions and moderation notes. Contributions proving the reduction, phase identities, amplitude recurrence, Chebyshev relation, or the final equality are all within scope Yoder, Low, and Chuang (2014), p. 3.
Machines in production lines deteriorate in ways that are only partly visible. A machine may run in a degraded state that raises costs without announcing itself, and eventually fail in a way that cannot be missed. The decision maker must choose between continuing production, paying for an inspection that reveals the hidden state, and replacing the machine preventively. Models of this kind are partially observable Markov decision processes (POMDPs), and for POMDPs closed-form optimal policies are rare: the value function lives on the space of beliefs and is usually only computed numerically.
H. Zhang and W. Zhang, Analytical Solution to a Partially Observable Machine Maintenance Problem with Obvious Failures (Management Science, 2022; read here as SSRN 2945049, version of 2022-08-21), solve the classical two-state version of this problem completely. Working in the dual "efficient frontier" framework of Zhang (2010), they show that the optimal solution has exactly six possible structures and give each in closed form, with explicit or implicitly characterized thresholds on the replacement and inspection costs.
A machine is in a hidden state (good or bad) or in the observable failure state . Each period, if the machine has failed it is replaced correctively at cost ; otherwise one of three actions is chosen:
Production always takes place. From state 0 the machine moves to state 1 with probability ; from state 1 it fails with probability . Write , , , , and . Costs are discounted by over an infinite horizon.
A continuation-cost vector records the cost of a continuation policy from each hidden state, and the cost after a failure. The expected optimal cost at an (unnormalized) belief is , where is the set of extreme points of the efficient frontier. The pair is the fixed point of the dual value iteration (12)–(16). In support-function form, a pair is mapped to
the three terms being , and . A finite set with a number is the optimal solution for an action set if value iteration from zero terminal costs converges to for every and to after a failure.
The structures are built from two point sequences. The production sequence is . Started on the diagonal at with , the self-consistency equation has a unique solution (31). Started instead at the inspection point (35), it gives (40).
Let and . Under :
with every structure an explicit pair from Table 1, and the thresholds characterized implicitly ( on the frontier of at ; at ).
Proposition 2 (the fixed-point equations), Proposition 3 (the cost of producing forever), Lemma 1 and Lemma 6 (the two sequences in closed form), Lemma 3 and Lemma 7 (the anchors and ), Proposition 4 (unimodality of ), Theorem 1 (the two-action solution: , , , with extreme-point exactness) and Lemma 5 (when inspection enters).
The result. The theorem turns a POMDP into a finite list of explicit policies. Each structure is a periodic plan that needs no belief updating: produce for periods and replace; or inspect every periods and replace only if the machine is found bad. The thresholds tell when inspection is worth its cost, and the comparative statics of and follow from the closed forms. The authors use the solution to justify common maintenance practices.
Formalizing it. The result is proved in the paper (main text §4, proofs in its e-companion, App. A); no part is machine-checked. The proofs of Theorems 1 and 2 argue geometrically from figures of convex curves in the plane ("the curve bends back", "all the points are still extreme points"). A formal development has to turn these into inequalities between piecewise-linear concave functions, and has to prove convergence of value iteration to the stated sets. The implicit thresholds of part (3) were not checked numerically when this mission was planned. Parts (1) and (2) and Theorem 1 were.
Verifying that a candidate set is a fixed point is not enough: the goal asserts that value iteration from zero converges to it, so uniqueness of the bounded fixed point must be proved (a contraction argument in the supremum norm over the simplex). More importantly, finding the frontier requires knowing which points of the infinite production sequence are extreme, which depends on the location of the anchor relative to the curve (Fig. 5 of the paper, five subcases). The natural induction on fails because is not monotone: its least minimizer must be located through the unimodality of the real extension (Proposition 4). In part (3) the thresholds are defined implicitly, and showing that the three regimes are ordered in requires monotonicity of the whole frontier in .
Everything is defined in the namespace MaintPOMDP.Frontier. Vectors and beliefs are Fin 2 → ℝ (index 0 = good state); beliefs are unnormalized, . The optimal solution is the limit of the support-function value iteration started from , ; "the structure is X" means that this limit equals over the points of row X of Table 1, with the failure cost of that row.
Standing assumptions: , (p. 14), and , , which the paper never states and which are added (the thresholds divide by ). The hypothesis is added only to Lemmas 1, 3, 6, 7 and Proposition 4, whose printed formulas divide by ; and themselves are defined as solutions of the affine anchor equations, so Theorems 1 and 2 cover . Proposition 4 also carries the range of that its proof uses. "" is the least minimizer, and its existence is part of the conclusion. In Theorem 2, the indices of Table 1 are existential and extreme-point exactness is not asserted for the and rows (Table 1's row conflicts with the paper's Proposition 8). It is asserted in Theorem 1. In part (3) the thresholds are chosen before and the claims hold for every .
Trivializing readings are ruled out: the value function is the limit of the iterates, not an arbitrary fixed point or a junk limit; identities hold for every belief , not only at vertices; every frontier set is given by formulas, so no extra points can be slipped in; minimizers are asserted, not assumed; and thresholds involving are evaluated with .
A complete development needs convergence of value iteration for a monotone contraction on bounded functions over the cone , explicit solutions of two-dimensional linear recurrences, and lemmas on lower envelopes of finitely many linear functions in two variables. These are reusable beyond this mission, for other two-state POMDPs. Contributions of any milestone, of the γ0 = γ1 closed forms (App. B), or of a proof of Theorem 1 alone are welcome.
Quantum computers need error correction, and the codes that are cheapest to run in hardware are quantum low-density parity-check (LDPC) codes: every check involves a bounded number of qubits, and every qubit takes part in a bounded number of checks. For a long time the only well-understood quantum LDPC codes were surface codes such as Kitaev's toric code, whose minimum distance grows like the square root of the length but which encode a fixed number of qubits, so their rate tends to zero. Tillich and Zémor (arXiv:0903.0566; IEEE Transactions on Information Theory, 2014; preliminary version ISIT 2009) gave the first general construction of quantum LDPC codes with positive rate and minimum distance proportional to , from any classical LDPC code. Their hypergraph product became the standard building block of the field.
Timeline.
All codes are binary linear codes, subspaces of for a finite coordinate set . The Hamming weight of is its number of nonzero coordinates. The minimum distance of a code is the least weight of a nonzero codeword, with the convention .
A Tanner graph is the bipartite graph of a parity-check matrix : the variable nodes index the columns, the check nodes index the rows, and iff . Its code is . The transpose Tanner graph is that of , and its code is the transpose code. It depends on the matrix , not only on .
A CSS code is a pair of codes of the same length with . Its quantum dimension and quantum minimum distance are
with defined symmetrically and .
Given and with Tanner graphs , the code has qubits and check matrices
with and . Write , , and .
Let be a full-rank parity-check matrix of an code. The code built from two copies of its Tanner graph is a CSS code with
and each row of and has weight , with a row weight and a column weight of .
The milestones follow the paper. They are Proposition 4 (validity), eq. (4), Fact 12 and Propositions 9, 10, 13 (product codes and transposes), which lead to Proposition 14. Then come eq. (17), the weight claim and Lemma 16 (lower bound), and the two claims of p. 17 and Lemma 17 (upper bound), which lead to Theorem 15. The degree count of p. 11 gives the row weights.
The result. The construction needs no orthogonality between the input codes: any two parity-check matrices give a valid CSS code. Its parameters are read off the classical inputs. A family of classical LDPC codes with fixed rate and linear distance therefore gives quantum LDPC codes with fixed rate and distance , and sparse inputs give sparse stabilizers. The toric code is the special case where both inputs are cycle graphs. The hypergraph product is also the base case of the later homological and lifted-product constructions, and the source of the standard decoding and fault-tolerance results for these codes.
Formalizing it. The theorem is proved in the paper; what is missing is a machine-checked proof. The platform holds the toric code's distance and dimension (ToricCode.toric_distance, ToricCode.toric_homologyRank), but over its own chain complex, not over a general construction. This mission produces a reusable layer: Tanner graphs as binary matrices, CSS dimension and distance with the convention, product codes, and the parameters of the hypergraph product for arbitrary finite index sets.
The dimension count is linear algebra once the codes and have been identified with product codes. The obstacle is the distance. Lower bounds on the minimum weights of and themselves are useless: contains the rows of , which have constant weight, so the minimum weight of is bounded by a constant. Any bound of order must use the definition of over and show that every low-weight codeword of is degenerate, i.e. lies in . The upper bound needs an explicit codeword of outside , and showing that it is not in requires an argument of its own.
Lean represents a Tanner graph by its matrix H : Matrix C V (ZMod 2) over arbitrary finite index types. The code is ker H, the transpose code is ker Hᵀ, and the dual code is CodingTheory.dualCode from the published definition CodingTheory. Hamming weight is Mathlib's hammingNorm. Minimum distances live in ℕ∞, where the empty infimum is ⊤, the paper's . is the dimension of the quotient of by . In and the qubits are ordered , as on p. 18. A product code is a set of matrices whose columns (fixed second coordinate) lie in the first code. The general results are stated without nonemptiness assumptions; they hold for empty index sets.
Theorem 1 has two disclosed differences from the page:
"There is a construction" is formalized as the paper's construction, the hypergraph product of with itself.
Several encodings would trivialize the statements and are excluded: an -valued minimum distance that is on the zero code; taken over instead of ; computed by truncated natural subtraction; an existential "there is a code with these parameters"; and the transpose code replaced by the dual code.
A complete development needs ranks and kernels of Kronecker products over , dimensions of product codes (Proposition 9, not in Mathlib), and the restriction of Tanner graphs to induced subgraphs. The product-code and CSS layers are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 14 via the Künneth formula.
Determining an unknown quantum state of qubits to good accuracy requires, in general, a number of copies of the state exponential in ; this follows from Holevo's theorem. One way around this barrier is to restrict the class of states. Stabilizer states are the natural candidate: they are the states produced from by Clifford circuits, they underlie quantum error-correcting codes, measurement-based computation and randomized benchmarking, and there are of them, so copies are necessary to identify one.
Timeline.
Bell sampling became a standard tool after this paper, for instance in stabilizer testing (Gross, Nezami and Walter, arXiv:1712.08628), so a machine-checked version of its analysis is a reusable base.
A state of qubits is a vector ; its complex conjugate is taken entrywise in the computational basis. The paper uses the four matrices
which are the Pauli matrices up to the factor on . For a string , ; strings are added bitwise, .
The Bell basis of is , , , . Bell sampling on qubits measures each pair in the Bell basis and returns a string . On two copies (first copy on the 's) the outcome has probability .
A stabilizer state is for a Clifford unitary (a unitary normalising the Pauli group). Its stabilizer set is the set of strings for which is an eigenvector of , i.e. those that lie in the stabilizer group of up to a phase.
Algorithm 1. Bell-sample two fresh copies to get ; repeat times to get ; find a basis of ; for each element of measure one copy of in the eigenbasis of the corresponding (Hermitian) Pauli matrix to learn whether or . It uses copies.
For every and every -qubit stabilizer state , with the Bell samples independent,
and for every basis of with Hermitian Paulis , each and every vector with the same eigenvalues under all is a scalar multiple of . Together: Algorithm 1 identifies except with probability at most .
The theorem gives a learning algorithm whose copy complexity is optimal and whose measurements are simple: one Bell measurement on corresponding qubits of two copies. Its analysis isolates a structural fact about stabilizer states, that Bell sampling on two copies produces a uniformly random element of a coset of the stabilizer subspace, which is the engine of later work on stabilizer testing and on learning states with few non-Clifford gates.
The result is proved in the paper; no machine-checked proof of it is known. A complete formalization adds: the stabilizer formalism in a form usable from the definition " for a Clifford " (the subspace , its dimension, vanishing expectations off , determination by signs); the conjugation identity, which the paper takes from a normal form cited from the literature; and the probabilistic bookkeeping of the algorithm with its exact constants.
The probability calculations (Lemma 2, eqn (1), the union bound) are finite sums. The difficulty lies in the stabilizer structure. The platform's definition of a stabilizer state is the image of under a Clifford unitary; from it one must derive that the strings whose fixes up to phase form an -dimensional subspace, that all other Pauli expectations vanish, and that differs from by a diagonal Pauli. The paper obtains the last fact from the Dehaene–De Moor normal form , a cited theorem whose proof is not on the page; formalizing either that normal form or a direct substitute is the central step. The natural shortcut, treating as given with "uniform outcomes on " as a hypothesis, proves only the counting lemma and is ruled out below.
StabilizerRank.QState n = (Fin n → Bool) → ℂ and stabilizer states are StabilizerRank.IsStabilizerState (published platform definition, referenced). Qubit is coordinate , false .Fin n → ZMod 2 × ZMod 2, coordinate the pair of qubit ; is +.Needed infrastructure: Kronecker-product manipulations of indexed by bit strings, the Bell basis as an orthonormal basis of , the stabilizer formalism over , and counting hyperplanes of finite -spaces. The stabilizer-formalism layer and the union bound are reusable beyond this mission. Contributions to any milestone are welcome, in particular direct proofs of milestones 4, 6 and 7 from the Clifford definition.
Cutting plane methods minimize a convex function, or find a point in a convex set, using only a separation oracle: a routine that, given a query point, either certifies it is good or returns a halfspace containing the target. Lee, Sidford and Wong (arXiv:1508.04874, FOCS 2015) gave a cutting plane method for a convex set in inside a box of radius that uses an expected oracle calls and additional time, improving on the additional time of Vaidya's method from over 25 years earlier, and derived from it faster algorithms for submodular function minimization, matroid intersection and submodular flow.
The speed-up depends on not recomputing the leverage scores of the current constraint matrix from scratch at every step. The algorithm maintains approximations and refreshes a few of them per step. Section 7.2 of the paper isolates the bookkeeping question this raises as a two-player game, the stochastic chasing game, and shows that a simple greedy strategy keeps the accumulated error small. The game is self-contained and has nothing to do with convexity: it is a statement about a random walk in that is partially reset at every step.
Fix a dimension and constants , . For , and .
A point starts at . Each round runs as follows (Algorithm 4).
The adversary may use everything that has happened so far to make its choices. The player wants to keep near in ; the adversary wants to push it away. The largest-coordinate strategy is : reset the coordinate that looks largest.
If the player uses the largest-coordinate strategy, then for every , with probability at least ,
The bound holds simultaneously for all rounds, against every adaptive adversary, and grows only logarithmically in , in and in .
The milestones are the steps that the paper's proof of Theorem 34 (pp. 43–44) displays:
Within the paper, Theorem 34 is what lets the cutting plane method keep its leverage-score estimates within a bounded multiplicative error while refreshing only one estimate per step; this is one of the ingredients behind the additional time. The game reappears whenever an algorithm tracks many slowly drifting quantities with noisy observations and can afford to recompute only a few of them exactly per step, which makes the statement useful beyond this paper.
None of the statements in this mission has a machine-checked proof. The theorem is published with a proof. The mission asks for a formal proof of the statement exactly as published, with the constant inside the logarithm. A formal proof of the milestones alone would already give a reusable exponential-potential toolkit for adaptive random processes in .
The point process is not a martingale: the player's resets depend on a noisy observation, the adversary is adaptive, and the reset can hit a coordinate that is up to smaller in absolute value than the largest one. Per-coordinate tail bounds do not suffice, because the adversary may concentrate its moves on whichever coordinates the player is not resetting. A bound that holds for all at once, with only logarithmic dependence on , has to control all coordinates jointly. Establishing such joint control, with the specific constant inside the logarithm, against the most adversarial interaction between the observation error and the step size , is where the work lies.
Fin m (0-based), with . Lean round is the paper's round , so the goal's bound reads ; at Lean round the point is .Fin m → ℝ. The step bound is written as , never as a sup-norm bound. The paper's prose once writes ; Algorithm 4 and the proof use , which is what is formalized.Mobile retail stalls (self-driving or driver-operated vending vehicles that move to customers who order through a phone app) are studied by Cao and Qi in Stall Economy: The Value of Mobility in Retail on Wheels (Operations Research, 2022; the mission cites the authors' SSRN manuscript 3711896). A retailer partitions a city into service zones, one stall per zone, and must decide how densely to deploy stalls. That decision is made by continuous approximation: each zone is modelled as a small queueing system whose service time includes the stall's travel to the next customer. The mean and variance of that travel distance enter the Pollaczek–Khinchine waiting-time formula of an M/G/1 queue (the paper's equations (1a)–(2), p. 18), so closed forms for them are the input of the paper's whole deployment and pricing analysis (§4).
The paper considers two on-demand modes. In the door-to-door mode the stall drives to each customer's doorstep. In the within-radius mode each customer walks up to a distance toward the stall, and the stall only moves until the two are apart. This mission formalizes the travel-distance moments of both modes: Proposition 1 (door-to-door, p. 11) and Proposition 3 (within-radius, p. 18), whose proofs are in the paper's Appendix B (pp. 44–45 and 49–51).
All distances are Manhattan () distances (p. 9): . A service zone is a square rotated by , a diamond, of Euclidean edge length ; the paper sets for a stall density (p. 11). In Manhattan coordinates centred at the zone's centre,
which has area . Customers arrive uniformly on .
Fix a walking radius . The inner diamond lies inward from the boundary and has edge length . The paper's model for the stall's position when a new customer arrives (proof of Proposition 3, p. 49) is: the stall is uniform on , the customer is uniform on , and the two are independent. The repositioning trip length is
and denotes the untruncated distance. In the door-to-door case , both points are uniform on the zone and . The variance is .
The uniform law of the stall is the paper's Theorem 1 (the subject of the companion mission I), read in a continuum limit that the paper states informally (p. 17). This mission takes the uniform law as its model and does not depend on that limit.
For all and ,
and both are non-decreasing in (on ) and non-increasing in (on ).
A supporting theorem, (p. 50), is posed as well.
The result. With Proposition 3 the service time of the within-radius mode has explicit first and second moments, so the M/G/1 waiting time, the stall's daily travel, and the profit density of §4 are explicit functions of . Part (III) is the qualitative content the paper calls the first effect of avoiding the "last 100 meters": a longer customer walk shortens the stall's repositioning, and a larger zone lengthens it. Proposition 1 is the benchmark against which that saving is measured.
Formalizing it. The results are proved in the paper by direct integration; none is machine-checked. The proofs split the domain into several regions by the signs of coordinate differences and assert the values of the resulting polynomial integrals "by calculation". A formal proof checks every one of those integrals, the use of conditional expectations given the event , and the derivative signs behind part (III), which the paper states without verification on the whole range. The intermediate moments are useful on their own for other models with uniform demand on diamonds under the Manhattan metric.
The obvious route rotates the diamond by , where the distance becomes an distance and the zone a square, and then integrates. For this works cleanly. For the stall's square is smaller than the customer's, and of two coordinate differences over two squares of different sizes splits into many polynomial pieces. The paper instead stays in the original coordinates and splits into six regions for . Either way, the truncation at is the delicate step: it requires that the whole ball of radius around the stall lies in the zone, which is exactly why the stall is confined to the inner diamond. Part (III) is not a consequence of (I) and (II) by inspection: the derivative in of the mean vanishes at the boundary , so the sign argument must be done on the closed range.
Points are elements of ℝ × ℝ with Lebesgue measure. The definition StallEconomy.TripLength.Setting provides zone R, innerZone R r, the scale factor shrink R r = 1 − √2 r / R, the Manhattan distance l1, the trip length Lr r, the expectation E R r F, meanL R r and varL R r. The stall's uniform law is realised as with and uniform on , which is the uniform law on ; it covers the endpoint , where the inner diamond is a single point, without dividing by . Thus
Standing conventions and deviations from the page:
Formalizations that would trivialize the goal are ruled out: meanL and varL are integrals, not the closed forms; part (III) is stated about those integrals, not about the polynomials; and nothing is restricted to or to a fixed .
A complete development needs iterated set integrals of piecewise polynomials over diamonds in ℝ × ℝ (Fubini on zone R, the change of variables ), and elementary calculus for part (III). Contributions of any of the moments, of a reusable lemma computing integrals of polynomials over diamonds, and of the monotonicity of the closed forms are all welcome. Proposition 2 of the paper, which is false as printed, is not claimed here.
A mobile retail stall can travel toward its next customer while that customer walks toward the stall. The customer's walking allowance changes where the stall stops, so it also changes the location from which the next trip begins. A useful trip-length calculation therefore needs a distribution for successive meeting points, not just a rule for one meeting. Cao and Qi study this question in a service zone assigned to one stall and give a particular magnet rule whose rendezvous chain has a simple stationary law Cao and Qi, §3.3. The result supplies the location model used in their analysis of repositioning distances.
The rule matters because different choices of a meeting point can produce different chains even when each choice lets the customer walk the same maximum distance. The paper's Theorem 1 establishes a distributional property of the specified rule, for every admissible finite grid. Its proof is in Appendix B, pp. 46–49 of the cited SSRN manuscript.
The service zone is a square drawn as a diamond in ordinary horizontal and vertical coordinates. Its edge length is in Euclidean distance, while stall and customer travel is measured in Manhattan distance. For the chain, use the paper's two edge coordinates, aligned with the lower edges of the zone. The full customer grid is , so it contains points. A customer is uniform on this full grid.
Write , where and is the customer's maximum walking distance. The paper chooses so that is an integer and assumes . The stall docks only at points of the inner diamond
The name “diamond” refers to its appearance in ordinary coordinates; in edge coordinates it is an axis-aligned square. A type-1 origin lies in . The other origins in are type 2. The closed small diamond around an origin is .
The magnet rule maps the origin and next customer location to a rendezvous . The stall stays at when . Otherwise, the location of in one of eight surrounding regions selects one of eight customer movement arrows. At a type-1 origin the head of that arrow is the rendezvous. At a type-2 origin the rule changes an arrow whose head would leave , keeping the rendezvous inside it while preserving the customer's allowed walking distance. These are Definitions 1 and 2 of the paper pp. 14–16.
For , let be the customer grid locations sent from to . The transition probability is
Thus the denominator is the number of possible customers, not the number of stall locations. Repeated independent customer locations produce a finite Markov chain on .
The goal is Theorem 1 p. 17. For every with , its first part says that is doubly stochastic:
Its second part says that the stationary distribution is uniform on . The formal target states existence and uniqueness: a probability vector is stationary for if and only if for every state .
The milestones follow the source's intermediate assertions: the rule keeps the rendezvous in at the prescribed customer distance; each row counts customers; the type-1 self-transition counts customers; type-1 and type-2 columns each count incoming customer events; and every transition entry is positive. The last assertion supports the uniqueness clause.
A uniform stationary law replaces an unknown, history-dependent location distribution with one specified directly by the inner diamond. In the paper, that distribution is the location input for later within-radius repositioning calculations Cao and Qi, §§3.2–3.3. The result is specific to the magnet rule. It does not say that every reasonable meeting rule has a uniform stationary law.
The paper proves the finite-grid theorem in Appendix B. This mission asks for a machine-checked account of its exact finite combinatorial statement. The development will provide reusable definitions of the grid rule and its transition counts, while using an existing formal library interface for finite Markov chains. The theorem statements are open proof targets; a successful local compilation of their statements alone is not a proof.
Unit row sums follow from assigning each customer location to one next rendezvous. Unit column sums are subtler: fixing a destination and varying the origin gives overlapping sets of customer locations. Interior destinations and boundary destinations have different counts because a type-2 origin can redirect an arrow that would otherwise leave the allowed stall region. The source treats these as Case I and Case II on pp. 46–49. An interior-only count cannot establish the theorem for all of , and positivity of every transition is a separate requirement for identifying the unique stationary law.
Lean uses integer coordinate pairs for grid points and finite sets for , , , and . The region boundaries use the paper's strict or inclusive inequalities exactly. The permitted parameters are all natural numbers satisfying , including , , and . In physical units ; no division by occurs in the formal statements. When , there is one customer point and one state.
The matrix is computed from the paper's two-part magnet rule and uniform demand on the full grid. Defining it as a uniform matrix, using a nearest-point rule, dropping the type-2 correction, fixing one grid size, or proving only column sums would miss the target. The definition of counts customer locations that induce a transition. This includes customers already inside in a self-transition, as required by the paper's Case I(IX) and row-count formula. The paper's separate Proposition 2 is not a claim of this mission because it is false as printed; none of these targets assumes it. The finite-grid theorem does not formalize the subsequent informal statement.
The complete development needs finite-set counting, integer interval bounds, real-valued stochastic matrices, and the stationary-distribution interface of the published MarkovChain definition. Contributions proving any of the stated counting milestones or strengthening the finite-chain consequences are welcome. The paper's own proof is in Appendix B, pp. 46–49.
A recurring proposal in the policy debate on dominant digital platforms is to make competing platforms interoperable, so that users of one service can interact with users of another; the EU Digital Markets Act (Regulation (EU) 2022/1925, Article 7) imposes such an obligation on gatekeepers' messaging services. The economic case is that users then enjoy network effects across platforms, not only within their own. The counter-argument is that a network shared with rivals is a weaker competitive weapon, so platforms may compete less hard and users may lose through higher fees.
Ekmekci, White and Wu, Platform Competition and Interoperability: The Net Fee Model (Management Science, 2025), resolve this trade-off in a tractable model of platform competition with strong network effects. Their device is the net fee: the membership fee net of the interaction charges a platform extracts once users have joined. Competition in net fees turns platform demand into an ordinary discrete-choice demand, so equilibria can be characterized by pricing formulas. This mission formalizes their Proposition 7(b): with symmetric platforms, more interoperability lowers the equilibrium net fee, except in a duopoly without an outside option, where it has no effect.
There are ex ante identical platforms, indexed by , and one side of users. Platform charges a net fee . A user either joins one platform or takes an outside option whose weight is ; means there is no outside option. Under Logit demand (13), platform 's user mass at the profile is
Every platform has marginal cost , and each user values each other user on the same platform at (the network effect). The degree of interoperability lets a user value each user of every other platform at (19). Platform extracts all interaction utility through its total price, so its profit is
A profile is a Nash equilibrium in net fees if no platform can raise its profit by changing its own net fee to any other real number. A symmetric equilibrium is an equilibrium in which every platform charges the same net fee. The diversion ratio (32) is the share of the users a platform gains by a small fee cut that come from rival platforms rather than from the outside option.
When all platforms charge , each has share and diversion ratio . The proof of Proposition 7 introduces
Let and , and suppose the constant profile is a Nash equilibrium under . Then
The result separates two forces that interoperability sets off. Platforms extract the new off-network utility of the users they add, which pushes them to compete harder for users; and part of the users they add are diverted from rivals, which erodes the off-network revenue they draw from existing users. Proposition 7(b) says the first force wins whenever there is an outside option or at least three platforms, so users gain twice from interoperability: wider network effects and lower net fees. In the knife-edge duopoly without an outside option the forces cancel exactly. The authors read the result, together with their Proposition 6 on dominance, as "reason for optimism about the effects of increasing interoperability" (p. 23) and as an encouraging view of interoperability regulation (p. 3).
The paper proves the result on pp. 52–53. No machine-checked version of it, or of any result of the paper, exists. The formalization adds three things: a fully specified equilibrium notion (global Nash, not a first-order condition); an explicit verification that first-order conditions are sufficient in the parameter range used; and a precise statement of the case split, which the paper phrases through and here is stated through the primitives and .
The proof reduces the comparison of equilibria to the zeros of the one-variable function , and then applies the intermediate value theorem. Two steps carry the substance. First, every symmetric equilibrium must satisfy : this needs the first-order condition for a maximum of a profit function that depends on the deviating platform's fee through every platform's share. Second, every zero of must be a Nash equilibrium: this is false for large network effects, since profit can then fail to be concave and a platform can profit from a large deviation. The paper establishes sufficiency through concavity of profit in the platform's own share, which needs for all shares and the independence of from the platform's own fee. Identifying equilibria with solutions of the pricing formula, without this argument, proves a statement about stationary points, not about equilibria.
IsEquilibrium is the global Nash condition over every deviation . A formalization in which equilibrium means "the pricing formula holds", or in which the interoperability term is dropped from profit (so that affects nothing), would make the goal trivial and is not this theorem.Fin J; is called lam; is cast to in the symmetric closed forms nSym, phiSym, xi.Many networks are recorded as a sequence of snapshots: contact networks in epidemiology, communication graphs, brain connectivity measured over time, trade or transport links. A basic statistical question is whether the law generating the snapshots changed at some point. Two features make the question hard in practice. The networks are often sparse, so each snapshot carries little information. And links are missing: a pair of vertices is observed only with some probability, so an absent edge may mean "no link" or "not sampled".
Enikeeva and Klopp (arXiv:2106.14470, Operations Research, 2025) give minimax bounds for this testing problem. They treat both a known change time (Theorems 1 and 2) and an unknown change time (Theorem 3). This mission formalizes the unknown-time case, where the test scans a dyadic grid of candidate times. Two companion missions formalize the known-time upper bound (Theorem 1) and the lower bound (Theorem 2).
There are vertices and time points. At time the statistician observes a symmetric matrix with zero diagonal, . Here is the adjacency matrix of the network and records which pairs were sampled. The entries , , are independent over pairs and times, and
where is the connection-probability matrix (symmetric, zero diagonal), is the sampling matrix (symmetric, entries in , unit diagonal), and is the entrywise product.
The sparsity level bounds the expected observed degree: when .
Under the null hypothesis for all . Under the alternative there is with for and for . Both parameter pairs lie in , and the jump has energy at least :
where is the spectral norm. A test maps the data to . Its type I error is the largest rejection probability over the null class. Its type II error is the largest acceptance probability over all and all alternatives of energy at least .
The Matrix CUSUM at time contrasts the averages before and after :
The dyadic grid is , . Fix . The test (14) of the paper rejects when
For every there are constants and , depending only on , such that for all , , and : if
then the grid test with threshold has and .
Theorem 3 shows that not knowing the change time costs at most a constant factor and a term in the detection energy. Together with the lower bound of Theorem 2, which is of order , this makes the grid test rate-optimal when grows at least polylogarithmically in (Remark 3 of the paper). The statistic depends on the data only through spectral norms of CUSUM matrices, so it is cheap to compute. The threshold needs only the degree bound , which can be estimated from the observed degrees.
The paper's proof is complete on paper apart from one step noted below. No part of it is machine-checked. Formalizing it produces a checked finite model of Bernoulli network data with missing links, a reusable Matrix CUSUM, and a precise statement of a Bandeira–van Handel type bound for symmetric matrices with independent bounded entries. That bound is a standard tool in random-matrix statistics and is not yet available in Mathlib or on the platform.
The level of the test is a union bound over the grid combined with a high-probability bound on at a fixed time. The hard part is that bound, Lemma 12. A matrix Bernstein inequality gives a leading term , which is too large. The statement needs the sharp form , where the variance proxy enters without a logarithmic factor. Proposition 11 supplies this only for matrices whose entries are bounded by . The entries of are sums over time and are only bounded by about with high probability. The paper applies Proposition 11 "given the event" , but conditioning on that event destroys centring and independence, so a truncation argument is missing there.
The power analysis is elementary once Lemma 12 is available. Its one subtlety is that the change time ranges over all of , while the test inspects only the grid.
HighDimProb.RandomMatrices.matrixOpNorm.Nat.log 2 (T / 2). "" is ", ". The threshold uses the real .Welcome contributions: a proof of Proposition 11, or of any sharp spectral-norm bound that implies it; a rigorous proof of Lemma 12, repairing the conditioning step; and the elementary grid lemmas.
Online platforms run randomized experiments on subjects (users, sessions, orders) that arrive one at a time and must be assigned to a control or a treatment group on arrival, before later subjects are seen. The precision of a treatment-effect estimate depends on how similar the two groups are in their observed covariates. When the groups are badly balanced, the estimator's variance grows, and a large literature on covariate balancing (blocking, rerandomization, matched pairs) addresses this for offline experiments, where all covariates are known in advance.
J. Zhao and Z. Zhou (arXiv:2201.12936, Management Science, 2025) cast the online problem as an online matching problem. The cost of an assignment is the discrepancy, the weight of a minimum-cost perfect matching between the two groups, and they compare three designs against an oblivious adversary that fixes the covariate sequence in advance:
For one continuous covariate the pigeonhole design attains against for complete randomization. This mission concerns the multi-dimensional result, Theorem 9.
subjects arrive in order; is even. Subject carries a covariate vector with discrete coordinates, the -th in a finite set of size , and continuous coordinates in . Distances are Euclidean in . An assignment puts each subject in control () or treatment ().
The discrepancy of a split with is
the value of the assignment problem (1) of the paper.
The completely randomized design picks uniformly among the subsets of size ; is the mean of .
A pigeonhole design fixes a partition of the covariate space into pigeonholes. When subject arrives:
Theorem 9 uses the pigeonholes
uniform cells of edge on each continuous axis, for parameters and . The expected discrepancy is the mean of over the design's coins.
There are and , depending only on , such that for every even and every admissible arrival sequence,
Corollary 2 (the case ) is an extra theorem after the goal.
At Theorem 9 gives for . This is the order of the matched-pair design (Theorem 7), which sees all covariates in advance. An online design that commits to each assignment on arrival therefore loses at most a constant factor in dimension , and at most a factor at . For the completely randomized design no comparable upper bound is known for general sequences (p. 21). Lemma 5 is the paper's bound for complete randomization on the special family of full grids, and is of independent interest as a random-labelling matching estimate.
The results are proved on paper; none of them has a machine-checked proof, and the platform holds no item on them. A formalization would close the gaps of the printed argument:
Every statement in the mission is believed true.
The matched part (Component 1) is deterministic: paired subjects share a pigeonhole of diameter . The difficulty lies in the subjects left over: the unmatched ones and the subjects after . Their labels come from coins, but which subjects end up unmatched, and when occurs, depend on the same coins. So the leftover set is not a fixed set with independent fair labels, and the conditional binomial law used on p. ec22 does not hold literally.
A second obstacle is the random-matching estimate itself. Bounding the expected optimal matching between randomly labelled points of a grid at the rates () and () is a multi-scale problem of Ajtai–Komlós–Tusnády type. A single-scale count of imbalances per cell gives only times a power of that is too large.
Bool (false = control). The covariate space is EuclideanSpace ℝ (Fin q ⊕ Fin p). Admissible sequences have discrete coordinates in and continuous ones in , with (the paper's normalisation).The following formalizations would trivialize the mission and are ruled out:
A complete development needs a binomial Hoeffding bound and an exact analysis of the design's recursion (balance, alternation within a pigeonhole before ). It also needs a multi-scale bound on random bichromatic matchings of grid points. That bound is reusable for Lemma 5 and for matching estimators generally. Contributions on any milestone are welcome, as are proofs of Lemma 5 for arbitrary subsets of grid points, which is what Component 2 needs.
Admissions offices and employers that run affirmative action usually measure representation one identity dimension at a time: the share of women among those admitted, the share of Black applicants, and so on. Applicants, however, belong to intersectional groups (Black women, white men, …), and a policy that looks balanced along every dimension can still leave some intersectional group under-represented. The sociological literature calls this hidden inequality. Carvalho, Pradelski and Williams (hal-04788142v1; published in Management Science 71(5), 2025, doi:10.1287/mnsc.2023.03839) put the question into a threshold-admission model with score adjustments. Their Theorem 1 shows that, for generic score distributions, no nonintersectional policy (one that adjusts each dimension separately and composes the adjustments) makes every intersectional group's share among the accepted equal to its population share.
This mission formalizes the paper's positive counterpart, Proposition 3: for the weaker, per-dimension target that committees actually monitor, nonintersectional policies do succeed on a nonempty open set of distributions. Together the two results explain why reductive monitoring can report success while intersectional groups remain under-represented (the paper's Example 3).
A decision maker accepts a share of a unit-mass applicant pool. An applicant has a score in an interval and an identity with . Everyone with belongs to category . The joint law of (score, identity) lies in the space of probability measures on whose conditional score laws are continuous and have full support on . carries the relative weak topology. Write for the mass of group and for the mass of category .
A policy assigns to each group a score adjustment taken from a family of strictly increasing bijections that is rich (for all some has ) and commutative (). The additive shifts on are the leading example. Given a threshold , an applicant from group is accepted when , subject to the capacity constraint
The accepted share of group is , and the accepted share of category is .
The milestones use the paper's parameterization (Appendix D). Fix , let be the map in sending to , and for let compose over the coordinates with . Let be the resulting acceptance rate of category and the total acceptance rate, and let solve . For , condition (5) reads
with the accepted mass of group . The policy may be any nonintersectional policy in . The set is not specified.
The result. Proposition 3 shows that the obstruction in Theorem 1 belongs to the intersectional target, not to nonintersectional policies as such. A committee that monitors only per-dimension shares can meet its target with a nonintersectional policy on an open set of distributions, and the paper's Example 3 shows that such a policy can at the same time lower the acceptance rate of an intersectional group (Black men) that receives affirmative action. Taken together, the two results make the case for monitoring representation at the intersectional level.
Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs pieces that do not yet exist in Lean. One is the algebraic structure of rich commutative families (Lemma 1: such a is an abelian group acting simply transitively on ). Another is weak-topology continuity of acceptance masses on . A third is a continuity-of-argmax argument (Berge's maximum theorem) for and for minima over boxes, and the last is the Poincaré–Miranda theorem. Mathlib has neither Poincaré–Miranda nor Brouwer's fixed-point theorem.
A first attempt is to solve one coordinate at a time with the intermediate value theorem. This fails because the coordinates interact through the common threshold: raising admits more of category , pushes up, and lowers every other . A genuinely -dimensional fixed-point argument is needed, here Poincaré–Miranda on the box , which in turn needs to be continuous in .
The open-set claim needs more than one good distribution: condition (5) must survive weak perturbations of . That requires continuity of acceptance masses in , which holds only because conditional laws in are atomless (so threshold boundaries carry no mass), and continuity of the implicitly defined threshold jointly in and . Exhibiting the distribution of Lemma 4 is the easy part.
Scores live in the subtype of an order-connected with at least two points. Identities are Fin n → Bool with 0-based indices, and is coordinatewise addition in . is a subtype of ProbabilityMeasure on (product topology, Borel σ-algebra), with Mathlib's weak topology. Membership in asks, for every group with , that the conditional law have no atoms and charge every nonempty open subinterval. Groups with are unconstrained (convention C1; the paper is silent, and Lemma 4's has null groups). "Increasing" is read as strictly increasing, which is the same thing for bijections. Accepted masses are measures of sets, and divides by (Lean returns when ). The objects and are chosen elements, unique for rich commutative and respectively.
Disclosed additions to the page:
Ruled out:
Contributions welcome: the group structure of rich commutative families (shared with the companion mission on Theorem 1), weak continuity of threshold acceptance masses, a Poincaré–Miranda theorem for boxes in , which is reusable well beyond this paper, and Berge's maximum theorem.
In offline stochastic matching a graph is given in which every edge is present only with some known probability, and the only way to find out is to probe it: a probed edge that turns out to be present must be added to the matching at once. Each vertex may also limit how many of its edges are probed (its patience). The model captures applications in which a proposed match may be refused and an accepted one is binding: organ (kidney) exchange, online dating, advertising, crowdsourcing and ride sharing are the examples the paper lists (pp. 1–2), following Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009) and Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012).
Finding the best probing strategy is computationally hard, so algorithms are compared with a linear-programming relaxation that upper-bounds every strategy (Lemma 1, from Bansal et al.).
Timeline (general graphs with patience, as recorded on p. 2 of the paper).
This mission formalizes the per-edge bound behind the result, Theorem 1 of the paper.
A finite graph is given. Each edge is active independently with probability , and each vertex has a patience , the largest number of probes that may be made to edges incident to . Write for the edges incident to .
LP (3). A vector is feasible if
Here is the probability of probing .
Attenuation. An attenuation function assigns to edge the probability . It is effective (Definition 3) if and is convex on for every . The two functions used here are and (Definition 4 with ).
Algorithm 1. Draw independent coins and for every edge, and process the edges in a uniformly random order. When is processed it is free if both endpoints are unmatched and have made fewer than their patience in probes. If is free and , probe ; if it is active (coin ), match it and both endpoints. Finally
If every vertex has patience at least , is feasible for LP (3), and is or , then for every edge
The probability is over the random order and the coins of Algorithm 1.
The milestones are numbered results and displays of the paper, in the order its argument uses them:
The result. Equation (4) of the paper writes the expected weight of the algorithm's matching as . Theorem 1 therefore gives at least , and with an optimal LP solution and the LP upper bound of Bansal et al. this is a -approximation for stochastic matching on general graphs with patience at least . The bound is per edge, which is the form a random-order contention resolution scheme needs: the same algorithm rounds fractional matchings edge by edge.
Formalizing it. The paper's proof combines a reduction (Lemma 2), the analytic bound of Lemma 3, the tail bounds of Lemmas 4–5, an exchange argument (Lemma 6) resting on a graph construction from another paper, and a case analysis in the patience values that is closed by numerical minimization of explicit integrals over two or three parameters ("we numerically minimize (12)", p. 13; "we numerically verify", p. 15). The margins are thin: the bound in the last case exceeds by about . No part of this argument has a machine-checked proof. A formal proof would certify both the probabilistic reasoning and every numerical step, and would supply a reusable finite model of random-order probing algorithms with patience, of which the platform has none.
The obvious argument bounds by a product over the two endpoints of and applies a Poisson approximation to the number of probes at each endpoint. For an endpoint of patience that approximation is only valid for arrival times , a threshold that can be , and the bound it gives, about (display (16)), falls below . Closing that case is what requires the exchange argument of Lemma 6. Beyond it, the remaining cases are optimization problems over the LP mass at each endpoint, which the paper settles by computer and a formal proof must settle by rigorous bounds.
EdmondsMatching65.Polyhedron.Graph (loopless); the goal adds that the endpoint map is injective, since the paper's edges are pairs . Patience is ℕ∞, with allowed; "minimum patience " is at every vertex.In stochastic matching a platform knows, for every potential pair, the probability that the pair would succeed, but learns whether it does only by trying it, and a successful trial is binding. Kidney exchange, online dating and labour markets are the standard examples: a crossmatch test, a date or an interview is a probe whose outcome is random, and a positive outcome commits both sides. Each participant also tolerates only a limited number of attempts, its patience. The algorithmic question, studied since Chen, Immorlica, Karlin, Mahdian and Rudra (ICALP 2009), is how much of the optimal adaptive strategy's expected weight a simple, non-adaptive rule can secure.
The modern approach solves a linear programming relaxation and rounds its fractional solution online, through a contention resolution scheme: edges are examined one at a time, and an edge is used only when it does not conflict with earlier decisions. Bansal, Gupta, Li, Mestre, Nagarajan and Rudra (Algorithmica 2012) introduced the relaxation (LP (3) below) and showed that it bounds every adaptive probing algorithm. Baveja, Chavan, Nikiforov, Srinivasan and Xu (Algorithmica 2018) analysed processing edges in a uniformly random order. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892) add attenuation: an independent coin that sometimes skips an edge on purpose, so that edges likely to block others are probed less often. This mission formalizes their guarantee when patience is unlimited.
Let be a finite graph. Each edge is active independently with known probability , and each vertex has a patience , the maximal number of edges at that may be probed. Write for the edges incident to . A vector is feasible for LP (3) when
is read as the probability of probing , and as the probability that is matched.
An attenuation function is a map , and the attenuation of an edge is . The paper's examples (Definition 4) are , , and . A function is effective (Definition 3) when and is convex on for every .
Algorithm 1 draws independent coins and and processes the edges in a uniformly random order. When it reaches , it probes if is free (both endpoints unmatched and with remaining patience), and . A probe uses one unit of patience at both endpoints and reveals the activeness ; if , both endpoints are matched. The edge is safe when, before is processed, each endpoint has received at most probes and no earlier edge at or has .
If every patience is , is feasible for LP (3), and is or with , then for every edge
On a star graph with infinite patience and the third attenuation function, . It comes with the identity of p. 16 behind it: for the third function, for all . Both are plain items of the mission, not milestones.
By (4), Corollary 5 bounds the expected weight of Algorithm 1 by , and with an optimal and the bound of Bansal et al. this is a -approximation for stochastic matching without patience constraints. Because the bound holds edge by edge and for every feasible , it also gives a random-order contention resolution scheme for the matching polytope, which is the form reused for other objectives and in online settings. Corollary 6 is the rank-one analogue with the constant .
None of this is formalized. Stochastic probing, patience, random-order processing and attenuation have no counterpart in Mathlib or on the platform. The mission produces a finite, executable model of a probing algorithm run on random coins and a random order, in which these probabilities are exact finite sums; that model is reusable for the other results of the paper and for related rounding schemes. The paper's results are proved in §3.2 (pp. 9–15) and §3.3 (p. 16); the milestones are the steps used there.
The obvious argument treats the edges at the two endpoints of as independent obstacles, each blocking with probability proportional to its LP value. That fails because being free is not a product event: whether an earlier edge blocks depends on whether was itself free, which depends on the whole run before . A second difficulty is uniformity. The bound must hold for every feasible , and the LP mass at an endpoint can be split among arbitrarily many edges of arbitrary sizes; the quantities involved are not monotone in how that mass is split, and the bound must survive the worst split, including the limit of many tiny edges. The choice of attenuation matters here: the third function of Definition 4 violates the convexity condition of Definition 3, which is why Corollary 6 is not covered by the paper's argument. Finally, the paper reasons with continuous arrival times, while the model has only permutations and finitely many coins.
EdmondsMatching65.Polyhedron.Graph (finite, loopless, parallel edges allowed). Probabilities , LP values , weights and attenuations are real; patience is in ℕ∞, with . Every probability is a finite average over the orders of and over all outcomes of the coins , , , with product weights. The paper's independent uniform arrival times induce exactly this uniform order. The run of Algorithm 1 is computed step by step, with matched vertices and probe counters; free, probed and safe are events of that run.