Mechanism Design

Motivation

In a budget-feasible procurement auction an auctioneer with a budget $B$ buys services from strategic sellers. Each seller knows privately what providing the service costs, and the auctioneer wants a set of services of maximum value without paying more than $B$ in total. The model was introduced by Singer (FOCS 2010) and is used to study crowdsourcing, data acquisition from individuals, and influence maximization in networks, where the value of a set of sellers typically shows diminishing returns: it is submodular.

Most of the mechanisms known for this problem are randomized, or are deterministic only when the auctioneer's valuation is monotone, i.e. adding a seller never lowers the value. Amanatidis, Kleer and Schäfer named the existence of deterministic budget-feasible constant-factor mechanisms for submodular valuations the most intriguing open problem of the area. Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) give deterministic clock auctions for these settings. In a clock auction each bidder only ever sees a sequence of decreasing take-it-or-leave-it prices, which makes truthful behaviour obvious to the bidders. This mission covers §4 of that paper: the first deterministic budget-feasible mechanism with a constant approximation ratio for general, not necessarily monotone, submodular valuations.

Timeline. Singer (2010) gave the first budget-feasible mechanisms for monotone submodular valuations. Chen, Gravin and Lu (SODA 2011) improved the constants. Amanatidis, Kleer and Schäfer (EC 2019) gave a randomized 505-approximate mechanism for non-monotone submodular valuations and introduced the idea of building two disjoint tentative sets simultaneously. Balkanski et al. (2021) give a deterministic clock auction for this class with approximation ratio 64.

Setting

There are $n$ bidders $N = \{0, \dots, n-1\}$. Bidder $i$ has a private cost $c_i \ge 0$, the least payment it accepts. The auctioneer has a budget $B > 0$ and a valuation $v : 2^N \to \mathbb{R}_{\ge 0}$ that is submodular: $v(S) + v(T) \ge v(S \cap T) + v(S \cup T)$ for all $S, T \subseteq N$. The marginal contribution of $T$ to $S$ is $v(T \mid S) = v(S \cup T) - v(S)$. A set $O$ is budget feasible if $\sum_{i \in O} c_i \le B$, and $OPT$ is the largest value of a budget-feasible set.

Simultaneous-Iterative-Pruning (Mechanism 3) works in phases with a target $\widetilde{OPT}_t$ that starts at $\max_i v(\{i\})$ and doubles in each phase. In phase $t$ it grows two disjoint tentative sets $S^1_t$ and $S^2_t$. At each step it picks a bidder $i$ and an index $k \in \{1,2\}$ maximizing $v(\{i\} \mid S^k_t)$, offers the price $p_i \leftarrow \min\{p_i,\ v(\{i\} \mid S^k_t)\cdot B/\widetilde{OPT}_t\}$, and adds $i$ to $S^k_t$ if it accepts. A bidder who rejects leaves the auction for good. A phase ends when one of the two sets reaches the target or no bidder remains to be offered a price. The two sets of the previous phase are set aside during a phase. After the last phase $\hat t$, an unconstrained submodular maximization subroutine $\mathrm{USM}$ is applied to the four sets of the last two phases, giving $T^k_j = \mathrm{USM}(S^k_j)$. The mechanism returns the best of the six sets $S^1_{\hat t-1}, S^2_{\hat t-1}, T^1_{\hat t}, T^2_{\hat t}, T^1_{\hat t-1}, T^2_{\hat t-1}$, minus its last added bidder if the prices of its bidders exceed $B$. The subroutine is required to be a 2-approximation: $\mathrm{USM}(X) \subseteq X$ and $2\,v(\mathrm{USM}(X)) \ge v(Y)$ for all $Y \subseteq X$.

Formalization targets

Goal: Theorem 5 (p. 12)

For every non-negative submodular $v$, costs $c \ge 0$, budget $B > 0$ and 2-approximate subroutine $\mathrm{USM}$, the set $S$ and prices $p$ returned by Simultaneous-Iterative-Pruning satisfy

$$\sum_{i \in S} p_i \le B \qquad\text{and}\qquad v(O) \le 64\, v(S) \ \text{ for every budget-feasible } O.$$

