All missions

Motivation

Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor $\lambda$ per step, so it needs on the order of $(1-\lambda)^{-1}\log(1/\epsilon)$ iterations, which is slow when $\lambda$ is close to $1$, the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map $v \mapsto v - T(v)$ and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate $\lambda$ of plain VI on every MDP? Theorem 6.3 of the paper answers no.

Setting

A finite MDP consists of a state set $S$ with $|S| = n$, a finite nonempty action set $A$, transition probabilities $P_{iaj} \ge 0$ with $\sum_j P_{iaj} = 1$, rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. Its Bellman operator $T : \mathbb{R}^n \to \mathbb{R}^n$ is

$$T(v)_i = \max_{a \in A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj} v_j \Big\}, \qquad i \in S,$$

a $\lambda$-contraction for the sup norm $\|\cdot\|_\infty$. Its unique fixed point $v^*$ is the optimal value function.

A sequence $(v_s)_{s \ge 0}$ in $\mathbb{R}^n$ is a first-order sequence for $T$ if

$$v_0 = 0, \qquad v_{s+1} \in \operatorname{span}\{v_0, \dots, v_s, T(v_0), \dots, T(v_s)\}, \quad s \ge 0 .$$

VI from $v_0 = 0$ ($v_{s+1} = T(v_s)$) and relaxed VI ($v_{s+1} = v_s - \alpha_s(v_s - T(v_s))$) from $0$ produce such sequences.

The chain MDP of Figure 1 has $n$ states and a single action. State $1$ is absorbing with reward $r_1 = 1$; every state $i \ge 2$ moves deterministically to $i - 1$ and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, $T$ is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.

Formalization targets

Goal: Theorem 6.3 (p. 12)

For every $n$, every $\lambda \in (0,1)$, the fixed point $v^*$ of the Bellman operator $T$ of the $n$-state chain, every first-order sequence $(v_s)$ for $T$, and every $s \in \{1, \dots, n-1\}$,

$$\|v_s - v^*\|_\infty \ge \frac{\lambda^s}{1+\lambda}.$$

Milestones

1. $T$ is a $\lambda$-contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
2. (3.5): $(1-\lambda)\|v - w\|_\infty \le \|(I-T)(v) - (I-T)(w)\|_\infty$ (p. 6).
3. (3.6): $\|(I-T)(v) - (I-T)(w)\|_\infty \le (1+\lambda)\|v - w\|_\infty$ (p. 6).
4. On the chain, the value function is $v^*_i = \lambda^{i-1}/(1-\lambda)$, and it is the only fixed point of $T$ (p. 12).
5. On the chain, every first-order sequence satisfies $v_{s,i} = 0$ for $i \ge s+1$ (p. 12).
6. (6.2)–(6.4): on the chain, $\|v_s - T(v_s)\|_\infty \ge \lambda^s$ for $1 \le s \le n-1$ (p. 12).

Significance

The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate $\lambda$ of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from $1 - \mu/L$ to $1 - \sqrt{\mu/L}$; with $\mu = 1-\lambda$, $L = 1+\lambda$, the analogue for MDPs would be a rate of about $1 - \sqrt{1-\lambda}$, and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.

Difficulty

The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with $s$ and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index $s$. The support claim has to be carried through the nonlinear max in $T$, which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of $v_s - v^*$ into a bound in sup norm with the exact constant $1/(1+\lambda)$, which requires the two-sided inequalities (3.5)–(3.6) for $I - T$ and the explicit value $v^*_{s+1} = \lambda^s/(1-\lambda)$.

Formalization scope

• States are Fin n and are 0-based: the paper's state $i$ is index $i - 1$, so $v^*_i = \lambda^{i-1}/(1-\lambda)$ is lam ^ k / (1 - lam) at index $k$ and "$i \ge s+1$" is $s \le k$. The action set of the chain is Unit.
• $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index $s$ inclusive.
• $v^*$ enters the goal through its defining equation $T(v^*) = v^*$; it is not replaced by the explicit vector. The initial distribution $p_0$ of the paper's MDP tuple is omitted, since no result here uses it.
• Pinned quantifiers. As printed, Theorem 6.3 asserts that there exists an MDP instance, with $n$ its own number of states; read literally, an instance with $n = 1$ has no admissible $s$. The proof fixes an arbitrary $n$ and $\lambda \in (0,1)$ and uses the chain. The goal states that claim for every $n$ and $\lambda$ on the explicit chain, which implies the printed form.
• $n - 1$ is natural-number subtraction, so the goal has content exactly when $n \ge 2$.
• The goal's constant is $\lambda^s/(1+\lambda)$ as printed; the sharper bound $\lambda^s/(1-\lambda)$, which the proof's chain also gives, is not the target.
• The Bellman operator and the kernel condition are the published platform definitions FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.
• A trivializing formalization would take an unsatisfiable fixed-point hypothesis or an empty first-order class. Both are satisfiable: the explicit vector is a fixed point (milestone 4), and VI from $0$ is first-order.

Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994/2014. https://doi.org/10.1002/9780470316887

Motivation

In many auctions a bidder's value for what is sold depends on information held by other bidders: the value of an oil-drilling lease depends on every bidder's geological survey, the value of a piece of art on what other experts know about its provenance. This is the interdependent values model of Milgrom and Weber (1982). With interdependent values the standard private-value tools fail: the Vickrey–Clarke–Groves (VCG) mechanism is no longer incentive compatible, exact efficiency in ex-post equilibrium requires a single-crossing condition, and with multidimensional signals maximizing welfare is generically impossible even in Bayes–Nash equilibrium (Jehiel and Moldovanu 2001). Without some structural condition on how values respond to others' information, even a single-item auction can force every truthful randomized mechanism to lose a factor of order $n$ (Example 1.3, after Eden et al. 2018), when values treat the signals as complements.

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384, Mathematics of Operations Research 2024) identify such a condition, submodularity over signals (SOS), and show that under SOS simple randomized mechanisms recover a constant fraction of the optimal welfare in rich settings. This mission formalizes their result for combinatorial auctions with multidimensional signals and separable SOS valuations, where the mechanism is a random-sampling variant of VCG with explicit payments.

