Operations Research

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

1. The exponential and linear functions with $\alpha=1/2$ are effective (p. 9).
2. 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}]$.
3. Equation (7) (p. 10): $a(e)\Pr[e\text{ is free}]\ge\tilde a(p_ey_e)\Pr[e\text{ is safe}]$.
4. 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$.
5. §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

Motivation

In a budget-feasible procurement auction a buyer with a hard budget $B$ acquires services from strategic sellers. Each seller $i$ has a private cost $c_i$, and the buyer values a set $S$ of hired sellers at $v(S)$. The auction must keep total payments within $B$ and make truthful behaviour optimal for every seller, while hiring a set whose value is close to the best set affordable at the true costs. The problem was introduced by Singer (FOCS 2010) and models crowdsourcing markets, influence maximization and data acquisition.

The known constant-factor auctions for monotone submodular valuations were sealed-bid and, for the most part, randomized: they choose between two candidate sets uniformly at random, or estimate the optimum from a random sample of the bidders. Amanatidis et al. named the existence of deterministic budget-feasible $O(1)$-approximation mechanisms for submodular valuations as the most intriguing open problem of the area. Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) answer it with a deterministic, polynomial-time mechanism with factor $4.75$, which is moreover a descending clock auction: each seller only sees a non-increasing sequence of take-it-or-leave-it prices, so the auction is obviously strategyproof and weakly group strategyproof.

Timeline, as recorded in the paper:

• 2010: Singer, the first constant-factor budget-feasible mechanism for monotone submodular valuations.
• 2011: Chen, Gravin and Lu, mechanisms for additive and monotone submodular valuations, and the lower bound $1+\sqrt2$ on the approximation factor already for additive valuations.
• Jalaly and Tardos (ACM TEAC 2021), a randomized $5$-approximation for monotone submodular valuations, the best factor before this paper.
• 2021: Balkanski et al., Iterative-Pruning, deterministic, factor $4.75$ (this mission).

Setting

There are $n$ bidders $N$. The valuation $v : 2^N \to \mathbb R_{\ge 0}$ is monotone ($v(S) \le v(T)$ for $S \subseteq T$) and submodular ($v(S)+v(T) \ge v(S\cap T)+v(S\cup T)$). Write $v(T \mid S) = v(S\cup T) - v(S)$ for a marginal contribution. Costs satisfy $c_i \ge 0$ and the budget is $B > 0$. A set $O$ is budget feasible if $\sum_{i\in O} c_i \le B$, and $\mathrm{OPT}$ is the largest value of such a set.

Iterative-Pruning works in phases. Phase 1 puts the single most valuable bidder in $S_1$ and sets the target $\widetilde{\mathrm{OPT}}_1 = v(S_1)$; all prices start at $B$. Each later phase $t$ doubles the target, $\widetilde{\mathrm{OPT}}_t = 2\widetilde{\mathrm{OPT}}_{t-1}$, sets aside the previous set $S_{t-1}$, and builds a new set $S_t$ greedily: the remaining bidder $i$ with the largest marginal contribution $v(\{i\}\mid S_t)$ is offered

$$p_i \leftarrow \min\{p_i,\; v(\{i\}\mid S_t)\cdot B/\widetilde{\mathrm{OPT}}_t\},$$

joins $S_t$ if she accepts and leaves the auction for good if she rejects. A phase ends when $v(S_t) \ge \widetilde{\mathrm{OPT}}_t$ or no bidder is left to ask; the auction ends at the phase $\hat t$ after which every active bidder is in $S_{\hat t-1} \cup S_{\hat t}$. A pruning step then makes $W_1 = S_{\hat t-1}$ budget feasible by re-offering its last bidder a lower price, and Maximize-Value returns the better of $W_1$ and $W_3 = W_2 \cup T$, where $W_2$ is the longest budget-feasible prefix of $\overline W_2 = S_{\hat t}$ and $T$ the longest prefix of $W_1$ that still fits.

Formalization targets

Goal: Theorem 1

With $(W, p)$ the winning set and the final prices of Iterative-Pruning,

$$\sum_{i\in W} p_i \le B \qquad\text{and}\qquad v(O) \le 4.75\, v(W)\ \text{ for every } O \subseteq N \text{ with } \textstyle\sum_{i\in O} c_i \le B.$$

Milestones

The benchmark $\mathrm{OPT} \le v(W_1\cup\overline W_2) + v(R\mid W_1\cup\overline W_2)$ (p. 7); Lemma 2, the bound $(3/2 - 1/2^{\hat t-2})\,\widetilde{\mathrm{OPT}}_{\hat t}$ on the value lost through rejections (p. 7); Lemma 3, the value kept when the last bidder of an over-budget set is dropped (p. 9); the lower bound on $v(T)$ and the incompatibility of the three constraints at $\rho \ge 4.75$ (Appendix A.1, pp. 20–21); Lemma 9 ($\hat t \le 2$, factor 4); Lemma 10 ($\overline W_2$ over budget, factor 3.75); Lemma 11 (budget feasibility). A companion item states Lemma 4: some instance has $\mathrm{OPT} > (4.5-\varepsilon)\,v(W)$.

Significance

The theorem shows that determinism, polynomial time, a constant approximation factor and the clock-auction format can be had together for monotone submodular valuations, which answers the open question of Amanatidis et al.; the factor $4.75$ also improves on the best randomized factor $5$. Clock prices are computed from public information only, so any budget-feasible selection rule can be plugged into the final step without affecting incentives, and the backward-greedy pruning technique is reused in the paper for non-monotone submodular and subadditive valuations.

