All missions

Motivation

In contextual inverse optimization a decision-maker repeatedly faces linear problems $\min_{x\in\mathcal X_t} f_t(x)'c^\star$ whose cost vector $c^\star\in S^d$ is unknown. After each period it observes an action that an expert who knows $c^\star$ would have taken. Every observation is a set of linear inequalities on $c^\star$, so the costs consistent with the data form a cone, the knowledge set. Besbes, Fonseca and Lobel (arXiv:2106.14015, published in Operations Research, 2025) measure the residual ignorance of such a set by its uncertainty angle, the half-aperture of the narrowest revolution cone containing it, and show that offline regret is governed exactly by this angle.

Online, their algorithms are efficient only when the knowledge set is pointed, i.e. has uncertainty angle below $\pi/2$. When it is not, the general algorithm of §5 (ProjectedCones) works inside a growing subspace $\Delta_t$ spanned by the observations that were sufficiently new. Each time the subspace grows, the algorithm replaces the knowledge set by a polyhedral cone $K_t$ and needs a bound on the uncertainty angle of $K_t$ that depends only on the separation parameter $\eta$ and the dimension. Lemma 10 of the paper provides that bound. This mission formalizes it, together with the chain of lemmas in Appendix B on which its proof rests.

Setting

Let $\mathbb R^d$ carry the Euclidean inner product $c'x$ and norm $\|\cdot\|$, and let $S^d$ be its unit sphere. The angle between $c$ and $\hat c$ is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, with $\theta=0$ when either vector is $0$. The uncertainty angle of a set $C\subseteq\mathbb R^d$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\theta(c,\hat c),$$

and a minimizer $\hat c$ is a circumcenter of $C$. The circumradius of a cone is $\mu(K)=\sin\alpha(K)$.

For vectors $g_1,\dots,g_p$, write $\Pi_{g_1,\dots,g_{i-1}}$ for the orthogonal projection onto their span and $g_{-i}=\{g_j:j\ne i\}$. The vector $g_i-\Pi_S(g_i)$ is the residual of regressing $g_i$ on $S$.

The algorithm's effective differences are unit vectors $\delta_1,\delta_2,\dots\in\mathbb R^d$. A difference triggers a subspace update when its residual against the current subspace exceeds $\eta$. The differences $\delta_1,\dots,\delta_p$ that triggered updates, in order of arrival, therefore satisfy

$$\|\delta_i-\Pi_{\delta_1,\dots,\delta_{i-1}}(\delta_i)\|\ \ge\ \eta,\qquad i=2,\dots,p .$$

They span the subspace $\Delta=\{\sum_i\gamma_i\delta_i:\gamma_i\in\mathbb R\}$, and the polyhedral cone of (14) is