Timeline of the line of work:

• Milgrom and Weber (1982): the interdependent values model.
• Jehiel and Moldovanu (2001): with multidimensional signals, welfare maximization is generically impossible even in Bayes–Nash equilibrium.
• Chawla, Fu and Karlin (2014): revenue approximation in interdependent value settings under single crossing.
• Roughgarden and Talgam-Cohen (2016): characterization of ex-post IC for single-parameter settings by monotone allocation rules.
• Eden, Feldman, Fiat and Goldner (2018): welfare approximation for single-item auctions under a relaxed c-single crossing condition; an SOS notion also appears there.
• Eden, Feldman, Fiat, Goldner and Karlin (2019, arXiv v2): welfare approximation under SOS, without single crossing, for downward-closed single-parameter settings and combinatorial auctions; the subject of this mission.

Setting

There are $n$ agents and $m$ items; a bundle is a set $T \subseteq [m]$. Each agent $i$ privately holds a signal $s_{iT} \ge 0$ for every bundle $T$, and $s_T = (s_{1T}, \dots, s_{nT})$ collects all agents' signals for $T$. Agent $i$'s value for bundle $T$ is $v_{iT}(s_T) \ge 0$, a known function of $s_T$, weakly increasing in every signal and strictly increasing in $s_{iT}$; the empty bundle is worth $0$.

A function $w$ of the signal vector is SOS when raising a single coordinate helps at least as much at a coordinatewise lower profile of the other coordinates: for every coordinate $j$, $x, \delta \ge 0$ and profiles $s' \le s$ off $j$,

$$w(s_{-j}, x + \delta) - w(s_{-j}, x) \le w(s'_{-j}, x + \delta) - w(s'_{-j}, x).$$

The valuations are separable SOS when

$$v_{iT}(s_T) = g_{-iT}(s_{-iT}) + h_{iT}(s_{iT}),$$