Milestones

• Lemma 6 (p. 12): the bidders of a budget-feasible $O$ rejected in phase $t \le \hat t$ have value $v(O^-_t) \le 6\,\widetilde{OPT}_t$. The page prints "$\ge$", a typo the proof corrects.
• Corollary 1 (p. 13): the bidders of $O$ still active at the end of phase $t$ have value $v(O^+_t) \ge v(O) - 12\,\widetilde{OPT}_t$.
• Lemma 7 (p. 13): one of the six candidates has value at least $v(O)/32$.
• Budget feasibility (p. 12): $\sum_{i \in S} p_i \le B$.
• Pruning step (p. 14): $v(S)$ is at least half the value of every candidate.

Significance

Theorem 5 shows that, for budget-feasible procurement with submodular valuations, determinism costs only a constant factor even without monotonicity. Before this paper no deterministic mechanism, polynomial-time or not, achieved a constant ratio for non-monotone submodular valuations. The mechanism is also a clock auction, whose interface to the bidders is a sequence of decreasing prices. The constant 64 is not claimed to be tight, and better constants are open.

No part of this paper is formalized anywhere that we know of. A machine-checked proof would verify an argument whose bookkeeping is easy to get wrong: two simultaneous tentative sets, sets of the previous phase put aside and later returned to the pool, prices that are lowered across phases, and a pruning step whose case analysis depends on the phase a candidate comes from. The formalization already surfaced two issues in the printed text. Lemma 6 states the wrong inequality. And for $n = 1$ it needs $v(\emptyset) = 0$, a normalization the paper never assumes.

Difficulty

The approach of the monotone case does not carry over. There, the value of the active optimal bidders is bounded by the value of all active bidders, and that fails once adding a bidder can lower the value. The proof therefore has to account separately for the optimal bidders the auction rejects (Lemma 6, which uses both tentative sets of a phase to absorb the rejected bidders) and for those it keeps, whose value is recovered only through the unconstrained maximization step applied to the four tentative sets of the last two phases (Lemma 7). Budget feasibility needs the fact that every accepted bidder's marginal contribution was non-negative when it was added. Otherwise its offered price would have been negative and it would have rejected. The final pruning step must not lose more than half the value. This holds because a removed bidder's marginal contribution is at most the initial target, while the best candidate exceeds twice that whenever a removal happens.

Formalization scope

Bidders are Fin n and sets of bidders are Finset (Fin n). The tentative sets are lists in insertion order, so that "the last bidder added" is defined; the candidate $T^k_j$ is the sublist of $S^k_j$ of the bidders that lie in $\mathrm{USM}(S^k_j)$. Valuations, costs and prices are real. The model's standing assumptions appear as hypotheses: $v \ge 0$, $v$ submodular (the published definition NonmonotoneSubmod.Shared.Submodular), and $c_i \ge 0$. A bidder offered the price $x$ accepts iff $c_i \le x$. Every argmax breaks ties by the least bidder index (in line 5, least bidder first, then $k = 1$ before $k = 2$; in line 12, the first maximizer in the printed order). The paper fixes no tie rule, and its claims hold for any.

Added hypotheses: $B > 0$ everywhere (the paper says only "a budget $B$"), and, in Lemma 6 only, "$n \ge 2$ or $v(\emptyset) = 0$", which excludes the one-bidder instances where the printed lemma fails. The theorems quantify over every subroutine $\mathrm{USM}$ with the 2-approximation guarantee. The paper's example of such a subroutine (Buchbinder et al.) is randomized, and a deterministic 2-approximation exists (Buchbinder and Feldman 2018). The phase loop runs with fuel $n + 2$. For non-negative submodular $v$ this is enough unless $\max_i v(\{i\}) = 0$, in which case $v \equiv 0$ and every statement is trivial.

Out of scope: running time (Lemma 12 and the "polynomial-time" clause) and the incentive properties. The clock-auction property is built into the definition, as every price update is a minimum with the old price. A Lean function is deterministic.

