The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Quantum query algorithms are known to beat classical ones on problems with algebraic structure -- period finding, hidden subgroups, forrelation. No such speedup is known for a problem with no structure at all. Aaronson and Ambainis proposed making that observation into a theorem, and reduced it to a question with no quantum content: a statement about bounded low-degree polynomials on the Boolean cube (Aaronson--Ambainis 2009).

The question has resisted since. A timeline of what is actually established:

2009. Aaronson and Ambainis state the conjecture and prove that it implies almost-everywhere classical simulation of quantum query algorithms.
2012. Montanaro settles the case of block-multilinear forms whose coefficients all have the same magnitude.
2016. O'Donnell and Zhao reduce the general conjecture to a restricted class, the one-block decoupled polynomials.
2019. Aaronson surveys a decade of partial progress (retrospective).
2022. Bansal, Sinha and de Wolf prove the conjecture for completely bounded degree- $d$ block-multilinear forms, obtaining influence $1/\mathrm{poly}(d)$ at constant variance (arXiv:2203.00212).
2024. The conjecture is established for a non-negligible fraction of random restrictions (arXiv:2402.13952).

The cases that are settled are settled under structural hypotheses -- block-multilinearity, complete boundedness, symmetry, Boolean range. The general statement is open.

Setting

Let $N$ be a positive integer. The Boolean cube is $\{0,1\}^N$ , carrying the uniform distribution; a point $x$ is identified with the $0/1$ real vector it names, so a real multivariate polynomial $p$ in $N$ variables has a value $p(x)$ at each cube point. For a function $f$ on the cube write

\mathbb{E}[f]=2^{-N}\sum_{x\in\{0,1\}^N}f(x).

The variance of $p$ is $\operatorname{Var}[p]=\mathbb{E}\big[(p-\mathbb{E}[p])^2\big]$ . Writing $x^{\oplus i}$ for $x$ with its $i$ -th bit flipped, the influence of coordinate $i$ on $p$ is

\operatorname{Inf}_i[p]=\mathbb{E}\big[(p(x)-p(x^{\oplus i}))^2\big].

These are the combinatorial forms of both quantities, as used in the source; no Fourier--Walsh expansion is required to state anything below. The degree of $p$ is its total degree as a polynomial. Call $p$ bounded when $0\le p(x)\le 1$ at every cube point -- a condition imposed only on the cube, not on all of $\mathbb{R}^N$ .

Target

The goal is the conjecture in the shape stated by its authors: there is an absolute constant $C$ such that for all $N$ , all $d$ , every polynomial $p$ of degree at most $d$ that is bounded on the cube, and every $\varepsilon>0$ with $\operatorname{Var}[p]\ge\varepsilon$ , some coordinate $i$ satisfies

\operatorname{Inf}_i[p]\;\ge\;\Big(\frac{\varepsilon}{d}\Big)^{C}.

The constant $C$ is quantified outermost and may depend on nothing. That uniformity is the entire content: bounds that degrade exponentially in $d$ are already known, and a goal naming a specific exponent would be superseded by the next improvement.

Significance

The result itself. Aaronson and Ambainis prove that the conjecture implies that the acceptance probability of any bounded-error $T$ -query quantum algorithm on a Boolean input can be approximated, to small error on all but a small fraction of inputs, by a classical algorithm making $\mathrm{poly}(T)$ queries. Quantum speedups would then require structure in a precise sense. The conjecture also has purely classical content, asserting that boundedness plus low degree forces variance to concentrate on some single coordinate rather than spread across all $N$ . Without it, no such concentration is known at any rate polynomial in $1/d$ .

Formalizing it. The conjecture is open, so this mission does not formalize a known proof of the goal. What it produces is a machine-checked statement of the conjecture together with formalizations of the partial results above, each currently existing only on paper. The milestone chain also yields reusable infrastructure for analysis of Boolean functions, of which Mathlib currently contains none: no Fourier--Walsh expansion, no influence, no variance on the cube.

Difficulty

The elementary bound is the Poincare inequality on the cube, $4\operatorname{Var}[p]\le\sum_i\operatorname{Inf}_i[p]$ , which yields a coordinate with influence at least $4\varepsilon/N$ . This is tight for the dictator $p(x)=x_1$ and depends on $N$ , so it says nothing: the conjecture demands a bound free of $N$ entirely.

The natural repair is the route available when $p$ takes only the values $0$ and $1$ . A Boolean-valued polynomial of degree $d$ depends on boundedly many coordinates, which immediately produces an influential one. That argument does not survive relaxing the range to the interval $[0,1]$ : a bounded real-valued polynomial of low degree need not depend on boundedly many coordinates, and every known substitute loses a factor exponential in $d$ . Closing the gap between exponential and polynomial dependence on $d$ is the difficulty, and it is where all of the partial results stop.

Formalization scope

Polynomials are MvPolynomial (Fin N) ℝ and degree is Mathlib's totalDegree, so the statement needs no bespoke notion of degree. Expectation is a finite sum scaled by $2^{-N}$ rather than a measure-theoretic integral, keeping every definition elementary. Bit flipping is Function.update x i (!x i). Boundedness is asserted at cube points only. Variance and influence are the combinatorial definitions above, published as the definition AaronsonAmbainis.

Three points close off degenerate readings. The exponent $O(1)$ of the source is rendered as an existentially quantified natural number with no leading multiplicative constant, since admitting one weakens the claim. Taking that exponent to be $0$ would demand influence at least $1$ and is therefore not a trivializing choice, while larger exponents only weaken the bound; the content is that some fixed exponent suffices for all $N$ and $d$ at once. The hypothesis $\deg p\le d$ is universally quantified over $d$ , which is equivalent to the source's exact-degree form because the smallest admissible $d$ gives the strongest conclusion. The cases $N=0$ and $d=0$ are vacuous, since $0<\varepsilon\le\operatorname{Var}[p]$ fails for a constant polynomial.

A complete development needs, beyond the published definitions, a Fourier--Walsh layer with Parseval's identity, the level- $k$ machinery used by the partial results, and -- for the completely bounded case -- operator-space norms on multilinear forms. All of the Boolean-analysis material is reusable well beyond this mission. Contributions of any milestone are welcome, as are alternative formalizations of the definitions in function-level rather than polynomial-level form.

Out of scope: the quantum simulation consequence is not formalized here. Stating it requires a formal quantum query model, which no Lean library currently provides.

Selected references

S. Aaronson, A. Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014) 133--166; arXiv:0911.0996. Conjecture 6.
N. Bansal, M. Sinha, R. de Wolf, Influence in Completely Bounded Block-multilinear Forms and Classical Simulation of Quantum Algorithms, CCC 2022; arXiv:2203.00212.
Aaronson--Ambainis Conjecture Is True For Random Restrictions, 2024; arXiv:2402.13952.
S. Aaronson, The Aaronson-Ambainis Conjecture (2008-2019), blog retrospective.
S. Arunachalam, J. Briet, C. Palazuelos, Quantum query algorithms are completely bounded forms, SIAM J. Comput. 48 (2019); arXiv:1711.07285.
AIM problem list, Analysis on the hypercube with applications to quantum computing, aimpl.org/hypercubequantum.

4 thms2 active usersReviewed

Completed

Combinatorics Probability·Captain: sr

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$ . Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$ . It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$ .

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$ . A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$ ; here vertices are labeled $0, \dots, N-1$ . A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$ -set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$ . This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$ -set is a graph with neither a $k$ -clique nor an independent $k$ -set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$ ", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

R(k) > 2^{k/2}, \qquad k \ge 3

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$ -set.

Stronger: the three steps of the proof, as separate targets

Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$ ,

\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.

Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.

Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$ -set in $G$ is at most

\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$ .

Difficulty

The central difficulty is that the bad events — "the $k$ -set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$ -sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$ ; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$ -set ( $2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$ ; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$ -set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$ -sets of $G$ .

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$ . The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$ , is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic- $k$ -set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$ ; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$ .
Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$ , for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$ ; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$ ; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$ .

5 thms2 active usersReviewed

Completed

Captain: wenxinzhang

Primal-Dual Online Load Balancing on Unrelated MachinesTextbook

The model

Fix $m \ge 1$ machines and $n$ jobs arriving one at a time in the order $0, \dots, n-1$ . Job $i$ carries a whole vector of nonnegative loads $\tilde p(i,j)$ , one per machine, with no assumed relationship between the entries — the same job may be cheap on one machine and unplaceable on another. This is the unrelated machines model. When job $i$ arrives its load vector becomes visible, and the algorithm must commit it to a single machine immediately and irrevocably, knowing nothing about the jobs still to come. A machine's load is the sum of $\tilde p(i,j)$ over the jobs assigned to it.

The setting formalized here is one normalized phase: loads are already scaled by a guessed makespan, so machine $j$ counts as eligible for job $i$ exactly when $\tilde p(i,j) \le 1$ . The phase is allowed to give up rather than assign badly — it fails if an arriving job has no eligible machine, or if an internal weight grows past $1$ .

The algorithm and the guarantee

The algorithm keeps a weight $x(j)$ per machine, initialized to $1/(2m)$ . Job $i$ goes to the eligible machine $\ell$ minimizing $\tilde p(i,\ell)\, x(\ell)$ ; that machine's weight is then scaled by $1 + \tilde p(i,\ell)/2$ , so a machine becomes exponentially unattractive as it fills. The weights are the primal variables of the covering LP

\min \sum_j x(j) + \sum_i z(i) \quad \text{s.t.} \quad \tilde p(i,j)\,x(j) + z(i) \ge 1 \ \text{ for every eligible pair } (i,j),

and each assignment raises one dual variable $y(i,\ell)$ to $1$ . The guarantee follows from weak duality rather than a bespoke potential argument, which is the point of the primal-dual method.

The goal theorem states that if the dual admits a feasible solution putting unit total mass on every job — the certificate that the guessed makespan was large enough — then the phase does not fail, every job is assigned, and every machine ends with load

\sum_{i \,\text{assigned to}\, j} \tilde p(i,j) \ \le\ \frac{\ln(3m)}{\ln(3/2)}.

The source states this as $O(\log m)$ ; the explicit constant is what its proof yields.

Note that the load bound alone is not the theorem: it holds vacuously when the phase assigns nothing, and the milestones state it that way deliberately. The content is the conjunction of succeeded, assigns all, and the bound.

Scope

The doubling wrapper — guess a makespan, run a phase, double the guess and restart on failure — is what turns this phase into an $O(\log m)$ -competitive online algorithm. It is outside this mission; the guarantee proved here is the conditional single-phase statement. The milestones break the argument into weak duality for finite LPs, the load bound, primal feasibility at each prefix, the primal objective identity, and the failure certificate.

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009, Chapter 8, pp. 193–196 (Theorem 8.1). PDF · doi:10.1561/0400000024

10 thms2 active usersReviewed

Probability Quantum Information·Captain: mikedeng1

Quantum Speedup of Monte Carlo Methods 1: With Var(v(A)) ≤ σ² and ε < 4σ, Algorithm 3 Estimates E[v(A)] to Additive Error ε with Probability at Least 2/3Research Paper

Why estimate a mean with a quantum algorithm?

Many computational tasks produce a real number by running a randomized procedure once, then estimate its expected value by running that procedure repeatedly. The number of repetitions needed for a given additive accuracy depends on the output variance. Montanaro's Quantum speedup of Monte Carlo methods studies the same estimation problem when the procedure can be run coherently as a quantum algorithm and its unitary part can also be inverted. The bounded-variance result gives an estimator whose dependence on the requested accuracy is approximately linear in $1/\epsilon$ , compared with the quadratic dependence of ordinary sampling, up to logarithmic factors and the paper's model-specific operation counts. The exact asymptotic claims are in Theorem 5 of the pinned preprint, p. 12.

This mission concentrates on the probability and accuracy claim of that theorem. It includes the mean-estimation result for a nonnegative output from Lemma 4, because Algorithm 3 invokes that estimator twice after centering a general real output. The underlying amplitude-estimation theorem is a separate, already posed result, QAmpEst.Est.theorem_12; this mission uses the accuracy guarantee stated in Montanaro's Theorem 3 as the interface to that subroutine.

Outputs, truncations, and estimates

Let $X=v(\mathcal A)$ denote the real output of a quantum algorithm $\mathcal A$ under one run, and let $P$ be its probability law. The mean is $\mathbb E[X]$ , and the variance is $\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]$ . The result assumes a known $\sigma>0$ with $\operatorname{Var}(X)\le\sigma^2$ . Although the paper describes a circuit that prepares and measures $X$ , its accuracy statements depend on the distribution of $X$ ; the Lean interface therefore represents a run as a measurable real random variable on a probability space.

For real thresholds $a<b$ , the truncation $X_{[a,b)}$ returns $X$ when $a\le X<b$ and zero otherwise. The variants $X_{<a}$ and $X_{\ge b}$ retain the output below $a$ and at or above $b$ , respectively. They do not clip a value to a threshold. The $L^2$ size is $\|X\|_2=\sqrt{\mathbb E[X^2]}$ . These are the output transformations defined in §2.2, p. 9, and used in Lemma 4, pp. 10–11.

Algorithm 2 estimates a nonnegative mean using the base interval $[0,1)$ and the half-open bands $[2^{\ell-1},2^\ell)$ for $1\le\ell\le k$ . It sets $k=\lceil\log_2(1/\epsilon)\rceil$ and $t_0=\lceil D\sqrt{\log_2(1/\epsilon)}/\epsilon\rceil$ , then adds the base estimate to $2^\ell$ times each band estimate. A successful Algorithm 1 call means that its estimate of a $[0,1]$ -valued output $Y$ differs from $\mathbb E[Y]$ by at most $C(\sqrt{\mathbb E[Y]}/t+1/t^2)$ , the accuracy bound of Theorem 3, pp. 8–9.

Algorithm 3 rescales $X$ by $\sigma$ , draws one sample $m$ from $X/\sigma$ , and centers the rescaled output at $m$ . It feeds the negative and nonnegative parts, each divided by four, to Algorithm 2 at accuracy $\epsilon/(32\sigma)$ and recombines their estimates. The two calls are specified to fail with probability at most $1/9$ each; the paper describes boosting Algorithm 2's initial success probability for this use on p. 11.

Formalization targets

Lemma 4: nonnegative mean accuracy

When every Algorithm 1 call satisfies its accuracy bound and $0<\epsilon<1/2$ , the output $\widetilde\mu$ of Algorithm 2 obeys

|\widetilde\mu-\mathbb E[X]|\le\epsilon(\|X\|_2+1)^2.

The constant $D>0$ is chosen once for a fixed positive universal constant $C$ from Theorem 3. It is independent of $X$ and $\epsilon$ .

Theorem 5: bounded-variance accuracy

For $\operatorname{Var}(X)\le\sigma^2$ , $\sigma>0$ , and $0<\epsilon<4\sigma$ , Algorithm 3 returns $\widehat\mu$ with

\Pr\bigl(|\widehat\mu-\mathbb E[X]|\le\epsilon\bigr)\ge\frac23.

This is the mission goal. Its probability is over the preliminary sample and both subsequent estimation runs. The milestone list follows the exact displayed statements used in Lemma 4 and the proof of Theorem 5, with their source pages.

What the result supplies

Theorem 5 turns an estimator for nonnegative outputs with finite second moment into one that handles signed outputs whose variance is bounded, without assuming a bound on the magnitude or mean of the output. That extension matters when the quantity being averaged can be negative or has a large offset: a second-moment bound on $X$ itself would then be much stronger than the paper's variance hypothesis. The stated error and success probability are the mathematical guarantee on which the paper's resource comparison rests; the comparison itself includes quantum operations absent from the measure-theoretic statement.

The formal development supplies reusable definitions of truncations, dyadic estimates, and the centered positive and negative parts, together with precisely quantified probability claims. It leaves Lemma 4 and Theorem 5 as open Lean proof targets. The amplitude-estimation statement behind Theorem 3 is already posed separately on Prove2Me, while the composed bounded-variance result and the displayed intermediate claims are the new targets here.

Where the difficulty lies

A bound for one $[0,1]$ -valued call does not directly bound the mean of a signed, unbounded output. Truncating after finitely many bands leaves a tail, and the sum of errors over the retained bands can grow with their weights. The theorem must control both effects while keeping $D$ independent of the output distribution. For the signed case, the initial sample is random; its deviation, the two later failures, and the scale of the centered output all contribute to the final probability. Replacing that sample by the exact mean would remove a substantive part of the claim.

Formalization scope

Lean uses probability measures and measurable real outputs for the laws of $v(\mathcal A)$ and Algorithm 3's preliminary sample. The law of that sample is fixed to the image law of $X/\sigma$ , so it cannot be selected arbitrarily. The successful-call predicate names the actual truncated outputs and the paper's $k$ and $t_0$ formulas; it does not assume Lemma 4's final error bound. The sample space carrying the later estimates is allowed to encode their joint dependence on the preliminary sample. Events are measured with extended nonnegative real values.

The $L^2$ hypotheses state that the second moment is finite. In Mathlib the real-valued variance and the integral can return a default value on a nonintegrable input, which would make a bare variance inequality or a bare $\|X\|_2$ bound misleading. The paper implicitly uses finite variance where those quantities occur. The condition $0<\epsilon$ makes the divisions and logarithms in the algorithm parameters meaningful. The natural-number expression $\ell-1$ occurs only on bands indexed by $\ell\ge1$ .

The quantum circuit for Algorithm 1, the construction of an inverse unitary, and the $O(\cdot)$ copy and operation counts are outside the formal statements. Their interface is Theorem 3's numerical accuracy event. Contributions to the dyadic inequalities, the finite-variance probability bound, and their composition into the final event are in scope. The definitions are also useful for other mean estimators that split a real output into bounded pieces.

Selected references

Ashley Montanaro, Quantum speedup of Monte Carlo methods, arXiv:1504.06987v3 [quant-ph], 2017, especially §§2.1–2.3, pp. 8–12. Pinned preprint.
Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation, Contemporary Mathematics 305, 2002. arXiv preprint.

9 thms1 active userReviewed

Linear algebra Optimization Quantum Information·Captain: mikedeng1

Optimization by Decoded Quantum Interferometry 1: The Semicircle Law — the Optimal Degree-ℓ DQI State Satisfies ⟨s⟩/m → (√(μ(1−ρ)) + √(ρ(1−μ)))² When 2ℓ + 1 < d⊥Research Paper

Motivation

Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over $\mathbb F_p$ , satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.

Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.

Setting

Fix a prime $p$ . A max-LINSAT instance is a matrix $B\in\mathbb F_p^{m\times n}$ with rows $\mathbf b_1,\dots,\mathbf b_m$ and subsets $F_1,\dots,F_m\subseteq\mathbb F_p$ ; constraint $i$ asks that $\mathbf b_i\cdot\mathbf x\in F_i$ (Definition 2.1). Throughout, $m>n$ and every $F_i$ has the same size $r\in\{1,\dots,p-1\}$ . Put $f_i(a)=+1$ if $a\in F_i$ and $-1$ otherwise, and

f(\mathbf x)=\sum_{i=1}^m f_i(\mathbf b_i\cdot\mathbf x),\qquad s(\mathbf x)=\#\{i:\mathbf b_i\cdot\mathbf x\in F_i\}.

For a real polynomial $P$ of degree at most $\ell$ , the DQI state is $|P(f)\rangle=\sum_{\mathbf x\in\mathbb F_p^n}P(f(\mathbf x))|\mathbf x\rangle$ , normalized so that $\sum_{\mathbf x}P(f(\mathbf x))^2=1$ . Measuring it in the computational basis returns $\mathbf x$ with probability $P(f(\mathbf x))^2$ , so the expected number of satisfied constraints is

\langle s\rangle=\sum_{\mathbf x}P(f(\mathbf x))^2\,s(\mathbf x),

and $\langle s^{(m,\ell)}\rangle_{\rm opt}$ is its supremum over all such $P$ .

The dual code is $C^\perp=\{\mathbf d\in\mathbb F_p^m:B^T\mathbf d=0\}$ and $d^\perp$ is the least Hamming weight of a nonzero codeword. The condition $2\ell+1<d^\perp$ says that syndromes of errors of weight up to $\ell$ (and a little more) determine the error.

The analysis passes through rescaled constraint functions $g_i=(f_i-\bar f)/\varphi$ with Fourier transforms $\tilde g_i$ , the elementary symmetric polynomials $P^{(k)}$ evaluated at the $g_i(\mathbf b_i\cdot\mathbf x)$ , and the $(\ell+1)\times(\ell+1)$ symmetric tridiagonal matrix $A^{(m,\ell,d)}$ with diagonal $0,d,2d,\dots,\ell d$ and off-diagonal entries $a_k=\sqrt{k(m-k+1)}$ , at $d=(p-2r)/\sqrt{r(p-r)}$ .

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Fix $p$ , $r$ and $\mu\ge0$ . For any sequence of instances with $m\to\infty$ , $\ell/m\to\mu$ and $2\ell+1<d^\perp$ , writing $\rho=r/p$ ,

\lim\frac{\langle s^{(m,\ell)}\rangle_{\rm opt}}{m}=\begin{cases}\big(\sqrt{\mu(1-\rho)}+\sqrt{\rho(1-\mu)}\big)^2,&\rho\le1-\mu,\\ 1,&\text{otherwise.}\end{cases}

For $\rho=\tfrac12$ the curve is $\tfrac12+\sqrt{\mu(1-\mu)}$ , a semicircle, which gives the theorem its name.

Milestones

The normalization of the rescaled $g_i$ , (37)–(40).
Lemma A.1: under a common quadratic identity, $P(x_1+\dots+x_m)$ is a fixed linear combination of elementary symmetric polynomials.
The counting identity (68), $\sum_{|\mathbf y|=k}|\tilde g(\mathbf y)|^2=\binom mk$ , and the Fourier picture (65) of the DQI state.
Lemma 9.1 (norm $=\|\mathbf w\|^2$ when $2\ell<d^\perp$ ) and Lemma 9.2 (the expected count is $\frac{mr}p+\frac{\sqrt{r(p-r)}}p\mathbf w^TA^{(m,\ell,d)}\mathbf w$ when $2\ell+1<d^\perp$ ).
The finite-size identity (131): $\langle s^{(m,\ell)}\rangle_{\rm opt}/m=\rho+\sqrt{\rho(1-\rho)}\,\lambda_{\max}^{(m,\ell,d)}/m$ .
Lemma 9.3, $\lambda_{\max}^{(m,\ell,d)}/m\to\mu d+2\sqrt{\mu(1-\mu)}$ , with its lower half (114) and the Gershgorin bound (129).
The algebra (132) and (136)–(137) that produce the closed form.

Significance

The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, $r/p$ and $\ell/m$ , and moves every question about an instance into coding theory: how large a $d^\perp$ the instance's dual code has, and whether it can be decoded efficiently up to $\ell$ errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations $\sqrt{p^{n-k}\binom mk}$ , character sums over $\mathbb F_p$ ), the claim that every degree- $\ell$ DQI state is a combination of the $|P^{(k)}\rangle$ and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the $f_i$ where the normalization requires the rescaled $g_i$ , and the "otherwise $=1$ " branch of Theorem 4.1 is argued only briefly on p. 34.

Difficulty

The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on $\lambda_{\max}$ from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under $d\ge-(m-2\ell)/\sqrt{\ell(m-\ell)}$ , which is exactly the regime $\rho\le1-\mu$ . In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit $1$ needs a separate argument; the observation that $\langle s\rangle_{\rm opt}$ "increases in $r$ ", printed on p. 34, does not give it at fixed $p$ and $r$ . A second difficulty is that $\langle s\rangle_{\rm opt}$ is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors $\mathbf w$ ; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.

Formalization scope

All objects live in the namespace DQI.Semicircle and one definitions file. $\mathbb F_p$ is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from $0$ . $\omega_p^a=\exp(2\pi i\,a/p)$ is computed from the representative of $a$ in $\{0,\dots,p-1\}$ . Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum $\langle s\rangle_{\rm opt}$ is the real supremum over exactly the normalized polynomials of degree at most $\ell$ evaluated at $f(\mathbf x)$ ; its set is nonempty (constant polynomials) and bounded by $m$ . The dual-distance condition is "every nonzero $\mathbf d$ with $B^T\mathbf d=0$ has weight $>t$ "; $d^\perp$ is never an infimum, and $m>n$ (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces $2\ell<m$ . $\lambda_{\max}$ is the supremum of the real spectrum. The limit " $m\to\infty$ with $\ell/m$ fixed" is any sequence of instances with $m_j\to\infty$ and $\ell_j/m_j\to\mu$ , with $p$ and $r$ fixed along it. Convergence of the ratio includes irrational $\mu$ with integer sizes.

Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the $g_i$ rather than the printed $f_i$ ; (129) assumes $\ell\ge1$ to avoid dividing by $\sqrt0$ ; Lemma 9.3 imposes its hypothesis on $d$ only when $\ell_j\ge1$ ; (114) is stated as a $\liminf$ with an explicit $\varepsilon$ .

A formalization that replaces $\langle s\rangle_{\rm opt}$ by a supremum over all states (which gives $1$ ), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single $m$ is not this theorem and is ruled out by the definitions above.

Needed infrastructure: Fourier analysis on $\mathbb F_p^n$ (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite- $m$ bounds on $\lambda_{\max}$ are welcome.

Selected references

S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025. https://arxiv.org/abs/2408.08292
S. Gershgorin, Über die Abgrenzung der Eigenwerte einer Matrix, Izv. Akad. Nauk SSSR, Ser. Fiz.-Mat. 6, 749–754, 1931.
R. G. Gallager, Low-Density Parity-Check Codes, IRE Trans. Inform. Theory 8(1), 21–28, 1962. https://doi.org/10.1109/TIT.1962.1057683

14 thms1 active userReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 3: In Simultaneous Offering With Values at Least τ, a Truncated-LP Value-Ordered Policy Earns ≥ α^τ_k Times the LP BoundResearch Paper

Motivation

A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves positions empty; sending too many hires beyond capacity at a cost. This trade-off is the same as overbooking in revenue management (airline seats, hotel rooms), with the difference that candidates are heterogeneous in both value and acceptance probability.

Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three hiring-pipeline models through linear programming relaxations. This mission formalizes their lower bound for the third model, Simultaneous Offering (§3.3 and §6 of the paper). The question it answers is practical: how much is lost if the firm restricts itself to value-ordered policies, which send offers to the $m$ most valuable candidates for some $m$ , instead of searching over all $2^n$ offer sets? Value-ordered policies are natural, because a firm rarely wants to withhold offers from its best candidates, and the optimal one is computable by a short dynamic program. The paper shows (Example 1, p. 25) that they can be arbitrarily bad in general, and that they are provably good when every candidate's value is bounded below.

Setting

An instance $I=(k,n,p,v)$ has $k$ positions and $n$ candidates, $1\le k\le n$ . Candidate $i$ accepts an offer independently with probability $p_i\in[0,1]$ and then contributes value $v_i\ge0$ . Candidates are labelled so that $v_1\ge v_2\ge\dots\ge v_n$ . The firm chooses an offer set $S\subseteq[n]$ ; with $A\subseteq S$ the random set of acceptances, the reward is

\sum_{i\in A}v_i-\big[\,|A|-k\,\big]^+,

the cost per candidate hired beyond capacity being normalised to $1$ . $\mathrm{OPT}_{\mathrm{sim}}(I)$ is the best expected reward over offer sets. For $\tau>0$ the instance is $\tau$ -bounded, $I\in\mathcal I^\tau_{\mathrm{sim}}$ , if $v_i\ge\tau$ for all $i$ ; the interesting range is $\tau\in(0,1)$ , since for $\tau\ge1$ offering to everyone is optimal.

The benchmark is the LP relaxation

\mathrm{LP}_{\mathrm{sim}}(I)=\max_{y,z}\ \sum_{i}v_ip_iy_i+z\quad\text{s.t.}\quad z\le k-\sum_ip_iy_i,\ \ z\le0,\ \ 0\le y_i\le1,

which charges the overage cost on the expected number of hires. Write $V_{\mathrm{high}}=\{i:v_i>1\}$ and $P_{\mathrm{high}}=\sum_{i\in V_{\mathrm{high}}}p_i$ .

The algorithm $\mathrm{ALG}^s_{\mathrm{sim}}$ , for $s\in[0,1]$ , takes an optimal LP solution $y$ , scales its total mass $\sum_iy_ip_i$ by $s$ to $\kappa$ , and fills mass $\kappa$ from the most valuable candidate down: $y'_i=1$ while the prefix mass $\sum_{l\le i}p_l$ stays at most $\kappa$ , one fractional entry, then zeros. Offers are then sent independently with probabilities $y'_i$ , so the algorithm randomises between two value-ordered policies. Its expected reward is $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)$ .

The guarantee involves the truncated Poisson mean $\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]=\sum_{j\ge0}\min\{j,k\}e^{-\lambda}\lambda^j/j!$ and