with $g_{-iT}$ (depending only on the other agents' signals for $T$) and $h_{iT}$ weakly increasing and $g_{-iT}$ SOS.

An allocation gives agent $i$ the bundle $T_i$, with the bundles pairwise disjoint. A deterministic mechanism maps reported signals to an allocation and payments. It is ex-post incentive compatible (IC) if, whatever the true signals, no agent gains by misreporting when the others report truthfully, where the agent's utility is her value at the true signals for the bundle she receives minus her payment; it is ex-post individually rational (IR) if the truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support is.

Random-Sampling VCG (RS-VCG) partitions the agents uniformly at random into $A$ and $B$. For $j \in B$ it sets the proxy weight

$$w_{jT} := v_{jT}(\tilde s_{jT}, \tilde s_{AT}, 0_{B - jT}),$$

the value with the bundle-$T$ signals of the other members of $B$ replaced by $0$. It allocates to $B$ a feasible allocation $\{T_i\}_{i\in B}$ maximising $\sum_{i \in B} w_{iT_i}$, and a winner $i \in B$ pays

$$p_i(\tilde s) = g_{-iT_i}(\tilde s_{-iT_i}) - g_{-iT_i}(\tilde s_{AT_i}, 0_{B-iT_i}) - \sum_{j \in B\setminus\{i\}} w_{jT_j} + w_{-i},$$

where $w_{-i}$ is the maximum proxy welfare of an allocation to $B \setminus \{i\}$.

Formalization targets

Goal: Theorem 5.1 (p. 17)

For separable SOS valuations, RS-VCG is ex-post IC and IR for every partition, and for every true profile $s$ and every feasible allocation $(S^*_i)$,

$$\sum_i v_{iS^*_i}(s_{S^*_i}) \le 4\, \mathbb{E}_B\Bigl[\sum_i v_{iT_i(B)}(s_{T_i(B)})\Bigr].$$

Milestones

1. Observation 2.2 (p. 12): a separable SOS valuation is SOS.
2. Display (5) (p. 17): $\mathbb{E}_B[w_{iT}\cdot\mathbf 1_{i\in B}] \ge \frac{v_{iT}(s_T)}{2}\cdot\frac12$ for every agent $i$ and bundle $T$.
3. Payment sign (p. 17): the payments $p_i(\tilde s)$ are nonnegative.
4. IC display (p. 18): for every partition, truthful reporting maximises each agent's utility.
5. IR display (p. 18): for every partition, the truthful utility is nonnegative.

Significance

The theorem shows that VCG-style reasoning survives interdependence when the dependence on other agents' information enters additively and submodularly: separability makes the payment absorb the effect of the others' signals, so that each agent of $B$ faces the proxy welfare as its objective. It gives a constant-factor welfare guarantee in ex-post equilibrium for combinatorial auctions with multidimensional interdependent signals, a setting in which exact efficiency is generically out of reach. The construction is the template for the paper's single-dimensional results in §6.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a reusable Lean model of interdependent-value combinatorial auctions (multidimensional signals, ex-post IC/IR, universal truthfulness of random mixtures) and of the SOS condition, and a checked account of the VCG accounting identity in this setting.

Difficulty

The approximation part rests on the Key Lemma 3.1: a uniformly random half of the other agents' signals set to zero keeps, in expectation, half of an SOS value. The obvious argument — monotonicity alone — gives no constant: with values depending on many signals, zeroing half of them can destroy almost all of the value, and the SOS condition is exactly what rules this out. The incentive part is where the obvious transfer of VCG fails: the proxy weight $w_{iT}$ of agent $i$ is not its value, and the true value $v_{iT}$ depends on signals that the proxy zeroes. Without separability, the payment of a VCG-style rule would itself depend on the agent's report (the paper's remark at the start of §5), and alignment of the agent's utility with the proxy objective breaks. Ties in the argmax and agents receiving the empty bundle must be handled for every tie-breaking rule.

Formalization scope

Agents are Fin n and items Fin m, with $n, m$ arbitrary; bundles are Finset (Fin m). Signals are NNReal, one per (agent, bundle), and $v_{iT}$ is a function of the bundle-$T$ signal vector. The empty bundle is worth $0$; monotonicity, strict own-signal monotonicity and the separable decomposition are assumed for nonempty bundles. The function $g_{-iT}$ is written on the whole vector with the hypothesis that it ignores coordinate $i$. The decomposition $(g, h)$ is data of the mechanism, since the payments use $g$.

The allocation is produced by an arbitrary selector returning a feasible maximiser of the proxy welfare for every partition and report; all statements hold for every such selector. $w_{-i}$ is a maximum over the finite set of feasible allocations to $B \setminus \{i\}$. Agents of $A$, and agents of $B$ that receive the empty bundle, pay $0$ (the paper defines payments for winners only). The expectation over the partition is the uniform average $2^{-n}\sum_{B \subseteq [n]}$, never an existential or universal over $B$; the approximation is stated for every feasible comparator allocation, with welfare at true values under truthful reports, never for proxy welfare or through a supremum. IC and IR are stated for each partition with the paper's explicit payments, not with existentially chosen payments.

A complete development needs finite averages over subsets, the Key Lemma 3.1 for SOS functions (posed in the companion mission on RS-V and not restated here), and finite argmax reasoning; the SOS layer and the combinatorial mechanism model are reusable for the other missions of this series. Proofs of the milestones, and of the d-SOS variant mentioned after the proof (a $2(d+1)$-approximation, not posed here), are welcome.

The source is the arXiv preprint arXiv:1903.08384v2 (2 June 2019); all page and display numbers refer to it, not to the journal version in Mathematics of Operations Research (2024).

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019; Mathematics of Operations Research, 2024. https://arxiv.org/abs/1903.08384
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00241
• S. Chawla, H. Fu, A. R. Karlin, Approximate Revenue Maximization in Interdependent Value Settings, EC 2014. https://doi.org/10.1145/2600057.2602858
• A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, EC 2018. https://arxiv.org/abs/1806.03865
• T. Roughgarden, I. Talgam-Cohen, Optimal and Robust Mechanism Design with Interdependent Values, ACM TEAC 4(3), 2016. https://doi.org/10.1145/2897185

Motivation

Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.

A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter $\gamma$, which measures how quickly a miner's operating cost grows with its scale, and the mining reward $R$. The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.

Setting

There are $n \ge 2$ active miners, indexed $i = 1, \dots, n$, with costs per hash $0 < c_1 \le c_2 \le \dots \le c_n$ (sorted, without loss of generality), a reward $R > 0$ and a capacity parameter $\gamma > 0$. Miner $i$ choosing hash rate $h_i$ earns $(h_i/H)R - c_ih_i - (\gamma/2)h_i^2$, where $H = \sum_j h_j$ is the aggregate hash rate (the paper's (3.4)). The cumulative cost is $c^{(n)} = c_1 + \dots + c_n$.

In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of $\gamma H^2 + c^{(n)}H - (n-1)R = 0$, and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:

$$g = g(c_1,\dots,c_n,\gamma,R) = \frac{\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} - c^{(n)}}{2\gamma},\qquad f_i = f_i(c_1,\dots,c_n,\gamma,R) = g\,\frac{R - c_i g}{R + \gamma g^2},$$

with $H^* = g$ and $h^*_i = f_i$. Miner $i$ is active exactly when $R - c_i g > 0$. The hash rate share of miner $i$ is $h^*_i/H^*$.

The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For $x \in \{\gamma, R\}$, (B.4) splits the derivative of $h^*_i$ into a direct part, $\Delta^{(x)}_{i,1} = \partial f_i/\partial x$ with $g$ held fixed, and an indirect part through the aggregate, $\Delta^{(x)}_{i,2} = (\partial f_i/\partial g)(\partial g/\partial x)$.

Formalization targets

Goal: Proposition 4.8 (p. 20)

For every active miner $i$,

$$\frac{\partial h^*_i}{\partial\gamma} = \Delta^{(\gamma)}_{i,1}+\Delta^{(\gamma)}_{i,2},\quad \Delta^{(\gamma)}_{i,1}<0,\quad \Delta^{(\gamma)}_{i,2}>0 \iff \frac{h^*_i}{H^*}<\frac12,$$ $$\frac{\partial h^*_i}{\partial R} = \Delta^{(R)}_{i,1}+\Delta^{(R)}_{i,2} > 0,\quad \Delta^{(R)}_{i,1}>0,\quad \Delta^{(R)}_{i,2}<0 \iff \frac{h^*_i}{H^*}<\frac12,$$

and the derivatives of $h^*_i/H^*$ with respect to $\gamma$ and to $R$ are increasing in $i$, for $1 \le i \le n$.

Milestones (the steps of the appendix proof)

1. (B.2), p. 39: $\partial H^*/\partial\gamma = -(H^*)^2/(c^{(n)}+2\gamma H^*) < 0$ and $\partial H^*/\partial R = (n-1)/(c^{(n)}+2\gamma H^*) > 0$.
2. p. 40: $\partial f_i/\partial\gamma = -g^3(R-c_ig)/(R+\gamma g^2)^2 < 0$ and $\partial f_i/\partial R = g^2(c_i+\gamma g)/(R+\gamma g^2)^2 > 0$.
3. (B.4), pp. 40–41: closed forms of $\partial h^*_i/\partial\gamma$ and $\partial h^*_i/\partial R$.
4. (B.6), pp. 42–43: closed forms of the share derivatives, and the p. 43 rewrites in which $i$ enters only through $f_i$ and $c_i + \gamma f_i$.

Significance

The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger $\gamma$ lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the $\gamma$ and $R$ columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).

Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the $\gamma$ and $R$ directions, the sign analysis, and the monotonicity in $i$. The proof text on p. 43 says "decreasing in $i$" where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).