The paper's proof is a case analysis whose details are partly deferred and partly informal: the printed proof of Lemma 2 needs a repair of one step, Lemma 2 is false for $\hat t = 2$ (the formal version requires $\hat t \ge 3$, which is all the main proof uses), and one sub-case of Lemma 9 is referred to an appendix argument written for $\hat t \ge 3$. A machine-checked proof settles that the factor $4.75$ holds for every run, including all short runs, ties and degenerate valuations. As far as is known, no part of this theory (budget-feasible mechanisms, clock auctions) is formalized in Lean or any other proof assistant.

Difficulty

The obvious argument would compare the greedy set of the last phase directly with $\mathrm{OPT}$. It fails because the greedy order and the prices interact across phases: a bidder rejected in an early phase was rejected against an earlier, smaller set and target, and the prices that make $W_1$ affordable were set in the previous phase. The proof must therefore track, for each rejected bidder, the phase and the set against which she rejected, and combine the bounds over all phases with a geometric sum. The final constant comes out of an optimization over the unused budget fraction $u$, the relative value $\alpha$ of $W_1$ and the relative loss $\beta$, which is tight at $\hat t = 3$.

Formalization scope

Bidders are Fin n; sets are Finset (Fin n); the ordered sets of the mechanism are duplicate-free List (Fin n). Valuations are real valued with non-negativity, monotonicity and submodularity as hypotheses (the platform definition NonmonotoneSubmod.Shared.Submodular); no normalization $v(\emptyset) = 0$ is assumed. Costs are non-negative, and the budget is assumed positive ($B > 0$), an addition to §2.

The mechanism is constructed, not axiomatized: one definition item implements Mechanism 1 and Algorithm 2 line by line, with an explicit state (active bidders, $S_{t-1}$, $S_t$, target, phase, prices). A bidder accepts a price $x$ iff $c_i \le x$. Every argmax is broken toward the least index. The outer loop is cut after $n+2$ phases beyond the first; for $\max_i v(\{i\}) > 0$ the mechanism stops earlier on its own, and for $\max_i v(\{i\}) = 0$ (constant $v$), where the paper's loop never ends, the cut is harmless. The output $W$ is $W_1$ when $v(W_3) \le v(W_1)$. Approximation is stated as $v(O) \le 4.75\,v(W)$ for every budget-feasible $O$, with no supremum and no division.

A trivializing formalization is ruled out: the goal assumes nothing about $\hat t$, $W_1$, $\overline W_2$, $R$ or the targets; those appear only in the milestones, and the lemmas are about the components of the defined run, not about arbitrary sets with a few properties.

Out of scope: the running time $O(n^2\log n)$ (Lemma 12; there is no cost model), and the incentive properties, which clock auctions have by construction (every price update is a minimum with the previous price, and a bidder who rejects is removed). Useful infrastructure beyond this mission: the greedy-prefix telescoping of prices against marginal contributions, and the bound $v(S)\le v(\emptyset)+\sum_{i\in S} v(\{i\}\mid\emptyset)$ for submodular $v$. Contributions to any milestone are welcome.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010 (reference [30] of the paper).
• N. Chen, N. Gravin, P. Lu, On the Approximability of Budget Feasible Mechanisms, SODA 2011 (reference [10]).
• P. Jalaly, É. Tardos, Simple and Efficient Budget Feasible Mechanisms for Monotone Submodular Valuations, ACM Transactions on Economics and Computation 9(1), 2021 (reference [20]).
• G. Amanatidis, P. Kleer, G. Schäfer, Budget-Feasible Mechanism Design for Non-Monotone Submodular Objectives, EC 2019 (reference [1]).

Motivation

Tele-driving separates a ride-hailing driver from the vehicle: a remote driver operates a car over a wireless link, and on finishing a trip can immediately take control of another car anywhere in the service region. Several companies have run pilots of this model; Benjaafar, Wang and Yang cite Vay's car-sharing service operated by tele-drivers and Halo's remotely operated robo-taxi pilot with T-Mobile. A platform with remote drivers can therefore hold more vehicles than drivers. The practical question is how many drivers such a platform needs.

Benjaafar, Wang and Yang (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687) model the system as a loss system with a state-dependent service rate and compare a fleet with $n$ remote drivers to one with a driver in every vehicle ($n = m$). This mission formalizes their answer for large markets that have many vehicles relative to demand (the supply-rich regime): asymptotically, a fraction $1/\alpha$ of the fleet size suffices, where $\alpha > 2$ measures how much the fleet exceeds the offered load. All page numbers refer to the SSRN working paper, version of 1 June 2023, which is the source of this mission.

Setting

Customers arrive as a Poisson process of rate $\lambda > 0$. The platform has $m$ vehicles and $n \le m$ remote drivers. When $q$ customers are being served, trips are completed at total rate $q\,\mu(m,q)$, where the service rate $\mu(m,q)$ accounts for the pick-up time (which shrinks as more idle vehicles are available) and the trip time. A customer arriving while all $n$ drivers are busy is lost. With

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)} \qquad (1)$$

the number of customers in service is a birth–death process on $\{0, \dots, n\}$ with stationary distribution

$$\pi_{m,n}(0) = \Big[1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)\Big]^{-1}, \qquad \pi_{m,n}(q) = \pi_{m,n}(0)\prod_{k=1}^{q}\rho(k), \quad 1 \le q \le n. \qquad (2)\text{–}(3)$$

The service level, the long-run fraction of demand served, is $SL(m,n) = 1 - \pi_{m,n}(n)$.

For the asymptotic analysis the paper uses the service rate of Besbes et al.,

$$\mu(m,q) = \Big[\frac{s}{\sqrt{m-q+1}} + s\Big]^{-1}, \qquad (4)$$