\alpha^\tau_k=\sup_{0\le s\le1}\Big(s-\frac{s}{\tau}+\frac{\mathbb E[\min\{\mathrm{Pois}(sk),k\}]}{\tau k}\Big).

Formalization targets

Goal: Theorem 3 (p. 30)

For $\tau\in(0,1)$ , every $I\in\mathcal I^\tau_{\mathrm{sim}}$ , every optimal solution of $\mathrm{LP}_{\mathrm{sim}}(I)$ and a maximiser $s^*\in[0,1]$ of the objective defining $\alpha^\tau_k$ ,

R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}(I)\ \ge\ \alpha^\tau_k\,\mathrm{LP}_{\mathrm{sim}}(I).

Milestones

Lemma 10 (p. 27): $\mathrm{LP}_{\mathrm{sim}}(I)\ge\mathrm{OPT}_{\mathrm{sim}}(I)$ .
Lemma 11 (p. 27): some optimal LP solution is a filled prefix $y=(1,\dots,1,y_j,0,\dots,0)$ with $y_j>0$ .
Lemma 12 (p. 28): the total mass of such a solution is $P_{\mathrm{high}}$ if $P_{\mathrm{high}}>k$ and $\min\{k,P_{\mathrm{total}}\}$ otherwise (posed under the disclosed hypothesis $v_i>0$ , $v_i\ne1$ , $p_i>0$ ).
Monotonicity (App. D.5, p. ec16): $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ is decreasing in $x$ .
Proposition EC.2 (p. ec3): $\mathbb E[\min\{\mathrm{Pois}(k),k\}]=k(1-e^{-k}k^k/k!)$ .
Lemma 13 (p. 29): if $P_{\mathrm{high}}\le k$ , then $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)\ge\big(s-s/\tau+\mathbb E[\min\{\mathrm{Pois}(sk),k\}]/(\tau k)\big)\mathrm{LP}_{\mathrm{sim}}(I)$ for every $s\in[0,1]$ .
The $\mathrm{ALG}^1$ bound (p. 30): on every $\tau$ -bounded instance, $R_{\mathrm{ALG}^1_{\mathrm{sim}}}(I)\ge(1-e^{-k}k^k/(k!\tau))\,\mathrm{LP}_{\mathrm{sim}}(I)$ .
Lemma 14 (p. 29): if $P_{\mathrm{high}}>k$ , deflating the acceptance probabilities to an instance with $P_{\mathrm{high}}=k$ does not increase the ratio $R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}/\mathrm{LP}_{\mathrm{sim}}$ (posed under the disclosed hypothesis $v_i\ne1$ ).

Significance

Theorem 3 makes value-ordered policies an $\alpha^\tau_k$ -approximation on $\tau$ -bounded instances, through Lemma 10. The factor tends to $1$ as $k\to\infty$ for fixed $\tau$ : at $s=1$ it is at least $1-e^{-k}k^k/(k!\tau)=1-O(1/\sqrt k)$ (Corollary 4). The paper's Theorem 4, the subject of the companion mission in this series, shows that no value-ordered policy beats the same expression with the supremum over $s\ge0$ , so the analysis is tight wherever the two suprema coincide. The interpretation of $\tau$ is how soft the capacity is: the bound degrades exactly as the overage cost dominates candidate values.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it has been machine-checked. A complete development would give the platform an overbooking-type stochastic selection model with an exact expected reward, an LP benchmark, and the truncated-Poisson constant that recurs in prophet-inequality and online-matching analyses (the $k$ -uniform correlation gap of Yan 2011). Proposition EC.2 and the monotonicity of $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ are reusable on their own.

Difficulty

The obvious argument compares the algorithm's random number of hires with the LP's expected number and loses everything to the overage term: the LP pays $[\mathbb E|A|-k]^+$ , the algorithm pays $\mathbb E[|A|-k]^+$ , and Jensen's inequality points the wrong way. The gap must be controlled by a sum of independent Bernoulli variables against a Poisson variable of the same mean, uniformly over how the mass is spread across candidates. A second difficulty is the regime $P_{\mathrm{high}}>k$ , where the LP optimum deliberately exceeds capacity; a direct bound there does not reduce to the first case, and the paper's reduction (Lemma 14) changes the instance rather than the algorithm. Tie cases $v_i=1$ make the LP optimum non-unique, which the formal statements must handle explicitly.

Formalization scope

Candidates are Fin n (0-based), all quantities are real. The sorted labelling $v_1\ge\dots\ge v_n$ is part of instance validity (Antitone I.v), as the paper assumes after relabelling; ties may be ordered arbitrarily. Every expectation is an explicit finite sum over the $2^n$ hire sets with independent probabilities $y'_ip_i$ ; there is no measure theory. The truncated Poisson mean is the series of the Poisson pmf. $\mathrm{LP}_{\mathrm{sim}}(I)$ is the supremum of the objective over the feasible set, which is the LP value; $\alpha^\tau_k$ is the supremum over $[0,1]$ . $s^*$ is any maximiser of the $\alpha^\tau_k$ objective over $[0,1]$ ; one exists by continuity. A candidate with $p_i=0$ receives $y'_i=0$ , which changes no reward.

The algorithm's reward is the exact expected reward of the run with independent offers, never the bound produced in the paper's proof, and the comparison is with the LP value at an optimal solution, not with the objective at an arbitrary feasible point; $\alpha^\tau_k$ is the supremum of the specific Poisson expression, not a free constant.

Two statements carry disclosed hypotheses, because the printed versions fail at ties: Lemma 12 assumes $v_i>0$ , $v_i\ne1$ , $p_i>0$ , and Lemma 14 assumes $v_i\ne1$ . Counterexamples are in the items' Formalization Notes. Theorem 3 and Lemma 13 need neither and hold for every optimal LP solution.

A complete development needs Poisson series manipulations (the closed form, concavity of $\lambda\mapsto\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]$ ), a Bernoulli-to-Poisson comparison for $\mathbb E\min\{\sum_iD_i,k\}$ , and fractional-knapsack structure for the LP. Contributions of alternative proofs of any milestone, and of the Poisson facts as standalone results, are welcome.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3 (2023); Operations Research (2024). https://arxiv.org/abs/2210.04059
Q. Yan, Mechanism Design via Correlation Gap, Proceedings of SODA 2011, 710–719. https://doi.org/10.1137/1.9781611973082.56
M. T. Goodrich, R. Tamassia, Algorithm Design: Foundations, Analysis, and Internet Examples, Wiley, 2001, Chapter 5 (fractional knapsack).

13 thms1 active userReviewed

Linear algebra Linear Optimization·Captain: mikedeng1

A Strongly Polynomial Algorithm for Linear Exchange Markets II: A Z₊-Matrix Polyhedron P_M Lies Between an M2VPI Polyhedron and Its Scaling by B²Research Paper

Motivation

In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.

No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a $Z_+$ -matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor $B^2$ . This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.

Setting

Matrices are rational. For integers $k, t \ge 0$ a matrix $M \in \mathbb{Q}^{k\times t}$ is a $Z_+$ -matrix, written $M \in \mathcal{Z}_+(k,t)$ , if every off-diagonal entry is nonpositive and every column sum is nonnegative:

M_{ij} \le 0 \quad (i \ne j), \qquad \sum_{i=1}^k M_{ij} \ge 0 \quad (j \in [t]).

For a non-square matrix the diagonal entries are the $M_{ii}$ with $1 \le i \le \min\{k,t\}$ . Square $Z_+$ -matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.

$\mathcal{M}_2(m,t)$ is the set of $m\times t$ rational matrices with at most one positive and at most one negative entry in every row. A system $\bar M x \le \bar b$ with $\bar M \in \mathcal{M}_2(m,t)$ is a monotone two-variable-per-inequality system (M2VPI).

For $M \in \mathcal{Z}_+(k,t)$ and $b \in \mathbb{Q}^k$ with $b > 0$ , the polyhedron of interest is

P_M = \{x \in \mathbb{R}^t : Mx \le b,\ x \ge 0\}.

Write $\ell$ for the number of nonzero entries of $M$ , $\alpha P = \{\alpha x : x \in P\}$ for $\alpha > 0$ , and

B = \frac{\sum_{j=1}^k b_j}{\min_{i\in[k]} b_i}.

In §7 the right-hand side is called $\gamma$ instead of $b$ , and $\lambda_i = \sum_{j\ne i}\gamma_j$ .

The proof works with a square $M \in \mathcal{Z}_+(t,t)$ with positive diagonal. Its digraph $([t],H)$ has an arc $ij$ whenever $M_{ij} < 0$ . $D_i$ is the set of vertices reachable from $i$ (including $i$ ), and $M^{(i)}$ is the submatrix of the rows $M_j$ , $j \in D_i$ . The vertices split into $T_1$ (at most one outgoing arc), $T_2$ (at least two arcs and $\operatorname{rk} M^{(i)} = |D_i|$ ) and $T_3$ (at least two arcs and $\operatorname{rk} M^{(i)} < |D_i|$ ).

Formalization targets

Goal: Theorem 6.4 (p. 15)