Difficulty

Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate $g$ is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity $\gamma g^2 + c^{(n)}g = (n-1)R$, i.e. $\sqrt{(c^{(n)})^2+4(n-1)R\gamma} = c^{(n)} + 2\gamma g$, and the first-order identity $c_i + \gamma f_i = (R/g)(1 - f_i/g)$. The sign of the indirect parts is not visible from the raw derivative: it requires rewriting $\partial f_i/\partial g$ so that the threshold $f_i/g = 1/2$ appears. The positivity of $\partial h^*_i/\partial R$ needs a separate bound, since its indirect part can be negative. The monotonicity in $i$ is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on $f_i$ (decreasing in $i$) from that on $c_i + \gamma f_i$ (increasing in $i$), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.

Formalization scope

Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner $i+1$, so "increasing in $i$" is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost ($c^{(n)}$), gH ((4.1)/(B.3), with both branches of (4.1)), fH ($f_i$ with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: $n\ge2$, $R>0$, $\gamma>0$, $c_k>0$, costs sorted, and $R - c_kg > 0$ for every $k$ (all $n$ miners active). The condition $\gamma > 0$ is the paper's: (B.3) defines $g$ only for $\gamma>0$. The definition Sensitivities defines the four $\Delta$'s as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.

The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That $f_i$ and $g$ are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and $\partial f_i/\partial g$ are posed in mission 2. This mission uses those identities but does not pose them.

Trivializing formalizations are ruled out: the $\Delta$'s are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with $c = (1,1)$, $\gamma = 1$, $R = 3$ give $g = 1$, $h^*_i = 1/2$); and the monotonicity is stated for derivatives asserted to exist.

Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for $g$ (the root identity, positivity, $c^{(n)}+2\gamma g > 0$) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.

Selected references

• A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint, 2021. https://arxiv.org/abs/2106.09783v1
• G. Tullock, The Welfare Costs of Tariffs, Monopolies, and Theft, Western Economic Journal 5(3), 224–232, 1967 (the rent-seeking model the paper builds on). https://doi.org/10.1111/j.1465-7295.1967.tb01923.x
• S. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. https://bitcoin.org/bitcoin.pdf

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack $\varepsilon$. Approximate incentive compatibility ($\varepsilon$-IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.

Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With $\varepsilon$-IC the feasible set grows, and the paper determines the order of the additional revenue as $\varepsilon\downarrow 0$.

Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an $\varepsilon$-IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by $O(\sqrt\varepsilon)$ for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only $\Theta(\varepsilon)$ (Theorem 2), and give a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.

Setting

A seller sells one item to one buyer. The buyer's value $v$ has a cumulative distribution function $F$ with density $f$ supported on $S=[0,\bar v]$, $\bar v>0$. Assumption 1 requires $f$ to have bounded variation on $S$. Write $\bar F=1-F$, the revenue curve $R(v)=v\,\bar F(v)$ (the revenue of a posted price $v$), and $\dot R(v)=\bar F(v)-v f(v)$.

A direct mechanism $m=(x,t)$ gives a buyer who reports $v$ the item with probability $x(v)\in[0,1]$ and charges $t(v)$. It is individually rational (IR) if $v\,x(v)-t(v)\ge 0$ for all $v\in S$, and $\varepsilon$-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S.$$

$\mathcal M(\varepsilon)$ is the set of IR and IC$_\varepsilon$ mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$. A best reporting mapping $v^\star$ for $m$ picks, for each value $v$, a report in $\arg\max_{w\in S}\{v\,x(w)-t(w)\}$.

Local $\alpha$-power envelopes (Definition 1): $R$ has a unique maximizer $p^\star$ on $S$, interior, and there are $\alpha>1$, $\kappa_L,\kappa_U>0$ and $\ell>0$ with $(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ and

$$\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\,\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\quad\text{on }(p^\star-\ell,p^\star+\ell).$$

The parameter $\alpha$ measures how flat $R$ is at its peak; $\alpha=2$ is the generic smooth case.

Perturbed delayed mechanisms (§5.1). For $\mu,\delta>0$ the buyer is steered to report $v^\star(v\,|\,\mu,\delta)$, equal to $0$ below $p^\star-\delta$, to $v-\mu$ on $[p^\star-\delta,p^\star+\delta+\mu]$, and to $p^\star+\delta$ above. With $w$ its generalized inverse, the allocation $x_{pd}$ solves on $[0,p^\star+\delta]$ the ordinary and delay differential equations

$$\dot x(v)=\frac{x(v)}{w(v)-v}\ \ (v\le p^\star-\delta),\qquad x(0)=\frac{\varepsilon}{p^\star-\delta},\qquad \dot x(v)=\frac{x(v)-x(v^\star(v))}{w(v)-v}\ \ (p^\star-\delta\le v\le p^\star+\delta),$$

is $1$ above $p^\star+\delta$, and the payment $t_{pd}$ is given explicitly in terms of $x_{pd}$ and $v^\star$.

Formalization targets

Goal: Theorem 3 (p. 27)

Under Assumption 1 and local $\alpha$-power envelopes there are $C>0$ and $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ some $m\in\mathcal M(\varepsilon)$ satisfies

$$\Pi(m)\ \ge\ \Pi^\star(\mathcal M(0))+C\,\varepsilon^{\alpha/(2\alpha-1)} .$$

The constants may depend on the distribution, but not on $\varepsilon$.

Milestones

1. Lemma 5 (p. 59): solutions of (ODE)-(DDE) are non-decreasing on $[0,p^\star+\delta]$.
2. Proposition 3 (p. 31): if $x_{pd}(v)\to 1$ as $v\uparrow p^\star+\delta$, then $v^\star(\cdot\,|\,\mu,\delta)$ is a best reporting mapping for $m_{pd}$.
3. Proposition 4 (p. 33): the system has a unique solution on $[0,p^\star+\delta]$, which is positive, non-decreasing and given in closed form (eq. (25)).
4. Lemma 6 (p. 60): with $\Gamma(t)=\sum_{j=0}^{\lfloor t\rfloor+1}\frac{(-1)^je^{-j}}{j!}(t+1-j)^j$,

$$2(t+1)e^{-1}e^{-t}<\Gamma(t)\le2(t+2)e^{-(t+1)}\qquad(t\ge0).$$

5. Proposition 5 (p. 34): for $\mu>\varepsilon e$ some $\delta\in[\mu^2/(4\varepsilon)-\mu,\ \mu^2/(4\varepsilon)]$ makes $x_{pd}$ reach $1$ at $p^\star+\delta$, and then $m_{pd}\in\mathcal M(\varepsilon)$.
6. Proposition 6 (p. 35): the revenue identity

$$\Pi(m_{pd})=\int_0^{p^\star+\delta}x_{pd}(v)\big(vf(v)-\bar F(v+\mu)\dot w(v)\big)dv+R(p^\star+\delta)+\int_{p^\star+\delta}^{p^\star+\delta+\mu}\bar F(v)\,dv .$$

Significance

The result. Theorem 3 shows that the $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound of Theorem 1 is tight up to the logarithm. Since $\alpha/(2\alpha-1)<1$ for $\alpha>1$, the revenue gain from approximate incentive compatibility is supralinear in $\varepsilon$: a seller who exploits $\varepsilon$-optimizing buyers gains strictly more than the order-$\varepsilon$ gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature $\alpha$ of the revenue curve at the optimal price determines the exponent, which ranges from $1$ (as $\alpha\downarrow1$) to $1/2$ (as $\alpha\to\infty$), the latter matching Nisan's universal bound.

Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of $\varepsilon$-IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on $\Gamma$, which the paper derives from the renewal function of uniform interarrival times.

Difficulty

The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order $\varepsilon$ (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples $x(v)$ to $x(v-\mu)$); choosing the delay $\delta$ so that the allocation reaches exactly $1$ at $p^\star+\delta$, which requires the sharp two-sided bound on $\Gamma$ and an intermediate value argument; and verifying global $\varepsilon$-IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain $\bar F(p^\star+\delta+\mu)\,\mu$ against losses of order $\kappa_U(\delta+\mu)^\alpha$, with $\mu$ of order $\varepsilon^{\alpha/(2\alpha-1)}$.

Formalization scope

Values are reals, every function is a total function $\mathbb R\to\mathbb R$ whose values matter only on $S=[0,\bar v]$, and the density is integrable on $S$ with total mass $1$. Mechanisms are required to be measurable, which the expectation $\mathbb E_v[t(v)]$ presumes. $\Pi^\star$ is a supremum (sSup); the goal is stated with an explicit witness $m\in\mathcal M(\varepsilon)$, which is equivalent because the revenue image is nonempty and bounded above by $\bar v$. $\dot R$ is defined as $\bar F-vf$, not as a derivative. The $\Omega$ constants are quantified after the distribution and before $\varepsilon$.

The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At $p^\star-\delta$ the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.

Disclosed additions relative to the page: $\mu\le p^\star-\delta$ in the §5.1 statements (presumed by the paper's definition of $w$); Propositions 3–6 and Lemma 5 are stated for any price $p^\star$ with $0<\delta<p^\star$ and $p^\star+\delta+\mu<\bar v$, since their proofs never use optimality of $p^\star$; in Proposition 6 the integrand $\psi\cdot f$ is written in product form because $\psi$ divides by $f$.

A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and $\Gamma$ results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, FOCS 2005, 605–614. https://doi.org/10.1109/SFCS.2005.50
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• R. D. Driver, Ordinary and Delay Differential Equations, Springer, 1977 (reprint 2012). https://doi.org/10.1007/978-1-4684-9467-9

Motivation

Fair division asks how to split a divisible resource among $n$ agents whose preferences differ. In the non-atomic ("cake-cutting") model the resource is a region of Euclidean space and an agent values each measurable piece. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research, 2023) study fair guarantees: utility levels that a division rule lets every agent secure for herself, whatever the other agents' preferences and behaviour. Two numbers bracket every such guarantee. Maxmin is an upper bound on any fair guarantee, and minMax is what Kuhn's Divide & Choose rule secures for arbitrary continuous preferences (Theorem 1 of the paper; a companion mission formalizes it).

For utilities that are monotone in the share (the manna is unanimously good), the authors ask whether rules of a different shape improve on minMax. They consider the classical Moving Knife rules, where a knife sweeps the manna and agents shout "stop", and introduce Bid & Choose rules, where a clock runs and the agent who stops it picks any share of a prescribed size. Each rule comes with a computable guarantee, $\Gamma^\kappa$ for the knife and $\Gamma^\theta$ for Bid & Choose. The question this mission formalizes is where these guarantees sit relative to the two benchmarks.

Setting

The manna $\Omega$ is a bounded measurable subset of $\mathbb R^d$, $d\ge1$, with Lebesgue measure $|\cdot|$ and $|\Omega|>0$. A share is a measurable $S\subseteq\Omega$. Shares are compared by the pseudo-metric $\delta(S,T)=|S\,\triangle\,T|$. A utility $u\in\mathcal D(\Omega)$ is a bounded, $\delta$-continuous function on shares with $u(\emptyset)=0$; it lies in $\mathcal M^+(\Omega)$ if $S\subseteq T$ implies $u(S)\le u(T)$.

An $n$-partition of $\Omega$ is a tuple of shares $(S_i)_{i=1}^n$ with union $\Omega$ and pairwise null overlaps; it is an equipartition for $u$ if all $u(S_i)$ are equal. The benchmarks are

$$\mathit{minMax}(u;n)=\inf_{\Pi}\max_i u(S_i),\qquad \mathit{Maxmin}(u;n)=\sup_{\Pi}\min_i u(S_i),$$

over all $n$-partitions $\Pi$.

A moving knife $\kappa$ is a $\delta$-continuous path $t\mapsto K(t)$ of shares on $[0,1]$ from $K(0)=\emptyset$ to $K(1)=\Omega$ with $|K(t')\setminus K(t)|>0$ whenever $t<t'$. A benchmark measure $\theta$ is a probability measure on $\Omega$, mutually absolutely continuous with Lebesgue measure on $\Omega$. Write $\Upsilon(n)$ for the sequences $0=t^0\le t^1\le\dots\le t^n=1$, and

$$u^\kappa(t^1,t^2)=u\big(K(t^2)\setminus K(t^1)\big),\qquad u^\theta(t^1,t^2)=\inf_{T:\,\theta(T)=t^1}\ \sup_{S:\,S\cap T=\emptyset,\ \theta(S)=t^2-t^1}u(S).$$

For $\alpha\in\{\kappa,\theta\}$ the guarantees are

$$\Gamma^\alpha(u;n)=\sup_{\tau\in\Upsilon(n)}\ \min_{0\le k\le n-1}u^\alpha(t^k,t^{k+1}).$$

Formalization targets

Goal: Theorem 2 iii), the provable part

For $n\ge1$, $u\in\mathcal D(\Omega)\cap\mathcal M^+(\Omega)$, every moving knife $\kappa$ and every benchmark measure $\theta$:

$$\mathit{minMax}(u;n)\le\Gamma^\kappa(u;n)\le\mathit{Maxmin}(u;n),\qquad \Gamma^\theta(u;n)\le\mathit{Maxmin}(u;n).$$

The paper also claims $\mathit{minMax}(u;n)\le\Gamma^\theta(u;n)$. That inequality is false and is not posed. Take $\Omega=[0,1]$, $\theta$ Lebesgue measure and $n=2$. There is an increasing continuous $u$, built from dyadic "spike" sets, for which $\Gamma^\theta(u;2)\le0.075$ while every 2-partition has a share worth about $0.9$.

Milestones

1. $u^\kappa$ and $u^\theta$ decrease weakly in $t^1$ and increase weakly in $t^2$ (p. 19).
2. Lemma 4 i), knife part: $u^\kappa$ is continuous on the triangle $0\le t^1\le t^2\le1$.
3. Lemma 4 ii), knife part: $\Gamma^\kappa(u;n)$ is attained at a $\tau\in\Upsilon(n)$ equalising all $u^\kappa(t^k,t^{k+1})$.
4. An equalising knife sequence cuts $\Omega$ into an $n$-equipartition (proof of Theorem 2).
5. The trimming step and Proposition 1 ii): for $u\in\mathcal M^+(\Omega)$, minMax and Maxmin are the infimum and supremum of equipartition utilities.
6. For every $\tau\in\Upsilon(n)$, $\min_k u^\theta(t^k,t^{k+1})\le\mathit{Maxmin}(u;n)$ (p. 20).