The goal cannot be satisfied trivially. It is stated about the mechanism's actual output for every non-negative submodular $v$ and every admissible subroutine, and the approximation compares $v(S)$ with every budget-feasible set rather than a supremum. Requiring $\mathrm{USM}$ to be an exact maximizer would weaken the theorem and is not done. Contributions of general lemmas on submodular functions (subadditivity of non-negative submodular functions, telescoping marginal sums along a list) are reusable well beyond this mission.

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. https://doi.org/10.1109/FOCS.2010.78
• N. Chen, N. Gravin, P. Lu, On the Approximability of Budget Feasible Mechanisms, SODA 2011. https://arxiv.org/abs/1007.3801
• G. Amanatidis, P. Kleer, G. Schäfer, Budget-Feasible Mechanism Design for Non-Monotone Submodular Objectives: Offline and Online, EC 2019; Mathematics of Operations Research 47(3), 2022. https://arxiv.org/abs/1905.00848
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5), 2015. https://doi.org/10.1137/130929205
• N. Buchbinder, M. Feldman, Deterministic Algorithms for Submodular Maximization Problems, ACM Trans. Algorithms 14(3), 2018. https://doi.org/10.1145/3184990

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

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

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

In budget-feasible procurement an auctioneer with a budget $B$ wants to buy services from $n$ strategic sellers. Each seller $i$ has a private cost $c_i\ge0$, the auctioneer has a public valuation $v$ over sets of sellers, and the mechanism must choose whom to pay and how much, so that sellers have no reason to misreport and the total payment never exceeds $B$. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a buyer with a fixed budget faces sellers whose costs it cannot observe.

Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239v2, Operations Research 2025) show that deterministic clock auctions, which repeatedly lower personalized prices and let sellers drop out, achieve constant approximations for monotone submodular valuations. Their Appendix B asks whether an even simpler family suffices: posted-price mechanisms, which approach each seller once with a take-it-or-leave-it offer. This mission formalizes their answer for additive valuations, Theorem 13 (p. 25): no deterministic posted-price mechanism achieves an approximation better than $\sqrt n/2$.

Setting

There are $n$ sellers $N=\{0,\dots,n-1\}$, a budget $B>0$, private costs $c_i\ge0$, and a valuation $v:2^N\to\mathbb R_{\ge0}$. The valuation is additive if there are values $v_i\ge0$ with $v(S)=\sum_{i\in S}v_i$ for every $S\subseteq N$.

A deterministic posted-price mechanism knows $n$, $B$ and $v$, but not $c$. It approaches sellers one at a time. At each step it looks at the history of earlier offers (the seller, the price, and whether the seller accepted) and either stops or names a seller not yet approached and a price $p_i$. The seller accepts if $p_i\ge c_i$ and rejects otherwise, and is never approached again. The output $M(v,c)$ is the set of sellers who accepted; each of them is paid its price. The mechanism is budget feasible if for every additive $v$ and every cost profile $c\ge0$ the accepted prices sum to at most $B$.

For an instance, $\mathrm{OPT}$ is the largest value $v(O)$ of a set $O$ with $\sum_{i\in O}c_i\le B$. A mechanism is a $\rho$-approximation on a class if $\mathrm{OPT}\le\rho\,v(M(v,c))$ on every instance of the class.

In Lean the sellers are Fin n, a mechanism is M : (Finset (Fin n) → ℝ) → PostedPrice n with PostedPrice n a rule next : List (Fin n × ℝ × Bool) → Option (Fin n × ℝ) on histories, run (M v) c is its history on the costs c, and accepted and payment read off the output and the total payment.

Formalization targets

Goal: Theorem 13 (p. 25)

For every $n\ge1$, every $B>0$ and every budget-feasible deterministic posted-price mechanism $M$, there are an additive $v$, costs $c\ge0$ and a set $O$ with

$$\sum_{i\in O}c_i\le B,\qquad v(O)>0,\qquad \frac{\sqrt n}{2}\,v\big(M(v,c)\big)\le v(O).$$

This is $\mathrm{OPT}/v(M)\ge\sqrt n/2$ on some instance, written without division.