For $M \in \mathcal{Z}_+(k,t)$ with $k \ge 1$ and $\ell$ nonzero entries, and $b \in \mathbb{Q}^k$ with $b > 0$ , there are $\ell' \le \ell$ , $\bar M \in \mathcal{M}_2(\ell',t)$ and $\bar b \in \mathbb{Q}^{\ell'}$ with

P_M \subseteq \{x \in \mathbb{R}^t : \bar Mx \le \bar b,\ x \ge 0\} \subseteq B^2 P_M.

Milestones (§7, pp. 16–23)

Lemma 7.1: for $M \in \mathcal{Z}_+(t,t)$ and $\bar p \ge 0$ with $M\bar p \le \gamma$ , $\ M\bar p \ge -\lambda \ge -(B-1)\gamma$ .
Lemma 7.2: the Gaussian elimination of the proof, run on $T \in \mathcal{Z}_+(\ell,t)$ , returns $T' = YT$ with $Y \ge 0$ , $T'$ upper triangular with diagonal entries in $\{0,1\}$ and nonpositive off-diagonal entries, and $T'_{kk} = 1$ whenever some $T_{ik} < 0$ with $i > k$ .
Claim 7.3(iii): for $i \in T_3$ , $M_i$ is a linear combination of $\{M_h : h \in D_i \setminus\{i\}\}$ .
Lemma 7.4(i): for $i \in T_2\cup T_3$ there is a unique $q^{(i)} \in \mathbb{R}^t_+$ with $M_\ell q^{(i)} = 0$ ( $\ell \in D_i\setminus\{i\}$ ), $q^{(i)}_i = 1$ and $q^{(i)}_\ell = 0$ off $D_i$ .
Lemma 7.4(iv) and (iii): points $r^{(i)} \in P_M$ tight on $D_i\setminus\{i\}$ (for $i \in T_3$ ) and on $D_i$ with $r^{(i)}_i = \kappa(i)$ (for $i \in T_2$ ).
Claim 7.5: $\kappa(i)\,M_i q^{(i)} \le B\gamma_i$ for $i \in T_2$ .
The reduced case (§7, p. 16): Theorem 6.4 for square $M$ with positive diagonal.

Significance

Theorem 6.4 turns an LP over a $Z_+$ constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor $B^2$ . In the exchange-market algorithm $B \le n$ , so the starting prices of each phase come within a factor $n^2$ of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form $\max \sum_i x_i$ over $P_M$ with $M$ a $Z_+$ -matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on $Z_+$ -matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.

Difficulty

The obvious approach, deleting all but two variables from each inequality of $P_M$ , fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc $ij$ of $H$ , as a nonnegative combination of the inequalities $M\bar p \ge -\lambda$ . Finding it requires an ordering of $D_i$ in which every vertex but $i$ has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment $\{\bar M\bar p \le \bar b\} \subseteq B^2P_M$ is the hard direction. It splits by whether the rows on $D_i$ are linearly independent ( $T_2$ ) or not ( $T_3$ ), and the $T_2$ case needs the extra constraint $\bar p_i \le \kappa(i)$ and the comparison of entries of the elimination multipliers $Y^{(ij)}$ in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.

Formalization scope

Indices are 0-based (Fin k, Fin t); the paper's $[n] = \{1,\dots,n\}$ . Matrices $M$ , $\bar M$ and right-hand sides $b$ , $\bar b$ , $\gamma$ are rational (ℚ), as on p. 15, and act on real vectors $x \in \mathbb{R}^t$ through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. $B^2P_M$ is the image $\{B^2x : x \in P_M\}$ . $B$ is defined for $k \ge 1$ only, and every statement using it assumes $k \ge 1$ (resp. $t \ge 1$ ).

Not formalized: the running time $O(\ell(\min\{k,t\})^3)$ and the polynomial bound on the encoding size of $\bar M$ , $\bar b$ in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 ( $\gamma > 0$ ; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.

Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is $Y \ge 0$ " form would be nearly trivial, since $Y = 0$ satisfies all but one clause. In the goal, $\bar M$ must have at most one positive and at most one negative entry per row, and $\ell' \le \ell$ . Dropping either requirement makes the goal weaker than the paper's theorem.

$\kappa(i)$ , defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the $i$ -th entry of $(M_{D_i,D_i})^{-1}\gamma_{D_i}$ , a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for $i \in T_2$ , where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.

A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any $Z_+$ -matrix. Contributions are welcome on any milestone, on the reduction from rectangular $M$ to the square positive-diagonal case, and on the two containments of the reduced case.

Selected references

J. Garg and L. A. Végh, A strongly polynomial algorithm for linear exchange markets, arXiv:1809.06266v3, 2022; Operations Research, 2023. https://arxiv.org/abs/1809.06266
N. Megiddo, Towards a genuinely polynomial algorithm for linear programming, SIAM Journal on Computing 12(2), 1983. https://doi.org/10.1137/0212022
D. S. Hochbaum and J. Naor, Simple and fast algorithms for linear and integer programs with two variables per inequality, SIAM Journal on Computing 23(6), 1994. https://doi.org/10.1137/S0097539793251876
R. W. Cottle and A. F. Veinott, Jr., Polyhedral sets having a least element, Mathematical Programming 3, 1972. https://doi.org/10.1007/BF01584975

11 thms1 active userReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 2: An LP-Rounding Policy That Sends Offers in Parallel Lists Earns at Least (1 − 1/e) Times the LP BoundResearch Paper

Motivation

Firms that hire for several roles at once face a timing problem. An offer occupies a candidate until they answer, a candidate can hold only one offer, and the hiring season has a fixed number of decision rounds. Sending offers one at a time is slow; sending them all at once risks over-hiring. Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three stylised models of this pipeline: interviewing with a cap on interviews (ProbeTop- $k$ ), offering in parallel rounds, and offering all at once. This mission formalizes their result for the second model, the Parallel Offering problem.

The question belongs to the literature on stochastic probing and LP-based approximation of adaptive policies. The Sequential Offering model of Purohit, Gollapudi and Raghavan (2019) sends one offer per round for identical positions. Parallel Offering lets each unfilled position send one offer per round, with heterogeneous positions, and asks how much a simple, non-adaptive policy loses against the best adaptive one.

Setting

A firm fills $k$ positions from $n$ candidates within $T$ rounds. Candidate $i\in[n]$ accepts an offer for position $j\in[k]$ with probability $p_{ij}$ and then adds the value $v_{ij}$ . An instance is $I=(k,T,n,p,v)$ with

1\le k\le T\le n,\qquad p\in[0,1]^{n\times k},\qquad v\in\mathbb R_+^{n\times k}.

In each round the firm may send one offer for every unfilled position, and each candidate receives at most one offer in total. Before the rounds start, each candidate $i$ has decided the set $A_i\subseteq[k]$ of positions they would accept, with $\mathbb P(j\in A_i)=p_{ij}$ . These decisions may be correlated across the positions of one candidate and are independent across candidates.

The linear program $\mathrm{LP}_{\mathrm{par}}(I)$ has a variable $y_{ij}$ for the probability that candidate $i$ is offered position $j$ :

\max\ \sum_{j=1}^k\sum_{i=1}^n v_{ij}y_{ij}p_{ij}\quad\text{s.t.}\quad \sum_i y_{ij}\le T,\quad \sum_i y_{ij}p_{ij}\le 1\ \ (\forall j),\qquad \sum_j y_{ij}\le 1\ \ (\forall i),\qquad 0\le y_{ij}\le 1.

The paper shows (Lemma 6) that its value bounds the expected reward of every policy.

The dependent rounding of Gandhi, Khuller, Parthasarathy and Srinivasan (2006) takes a bipartite graph with edge weights $x_e\in[0,1]$ and outputs random indicators $X_e\in\{0,1\}$ with (P1) $\mathbb E X_e=x_e$ ; (P2) every vertex degree $\sum_{e\ni u}X_e$ is the floor or the ceiling of its fractional degree, with probability 1; (P3) for every vertex $u$ , every set $S$ of edges at $u$ and every $c\in\{0,1\}$ , $\mathbb P(\bigcap_{e\in S}\{X_e=c\})\le\prod_{e\in S}\mathbb P(X_e=c)$ .

The algorithm $\mathrm{ALG}_{\mathrm{par}}$ solves $\mathrm{LP}_{\mathrm{par}}(I)$ to optimality, rounds the optimal $y$ on the complete bipartite graph candidates $\times$ positions, and puts candidate $i$ on the list of position $j$ iff $Y_{ij}=1$ . Every list is then run in parallel, in decreasing order of $v_{ij}$ : position $j$ offers to the next candidate on its list each round until someone accepts, the list ends or the $T$ rounds are over. $R_{\mathrm{ALG}_{\mathrm{par}}}(I)$ is its expected total value.

For the analysis, $D_j=\{i: Y_{ij}=1,\ j\in A_i\}$ is the set of candidates on list $j$ who would accept, $v^*_j(S)=\max_{i\in S}v_{ij}$ (zero on the empty set), $\tilde D_j$ is the same set built from independent Bernoulli( $y_{ij}$ ) variables instead of $Y_{ij}$ , and $L^*_j=\sum_i v_{ij}y_{ij}p_{ij}$ .

Formalization targets

Goal: Theorem 2

R_{\mathrm{ALG}_{\mathrm{par}}}(I)\ \ge\ \Big(1-\frac1e\Big)\,\mathrm{LP}_{\mathrm{par}}(I)\qquad\text{for every } I\in\mathcal I_{\mathrm{par}}.

The constant is tight (App. C.5 of the paper), so the goal states the paper's result in its final form.

Milestones

Properties (a) and (b) (§5.2): with probability 1 every list has at most $T$ candidates and every candidate is on at most one list.
$L_j=\mathbb E\,v^*_j(D)$ (§5.3): the expected value hired for position $j$ is the expected best value among the accepting list members.
Lemma 7: $\mathbb E\,v^*_j(D)\ge\mathbb E\,v^*_j(\tilde D)$ for every position $j$ .
Lemma 8: $\mathbb E\,v^*_j(\tilde D)\ge(1-1/e)L^*_j$ for every position $j$ .
Lemma 9 (companion, §5.4): if all positions are identical, $\mathrm{LP}_{\mathrm{par}}(I)=\mathrm{LP}_{\mathrm{seq}}(I')$ , where $I'$ is the Sequential Offering instance with the same candidates and a budget of $kT$ offers.

Significance

Theorem 2 shows that a non-adaptive policy, fixed before any offer is answered, earns at least $1-1/e\approx0.632$ of the LP bound, hence of the best adaptive policy, for heterogeneous positions and with acceptance decisions correlated across positions. Through Lemma 9 it also bounds the cost of batching: $T$ parallel rounds lose at most a factor $1-1/e$ against $kT$ sequential offers (Corollary 3 of the paper).

The results are proved in the paper; none of them is formalized. The mission adds to the platform a reusable statement of the GKPS rounding properties on bipartite graphs, an explicit finite model of a parallel offering process computed from its run, and a $(1-1/e)$ LP-rounding guarantee that a solver must connect end to end: the algorithm's reward, the per-position reduction, the comparison with independent rounding, and the bound for independent rounding.

Difficulty

The obvious first step, replacing the dependent rounding by independent rounding with the same marginals, is not free: the rounding couples the candidates of a list, and an expected maximum is not linear in the indicators. Only the negative correlation of the rounding at a single position rescues it, and the paper notes (App. C.3) that (P1) and (P3) alone do not suffice once several identical positions are pooled, so the argument is genuinely per position. The written proof of Lemma 7 (p. ec10) has a sign error and a wrong indicator; the statement is correct. Independent rounding then still has to be compared with the LP: the LP only controls each list in expectation, through $\sum_i y_{ij}p_{ij}\le1$ , while the algorithm collects at most one value per list.

Formalization scope

Candidates are Fin n, positions Fin k, all quantities real. All randomness is finite: an expectation is an explicit sum over the rounded edge set $Y\subseteq[n]\times[k]$ , weighted by a distribution $\mu$ , and over acceptance profiles $(A_i)_i$ , weighted by $\prod_i\mathrm{acc}_i(A_i)$ , where $\mathrm{acc}_i$ is any law on subsets of $[k]$ with marginals $p_{ij}$ . The rounding is independent of the acceptance decisions.

The rounding scheme is represented by its properties: the goal holds for every distribution $\mu$ with (P1)–(P3) for the weights $y$ , which includes the scheme of Gandhi et al. The LP solution is any optimal one. The order of list $j$ is a permutation of the candidates that is decreasing in $v_{ij}$ , ties in any order. $R_{\mathrm{ALG}_{\mathrm{par}}}$ is computed from the run: candidate $i$ is hired for $j$ iff $i$ is on list $j$ , would accept $j$ , nobody earlier on list $j$ would accept $j$ , and fewer than $T$ candidates precede $i$ on the list. It is not defined by the formula $\mathbb E\,v^*_j(D)$ , which is a milestone, and the goal is compared with the objective at an optimal LP solution, never at an arbitrary feasible point. The degree condition (P2) is kept in the rounding predicate, not replaced by the list properties it implies.

A complete development needs finite sums over product distributions, expected maxima of random subsets of sorted values, and elementary estimates involving $e^{-1}$ ; no measure theory is required. The GKPS definition is generic in the two vertex sets and reusable for other dependent-rounding results. Proofs of any milestone are welcome, as is a proof of Lemma 7 for general negatively correlated roundings.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, Operations Research, 2024; preprint arXiv:2210.04059v3, 2023. https://arxiv.org/abs/2210.04059
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3), 2006. https://doi.org/10.1145/1147954.1147956
M. Purohit, S. Gollapudi, M. Raghavan, Hiring under uncertainty, ICML 2019. https://proceedings.mlr.press/v97/purohit19a.html

8 thms1 active userReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 1: A Non-Adaptive, Committed LP-Rounding Policy for ProbeTop-k Earns at Least (1 − e^{−k}k^k/k!) Times the LP BoundResearch Paper

Motivation

Hiring is a pipeline: a firm with $k$ openings and a large pool of applicants cannot interview everyone, so it must decide whom to interview, in what order, and whether to hire on the spot. The ProbeTop-k problem models this. Each applicant has a random value with a known distribution, an interview reveals the value, at most $T$ interviews may be conducted, and at most $k$ applicants are hired. The firm maximises the expected total value of its hires.

The same structure appears in stochastic probing, sequential testing and assortment problems, and its benchmark, the best adaptive, non-committed policy (one that may choose the next interview after seeing earlier values and may hire only at the end), is hard to compute. Practical policies are non-adaptive (fix the interview order in advance) and committed (hire or reject right after each interview). Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) ask how much is lost by restricting to such policies, and answer with an LP-rounding algorithm whose guarantee improves with $k$ .

Setting

An instance $I = (k, T, n, F)$ has $1 \le k \le T \le n$ . Applicant $i \in [n]$ has value $V_i$ supported on finitely many non-negative values $r_1, \dots, r_J$ , with $q_{ij} = \Pr(V_i = r_j)$ ; values are independent across applicants.

The linear relaxation $\mathrm{LP}_{ptk}(I)$ has variables $y_i$ (probability of interviewing $i$ ) and $x_{ij}$ (probability of hiring $i$ when $V_i = r_j$ ):

\mathrm{LP}_{ptk}(I) = \max \sum_{i=1}^n \sum_{j=1}^J r_j x_{ij} \quad \text{s.t.}\quad x_{ij} \le y_i q_{ij},\ \ \sum_i y_i \le T,\ \ \sum_{i,j} x_{ij} \le k,\ \ x_{ij} \ge 0,\ \ 0 \le y_i \le 1 .

From a solution $(x, y)$ define

p_i = \frac{\sum_j x_{ij}}{y_i}, \qquad v_i = \frac{\sum_j r_j x_{ij}}{\sum_j x_{ij}},

each $0$ when its denominator is $0$ .

The algorithm ALGptk solves the LP and takes a basic optimal solution $(x, y)$ . It then draws the interview set $S$ by the dependent rounding DR: applicants with $y_i = 1$ are always in $S$ ; a single fractional $y_a$ puts $a$ in $S$ with probability $y_a$ ; two fractional $y_a + y_b = 1$ put exactly one of them in $S$ , $a$ with probability $y_a$ . ALGptk interviews $S$ in decreasing order of $v_i$ , and on observing $V_i = r_j$ hires $i$ with probability $x_{ij}/(y_i q_{ij})$ if a position is still open. Its expected reward is $R_{ALG_{ptk}}(I)$ .

Formalization targets

Goal: Theorem 1

R_{ALG_{ptk}}(I) \;\ge\; \Big(1 - \frac{e^{-k}k^k}{k!}\Big)\, \mathrm{LP}_{ptk}(I) \qquad \text{for every valid instance } I \text{ with } k \text{ positions.}

The factor is $1 - 1/e$ at $k = 1$ and tends to $1$ as $k \to \infty$ .

Milestones

The paper's own steps, in attack order:

Lemma 2 (p. 16): a basic feasible solution has at most two fractional $y_i$ , and two fractional ones sum to $1$ .
(P1), (P2) (p. 17): DR has marginals $\mathbb{E}(Y_i) = y_i$ and never exceeds $T$ interviews.
$\mathbb{E}(P_i) = p_i$ (p. 18): the hiring coin has mean $p_i$ .
Lemma 3 (p. 18): $R_{ALG_{ptk}}(I) = \sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$ , where $Z_i = Y_i P_i$ , the $P_i$ are independent Bernoulli( $p_i$ ) indicators, and $N_{i-1}$ counts the earlier applicants with $Z_\ell = 1$ .
Lemma 4 (p. 18): with two fractional components, this quantity under DR is at least its value under independent rounding of $y$ .
LP identity (p. ec8): $\sum_{i,j} r_j x_{ij} = \sum_i y_i v_i p_i$ .
Proposition EC.1 (Yan 2011; p. ec2): the weighted rank function of a $k$ -uniform matroid has correlation gap at most $(1 - e^{-k}k^k/k!)^{-1}$ .
Independent version (p. ec8): with independent rounding, the reward is at least $(1 - e^{-k}k^k/k!)\,\mathrm{LP}_{ptk}(I)$ .

A companion milestone, Lemma 5 (p. 21), states that for weighted Bernoulli instances the LP has an optimal solution with $x_i = y_i q_i$ . It does not feed Theorem 1.

Significance

Theorem 1, combined with the fact that $\mathrm{LP}_{ptk}$ bounds every adaptive, non-committed policy (Lemma 1 of the paper), shows that a policy that is both non-adaptive and committed earns at least a fraction $1 - e^{-k}k^k/k!$ of the optimal adaptive, non-committed reward; the lost fraction $e^{-k}k^k/k!$ vanishes as $k$ grows. The factor is tight for this LP (App. B.6). The theorem also underlies a PTAS for ProbeTop-k (Corollary 1) and, through Lemma 5, the same guarantee for the Sequential Offering problem of Purohit et al. (Corollary 2).

The result is proved in the paper; to our knowledge nothing in it is machine-checked. A formalization would add to the platform:

an LP relaxation with basic feasible solutions as extreme points of a polytope;
an explicit model of a randomised, committed selection algorithm as a finite expectation;
the correlation gap of $k$ -uniform weighted rank functions, a tool that recurs across prophet inequalities, posted pricing and stochastic probing.

Proposition EC.1 is a cited result (Yan 2011), not proved in the paper. Formalizing it is part of the work.

Difficulty

The obvious argument compares the algorithm with the LP term by term, $\Pr(i \text{ hired}) \ge c\, y_i p_i$ for each $i$ . This fails because hiring is capped at $k$ : applicants late in the order are hired only if few earlier ones were. The guarantee must be obtained in aggregate, which is what the correlation gap does.

Two steps carry the weight:

Proposition EC.1 is a genuine extremal inequality over all distributions on subsets with given marginals.
Lemma 4 must show that the negative correlation DR introduces between the two fractional applicants never hurts a committed, order-dependent selection. It is a case analysis over sample paths that uses the decreasing order of $v_i$ .

Lemma 3 is a conditional-expectation identity, but in a fully explicit model it requires marginalising out the values and coins of all other applicants.

Formalization scope

Lean namespace HiringLP.ProbeTopK.

Representation.

Applicants are Fin n and support points Fin J. All quantities are real.
Instances are valid when $1 \le k \le T \le n$ , $r_j \ge 0$ , $q_{ij} \ge 0$ and $\sum_j q_{ij} = 1$ .
Basic feasible solutions are Set.extremePoints ℝ of the feasible set in $(x, y)$ -space. An optimal solution is feasible and objective-maximal among feasible points, and $\mathrm{LP}_{ptk}(I)$ is the objective at it.

Conventions.

$p_i$ , $v_i$ and the hiring probability $x_{ij}/(y_i q_{ij})$ are $0$ when their denominators vanish (the paper's footnote 2).
The interview order is a permutation required to be non-increasing in $v_i$ , with ties in any order.
DR is an explicit formula for the probability of each interview set.

The expected reward. $R_{ALG_{ptk}}(I)$ is a finite sum over the interview set, the value vector (independent, law $q$ ) and the vector of hiring coins (independent given the values). Applicant $i$ is hired exactly when it is interviewed, its coin succeeds, and fewer than $k$ earlier interviewed applicants had successful coins. The reward collects the realised values $r_{V_i}$ .

Ruled out.

Defining the reward as $\sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$ . That is Lemma 3, which would make the goal a statement about its own proof.
Comparing with the objective at an arbitrary feasible point instead of an optimal one.

Infrastructure and contributions. The weighted rank function, independent rounding and marginals are separate, reusable definitions. Contributions are welcome on each milestone, especially Proposition EC.1. So is general infrastructure: extreme points of polytopes as basic solutions, and finite product distributions.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, Operations Research, 2024; preprint arXiv:2210.04059v3, 2023. https://arxiv.org/abs/2210.04059
Q. Yan, Mechanism design via correlation gap, Proceedings of the 22nd ACM-SIAM Symposium on Discrete Algorithms (SODA), 710–719, 2011. Proceedings volume: https://doi.org/10.1137/1.9781611973082
S. Agrawal, Y. Ding, A. Saberi, Y. Ye, Correlation robust stochastic optimization, Proceedings of the 21st ACM-SIAM Symposium on Discrete Algorithms (SODA), 1087–1096, 2010. Proceedings volume: https://doi.org/10.1137/1.9781611973075
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
M. Purohit, S. Gollapudi, M. Raghavan, Hiring under uncertainty, Proceedings of the 36th International Conference on Machine Learning (PMLR 97), 5181–5189, 2019. https://proceedings.mlr.press/v97/purohit19a.html

13 thms1 active userReviewed

Quantum Information·Captain: mikedeng1

A Grand Unification of Quantum Algorithms: Phase Estimation by QSVT Errs by Less Than 2^{−n}, and Meets the Δ-Region Only at Iteration n − 1, When Δ < 2(cos(3π/16) − 1/√2)Research Paper

Motivation

Phase estimation asks: given access to a unitary $U$ and an eigenvector $|u\rangle$ with $U|u\rangle = e^{2\pi i\varphi}|u\rangle$ , determine $\varphi \in [0,1)$ . It is the subroutine behind Shor's factoring algorithm, quantum chemistry energy estimation, and amplitude estimation, and is one of the standard sources of quantum speed-up.

Martyn, Rossi, Tan and Chuang, A Grand Unification of Quantum Algorithms (PRX Quantum 2, 040203, 2021), present search, phase estimation and Hamiltonian simulation as instances of one primitive, the quantum singular value transformation (QSVT) of Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019). Most of the paper's numbered results restate QSVT theory from earlier work. Its own proved content is Appendix B: the analysis of phase estimation by QSVT (Section V, Algorithm 3), a bit-by-bit binary search in the spirit of Kitaev's iterative phase estimation, where each bit is read by applying a sign function to a singular value. A closely related QSVT phase-estimation algorithm was found independently by Rall (arXiv:2103.09717).

This mission formalizes that analysis: the exact-arithmetic correctness of the bit search (Theorems 6 and 7), and its robustness when the sign function is only approximated (Theorem 8).

Setting

Fix a unitary $U$ , an eigenvector $|u\rangle$ , and the phase $0 \le \varphi < 1$ . Write $0.\varphi_{[j+1:]} = 0.\varphi_{j+1}\varphi_{j+2}\ldots$ for the fractional part of $2^j\varphi$ .

For $j \in \mathbb N$ and $\theta \in \mathbb R$ , the matrix $A_j(\theta) = \tfrac12(I + e^{-2\pi i\theta}U^{2^j})$ acts on $|u\rangle$ with singular value

\sigma^j(\theta) = \bigl|\cos\bigl(\pi(2^j\varphi - \theta)\bigr)\bigr| = \bigl|\cos\bigl(\pi(0.\varphi_{[j+1:]} - \theta)\bigr)\bigr|. \tag{64–65}

The procedure keeps a binary fraction $\theta$ , initially $0$ , and runs iterations $j = n-1, n-2, \ldots, 0$ for a positive integer $n$ . Iteration $j$ halves $\theta$ , evaluates the sign function $\Theta(1/\sqrt2 - x)$ at $x = \sigma^j(\theta)$ through QSVT, measures one ancilla bit $b_j$ , and sets the first binary digit of $\theta$ to $b_j$ :

\theta_j = \tfrac12\theta_{j+1} + \tfrac12 b_j, \qquad \theta_n = 0.

An additional $j = 0$ iteration then sets the units digit $b_0'$ , and the output is $\theta = b_0' + \theta_0$ .

The ideal measurement returns $b = 1$ when $\sigma < 1/\sqrt2$ and $b = 0$ when $\sigma > 1/\sqrt2$ . In practice the sign function is replaced by a polynomial that is reliable only outside the Δ-region $\bigl[\tfrac1{\sqrt2} - \tfrac\Delta2, \tfrac1{\sqrt2} + \tfrac\Delta2\bigr]$ ; inside it either bit may be returned.

Formalization targets

Goal: Theorem 8 (p. 17)

If

0 \le \Delta < 2\Bigl(\cos\frac{3\pi}{16} - \frac1{\sqrt2}\Bigr) \approx 0.25,

then in every run of the procedure, the singular value $\sigma^j$ can fall in the Δ-region only at the first iteration $j = n-1$ , and the output satisfies

|\theta - \varphi| < 2^{-n}.

Milestones

(64)–(65), p. 15: the singular value and singular vectors of $A_j(\theta)$ on $|u\rangle$ .
Lemma 11 and Theorem 6 (pp. 27, 16): for an $n$ -bit $\varphi$ and the exact sign function, $\theta_j = 0.\varphi_{[j+1:]}$ , so the loop ends with $\theta = \varphi$ .
Lemma 12 and Theorem 7 (pp. 28, 16): otherwise $\theta_j$ is an $(n-j)$ -digit rounding of $0.\varphi_{[j+1:]}$ up to a carry, with error $\le 2^{j-n-1}$ , and the output satisfies $|\theta - \varphi| \le 2^{-n-1}$ .
(B14), p. 30: membership of $|\cos(\pi x)|$ in the Δ-region in terms of two arccos intervals for $\pi|x|$ .
(B15), (B16) ⟺ (B21), pp. 30–31: the arccos condition is equivalent to the explicit threshold on $\Delta$ .
Lemma 13, p. 30, and its base step (B17)–(B20), pp. 30–31: the Δ-region can only be met at iteration $n-1$ , and an error there does not propagate.

A companion item states (68): the $2N \times 2N$ matrix $W_j(\theta)$ of Figure 10 is unitary and block-encodes $A_j(\theta)$ .

Significance

Theorem 8 is what makes phase estimation by QSVT implementable: a sign function cannot be realized exactly by a polynomial, and the theorem shows that a polynomial approximation which fails on a band of width about $0.25$ around $1/\sqrt2$ costs at most one bit of accuracy, and only at one iteration. Combined with the per-iteration failure probability analysis (71)–(72), it yields the paper's claim that $O(n\log(n/\delta))$ queries give an $n$ -bit estimate with probability $1-\delta$ .

On the formal side, the paper proves these results in Appendix B by case analysis on binary digits with carries. No machine-checked version of the analysis exists on the platform, and no QSVT-based phase-estimation result has been formalized elsewhere to the curators' knowledge. The mission separates the deterministic correctness of the bit search from the quantum machinery, so the combinatorial core can be checked independently of QSVT itself.

Difficulty

The obvious argument tracks the digits of $\varphi$ one at a time, and it works for an $n$ -bit phase. It fails when $\varphi$ has more than $n$ digits: the sign function rounds rather than truncates, so a bit can be set to $1$ when the true digit is $0$ , carries propagate, and the invariant must be a rounding statement with a carry bit $\tilde r_j$ (Lemma 12's nine-case induction). The final bit can carry into the units place, which is why the additional $j = 0$ iteration exists.

For Theorem 8, the natural first idea, that a bit error makes all later bits unreliable, is false; the content is that after an error at $j = n-1$ the distance $|0.\varphi_{[j+1:]} - \theta|$ stays a fixed amount away from the Δ-region at every later iteration. Turning this into the threshold requires precise bounds on $\arccos$ near $1/\sqrt2$ .

Formalization scope

Everything is stated in Lean 4 with Mathlib, over $\mathbb R$ , in the namespace QSVTPhaseEst.BitSearch. The conventions:

$0 \le \varphi < 1$ , $n \ge 1$ , $\Delta \ge 0$ in every item; bits are Bool; $0.\varphi_{[j+1:]}$ is Int.fract (2^j * φ).
" $\varphi$ is an $n$ -bit number" ( $n \ge m$ ) is $\varphi = k/2^n$ for some $k \in \mathbb N$ ; " $n < m$ , including $m = \infty$ " is its negation.
The outcome rule is the only place the measurement enters: below the Δ-region the bit is $1$ , above it the bit is $0$ , inside it (including ties at $\Delta = 0$ ) either bit may occur. Every theorem quantifies over all bit sequences satisfying this rule. The exact sign function of Theorems 6 and 7 is the rule with $\Delta = 0$ .
The additional $j = 0$ iteration is encoded as Appendix B 1 b (p. 29) analyses it: the general step applied to $0.\varphi_0\varphi_1\ldots = \varphi/2$ with $\theta$ halved, singular value $|\cos(\pi(\varphi - \theta_0)/2)|$ . The literal reading of Algorithm 3, line 9 makes Theorem 7 false on the paper's own example $\varphi = 0.1110101_2$ , $n = 2$ .
Theorem 8's bound is stated for every run, as Algorithm 3's Output claims; runs with an error at iteration $n-1$ are the printed case, runs without one are covered by Theorems 6 and 7. Its first part also covers the additional iteration.
(B14) assumes $\Delta \le 2 - \sqrt2$ and $|x| \le 1$ , which keep the arccos arguments in $[-1,1]$ .

A formalization in which the outcome rule mentions $\varphi$ , its digits or its rounding, in which $\sigma^j$ is written through the digits of $\varphi$ , or in which the output is defined as a rounding of $\varphi$ , would make the theorems circular; none of these is used.

Not formalized: QSP and QSVT themselves (Theorems 1–4, 9, 10; Theorem 1 is already an open goal on the platform), the polynomial $P^{\mathrm{PE}}_{\epsilon,\Delta}$ of (69), the $\epsilon$ -error probability analysis (71)–(72), and the runtime. Contributions of reusable lemmas on binary roundings (Int.fract of $2^j\varphi$ , nearest dyadic rounding with carry) and on $\arccos$ near $1/\sqrt2$ are welcome.

Selected references

J. M. Martyn, Z. M. Rossi, A. K. Tan, I. L. Chuang, A Grand Unification of Quantum Algorithms, PRX Quantum 2, 040203, 2021. https://arxiv.org/abs/2105.02859 (v5 is the version formalized)
A. Gilyén, Y. Su, G. H. Low, N. Wiebe, Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics, STOC 2019. https://arxiv.org/abs/1806.01838
P. Rall, Faster coherent quantum algorithms for phase, energy, and amplitude estimation, Quantum 5, 566, 2021. https://arxiv.org/abs/2103.09717
A. Yu. Kitaev, Quantum measurements and the Abelian Stabilizer Problem, 1995. https://arxiv.org/abs/quant-ph/9511026

11 thms1 active userReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes III: Bipartite, Unit-Patience Side: Rounding Then Probing by Weight Earns ≥ (1 − 1/e)·Σ w_e p_e y_eResearch Paper

Motivation

Stochastic matching with patience models kidney exchange, online dating and labour platforms: every edge of a graph is present only with some probability, the only way to learn whether it is present is to probe it, and a probed edge that turns out to be present must be added to the matching. Each vertex $v$ also has a patience $t_v$ , a limit on how many of its edges may be probed. The goal is a probing strategy whose expected matched weight is a large fraction of what the best adaptive strategy obtains. Since the best strategy is hard to compute, algorithms are compared with the value of a linear program (LP (3) below), which upper-bounds every probing strategy (Bansal, Gupta, Li, Mestre, Nagarajan, Rudra, Algorithmica 2012).

Bansal et al. gave a $1/3$ -approximation for stochastic bipartite matching. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892v3) single out the case in which one side of the bipartition has unit patience, $t_u=1$ for every $u\in V_1$ . This case contains "Problem A" of Hikima et al. (AAAI 2021), whose approximation ratio transfers to their integrated two-stage problem ISPCB; Hikima et al. obtained $1/3$ from the bound of Bansal et al. For the special case in which one side has arbitrary patience and the other unlimited patience, Borodin and MacRury had already obtained the same $(1-1/e)$ guarantee through an online problem.

Setting

Let $G=(V_1\cup V_2,E)$ be a finite bipartite graph; $\delta(x)$ denotes the set of edges at a vertex $x$ . Each edge $e$ has a weight $w_e\ge 0$ and an activation probability $p_e\in[0,1]$ , independently across edges. Every $u\in V_1$ has patience $1$ ; every $v\in V_2$ has a patience $t_v\in\mathbb N\cup\{\infty\}$ .

LP (3). A vector $(y_e)_{e\in E}$ is feasible when $0\le y_e\le 1$ and, for every vertex $x$ ,

\sum_{e\in\delta(x)}y_ep_e\le 1,\qquad \sum_{e\in\delta(x)}y_e\le t_x .

Write $z_e=y_ep_e$ and $\mathsf{OPT}(v)=\sum_{e\in\delta(v)}w_ez_e$ .

The algorithm. A dependent rounding (Gandhi, Khuller, Parthasarathy, Srinivasan, J. ACM 2006) turns $y$ into a random set $\hat E=\{e:Y_e=1\}$ of rounded edges with $\Pr[Y_e=1]=y_e$ , at most one rounded edge at each $u\in V_1$ , at most $t_v$ at each $v\in V_2$ , and the negative correlation property (2): for $v\in V_2$ , $S\subseteq\delta(v)$ and $b\in\{0,1\}$ ,

\Pr\Big[\bigcap_{e\in S}(Y_e=b)\Big]\le\prod_{e\in S}\Pr[Y_e=b].

In the rounded graph every $v\in V_2$ is the centre of a star. Each $v$ probes its rounded edges in decreasing order of weight and is matched to the first active one; $W(v)$ is the weight of that edge ( $0$ if none), and $\mathbb E[\mathsf{ALG}]=\mathbb E[\sum_{v\in V_2}W(v)]$ .

Formalization targets

Goal: Theorem 2 (p. 18)

For every feasible $y$ , every rounding with the properties above and every decreasing-weight probing order,

\mathbb E[\mathsf{ALG}]\ \ge\ \Big(1-\frac1e\Big)\sum_{v\in V_2}\sum_{e\in\delta(v)}w_ep_ey_e .

Milestones

The proof of Lemma 7 (p. 17) expresses $W(v)$ as $\mathbb E[\sum_i w_iY_iP_i\prod_{j<i}(1-Y_jP_j)]$ and bounds $\mathbb E[\prod_{j\le i}(1-Y_jP_j)]\le\prod_{j\le i}(1-y_jp_j)$ using (2).
Lemma 7 (p. 16): $\mathbb E[W(v)]\ge\sum_{i=1}^k w_iz_i\prod_{j=1}^{i-1}(1-z_j)$ for the edges of $\delta(v)$ labelled by decreasing weight.
Eq. (29) (p. 18): the bound $F(i)\ge1-e^{-F^*(i)}\ge(1-1/e)F^*(i)$ . The summation-by-parts identity (27) on the same page is included as a supporting lemma.
Lemma 8 (p. 17): $\sum_i w_iz_i\prod_{j<i}(1-z_j)\ge(1-1/e)\sum_iw_iz_i$ when $z_i\in[0,1]$ , $\sum_iz_i\le1$ and $w_1\ge\cdots\ge w_k\ge0$ .
Lemma 9 (p. 18): $\mathbb E[W(v)]\ge(1-1/e)\,\mathsf{OPT}(v)$ for every $v\in V_2$ .

The paper's proofs are in §4, pp. 16–19.

Significance

Combined with the LP upper bound (Lemma 1 of the paper, from Bansal et al.), Theorem 2 is a $(1-1/e)$ -approximation for stochastic matching on bipartite graphs with a unit-patience side, improving and generalizing the $1/3$ guarantee of Hikima et al. for Problem A and, through their reduction, for ISPCB. By the paper's account (§1.1, p. 4), the guarantee rests on a new ingredient, a $(1-1/e)$ -balanced ordered contention resolution scheme for rank-1 matroids under negative correlation, in which the algorithm chooses the order: the per-star bound of Lemmas 7 and 9 holds for every rounding satisfying (2), not only for independent activations.

The result is proved in the paper; none of it has been machine-checked. This mission formalizes the per-star analysis and the theorem for an abstract rounding described by its properties, which is reusable for any algorithm that probes stars after a negatively correlated rounding.

Difficulty

If the rounded indicators $Y_e$ at a vertex were independent, Lemma 7 would be an equality and the remaining work would be the deterministic inequality of Lemma 8. They are not: the rounding is dependent, and Example 1 (p. 19) shows that this dependence can raise the probability that a particular edge is blocked to $1/2$ , so that no correlation-agnostic contention resolution scheme is better than $1/2$ -balanced. A per-edge guarantee, of the kind a contention resolution scheme that ignores correlation provides, is therefore unavailable: the bound of Theorem 2 holds only for the total weight collected at each $v$ , and the negative correlation property (2) is one-sided, so it can be used only in the direction in which it holds.

Formalization scope

All randomness is finite. The rounding is a probability vector $\mu$ on subsets of $E$ ; the activeness pattern $P:E\to\{0,1\}$ is independent with product weights. Every expectation is an explicit finite sum.
The rounding of Gandhi et al. is represented by its properties: $\mu\ge0$ , $\sum\mu=1$ , the marginals $\Pr[Y_e=1]=y_e$ , at most one rounded edge at each $u\in V_1$ , at most $t_v$ at each $v\in V_2$ , and (2) on the rounded indicators for every $v\in V_2$ , $S\subseteq\delta(v)$ , $b\in\{0,1\}$ . The goal holds for every such $\mu$ , so it covers the paper's rounding; formalizing the rounding procedure itself is a separate project.
$W(v)$ is defined from the run (the first active edge in $v$ 's probe list), not by the formula of Lemma 7; the identity between the two is a milestone.
Standing assumptions, disclosed: $w_e\ge0$ (with a negative weight the bound fails), $p_e\in[0,1]$ , patience $\infty$ is allowed on $V_2$ , and parallel edges are allowed. The goal is stated for every feasible $y$ , a stronger statement than the paper's "optimal" $y$ , since the proof never uses optimality. The phrase "yielding a $(1-1/e)$ -approximation" is not formalized: it needs Lemma 1 of Bansal et al.
Ruled out: defining $W(v)$ as $\sum_iw_iY_iP_i\prod_{j<i}(1-Y_jP_j)$ , as the best active edge regardless of the rounding, or stating the goal for one specific (independent) rounding or "for some rounding" would each be a different, weaker theorem.
Useful infrastructure: finite expectations over product measures, a negative-correlation inequality for products, Abel summation (Finset.sum_range_by_parts), and $1-x\le e^{-x}$ . Proofs of any milestone, and of the theorem from the milestones, are welcome.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025. arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012. https://doi.org/10.1007/s00453-011-9511-8
Y. Hikima, Y. Akagi, H. Kim, M. Kohjima, T. Kurashima, H. Toda, Integrated optimization of bipartite matching and its stochastic behavior: new formulation and approximation algorithm via min-cost flow optimization, The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI 2021) (reference [28] of the paper; no link).
A. Borodin, C. MacRury, Online bipartite matching in the probe-commit model, Mathematical Programming, 2025, pp. 1–54 (reference [9] of the paper; no link).

10 thms1 active userReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes I: With Patience at Least 2, Attenuated Random-Order Probing Gives Every Edge a(e)·Pr[e Is Free] ≥ β*Research Paper

Motivation

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).

2012: Bansal et al., a $0.25$ -approximation.
2015: Adamczyk, Grandoni and Mukherjee, $0.269$ .
2018: Baveja, Chavan, Nikiforov, Srinivasan and Xu, $0.31$ .
2021–2026: Brubach, Grammel, Ma, MacRury and Srinivasan (arXiv:2106.06892v3; Mathematics of Operations Research, 2025), $0.382$ when every patience is at least $2$ . Their algorithm processes the edges in random order and attenuates each probe with an extra coin flip. Version 3 restricts the result to patience at least $2$ ; earlier versions claimed it for all patience values, and Remark 1 shows why patience $1$ fails.
Since then Pollner et al. have obtained $0.395$ for general graphs (reference [35] of the paper).

This mission formalizes the per-edge bound behind the $0.382$ result, Theorem 1 of the paper.

Setting

A finite graph $G = (V, E)$ is given. Each edge $e$ is active independently with probability $p_e \in [0,1]$ , and each vertex $v$ has a patience $t_v \in \{1, 2, \dots\} \cup \{\infty\}$ , the largest number of probes that may be made to edges incident to $v$ . Write $\delta(v)$ for the edges incident to $v$ .

LP (3). A vector $(y_e)_{e \in E}$ is feasible if

0 \le y_e \le 1, \qquad \sum_{e \in \delta(v)} y_e p_e \le 1, \qquad \sum_{e \in \delta(v)} y_e \le t_v \quad (e \in E,\ v \in V).

Here $y_e$ is the probability of probing $e$ .

Attenuation. An attenuation function $\tilde a : [0,1] \to [0,1]$ assigns to edge $e$ the probability $a(e) = \tilde a(p_e y_e)$ . It is effective (Definition 3) if $\tilde a(0) = 1$ and $z \mapsto \ln(1 - x z \tilde a(z))$ is convex on $[0,1]$ for every $x \in (0,1)$ . The two functions used here are $\tilde a_{\exp}(z) = e^{-z/2}$ and $\tilde a_{\mathrm{lin}}(z) = 1 - z/2$ (Definition 4 with $\alpha = 1/2$ ).

Algorithm 1. Draw independent coins $Y_e \sim \mathrm{Bernoulli}(y_e)$ and $A_e \sim \mathrm{Bernoulli}(a(e))$ for every edge, and process the edges in a uniformly random order. When $e$ is processed it is free if both endpoints are unmatched and have made fewer than their patience in probes. If $e$ is free and $Y_e = A_e = 1$ , probe $e$ ; if it is active (coin $P_e \sim \mathrm{Bernoulli}(p_e)$ ), match it and both endpoints. Finally

\beta^* = \int_0^1 \bigl(e^{-2x} + x e^{-2x}\bigr)^2\,dx \approx 0.38278.

Formalization targets

Goal: Theorem 1 (p. 9)

If every vertex has patience at least $2$ , $y$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\mathrm{lin}}$ , then for every edge $e$

a(e) \cdot \Pr[e \text{ is free}] \;\ge\; \beta^*.

The probability is over the random order and the coins of Algorithm 1.