A further item records what the page's left-hand argument for $\theta$ does prove: $\mathit{minMax}(u;n)\le\max_k u^\theta(t^k,t^{k+1})$ for every $\tau\in\Upsilon(n)$.

Significance

The goal shows that, for a good manna, a Moving Knife rule is never worse than Divide & Choose by the minMax measure and never promises more than the Maxmin ceiling. Bid & Choose likewise never exceeds Maxmin. Since Maxmin profiles need not be feasible (the paper's Leontief example, p. 16), these inequalities locate the new guarantees inside the only interval where fair guarantees can live.

The mission also corrects the record. The paper is published, but its Lemma 4 and Theorem 2 iii) as printed in the arXiv v3 preprint are not right for $\theta$. Lemma 4 i) asserts continuity of $u^\theta$ and Lemma 4 ii) the existence of an equalising $\theta$-sequence, and both fail for some $u\in\mathcal M^+([0,1])$. The left-hand θ-inequality fails as well. The mission states only true claims and leaves precise statements on record. As far as we know none of these results has been machine-checked. The platform has no prior cake-cutting, moving-knife or equipartition development, so the definitions here are new.

Difficulty

The knife sandwich hinges on an equalising sequence. One must show that $u^\kappa$ is jointly continuous and run an $n$-step intermediate value argument whose optimality proof needs the two-sided monotonicity of $u^\kappa$. Proposition 1 ii) needs the trimming step. A share must be continuously shrunk inside $\mathbb R^d$ while its utility is tracked, and then iterated across $n$ shares while all trimmed shares are kept equal. This is the longest argument in the mission.