where $s > 0$ is the mean trip time and $s/\sqrt{m-q+1}$ the mean pick-up time with $m - q$ idle vehicles. The fleet grows with demand as $m_\lambda = \lfloor \alpha\lambda s\rfloor$ for a constant $\alpha > 0$; the offered load is $\lambda s$, so $\alpha$ is the ratio of fleet size to offered load. The supply-rich regime is $\alpha > 2$.

For the rate (4) and $m > 2\lambda s$, the equation $\rho(q) = 1$ has a unique root $q_3$ in $[\lambda s, m]$; to its left $\rho > 1$ (the chain drifts upward), to its right $\rho < 1$. For a tolerance $\epsilon > 0$ the paper defines

$$n^*_\lambda = \min\{\, n : SL(m_\lambda, m_\lambda) - SL(m_\lambda, n) < \epsilon \,\},$$

the smallest number of remote drivers whose service level is within $\epsilon$ of that of a fleet with one driver per vehicle.

Formalization targets

Goal: Theorem 2.C (p. 22)

For $\alpha > 2$ and every $\epsilon > 0$,

$$\limsup_{\lambda\to\infty} \frac{n^*_\lambda}{m_\lambda} \le \frac{1}{\alpha}.$$

The bound does not depend on $\epsilon$, and since $\alpha > 2$ it says that a large supply-rich system can be run with at most about half as many drivers as vehicles.

Milestones

1. App. D, case (iii) (p. 42): for the rate (4) and $m > 2\lambda s$, $\rho(q) = 1$ has a unique root $q^* \in [\lambda s, m]$, and on $(0, m]$, $\rho(q) < 1$ exactly when $q > q^*$.
2. App. D.3 (p. 48): $\lim_{\lambda\to\infty} \lambda s / q_3 = 1$.
3. Lemma 5 (pp. 47–48): with $n_\epsilon = \lfloor (1+\epsilon) q_3\rfloor$ drivers,

$$\lim_{\lambda\to\infty}\Big[\sum_{i=\lfloor (1+\epsilon/2)q_3\rfloor}^{n_\epsilon}\pi_{m_\lambda,n_\epsilon}(i) + \sum_{i=0}^{\lfloor(1-\epsilon/2)q_3\rfloor}\pi_{m_\lambda,n_\epsilon}(i)\Big] = 0.$$

4. Footnote 14 (pp. 22–23): $\lim_{\lambda\to\infty}\big[SL(m_\lambda,m_\lambda) - SL(m_\lambda, \lfloor(1+\delta)q_3\rfloor)\big] = 0$.

Significance

The result. Theorem 2.C quantifies the labour saving of tele-driving in markets where vehicles are plentiful. A conventional platform needs one driver per vehicle; a remote-driver platform with $m_\lambda \approx \alpha\lambda s$ vehicles needs only about $\lambda s$ drivers, essentially the offered load, while losing at most $\epsilon$ of service level. Together with Theorems 2.A and 2.B of the same paper (the supply-limited and intermediate regimes), it gives a complete asymptotic picture of when pooling drivers across vehicles pays off: in the supply-rich regime, the gain appears as fewer drivers rather than as a higher service level. Footnote 14 strengthens this: the service level with $(1+\delta)q_3$ drivers matches the full-staffing service level in the limit.

Formalizing it. The result is proved on paper in Appendix D.3; it has no machine-checked proof. The formalization adds a precise reading of the limit statements (the range of the minimum defining $n^*_\lambda$, the meaning of "small $\epsilon$") and a verified account of the concentration of a birth–death distribution with a state-dependent rate, in the form of Lemma 5. The same model underlies four sibling missions on this paper.

Difficulty

The obvious first idea, comparing $SL(m,n)$ with the Erlang loss formula for a constant service rate, does not apply: under (4) the service rate depends on the state through the pick-up time, so the stationary weights $\prod_{k\le q}\rho(k)$ are not Poisson probabilities and their tails have no closed form. The quantities that govern the answer are defined only implicitly: the critical point $q_3$ solves $\rho(q) = 1$, and its explicit expression (17) involves the arccosine of a cubic's coefficients, which is unusable for estimates. The statements also take a limit $\lambda\to\infty$ in which the number of states, the root $q_3$ and the floors $\lfloor(1\pm\epsilon/2)q_3\rfloor$ all move together, so any bound on the stationary distribution must hold uniformly along this family rather than for a fixed chain. Finally, $n^*_\lambda$ is a minimum over integers of a difference of service levels, and the goal concerns its growth rate relative to $m_\lambda$, not a single system.

Formalization scope

The Lean development lives in the namespace TeleDriving.AsymRich.

• Model. rho mu lam m q is (1) with $q$ real; piMN mu lam m n q and SL mu lam m n are (2)–(3) and the service level, with $q, n$ natural; muBesbes s is the rate (4); mLam alpha s lam is $\lfloor\alpha\lambda s\rfloor$ as a natural-number floor. The shared Model file also contains the paper's Assumptions 1–2, its size restriction, the regime predicates and the maximal service-level ratio, which this mission does not use.
• Domains. $\pi_{m,n}(q)$ is the paper's only for $q \le n$, $SL(m,n)$ only for $1 \le n \le m$, the rate (4) only for $q \le m+1$; Lean's junk values outside these ranges are never invoked by the statements.
• $n^*_\lambda$ (nStar) is the minimum over $n \in \{1,\dots,m_\lambda\}$, a set that contains $n = m_\lambda$ when $m_\lambda \ge 1$ and $\epsilon > 0$; the paper leaves this range implicit.
• Limits are written in $\varepsilon$-form: $\limsup f \le c$ as "for every $\delta > 0$, eventually $f(\lambda) \le c + \delta$"; plain limits use Filter.Tendsto along atTop on $\mathbb R$.
• The root $q_3$ is a function of $\lambda$ with the hypothesis that, for all sufficiently large $\lambda$, $\lambda s \le q_3(\lambda) \le m_\lambda$ and $\rho(q_3(\lambda)) = 1$. By milestone 1 this determines $q_3(\lambda)$ uniquely once $m_\lambda > 2\lambda s$, which holds eventually for $\alpha > 2$. The closed form (17) is not used.
• "Small $\epsilon$" and "any $\delta > 0$" in Lemma 5 and footnote 14 are read as $0 < \epsilon, \delta < \alpha - 1$: exactly in this range $\lfloor(1+\epsilon)q_3\rfloor \le m_\lambda$ for large $\lambda$, so the number of drivers does not exceed the number of vehicles. The goal's tolerance $\epsilon > 0$ is unrestricted, as printed.
• The paper uses $\epsilon$ for both the service-level tolerance of Theorem 2.C and the window of Lemma 5; the Lean statements use distinct names.