Milestones

The milestones are numbered results and displays of the paper, in the order its argument uses them:

$\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$ are effective (Definition 4, p. 9).
(7), p. 10: a safe edge (one whose neighbourhood has neither a successful probe nor an exhausted patience before it arrives) is free, so $a(e)\Pr[e \text{ is free}] \ge \tilde a(p_e y_e)\Pr[e \text{ is safe}]$ .
Lemma 3, p. 11: $\prod_{f \in E_1(r)} (1 - x\,a(f) y_f) \ge e^{-x \sum_{f \in E_1(r)} y_f}$ for an effective attenuation, where $E_1(r)$ is the set of edges at $r$ other than $e$ with $p_f = 1$ .
Lemma 4, p. 12 (Baveja et al.): $\Pr[\sum_i B_i < t] \ge \Pr[\mathrm{Pois}(\mu) < t]$ for independent Bernoullis with mean sum $\mu < t - 1$ .
Lemma 5, p. 12: the Chernoff bound $\Pr[\sum_i B_i < (1+\varepsilon)\mu] \ge 1 - e^{-\varepsilon^2 \mu/(2+\varepsilon)}$ .
Proposition 1, p. 14: $\int_0^1 \lambda\varphi \ge \lambda(z^*)\int_0^1 \varphi$ for $\lambda \ge 0$ non-increasing and $\varphi$ changing sign once, from $+$ to $-$ , at $z^*$ .
(22), p. 15: $\tilde a(y_e)\int_0^1 (e^{-x(2-y_e)} + x e^{-x(2-y_e)})^2\,dx \ge \beta^*$ on $[0,1]$ , with equality at $y_e = 0$ .

Significance

The result. Equation (4) of the paper writes the expected weight of the algorithm's matching as $\sum_e w_e p_e y_e\, a(e)\Pr[e \text{ is free}]$ . Theorem 1 therefore gives at least $\beta^* \sum_e w_e p_e y_e$ , and with an optimal LP solution and the LP upper bound of Bansal et al. this is a $0.382$ -approximation for stochastic matching on general graphs with patience at least $2$ . 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 $0.3828$ in the last case exceeds $\beta^*$ by about $5 \cdot 10^{-5}$ . 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.

Difficulty

The obvious argument bounds $\Pr[e \text{ is free}]$ by a product over the two endpoints of $e$ and applies a Poisson approximation to the number of probes at each endpoint. For an endpoint of patience $2$ that approximation is only valid for arrival times $x < x_c$ , a threshold that can be $1/2$ , and the bound it gives, about $0.347$ (display (16)), falls below $\beta^*$ . 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.

Formalization scope

The graph is the platform's EdmondsMatching65.Polyhedron.Graph (loopless); the goal adds that the endpoint map is injective, since the paper's edges are pairs $\{u,v\}$ . Patience is ℕ∞, with $\infty$ allowed; "minimum patience $2$ " is $t_v \ge 2$ at every vertex.
Standing assumptions: $p_e \in [0,1]$ for every edge; $y$ feasible for LP (3) (which includes $y_e \in [0,1]$ ).
Every probability is a finite average: over the $|E|!$ orders of the edges and over the $2^{3|E|}$ outcomes of the coins $Y, A, P$ , each weighted by a product of Bernoulli weights. The paper's continuous arrival times induce exactly this uniform order. $\Pr[e \text{ is free}]$ is computed from the run of Algorithm 1 (matched vertices and probe counters, step by step), never from the product formulas of p. 11, which would assume the lemmas being proved.
The goal is stated for $\tilde a_{\exp}$ and $\tilde a_{\mathrm{lin}}$ with $\alpha = 1/2$ . Theorem 1 cites "Definition 3 where $\alpha = 1/2$ "; $\alpha$ belongs to Definition 4, and an arbitrary effective function would make the statement false. The third function of Definition 4 is not effective (its $\ln(1 - xz\tilde a(z))$ is concave near $z = 0$ for $x$ close to $1$ ), so neither the effectiveness milestone nor the goal covers it.
Lemma 4 prints $e^{-x\mu}$ in the Poisson sum; the statement uses $e^{-\mu}$ .
A formalization that defines "free" without the patience counters or the matched set, one that bounds $\Pr[e \text{ is safe}]$ or the integral (8) instead of $a(e)\Pr[e \text{ is free}]$ , or one stated for "some" attenuation function, is a different theorem and does not count.
Not stated: Lemma 2 (a without-loss-of-generality reduction), Lemma 6 (its hypothesis is a graph built in another paper, with property (18) asserted there), the conditional bounds (8)–(17) and (23)–(25), whose objects live inside the proof, and the numerical values of pp. 13–15. Solvers who need them are welcome to state them as their own lemmas. The paper's proofs are in §3.2, pp. 9–15.
Reusable beyond this mission: the finite model of Algorithm 1 and its events, Lemma 4 (Bernoulli versus Poisson lower tails), Lemma 5 (a Chernoff bound for independent Bernoullis), and Proposition 1.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3 (20 Apr 2026). https://arxiv.org/abs/2106.06892v3
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012 (reference [7] of the paper).
A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved bounds in stochastic matching and optimization, Algorithmica 80(11):3225–3252, 2018 (reference [8]; source of Lemma 4).
M. Adamczyk, F. Grandoni, J. Mukherjee, Improved approximation algorithms for stochastic matching, ESA 2015, 1–12 (reference [1]).
N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating matches made in heaven, ICALP 2009, 266–278 (reference [15]).

10 thms1 active userReviewed

Combinatorics Operations Research Optimization+1·Captain: mikedeng1

Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes II: With Infinite Patience, Attenuated Random-Order Probing Probes Each Edge w.p. ≥ (1 − e^(−2))y_e/2Research Paper

Motivation

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.

Setting

Let $G=(V,E)$ be a finite graph. Each edge $e$ is active independently with known probability $p_e\in[0,1]$ , and each vertex $v$ has a patience $t_v\in\mathbb N\cup\{\infty\}$ , the maximal number of edges at $v$ that may be probed. Write $\delta(v)$ for the edges incident to $v$ . A vector $(y_e)_{e\in E}$ is feasible for LP (3) when

0\le y_e\le 1,\qquad \sum_{e\in\delta(v)}y_ep_e\le 1,\qquad \sum_{e\in\delta(v)}y_e\le t_v\qquad(e\in E,\ v\in V);

$y_e$ is read as the probability of probing $e$ , and $z_e=y_ep_e$ as the probability that $e$ is matched.

An attenuation function is a map $\tilde a:[0,1]\to[0,1]$ , and the attenuation of an edge is $a(e)=\tilde a(p_ey_e)$ . The paper's examples (Definition 4) are $\tilde a_{\exp}(z)=e^{-\alpha z}$ , $\tilde a_{\rm lin}(z)=1-\alpha z$ , and $\tilde a(z)=\frac{1-z}{1-e^{-(1-z)}}(1-1/e)$ . A function is effective (Definition 3) when $\tilde a(0)=1$ and $z\mapsto\ln(1-xz\tilde a(z))$ is convex on $[0,1]$ for every $x\in(0,1)$ .

Algorithm 1 draws independent coins $Y_e\sim\mathrm{Bernoulli}(y_e)$ and $A_e\sim\mathrm{Bernoulli}(a(e))$ and processes the edges in a uniformly random order. When it reaches $e$ , it probes $e$ if $e$ is free (both endpoints unmatched and with remaining patience), $Y_e=1$ and $A_e=1$ . A probe uses one unit of patience at both endpoints and reveals the activeness $P_e\sim\mathrm{Bernoulli}(p_e)$ ; if $P_e=1$ , both endpoints are matched. The edge $e=\{u,v\}$ is safe when, before $e$ is processed, each endpoint $r$ has received at most $t_r-1$ probes and no earlier edge $f\neq e$ at $u$ or $v$ has $A_fP_fY_f=1$ .

Formalization targets

Goal: Corollary 5 (p. 16)

If every patience is $\infty$ , $(y_e)$ is feasible for LP (3), and $\tilde a$ is $\tilde a_{\exp}$ or $\tilde a_{\rm lin}$ with $\alpha=1/2$ , then for every edge $e$

\Pr[\text{Algorithm 1 probes }e]\ \ge\ \Bigl(\int_0^1e^{-2x}\,dx\Bigr)y_e=\tfrac12\bigl(1-e^{-2}\bigr)y_e\approx0.432\,y_e .

Milestones

The exponential and linear functions with $\alpha=1/2$ are effective (p. 9).
Equation (4) (p. 9): the expected matched weight is $\sum_ew_ep_e\Pr[e\text{ free}]\Pr[Y_e=1\cap A_e=1]=\sum_ew_ep_ey_ea(e)\Pr[e\text{ free}]$ .
Equation (7) (p. 10): $a(e)\Pr[e\text{ is free}]\ge\tilde a(p_ey_e)\Pr[e\text{ is safe}]$ .
Lemma 3 (p. 11): $\prod_{f\in E_1(r)}(1-xa(f)y_f)\ge e^{-x\sum_{f\in E_1(r)}y_f}$ for effective $\tilde a$ , where $E_1(r)$ is the set of edges $f\neq e$ at $r$ with $p_f=1$ .
§3.3 (p. 16): $z\mapsto\tilde a(z)\int_0^1e^{-2x(1-z)}dx$ is minimized on $[0,1]$ at $z=0$ .

Companion: Corollary 6 (p. 16)

On a star graph with infinite patience and the third attenuation function, $\Pr[e\text{ is probed}]\ge(1-1/e)\,y_e$ . It comes with the identity of p. 16 behind it: for the third function, $\tilde a(z)\int_0^1e^{-x(1-z)}dx=1-1/e$ for all $z\in[0,1]$ . Both are plain items of the mission, not milestones.

Significance

By (4), Corollary 5 bounds the expected weight of Algorithm 1 by $\frac12(1-e^{-2})\sum_ew_ep_ey_e$ , and with an optimal $y$ and the bound of Bansal et al. this is a $0.432$ -approximation for stochastic matching without patience constraints. Because the bound holds edge by edge and for every feasible $y$ , 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 $1-1/e$ .

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.

Difficulty

The obvious argument treats the edges at the two endpoints of $e$ as independent obstacles, each blocking $e$ with probability proportional to its LP value. That fails because being free is not a product event: whether an earlier edge $f$ blocks $e$ depends on whether $f$ was itself free, which depends on the whole run before $f$ . A second difficulty is uniformity. The bound must hold for every feasible $y$ , 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.

Formalization scope

Model. The graph is the platform's EdmondsMatching65.Polyhedron.Graph (finite, loopless, parallel edges allowed). Probabilities $p$ , LP values $y$ , weights $w$ and attenuations are real; patience is in ℕ∞, with $\top=\infty$ . Every probability is a finite average over the $|E|!$ orders of $E$ and over all outcomes of the coins $Y$ , $A$ , $P$ , 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.
Standing assumptions. $0\le p_e\le1$ for every edge (the meaning of "probability of being active"); LP (3) feasibility, which contains $0\le y_e\le1$ ; attenuations with values in $[0,1]$ on $[0,1]$ .
Disclosed choices. Corollary 5 is stated for $\tilde a_{\exp}$ and $\tilde a_{\rm lin}$ with $\alpha=1/2$ : the corollary says "the effective attenuation functions from Definition 4", its proof names these two, and the third function fails Definition 3 ( $g''(0)<0$ for $x$ near 1). The effectiveness milestone is stated for these two only. The third function is given its limit $1-1/e$ at $z=1$ , where the printed formula is $0/0$ . Corollary 6 is a companion item, not a milestone: the paper's argument for it passes through Lemma 3, which does not apply to the third function, so it is supported by numerical checks but its printed proof has a gap.
Not stated. The approximation-ratio and "balanced contention resolution scheme" sentences of Corollaries 5 and 6 need a model of all adaptive probing algorithms (Lemma 1 of the paper, from Bansal et al.) and are out of scope; the goals are the displayed probability bounds.
Ruled out. Defining $\Pr[e\text{ is free}]$ or $\Pr[e\text{ is probed}]$ by the product formula of p. 11 instead of from the run, or stating the goal for "some" attenuation function, would make the goal a different and easier theorem; neither is done.
Welcome contributions. Proofs of the milestones; a general lemma that an event depending only on the edges before $e$ is independent of $e$ 's coins; a conditioning-on-arrival-time lemma for uniform permutations; a proof (or a counterexample) for Corollary 6.

Selected references

B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025; arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP Is the Cure for Your Matching Woes: Improved Bounds for Stochastic Matchings, Algorithmica 63(4):733–762, 2012. https://link.springer.com/journal/453/volumes-and-issues/63-4
A. Baveja, A. Chavan, A. Nikiforov, A. Srinivasan, P. Xu, Improved Bounds in Stochastic Matching and Optimization, Algorithmica 80(11):3225–3252, 2018. https://link.springer.com/journal/453/volumes-and-issues/80-11
N. Chen, N. Immorlica, A. R. Karlin, M. Mahdian, A. Rudra, Approximating Matches Made in Heaven, ICALP 2009, LNCS 5555. https://doi.org/10.1007/978-3-642-02927-1

8 thms1 active userReviewed

Completed

Captain: Chutong

CLRS — Chapter 4, §4.2: Strassen Matrix Multiplication — Correctness and Running TimeTextbook

Prove2Me mission category: Textbook.

Reusable fast matrix multiplication

Matrix multiplication is often a component of a larger computation. A useful verified routine must return the right product, preserve its caller's data, and bound the work performed by the same returning call. Strassen's algorithm reduces the number of recursive block products from eight to seven, obtaining a subcubic arithmetic bound. This mission connects that algorithm to a mutable array implementation and a reusable Lean contract.

The reference is Introduction to Algorithms (CLRS), fourth edition, Chapter 4, §4.2: Strassen's algorithm for matrix multiplication. CLRS, fourth edition. The underlying algorithm is an established result originating in Strassen's 1969 paper.

Matrices, returned product, and measured work

A matrix is represented by an array of row arrays, written Seq[Seq[Int]]. Each row contains unbounded mathematical integers. Let $k\in\mathbb N$ be the recursion depth and $n=2^k$ the matrix dimension. The mathematical input values are functions $A,B:\mathbb Z\to\mathbb Z\to\mathbb Z$ ; only their entries inside the $n\times n$ square enter the product.

A heap $h$ stores mutable rows, outer arrays, objects, and named natural-number counters. The predicate MatrixHeap.Stored h a A connects an allocated outer-array reference $a$ to its row contents $A$ . Both input arrays must satisfy this representation predicate. Input matrices and their rows may share references, including sharing between the two inputs.

A Call contract supplies a finite execution in the generated semantics: for every suspended caller stack, strassen.Call returns the same result reference $r$ and final heap $h'$ . All correctness, preservation, and work conclusions below concern that same $h'$ and $r$ .

The counted work $T$ sums the increments of four source clocks: products for scalar leaf products, calls for all Strassen invocations (including the initial call), linear_cells for entrywise combinations, and copied_cells for entries copied during quadrant extraction and joining. Each increment has unit weight. Initial counters may be nonzero; the bound concerns additional work.

Formalization targets

The main correctness-and-running-time theorem already has an accepted proof on Prove2Me under Lean 4.33.1. Its name is CLRS.Chapter4Publication.Strassen.correctness_and_running_time.

For every represented input of dimension $n=2^k$ , the contract supplies a finite returning call whose output matrix $R$ satisfies

R_{ij}=\sum_{t=0}^{n-1} A_{it}B_{tj}\quad(0\le i,j<n), \qquad R_{ij}=0\quad\text{outside this square}.

Every previously allocated row, outer array, and object is preserved. The result's outer array is fresh, and its $n$ in-square rows are fresh and pairwise distinct. One positive natural constant is chosen before all depths, heaps, and matrix inputs:

\exists C>0,\quad \forall\text{ represented inputs with }n=2^k,\quad \exists\text{ a correct returning call with }7^k\le T\le C7^k.

Thus the main proposition leaves the upper constant available for improvement. The accepted proof supplies $C=13$ . On the permitted dimensions this gives the conventional $\Theta(n^{\log_2 7})$ counted-work bound. The checked headline states natural-power inequalities, rather than a real-logarithm asymptotic relation over arbitrary dimensions.

The exact counter schedule is stronger than the displayed upper bound. Writing $Q_0=1$ , $Q_{k+1}=1+7Q_k$ , $H_0=0$ , and $H_{k+1}=4^k+7H_k$ , the four increments are

\Delta\mathrm{products}=7^k,\quad \Delta\mathrm{calls}=Q_k,\quad \Delta\mathrm{linear\_cells}=18H_k,\quad \Delta\mathrm{copied\_cells}=12H_k.

All other clocks remain unchanged. Consequently the total satisfies $T(0)=2$ and $T(k+1)=7T(k)+30\cdot4^k+1$ . These are properties of the existing combined contract and its supporting definitions, rather than additional open targets.

What callers can reuse

A later algorithm can invoke the multiplication routine with its existing heap and counters and use the established product, preservation, freshness, and work guarantees. Fresh independent output rows permit subsequent row updates without aliasing another in-square output row or an input row. The surrounding algorithm still proves its own input representation and any new conclusions; it can reuse this multiplication analysis unchanged.

The source development contains the matrix algebra, mutable execution analysis, and exact clock summaries. The contribution is their connection in one importable contract. The mission reuses the published theorem and its existing dependencies. Alternative checked proofs, improved constants, and verified client examples can build on that result.

Where the formalization is demanding

The seven-product identity alone does not establish that a mutable program returns the product. Quadrant copies, intermediate combinations, allocations, and possible input sharing must agree with the mathematical matrices. Equal row contents do not imply independent row references.

Counting only scalar leaf products also omits copying and combination work. A numerical recurrence by itself does not supply a returning program execution. The contract must connect those charges and the returned values to the same finite call while preserving caller storage.

Formalization scope and source

The .algo implementation follows the seven recursive products and block recombination of CLRS §4.2, making quadrant copies and result allocation explicit. The complete source file is shown below.

Sequences are total over integer indices. Stored requires an allocated row at every integer row index, including indices outside the finite square. In a fixed heap only finitely many distinct whole row sequences can be represented; out-of-square rows may share storage. The contract does not assume the desired product, an existing transcript, or an unverified runtime bound. Its execution conclusion is an existential returning-call guarantee; the headline alone does not quantify over every possible execution.

Depth zero gives dimension one and $T=2$ . Dimension zero, other dimensions, rectangular multiplication, and automatic padding are outside this contract. Freshness and pairwise distinctness of output rows apply to the finite square. The cost model excludes allocation, uncharged bookkeeping, total generated transition counts, elapsed time, and integer bit complexity. Multiplication by sign in a linear combination is charged to linear_cells, not products.

The exact compiler/source snapshot is fd33cf959b39f9e4a9fcfda4ef31d5a36b784d41, an Algo2Lean development snapshot distinct from public v0.1.4. The repository pins Lean 4.26.0; the accepted platform declarations use Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The publication record records the source and adaptation checks. Platform packaging uses the CLRS namespace and adapted imports. Source generation, declaration comparison, and Lean proof checking are separate checks; the compiler itself has no formal semantics-preservation proof.

`examples/matrix_strassen.algo`

# Strassen multiplication with correctness and Θ(n^(log₂ 7)) counted work for n = 2^k (CLRS 4.2).
# Preconditions: n = 2^depth for a natural depth; inputs have arbitrary Int entries.
# Every finite output row is fresh. Input matrices and their rows are never modified.

def matrix_linear_row(a: Seq[Int], b: Seq[Int], count: Int, sign: Int) -> Seq[Int]:
    c = const(0)
    i = 0
    # @loop
    while i < count:
        c[i] = a[i] + sign * b[i]
        tick("linear_cells")
        i += 1
    return c


def matrix_linear(a: Seq[Seq[Int]], b: Seq[Seq[Int]], count: Int, sign: Int) -> Seq[Seq[Int]]:
    c: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < count:
        c[i] = matrix_linear_row(a[i], b[i], count, sign)
        i += 1
    return c


def matrix_quadrant_row(a: Seq[Int], h: Int, column: Int) -> Seq[Int]:
    c = const(0)
    i = 0
    # @loop
    while i < h:
        c[i] = a[column + i]
        tick("copied_cells")
        i += 1
    return c


def matrix_quadrant(a: Seq[Seq[Int]], n: Int, h: Int, row: Int, column: Int) -> Seq[Seq[Int]]:
    c: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < h:
        c[i] = matrix_quadrant_row(a[row + i], h, column)
        i += 1
    return c


def matrix_join_row(a: Seq[Int], b: Seq[Int], h: Int) -> Seq[Int]:
    result = const(0)
    i = 0
    # @loop
    while i < h:
        result[i] = a[i]
        result[i + h] = b[i]
        tick("copied_cells", 2)
        i += 1
    return result


def matrix_join(a: Seq[Seq[Int]], b: Seq[Seq[Int]], c: Seq[Seq[Int]], d: Seq[Seq[Int]], h: Int) -> Seq[Seq[Int]]:
    result: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < h:
        result[i] = matrix_join_row(a[i], b[i], h)
        result[i + h] = matrix_join_row(c[i], d[i], h)
        i += 1
    return result


def strassen(a: Seq[Seq[Int]], b: Seq[Seq[Int]], n: Int) -> Seq[Seq[Int]]:
    tick("calls")
    if n <= 1:
        c: Seq[Seq[Int]] = const(const(0))
        c[0] = const(0)
        c[0][0] = a[0][0] * b[0][0]
        tick("products")
        return c
    else:
        h = n // 2
        a11 = matrix_quadrant(a, n, h, 0, 0)
        a12 = matrix_quadrant(a, n, h, 0, h)
        a21 = matrix_quadrant(a, n, h, h, 0)
        a22 = matrix_quadrant(a, n, h, h, h)
        b11 = matrix_quadrant(b, n, h, 0, 0)
        b12 = matrix_quadrant(b, n, h, 0, h)
        b21 = matrix_quadrant(b, n, h, h, 0)
        b22 = matrix_quadrant(b, n, h, h, h)
        # Seven recursive products replace the ordinary eight.
        p1 = strassen(a11, matrix_linear(b12, b22, h, -1), h)
        p2 = strassen(matrix_linear(a11, a12, h, 1), b22, h)
        p3 = strassen(matrix_linear(a21, a22, h, 1), b11, h)
        p4 = strassen(a22, matrix_linear(b21, b11, h, -1), h)
        p5 = strassen(matrix_linear(a11, a22, h, 1), matrix_linear(b11, b22, h, 1), h)
        p6 = strassen(matrix_linear(a12, a22, h, -1), matrix_linear(b21, b22, h, 1), h)
        p7 = strassen(matrix_linear(a11, a21, h, -1), matrix_linear(b11, b12, h, 1), h)
        c11 = matrix_linear(matrix_linear(matrix_linear(p5, p4, h, 1), p2, h, -1), p6, h, 1)
        c12 = matrix_linear(p1, p2, h, 1)
        c21 = matrix_linear(p3, p4, h, 1)
        c22 = matrix_linear(matrix_linear(matrix_linear(p5, p1, h, 1), p3, h, -1), p7, h, -1)
        return matrix_join(c11, c12, c21, c22, h)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 4, §4.2. Publisher.
Volker Strassen, “Gaussian Elimination is Not Optimal,” Numerische Mathematik 13, 354–356, 1969. DOI.
Algo2Lean, Chapter 4 source and proof development, 2026. Source snapshot. Algo2Lean was created by Lunjia Hu; Chutong Yang is a contributor, and both are software citation authors.

1 thm1 active userReviewed

Completed

Captain: lunjia

CLRS — Chapter 21, §21.2: Kruskal — Correctness and Inverse-Ackermann Running TimeTextbook

Prove2Me mission category: Textbook.

Reusable minimum spanning forest algorithms

Kruskal builds a cheapest connecting forest by considering edges in weight order and selecting those that join different components. A caller may already have that order, so the cost of sorting should be distinguished from the work that remains. This development provides two callable entry points and two running-time results: the complete algorithm, and the algorithm after sorting.

The .algo implementation closely follows the textbook pseudocode in CLRS. It makes the edge scan, representative tests, edge selection, union by rank, and full path compression explicit. The separate post-sorting entry point lets callers reuse a supplied order without repeating the sorting step.

This mission belongs to the formalization series for Introduction to Algorithms (CLRS), fourth edition: Chapter 21, §21.2 for Kruskal, Theorem 21.1 in §21.1 for safe edges, and Theorem 19.14 in §19.4 for union by rank with path compression. These are established textbook results; the contribution here is their connection to executable-looking source and reusable Lean call contracts. CLRS, fourth edition.

Graph, supplied edge order, and measured work

An undirected weighted graph has vertices 0, …, V−1 and edge identifiers 0, …, E−1. Three integer sequences give each edge's source, target, and weight. Counts are nonnegative, and endpoints lie in the declared vertex range. Edge identifiers distinguish parallel edges. Weights may be negative, and self-loops are permitted.

A minimum spanning forest is an acyclic selection that connects exactly the original graph's connected components and minimizes total weight among all such forests. The returned sequence marks selected identifiers with 1 and every other integer index with 0. For a nonempty connected graph the result is a minimum spanning tree.

The complete entry point is kruskal(size, sources, targets, weights, count). The post-sorting entry point is kruskal_sorted(size, sources, targets, weights, count, order). Its additional sorted order is a permutation of all edge identifiers, in nondecreasing weight order. Equal-weight identifiers may occur in either order; the arrays and output flags retain the original identifiers. The predicate SortIndicesAnalysis.SortedPermutation states this precondition.

A heap stores mutable sequences, objects, collections, and named counters. A Call contract supplies a finite returning execution that can be invoked from another program with its existing heap and counters. Input sequence references must be allocated and may alias. Both entry points preserve all previously allocated caller storage.

Runtime T is the sum of increments of eight natural-number clocks: sort_steps, heap_comparisons, heap_swaps, uf_init, uf_find, uf_compress, uf_union, and kruskal. Each has unit weight. The post-sorting call has zero increments on the three sorting clocks. Let $L(E)=\lfloor\log_2(E+1)\rfloor$ and let $\alpha$ denote the inverse Ackermann function with convention $A_0(r)=r+1$ , $A_{k+1}(r)=A_k^{\circ(r+1)}(r)$ , and $\alpha(n)=\min\{k>0:A_k(1)>n\}$ , where the superscript denotes repeated composition. Its published definition is shared with the data-structure analysis.

Formalization targets

Both main results provide termination, minimum spanning forest correctness, fresh output storage, preservation of caller storage, and a bound on the same call's additional work. Each quantifies one positive constant before all graph inputs and initial heaps.

Entire algorithm, including sorting

\exists C>0,\qquad T\le C\bigl(V+1+E L(E)\bigr) \quad\text{for every well-formed graph input.}

This is KruskalAnalysis.correctness_and_running_time, with scale KruskalAnalysis.runtimeScale. It gives the conventional total $O(V+E\log(E+1)+1)$ bound; sorting remains charged. The proof absorbs the inverse-Ackermann contribution into the vertex and sorting terms, without requiring connectedness or a density assumption. Thus the total bound has no redundant inverse-Ackermann factor.

After sorting

\exists C>0,\qquad T\le C\bigl(V+1+E\alpha(V)\bigr) \quad\text{for every well-formed input and supplied sorted order.}