For $\theta$, the natural first idea is to copy the knife argument: prove $u^\theta$ continuous, then equalise. It fails, because $u^\theta$ is an inf–sup over the non-compact space of shares and can jump. The right-hand inequality has to hold for every $\tau$ without any attainment, and any argument for it requires shares of every prescribed $\theta$-size, i.e. a non-atomicity (Sierpiński-type) argument for $\theta$.

Formalization scope

Space: EuclideanSpace ℝ (Fin d) with volume, and $d\ge1$ is assumed in every theorem, because in $\mathbb R^0$ Lebesgue measure is a point mass, which the paper's non-atomic model excludes. Utilities are functions on all subsets, constrained on shares only. Partitions are Fin n-indexed, with union exactly $\Omega$ and null pairwise overlaps (not disjointness). Every min/max of the paper is an inf/sup (sInf, sSup), as the paper itself says on p. 9. Each defining set is nonempty and bounded for $n\ge1$, which every theorem assumes. Knife continuity is $\varepsilon$–$\eta$ continuity for $\delta$ on $[0,1]$. $\theta$ is mutually absolutely continuous with volume.restrict Ω, with $\theta(\Omega)=1$. $u^\theta$ quantifies over shares $S,T$, with exact disjointness and exact $\theta$-sizes. Only $\mathcal M^+(\Omega)$ is treated, as Theorem 2 states.

Ruled out: $\Gamma$ as a supremum over a possibly empty set, an inner supremum in $u^\theta$ over arbitrary sets, the sandwich without monotonicity of $u$, a single rule in place of both, and $\Gamma^\alpha$ replaced by its value at one particular $\tau$. None of these is the paper's statement, and some are trivially true.