Milestones: the three cases of the proof (p. 25)

All three concern one valuation $v_0$: a high-value seller $b_h$ worth $\sqrt n$ and $n-1$ small sellers worth $1$ each, with $c_{b_h}=B$.

1. Case 1. If the first positive offer goes to a small seller $i$, before $b_h$ is approached, then on the costs $c_i=p_i$, $c_j=B$ otherwise, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n=v_0(\{b_h\})$.
2. Case 2. If every earlier offer is $0$ and $b_h$ is offered $B$, then on small costs $B/(n-1)$, $v_0(M)=\sqrt n$ and $\frac{\sqrt n}2 v_0(M)<n-1$ for $n\ge3$, the value of the budget-feasible set of small sellers.
3. Case 3. If every earlier offer is $0$ and $b_h$ is offered $p_h<B$, then on all costs $B$, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n$.

Significance

The theorem separates two families of simple mechanisms. Deterministic clock auctions achieve a constant approximation for monotone submodular valuations (Theorem 1 of the same paper, a $4.75$-approximation), while deterministic posted prices cannot achieve better than $\sqrt n/2$ even for additive valuations, the simplest class. Clock auctions are therefore not merely sufficient but needed among these simple formats: the ability to lower a price after a refusal is what the constant approximation rests on. The bound also explains why the paper's positive result for posted prices (Theorem 15, symmetric submodular valuations) must give up a logarithmic factor.

The result is proved in the paper; it has not been formalized. A formal version fixes what "deterministic posted-price mechanism" means, an adaptive rule on histories that never sees costs, and makes the adversary argument checkable: the hard instance depends on the mechanism, and the case analysis must be exhaustive over all such rules. The mission also provides a reusable model of sequential take-it-or-leave-it mechanisms with budget constraints.

Difficulty

The statement is a lower bound over all mechanisms, so the instance must be chosen after the mechanism. The mechanism is adaptive: which seller it approaches next and at what price can depend on every earlier answer. The proof handles this by noting that, on the hard family, every seller rejects a non-positive offer, so all instances share the run up to the first positive offer or the offer to $b_h$. Making that "common prefix" precise for an arbitrary history-dependent rule, and covering the mechanisms that fall outside the three printed cases (those that never approach $b_h$, or offer $b_h$ more than $B$), is the work of the formal proof. A naive attempt that fixes one instance for all mechanisms fails: a mechanism tailored to that instance is optimal on it.

Formalization scope

• Sellers are Fin n; valuations are functions Finset (Fin n) → ℝ, and additivity carries nonnegative weights. Costs are real and nonnegative.
• The budget satisfies $B>0$, an addition to §2's "a budget $B$"; with $B=0$ nothing can be bought.
• A mechanism may depend on the valuation (and on $n$ and $B$, which are fixed outside it) but not on costs. Prices are arbitrary reals. The run asks the rule for at most $n$ offers; a proposal of an already approached seller ends the run.
• Budget feasibility is a property of the mechanism on every additive instance, as defined on p. 24, not of a single run.
• $\mathrm{OPT}$ is never a supremum: the goal exhibits a budget-feasible set $O$ with $v(O)>0$. The condition $v(O)>0$ rules out the trivial instance with $\mathrm{OPT}=0$, where every bound holds.
• The Case 2 cost is $B/(n-1)$; the page prints $1/(n-1)$, which is budget feasible for the small sellers only when $B\ge1$.
• The cases' hypotheses ("before $b_h$", "price $0$") are read off the run on the profile with all costs $B$; "price $0$" is rendered as "price at most $0$".
• Out of scope: running time, truthfulness (posted-price mechanisms are truthful by construction), and randomized mechanisms.

Contributions welcome: proofs of the three cases, the "common prefix" lemma for runs on cost profiles that agree on every seller approached, and the assembly of the goal.

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.09239v2
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78

Motivation