This is KruskalSortedAnalysis.correctness_and_running_time, with scale KruskalSortedAnalysis.runtimeScale. It describes an actual call that skips sorting, including singleton initialization and the entire edge scan. It is not obtained by supplying sorted data to a function that sorts again. The additive unit in both statements covers the empty graph.

The explicit supporting call_contract results retain the budgets

T_{\mathrm{sorted}}\le V+2+E\bigl(10\alpha(V)+14\bigr),

T_{\mathrm{total}}\le 2E\bigl(3L(E)+2\bigr) +V+2+E\bigl(10\alpha(V)+14\bigr).

These expressions are the respective runtimeBound definitions. Main statements leave the constant unspecified so improved constants do not change their propositions. The component milestones are independent union-find method contracts, the sorter's permutation/order contract, the post-sorting call contract, and the complete composition.

What callers can reuse

The union-find implementation and its published correctness and inverse-Ackermann analysis are reused unchanged. Its find contract, union contract, and constructor contract apply independently of graphs. They account for the same evolving object's state and amortized potential across calls. Future algorithms can import them without repeating the rank or path-compression analysis. The indexed-heap sorting contract is also reused unchanged.

A caller with its own verified sorted order can invoke kruskal_sorted and receive an allocated, fresh output, its mathematical specification, unchanged caller storage, and the smaller runtime bound. The complete algorithm invokes that same verified entry point after sorting; the two results share the scan and data-structure proofs. Initial counters need not be zero. Ordinary Returns and ReturnsWithCost theorems are convenient views of these reusable Call results.

The revised source analyses have been checked under Lean 4.33.1. Both the complete algorithm result and the post-sorting result have accepted Prove2Me proofs, as do their shared union-find and sorting components. This is a formalization of known algorithms, not a claim of a new mathematical bound.

Where the formalization is demanding

Union by rank bounds an individual parent path logarithmically. Applying that bound independently to every operation does not establish the sharper accumulated inverse-Ackermann bound. Path compression changes future costs, so a usable method contract must describe the actual returned state and the same object's remaining amortized potential.

The component partition must also agree with the concrete selected flags. An abstract forest theorem alone does not show what the source returned. A cost theorem must include the two finds on each edge, the finds inside accepted unions, initialization, and any sorting the entry point performs. These obligations connect the graph result, mutable implementation, and measured work.

Formalization scope and source

The .algo code closely matches textbook MST-KRUSKAL: sort edges, create singleton components, compare endpoint representatives, and mark and join accepted edges. The sorting and following initialization/scan are separate callable functions. Sorting precedes singleton initialization here; neither stage changes the graph arrays. Integer identifiers and zero/one flags represent edge sets, and the constructor performs the MAKE-SET loop. The source retains full path compression, union by rank, and the explicit finds inside union.

Inputs use unbounded mathematical integers and mutable sequences defined at every integer index; finite prefixes describe the graph. Empty and disconnected graphs, negative weights, parallel edges, and self-loops are covered. Invalid counts, out-of-range endpoints, or an invalid supplied order are outside the main contracts. No contract assumes a preexisting successful transcript, an already minimal answer, or unverified data-structure behavior.

The runtime counts the eight named tick events, including imported calls. It does not measure elapsed time, integer bit complexity, or every arithmetic operation, access, allocation, or generated transition. Constructing input arrays and a caller-supplied sorted order is outside kruskal_sorted; the complete entry point includes sorting. The amortized bound does not assert inverse-Ackermann worst-case time for each individual operation.

Definitions and proofs cover the Ackermann hierarchy, rank/partition model, amortized union-find, mutable method contracts, sorting, graph exchange mathematics, and generated call composition. These components support further clients and sharper explicit bounds independently of Kruskal.

The compiler is Algo2Lean v0.1.4, with immutable release commit 0f79d5e. The examples and analyses are frozen separately at public commit 9755b41d188977ae1aafdaf9eccdac0b0edb0420; the compiler version is unchanged. The source and proof guide locates both entry points and their theorems. Raw generated Lean and Prove2Me packaging are distinct: platform packaging adapts module imports and declaration layout. The compiler itself does not yet have a formal semantics-preservation proof, so the source and generated semantics remain part of the reviewable development.

The import root is examples/kruskal. All five source files are shown below, including every imported module.

`kruskal.algo`

# CLRS MST-KRUSKAL (fourth edition, Section 21.2): sort edge identifiers,
# then scan them using union by rank and path compression.
# The separate kruskal_sorted entry point reuses an order supplied by a caller.
from sort_indices import sort_indices
from kruskal_sorted import kruskal_sorted


def kruskal(size: Int, sources: Seq, targets: Seq, weights: Seq, count: Int) -> Seq:
    order = sort_indices(weights, count)
    return kruskal_sorted(size, sources, targets, weights, count, order)

`kruskal_sorted.algo`

# The post-sorting phase of CLRS MST-KRUSKAL (fourth edition, Section 21.2).
# order lists every edge identifier once, in nondecreasing weight order.
# Edge identifiers are 0, ..., count - 1; endpoint arrays contain vertices
# in 0, ..., size - 1. The zero/one flag sequence represents the edge set A.
from union_find import UnionFind


def kruskal_sorted(size: Int, sources: Seq, targets: Seq, weights: Seq, count: Int, order: Seq) -> Seq:
    chosen = const(0)
    # Construct one singleton set for each vertex (the textbook MAKE-SET loop).
    sets = UnionFind(size)
    index = 0
    tick("kruskal")
    # @scan
    while index < count:
        edge = order[index]
        a = sources[edge]
        b = targets[edge]
        tick("kruskal")
        left = sets.find(a)
        right = sets.find(b)
        # @test
        if left != right:
            # @select
            chosen[edge] = 1
            # @join
            sets.union(a, b)
        index += 1
    return chosen

`union_find.algo`

# Disjoint sets over the integer elements 0, ..., size - 1.
# Each root names one component. Union by rank bounds parent paths, and
# find compresses every visited path directly to its root.
# Clients must pass in-range elements. The representation is independent
# of graphs, edge weights, or any particular client algorithm.

class UnionFind:
    parent: Seq
    rank: Seq
    size: Int

    def __init__(self, size: Int) -> None:
        # Batch the CLRS MAKE-SET operation for all elements in [0, size).
        self.parent = const(0)
        self.rank = const(0)
        self.size = size
        vertex = 0
        tick("uf_init")
        # @initialize
        while vertex < size:
            self.parent[vertex] = vertex
            vertex += 1
            tick("uf_init")

    def find(self, vertex: Int) -> Int:
        # CLRS FIND-SET: recursion finds the root, then rewrites every parent
        # along the return path. This is full path compression, not path halving.
        parent = self.parent
        tick("uf_find")
        # @follow
        if parent[vertex] == vertex:
            return vertex
        root = self.find(parent[vertex])
        # @compress
        parent[vertex] = root
        tick("uf_compress")
        return root

    def union(self, a: Int, b: Int) -> Bool:
        # CLRS UNION: find both roots, then apply union by rank (LINK).
        # The Boolean result reports whether two components were joined.
        left = self.find(a)
        right = self.find(b)
        tick("uf_union")
        if left == right:
            return False
        # @link
        if self.rank[left] < self.rank[right]:
            self.parent[left] = right
        elif self.rank[right] < self.rank[left]:
            self.parent[right] = left
        else:
            # Equal ranks may choose either root; here the left root wins.
            self.parent[right] = left
            self.rank[left] = self.rank[left] + 1
        return True

`sort_indices.algo`

# Order the identifiers [0, count) by their keys using a reusable binary heap.
# This supplies Kruskal's sort-by-weight step: insert every identifier, then
# extract minima. It is not the in-place HEAPSORT procedure from CLRS Chapter 6.
# Only identifiers are reordered; keys are unchanged. Equal-key identifiers
# may appear in either order.
from indexed_heap import MinHeap


def sort_indices(keys: Seq, count: Int) -> Seq:
    queue = MinHeap()
    result = const(0)
    index = 0
    # @insert
    while index < count:
        tick("sort_steps")
        queue.push_or_decrease(index, keys[index])
        index += 1
    index = 0
    # @extract
    while index < count:
        tick("sort_steps")
        result[index] = queue.pop_min()
        index += 1
    return result

`indexed_heap.algo`

# An indexed binary min-heap for Dijkstra's priority queue.
# vertices[position] and positions[vertex] are inverse on the active prefix.
# keys is indexed by vertex; position -1 means the vertex is not in the heap.
# Clients use nonnegative vertex identifiers, so pop_min can use -1 for empty.

class MinHeap:
    vertices: Seq
    positions: Seq
    keys: Seq
    size: Int

    def __init__(self) -> None:
        self.vertices = const(0)
        self.positions = const(-1)
        self.keys = const(0)
        self.size = 0

    def swap(self, i: Int, j: Int) -> None:
        a = self.vertices[i]
        b = self.vertices[j]
        # @exchange
        self.vertices[i] = b
        self.vertices[j] = a
        self.positions[a] = j
        self.positions[b] = i
        tick("heap_swaps")

    def sift_up(self, i: Int) -> None:
        # @up_loop
        while i > 0:
            parent = (i - 1) // 2
            tick("heap_comparisons")
            if self.keys[self.vertices[parent]] <= self.keys[self.vertices[i]]:
                return
            self.swap(i, parent)
            i = parent

    def sift_down(self, i: Int) -> None:
        # @down_loop
        while 2 * i + 1 < self.size:
            child = 2 * i + 1
            right = child + 1
            if right < self.size:
                tick("heap_comparisons")
                if self.keys[self.vertices[right]] < self.keys[self.vertices[child]]:
                    child = right
            # @compare_child
            tick("heap_comparisons")
            if self.keys[self.vertices[i]] <= self.keys[self.vertices[child]]:
                return
            self.swap(i, child)
            i = child

    def push_or_decrease(self, vertex: Int, key: Int) -> None:
        i = self.positions[vertex]
        if i < 0:
            self.keys[vertex] = key
            i = self.size
            self.vertices[i] = vertex
            self.positions[vertex] = i
            self.size += 1
            self.sift_up(i)
        else:
            tick("heap_comparisons")
            if key < self.keys[vertex]:
                self.keys[vertex] = key
                self.sift_up(i)

    def pop_min(self) -> Int:
        if self.size <= 0:
            return -1
        vertex = self.vertices[0]
        last = self.size - 1
        self.swap(0, last)
        self.size = last
        self.positions[vertex] = -1
        if last > 0:
            self.sift_down(0)
        return vertex

    def is_empty(self) -> Bool:
        return self.size <= 0

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022: Chapter 21, §§21.1–21.2, Theorem 21.1; Chapter 19, §§19.3–19.4, Theorem 19.14; and Chapter 6, §§6.1–6.2 and §6.5. Publisher.
Algo2Lean, version 0.1.4, Lean-targeting compiler and source examples. Compiler and source repository.
UnionFindAnalysis.find_amortized and UnionFindAnalysis.union_amortized, independently verified mutable union-find correctness and amortized work. Find and union.
SortIndicesAnalysis.call, independently verified indexed-heap sorting with a permutation, nondecreasing keys, preserved caller storage, and work budget. Published theorem.

11 thms1 active userReviewed

Completed

Captain: lunjia

CLRS — Chapter 21, §21.2: Prim with a Fibonacci Heap — Correctness and Running TimeTextbook

Prove2Me mission category: Textbook.

Reusable minimum spanning tree algorithms

A minimum spanning tree connects a weighted network at minimum total edge cost. When this routine is part of a larger algorithm, its caller also needs termination, preservation of existing data, and a bound on the work performed. These guarantees belong in a reusable contract, together with the returned mathematical result.

Prim reuses the Fibonacci heap already formalized for Dijkstra, including its published correctness and amortized running-time proofs.

This development follows Introduction to Algorithms (CLRS), fourth edition, Chapter 21, §21.2 for Prim and Theorem 21.1 in §21.1 for safe edges. The Fibonacci-heap analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5. That supplement is distinct from printed fourth-edition Chapter 19, which concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, returned tree, and measured work

An undirected weighted graph has vertices 0, …, V−1 and finite adjacency lists. Every edge occurs in both directions with the same integer weight. Weights may be negative. Parallel edges retain separate occurrence identities, and self-loops are permitted. Let m count undirected edge occurrences and E count stored adjacency occurrences: the supplied graph constructor gives E = 2m, including for self-loops. The root satisfies 0 ≤ root < V, and the main result assumes the graph is connected.

The output is a parent sequence, a mutable mathematical function from all integer indices to integers. The root has parent −1; every other declared vertex names its predecessor toward the root. A minimum spanning tree is an acyclic selection of input edges connecting every declared vertex, with minimum total weight among all competing spanning forests. The formal SpanningParents predicate asserts this full property for the returned sequence.

A heap contains mutable sequences, objects, typed collections, and named natural-number counters. A Call contract supplies a finite returning execution in the generated semantics for every caller stack. Runtime T is the increase in clockWork: each of seven Fibonacci-heap event counters and six Prim bookkeeping counters is counted once. This measures explicit source ticks, not elapsed time or integer bit complexity.

Formalization targets

The main target combines termination, minimum spanning tree correctness, preservation of existing caller storage, fresh output allocation, and a bound on the same execution's work. Its statement quantifies a single positive constant before every graph, root, and initial heap:

\exists C>0,\quad T\le C\bigl(E+V(\lfloor\log_2 V\rfloor+1)\bigr) \quad\text{for every valid connected input.}

The constant is independent of the input and its initial counter values. With E = 2m, this is the conventional $O(m+V\log V)$ bound. The logarithmic unit covers a graph containing only the root. The supporting reusable result retains the explicit estimate

T\le 23(E+1)+\bigl(12(2\lfloor\log_2 V\rfloor+2)+3\bigr)V.

FibonacciPrimAnalysis.correctness_and_running_time is the uniform-constant main result. FibonacciPrimAnalysis.summary provides the explicit bound and operation counts through prim_fibonacci.Call; runtimeBound and runtimeScale name the two expressions. The ordinary-output consequences are output_exists and output_with_cost_correct.

The component targets are the existing Fibonacci-heap correctness and amortized contract, the pure safe-edge and parent-tree results, the queue-independent Prim call contract, and their concrete composition. Invalid roots additionally return a fresh all-−1 sequence with zero ticks; no tree property is asserted for them.

What callers can reuse

The Fibonacci heap is reused from the Dijkstra formalization. This mission imports the same published implementation, shared definitions, correctness proofs, and amortized running-time contracts used by Dijkstra with a Fibonacci Heap. The existing heap contract keeps its original Prove2Me identity. Prim does not introduce a replacement heap or repeat its structural and amortized analysis; it proves the new algorithm-specific facts and composes them with that established contract. This reuse demonstrates how a verified data structure can support another algorithm without being formalized again.

The result lets a later algorithm invoke Prim on its current heap and receive a valid new parent sequence, an unchanged graph representation, unchanged preexisting sequences, objects, and typed collections, and a bound on the additional work. Initial counters need not be zero. The generic Prim theorem counts queue operations without depending on Fibonacci-heap internals; the concrete theorem discharges its queue assumptions using the existing published contract.

Prim's mathematical correctness and asymptotic complexity are established textbook results. The Algo2Lean development adds proofs about this actual mutable source program, including termination and storage preservation. Its complete Prim analysis has been checked locally under Lean 4.33.1. Prove2Me has accepted all four new Prim proofs, including the main correctness and running-time theorem, which reuses the already accepted Fibonacci-heap contract. The graph definitions are shared with the Kruskal analysis. Later clients can reuse these components without formalizing the data structure again. Alternative queue implementations and improvements to the explicit constants can retain the same mathematical specification.

Where the formalization is demanding

A minimum key alone does not establish that its parent pointer represents an input edge, that the chosen edges connect all vertices, or that their total weight is globally minimal. Those properties must remain connected to the mutable sequences that the source updates, including when weights tie or are negative.

A heap operation also changes shared mutable storage. Correct queue contents alone do not guarantee preservation of the graph or unrelated caller data. Moreover, some individual Fibonacci-heap operations are expensive despite small amortized budgets. The contract must account for the same evolving queue and counters across calls, rather than assume that every operation starts with an empty heap. These obligations distinguish the complete algorithm contract from a mathematical MST theorem or a count of queue calls.

Formalization scope and source

The .algo code closely follows the textbook pseudocode, with initialization, minimum extraction, and adjacency relaxation expressed as source operations and loops. It uses integer vertex handles and queues a vertex when first discovered. A parent of −1 denotes no discovered predecessor, so undiscovered keys require no artificial infinity. The root is selected before any edge is scanned. Relaxation compares an edge's weight directly; it does not add a path distance.

Inputs are finite linked adjacency lists with bounded endpoints and signed, unbounded integer weights. The theorem assumes a valid graph representation, symmetric adjacency, connectedness, and an in-range root. It assumes neither an existing successful transcript, a correct answer, nor an unverified queue-runtime estimate. The conclusion compares the result with every spanning forest. The whole-graph theorem does not apply to disconnected inputs.

The cost model counts the specified heap and Prim ticks. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Constant-sequence and queue construction add no ticks; constructing the input graph is outside the call. The imported queue API covers the insert/decrease, minimum extraction, and emptiness operations used here; meld and arbitrary deletion are outside this contract.

The compiler is Algo2Lean v0.1.4, whose immutable release commit is 0f79d5e. The Prim example and its proofs are versioned separately from this unchanged compiler release. Compiler-output reproduction and Prove2Me import packaging are separate checks: platform-adapted files need not have the raw generated files' hashes. The compiler does not yet have a formal semantics-preservation proof. The Prim source and proof guide identifies the exact statements, definitions, and source files. The separate example source commit is d832a565.

The project import root is examples. These are its three new source files. The other imports are the existing fibonacci_heap.algo and dijkstra/priority_queue.algo; the heap's independent source and analysis belong to the linked published component.

`prim/graph.algo`

# An undirected graph with integer edge weights. Each edge is stored in both
# adjacency lists. Negative weights, parallel edges, and self-loops are allowed.

class Edge:
    target: Int
    weight: Int
    next: Edge | None

    def __init__(self, target: Int, weight: Int, next: Edge | None) -> None:
        self.target = target
        self.weight = weight
        self.next = next


class Graph:
    size: Int
    heads: Seq[Edge | None]

    def __init__(self, size: Int) -> None:
        self.size = size
        if size < 0:
            self.size = 0
        self.heads = const(None)

    def add_edge(self, source: Int, target: Int, weight: Int) -> Bool:
        if source < 0 or source >= self.size or target < 0 or target >= self.size:
            return False
        self.heads[source] = Edge(target, weight, self.heads[source])
        self.heads[target] = Edge(source, weight, self.heads[target])
        return True

`prim/prim.algo`

from prim.graph import Graph, Edge
from dijkstra.priority_queue import PriorityQueue

# Prim's key is the cheapest edge from the growing tree to each vertex.
# parent stores the predecessor; -1 means no predecessor has been assigned.
# Vertices enter the queue when first reached, so infinity need not be encoded.
# The caller supplies an empty queue, zero keys and selected flags, and parents
# filled with -1. The root retains parent -1. Queue and client storage are disjoint.

def scan_edges(queue: PriorityQueue, key: Seq, parent: Seq, selected: Seq,
               vertex: Int, edge: Edge | None) -> None:
    # @scan
    while edge is not None:
        tick("edges")
        target = edge.target
        if selected[target] == 0:
            weight = edge.weight
            if parent[target] < 0 or weight < key[target]:
                # @improve
                key[target] = weight
                parent[target] = vertex
                tick("queue_updates")
                queue.push_or_decrease(target, weight)
                tick("improvements")
        edge = edge.next


def prim(graph: Graph, root: Int, queue: PriorityQueue,
         key: Seq, parent: Seq, selected: Seq) -> Seq:
    key[root] = 0
    tick("queue_updates")
    queue.push_or_decrease(root, 0)
    tick("queue_empty_checks")
    # @extract
    while not queue.is_empty():
        tick("queue_pops")
        vertex = queue.pop_min()
        selected[vertex] = 1
        tick("settlements")
        scan_edges(queue, key, parent, selected, vertex, graph.heads[vertex])
        tick("queue_empty_checks")
    return parent

`prim/prim_fibonacci.algo`

from prim.graph import Graph
from fibonacci_heap import FibonacciHeap
from prim.prim import prim as grow_tree

# On a connected graph, the returned predecessors describe a minimum spanning
# tree rooted at root. The root has predecessor -1. An invalid root returns -1
# everywhere without constructing a queue.
def prim_fibonacci(graph: Graph, root: Int) -> Seq:
    parent = const(-1)
    if root < 0 or root >= graph.size:
        return parent
    key = const(0)
    selected = const(0)
    queue = FibonacciHeap()
    return grow_tree(graph, root, queue, key, parent, selected)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 21, §§21.1–21.2, Theorem 21.1. Publisher.
The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 of the third edition, MIT Press, 2009/2022, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
Algo2Lean, version 0.1.4, Lean-targeting compiler and source examples. Compiler and source repository.
FibonacciQueueAnalysis.contracts, independently verified Fibonacci-heap queue behavior, preservation, and amortized work. Published Prove2Me theorem.

7 thms1 active userReviewed

Completed

Captain: lunjia

CLRS — Chapter 22, §22.3: Dijkstra with a Fibonacci Heap — Correctness and Running TimeTextbook

Prove2Me mission category: Textbook.

Reusable shortest-path algorithms

A shortest-path routine is often one component of a larger algorithm. Its useful contract must describe more than its returned numbers: it must also say that the routine terminates, preserves its caller's data, and incurs a bounded amount of work. Without these guarantees at a reusable boundary, each new caller must repeat parts of the implementation analysis.

This mission belongs to a series formalizing Introduction to Algorithms (CLRS), fourth edition. Its reference is Chapter 22, §22.3, Theorem 22.6, which establishes Dijkstra's correctness for nonnegative edge weights. The chosen queue is a Fibonacci heap, whose analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5 on degree. The fourth edition moved this material online; its printed Chapter 19 instead concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, program, and measured work

A directed weighted graph consists of a finite set of vertices and a finite list of weighted outgoing edges for each vertex. Here vertices are integers 0, …, V−1, and every weight is a nonnegative integer. The number E counts adjacency-list entries, so parallel edges are counted separately. A source is in range when 0 ≤ source < V.

The program returns a distance sequence: a mathematical function from integer indices to integers, stored through a mutable reference. Its value is −1 at an unreachable vertex and otherwise is the minimum sum of edge weights over paths from the source. It uses a mutable Fibonacci heap to maintain unsettled vertices and their current distance estimates. A new vertex is inserted; a better estimate decreases its existing key.

A heap records the program's mutable arrays, objects, typed collections, and named natural-number counters. A Call contract relates the initial and final heap in the generated execution model: for every caller stack it supplies a finite execution returning the same final heap and result. The reusable theorem gives one such final state with all correctness, preservation, and cost properties together. The runtime T is the change in the sum of seven heap-event counters and six graph-algorithm counters. It measures the explicitly instrumented source operations, rather than elapsed time or integer bit complexity.

Formalization targets

The main correctness-and-running-time theorem has an accepted proof on Prove2Me under Lean 4.33.1.

The capstone target is one reusable contract giving termination, shortest distances, protected caller storage, a fresh result reference, and a total work bound for the same execution. Its main statement quantifies one positive constant before all graph, heap and source inputs:

\exists C>0,\quad T \le C\bigl(E+V(\lfloor\log_2 V\rfloor+1)\bigr) \quad\text{for every valid input.}

Thus different proofs may provide different constants without changing the main proposition. The constant cannot depend on the graph or its initial heap. This states the familiar $O(E+V\log V)$ scale while covering small instances. The published Lean statement includes an additional constant $1$ in its runtimeScale. A valid source requires $V\ge1$ , so this displayed form absorbs that term into the unspecified constant, at most doubling it. The reusable supporting result retains the explicit estimate

T \le 23(E+1) + \bigl(12(2\lfloor\log_2 V\rfloor+2)+3\bigr)V \qquad (V\ge1).

The explicit supporting declaration is FibonacciDijkstraAnalysis.summary; its ordinary-output consequence is output_with_cost_correct. Its named runtimeBound has fixed coefficients. The main proposition is a separate corollary that hides those coefficients and retains the same termination, correctness, allocation, preservation and actual-call guarantees.

The component milestones are the independently verified Fibonacci-heap contract, the generic priority-queue Dijkstra contract, and their concrete composition. The heap milestone includes correct insertion of an absent in-range handle or strict decrease of a present key, extraction from a nonempty represented queue, preservation, and constant/logarithmic amortized budgets. Clients maintain the heap representation and the required separation from protected storage. The generic milestone includes shortest distances and counts of queue and edge operations. The concrete milestone removes abstract queue assumptions by using the verified heap. Invalid sources additionally terminate with a fresh all-−1 result and no ticks.

What clients receive

A verified client can call this implementation and immediately use the resulting distance sequence in another algorithm. It receives the graph representation unchanged, all previously allocated sequences, objects, and typed collections unchanged, a valid newly allocated result, and a bound on the work added to arbitrary initial counters. The result is useful for nested calls: the surrounding computation need not restart its clocks or forget its existing heap.

The mathematical algorithm and its asymptotic bound are established textbook results, not new open problems. The Algo2Lean source development contains the correctness, termination, preservation, and runtime proofs. The complete source project and exact submission files have been checked locally under Lean 4.33.1. This mission presents those proofs as importable definition and theorem nodes, with the source program displayed alongside the generated execution semantics. Future contributions can reuse the heap independently, instantiate the generic queue boundary with another implementation, or improve explicit bounds without redoing the complete graph proof.

Where the formalization is demanding

A heap operation changes a shared mutable representation. Correct abstract queue contents alone do not establish that graph storage survived, that an array reference remains allocated, or that the cost argument describes the same execution as the correctness argument. The contract must connect all these facts rather than leave them as independent assumptions.

Fibonacci heaps also have expensive individual calls despite small amortized budgets. A worst-case bound applied separately to every decrease-key loses the intended running time. The reusable boundary must therefore describe the potential of the evolving queue, not a fresh empty queue for each operation. The generic Dijkstra result must remain independent of the internal tree and pointer representation of its chosen heap.

Formalization scope and source

The .algo code closely follows the textbook pseudocode: initialization, minimum extraction, and adjacency relaxation appear as explicit source loops and operations. Representation choices are made explicit: -1 denotes infinity, flags record settled vertices, and only discovered vertices enter the queue. The routine returns distances without a predecessor tree. Thus it preserves the textbook's shortest-distance algorithm for nonnegative weights, while differing from its all-vertices initial queue and literal notation.

The Lean representation includes finite adjacency lists stored as linked Edge objects, a Graph with typed heads, unbounded mathematical integers, and mutable sequences indexed by every integer. Zero-weight edges, self-loops, parallel edges, and shared adjacency suffixes are allowed. The theorem assumes a valid finite graph representation and an in-range source for its shortest-distance claim. It does not assume the desired distances, a pre-existing execution transcript, or an unverified queue-runtime bound.

The cost model sums the stated named ticks over unbounded mathematical integers and total sequences. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Queue and constant-sequence construction add no ticks; input-graph construction is outside the call being analyzed. The independent queue API covers the operations used here, not heap meld or arbitrary deletion.