Needed infrastructure: δ-continuity of set-valued paths, existence of measurable subsets of prescribed measure for non-atomic measures on $\mathbb R^d$, and intermediate-value arguments in several variables. The model definitions are reusable for any non-atomic fair-division development. Proofs of any item are welcome, as are formal versions of the counterexamples to the θ claims.

Selected references

• A. Bogomolnaia, H. Moulin, Guarantees in Fair Division: General or Monotone Preferences, Mathematics of Operations Research, 2023; preprint arXiv:1911.10009v3, 2020. https://arxiv.org/abs/1911.10009
• S. Avvakumov, R. Karasev, Envy-free Division under Mapping Degree, 2019. https://arxiv.org/abs/1907.11183

Motivation

Ride hailing, online advertising and kidney exchange share a decision problem: resources that are present from the start must be matched, irrevocably and one at a time, to requests that arrive at random. When the arrival probabilities are known in advance, the natural benchmark for an online algorithm is not the offline optimum (the "prophet", who sees every arrival in advance) but the optimal online algorithm: the best expected profit any algorithm can earn when it must decide without seeing the future. That benchmark is well defined and computable in exponential time, so the question becomes one of approximation algorithms: how much of it can a polynomial-time algorithm guarantee?

Papadimitriou, Pollner, Saberi and Wajc (arXiv:2102.10261, Math. Oper. Res. 2024) answer both halves of that question for online Bayesian bipartite matching. They show that approximating the optimal online algorithm within some constant $\alpha<1$ is PSPACE-hard (Theorem 1.1, not part of this mission), and they give a polynomial-time algorithm that earns a $0.51$ fraction of it (Theorem 1.2). The number matters because $1/2$ is the best possible ratio against the prophet, already for a single bin, so $0.51$ shows that comparing with the online optimum genuinely permits better guarantees.

Timeline:

• 1978: Krengel and Sucheston's prophet inequality: for a single item, no online algorithm earns more than $1/2$ of the offline optimum in the worst case, and $1/2$ is achievable.
• 2015–2020: $1/2$-competitive algorithms against the offline optimum for unit-demand combinatorial auctions (Feldman, Gravin and Lucier, SODA 2015) and for online stochastic max-weight matching with vertex arrivals (Ezra, Feldman, Gravin and Tang, EC 2020).
• 2017: Torrico and Toriello's LP relaxations for online bipartite matching (arXiv:1709.01557), which imply that LP-Match bounds the optimal online algorithm (Lemma 4.1 here).
• 2021: this paper, $0.51$ of the online optimum by rounding LP-Match online.
• 2021: Saberi and Wajc's online edge-colouring algorithm (ICALP 2021), whose ideas improve the ratio of Theorem 1.2 to $0.526$ (as reported on p. 4 of the paper).

Setting

A RideHail instance $I$ has a finite set of bins (taxis) $i$ and balls (passengers) $t=1,\dots,n$, revealed in this fixed order. Ball $t$ arrives with probability $p_t\in[0,1]$, independently of every other ball. If it arrives it may be matched, irrevocably and before ball $t+1$ is revealed, to an unmatched bin $i$, earning $w_{i,t}\ge 0$. A deterministic online policy chooses the bin for ball $t$ as a function of the arrivals of balls $1,\dots,t$ only. Its expected profit is the average, over the $2^n$ arrival patterns, of the total weight of the matching it builds, and $\mathrm{OPT}_{on}(I)$ is the largest expected profit over all such policies.

LP-Match is the linear program in variables $x_{i,t}$, read as "the probability that the algorithm matches $t$ to $i$":

$$\max \sum_{i,t} w_{i,t}x_{i,t}\ \ \text{s.t.}\ \ \sum_t x_{i,t}\le 1,\ \ \sum_i x_{i,t}\le p_t,\ \ x_{i,t}\le p_t\Big(1-\sum_{t'<t}x_{i,t'}\Big),\ \ x_{i,t}\ge 0.$$

Its optimal value is $\mathrm{LP\text{-}Match}(I)$. The third family of constraints, (11), holds for online algorithms only.

Algorithm 1 (Rounding LP-Match Online), with $c=0.01$, takes an optimal solution $x$ of LP-Match, adds a weight-zero dummy bin for each ball so that $\sum_i x_{i,t}=p_t$, and then processes the balls in order. When ball $t$ arrives it picks a bin $i$ with probability $x_{i,t}/p_t$. If $i$ is vacant, $(i,t)$ is matched with probability

$$q_{i,t}=\min\Big(1,\ \frac{1/2+c}{1-\sum_{t'<t}x_{i,t'}(1/2+c)}\Big).$$

If $t$ is still unmatched, it picks again from the same distribution, and is matched to the new pick when that bin is vacant and $\sum_{t'<t}x_{i,t'}>\frac{1/2-c}{1/2+c}$. Edges added by the first pick form $M_1$, those added by the second pick form $M_2$, and $M=M_1\sqcup M_2$.

Formalization targets

Goal: Theorem 1.2

For every instance $I$ and every optimal solution $x$ of LP-Match,

$$\mathbb E\Big[\sum_{(i,t)\in M}w_{i,t}\Big]\ \ge\ 0.51\cdot \mathrm{OPT}_{on}(I),$$

where $M$ is the output of Algorithm 1 run on $x$.

The path

The milestones follow the paper's proof. LP-Match is a relaxation of the online problem (Lemma 4.1). Algorithm 1 matches every edge with probability at least $x_{i,t}(1/2+c)$ (Theorem 4.2), which rests on two bounds:

• the first-pick analysis, Lemma 4.4 with the vacancy bounds of Corollary 4.5;
• the second-pick bound, Theorem 4.6. It uses Equation (20), Lemma 4.7, the covariance bound of Lemma 4.8 and the conditioning bound of Lemma 4.11.