The goal carries no hypothesis on $\pi$, $SL$, $n^*_\lambda$ or $q_3$: its only assumptions are $s > 0$, $\alpha > 2$ and $\epsilon > 0$, so it cannot be discharged by an assumption that makes the minimum small by fiat. A complete development needs elementary real analysis of the rate (4) (concavity of $q/(\lambda s) - 1/\sqrt{m-q+1}$), estimates for products of $\rho$ along integer ranges, and asymptotics with floors; the concentration estimate for birth–death chains with state-dependent rates is reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 ; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112

Motivation

Autonomous vehicles that cannot yet drive every trip on their own can be supervised or driven by remote (tele-)drivers who sit in a control center and take over a vehicle only while it serves a customer. Because a remote driver is not tied to one vehicle, a platform may operate more vehicles than drivers. Benjaafar, Wang and Yang ask when this decoupling pays off: given a fleet of $m$ vehicles, how many remote drivers $n \le m$ should a ride-hailing operator staff, and how much better is the best choice than the conventional one driver per vehicle ($n = m$)?

The question is sharpened by a feature of ride-hailing that classical loss systems lack. A trip consists of a pick-up leg and a delivery leg, and the pick-up leg is long when few vehicles are idle. Following Besbes, Castro and Lobel (2022), the paper models this through a state-dependent service rate: with $q$ customers in service, each trip ends at rate $\mu(m,q)$, which falls as $q$ approaches $m$. Withholding drivers keeps idle vehicles available, shortens pick-ups and can raise throughput. This mission formalizes the asymptotic size of that gain in the supply-limited regime, where vehicles are scarce relative to demand.

The source is the authors' SSRN working paper (abstract 4130757, version of 1 June 2023); all numbering in this mission is that version's. The paper was published in Management Science in 2024.

Setting

Customers arrive as a Poisson process of rate $\lambda > 0$. A customer who arrives when all $n$ remote drivers are busy is lost. The number $q$ of customers in service is a birth–death process with birth rate $\lambda$ and death rate $q\,\mu(m,q)$. Its load is

$$\rho(q) = \frac{\lambda}{q\,\mu(m,q)} \qquad (1),$$

and its stationary distribution is

$$\pi_{m,n}(q) = \frac{\prod_{k=1}^{q}\rho(k)}{1 + \sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)}, \qquad 0 \le q \le n \qquad (2)\text{–}(3).$$

The service level is the long-run fraction of demand served, $SL(m,n) = 1 - \pi_{m,n}(n)$.

The mission uses the service rate

$$\mu(m,q) = \Big[\frac{s}{\sqrt{m-q+1}} + s\Big]^{-1} \qquad (4),$$

where $s > 0$ is the expected trip time and $s/\sqrt{m-q+1}$ is the expected pick-up time when $m - q$ vehicles are idle. Demand and fleet scale together: for a fixed $\alpha > 0$ the fleet has

$$m_\lambda = \lfloor \alpha\lambda s \rfloor$$

vehicles. The load at full occupancy is $\rho(m_\lambda) = 2\lambda s/m_\lambda \to 2/\alpha$. The case $\alpha \in (0,1)$ is the supply-limited regime: there $\rho(k) > 1/\alpha > 1$ at every occupancy $1 \le k \le m_\lambda$.

In Lean the namespace is TeleDriving.AsymLimited; the functions are rho, piMN, SL, muBesbes (the rate (4)), mLam ($m_\lambda$) and maxSLRatio (the maximum below).

Formalization targets

Goal: Theorem 2.A (p. 22)

For $\alpha \in (0,1)$,

$$\liminf_{\lambda\to\infty}\ \Big[\max_{n\in\{1,\dots,m_\lambda\}}\frac{SL(m_\lambda,n)}{SL(m_\lambda,m_\lambda)}\Big] \ \ge\ 2-\alpha.$$

The theorem asserts a lower bound on the limiting gain only; it does not assert that $2-\alpha$ is attained or that the limit exists.

Milestones (Appendix D.1, pp. 44–46)

With $a = 1/\alpha$:

1. $\rho(k) > 1/\alpha$ for $1 \le k \le m_\lambda$ (p. 44).
2. The comparison probability $\tilde\pi = 1/\big[1+\sum_{i=0}^{m_\lambda-1} 1/(\rho(m_\lambda)a^i)\big]$ of (19) satisfies $\tilde\pi < \pi_{m_\lambda,m_\lambda}(m_\lambda)$ and $\tilde\pi \to (2a-2)/(2a-1)$ (p. 44).
3. For $m > 4$, $H(n) = 1/\rho(n)$ strictly increases and then strictly decreases on $[0,m]$, so it has a unique maximizer $n^*$ (p. 45).
4. For $0 < \epsilon < 1$, $\sum_{i=0}^{\lfloor(1-\epsilon)n^*\rfloor}\pi_{m_\lambda,\lfloor n^*\rfloor}(i) \to 0$ (display (21), pp. 45–46).
5. The comparison probability $\hat\pi$ of (22) satisfies $\hat\pi \to 1-(1-\epsilon)/a$ and $\hat\pi > \pi_{m_\lambda,\lfloor n^*\rfloor}(\lfloor n^*\rfloor)$ (p. 46).