The compiler is Algo2Lean v0.1.4, at release commit 0f79d5e. The downloaded website compiler reproduces all 15 generated modules for this project exactly; the manifests identify the compiler and every source file. Byte-for-byte reproduction concerns unmodified compiler output. The Prove2Me transplant separately rewrites module imports/names, declaration packaging, and explicit options as required by the platform; its adapted files are not claimed to have the raw output's hashes. The edits and source mapping are recorded, the adapted dependency closure has been checked, and every theorem's elaborated type matches the original. The supplementary analysis archive contains the uniform-constant capstone, a reproducible source build, and an independent statement readback. The handwritten libraries include shortest-path mathematics, finite execution and call composition, heap representation, Fibonacci-heap operations, and reusable queue contracts. These boundaries are intended for later CLRS formalizations. The compiler itself is not yet equipped with a formal semantics-preservation proof.

The project import root is examples. The entry file is dijkstra/dijkstra_fibonacci.algo:

from graph import Graph
from fibonacci_heap import FibonacciHeap
from dijkstra.dijkstra import dijkstra as search

# Construct a Fibonacci heap and bind its operations to generic Dijkstra.
def dijkstra_fibonacci(graph: Graph, source: Int) -> Seq:
    distance = const(-1)
    if source < 0 or source >= graph.size:
        return distance
    settled = const(0)
    queue = FibonacciHeap()
    return search(graph, source, queue, distance, settled)

The companion algorithm description displays the complete five-file source: graph.algo, fibonacci_heap.algo, dijkstra/priority_queue.algo, dijkstra/dijkstra.algo, and this entry wrapper. The Fibonacci-heap component also displays its independent source. Improvements to exposed contracts, client examples, and source-level cost models are welcome when they preserve the stated semantics and remain separately checkable.

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 22, §22.3, Theorem 22.6. Publisher.
The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 from the third edition, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
Algo2Lean, version 0.1.4, compiler and source semantics. Compiler and source repository.

7 thms1 active userReviewed

Completed

Probability·Captain: YY

Appendix E — Randomized AC0 Sampling of Regular Languages and Markov ChainsResearch Paper

Motivation

Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe allowable executions and when parallel generation should avoid a sequential pass through every transition. The source paper establishes constant-depth sampling results for regular languages and finite Markov chains in Appendix E (Zhang et al., 2026).

The mission concerns that appendix's finite-state sampling results. It formalizes all six numbered results E.1–E.6, together with the seed bounds stated in the surrounding text. Each milestone points to a published theorem with a separately checked proof. The objects to sample are complete words, word–acceptance pairs, and complete state trajectories. Sampling only the final state would lose the joint temporal information required by the targets.

Finite-state models and fair-bit circuits

A binary deterministic finite automaton has finitely many states, a designated start state, a transition for each state and bit, and a set of accepting states. Starting from its initial state, a binary word of length $n$ determines a run. Let $L$ be the set of words whose final state is accepting. Put $L_n=L\cap\{0,1\}^n$ . An arbitrary such automaton represents an arbitrary binary regular language, with no assumption that membership belongs to $\mathrm{AC}^0$ .

A finite Markov chain consists of a nonempty finite state set $Q$ , an initial probability vector $\mu$ , and a row-stochastic transition matrix $P$ . Entries are nonnegative real numbers, not restricted to rational numbers. For $\gamma=(x_0,\ldots,x_n)$ , its probability is $p_M(\gamma)=\mu(x_0)\prod_{i=1}^{n}P(x_{i-1},x_i)$ . The distribution of all $n+1$ states is denoted $\mathrm{Path}_n(M)$ . For $F\subseteq Q$ , conditioning is allowed when the probability that $X_n\in F$ is positive.

A randomized $\mathrm{AC}^0$ sampler is a deterministic Boolean circuit supplied with independent, unbiased random bits. AND and OR gates have unbounded fan-in; NOT gates and Boolean constants are permitted. Its size is polynomial and its depth has a constant bound independent of trajectory length. Approximate families are nonuniform in both $n$ and their real error tolerance $\epsilon$ : existence does not require efficiently computing circuit descriptions or numerical tables from a supplied transition matrix.

Formalization targets

The main goal is the conjunction of all results E.1–E.6, including the linear seed guarantee for E.5. This organizational theorem is not an additional numbered result attributed to the paper. All six milestones must be proved for the goal to hold. The exact Markov sampling criterion in Theorem E.5 is one component. A nonnegative real number is dyadic if it equals $a/2^k$ for natural numbers $a,k$ , including zero. A chain is path-dyadic when every finite trajectory, including a trajectory of length zero, has a dyadic probability. The target is

\mathrm{Path}_n(M)\text{ has an exact randomized }\mathrm{AC}^0\text{ sampler family} \quad\Longleftrightarrow\quad \forall n\geq0\;\forall\gamma\in Q^{n+1},\ p_M(\gamma)\text{ is dyadic}.

On the left, the family has polynomial size in $n+1$ and depth bounded independently of $n$ . A supporting target records the linear fair-bit budget $O_M(n+1)$ when path-dyadicity holds. Lemma E.4 supplies another target: every path-dyadic chain is the coordinatewise projection of a finite chain whose initial and transition probabilities are all dyadic. Path-dyadicity must not be replaced by the stronger requirement that the original transition matrix itself be dyadic (Appendix E.3).

Theorem E.1 concerns exact sampling of a uniformly random word together with its acceptance indicator:

(X,\mathbf 1[X\in L]),\qquad X\sim\operatorname{Unif}(\{0,1\}^n).

The sampler uses exactly $n$ fair bits, polynomial size, and depth depending only on the fixed automaton. This is a sampling assertion and does not assert that membership can be computed in constant depth on an arbitrary externally supplied word.

Theorem E.2 concerns the uniform law on nonempty $L_n$ . For every $0<\epsilon\leq1/2$ , the target is

d_{\mathrm{TV}}(Q_{n,\epsilon},\operatorname{Unif}(L_n))\leq\epsilon, \qquad r_{n,\epsilon}\leq n+C_L\log_2(1/\epsilon).

Every possible output is accepted. Size is polynomial in $n+1$ and $1/\epsilon$ , and depth depends only on the fixed language or its automaton. In particular, the leading coefficient of the $n$ term in the random-bit bound is one (Appendix E.2).

Theorem E.6 is the corresponding approximate target for trajectories conditioned on $X_n\in F$ . It requires total variation error at most $\epsilon$ , only positive-probability outputs ending in $F$ , $O_M(n+\log(1/\epsilon))$ fair bits, polynomial size in $n+1$ and $1/\epsilon$ , and depth depending only on the chain. There is no lower bound on the conditioning probability beyond strict positivity (Appendix E.4).

Lemma E.3 supplies the exact representation used in the Markov construction. A transition-dyadic chain is represented by one binary DFA and a fixed state projection. On a uniform input of length $v+ns$ , with positive constants $v,s$ , the states observed after $v,v+s,\ldots,v+ns$ bits project to exactly the complete trajectory law of the chain. The same DFA and projection work for every length, including zero.

Significance of the targets

These results separate sampling an input together with its finite-state behavior from computing that behavior on a prescribed input. They also identify a precise obstruction to exact sampling with a finite fair-bit seed: each output probability must be dyadic. Approximate sampling allows arbitrary real transition probabilities while retaining the valid trajectory support. The complete trajectory requirement preserves correlations among all time coordinates.

The formalization makes the circuit model, seed accounting, support guarantees and asymptotic quantifiers explicit and reusable. The theorem statements and their separately submitted proofs have passed the platform verifier. The goal proof imports all six milestones; its E.5 milestone in turn imports both the equivalence and the linear seed theorem. Thus the platform dependency graph covers the entire appendix. Platform verification establishes the formal statements; semantic correspondence is documented in the statement descriptions and source references.

Difficulty

A literal step-by-step implementation of a run makes circuit depth grow with $n$ , so it does not meet the constant-depth target. Recognition results alone do not furnish the required joint sampler. For approximate word sampling, an error estimate alone is insufficient: the output must remain in the accepted support, and the coefficient-one seed bound must also hold. For exact Markov sampling, unreachable states and non-dyadic individual transitions prevent identifying the desired criterion with entrywise dyadicity. Conditioning on a rare terminal event must not introduce an unstated dependence on its probability.

Formalization scope

States are indexed by finite types $\mathrm{Fin}(q)$ . Binary words have type $\mathrm{Fin}(n)\to\mathrm{Bool}$ ; trajectories have $n+1$ coordinates. Markov vectors and matrices are real-valued and carry normalization and nonnegativity proofs. Sampling probabilities are defined by counting all seeds that give a particular encoded outcome and dividing by $2^r$ . Total variation is half the finite sum of absolute probability differences.

The circuit representation is an explicit topologically ordered gate list with checked wire references. Size counts input bits, gates, gate-input wires and output wires; this yields the usual polynomial-size class. State trajectories use a fixed one-hot encoding at each time coordinate. The invalid-output predicate is checked over every seed, so neither arbitrary decoders nor unrepresented outcomes can satisfy an exact or support-preserving claim. The encodings used by the targets are injective. The circuit family is existentially quantified after the fixed finite-state model; the depth and polynomial constants precede $n$ and $\epsilon$ .

Zero-length words and zero-transition Markov paths are included. The word target excludes empty accepted slices. The conditioned target excludes zero-probability conditioning events. Definitions of division by zero still exist as total Lean functions, but the hypotheses exclude those cases from approximate claims. Extensions of these results, reusable finite-state probability lemmas, and further circuit constructions are welcome. No sampler-existence axiom, vacuous model or final-state-only replacement is part of the interface.

Selected references

Jiarui Zhang, Chengwei Liang, Haozhe Jiang, Binhang Yuan and Jingzhao Zhang. Revision Provably Reduces Sequential Computation in Diffusion Language Models. Zenodo preprint, 2026. DOI 10.5281/zenodo.23105365, Appendix E, Theorems E.1, E.2, E.5, E.6 and Lemmas E.3, E.4, printed pages 33–36.

10 thms1 active userReviewed

Analysis Operations Research·Captain: mikedeng1

Online Stochastic Matching: New Algorithms with Better Bounds 2: The Per-Advertiser Inequality Behind the 0.706 Ratio for General Arrival Rates, in the Limit f − s ≤ 1 − ln 2Research Paper

Motivation

Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set $A$ of advertisers to a set $I$ of impression types; $n$ requests arrive, each of a type drawn independently with $\mathbb P(\text{type } i) = r_i/n$ , and each request must be assigned at once and irrevocably to an unmatched interested advertiser, or dropped. Performance is measured by the competitive ratio $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}]$ , where OPT is the maximum matching of the realized graph.

Without distributional knowledge the best possible ratio is $1 - 1/e$ (Karp, Vazirani and Vazirani, 1990). Knowing the type distribution allows more:

Feldman, Mehta, Mirrokni and Muthukrishnan (2009) first beat $1 - 1/e$ , with $0.670$ , when every arrival rate is integral; Bahmani and Kapralov improved this to $0.699$ .
Manshadi, Oveis Gharan and Saberi (2011) obtained $0.705$ for integral rates and $0.702$ for general arrival rates, using offline statistics drawn by sampling.
Jaillet and Lu (2014) introduced Random Lists Algorithms with modified LPs and obtained $1 - 2e^{-2} \approx 0.729$ for integral rates (Theorem 1), $0.725$ for vertex weights (Theorem 2) and $0.706$ for general rates (Theorem 3).

This mission concerns the analytic core of Theorem 3, the general-rates bound.

Setting

For an advertiser $a$ , let $f = f_a \le 1$ be the LP flow into $a$ . Its neighbours $a_1 \in A^*_a$ , which include a dummy advertiser $a_d$ with $f_{a_d} = 1$ , are indexed by $j = 1, \dots, k$ . For each neighbour, $x_j = m_{a,a_1} = m_{a_1,a} \ge 0$ is the expected number of random lists $\langle a, a_1\rangle$ , and $y_j = f_{a_1} \le 1$ is the neighbour's flow, so that $x_j \le y_j$ . Write $s = \sum_j x_j \le f$ and $\beta = \max_j x_j$ .

Claim 2 of the paper introduces the functions

h(y,x)=\begin{cases}\dfrac{y}{y-x}\bigl(e^{-x}-e^{-y}\bigr), & x\ne y,\\[4pt] y\,e^{-y}, & x=y,\end{cases}\qquad g(y,x)=h(y,0)-h(y,x),

where $g(f_{a_1}, m_{a_1,a})$ is the probability that $a$ is matched through a list headed by $a_1$ . The per-advertiser bracket is

B(f;x,y)=1-e^{-f}+\frac1e\sum_j g(f,x_j)-\frac1{2e}\Bigl(\sum_j g(y_j,x_j)\Bigr)^2+\frac1{2e}\sum_j g(f,x_j)^2,

and the reduced function of three variables is

R(f,\beta,s)=\frac1f\Bigl(1-e^{-f}+\frac1e\frac{s}{\beta}g(f,\beta)-\frac1{2e}\bigl(e^{-1}(s-\beta)+g(1,\beta)\bigr)^2+\frac1{2e}g(f,\beta)^2\Bigr).

In Lean these are h, g, bracket f x y and R f β s in RandomListsMatching.GeneralRates.

Formalization targets

Goal: the per-advertiser bound

For $0 < f \le 1$ , any $k \ge 0$ and reals with $0 \le x_j \le y_j \le 1$ , $s = \sum_j x_j \le f$ and $f - s \le 1 - \ln 2$ ,

\frac{B(f;x,y)}{f} \ge 0.706 .

The paper bounds $\sum_a p_a / \sum_a f_a$ below by $\min_a B(f_a; \cdot)/f_a$ (p. 15), so this inequality is the whole of what Theorem 3's numerical constant rests on.

Milestones

Claim 3 (three clauses, p. 15): for $y \in [0,1]$ , $h(y,\cdot)$ is convex and decreasing on $[0,y]$ and $g(y,\cdot)$ is concave and increasing on $[0,y]$ ; for $x \ge 0$ , $g(\cdot, x)$ is increasing on $[x,\infty)$ .
Inequality (5), analytic part (p. 15): for $0 \le x \le y \le 1$ , $h(y,0)-h(y,x) \le -x\,\partial_2 h(y,0) \le e^{-1}x$ .
Chord bound (p. 15): $\sum_j g(f,x_j) \ge (s/\beta)\, g(f,\beta)$ .
Cross-sum bound (p. 15): $\sum_j g(y_j,x_j) \le e^{-1}(s-\beta) + g(1,\beta)$ .
Reduction (p. 15): $B(f;x,y)/f \ge R(f,\beta,s)$ when $\beta > 0$ .
Claim 4, corrected (p. 16): $R(f,\beta,s) \ge 0.706$ on $1 \ge f \ge s \ge \beta > 0$ , $f - s \le 1 - \ln 2$ .

Significance

The result. Theorem 3 gives $0.706$ for online stochastic matching with general (non-integral) arrival rates, improving the $0.702$ of Manshadi et al. The probabilistic half of its proof reduces matching probabilities to the closed forms $h$ and $g$ ; the paper then states that "in the remaining part of the section, we only use algebraic manipulations and the following properties of functions $g$ and $h$ ". That remaining part, posed here, is an exact real inequality, and it is where the constant $0.706$ is decided.

Formalizing it. The paper proves Claim 3 in one line ("can be easily verified by taking first and second order partial derivatives") and Claim 4 by a grid computation over cubes of side $0.001$ , with no recorded error analysis. A machine-checked proof replaces both. It also settles the regime of the constant: Claim 4 as printed, with the constraint $f - s \le (1 - \ln 2) + 1/n$ "for $n \ge 100$ ", is false, and the bound holds in the limit form stated here. None of these statements has a formal proof anywhere, to the extent of the search made for this mission.

Difficulty

The margin is small. The minimum of $R$ over the feasible region is about $0.706028$ , attained near $(f,\beta,s) = (1, 0.565, \ln 2)$ on the boundary $f - s = 1 - \ln 2$ ; the margin over $0.706$ is under $3 \cdot 10^{-5}$ . Any argument that loses a constant factor in the estimates of $e^{-x}$ , or replaces $\ln 2$ by a rational bound that is not tight to five digits, fails. The bound is a three-variable statement with the minimum on a boundary face, so a one-variable monotonicity argument does not settle it.

The second difficulty is the function $h$ itself. Its two-case definition is continuous but the quotient form has a removable singularity at $x = y$ , which is exactly the end of the interval $[0, y]$ on which Claim 3 asserts convexity and concavity. Derivative computations that are routine away from the diagonal need care there.

The natural first idea for the goal, to apply Claim 4 directly to the bracket, does not type-check: the bracket depends on the whole family $(x_j, y_j)$ , and the reduction to three variables through the chord and cross-sum bounds is a separate step.

Formalization scope

All quantities are real numbers. $e$ is Real.exp 1, $\ln 2$ is Real.log 2, and $0.706$ is the exact rational (0.706 : ℝ).
$h$ keeps the paper's case split at $x = y$ . The neighbour family is indexed by Fin k, and $k = 0$ is allowed.
"Increasing" and "decreasing" are non-strict (MonotoneOn, AntitoneOn); convexity is ConvexOn ℝ (Set.Icc 0 y). The derivative in (5) is deriv (fun t => h y t) 0, the derivative in the second argument; the page's $\partial h/\partial y$ is a slip.
Pinned hypotheses. The goal requires $f > 0$ (an advertiser with $f_a = 0$ contributes $0/0$ in the paper and $0$ in Lean). Claim 4 and the reduction require $\beta > 0$ , because $s/\beta$ is $0$ in Lean at $\beta = 0$ and $R(1,0,1) \approx 0.607$ ; in the paper $\beta = 0$ forces $s = 0$ , a case the goal covers directly. The hypotheses $x_j \le y_j \le 1$ are the paper's $m_{a_1,a} \le s_{a_1} \le f_{a_1} \le 1$ .
Claim 4 is corrected. As printed it is false: at $n = 100$ , $(f,\beta,s) = (1, 0.55886, \ln 2 - 0.01)$ meets the printed constraints and gives $R \approx 0.70521$ . The goal fails at $n = 100$ as well (about $0.70543$ ). Both are stated in the limit $f - s \le 1 - \ln 2$ , the regime in which the paper claims Theorem 3 (" $n$ is large enough so that a factor of $1 + O(1/n)$ is negligible", p. 6). The constant $0.706$ is unchanged.
Out of scope. Theorem 3 itself, LP (4), the list construction of §5.3, Claim 2 and the bound on $p_a$ are not posed. They rest on " $\approx$ " replacements of binomial sums and on an asymptotic independence whose proof "is omitted in the paper", so they have no exact finite- $n$ statement.
No trivializing reading. The goal's hypotheses are met, for example, by $k = 1$ , $f = 1$ , $x_1 = 0.7$ , $y_1 = 1$ , and the conclusion is not vacuous there. Its hypotheses do not exclude the minimizer, and the division by $f$ is guarded.

A complete development needs the derivative calculus of $h$ on $[0,y]$ , including the diagonal, and certified interval bounds for $e^{-x}$ and $\ln 2$ . The latter is reusable well beyond this mission. Proofs of Claim 3 or Claim 4 alone are welcome contributions.

Selected references

P. Jaillet and X. Lu, Online Stochastic Matching: New Algorithms with Better Bounds, Mathematics of Operations Research, 2014; authors' accepted manuscript, rev. June 2013. https://doi.org/10.1287/moor.2013.0621
V. H. Manshadi, S. Oveis Gharan and A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, Mathematics of Operations Research 37(4):559–573, 2012. https://doi.org/10.1287/moor.1120.0551
J. Feldman, A. Mehta, V. Mirrokni and S. Muthukrishnan, Online Stochastic Matching: Beating 1 − 1/e, FOCS 2009, pp. 117–126. https://arxiv.org/abs/0905.4100
R. M. Karp, U. V. Vazirani and V. V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990, pp. 352–358. https://doi.org/10.1145/100216.100262

10 thms1 active userReviewed

Combinatorics Operations Research Probability·Captain: mikedeng1

Online Stochastic Matching: New Algorithms with Better Bounds 1: Every Random-Lists Algorithm Has ALG/OPT ≥ E[ALG]/E[OPT] − 2ε/(c+ε) with Probability at Least 1 − 2exp(−2nε²)Research Paper

Motivation

Online bipartite matching with stochastic arrivals models the assignment of display-advertising impressions to advertisers: requests arrive one at a time, each must be assigned irrevocably on arrival or dropped, and the arrival sequence is random rather than adversarial. Since Feldman, Mehta, Mirrokni and Muthukrishnan beat the $1 - 1/e$ barrier in the i.i.d. arrival model (FOCS 2009), a line of work has designed algorithms with better guarantees. Jaillet and Lu (Math. Oper. Res. 2014) introduce a whole class of such algorithms, the Random Lists Algorithms, and obtain ratios $0.729$ , $0.725$ and $0.706$ for integral arrival rates, vertex weights and general arrival rates.

Two notions of performance coexist in this literature. One compares expectations, $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}]$ ; the other asks that $\mathrm{ALG}/\mathrm{OPT}$ be large on most realizations, as in Feldman et al. Section 2 of Jaillet and Lu shows that, for every algorithm of their class, the two notions are quantitatively linked by an explicit exponential tail bound. This mission formalizes that section.

Setting

A bipartite graph $G = \{A \cup I, E\}$ has a finite set $A$ of advertisers, a set $I$ of impression types, and edges $E \subseteq A \times I$ ; $(a, i) \in E$ means advertiser $a$ is interested in type $i$ . A fixed number $n$ of requests arrive at periods $1, \dots, n$ , and their types are drawn i.i.d. from a known distribution on $I$ . Every advertiser can receive at most one request.

A list for type $i$ is an ordered sequence of advertisers interested in $i$ . A Random Lists Algorithm fixes, for each type $i$ , a distribution $\mathcal D_i$ over lists (constructed from an LP solution; the construction is irrelevant here). When a request of type $i$ arrives it draws a list from $\mathcal D_i$ and assigns the request to the first advertiser on the list not yet matched, or drops it if every listed advertiser is matched.

Formally, each request carries an outcome $x$ in a finite set $\mathcal X$ determining its type $\mathrm{typ}(x)$ and its list $\mathrm{lst}(x)$ ; outcomes $\omega_1, \dots, \omega_n$ are i.i.d. with law $\nu$ . Starting from $W_0 = \emptyset$ , the set $W_j$ of matched advertisers after the $j$ -th request is obtained from $W_{j-1}$ by adding the first advertiser of $\mathrm{lst}(\omega_j)$ outside $W_{j-1}$ , if any. Then:

$\mathrm{ALG}(\omega) = |W_n|$ , the number of assigned requests;
$\mathrm{OPT}(\omega)$ is the cardinality of a maximum matching of the realized graph, in which request $j$ may go to $a$ iff $(a, \mathrm{typ}(\omega_j)) \in E$ ;
$\mathbb E[\mathrm{ALG}]$ , $\mathbb E[\mathrm{OPT}]$ are expectations under $\nu^{\otimes n}$ , and $c = \mathbb E[\mathrm{OPT}]/n$ .

Formalization targets

Goal: the concluding display of Section 2 (p. 6)

If every list contains only interested advertisers, then for every $n \ge 1$ and every $\epsilon > 0$ ,

\mathbb P\left(\frac{\mathrm{ALG}}{\mathrm{OPT}} \ge \frac{\mathbb E[\mathrm{ALG}]}{\mathbb E[\mathrm{OPT}]} - \frac{2\epsilon}{c + \epsilon}\right) \ge 1 - 2\exp(-2n\epsilon^2).

It holds for every instance and every law $\nu$ , with no assumption on the size of $\mathbb E[\mathrm{OPT}]$ .

Milestones

Claim 1 (p. 5). If two list sequences differ in one position, the cardinalities of the resulting matchings differ by at most one.
Lemma 1 (p. 5). $\mathbb P(\mathrm{ALG} - \mathbb E[\mathrm{ALG}] < -n\epsilon) \le \exp(-2n\epsilon^2)$ .
Lemma 2 (p. 5). $\mathbb P(\mathrm{OPT} - \mathbb E[\mathrm{OPT}] > n\epsilon) \le \exp(-2n\epsilon^2)$ .

A supporting theorem, not a milestone, records the fact the display uses without stating it: with interested lists, $\mathrm{ALG} \le \mathrm{OPT}$ on every realization.

Significance

The display shows that the paper's guarantees, proved for the ratio of expectations, transfer to realizations: when $\mathbb E[\mathrm{OPT}] = \Theta(n)$ , $\mathrm{ALG}/\mathrm{OPT}$ is at least $\mathbb E[\mathrm{ALG}]/\mathbb E[\mathrm{OPT}] - O(\epsilon)$ except with probability $2e^{-2n\epsilon^2}$ . It applies uniformly to the whole class of Random Lists Algorithms, whatever the LP and the list distributions, so it covers each of the paper's later algorithms at once.

The result is proved in the paper; nothing about it is open. It has no machine-checked proof. Formalizing it produces a precise model of list-based online matching (the greedy run, the realization-graph optimum, the joint type–list law) that later formalizations of the paper's competitive ratios can build on, and a worked application of the bounded-differences method to a combinatorial online algorithm.

Difficulty

The concluding display is elementary once Lemmas 1 and 2 are available. The two lemmas need McDiarmid's bounded-differences inequality in one-sided form, which Mathlib does not provide, and the bounded-difference properties of ALG and OPT.