A budget-feasible procurement auction buys services from strategic sellers under a hard budget. Each of $n$ bidders can provide a service at a private cost; the auctioneer values each set of acquired services through a set function $v$ and must keep total payments within a budget $B$. The question, introduced by Singer (FOCS 2010), is how much of the optimal value a truthful mechanism can secure when it does not know the costs. The model covers crowdsourcing, influence maximization with paid seeds, and experimental design with paid participants.

For subadditive valuations, the most general class with non-trivial guarantees, the timeline is short:

• Dobzinski, Papadimitriou and Singer (EC 2011) gave a randomized mechanism with an $O(\log^2 n)$ approximation and a deterministic one with $O(\log^3 n)$.
• Bei, Chen, Gravin and Lu (STOC 2012; SIAM J. Comput. 46(4), 2017) gave a randomized mechanism with an $O(\log n / \log\log n)$ approximation.
• Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239; Operations Research 2025) matched that bound with a deterministic clock auction, Mechanism 4 of their paper, Theorem 8.

Clock auctions are prized beyond truthfulness: they are obviously strategy-proof, they protect the privacy of the winners' costs, and a bidder only ever decides whether to accept a price that keeps falling.

Setting

There are $n$ bidders $N = \{1, \dots, n\}$. Bidder $i$ has a private cost $c_i \ge 0$, the least payment for which it provides its service, and it accepts an offered price $p$ exactly when $c_i \le p$. The auctioneer has a budget $B > 0$ and a valuation $v : 2^N \to \mathbb{R}_{\ge 0}$. The valuation is subadditive:

$$v(S \cup T) \le v(S) + v(T) \quad \text{for all } S, T \subseteq N.$$

It is not assumed monotone, nor normalized.

A set $O$ is budget feasible at true costs if $\sum_{i \in O} c_i \le B$; the optimum $\mathrm{OPT}$ is the largest value of such a set. A mechanism outputs a set $W$ and payments $p_i$ for $i \in W$; it is budget feasible if $\sum_{i \in W} p_i \le B$, and it is a $\rho$-approximation if $\mathrm{OPT} \le \rho \cdot v(W)$ on every instance.

Mechanism 4 runs in phases $t = 1, 2, \dots$ and keeps a set $A$ of active bidders and two solutions $S_{\mathrm{prev}}$ and $S_{\mathrm{curr}}$, all starting from $A = N$, $S_{\mathrm{prev}} = S_{\mathrm{curr}} = \emptyset$. While some active bidder lies outside $S_{\mathrm{prev}} \cup S_{\mathrm{curr}}$, a phase

1. increments $t$;
2. replaces $S_{\mathrm{prev}}$ by the more valuable of $S_{\mathrm{prev}}$ and $S_{\mathrm{curr}}$;
3. offers the price $B/t$ to every active bidder outside $S_{\mathrm{prev}}$; those with $c_i > B/t$ leave for good;
4. sets $S_{\mathrm{curr}}$ to the output of a 2-approximation oracle on the pool $A \setminus S_{\mathrm{prev}}$ at the current price level.

At price $B/t$ a set of candidates is affordable exactly when it has at most $t$ members, so the oracle $\mathrm{alg}(t, X)$ returns a subset of $X$ with at most $t$ members whose value is at least half that of every such subset. The paper uses the demand-query algorithm of Badanidiyuru, Dobzinski and Oren for this step. The mechanism returns the more valuable of the two solutions, $S_{\mathrm{final}}$, and pays each of its members its current price.

Formalization targets

Goal: Theorem 8

There is an absolute constant $C > 0$ such that for every $n \ge 3$, every instance $(v, c, B)$ as above, every oracle with the 2-approximation guarantee and every run of Mechanism 4 of at least $n$ phases,

$$\sum_{i \in S_{\mathrm{final}}} p_i \le B \qquad\text{and}\qquad v(O) \le C \cdot \frac{\log n}{\log \log n}\cdot v(S_{\mathrm{final}}) \ \text{ for every budget-feasible } O.$$

The constant is left unspecified, as in the paper's $O(\cdot)$; the proof gives roughly $40$ for large $n$.

Milestones