Significance

Theorem 2.A quantifies the value of decoupling drivers from vehicles when vehicles are scarce. A platform that staffs only enough remote drivers to keep some vehicles idle serves, asymptotically, at least $2-\alpha$ times the fraction of demand it would serve with one driver per vehicle. The bound decreases in $\alpha$ and reaches $1$ at $\alpha = 1$, where the companion Theorem 2.B (intermediate regime, $\alpha \in (1,2)$) shows the gain vanishes. Theorems 2.A–2.C together describe how the benefit of remote driving changes from supply-limited to supply-rich markets.

The result is proved in the paper, by explicit comparison distributions. As far as is known it has not been machine-checked; no ride-hailing or state-dependent loss-system result of this kind is formalized in Mathlib or on the platform. A formal proof would establish the asymptotics of a birth–death loss system whose rates depend on the system size in a non-classical way, using only elementary real analysis: geometric series, floors and limits of explicit expressions. The intermediate statements, such as the vanishing of the low-occupancy mass, are reusable for the sibling missions on Theorems 2.B and 2.C.

Difficulty

The obvious argument compares the two blocking probabilities with an Erlang loss system, but the load $\rho(q)$ is not constant: it depends on $q$, on $m_\lambda$ and on $\lambda$ simultaneously, and all three grow together. Neither the stationary distribution with $m_\lambda$ drivers nor the one with the optimal number of drivers converges to a fixed geometric law. The goal concerns a ratio of two quantities that both tend to explicit nonzero limits only after the distribution has been localized near a moving maximizer $n^*$ of $1/\rho$. That maximizer has a closed form only through cube roots, and the localization has to hold uniformly as $\lambda \to \infty$. The two bounds also use different comparison distributions, and the floors $\lfloor n^*\rfloor$, $\lfloor(1-\epsilon)n^*\rfloor$ and $\lfloor\alpha\lambda s\rfloor$ must be controlled at the same time.

Formalization scope

• Model. $\mu$ is a function ℕ → ℝ → ℝ; the rate (4) is muBesbes s. $\rho$ takes a real occupancy, while $\pi_{m,n}(q)$ and $SL(m,n)$ take natural arguments. $\pi_{m,n}$ is written as one quotient of products; it equals (2)–(3). The objects carry the page's meaning only on the page's domains ($1 \le q \le m$ for $\rho$, $0 \le q \le n \le m$ for $\pi$), because Lean's division by $0$ returns $0$ and Real.sqrt of a negative number returns $0$. Every statement stays inside these domains.
• Standing hypotheses. $s > 0$ and $\alpha \in (0,1)$. Assumptions 1–2 and the size restriction of p. 13 are part of the shared model file but are not hypotheses here: the rate (4) satisfies them, and the size restriction holds for all large $\lambda$.
• Maximum. $\max_{n\in\{1,\dots,m\}}$ is a supremum over Fin m with index $n \mapsto n+1$. It ranges over $n \in \{1,\dots,m_\lambda\}$ only, and $m_\lambda \ge 1$ for large $\lambda$.
• Limits. $\liminf \ge c$ is stated in $\varepsilon$-form (for every $\varepsilon > 0$, eventually $\ge c-\varepsilon$), and $\lim$ as Filter.Tendsto along atTop on $\mathbb R$. The $\varepsilon$ of the liminf is not the $\epsilon$ of D.1's cut-off $(1-\epsilon)n^*$, which is named eps.
• The maximizer $n^*$. It is a function of $\lambda$, characterized by a hypothesis that holds for all large $\lambda$: $n^*(\lambda) \in [0,m_\lambda]$ maximizes $H$ there. It is not computed from the closed form (20), whose cube roots of negative numbers Lean's Real.rpow does not represent. The unimodality milestone is stated for every $m > 4$ and $\lambda > 0$; the page states it for $m = m_\lambda$.
• Eventual inequalities. The strict inequalities $\tilde\pi < \pi$ and $\hat\pi > \pi$ are stated for large $\lambda$, because they fail in degenerate small cases ($m_\lambda = 1$; $\lfloor n^*\rfloor = \lfloor(1-\epsilon)n^*\rfloor$).
• Ruled out. No hypothesis states a limit of $\pi_{m_\lambda,m_\lambda}(m_\lambda)$ or of any ratio, so the goal cannot be trivialized. The maximum is not taken over all $n$, so values of $\pi_{m,n}$ outside the page's domain cannot enter.

No external library is needed beyond Mathlib. Proofs of any milestone are welcome, and so are alternative proofs of the goal that bypass them.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 ; published in Management Science, 2024, https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2), 2022. https://doi.org/10.1287/opre.2021.2112

Why remote drivers in ride-hailing

In a conventional ride-hailing system every vehicle needs its own driver. Tele-driving, in which a vehicle is driven by a remote operator over a network, separates the two: a pool of $n$ remote drivers can serve a fleet of $m \ge n$ vehicles, each driver taking control of an idle vehicle near the next customer. Fewer drivers mean lower labor cost, but also fewer simultaneous trips; more vehicles mean shorter pick-up legs. Benjaafar, Wang and Yang (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687) model this trade-off as a loss system with a state-dependent service rate and ask when it pays to have fewer drivers than vehicles. This mission takes its asymptotic answer for markets that are neither short of vehicles nor flush with them.