Lemma 4.8 comes from the negative association of early-occupancy indicators: Lemma 4.9 and Corollary 4.10, resting on Definition 2.5 and Propositions 2.6–2.8.

Significance

The result. Theorem 1.2 is the first polynomial-time algorithm for online stochastic matching with a ratio above $1/2$ against the optimal online algorithm. It separates the online benchmark from the prophet benchmark in an algorithmic sense, and its main technical step, bounding positive correlation between bins' matched statuses through negative association, has been reused for online edge colouring.

Formalizing it. The result is proved on paper and is not machine-checked anywhere. The mission produces:

• a formal model of online Bayesian matching, with the optimal online policy as a benchmark;
• a formal LP relaxation and its validity for online policies;
• a formal statement of a randomized online rounding scheme and its per-edge guarantee.

The negative-association layer (Definition 2.5, Propositions 2.6–2.8) is general probability, absent from Mathlib, and reusable well beyond this mission.

Difficulty

The obvious argument fails at the second pick. Once ball $t$ has been rejected by its first pick, the events "bin $i$ is vacant" and "the first pick was rejected" are dependent, for two reasons:

1. The second pick may re-draw the very bin that just rejected.
2. Bins' occupancy statuses may be positively correlated, so a rejection by one bin makes the others likely occupied too.

Either effect alone can make the second pick useless. The first is controlled by Constraint (11) (Lemma 4.7). The second needs a quantitative bound on the covariance of vacancy indicators (Lemma 4.8), proved by splitting occupancy into early and late parts and showing that the early parts are negatively associated, through a coupling of the algorithm's randomness with independent pick and coin variables. Lemma 4.1 is also not routine to formalize: it requires turning an arbitrary history-dependent online policy into a feasible LP solution, using the independence of arrivals from past decisions.

Formalization scope

Conventions committed to in Lean (namespace OnlineMaxWeightMatch.Approx):

• Bins form a finite type ι; balls are Fin n in arrival order (paper ball $t$ is index $t-1$). Weights and probabilities are real numbers with $w\ge 0$ and $0\le p_t\le 1$; missing edges have weight $0$.
• $\mathrm{OPT}_{on}(I)$ is the supremum over deterministic non-anticipating policies: the choice for ball $t$ is a function of the arrival indicators of balls $s\le t$. Randomized online algorithms are mixtures of these and add nothing. Policies never see later arrivals; comparing against the prophet would make the goal false.
• $\mathrm{LP\text{-}Match}(I)$ is the supremum of the objective over the feasible set (9)–(12), which is nonempty and compact.
• Algorithm 1's randomness is a finite product space: for each ball, an arrival bit, a first pick, one acceptance coin per bin and a second pick, all independent. $M$, $M_1$, $M_2$ are computed from an outcome by recursion over the balls.
• Picks are Option-valued: "no bin" carries the leftover mass $1-\sum_i x_{i,t}/p_t$. When $p_t=0$, $x_{i,t}/p_t$ is $0$ in Lean and the ball never arrives.
• Dummy bins are genuine bins of type ι ⊕ Fin n with weight $0$. A dummy first pick is accepted with probability $1/2+c$ and consumes the ball's turn, as in the paper. A dummy is never matched as a second pick.
• $c$ is the fixed constant $1/100$, not a parameter.
• The milestones are stated for any LP-Match-feasible $x$ with $\sum_i x_{i,t}=p_t$ (the paper's standing assumption); the goal does the augmentation and assumes optimality only.
• Conditional probabilities use ProbabilityTheory.cond, which is $0$ on null events. Equation (20) and Lemma 4.7 therefore carry positivity hypotheses ($x_{j,t}>0$, $p_t>0$) that make the conditioning event non-null.
• Negative association uses bounded, measurable, non-decreasing test functions; covariances are ProbabilityTheory.covariance.

"Polynomial time" is not formalized. Because "some online algorithm earns $0.51\cdot\mathrm{OPT}_{on}$" is trivially true of the optimal online algorithm itself, the goal names Algorithm 1 run on an arbitrary optimal LP-Match solution. That solution exists, so the goal is not vacuous. Replacing $\mathrm{OPT}_{on}$ by an offline benchmark, dropping Constraint (11), restricting to non-adaptive policies, or treating the dummy pick as "pick nothing" would each change the theorem.

Infrastructure a complete development needs: negative association with its closure properties, finite product probability spaces, conditioning on events, covariance of indicators, and linear-programming feasibility arguments for online policies. Contributions to any milestone are welcome; the probability layer (Propositions 2.6–2.8) is independent of the rest.

Selected references

• C. Papadimitriou, T. Pollner, A. Saberi, D. Wajc, Online Stochastic Max-Weight Bipartite Matching: Beyond Prophet Inequalities, arXiv:2102.10261v3 (2021); Mathematics of Operations Research (2024). https://arxiv.org/abs/2102.10261
• K. Joag-Dev, F. Proschan, Negative Association of Random Variables, with Applications, Annals of Statistics 11(1):286–295, 1983. https://doi.org/10.1214/aos/1176346079
• D. Dubhashi, D. Ranjan, Balls and Bins: A Study in Negative Dependence, BRICS Report Series 3(25), 1996; Random Structures & Algorithms 13(2), 1998. https://doi.org/10.1002/(SICI)1098-2418(199809)13:2<99::AID-RSA1>3.0.CO;2-M
• A. Torrico, A. Toriello, Dynamic Relaxations for Online Bipartite Matching, arXiv:1709.01557, 2017. https://arxiv.org/abs/1709.01557
• T. Ezra, M. Feldman, N. Gravin, Z. G. Tang, Online Stochastic Max-Weight Matching: Prophet Inequality for Vertex and Edge Arrival Models, EC 2020. https://doi.org/10.1145/3391403.3399513
• A. Saberi, D. Wajc, The Greedy Algorithm Is Not Optimal for On-Line Edge Coloring, ICALP 2021. https://doi.org/10.4230/LIPIcs.ICALP.2021.109