• Value monotonicity (p. 15): the value of the output never decreases as more phases run.
• The block bound (p. 15): a set $Z$ of $k \ge 1$ bidders, each of cost at most $B/k$, satisfies $v(Z) \le 4\,v(S_{\mathrm{final}})$.
• The subadditive cover (p. 16): if $O = Z_1 \cup \dots \cup Z_{r+1}$ then $v(O) \le \sum_{i} v(Z_i)$.
• The counting chain (p. 16): natural numbers $z_1, \dots, z_r \ge 1$ with $\frac{1}{z_1+1} + \sum_{i=1}^{r-1} \frac{z_i}{z_{i+1}+1} \le 1$ satisfy $z_r \ge (r/2)^r$.

Significance

Theorem 8 shows that randomization buys nothing asymptotically for budget-feasible procurement with subadditive valuations: the best known approximation factor is achieved by a deterministic mechanism, and moreover by a clock auction, which adds obvious strategy-proofness and transparency. It improves the previous best deterministic factor from $O(\log^3 n)$ to $O(\log n / \log\log n)$. The same template, two maintained solutions and a gradually refined benchmark, drives the paper's constant-factor auctions for submodular valuations (the companion missions of this series).

Nothing in this paper is formalized yet, and no budget-feasible mechanism exists on the platform. The mission produces a machine-checked model of a clock auction with an abstract demand oracle, a monotonicity lemma for two-solution auctions, and the counting argument behind the $\log n/\log\log n$ factor, which is a self-contained real inequality.

Difficulty

The obvious argument looks only at the phase whose size bound matches a large block $Z$ of the optimal set and invokes the oracle there. It fails because part of $Z$ may already sit in $S_{\mathrm{prev}}$, which is never offered to the oracle again, and because the output is decided in the last phase, when the bidders of $Z$ may have been priced out. Both gaps have to be closed with properties of the run (what the oracle guaranteed when $S_{\mathrm{prev}}$ was formed, and that the value of the output never decreases), not of a single phase.

The second case of the analysis, where every block is small, is a counting argument whose final contradiction is asymptotic and involves $\log\log$ terms that are only meaningful for large $n$. A statement with a single uniform constant must also cover small $n$, which the printed argument leaves implicit.

Formalization scope

• Bidders are Fin n, sets are Finset (Fin n), values and costs are real. Non-negativity of $v$ and $c$ are hypotheses; subadditivity is IsSubadditive v. No monotonicity or normalization is assumed.
• The budget is strictly positive, $B > 0$; the paper says only "a budget $B$".
• The oracle is an arbitrary function alg : ℕ → Finset (Fin n) → Finset (Fin n) satisfying IsTwoApproxOracle v alg; feasibility at price $B/t$ is encoded as cardinality at most $t$.
• The argmax steps keep $S_{\mathrm{prev}}$ on ties. Every bidder starts at the price $B$, which is never paid.
• The loop runs with a fuel $F$: it stops when its condition fails or after $F$ phases. The paper does not prove termination, and the loop need not terminate (zero-cost bidders never reject). The goal is stated for every $F \ge n$.
• $\mathrm{OPT} \le \rho\, v(S_{\mathrm{final}})$ is stated for every budget-feasible $O$, never through a supremum. The constant $C$ is quantified before $n$ and the instance; a constant chosen after the instance would make the statement trivial. The threshold $n \ge 3$ keeps $\log\log n > 0$.
• Out of scope: running time ("polynomial-time" has no Lean model here), determinism (automatic for a Lean function), and the clock-auction property, which is built into the definition (prices $B/t$ only fall; a rejecting bidder leaves for good). Truthfulness is a consequence of the clock format and is not stated.

Contributions welcome: proofs of the milestones and the goal; a concrete demand-oracle implementation satisfying IsTwoApproxOracle; and a definition of the block decomposition $Z_1, \dots, Z_{r+1}$ with the cost chain of p. 16, which this mission does not state.

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
• X. Bei, N. Chen, N. Gravin, P. Lu, Budget Feasible Mechanism Design: From Prior-Free to Bayesian, STOC 2012. https://doi.org/10.1145/2213977.2214039; journal version Worst-Case Mechanism Design via Bayesian Analysis, SIAM J. Comput. 46(4):1428–1448, 2017.
• A. Badanidiyuru, S. Dobzinski, S. Oren, Optimization with Demand Oracles, EC 2012. https://doi.org/10.1145/2229012.2229024
• S. Dobzinski, C. Papadimitriou, Y. Singer, Mechanisms for Complement-Free Procurement, EC 2011. https://doi.org/10.1145/1993574.1993602
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78