Claim 1 is the step where the naive argument fails. Changing one list can change the assignment of every later request, so ALG is not a sum of local contributions, and a single changed list could a priori cascade into many changed assignments; the claim asserts that the cascade never changes the total by more than one. The analogous property for OPT (changing one request's type moves the maximum matching by at most one) is used in Lemma 2's proof but is not stated in the paper.

Formalization scope

Arrivals. Outcomes live in a finite type $\mathcal X$ with the discrete σ-algebra, and the law of the arrivals is the product measure $\nu^{\otimes n}$ (Measure.pi). Any joint law of type and list is allowed; every Random Lists Algorithm is the case $\mathcal X = \{(i, l)\}$ , $\nu(i, l) = p_i\,\mathcal D_i(l)$ . Types and lists are not modelled as independent sequences, which would break $\mathrm{ALG} \le \mathrm{OPT}$ .
Expectations are Bochner integrals of functions on the finite space $\mathcal X^n$ , hence honest finite sums.
Matchings. OPT is the maximum size of a partial assignment Fin n → Option A that uses only edges and gives each advertiser at most one request; the empty assignment qualifies, so the maximum is over a nonempty set. ALG is $|W_n|$ for the greedy recursion.
Pinned hypotheses. The goal assumes $n \ge 1$ (the paper's $c = \mathbb E[\mathrm{OPT}]/n$ ) and that every list only contains interested advertisers (stated in §2, p. 5). Claim 1 and Lemma 1 hold for arbitrary lists and carry neither hypothesis. Lists need not be nonempty or repetition-free.
Division by zero. No hypothesis $\mathbb E[\mathrm{OPT}] > 0$ or $\mathrm{OPT} > 0$ is made. On realizations with $\mathrm{OPT} = 0$ , and when $\mathbb E[\mathrm{OPT}] = 0$ , Lean's $x/0 = 0$ applies; the statement remains true under it, and adding a positivity hypothesis would weaken the result.
Not posed. Theorems 1–3 (the competitive ratios, which hold up to $1 + O(1/n)$ ) and the LP constructions of the algorithms are out of scope. McDiarmid's inequality is a proof tool, not an item. A one-sided version is posed elsewhere on the platform and not yet proved.

Contributions welcome: a one-sided McDiarmid inequality for Measure.pi (reusable well beyond this mission), the bounded-difference property of maximum bipartite matchings, and Claim 1.

Selected references

P. Jaillet and X. Lu, Online Stochastic Matching: New Algorithms with Better Bounds, Mathematics of Operations Research 39(3), 2014; accepted manuscript, rev. June 2013. https://doi.org/10.1287/moor.2013.0621
J. Feldman, A. Mehta, V. Mirrokni and S. Muthukrishnan, Online Stochastic Matching: Beating 1 − 1/e, FOCS 2009. https://arxiv.org/abs/0905.4100
C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, London Math. Soc. Lecture Note Series 141, 1989. https://doi.org/10.1017/CBO9781107359949.008

5 thms1 active userReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-Dependent Competitive Ratios II: In the Deterministic Case Multi-price Ranking Is minᵢ F(𝒫ᵢ)-CompetitiveResearch Paper

Motivation

Online matching models a platform that must commit resources to requests as they arrive, without knowing the future. In revenue management the resources are items in limited supply and the requests are customers, and the firm also chooses the price. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020, DOI 10.1287/opre.2019.1957) give algorithms whose worst-case guarantee depends on the set of prices each item can be sold at, and show that the guarantee is tight.

Timeline of the deterministic (matching) case:

1990. Karp, Vazirani and Vazirani introduce RANKING for unweighted online bipartite matching: each item gets a random rank, and each arriving customer takes the best-ranked available neighbour. Its competitive ratio is $1-1/e$ , which is optimal.
2011. Aggarwal, Goel, Karande and Mehta extend RANKING to vertex-weighted matching, where each item has a single fixed price, with the same ratio $1-1/e$ .
2013. Devanur, Jain and Kleinberg give a randomized primal–dual proof of these results with continuous seeds $W_i\sim U[0,1]$ .
2019. Ma and Simchi-Levi allow each item a set of prices. Their Multi-price Ranking ranks items by a price-dependent value function, and it is $\min_iF(\mathcal P_i)$ -competitive. $F(\mathcal P)$ depends only on the ratios of the prices; it equals $1-1/e$ for one price and lies in $[1-e^{-1/m},1-1/e]$ for $m$ prices (p. 14).

Setting

A firm sells $n$ items, one unit of each. Item $i$ has a price set $\mathcal P_i=\{r_i^{(1)}<\dots<r_i^{(m_i)}\}$ with $r_i^{(1)}>0$ , and $r_i^{(0)}:=0$ . Customers $t=1,\dots,T$ arrive one at a time. In the deterministic case, customer $t$ either would or would not buy item $i$ at price $j$ : $p^{(j)}_{t,i}\in\{0,1\}$ . Let $j_{t,i}$ be the largest $j$ with $p^{(j)}_{t,i}=1$ , or $0$ if there is none. Assigning item $i$ to customer $t$ earns $r_i^{(j_{t,i})}$ . An online algorithm sees $p_{t}$ only when customer $t$ arrives.

The benchmark is the LP (5): maximize $\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}$ subject to $\sum_{t,j}p^{(j)}_{t,i}x^{(j)}_{t,i}\le k_i$ , $\sum_{i,j}x^{(j)}_{t,i}\le1$ and $x\ge0$ , with optimal value $\mathrm{OPT}$ . Its dual (19) minimizes $\sum_ik_iy_i+\sum_tz_t$ subject to $p^{(j)}_{t,i}y_i+z_t\ge p^{(j)}_{t,i}r_i^{(j)}$ and $y,z\ge0$ . An algorithm is $c$ -competitive if $\mathbb E[\mathrm{ALG}]\ge c\cdot\mathrm{OPT}$ for every arrival sequence.

Booking limits. By Proposition 1 there are unique positive $\alpha^{(1)},\dots,\alpha^{(m)}$ that sum to $1$ and satisfy

1-e^{-\alpha^{(1)}}=\frac{1-e^{-\alpha^{(j)}}}{1-r^{(j-1)}/r^{(j)}}\quad (j=2,\dots,m).

Set $F(\mathcal P)=1-e^{-\alpha^{(1)}}$ and $L^{(j)}=\alpha^{(1)}+\dots+\alpha^{(j)}$ . For $w\in[0,1]$ let $\ell(w)$ be the segment containing $w$ . The value function is

\Phi_{\mathcal P}(w)=r^{(\ell-1)}+\bigl(r^{(\ell)}-r^{(\ell-1)}\bigr)\frac{e^{\,w-L^{(\ell-1)}}-1}{e^{\alpha^{(\ell)}}-1},\qquad \ell=\ell(w).

It increases continuously from $0$ to $r^{(m)}$ and equals $r^{(j)}$ at $L^{(j)}$ .

Multi-price Ranking (Algorithm 2). Each item draws an independent seed $W_i\sim U[0,1]$ . Customer $t$ is assigned an available item maximizing $r_i^{(j_{t,i})}-\Phi_{\mathcal P_i}(W_i)$ , provided the maximum is strictly positive. Ties are broken arbitrarily. The analysis uses dual variables: when $i$ is assigned to $t$ , $Z_t=r_i^{(j_{t,i})}-\Phi_{\mathcal P_i}(W_i)$ and $Y_i=\Phi'_{\mathcal P_i}(W_i)$ ; all other dual variables are $0$ .

Formalization targets

Goal: Theorem 2 (p. 16)

For every setup in the deterministic case with $k_i=1$ , every arrival sequence, every tie-breaking rule and every feasible $x$ of (5),

\min_iF(\mathcal P_i)\cdot\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}\ \le\ \mathbb E_{W}\bigl[\mathrm{ALG}\bigr].

Milestones

Weak duality for (5)/(19) (p. 19).
Lemma 2 (p. 22): if item $i$ is assigned to customer $t$ , then $(1-e^{-\alpha_i^{(1)}})(Y_i+Z_t)\le r_i^{(j_{t,i})}$ .
Dominance claim (App. C, pp. 45–46): let $Z^{\mathrm{crit}}$ be the pseudorevenue at $t$ of the run without item $i$ . If $W_i\in[0,W^{\mathrm{crit}})$ , then item $i$ is matched by time $t$ in the run with item $i$ .
Monotonicity claim (App. C, p. 46): $Z_t\ge Z^{\mathrm{crit}}$ for every value of $W_i$ .
Lemma 3 (p. 22): $y_i=\mathbb E[Y_i]$ , $z_t=\mathbb E[Z_t]$ is feasible for (19).

Significance

The theorem shows that one randomized rule achieves the optimal guarantee for every price set, and that the guarantee depends only on the price ratios. For one price, $F=1-1/e$ and the classical vertex-weighted result is recovered. With several prices the benchmark (5) is stronger, because the offline optimum may also choose prices, and the guarantee degrades gracefully: $F(\mathcal P)$ lies in $[1-e^{-1/m},1-1/e]$ and depends only on how far apart the prices are. Theorem 3 of the same paper shows that no online algorithm does better than $F(\mathcal P)$ when every item has price set $\mathcal P$ , so the ratio is tight.

The results are proved in the paper, in §4 and App. C. As far as the platform's records show, they have not been formalized. A formalization adds three things on top of the paper. It machine-checks a randomized primal–dual argument whose expectations are integrals over $[0,1]^n$ . It makes precise the measure-zero conventions the paper uses: ties in (23), and $\Phi'$ at segment borders. It also gives a Lean model of a ranking algorithm with continuous seeds that sees only the present customer, which could be reused for related online algorithms.

Difficulty

The pointwise part (Lemma 2) is a direct computation from the booking-limit identity (7). The difficulty is Lemma 3. The constraint for a pair $(t,i)$ needs $\mathbb E[Y_i+Z_t]\ge r_i^{(j_{t,i})}$ , but on a single sample path $Y_i+Z_t$ can be far below this: item $i$ may be taken by an earlier customer, or customer $t$ may take another item. The bound only holds after conditioning on the other seeds and comparing two coupled runs, one with item $i$ and one without. That comparison needs an invariant that holds at every step: the set of items still available in the run with $i$ contains the set in the run without $i$ . The invariant fails when ties are broken differently in the two runs, so the measure-zero set of ties must be handled explicitly. The conditional expectation of $Y_i$ is then an integral of $\Phi'$ , which is discontinuous at the segment borders.

Formalization scope

Indexing. Items are Fin n and customers Fin T, both 0-based. Prices are 1-based within an item, with pr r 0 = 0 for $r^{(0)}=0$ . Data at indices outside $[1,m_i]$ are never read.
Standing assumptions (p. 11), passed as hypotheses: every price set has $m_i\ge1$ and $0<r_i^{(1)}<\dots<r_i^{(m_i)}$ ; the booking limits are positive, sum to $1$ and satisfy (7) (IsBookingLimits, unique by Proposition 1); $p\in\{0,1\}$ on $[1,m_i]$ ; $k_i=1$ . Weak duality is stated for any $p\in[0,1]$ and any inventories.
Algorithm. The step at customer $t$ reads only $p_t$ , the seeds and the set of available items. Tie-breaking is any rule returning a maximizer of (23), universally quantified. A run can start from a subset of the items, which gives the run "with item $i$ removed".
Expectations are Lebesgue integrals over the product of $n$ uniform laws on $[0,1]$ . No integrability hypothesis is added: the integrands are bounded, and measurable outside the null set of ties.
Competitive ratio. It is stated multiplied out, for every feasible $x$ of (5), and needs $n\ge1$ for the minimum (with no items both sides are $0$ ). This rules out the trivializing readings $\mathbb E[\mathrm{ALG}]/\mathrm{OPT}$ with $x/0=0$ , and an infimum over arrival sequences. The algorithm is fixed as Algorithm 2; it is not "any algorithm with a property".
Added or changed hypotheses.
- Lemma 2 is claimed for every seed vector in $[0,1]^n$ , with $\Phi'$ the right derivative at a border. This implies the paper's "w.p.1".
- The two claims assume no ties, the paper's "we ignore measure-zero events".
- Dominance is written as $\Phi_{\mathcal P_i}(W_i)<r_i^{(j)}-Z^{\mathrm{crit}}$ . This is equivalent to $W_i<W^{\mathrm{crit}}$ because $\Phi$ is a strictly increasing bijection $[0,L_i^{(j)}]\to[0,r_i^{(j)}]$ .
Infrastructure. A solver needs: monotonicity and continuity of $\Phi_{\mathcal P}$ and the integral $\int_0^{w}\Phi'=\Phi(w)$ ; measurability of the run in $W$ ; the fact that ties are null under the product of uniform laws; and conditioning via Fubini on $[0,1]^n$ . These pieces are reusable for other randomized primal–dual analyses. The paper's proofs are in §4 (p. 23) and App. C (pp. 45–46). Proofs of any milestone, and lemmas on $\Phi_{\mathcal P}$ , are welcome.

Selected references

W. Ma, D. Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1, 2019; Operations Research 68(6), 2020. https://arxiv.org/abs/1905.04770 · https://doi.org/10.1287/opre.2019.1957
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
G. Aggarwal, G. Goel, C. Karande, A. Mehta, Online vertex-weighted bipartite matching and single-bid budgeted allocations, SODA 2011. https://arxiv.org/abs/1007.1271
N. R. Devanur, K. Jain, R. D. Kleinberg, Randomized primal-dual analysis of RANKING for online bipartite matching, SODA 2013. https://doi.org/10.1137/1.9781611973105.7

9 thms1 active userReviewed

Operations Research Probability·Captain: mikedeng1

Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-Dependent Competitive Ratios III: No Online Algorithm Earns More Than F(𝒫) Times the Expected Offline OptimumResearch Paper

Motivation

A firm sells several products, each in limited supply. Customers arrive one at a time, and each product can be offered at one of a few prices. This is the setting of airline fare classes, hotel rate plans and e-commerce discounting. Because future demand is unknown, the firm must decide online whether to sell a unit now at a low price or keep it for a customer who may pay more later. The competitive ratio measures how much an online policy loses against an omniscient benchmark in the worst case.

Ma and Simchi-Levi (arXiv:1905.04770; Oper. Res. 2020, doi:10.1287/opre.2019.1957) give online algorithms whose competitive ratio depends on the price set 𝒫 of each item through a number F(𝒫), and prove that this dependence is the best possible. This mission formalizes the second half, the impossibility result: no online algorithm can beat F(𝒫).

Timeline of the single-price precursors:

Karp, Vazirani and Vazirani (1990) introduced the upper-triangular random-permutation instance and showed that 1 − 1/e is optimal for online bipartite matching.
Mehta, Saberi, Vazirani and Vazirani (2007) used a similar construction for AdWords with small bids.
Golrezaei, Nazerzadeh and Rusmevichientong (2014) used one for personalized assortment with large inventories.
Ma and Simchi-Levi (2019, preprint v1) add phases of customers who pay different prices. With the phase lengths chosen adversarially, the bound becomes F(𝒫).

Setting

A setup has n items. Each item has starting inventory k ∈ ℕ, k ≥ 1, and the same price set 𝒫 = {r⁽¹⁾ < … < r⁽ᵐ⁾}, with r⁽¹⁾ > 0 and r⁽⁰⁾ := 0.

An arrival sequence 𝒜 has T customers. For each customer t, item i and price j it gives a purchase probability p⁽ʲ⁾{t,i}. It is deterministic if every p⁽ʲ⁾{t,i} is 0 or 1.

When customer t arrives, an online algorithm offers at most one in-stock item at one price. It decides using only the setup, the past, and the present customer's probabilities. A deterministic customer buys exactly when p⁽ʲ⁾_{t,i} = 1. A sale earns r⁽ʲ⁾ and uses one unit. ALG(𝒮, 𝒜) is the total revenue. A randomized online algorithm picks a deterministic one at random, ω ↦ alg(ω) with ω ~ μ.

The benchmark OPT(𝒮, 𝒜) is the value of the linear program (5):

\max \sum_{t,i,j} p^{(j)}_{t,i} r^{(j)} x^{(j)}_{t,i}\ \text{ s.t. } \sum_{t,j} p^{(j)}_{t,i} x^{(j)}_{t,i} \le k,\ \ \sum_{i,j} x^{(j)}_{t,i} \le 1,\ \ x \ge 0.

The booking limits α⁽¹⁾, …, α⁽ᵐ⁾ of Proposition 1 are the unique positive numbers summing to 1 with

1 - e^{-\alpha^{(1)}} = \frac{1 - e^{-\alpha^{(j)}}}{1 - r^{(j-1)}/r^{(j)}}, \qquad j = 2, \dots, m. \qquad (7)

The tight ratio is F(𝒫) = 1 − e^{−α⁽¹⁾}. For a single price F(𝒫) = 1 − 1/e. As r⁽ᵐ⁾/r⁽¹⁾ → ∞, F(𝒫) decreases.

Formalization targets

Goal: Theorem 3 (p. 17), in ε-form

For every k ≥ 1, every price set 𝒫 and every ε > 0, there are a setup with all items of inventory k and price set 𝒫 and a finite distribution over deterministic arrival sequences, with 𝔼[OPT] > 0, such that every (measurable) randomized online algorithm satisfies

\mathbb E_{\mathcal A}\,\mathbb E[\mathrm{ALG}(\mathcal S,\mathcal A)] \le \big(1 - e^{-\alpha^{(1)}} + \varepsilon\big)\,\mathbb E_{\mathcal A}[\mathrm{OPT}(\mathcal S,\mathcal A)].

The statement only asserts that such an instance exists; it does not fix the paper's construction.

Milestones

The instance of §5 has n items and nk customers in n groups of k. The groups are ordered by a uniformly random permutation π: group g wants items π_g, …, π_n. The groups are split into m phases; phase j pays up to r⁽ʲ⁾ and contains a fraction β_j = B_j − B_{j+1} of the groups. The milestones are:

(35): r⁽ʲ⁻¹⁾/r⁽ʲ⁾ ≤ e^{−α⁽ʲ⁾};
Proposition 4: the system B_j r⁽ʲ⁾ e^{−α⁽ʲ⁾} = r⁽¹⁾e^{−α⁽¹⁾} has a unique solution with 0 < B_m < … < B₁ = 1;
(25): on the instance, OPT = Σⱼ (r⁽ʲ⁾ − r⁽ʲ⁻¹⁾)Bⱼnk up to rounding;
Lemma 5: the maximum of the concave program (27) is (28);
(29): (28) at j = 1, τ = 1 equals F(𝒫) times (25);
Lemma 4: the expected revenue of any online algorithm is at most the maximum of (26), up to εnk for large n.

Significance

The theorem shows that the guarantees of the paper's online algorithms cannot be improved. Theorem 2 of the paper (Multi-price Ranking is F(𝒫)-competitive in the deterministic case) and Corollary 1 (Multi-price Balance tends to F(𝒫) as inventories grow) meet this bound, by Yao's minimax principle. So F(𝒫) is the exact competitive ratio for each price set. Without the theorem, the algorithms' ratios would only be lower bounds. The paper also shows (Proposition 2) that F(𝒫) exceeds the ratios of earlier approaches, so the tight value has practical bite.

The result is proved in the paper, with proofs in §5 and Appendix D, but not machine-checked. The formalization adds three things. First, an explicit treatment of rounding, which the paper sets aside as negligible for large n. Second, a corrected Lemma 5, which as printed is false for small τ. Third, a reusable model of online algorithms with deterministic arrivals and their randomized mixtures, and of the random-permutation instance.

Difficulty

The bound must hold for every online algorithm, including adaptive and randomized ones. An algorithm's decision can depend on everything it has seen, and the instance is averaged over n! permutations. So computing the best online algorithm's revenue directly is hopeless. The single-price instances of earlier work do not suffice either. On them all reasonable algorithms perform alike, whereas here the adversary's phase lengths must leave exactly one optimal way to ration inventory across phases. The upper bound on online revenue holds only asymptotically: the paper approximates harmonic sums by logarithms as n → ∞ and ignores the rounding of phase lengths. That is why the goal is in ε-form. Finally, the concave program that evaluates the bound has a closed-form optimum only when the candidate maximizer is nonnegative; Lemma 5 as printed omits this condition.

Formalization scope

Lean conventions:

Items and customers are 0-based (Fin n, Fin T); prices are 1-based functions ℕ → ℝ with r⁽⁰⁾ = 0 via price.
The booking limits α and the phase sizes B are hypotheses (IsBookingLimits, IsPhaseB), not chosen functions; Propositions 1 and 4 make them unique.
OPT is the real supremum of the LP's objective, a true maximum because the feasible set is nonempty and bounded.
A deterministic online algorithm is a rule taking the rows of customers 0, …, t to an optional (item, price) offer. It never sees later customers, or T. In the deterministic case this is the paper's information set.
A randomized algorithm is alg : Ω → OnlineAlg n on any probability space. Its expected revenue is a Bochner integral, with measurability in ω assumed; without that the integral could be 0 and the bound trivial.
The instance's phase borders are ⌊(1 − B_j)n⌋ and customer t is in group ⌊t/k⌋.

Disclosed departures from the page:

The goal and Lemma 4 carry an ε, as their proofs require.
The goal assumes 𝔼[OPT] > 0, because an empty arrival sequence would otherwise satisfy it trivially.
Lemma 5 assumes every candidate λ_ℓ = α⁽ℓ⁾ − (A_j − τ)/(m − j + 1) is nonnegative; the paper's one use (j = 1, τ = 1) satisfies this.
(25) is stated with an explicit rounding error of at most k(r⁽ᵐ⁾ − r⁽¹⁾).

The quantifier order is part of the theorem: the instance and distribution are fixed before the algorithm. A statement in which each algorithm gets its own hard instance is weaker and is not this theorem.

Needed infrastructure: finite sums over permutations, measure-theoretic expectation over the algorithm's randomness, harmonic-sum asymptotics, and one-dimensional concave maximization. The definitions of online algorithms and of the random-permutation instance are reusable for other Karp–Vazirani–Vazirani-type lower bounds. Contributions are welcome on any milestone. (35), Proposition 4 and (29) are elementary; (25) needs LP weak duality on the instance; Lemma 4 is the main work.

Selected references

W. Ma, D. Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1, 2019; Operations Research 68(6), 2020. https://arxiv.org/abs/1905.04770, https://doi.org/10.1287/opre.2019.1957
R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
N. Golrezaei, H. Nazerzadeh, P. Rusmevichientong, Real-time optimization of personalized assortments, Management Science 60(6), 2014. https://doi.org/10.1287/mnsc.2014.1939
A. C. Yao, Probabilistic computations: Toward a unified measure of complexity, FOCS 1977. https://doi.org/10.1109/SFCS.1977.24

11 thms1 active userReviewed

Linear Optimization Operations Research Probability·Captain: mikedeng1

Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-Dependent Competitive Ratios I: Multi-price Balance Is minᵢ F̃ᵢ-Competitive, F̃ᵢ Bounded via F(𝒫ᵢ), G(𝒫ᵢ)/2 and kᵢResearch Paper

Motivation

Online matching and its revenue-management variants model a firm that allocates limited inventory to customers who arrive one at a time, without knowing who comes next. Classical results in this area assume each item has a single price, or weight. For a single price and large inventories, the BALANCE algorithm of Kalyanasundaram and Pruhs (2000) and its generalizations by Mehta, Saberi, Vazirani and Vazirani (2007), Buchbinder, Jain and Naor (2007) and Golrezaei, Nazerzadeh and Rusmevichientong (2014) achieve the competitive ratio $1-1/e$ , which is best possible.

Firms that can also choose a price for each sale face a different problem. Selling an item cheaply now uses inventory that a later customer might have paid more for. Ma and Simchi-Levi (2020) study this setting. Each item can be offered at one of finitely many prices, and the attainable competitive ratio depends on those prices. Their Multi-price Balance algorithm attains, as inventories grow, a ratio that their Theorem 3 shows no online algorithm can beat. This mission formalizes their Theorem 1, the guarantee of Multi-price Balance for finite inventories.

Setting

A firm sells items $i$ from a finite set. Item $i$ starts with $k_i\ge1$ units and has a price set $\mathcal P_i$ of $m_i\ge1$ prices $0<r_i^{(1)}<\dots<r_i^{(m_i)}$ , with $r_i^{(0)}:=0$ . Customers $t=1,\dots,T$ arrive one by one. On arrival of customer $t$ the firm learns $p^{(j)}_{t,i}\in[0,1]$ , the probability that $t$ buys item $i$ at price $j$ . It offers at most one item, at one price. The customer accepts with that probability, and a sale earns $r_i^{(j)}$ and uses one unit. An online algorithm decides using only the setup, the past, and the present customer's probabilities.

The benchmark is the linear program (5):

\mathrm{OPT}=\max\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}\ \ \text{s.t.}\ \ \sum_{t,j}p^{(j)}_{t,i}x^{(j)}_{t,i}\le k_i,\ \ \sum_{i,j}x^{(j)}_{t,i}\le1,\ \ x\ge0 .

An algorithm is $c$ -competitive on a setup if $\mathbb E[\mathrm{ALG}]\ge c\cdot\mathrm{OPT}$ for every arrival sequence (6).

For a price set $\mathcal P$ , the booking limits $\alpha^{(1)},\dots,\alpha^{(m)}$ are the unique positive numbers summing to $1$ with

1-e^{-\alpha^{(1)}}=\frac{1-e^{-\alpha^{(j)}}}{1-r^{(j-1)}/r^{(j)}}\qquad(j=2,\dots,m),

and the values $\sigma^{(j)}$ are the unique positive numbers summing to $1$ with $\sigma^{(1)}=\sigma^{(j)}/(1-r^{(j-1)}/r^{(j)})$ (Proposition 1). Write $F(\mathcal P)=1-e^{-\alpha^{(1)}}$ and $G(\mathcal P)=\sigma^{(1)}$ , and $L^{(j)}=\alpha^{(1)}+\dots+\alpha^{(j)}$ .

Multi-price Balance (Algorithm 1) gives each item random segment borders $0=\tilde L_i^{(0)}\le\dots\le\tilde L_i^{(m_i)}=1$ in $\{0,1/k_i,\dots,1\}$ and a nondecreasing value function $\tilde\Phi_i$ on that grid with $\tilde\Phi_i(0)=0$ . Both are drawn from a randomized procedure, independently across items. With $N_i$ units of item $i$ sold, customer $t$ is offered a pair $(i,j)$ maximizing

p^{(j)}_{t,i}\big(\tilde\Phi_i(\tilde L_i^{(j)})-\tilde\Phi_i(N_i/k_i)\big)

when this maximum is positive. Two procedures are used. Definition 3 draws one uniform seed $W$ and rounds every $L^{(j)}k$ up or down with it, then sets $\tilde\Phi$ by formula (20). The procedure (45), for $k=1$ , draws configuration $d$ with probability $\sigma^{(d)}$ and sets $\tilde\Phi(1)=r^{(d)}/\sigma^{(1)}$ .

Formalization targets

Goal: Theorem 1 (p. 16)

Give each item a mode. A perturbed item uses Definition 3. A split item is replaced by $k_i$ single-unit copies, each using (45). With

b_i=\frac{F(\mathcal P_i)}{(1+k_i)(e^{1/k_i}-1)}\ \text{(i)},\qquad b_i=\frac{G(\mathcal P_i)}{2}\ \text{(ii, split)},\qquad b_i=\frac{1-1/e}{(1+k_i)(1-e^{-1/k_i})}\ \text{(iii, if }|\mathcal P_i|=1),

Multi-price Balance with those modes satisfies, for every arrival sequence, every tie-breaking rule and every feasible $x$ of (5),

\Big(\min_i b_i\Big)\sum_{t,i,j}p^{(j)}_{t,i}r_i^{(j)}x^{(j)}_{t,i}\le\mathbb E[\mathrm{ALG}].

Milestones

Weak duality for (5) and its dual (19) (p. 19).
Theorem 4 (p. 19). If every item's procedure satisfies

k_i\big(\tilde\Phi_i(\tfrac{N+1}{k_i})-\tilde\Phi_i(\tfrac N{k_i})\big)+\tilde\Phi_i(\tilde L_i^{(j)})-\tilde\Phi_i(\tfrac N{k_i})\le\frac{r_i^{(j)}}c\ \ (17),\qquad \mathbb E[\tilde\Phi_i(\tilde L_i^{(j)})]\ge r_i^{(j)}\ \ (18),

then Algorithm 1 is $c$ -competitive. 3. Proposition 3 (p. 21). $\mathbb E[\tilde L^{(j)}]=L^{(j)}$ , and $|(\tilde L^{(j)}-\tilde L^{(j')})-(L^{(j)}-L^{(j')})|\le1/k$ . 4. (35) (p. 39). $r^{(j-1)}/r^{(j)}\le e^{-\alpha^{(j)}}$ . 5. Theorem 5 (p. 22). Definition 3 satisfies (17)–(18) with $c=F(\mathcal P)/((1+k)(e^{1/k}-1))$ , and with $c=F(\mathcal P)/((1+k)(1-e^{-1/k}))$ when $m=1$ . 6. (45) (p. 44). For $k=1$ , the procedure (45) satisfies (17)–(18) with $c=\sigma^{(1)}/2$ .