The model

Customers arrive as a Poisson process of rate $\lambda > 0$. With $m$ vehicles and $q$ customers in service, each customer is served at rate $\mu(m,q)$: the more vehicles are busy, the farther the nearest idle vehicle, and the slower a trip completes. A customer who finds all $n$ drivers busy is lost. The number of customers in service is then a birth–death process on $\{0,\dots,n\}$ with birth rate $\lambda$ and death rate $q\mu(m,q)$. With the load $\rho(q) = \lambda/(q\mu(m,q))$ (equation (1) of the paper), its stationary distribution is

$$\pi_{m,n}(q) = \frac{\prod_{k=1}^{q}\rho(k)}{1+\sum_{i=1}^{n}\prod_{k=1}^{i}\rho(k)}, \qquad 0 \le q \le n,$$

(equations (2)–(3)), and the service level, the long-run fraction of demand served, is $SL(m,n) = 1 - \pi_{m,n}(n)$.

The asymptotic results use the service rate of Besbes, Castro and Lobel, equation (4):

$$\mu(m,q) = \left[\frac{s}{\sqrt{m-q+1}} + s\right]^{-1},$$

where $s > 0$ is the expected trip time between two uniformly drawn points of the service region and $s/\sqrt{m-q+1}$ the pick-up time with $m-q$ idle vehicles. The fleet grows in proportion to demand, $m_\lambda = \lfloor \alpha\lambda s\rfloor$ for a fixed $\alpha > 0$. For this rate the equation $\rho(q) = 1$ has, in the intermediate regime $\lambda s + 3(\lambda s/2)^{2/3} - 1 < m < 2\lambda s$ (equation (14)), exactly two roots $q_1 < q_2$ in $[\lambda s, m]$, and $\rho < 1$ strictly between them. For $m_\lambda = \lfloor\alpha\lambda s\rfloor$ this regime is $\alpha \in (1,2)$ for large $\lambda$.

Formalization targets

Goal: Theorem 2.B (p. 22)

For $\alpha \in (1,2)$,

$$\lim_{\lambda\to\infty}\left[\max_{n\in\{1,\dots,m_\lambda\}} \frac{SL(m_\lambda,n)}{SL(m_\lambda,m_\lambda)}\right] = 1 .$$

Milestones (App. D and D.2, pp. 42, 46–47)

1. App. D, case (ii). For the rate (4) and $\lambda s + 3(\lambda s/2)^{2/3} - 1 < m < 2\lambda s$ (with $\lambda s \ge 2$), $\rho = 1$ has two roots $q_1 < q_2$ in $[\lambda s, m]$, and on $(0,m]$, $\rho(q) < 1$ exactly for $q_1 < q < q_2$.
2. Step (i). $\limsup_\lambda [m_\lambda - \lfloor q_2\rfloor] < \infty$ and $\limsup_\lambda \prod_{k=\lfloor q_2\rfloor+1}^{m_\lambda}\rho(k) < \infty$.
3. Step (ii). $\lim_\lambda \prod_{k=\lfloor q_1\rfloor+1}^{\lfloor q_2\rfloor}\rho(k) = 0$.
4. The reduction. $\pi_{m_\lambda,m_\lambda}(\lfloor q_1\rfloor)/\pi_{m_\lambda,m_\lambda}(m_\lambda) \to \infty$, with the paper's product identity for this ratio.

Significance

Theorem 2.B is the middle of the paper's three asymptotic results. In the supply-limited regime $\alpha \in (0,1)$, Theorem 2.A says that choosing the number of drivers optimally improves the service level by a factor of at least $2-\alpha$; in the supply-rich regime $\alpha > 2$, Theorem 2.C bounds the fraction of drivers needed to keep the full service level. Theorem 2.B closes the gap: in a large intermediate market the system with one driver per vehicle is already asymptotically as good as the best system with fewer drivers, so the benefit of tele-driving there is cost, not service. The mechanism is that the stationary distribution with $n = m$ is bimodal, and the mass of the congested mode at $m$ becomes negligible compared with the mode at $\lfloor q_1\rfloor$.

The result is proved in the paper (App. D.2). It has no machine-checked proof; this mission formalizes the statement and the steps of the published proof, with the root characterization of App. D made explicit.

Difficulty

The ratio of service levels is at least one (take $n = m_\lambda$) and at most $1/SL(m_\lambda, m_\lambda)$, so everything rests on showing that the loss probability $\pi_{m_\lambda,m_\lambda}(m_\lambda)$ of the full system vanishes. The obvious bound fails: the loads $\rho(k)$ exceed one both below $q_1$ and above $q_2$, so the stationary distribution is not monotone, and the product of loads from the lower mode to $m_\lambda$ mixes factors above and below one. What is needed is quantitative control of both roots as $\lambda \to \infty$: $q_2$ stays within a bounded distance of $m_\lambda$, while $q_2 - q_1$ grows linearly in $m_\lambda$ with loads bounded away from one in between. The roots have no simple closed form; the paper's expressions (17)–(18) involve a cubic and an arccosine.

Formalization scope

All objects are defined in one definitions module, TeleDriving.AsymIntermediate.Model, shared verbatim (up to the namespace) with the other four missions of the series. The service rate is a function $\mu : \mathbb N \times \mathbb R \to \mathbb R$; $\rho$ is evaluated at real $q$; $\pi_{m,n}$ and $SL$ are the closed forms (2)–(3) rather than a stationary-distribution predicate. $m_\lambda$ is the natural-number floor $\lfloor \alpha\lambda s\rfloor$, and $\lambda \to \infty$ along the reals. The maximum over $n \in \{1,\dots,m\}$ is a supremum over a finite index set; its value at $m = 0$ is $0$ and irrelevant because $m_\lambda \to \infty$. Limits superior below infinity are stated as "bounded for all large $\lambda$"; divergence to infinity as Tendsto … atTop atTop.