Budget-feasible procurement with posted prices

In budget-feasible procurement an auctioneer with a fixed budget $B$ wants to buy services from strategic sellers whose costs are private. The auctioneer values sets of services through a valuation function $v$, and wants a mechanism that pays the sellers at most $B$ in total while acquiring a set of nearly maximal value. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a platform recruits workers or data owners under a fixed spending cap.

Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) study deterministic clock auctions for this problem: mechanisms that offer each seller a sequence of non-increasing prices, where a seller who rejects an offer leaves for good. Clock auctions are obviously strategyproof and robust to collusion, which makes them attractive in practice. A posted-price mechanism is the most restrictive kind: every seller receives a single take-it-or-leave-it offer.

Appendix B of the paper asks how much is lost by restricting to posted prices. For additive valuations no deterministic posted-price mechanism beats $\sqrt{n}/2$ (Theorem 13). For symmetric submodular valuations, where the value of a set depends only on how many sellers it contains, no such mechanism achieves a factor better than $\log n/4$ (Theorem 14), and Theorem 15, the subject of this mission, shows that a simple posted-price mechanism achieves a logarithmic factor.

Setting

There are $n$ sellers (bidders) $N = \{1, \dots, n\}$. Seller $i$ has a private cost $c_i \ge 0$ and accepts an offered price $p$ exactly when $c_i \le p$. The auctioneer has a budget $B > 0$, and throughout this mission every cost satisfies $c_i \le B$, as the paper assumes for Mechanism 5.

A valuation $v : 2^N \to \mathbb{R}_{\ge 0}$ is symmetric submodular if there are numbers $r_1 \ge r_2 \ge \cdots \ge r_n \ge 0$ such that

$$v(S) = \sum_{i=1}^{|S|} r_i \qquad \text{for all } S \subseteq N.$$

The case $r_i \equiv 1$ counts the sellers bought.

A set $O \subseteq N$ is budget feasible at true costs if $\sum_{i \in O} c_i \le B$; the optimum $\mathrm{OPT}$ is the largest value $v(O)$ over such sets.

Mechanism 5 (p. 27) sets aside an arbitrary seller $j$ and keeps a counter $a$ of accepted offers, initially $0$, and a winning set $W$, initially empty. It visits every other seller once, offering

$$p_i = \frac{B}{2\ln n} \text{ if } a = 0, \qquad p_i = \frac{B}{a\cdot 2\ln n} \text{ if } a \ge 1;$$

a seller who accepts joins $W$ and increments $a$. If nobody accepted, $j$ is offered the whole budget $B$. Winners are paid their offered price. In Lean the mechanism is BudgetClock.PostedSym.mech5 n B c j, the loop is scan n B c j, and the valuation class is IsSymmetricSubmodular n v.

Formalization targets

Goal: Theorem 15

There is an absolute constant $C > 0$ such that for every $n \ge 2$, every symmetric submodular $v$, every budget $B > 0$, every cost vector with $0 \le c_i \le B$ and every choice of the set-aside seller $j$, the winning set $W$ of Mechanism 5 and its prices $p$ satisfy

$$\sum_{i \in W} p_i \le B \qquad\text{and}\qquad v(O) \le C\,\ln n \cdot v(W) \ \text{ for every budget-feasible } O.$$

The constant is left unspecified, as in the paper's $O(\log n)$; the goal survives any improvement of it.

Milestones

1. Budget feasibility (proof of Theorem 15, p. 27): the payments made during the scan stay strictly below $B$, and the payments of the final output are at most $B$.
2. Case 1 (p. 28): if no scanned seller accepts, then $W = \{j\}$ and $v(O) \le (2\ln n + 1)\,v(W)$ for every budget-feasible $O$.
3. Case 2 (p. 28, corrected): if at least one scanned seller accepts, then $v(O) \le (2\ln n + 2)\,v(W)$ for every budget-feasible $O$.