$$K=\{c\in\Delta:\ c'\delta_i\ge0,\ i=1,\dots,p\}.$$

Two further cone quantities appear. The simplicial cone of linearly independent $g_1,\dots,g_p\in\mathbb R^p$ is $\operatorname{cone}(g)=\{\sum_i\alpha_ig_i:\alpha_i\ge0\}$. The inradius of a cone $K\subseteq\mathbb R^p$ is $\rho(K)=\max_{x\in S^p\cap K}\min_{y\in\partial K}\|x-y\|$, and the dual cone is $K^\star=\{c:c'x\ge0\ \forall x\in K\}$. With $G$ the matrix of columns $g_i$, $\lambda_{\min}(G'G)$ and $\lambda_{\max}(G'G)$ are the extreme eigenvalues of the Gram matrix.

Formalization targets

Goal: Lemma 10, angle bound (p. 25)

For $0<\eta\le1$, $d\ge2$ and unit vectors $\delta_1,\dots,\delta_p\in\mathbb R^d$ obeying the separation rule,

$$\alpha(K)\ \le\ \arccos\!\Big(\frac{\eta^{d-1}}{d^{3/2}}\Big).$$

The bound depends on $\eta$ and $d$ only, not on the number $p\le d$ of vectors or their configuration.

Milestones (Appendix B)

1. Lemma B-4 (App-28). Backward separation implies two-sided separation:

$$\|g_i-\Pi_{g_{-i}}(g_i)\|^2\ \ge\ \eta^{2(p-i)}(\eta^2)^{\mathbf 1\{i>1\}},\qquad i=1,\dots,p.$$

2. Lemma B-3 (App-27). With $\varphi=\min_i\|g_i-\Pi_{g_{-i}}(g_i)\|$,

$$\frac{\lambda_{\max}(G'G)}{\lambda_{\min}(G'G)}\le\Big(\frac p\varphi\Big)^2 .$$

3. Lemma B-2 (App-25). $\displaystyle\rho(\operatorname{cone}(g))\ \ge\ \frac1{\sqrt p}\sqrt{\frac{\lambda_{\min}(G'G)}{\lambda_{\max}(G'G)}}$.
4. (B-9) (App-20). $\mu^2(K)+\rho^2(K^\star)=1$, for every closed convex pointed cone $K\ne\{0\}$.
5. (B-8) (App-19). For $K=\{c\in\mathbb R^p:c'g_i\ge0\}$ with separated unit $g_i$,

$$\mu(K)\le\sqrt{1-\eta^{2(p-1)}/p^3}.$$

Significance

The bound is what makes the subspace stage of ProjectedCones restartable. After each update the algorithm discards its previous ellipsoidal cone and starts afresh from a revolution cone of aperture $\arccos(\eta^{d-1}/d^{3/2})$ around the circumcenter of $K_t$. Lemma 10 guarantees that this cone contains $K_t$, and with it the projected knowledge set, and that it is pointed. The number of later ellipsoid steps grows with the logarithm of the tangent of this aperture, so the shape of the bound enters the paper's regret analysis directly. The lemmas behind it are statements about general vector families: a residual inequality of Frisch–Waugh–Lovell type, a condition-number bound for correlation matrices, an inradius bound for simplicial cones, and the circumradius–inradius duality of Henrion and Seeger. Each is usable outside this paper.

The result is proved on paper; no part of it is formalized. The mission asks for machine-checked proofs of Lemma 10's angle bound and of the five appendix statements. Henrion–Seeger duality is cited, not proved, in the source. Its formalization would be new.

Difficulty

The separation rule controls each new vector only against the earlier ones. A bound on the cone's aperture needs control of each vector against all the others, and later vectors can lie close to the span of an earlier vector together with the remaining ones. The loss compounds, which is where the exponential factor $\eta^{d-1}$ comes from. A direct estimate of the circumcenter of $K$ is not available in closed form: the circumcenter is the solution of a quadratic program. The natural first attempt, bounding the angle between the circumcenter candidate $\sum_i\delta_i/\|\sum_i\delta_i\|$ and the extreme rays of $K$, requires the extreme rays of $K$, which are the columns of a dual basis whose norms are not controlled by the separation rule alone.

A second difficulty is dimensional. $K$ lives in the subspace $\Delta$, possibly of dimension $p<d$, while the uncertainty angle is measured on the sphere of $\mathbb R^d$. The appendix statements are posed in $\mathbb R^p$, in coordinates of $\Delta$. Transferring them requires an isometry onto $\Delta$ that preserves the cone, the angles and the projections.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d); families are indexed by Fin p, so all indices are 0-based and Lean's $i$ is the paper's $i+1$. Projections are Submodule.starProjection onto Submodule.span. The uncertainty angle is a real infimum of real suprema of angles in $[0,\pi]$. The angle at the zero vector is $0$, as in the paper, not Mathlib's $\pi/2$. The inradius is a real supremum of Metric.infDist to the frontier. It equals the paper's maximum on every cone of this mission. The dual cone is the platform's ConvexOptimization.dualCone. Eigenvalue ratios are stated without spectra: Lemma B-3 in the Rayleigh form $\|Gu\|^2\|v\|^2\le(p/\varphi)^2\|Gv\|^2\|u\|^2$, and Lemma B-2 with arbitrary bracket constants $\ell_{\min}\|u\|^2\le\|Gu\|^2\le\ell_{\max}\|u\|^2$. Both forms are equivalent to the printed ones.

Conventions and pins:

• The separation rule is "residual $\ge\eta$", the form of (B-14). The algorithm's strict "$>\eta$" is a special case, so the goal is stronger than the page needs. The first vector carries no condition.
• Lemma 10's inclusion $\Pi_{\Delta_t}(C(\mathcal I_t))\subseteq K_t$ is not posed: it concerns the algorithm's run. The polynomial-time computation of the circumcenter is not posed either: it is a complexity claim. "For every period $t$" becomes "for every family $\delta$ obeying the separation rule"; $p=0$ is the first period, with $K=\{0\}$.
• $d\ge2$ is the paper's standing assumption (§2), and $d^{3/2}$ is the real power.
• Lemma B-3 as printed takes $\varphi$ as the minimum over $i=2,\dots,p$ only. With that minimum the bound is false. The printed proof bounds every $i=1,\dots,p$, and the proof of Lemma 10 applies it so. The minimum over all $i$ is stated.
• (B-9) is stated on the page for every closed convex cone. It is posed for every closed convex pointed cone $K\ne\{0\}$ in $\mathbb R^p$: App-19 defines $\mu(K)=\sin\alpha(K)$ for pointed cones, and $K=\{0\}$ is excluded because its dual $\mathbb R^p$ has empty boundary.
• Lemmas B-3 and B-4 are posed in $\mathbb R^m$ for every $m$, which is equivalent to the page's $\mathbb R^p$. Lemma B-4 assumes no range for $\eta$, since only $\eta^2$ and even powers occur.

The cone in the goal is intersected with $\Delta$. A formalization of $K$ as $\{c\in\mathbb R^d:c'\delta_i\ge0\}$ would be false for $p<d$ (that set contains a line, so $\alpha\ge\pi/2$). A separation hypothesis that does not exclude nearly collinear vectors would make the bound unobtainable, and one that is never satisfiable would make it empty. The sanity check in the drafting workspace exhibits the hypotheses at $p=d=2$, $\eta=1$.

Contributions welcome: proofs of any milestone; the passage from $\mathbb R^p$ to the subspace $\Delta\subseteq\mathbb R^d$ (an isometry lemma for cones and angles); Gram-matrix facts (the inverse correlation matrix diagonal $a_{ii}=1/(1-R_i^2)$) as reusable lemmas.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023 (the version formalized; published in Operations Research, 2025). https://arxiv.org/abs/2106.14015
• R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18, 483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z
• M. C. Lovell, A simple proof of the FWL theorem, Journal of Economic Education 39(1), 88–91, 2008. https://doi.org/10.3200/JECE.39.1.88-91

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

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

Motivation

A seller offers one indivisible item to $n$ buyers but does not know the joint distribution of their valuations. The seller knows only that every valuation lies in $[0,1]$. Prior-independent mechanism design asks for a selling mechanism that performs well against every distribution in a class. One measure of performance is the regret: the expected gap between the full surplus $\max(v)$, which a seller who knew the valuations could extract, and the revenue actually collected. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478v5, Operations Research 2025) solve the minimax-regret problem over dominant-strategy incentive compatible (DSIC) mechanisms. For i.i.d. valuations the optimum is a second-price auction with a random reserve price (their Theorem 1).

I.i.d. valuations are a strong assumption in auction practice. In common-value and interdependent settings, bidders' values are positively dependent. The standard model of positive dependence in auction theory is affiliation, introduced by Milgrom and Weber (Econometrica 1982). §4.1 of the paper asks whether letting Nature choose an exchangeable affiliated distribution, rather than an i.i.d. one, changes the answer. It does not: the same auction and the same worst-case distribution form a saddle point, and the minimax regret is unchanged.

Setting

There are $n\ge1$ buyers with valuation profile $v=(v_1,\dots,v_n)\in[0,1]^n$. A mechanism $m=(x,p)$ assigns to each profile allocation probabilities $x_i(v)\in[0,1]$ and payments $p_i(v)$. It is DSIC, $m\in\mathcal M$, if it satisfies ex post individual rationality (IR), dominant-strategy incentive compatibility (IC), and the allocation constraint $\sum_i x_i(v)\le1$ (AC). The regret of $m$ against a joint law $F$ on $[0,1]^n$ is

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

and the minimax regret of a class $\mathcal F$ is $\mathcal R^*_n(\mathcal F)=\inf_{m\in\mathcal M}\sup_{F\in\mathcal F}R_n(m,F)$.

Two classes of laws on $[0,1]^n$ appear:

• $\mathcal F_{\mathrm{iid}}$: products $G^{\otimes n}$ of a law $G$ on $[0,1]$.
• $\mathcal F_{\mathrm{aff}}$: exchangeable and affiliated laws. Exchangeable means invariant under permutations of the coordinates. A set $A\subseteq\mathbb R^n$ is increasing if its indicator is nondecreasing. A set $S$ is a sublattice if it is closed under componentwise $\min$ ($\wedge$) and $\max$ ($\vee$). $F$ is affiliated if $\Pr_F(A\cap B\mid S)\ge\Pr_F(A\mid S)\Pr_F(B\mid S)$ for all increasing $A,B$ and every sublattice $S$.

The candidate saddle point comes from Theorem 1. Let $r^*_n\in(0,1/n)$ solve $(1-r)^{n-1}+\log r+\sum_{k=1}^{n-1}(1-r)^k/k=0$. The mechanism $m^*_n=\mathrm{SPA}(\Phi^*_n)$ draws a reserve $q$ from the CDF $\Phi^*_n$ of Theorem 1, sells to the highest bidder if the highest bid is at least $q$, and charges $\max(v^{(2)},q)$, where $v^{(2)}$ is the second-highest bid. The distribution $F^*_n$ makes the valuations i.i.d. with the isorevenue CDF: $F^*(t)=1-r^*_n/t$ on $[r^*_n,1)$, with an atom of mass $r^*_n$ at $1$. Order statistics enter through $F^{(1)}_k(p)=\Pr_F(\max(v_1,\dots,v_k)\le p)$ and $F^{(2)}_n(p)=\Pr_F(v^{(2)}\le p)$.

Formalization targets

Goal: Proposition 2 (p. 19)

For every $F\in\mathcal F_{\mathrm{aff}}$ and every $m\in\mathcal M$,

$$R_n(m^*_n,F)\ \le\ R_n(m^*_n,F^*_n)\ \le\ R_n(m,F^*_n),\qquad\text{hence}\qquad \mathcal R^*_n(\mathcal F_{\mathrm{aff}})=\mathcal R^*_n(\mathcal F_{\mathrm{iid}}).$$

The second inequality is Step 2 of Theorem 1 and is restated here. The first is new to §4.1.

Milestones (proof of Proposition 2)

1. Lemma 1 (p. 19): for exchangeable affiliated $F$ and $n\ge2$, $F^{(1)}_n(p)^{1/n}\ge F^{(1)}_{n-1}(p)^{1/(n-1)}$ for every $p$.
2. Order-statistic identity (p. 20, David–Nagaraja 5.3.2): for exchangeable $F$, $F^{(2)}_n=nF^{(1)}_{n-1}-(n-1)F^{(1)}_n$.
3. Nature's bound (p. 20):

$$R_n(\Phi^*_n,F)\le r^*_n+\int_{r^*_n}^1\Big(\tfrac{(n-1)r^*_n}{p-r^*_n}-1-\tfrac{(n-1)p}{p-r^*_n}F^{(1)}_n(p)+nF^{(1)}_{n-1}(p)\Big)\Phi^*_n(p)\,dp.$$

4. Pointwise maximization (p. 21): for $p\in(r^*_n,1)$, the function $z\mapsto\frac{(n-1)r^*_n}{p-r^*_n}-1-\frac{(n-1)p}{p-r^*_n}z+nz^{(n-1)/n}$ on $[0,1]$ is maximized at $z=F^*_n(p)^n$.

Significance

The result. Proposition 2 shows that positive dependence of the affiliated kind gives Nature no advantage against the optimal second-price auction. The minimax regret over $\mathcal F_{\mathrm{aff}}$ is the explicit i.i.d. value $(1-r^*_n)^{n-1}-\int_{r^*_n}^1(1-r^*_n/v)^{n-1}\,dv$, and the same randomized-reserve auction remains optimal. This contrasts with arbitrary or merely exchangeable dependence, where §4.3 of the paper shows the minimax regret jumps to $1/e$ for every $n$. Affiliation is therefore the dividing line between the dependence structures that the i.i.d. analysis covers and those it does not. Lemma 1, a comparison between the maximum of $n$ and of $n-1$ affiliated variables, is a self-contained inequality about order statistics under positive dependence.

Formalizing it. The result is proved in the paper. No machine-checked version of any part of it exists. The mission produces: a formal definition of affiliation in the measure-theoretic form of Milgrom and Weber's appendix; the order-statistic identity for exchangeable laws; Lemma 1; and the saddle-point statement. The proof of Lemma 1 quotes Milgrom–Weber Theorem 23 (monotone functions of affiliated variables are affiliated), and the identity is quoted from David and Nagaraja. Neither is proved in the paper, so formalizing them is part of the work.

Difficulty

The obvious route to the first inequality is to show that regret is monotone in dependence. That route fails, because the benchmark $\mathbb E[\max(v)]$ moves with dependence as well. With the marginals fixed, stronger positive dependence raises the auction's revenue, since $v^{(2)}$ moves toward $v^{(1)}$, but it also lowers $\mathbb E[\max(v)]$. Neither effect dominates uniformly, and the comparison must come out exactly at the isorevenue law. Nature's class is also not parametrized by marginals: an affiliated law need not have the marginals of $F^*_n$, so no coupling argument with a fixed i.i.d. law is available.

The second difficulty is in Lemma 1. It needs affiliation conditional on sublattices, not merely positive correlation of increasing events. The Harris-type inequality for $S=\mathbb R^n$ alone (association) is a strictly weaker property, and a formalization that keeps only it states a different class. Both the definition and the inequality must be handled for general laws without densities, since Definition 4 does not assume one.

Formalization scope

Valuation profiles are functions Fin n → ℝ, and laws are measures on that space giving full mass to $[0,1]^n$. (IR), (IC), (AC) and $x\in[0,1]^n$ are imposed on the cube. Mechanisms are additionally required to have measurable allocation and payment rules and bounded payments on the cube, so that (2) is a genuine expectation. $\mathcal R^*_n$ is an $\inf$ over DSIC mechanisms of a $\sup$ over the class; both are bounded, so the real-valued $\inf$/$\sup$ are not default values. Affiliation is stated for measurable $A$, $B$, $S$ in the cross-multiplied form $F(A\cap S)F(B\cap S)\le F(A\cap B\cap S)F(S)$. Ties in the auction go to the lowest index, which does not affect revenue. The reserve law and $F^*_n$ are given by CDF hypotheses ("CDF equals $\Phi^*_n$", "CDF equals the isorevenue CDF"), and $r^*_n$ by the hypothesis that it solves the $r^*$-equation in $(0,1/n)$. These restate Theorem 1, which belongs to mission I of this series.

Trivializing encodings are ruled out explicitly. Affiliation quantifies over every measurable sublattice $S$, not only $S=\mathbb R^n$. $\mathcal F_{\mathrm{aff}}$ requires exchangeability; without it Nature can set all but one valuation to zero and the statement is false. The CDF hypotheses are satisfiable, and the sanity file constructs the isorevenue law.

Needed infrastructure: the regret representation of Proposition 1 for a joint law; Myerson-type payment identities for DSIC mechanisms (for the second inequality); Milgrom–Weber Theorem 23 or a direct proof of the pmf inequalities for the indicator vector $\mathbf 1(v_k>p)$; the order-statistic identity. Affiliation and the order-statistic identity are reusable beyond auctions. Contributions to any milestone, or to these supporting results stated as separate theorems, 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
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1089–1122, 1982. https://doi.org/10.2307/1911865
• H. A. David, H. N. Nagaraja, Order Statistics, 3rd ed., Wiley, 2003. https://doi.org/10.1002/0471722162
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 560–569, 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560

Motivation

Remote driving, or tele-driving, lets a human operator in a control center drive a vehicle over a wireless link. A ride-hailing platform that adopts it decouples drivers from vehicles: a driver is attached to a vehicle only while that vehicle carries or fetches a customer, and is released the moment the trip ends. Since an idle vehicle needs no driver, the platform can run a fleet of $m$ vehicles with $n \le m$ drivers. The operational question is how much service is lost by having fewer drivers than vehicles.

Benjaafar, Wang and Yang study this question with a loss queue in which the service rate depends on the number of idle vehicles, capturing the fact that pickups take longer when fewer vehicles are free (SSRN 4130757; published in Management Science, 2024, doi:10.1287/mnsc.2022.01687). The state-dependent rate builds on the spatial capacity model of Besbes, Castro and Lobel (doi:10.1287/opre.2021.2112). Their main finite-system results describe how the service level changes with the number of drivers in three regimes of vehicle supply. This mission formalizes the third regime, where vehicles are ample. The source is the authors' 2023 SSRN working paper; all labels and page numbers below refer to it.

Setting

A fleet of $m$ vehicles is operated by $n \le m$ remote drivers. Customers request trips according to a Poisson process with rate $\lambda > 0$. A request that arrives when all $n$ drivers are busy is lost. When $q$ customers are in service, each one completes at rate $\mu(m,q)$, so the total completion rate is $q\,\mu(m,q)$. The rate is defined for real $q \in [1,m]$. Let

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

The number of customers in service is a birth–death chain on $\{0,\dots,n\}$. Its stationary law 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,$$

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

The paper's standing assumptions on the rate are:

• Assumption 1. $\mu(m,q)$ is strictly increasing in $m$, decreasing in $q$, and strictly concave in $q$; $\mu(m,q) \to 1/s$ as $m \to \infty$, where $s > 0$ is the expected trip time; and $\mu(m,m)$ does not depend on $m$.
• Assumption 2. There is $\bar m > 0$ such that, for every $m \ge \bar m$, the map $q \mapsto q\,\mu(m,q)$ first increases and then decreases.
• Size restriction (p. 13). $m \ge \bar m$ and $\lambda > \max\{1/s,\ \max_{q \le \bar m} q\,\mu(\bar m,q)\}$.

The supply-rich regime $m > \gamma_2(\lambda)$ is the case $\rho(m) < 1$, that is, $\lambda < m\,\mu(m,m)$: even with every vehicle busy, the system clears work faster than it arrives. In this regime there is a unique $q_3 \in (1,m)$ with $\rho(q_3) = 1$, and $\rho(q) < 1$ exactly when $q > q_3$.

Formalization targets

Goal: Theorem 1.C (pp. 20–21)

In the supply-rich regime, $SL(m,n)$ is strictly increasing in $n \in \{1,\dots,m\}$. For every $n \in \{1,\dots,m\}$ with $n > q_3$,

$$SL(m,n) > 1 - \frac{1}{n - \lfloor q_3 \rfloor}.$$

Milestones

1. Lemma 3, first sentence: $\rho$ is strictly convex and $1/\rho$ is strictly concave on $[1,m]$.
2. Lemma 3(iii): in the supply-rich regime the root $q_3$ exists, with $\rho < 1$ exactly to its right.
3. Lemma 4: $\pi_{m,n-1}(n-1) > \pi_{m,n}(n)$ holds if and only if $\pi_{m,n-1}(n-1) > (\rho(n)-1)/\rho(n)$, and if and only if $\pi_{m,n}(n) > (\rho(n)-1)/\rho(n)$.
4. App. C.3: $\pi_{m,n}(n)$ is strictly decreasing in $n \in \{1,\dots,m\}$.
5. App. C.3: $\pi_{m,n}(n) < 1/(n - \lfloor q_3 \rfloor)$ for $q_3 < n \le m$.

Significance

The first part of Theorem 1.C says that, when vehicles are ample, every driver removed costs some service. The second part says the cost is small once $n$ exceeds $q_3$ by a margin. The bound $1 - 1/(n - \lfloor q_3 \rfloor)$ is increasing and concave in $n$, so a platform can run noticeably fewer drivers than vehicles at a controlled loss of service. The paper's numerical study (Figure 7) reports reductions of 35–60% in the number of drivers at a service loss below 0.01. The same objects carry over to the paper's asymptotic Theorem 2.C, where the driver-to-vehicle ratio needed in a large supply-rich market tends to $1/\alpha$.

The result is proved on paper and has no machine-checked proof. The work this mission adds is formal:

• statements of the model in which the regimes are explicit and the threshold $q_3$ is pinned by its characterization;
• a proof of the convexity and root structure of $\rho$ that does not rely on second derivatives, which the paper uses but the assumptions do not supply;
• the comparison lemma for consecutive blocking probabilities, which the companion missions on this paper also use.

Difficulty

$\pi_{m,n}(n)$ is a ratio whose numerator and denominator both change with $n$. For the drivers beyond $q_3$, monotonicity is immediate, since each additional factor $\rho(n) < 1$ shrinks the numerator while the denominator grows. Below $q_3$, $\rho(n) \ge 1$ and the numerator grows, so that argument fails, and the comparison has to use the shape of $\rho$ on $[1, q_3]$. The shape of $\rho$ (Lemma 3) has to be derived from concavity and monotonicity of $\mu$ alone: the assumptions give no smoothness, although the paper's proof differentiates twice. The page argues the two ranges separately, so the step across $q_3$ also has to be covered. The lower bound needs care at the integer part of $q_3$: the sum in the denominator is taken from $\lfloor q_3 \rfloor$, which is at least 1 only because $q_3 > 1$.

Formalization scope

• The rate is a function $\mu : \mathbb N \to \mathbb R \to \mathbb R$, with $m$ natural and $q$ real. Assumptions 1–2 are imposed only for $q \in [1,m]$. "Decreasing in $q$" is read as non-increasing. Positivity of $\mu$ and $s > 0$, implicit on the page, are stated. Assumption 2's "first increases then decreases" is a turning point strictly inside $(1,m)$.
• Every statement carries Assumptions 1–2 and the size restriction as explicit hypotheses. The regime $m > \gamma_2(\lambda)$ is stated through its characterization $\lambda < m\,\mu(m,m)$; $\gamma_2$ itself is not defined.
• $q_3$ is a real variable with its Lemma 3(iii) characterization: $q_3 \in [1,m]$, $\rho(q_3) = 1$, and $\rho(q) < 1$ exactly for $q > q_3$ in $[1,m]$. This determines $q_3$ uniquely, and milestone 2 shows that such a $q_3$ exists. No monotonicity of $\rho$, $\pi$ or $SL$ is assumed anywhere; such facts are milestones.
• $n$ ranges over $\{1,\dots,m\}$. $\lfloor q_3 \rfloor$ is the natural-number floor, and $n - \lfloor q_3 \rfloor$ is computed in $\mathbb R$.
• "Increasing" and "lower bounded" are stated strictly, as the paper's proof derives them.
• A statement that assumed $\pi_{m,n}(n)$ decreasing, or left $q_3$ unconstrained, would make the goal trivial or vacuous. Neither is done here.

Needed infrastructure: finite products and sums over Finset.Icc, StrictConvexOn/StrictConcaveOn on intervals, and the intermediate value theorem for a function that is continuous on $[1,m)$. The model file is shared, up to namespace, with four companion missions on the same paper. Proofs of the general facts used here are reusable beyond this mission and are welcome as separate contributions: the product of a positive increasing linear function and a positive antitone concave function is concave, and the reciprocal of a positive strictly concave function is strictly convex.

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. https://doi.org/10.1287/opre.2021.2112

Motivation

Decision makers facing uncertainty treat different sources of uncertainty differently. The Ellsberg paradox, home bias in investment, and the competence effect all show people preferring bets on one source (a known urn, domestic stocks, a familiar domain) over equally likely bets on another. Ambiguity theories try to describe these differences. Most of them are hard to apply empirically because they work with sets of priors or nonadditive measures on the whole state space.

Baillon, Bleichrodt, Li and Wakker (Management Science 71(10), 2025) propose source theory. Within a source, the agent behaves as if she has a probability measure (probabilistic sophistication). Across sources, she may weight those probabilities differently, through a source function $w_{\mathcal S}$. Two attitude components measure the difference between sources: source preference (ambiguity aversion) and insensitivity (a-insensitivity, the tendency to treat all intermediate likelihoods alike). Their Theorem 4 answers a basic question for this framework. When are two sources at exactly the same level on both components?

Setting

A state space $S$ carries an algebra $\mathcal E$ of events. An act is a finite-valued map $x : S \to \Gamma$ into an outcome set $\Gamma$ whose level sets are events. A weak order $\succcurlyeq$ on acts is represented by biseparable utility: a utility $U$ on outcomes and a weighting function $W$ on events ($W(\emptyset)=0$, $W(S)=1$, monotone) evaluate a binary act $\gamma E \beta$ with $\gamma \succcurlyeq \beta$ by $W(E)U(\gamma) + (1-W(E))U(\beta)$. Structural Assumption 1 adds three nonindifferent outcomes, convex rangedness of $W$, strong monotonicity, cumulative dominance and an Archimedean axiom. Events are ranked by $W$: $A \succcurlyeq B$ iff $W(A) \ge W(B)$.

A source is a subalgebra $\mathcal S \subseteq \mathcal E$ on which $W$ is convex ranged. It is uniform if a finitely additive probability measure $P_{\mathcal S}$ on $\mathcal S$ satisfies stochastic dominance for all acts from $\mathcal S$. Then $W = w_{\mathcal S} \circ P_{\mathcal S}$ on $\mathcal S$ for a continuous, strictly increasing $w_{\mathcal S} : [0,1] \to [0,1]$, the source function.

For two sources $\mathcal A$ and $\mathcal C$:

• $\mathcal C$ is preferred to $\mathcal A$ (Definition 2) if for $A_1 \in \mathcal A$, $C_1 \in \mathcal C$, $W(A_1) = W(C_1)$ implies $W(A_1^c) \le W(C_1^c)$.
• $\mathcal A$ is more insensitive than $\mathcal C$ with insensitivity region $[B, D]$ (Definition 4) if, for matching threefold partitions, the middle cell of $\mathcal A$ gains at least as much weight as that of $\mathcal C$ when moved from the worst to the middle rank (if the worst cell is large enough, bounded by $D$), and dually at the best rank (if the best cell is at least as likely as $B$).
• The region $[B, D]$ is regular for $\mathcal S$ if every fourfold partition of $S$ from $\mathcal S$ has a cell $E_j$ with $E_j \succcurlyeq B$ and $E_j^c \preccurlyeq D$.
• Two sources are equally preferred (equally insensitive) if the relation holds in both directions.

Formalization targets

Goal: Theorem 4

Under Assumption 1, sources $\mathcal A$ and $\mathcal C$ are equally preferred and equally insensitive with a regular insensitivity region if and only if both are uniform and

$$w_{\mathcal A} = w_{\mathcal C}.$$

Moreover, $\mathcal A$ and $\mathcal C$ are then equally insensitive with the maximal region $[\emptyset, S]$.

Milestones

In the order of the proof (p. 8780):

1. the reversed implication, which the paper calls direct;
2. transitivity of source preference and insensitivity (Observation 3);
3. Theorem 1: a source is uniform iff it is equally preferred and insensitive to itself with a regular region;
4. for a uniform source, a regular region $[B, D]$ from the source has $P(B) \le \tfrac14 \le \tfrac34 \le P(D)$;
5. for equally preferred uniform sources, the pmatcher $\varphi$ with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ satisfies $\varphi(p) + \varphi(1-p) = 1$, so $\varphi(\tfrac12) = \tfrac12$;
6. insensitivity in each direction makes $\varphi$ and $\varphi^{-1}$ sub-additive on $[0, \tfrac12]$;
7. these two inequalities and $\varphi(\tfrac12) = \tfrac12$ force $\varphi$ to be linear on $[0, \tfrac12]$;
8. $\varphi$ is then the identity on $[0, 1]$.

Significance

The theorem says that a comparison of ambiguity attitudes "at the same level" is only possible between uniform sources. Equal preference and equal insensitivity, both observable through bets, already force probabilistic sophistication within each source and identical source functions. With risk as the second source, it characterizes ambiguity neutrality of a source behaviorally (Corollary 1 of the paper). It also shows that both attitude components are needed: the paper's Example 1 exhibits sources that are equally preferred but differ in insensitivity.

The result is proved in the paper, partly by reference. The linearity step defers to an Online Appendix, and Theorem 1's proof relies on a representation theorem of Krantz, Luce, Suppes and Tversky (1971). As far as known, none of the paper's results has a machine-checked proof. A formalization would check the paper's proof, including the deferred functional-equation step and the boundary bookkeeping of insensitivity regions. It would also provide a reusable Lean layer for Savage-style acts, biseparable utility and comparative ambiguity attitudes.

Difficulty

The forward direction is the hard one. The obvious route is to compare the two sources directly through the pmatcher $\varphi$. But $\varphi$ exists only once both sources are known to be uniform, and nothing in the hypotheses says so. The proof first collapses the cross-source conditions into conditions of each source with itself, by transitivity, and then invokes Theorem 1. Theorem 1 in turn needs a qualitative-probability representation theorem.

Once $\varphi$ exists, the insensitivity conditions give only one-sided inequalities: $\varphi$ and $\varphi^{-1}$ are sub-additive on $[0, \tfrac12]$. Sub-additivity of $\varphi^{-1}$ gives super-additivity of $\varphi$ only where $\varphi(p) + \varphi(\varepsilon) \le \tfrac12$. The symmetry $\varphi(\tfrac12) = \tfrac12$, which comes from source preference, is what closes the gap. Regularity is used twice: it brings Theorem 1 into play, and it guarantees that the region's upper bound lies above probability $\tfrac12$.

Formalization scope

The Lean development works in the sub-namespace SourceTheory.EqualSources, with one definition module holding the whole model:

• Assumption1 bundles Structural Assumption 1.
• IsSource is a subalgebra on which $W$ is convex ranged.
• IsUniformWith and IsSourceFunction encode uniformity and (5).
• IsPreferredTo, IsMoreInsensitive and IsRegularRegion encode Definition 2, Definition 4 and regularity.

Conventions committed to:

• events form an algebra $\mathcal E$, which the paper allows in its endnote 1;
• convex rangedness is imposed on $\mathcal E$ and on each named source, since the trivial algebra is never convex ranged;
• event preference is $W$-order;
• probability measures are finitely additive;
• twofold partitions are $(A_1, A_1^c)$, and partitions may have empty cells;
• a "transformation" is a continuous probability weighting function;
• the pmatcher is a binder with $w_{\mathcal A} = w_{\mathcal C} \circ \varphi$ on $[0,1]$, and its inverse is a binder with two-sided inverse laws, never Function.invFun;
• the region in Theorem 4 is read as regular for both sources, and "$w_{\mathcal A} = w_{\mathcal C}$" as a single function that is the source function of both.

The goal deliberately has no Assumption 2: the paper says it is implied by the other conditions, and adding it would weaken the theorem. Neither regularity hypothesis may be dropped either. Without regularity, a degenerate region such as $[S, \emptyset]$ makes the insensitivity conditions nearly empty, and the left-hand side holds for sources that are not uniform.

A complete development needs:

• finitely additive probabilities on algebras;
• a range lemma (convex rangedness makes $P_{\mathcal S}$ onto $[0,1]$);
• the Krantz et al. representation of qualitative probabilities;
• an interval version of the Cauchy functional equation.

The last two are reusable beyond this mission. Contributions to any milestone, and to the shared model layer, are welcome.

Selected references

• A. Baillon, H. Bleichrodt, C. Li, P. P. Wakker, Source Theory: A Tractable and Positive Ambiguity Theory, Management Science 71(10):8767–8782, 2025. https://doi.org/10.1287/mnsc.2023.03307
• D. H. Krantz, R. D. Luce, P. Suppes, A. Tversky, Foundations of Measurement, Vol. I, Academic Press, 1971.
• D. Ellsberg, Risk, Ambiguity, and the Savage Axioms, Quarterly Journal of Economics 75(4):643–669, 1961. https://doi.org/10.2307/1884324
• L. J. Savage, The Foundations of Statistics, Wiley, 1954.