Standing hypotheses: $s > 0$ and $1 < \alpha < 2$. The roots $q_1(\lambda) < q_2(\lambda)$ in Steps (i)–(ii) and the reduction are functions of $\lambda$ characterized only for all sufficiently large $\lambda$ by $\lambda s \le q_1 < q_2 \le m_\lambda$ and $\rho(q_1) = \rho(q_2) = 1$; by milestone 1 they then coincide with the paper's $q_1, q_2$. A characterization required for every $\lambda$ would be unsatisfiable for small $\lambda$ and make those items vacuous; it is ruled out. The goal theorem does not mention the roots and assumes nothing about $\pi$ or $SL$. Milestone 1 adds the hypothesis $\lambda s \ge 2$, which the paper's derivation uses tacitly (it places the maximizer of its auxiliary function inside $[\lambda s, m]$) and without which the claim fails for small $\lambda s$.

The development needs elementary real analysis: concavity of $q/(\lambda s) - (m-q+1)^{-1/2}$, asymptotics of $\lfloor\alpha\lambda s\rfloor$, and estimates on finite products. No probability theory beyond the closed forms is required. The root analysis of milestone 1 is reusable for the supply-limited and supply-rich missions of the series. Proofs of the milestones, alternative arguments for the goal, and a formal treatment of the closed forms (17)–(18) are welcome. The source is the 2023 SSRN working paper; theorem numbers are those of that version.

Selected references

• S. Benjaafar, Z. Wang, X. Yang, Human in the Loop Automation: Ride-Hailing with Remote (Tele-)Drivers, SSRN working paper 4130757, version of 1 June 2023. https://ssrn.com/abstract=4130757 ; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01687
• O. Besbes, F. Castro, I. Lobel, Spatial Capacity Planning, Operations Research 70(2):1271–1291, 2022.

Motivation

A seller with one item faces $n$ buyers whose valuations she does not know, not even in distribution. Prior-independent mechanism design asks which selling mechanism performs well against every distribution in a given class, rather than against one known prior. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) measure performance by regret: the expected gap between the highest valuation, which a seller who knew the valuations could extract, and the revenue actually collected. They solve the resulting minimax problem for several classes of joint distributions: i.i.d., exchangeable and affiliated, mixtures of i.i.d., exchangeable, and arbitrary.

This mission formalizes the last two cases. The answer is that the minimax regret against exchangeable or arbitrary joint valuations is $1/e$ for every number of buyers $n$, so competition among buyers does not help the seller unless Nature's power is restricted.

Timeline. Bergemann and Schlag (2008) solved the one-buyer regret problem: the optimal mechanism is a randomized posted price and the minimax regret is $1/e$. Koçyiğit, Kuhn and Rujeerapaiboon (2020; doi:10.1287/ijoc.2022.0275) showed, for several bidders and several items, that with arbitrary joint distributions the minimax regret problem reduces to the one-bidder case, so the value does not improve with $n$. Anunrojwong, Balseiro and Besbes (2022–2024, Proposition 4) recover this within their framework, show that the worst case can be taken exchangeable, and identify the optimal mechanism as a second-price auction with a random reserve.

Setting

There are $n \ge 1$ buyers with valuations $v = (v_1,\dots,v_n)$ in the type cube $[0,1]^n$. A mechanism $m = (x,p)$ maps reported valuations to allocation probabilities $x_i(v)$ and payments $p_i(v)$. The class $\mathcal M$ of DSIC mechanisms consists of those satisfying, on $[0,1]^n$: individual rationality (IR) $v_i x_i(v) - p_i(v) \ge 0$; dominant-strategy incentive compatibility (IC), truthful reporting is optimal for each buyer whatever the others report; and the allocation constraint (AC) $\sum_i x_i(v) \le 1$.

Write $v^{(1)}$ and $v^{(2)}$ for the highest and second-highest valuation. The regret of $m$ against a joint law $\mathbf F$ on $[0,1]^n$ is

$$R_n(m,\mathbf F) = \mathbb E_{v\sim\mathbf F}\Big[v^{(1)} - \sum_{i=1}^n p_i(v)\Big],$$

and the minimax regret over a class $\mathcal F$ is $\mathcal R^*_n(\mathcal F) = \inf_{m\in\mathcal M}\sup_{\mathbf F\in\mathcal F} R_n(m,\mathbf F)$. Here $\mathcal F_{\mathrm{all}}$ is the class of all distributions on $[0,1]^n$, and $\mathcal F_{\mathrm{exc}}$ the exchangeable ones, invariant under every permutation of the buyers.

A second-price auction with random reserve $\mathrm{SPA}(\Phi)$ draws a reserve $p\sim\Phi$, gives the item to a highest bidder if her bid is at least $p$, and charges her $\max(v^{(2)},p)$. Proposition 4 uses the reserve CDF $\Phi^*(p) = \log p + 1$ on $[1/e,1]$ ($0$ below $1/e$), and the isorevenue law on $[1/e,1]$, with CDF $1 - 1/(e t)$ on $[1/e,1)$ and an atom of mass $1/e$ at $1$. Nature's candidate $\mathbf F^*$ picks a buyer $k$ uniformly at random, gives her an isorevenue value and gives everyone else value $0$.

Formalization targets

Goal: Proposition 4