Significance

Theorem 15 locates the price of posting prices for symmetric submodular valuations: together with Theorem 14 (no deterministic posted-price mechanism beats $\log n/4$) it shows that the best such mechanism loses a factor of order exactly $\log n$, while the clock auctions of the main body of the paper achieve constant factors for all monotone submodular valuations. The gap between one-shot offers and descending clocks is therefore a genuine separation, not an artefact of the analysis.

The result is proved in the paper. Its formal value lies in pinning down the mechanism and the constants. Checking the printed argument against a precise model exposes three slips: the pseudocode never adds the set-aside seller to $W$, the printed payment bound fails for $2 \le n \le 6$, and the constant $2\ln n + 1$ of Case 2 ignores the set-aside seller and is false (see the milestone notes). None of them affects the $O(\log n)$ claim, and the formal statements record the corrected forms. To our knowledge no machine-checked proof of any result of this paper exists.

Difficulty

The mechanism decides each offer without knowing the remaining costs, and the optimum is defined at the true costs, which the mechanism never learns for rejected sellers. The only information available is a lower bound on each rejected seller's cost, and these lower bounds shrink as the counter $a$ grows. The difficulty is to convert the history of offers into an upper bound on how many sellers any budget-feasible set can hold, uniformly in the order of the scan and the choice of $j$, while keeping the total payment, a harmonic-type sum, below the budget for every $n \ge 2$. The set-aside seller is the subtle point: it receives no offer when $a \ge 1$, so nothing is known about its cost, and a count that forgets it is wrong.

Formalization scope

• Sellers are Fin n; costs are a real vector with $0 \le c_i \le B$; the budget is a real $B > 0$ (the paper says only "a budget $B$"; $B > 0$ is an added hypothesis, since a zero budget makes every offer zero).
• The scan visits $[n]\setminus\{j\}$ in increasing index order. The paper's "arbitrarily ordered" sellers and "arbitrary agent $j$" are covered because every statement quantifies over all cost vectors and all $j$; relabelling sellers changes only the costs.
• A seller accepts iff $c_i \le p_i$. The mechanism returns the winning set and the price offered to each seller (zero for a seller who was never offered anything).
• The set-aside seller $j$ joins $W$ when it accepts the offer $B$. The printed pseudocode omits this step, but the proof relies on it, and without it the goal is false when every scanned seller rejects.
• The symmetric submodular sequence is indexed from $0$ in Lean (r 0 is $r_1$).
• $\mathrm{OPT}$ is never a supremum: the approximation is stated as $v(O) \le C\ln n\cdot v(W)$ for every budget-feasible $O$ at true costs, which avoids dividing by $v(W)$.
• The constant $C$ is quantified before $n$ and all instance data, so it is uniform. The threshold $n \ge 2$ is required: $\ln 1 = 0$, and at $n = 1$ the price $B/(2\ln n)$ is a division by zero, which Lean evaluates to $0$.
• Out of scope: running time, determinism (every Lean function is deterministic) and the posted-price property (built into the definition: each seller receives at most one offer).
• A formalization in which $C$ depends on $n$ or on the instance, or in which $\mathrm{OPT}$ is taken over a set that excludes $j$, would make the goal trivial or different; both are ruled out by the statement's quantifier order and by quantifying over all budget-feasible $O \subseteq N$.

A complete development needs elementary facts about finite sums, the harmonic numbers ($H_m \le 1 + \ln m$, available in Mathlib) and a reasoning principle for the left fold that defines the scan; the latter is reusable for any sequential posted-price mechanism. Proofs of the three milestones, and of the goal from them, are all 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. https://doi.org/10.1109/FOCS.2010.78
• A. Badanidiyuru, R. Kleinberg, Y. Singer, Learning on a Budget: Posted Price Mechanisms for Online Procurement, EC 2012. https://doi.org/10.1145/2229012.2229026
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x