Significance

For a single price, bound (iii) improves the dependence on $k_i$ of the guarantee of Golrezaei et al. (2014). For several prices, bound (i) tends to $F(\mathcal P_i)$ as $k_i\to\infty$ (Corollary 1). Mission III of this series formalizes Theorem 3, by which no online algorithm beats $F(\mathcal P)$ , so Theorem 1 makes that ratio tight. Bound (ii) uses a different procedure and gives a guarantee for small inventories that does not rely on perturbing the ideal value function. The paper's Section 6 applies the same framework to the Adwords problem and to assortment problems with multiple prices.

The paper's proofs are in its Appendix B: Theorem 4 by a randomized primal–dual argument, Proposition 3 and Theorem 5 by analysis of the comonotone rounding, (45) by solving a small system, and Theorem 1 by assembling them. None of these results has a machine-checked proof. A complete formalization would yield a reusable, checked primal–dual framework for randomized online allocation: Theorem 4 holds for any family of procedures satisfying (17)–(18).

Difficulty

The primal–dual proof of Theorem 4 sets the dual variables $y_i=\mathbb E[\tilde\Phi_i(N_{T,i}/k_i)]$ and $z_t=\mathbb E[Z_t]$ , where $Z_t$ is the pseudorevenue. These are expectations over both the initialization and the purchase decisions, and the dual constraint holds only after conditioning on the history and taking expectations. A deterministic value function does not suffice for multiple prices with finite inventory, since the borders $L^{(j)}k_i$ are generally not integers. This is why the value functions are random. Rounding each border independently would break the segment-length control. Theorem 5 needs the comonotone bound (22), and an induction over segments with careful bookkeeping of the rounding errors.

Formalization scope

Indices. Items form an arbitrary nonempty finite type. Customers are indexed $0,\dots,T-1$ . Prices are $1$ -based with $r^{(0)}=0$ . Probabilities $p^{(j)}_{t,i}\in[0,1]$ , $k_i\ge1$ , $m_i\ge1$ and $0<r_i^{(1)}<\dots<r_i^{(m_i)}$ are hypotheses.
Booking limits. $\alpha$ and $\sigma$ enter as functions satisfying the defining systems (7) and (8) with positivity and unit sum. By Proposition 1 they are the paper's values.
Unit indices. Borders are stored as $k\tilde L^{(j)}\in\{0,\dots,k\}$ and value functions as $N\mapsto\tilde\Phi(N/k)$ . In (17) the range of $N$ is $N<k\tilde L^{(j)}$ .
The algorithm. The offer at customer $t$ is computed from that customer's probabilities and the sales counts. The count in (16) is read as $\min(N_i,k_i)$ , which equals $N_i$ because the algorithm never sells a stocked-out item. Ties are broken by an arbitrary rule returning a maximizer, and every statement holds for every such rule.
Expectations. Expected revenue is a finite sum over configurations, weighted by product probabilities, combined with a backward recursion over accept/reject outcomes. Definition 3's configuration probabilities are Lebesgue measures of seed sets.
Competitive ratio. The ratio is always stated as $c\cdot(5\mathrm a)(x)\le\mathbb E[\mathrm{ALG}]$ for every feasible $x$ of the original LP (5). This rules out the trivializations through $x/0=0$ when $\mathrm{OPT}=0$ , through an infimum over arrival sequences, and through a benchmark taken on the split setup instead of the original one.
$\tilde F_i$ is not used. The printed theorem is phrased through $\tilde F_i$ , the optimum of the problem (44). The proof never shows that this optimum is attained. Its bound (ii) also comes from splitting the item, not from a procedure feasible for (44). The goal is therefore stated with explicit bounds and modes; choosing the better mode per item gives the printed $\min_i\max\{\dots\}$ .
Not posed. Corollaries 1–2 and the optimality and uniqueness claims about (45).

Weak duality is shared with mission II and (35) with mission III; each mission defines its own copy of the model. Contributions welcome: proofs of the milestones, and of the goal from them.

Selected references

W. Ma, D. Simchi-Levi, Algorithms for Online Matching, Assortment, and Pricing with Tight Weight-dependent Competitive Ratios, arXiv:1905.04770v1 (2019); Operations Research 68(6), 2020. https://arxiv.org/abs/1905.04770, https://doi.org/10.1287/opre.2019.1957
B. Kalyanasundaram, K. Pruhs, An optimal deterministic algorithm for online b-matching, Theoretical Computer Science 233, 2000. https://doi.org/10.1016/S0304-3975(99)00140-1
A. Mehta, A. Saberi, U. Vazirani, V. Vazirani, AdWords and generalized online matching, Journal of the ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284321
N. Buchbinder, K. Jain, J. Naor, Online primal-dual algorithms for maximizing ad-auctions revenue, ESA 2007. https://doi.org/10.1007/978-3-540-75520-3_24
N. Golrezaei, H. Nazerzadeh, P. Rusmevichientong, Real-time optimization of personalized assortments, Management Science 60(6), 2014. https://doi.org/10.1287/mnsc.2014.1939

11 thms1 active userReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Optimal Approximation for Submodular and Supermodular Optimization with Bounded Curvature I: Swap-Local Optima of the Non-Oblivious Potential Are (1 − c/e)-Approximate for Submodular MaximizationResearch Paper

Motivation

Maximizing a monotone submodular function over the bases of a matroid is the standard model for coverage, facility location, sensor placement and welfare maximization. The best possible approximation factor in the value-oracle model is $1 - 1/e$ (Nemhauser–Wolsey 1978; Călinescu–Chekuri–Pál–Vondrák 2011). Many functions met in practice are far from the worst case: they are close to linear. Total curvature measures how close. Conforti and Cornuéjols (1984) showed that the greedy algorithm achieves $(1 - e^{-c})/c$ on uniform matroids and $1/(1+c)$ on general matroids when the curvature is at most $c$ ; Vondrák (RIMS Kôkyûroku Bessatsu, 2010) obtained $(1 - e^{-c})/c$ for every matroid, for a weaker curvature notion.

Sviridenko, Vondrák and Ward (SODA 2015; journal version Math. Oper. Res. 2017) improve this to $1 - c/e$ , show it is optimal, and obtain the matching factor $1 + \frac{c}{1-c} e^{-1}$ for minimizing a monotone decreasing supermodular function. One of their two algorithms is a non-oblivious local search, a single-swap search guided not by $f$ but by an auxiliary potential. This mission formalizes the exact guarantee of that local search. All numbering below is that of the SODA 2015 version (authors' copy dated Oct. 9, 2014).

Setting

Let $X$ be a finite set. A set function assigns a real number $f(A)$ to every $A \subseteq X$ . Its marginal value at $i \in X$ over $A$ is $f_A(i) = f(A + i) - f(A)$ . The function is submodular if $f(A) + f(B) \ge f(A \cap B) + f(A \cup B)$ for all $A, B$ ; supermodular if $-f$ is submodular; monotone increasing if every $f_A(i) \ge 0$ , and monotone decreasing if every $f_A(i) \le 0$ .

A monotone increasing $f$ has total curvature at most $c$ if $f_{X-j}(j) \ge (1-c) f_\emptyset(j)$ for every $j \in X$ : adding $j$ last is worth at least a $(1-c)$ fraction of adding it first. For $c = 0$ the function is linear up to a constant; $c = 1$ is no restriction. For a monotone decreasing $f$ the inequality is reversed: $f_{X-j}(j) \le (1-c) f_\emptyset(j)$ .

A matroid $\mathcal M = (X, \mathcal I)$ is given by its independent sets; its bases $\mathcal B(\mathcal M)$ are the maximal independent sets, and its dual $\mathcal M^*$ has the complements $X \setminus B$ of bases as bases.

For a monotone increasing submodular $f$ , §6.1 of the paper splits $f = g + \ell$ with a linear part and a remainder,

\ell(A) = \sum_{j \in A} f_{X-j}(j), \qquad g(A) = f(A) - \ell(A).

The local search uses the Filmus–Ward potential of $g$ and the potential $\psi$ :

h(A) = \sum_{\emptyset \ne B \subseteq A} g(B) \int_0^1 \frac{e^p}{e-1}\, p^{|B|-1}(1-p)^{|A|-|B|}\, dp, \qquad \psi(A) = (1 - e^{-1})\, h(A) + \ell(A).

A base $S$ is a swap-local optimum of $\psi$ if $\psi(S - a + b) \le \psi(S)$ for every $a \in S$ and $b \in X \setminus S$ with $S - a + b$ a base.

Formalization targets

Goal: exact core of Theorem 6.1

For $f \ge 0$ monotone increasing and submodular with curvature at most $c \in [0,1]$ , every swap-local optimum $S$ of $\psi$ satisfies

f(S) \ \ge\ \Bigl(1 - \frac{c}{e}\Bigr)\, f(O) \qquad \text{for every } O \in \mathcal I.

The printed Theorem 6.1 asserts a randomized polynomial-time algorithm losing $O(\epsilon)$ ; the goal is the $\epsilon = 0$ statement its proof establishes for local optima.

Milestones

Lemma 2.1: $\sum_{j \in A} f_{X-j}(j) \ge (1-c) f(A)$ , for $f(\emptyset) = 0$ .
Lemma A.1: $g = f - \ell$ is submodular, monotone increasing and nonnegative.
Lemma 5.1 (Brualdi): two bases $A, B$ admit a bijection $\pi : A \to B$ with $A - x + \pi(x)$ a base for every $x \in A$ .
Display (5.4) (Filmus–Ward): $\frac{e}{e-1} g(A) \ge g(B) + \sum_i [h(A) - h(A - a_i + b_i)]$ .
Lemma 5.2: $g(A) + \ell(A) \ge (1 - e^{-1}) g(B) + \ell(B) + \sum_i [\psi(A) - \psi(A - a_i + b_i)]$ .
§5.1: a swap-local optimum $S$ satisfies $g(S) + \ell(S) \ge (1 - e^{-1}) g(O) + \ell(O)$ for every base $O$ .

Companion statements

Lemma 2.2, Lemma A.2 and the exact core of Theorem 6.2: for $f \ge 0$ monotone decreasing and supermodular with curvature at most $c \in [0, 1)$ , a swap-local optimum $S$ of the corresponding $\psi$ in $\mathcal M^*$ yields a base $X \setminus S$ of $\mathcal M$ with

f(X \setminus S) \ \le\ \Bigl(1 + \frac{c}{1-c}\, e^{-1}\Bigr) f(O) \qquad \text{for every } O \in \mathcal I.

Lemmas A.3 and A.4 are the curvature constructions behind the paper's matching lower bounds.

Significance

The factor $1 - c/e$ equals $1 - 1/e$ at $c = 1$ and tends to $1$ as $c \to 0$ , so it recovers the classical bound and improves it for every curvature below $1$ ; Theorem 7.1 of the paper shows that no algorithm using polynomially many value queries does better. The decomposition $f = g + \ell$ and the joint guarantee $g(S) + \ell(S) \ge (1 - e^{-1}) g(O) + \ell(O)$ are reusable: they give the supermodular-minimization result of Theorem 6.2, and §8 of the paper applies that result to column-subset selection.

The results are proved in the literature; none is machine-checked. The mission produces a formal proof of the exact local-search guarantee, of Brualdi's bijective exchange for Mathlib matroids, and of Filmus and Ward's inequality for their potential $h$ , which underlies other non-oblivious local searches for submodular functions.

Difficulty

The reduction from the goal to the §5.1 claim is short. The work is in (5.4): the obvious argument, summing submodularity over the swaps, controls $\sum_i [g(A) - g(A - a_i + b_i)]$ and gives only the oblivious factor $1/2$ . The potential $h$ averages $g$ over all subsets of $A$ with Beta-type weights, and (5.4) is an identity-level computation with the integrals $\int_0^1 e^p p^{k-1}(1-p)^{m-k}\,dp$ . Brualdi's lemma needs a Hall-type argument on the exchange graph; Mathlib has only single-element exchange. Lemma 2.1 also hides a point the paper skips: it is false unless $f(\emptyset) = 0$ , so the goal needs a normalisation $f \mapsto f - f(\emptyset)$ that leaves marginals, $\ell$ and the swap-local optima unchanged.

Formalization scope

Subsets are Finset X over [Fintype X] [DecidableEq X] with X : Type; set functions are Finset X → ℝ, and the paper's codomain $\mathbb R_{\ge 0}$ is a hypothesis ∀ A, 0 ≤ f A. Submodularity is the published definition NonmonotoneSubmod.Shared.Submodular. Total curvature is in the product form above, not the ratio of (1.1), which is undefined when some $f_\emptyset(j) = 0$ . Matroids are Mathlib's Matroid X, with M.E = Set.univ wherever $f$ and $\mathcal M$ meet, so that $X \setminus S$ is complemented in the right set; the dual is M✶. $e$ is Real.exp 1. The bijection of Lemma 5.1 is a function π : X → X with Set.BijOn π A B, and sums over $i = 1, \dots, r$ are sums over $a \in A$ with $b = \pi(a)$ .

Conventions that differ from the page, each disclosed in the item's Formalization Note:

the $B = \emptyset$ term of $h$ is excluded (on the page it is $g(\emptyset) \int_0^1 p^{-1} \cdots dp$ , finite only when $g(\emptyset) = 0$ );
(5.4), Lemma 5.2 and the §5.1 claim assume $g$ monotone and nonnegative, the setting of Filmus and Ward and of every use in the paper;
Lemma 2.1 adds $f(\emptyset) = 0$ , Lemma A.2's nonnegativity adds $f(X) = 0$ , and Lemmas A.3 and A.4 take $c > 0$ ; Lemma A.4 is stated as its proof proves it (supermodular, monotone decreasing).

The goal is about every swap-local optimum of $\psi$ , not about the existence of a good base: "some base satisfies $f(S) \ge (1 - c/e) f(O)$ " is trivially true by taking $S$ optimal, and is not the theorem.

Welcome contributions: Brualdi's lemma for Mathlib matroids (reusable well beyond this mission), the Beta-integral identities behind $h$ , and the normalisation argument. The polynomial-time algorithm, the sampling estimate of $\psi$ (§5.2), the continuous greedy of §4 and the lower bounds of §7 are out of scope.

Selected references

M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015; Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
Y. Filmus, J. Ward, Monotone submodular maximization over a matroid via non-oblivious local search, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/110832318
M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
R. A. Brualdi, Comments on bases in dependence structures, Bull. Austral. Math. Soc. 1(2), pp. 161–167, 1969.
G. L. Nemhauser, L. A. Wolsey, Best algorithms for approximating the maximum of a submodular set function, Math. Oper. Res. 3(3), 1978. https://doi.org/10.1287/moor.3.3.177
G. Călinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a monotone submodular function subject to a matroid constraint, SIAM J. Comput. 40(6), 2011. https://doi.org/10.1137/080733991
J. Vondrák, Submodularity and curvature: the optimal algorithm, RIMS Kôkyûroku Bessatsu B23, pp. 253–266, 2010.

9 thms1 active userReviewed

Combinatorics Linear algebra Markov Chain·Captain: mikedeng1

High Order Random Walks: Beyond Spectral Gap 2: On a Two-Sided λ-Local Spectral Expander, Spec(M⁺_k) ⊆ {1} ∪ ⋃_j [(k+1−j)/(k+2) ± √(k+1)·ε_k/(k+2)] and Eigenvectors Lie Near U^j_kResearch Paper

Motivation

High-dimensional expanders are simplicial complexes whose local structure forces global mixing. Random walks on their $k$ -dimensional faces, the high order random walks, are used to analyse sampling algorithms: the bases-exchange walk on the bases of a matroid is such a walk, and its spectral analysis by Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) settled the Mihail–Vazirani conjecture on counting matroid bases. Agreement tests and PCP constructions use the same walks (Dinur–Kaufman, FOCS 2017).

Most of these applications use only the second eigenvalue of the walk. Kaufman and Oppenheim (arXiv:1707.02799v3) observe that this eigenvalue cannot be very small, because of natural obstructions such as cochains pulled up from lower dimensions, and ask instead for the whole spectrum and the structure of the eigenvectors. For complexes whose links have both small second eigenvalue and bounded-below smallest eigenvalue (two-sided local spectral expanders), they show that the spectrum of the walk on $k$ -faces clusters around $k+1$ explicit values, each cluster corresponding to cochains built from a lower dimension.

Timeline. Garland (1973, doi:10.2307/1970833) introduced the localization method relating global cohomology to spectra of links. Kaufman and Mass (ITCS 2017, arXiv:1604.02947) defined high order random walks and bounded their second eigenvalue. Oppenheim (Discrete Comput. Geom. 2018, arXiv:1709.04431) developed the local spectral expansion framework and its trickle-down theorem. Kaufman and Oppenheim gave the decomposition theorems this mission formalizes; arXiv v3 (2021) corrects an error of the published version. Alev and Lau (arXiv:2001.02827) later improved the one-sided bounds.

Setting

Let $X$ be a pure $n$ -dimensional finite simplicial complex on a vertex set $V$ : a finite family of finite subsets of $V$ , closed under subsets, in which every face lies in a face with $n+1$ vertices. $X(k)$ is the set of faces with $k+1$ vertices, and $X(-1)=\{\emptyset\}$ . A weight is a function $m:X\to(0,\infty)$ with $m(\tau)=\sum_{\sigma\in X(k+1),\,\tau\subseteq\sigma}m(\sigma)$ for $\tau\in X(k)$ , $k\le n-1$ .

A $k$ -cochain is a function $\phi:X(k)\to\mathbb R$ ; the space $C^k(X)$ carries the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ . $C^k_0(X)$ is the subspace of cochains orthogonal to the constants.

The signless differential $d_k:C^k\to C^{k+1}$ is $d_k\phi(\sigma)=\sum_{\tau\subset\sigma,\,\tau\in X(k)}\phi(\tau)$ , and $d_k^*$ is its adjoint.
The upper random walk $M^+_k$ on $X(k)$ stays at $\tau$ with probability $\frac1{k+2}$ and moves to $\tau'$ with probability $\frac{m(\tau\cup\tau')}{(k+2)m(\tau)}$ when $\tau\cup\tau'\in X(k+1)$ ; equivalently $d_k^*d_k=(k+2)M^+_k$ .
The link of $\tau$ is $X_\tau=\{\eta:\ \eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$ with weight $m_\tau(\eta)=m(\tau\cup\eta)$ . On its vertices, $(M')^+_{\tau,0}$ is the non-lazy walk; $\mu_\tau$ and $\nu_\tau$ are its second largest and smallest eigenvalues.
$X$ is a two-sided $\lambda$ -local spectral expander if $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$ .

For $0\le k\le n-1$ the paper defines subspaces of $C^k_0(X)$ : $V^0_0=C^0_0$ ; for $k\ge1$ , $V^j_k=d_{k-1}\cdots d_j(C^j_0)$ for $j<k$ and $V^k_k=\ker d^*_{k-1}$ ; and $U^0_k=V^0_k$ , $U^j_k=V^j_k\cap(V^{j-1}_k)^\perp$ for $0<j<k$ , $U^k_k=V^k_k$ . With $\varepsilon_0=\lambda$ and $\varepsilon_k=2k(1+2k\sqrt k)\varepsilon_{k-1}+(k+1)\lambda$ , $P_{U}$ denotes the weighted orthogonal projection onto $U$ .

Formalization targets

Goal: Theorem 5.9 (p. 22)

If $\varepsilon_k\le\frac{1}{2(1+2(k+1)\sqrt{k+1})}$ for $0\le k\le n-2$ and $\varepsilon_{n-1}<\frac1{2\sqrt n}$ , then for $0\le k\le n-1$

\operatorname{Spec}(M^+_k)\subseteq\{1\}\cup\bigcup_{j=0}^{k}\Big[\tfrac{k+1-j}{k+2}-\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k,\ \tfrac{k+1-j}{k+2}+\tfrac{\sqrt{k+1}}{k+2}\varepsilon_k\Big],

and an eigenvector $\phi\in C^k_0$ whose eigenvalue lies in the $j$ -th interval satisfies $\|\phi-P_{U^j_k}\phi\|\le\frac{\sqrt{k+1}\varepsilon_k}{1-\sqrt{k+1}\varepsilon_k}\|\phi\|$ .

Milestones

the localization identities (Lemma 3.6, Corollary 3.7, Propositions 4.1, 4.2) and the two-sided bound of Lemma 4.3;
Lemma 5.1 and the orthogonal decomposition $C^k_0(X)=U^k_k\oplus\cdots\oplus U^0_k$ (§5.3);
Theorem 5.6: $\|d^*_kd_kP_{U^j_k}\phi-(k+1-j)P_{U^j_k}\phi\|\le\varepsilon_k\|P_{U^j_k}\phi\|$ ;
Corollary 5.8: the same for $M^+_k$ , with $\frac{k+1-j}{k+2}$ and $\frac{\varepsilon_k}{k+2}$ .

Significance

The result. Theorem 5.9 describes the spectrum of $M^+_k$ , not only its second eigenvalue. The eigenvalue $\frac{k+1-j}{k+2}$ is the one carried by cochains pulled up from dimension $j$ , so it explains which cochains are shrunk slowly by the walk and which quickly. It is the two-sided counterpart of the paper's one-sided mixing bound (Theorem 5.4, the subject of the first mission in this series). It gives approximate eigenspaces explicitly, which a mixing-time analysis or an agreement-test analysis can use in place of a bound on a single eigenvalue.

Formalizing it. No machine-checked development of simplicial-complex random walks, Garland's method, or local spectral expansion is known to exist; Mathlib has simplicial complexes in a geometric sense but no weighted cochain calculus. The mission produces the cochain calculus of §2–§4 together with the spectral statements of §5.3. The statements are those of the arXiv v3 preprint. They are published results but have not been formalized.

Difficulty

The obvious route would show that the spaces $U^j_k$ are exact eigenspaces. That holds for the complete complex but not in general: $d^*d$ maps $U^j_k$ only approximately into itself, and the error has to be controlled through every lower dimension at once. Theorem 5.6 is an induction on $k$ in which the error $\varepsilon_{k-1}$ of dimension $k-1$ enters dimension $k$ multiplied by norms of $d^*_{k-1}d_{k-1}$ and its square root. Controlling these factors on the correct subspaces, rather than on all of $C^{k-1}$ , is the delicate step: $d^*_{k-1}d_{k-1}=(k+1)M^+_{k-1}$ has norm $k+1$ on $C^{k-1}(X)$ , attained on the constants, and the bound needed is on the complement of the constants. Passing from Corollary 5.8 to the spectral statement of Theorem 5.9 needs the intervals to be disjoint and the eigenvector to be split along the orthogonal decomposition.

Formalization scope

Encoding. Faces are Finset V and $X$ is a Finset (Finset V); faces are indexed by their number of vertices (cells X (k + 1) is $X(k)$ ). Cochains are functions Finset V → ℝ, and every operator vanishes off $X$ .
Supports. Subspaces, eigenvectors and orthogonal complements consist of functions supported on $X(k)$ (Supp X (k + 1)). Without this, a function living off the faces would have norm $0$ , would be an eigenvector with eigenvalue $0$ , and would make the spectral statement false; a formalization without supports is ruled out for this reason.
Weights and adjoints. The weight is strictly positive on faces. $d^*$ is defined by its explicit formula, and Lemma 3.6 states that this formula is the adjoint.
Expansion. The eigenvalue conditions on links are stated in Rayleigh form on the weighted complement of the constants, $|\langle(M')^+_{\tau,0}g,g\rangle|\le\lambda\|g\|^2$ ; this encodes $-\lambda\le\nu_\tau$ and $\mu_\tau\le\lambda$ and needs no connectivity. Definition 1.2 is followed where Definition 4.4 misprints the two-sided clause.
Projections. $P_U\phi$ is characterised relationally (IsWProj: $u\in U$ and $\phi-u\perp U$ ) instead of by an operator. On these finite-dimensional subspaces it exists and is unique.
Indices and constants. $\varepsilon_k$ is eps lam k, with the recursion shifted by one index. $k$ is quantified inside each conclusion, and $\varepsilon_{n-1}$ is written without natural subtraction. The statements follow the printed constants of arXiv v3.

A complete development needs finite-dimensional weighted inner-product spaces of cochains, Garland localization, Courant–Fischer for self-adjoint operators on these spaces, and orthogonal projections onto images of iterated differentials. The cochain calculus and the localization identities are reusable for any weighted simplicial complex, and the first mission of this series needs the same objects. Proofs of the localization identities, of the decomposition, and of any milestone are welcome, as are proofs of the results with weaker hypotheses.

Selected references

T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Annals of Mathematics 97, 1973. https://doi.org/10.2307/1970833
T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete & Computational Geometry 59, 2018. https://arxiv.org/abs/1709.04431
N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: high-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
V. L. Alev, L. C. Lau, Improved analysis of higher order random walks and applications, STOC 2020. https://arxiv.org/abs/2001.02827

15 thms1 active userReviewed

Theoretical Computer Science

Missions

The Aaronson-Ambainis ConjectureOpen Problem

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: the probabilistic lower bound

Stronger: the three steps of the proof, as separate targets

Significance

Difficulty

Formalization scope

Selected references

Context: where this sits in the formalization landscape

Primal-Dual Online Load Balancing on Unrelated MachinesTextbook

The model

The algorithm and the guarantee

Scope

Source

Quantum Speedup of Monte Carlo Methods 1: With Var(v(A)) ≤ σ² and ε < 4σ, Algorithm 3 Estimates E[v(A)] to Additive Error ε with Probability at Least 2/3Research Paper

Why estimate a mean with a quantum algorithm?

Outputs, truncations, and estimates

Formalization targets

Lemma 4: nonnegative mean accuracy

Theorem 5: bounded-variance accuracy

What the result supplies

Where the difficulty lies

Formalization scope

Selected references

Optimization by Decoded Quantum Interferometry 1: The Semicircle Law — the Optimal Degree-ℓ DQI State Satisfies ⟨s⟩/m → (√(μ(1−ρ)) + √(ρ(1−μ)))² When 2ℓ + 1 < d⊥Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 3: In Simultaneous Offering With Values at Least τ, a Truncated-LP Value-Ordered Policy Earns ≥ α^τ_k Times the LP BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 30)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Strongly Polynomial Algorithm for Linear Exchange Markets II: A Z₊-Matrix Polyhedron P_M Lies Between an M2VPI Polyhedron and Its Scaling by B²Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.4 (p. 15)

Milestones (§7, pp. 16–23)

Significance

Difficulty

Formalization scope

Selected references

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 2: An LP-Rounding Policy That Sends Offers in Parallel Lists Earns at Least (1 − 1/e) Times the LP BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 1: A Non-Adaptive, Committed LP-Rounding Policy for ProbeTop-k Earns at Least (1 − e^{−k}k^k/k!) Times the LP BoundResearch Paper

Motivation

Setting

Formalization targets

`examples/matrix_strassen.algo`

`kruskal.algo`

`kruskal_sorted.algo`

`union_find.algo`

`sort_indices.algo`

`indexed_heap.algo`