With $m^* = \mathrm{SPA}(\Phi^*)$ and $\mathbf F^* = \frac1n\sum_k \mathbf F^{*,k}$, for every $m\in\mathcal M$ and $\mathbf F\in\mathcal F_{\mathrm{all}}$,

$$R_n(m^*,\mathbf F) \le R_n(m^*,\mathbf F^*) \le R_n(m,\mathbf F^*),$$

$\mathbf F^*$ is exchangeable, and

$$\mathcal R^*_n(\mathcal F_{\mathrm{exc}}) = \mathcal R^*_n(\mathcal F_{\mathrm{all}}) = R_n(m^*,\mathbf F^*) = \frac1e .$$

Milestones

1. $\mathrm{SPA}(\Phi)\in\mathcal M$ for every reserve distribution $\Phi$ (p. 16).
2. The pointwise regret of $\mathrm{SPA}(\Phi)$ for $\Phi$ with a density: $v^{(1)} - v^{(1)}\Phi(v^{(1)}) + \int_{v^{(2)}}^{v^{(1)}}\Phi(p)\,dp$ (proof of Proposition 1, App-4).
3. The pointwise regret of $\mathrm{SPA}(\Phi^*)$ is at most $1/e$, with equality when $v^{(1)}\ge 1/e\ge v^{(2)}$ (Cases 1–3, App-8).
4. The expected revenue of any $m\in\mathcal M$ under $\mathbf F^*$ is at most $\frac1n\sum_k\big(r^*x_k(e_k) - \int_0^{r^*}x_k(t e_k)\,dt\big)$ with $r^* = 1/e$, with equality under the normalization $p_i = 0$ when $v_i = 0$ (App-8).
5. $\mathbf F^*$ is exchangeable (p. 22).

Significance

The result. Proposition 4 gives the exact minimax regret and an explicit saddle point for the two largest distribution classes of the paper. The value $1/e$ is independent of $n$, in contrast with the i.i.d. class, where the minimax regret decreases in $n$ (Theorem 1 of the same paper). Together with the other propositions it shows precisely how much structure Nature must be denied before additional buyers reduce the seller's regret. The worst case being exchangeable shows that symmetry alone does not help.

Formalizing it. The result is proved on paper; it is not formalized anywhere to our knowledge. A formalization produces machine-checked versions of: dominant-strategy incentive compatibility of the second-price auction with random reserve; the pointwise regret identity for that auction; a revenue identity for arbitrary DSIC mechanisms under a mixture of one-buyer laws, which rests on Myerson's payment characterization; and a minimax value computed over all DSIC mechanisms and all distributions. Each of these is reusable by the sister missions on i.i.d., affiliated and fixed-reserve settings.

Difficulty

The minimax problem ranges over all DSIC mechanisms, an infinite-dimensional and unstructured class, and over all joint distributions. The upper bound needs only one mechanism, but the lower bound must hold against every DSIC mechanism, including randomized ones whose allocation is not of auction form; the step from incentive compatibility to an explicit revenue formula along the line $\{t e_k\}$ is where the work lies. Myerson's payment characterization is quoted by the paper without proof and must be established here for mechanisms that are incentive compatible only on $[0,1]$. A second obstacle is measure-theoretic: the regret is an integral of an arbitrary mechanism's payments against an arbitrary law, so its finiteness and the interchange of expectation with the reserve randomization must be justified. The tempting shortcut of restricting Nature to i.i.d. laws gives a different, smaller value.

Formalization scope

Lean represents valuations as Fin n → ℝ and laws as measures on that space; $\mathcal F_{\mathrm{all}}$ is the set of probability measures giving the complement of $[0,1]^n$ measure zero, and $\mathcal F_{\mathrm{exc}}$ those also invariant under $v\mapsto v\circ\sigma$ for every permutation $\sigma$. (IR), (IC), (AC) are imposed on $[0,1]^n$, with misreports in $[0,1]$. Two hypotheses are added to the class $\mathcal M$ and disclosed in every statement: allocation and payment functions are measurable, and payments are bounded on $[0,1]^n$, so that the regret is a genuine expectation. Ties for the highest bid are broken towards the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule). $v^{(2)}$ is $0$ when $n = 1$. The minimax regret is a real infimum of real suprema; for DSIC mechanisms the regrets lie in a bounded interval and both index sets are nonempty, so these are not junk values. The reserve law $\Phi^*$ and the isorevenue law are given through their CDFs, and $\mathbf F^{*,k}$ as the push-forward of the isorevenue law under $t\mapsto t\,e_k$; $\mathbf F^*$ is not a product measure. The page prints $\Phi^*(p) = \log(v)+1$; the formalization uses $\log p + 1$.

Trivializing formalizations are ruled out: $\mathcal F_{\mathrm{all}}$ carries the support condition (without it the regret is unbounded), the regret at $\mathbf F^*$ is that of the stated reserve law $\Phi^*$, and both classes are nonempty.

A complete development needs: Lebesgue–Stieltjes integration by parts for CDFs, Myerson's envelope characterization of DSIC payments, push-forwards and mixtures of measures on $\mathbb R^n$, and conditionally complete lattice reasoning for the minimax value. The DSIC property of $\mathrm{SPA}(\Phi)$ and the payment characterization are reusable throughout auction theory. Proofs of any milestone, and lemmas towards Myerson's characterization, are welcome.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• Ç. Koçyiğit, D. Kuhn, N. Rujeerapaiboon, Regret Minimization and Separation in Multi-Bidder Multi-Item Auctions, technical report, 2020 (cited as Koçyiğit et al. [2020] in arXiv:2204.10478v5, p. 6); published in INFORMS Journal on Computing 36(6):1543–1561, 2024. https://doi.org/10.1287/ijoc.2022.0275
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58