Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

• 1961: Vickrey introduces the second-price auction (J. Finance 16).
• 1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
• 1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$-approximation, and that no truthful mechanism beats ratio 2.
• 2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$'s type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$. A type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

and agent $i$'s valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$.

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$, and hands agent $i$ a payment $p^i(d)$. Agent $i$'s utility is $p^i(d) + v^i(x(d), t^i)$, with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$'s utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$-approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$.

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$:

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

Milestones

1. Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
2. MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$, and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$.
3. Claim 4.2: MinWork is strongly truthful.
4. $g(x(t),t) \le \sum_{j} \min_i t^i_j$.
5. $g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$.
6. Claim 4.3: MinWork is an $n$-approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

• Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
• Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
• The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
• $n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$. There is no hypothesis on $k$.
• The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
• Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$.
• Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$, instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$. The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
• Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
• Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

Motivation

In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has $2^m$ numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.

The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order $\sqrt m$. For general valuations in the value-query model the paper cites a lower bound of order $m/\log m$ (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within $m^{1/2-\epsilon}$ with polynomially many value queries.

Setting

A set $M=\{1,\dots,m\}$ of items is sold to $n$ bidders. Bidder $i$ has a valuation $v_i$ that assigns a real number $v_i(S)$ to every bundle $S\subseteq M$. Throughout, valuations are normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free (CF) if $v(S\cup T)\le v(S)+v(T)$ for all bundles $S,T$. An allocation $A=(A_1,\dots,A_n)$ gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is $\sum_i v_i(A_i)$.

The mechanism receives reports $b=(b_1,\dots,b_n)$ and runs the following algorithm $\mathrm{ALG}$:

1. query $b_i(M)$ and $b_i(\{j\})$ for every bidder $i$ and item $j$;
2. compute a maximum-weight matching $P$ in the complete bipartite graph between items and bidders, where the edge between item $j$ and bidder $i$ costs $b_i(\{j\})$;
3. if the bidder $t$ maximizing $b_i(M)$ has $b_t(M)$ strictly larger than the weight $|P|$, give all items to $t$; otherwise give every item matched by $P$ to its matched bidder.

Its range $R$ is the set of allocations that give all of $M$ to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder $i$ receives $\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$, so its utility is $v_i(\mathrm{ALG}(b)_i)+\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$. The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.

Formalization targets

Goal: Theorem 5.1 (p. 11)

For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile $v$ of normalized, monotone, CF valuations and every allocation $O$,

and the mechanism $(\mathrm{ALG},\text{VCG payments})$ is incentive compatible on the CF valuations.

Milestones, in attack order

1. §5.1, VCG. Welfare maximization with Groves payments is incentive compatible (a published platform theorem, AGT.vcg_incentive_compatible).
2. §5.1, maximal in range. Any allocation rule that optimizes reported welfare exactly over a fixed range is incentive compatible under VCG payments on the same domain.
3. ALG is maximal in range with range $R$ on normalized reports.
4. The CF single-item bound. For a CF valuation and $c\in T$ maximizing $v(\{j\})$ over $T$: $v(T)\le\sum_{j\in T}v(\{j\})\le|T|\,v(\{c\})$.
5. First case. If bidders with $|O_i|\ge\sqrt m$ carry at least half the welfare of $O$, then $\sum_i v_i(O_i)\le 2\sqrt m\,v_t(M)$ for the top bidder $t$.
6. Second case. Otherwise some allocation in which every bidder gets at most one item has welfare at least $\sum_i v_i(O_i)/(2\sqrt m)$.

Significance

The theorem shows that, for subadditive bidders, the $\sqrt m$ barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only $m+1$ value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than $m^{1/2-\epsilon}$.

The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant $2$ in the $O(\sqrt m)$ bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.

Difficulty

The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least $\sqrt m$ items, and the two cases need different facts: disjointness bounds the number of large bundles by $\sqrt m$, and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by $|T_i|$ and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.

Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.

Conventions the formalization commits to:

• Explicit constant. The paper writes $O(\sqrt m)$; its proof yields $2\sqrt m$ (both cases end with $|OPT|/(2\sqrt m)$), and the goal states $2\sqrt m$ with Real.sqrt m.
• Oracles and ties. The maximum-weight matching and the top bidder enter as functions mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between $b_t(M)$ and $|P|$ goes to the matching, as on the page.
• Payments. The mechanism pays each bidder $\sum_{k\ne i}b_k(\cdot)$, the paper's convention (footnote 2, p. 11); incentive compatibility is stated on the CF domain, the paper's. The local definition mirrors AGT.MechIncentiveCompatible on outcomes $a\mapsto v_i(a_i)$.
• Reference allocation. The approximation is stated against every allocation $O$, not only an optimal one; this is equivalent and avoids a junk maximum.
• Printed slips. The strict inequalities and the division by $|T_i|$ in the second case are replaced by non-strict, multiplied forms; the first case concludes for a bidder maximizing $v_i(M)$ rather than $v_i(O_i)$.
• Degenerate sizes. At $m=0$ everything is zero and the bound holds trivially; with $n=0$ no top-bidder rule exists.
• Out of scope. "In polynomial time" is a running-time claim and is not modelled.

A trivializing formalization is ruled out: the ratio is the explicit $2\sqrt m$ rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when $n\ge1$).

Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29:19–47, 2007. https://doi.org/10.1613/jair.2046
• S. Dobzinski, M. Schapira, Optimal Upper and Lower Approximation Bounds for k-Duplicates Combinatorial Auctions, working paper, The Hebrew University of Jerusalem, 2005 (reference [7] of the paper).
• L. Blumrosen, N. Nisan, On the Computational Power of Iterative Auctions I: Demand Queries, Discussion Paper 381, Center for the Study of Rationality, The Hebrew University of Jerusalem, 2005 (reference [2] of the paper).
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), in N. Nisan, T. Roughgarden, E. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, pp. 209–242.
• P. Cramton, Y. Shoham, R. Steinberg (eds.), Combinatorial Auctions, MIT Press, 2006.

Motivation

Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.

Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor $n$. Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.

Setting

There are $k$ tasks and $n$ agents. The type of agent $i$ is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive numbers, $t^i_j$ being the least time in which agent $i$ can perform task $j$. An allocation $x$ gives each task to one agent; $x^i$ is the set of tasks of agent $i$. For a type vector $t$ and for a vector $\tilde t$ of actual execution times the make-spans are

A mechanism with verification is a pair $(x, p)$. The allocation $x(d)$ is computed from the agents' declarations $d = (d^1,\dots,d^n)$ only. Each agent then performs its tasks, in any times $\tilde t_j \ge t^i_j$ it chooses, and the mechanism pays agent $i$ the amount $p^i(d, \tilde t)$, which may depend on the declarations and on the observed actual times. Agent $i$'s utility is $p^i(d,\tilde t) - \sum_{j \in x^i} \tilde t_j$. A strategy of agent $i$ therefore has two parts: a declaration $d^i$ and an execution plan $e^i$ that says, for every allocation, how long the agent takes on each of its tasks.

A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.

The Compensation-and-Bonus mechanism uses an optimal allocation algorithm $x(\cdot)$ and pays

where the corrected time vector $\mathrm{corr}^i$ lists agent $i$'s own tasks at their actual times and every other task at the time declared by the agent it was given to.

Formalization targets

Goal: Theorem 5.1

For $n \ge 2$ agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:

Milestones (proof of Claim 5.2)

1. The utility of every agent equals its bonus.
2. For every allocation, the bonus of agent $i$ is maximized by executing its tasks in minimal time.
3. With $t = (d^{-i}, t^i)$, for every declaration $t'^i$,

4. Declaring the true type and executing in minimal time is dominant.
5. Claim 5.2: the mechanism is strongly truthful.

Further target: Theorem 5.4

For $n \ge 2$ there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.

Significance

The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).

Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).

Difficulty

Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent $i$'s slower execution only hurts it when agent $i$ is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare $+\infty$ elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.

Formalization scope

• Agents are Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).
• Types and declarations are positive real vectors; declarations range over this type space (Definition 18's "unrestricted" declaration is any element of it).
• An execution plan is a function from allocations to actual times; feasibility for type $t^i$ requires $\tilde t_j \ge t^i_j$ on the agent's own tasks only. In the dominance quantifier the other agents' plans are arbitrary.
• Payments are amounts handed to the agent; utility is quasi-linear.
• The optimal allocation algorithm is a parameter with the hypothesis that it minimizes $g(\cdot, d)$ on every positive $d$; every theorem holds for every such algorithm.
• Strong truthfulness constrains both parts of the strategy: the declaration equals the type, and the plan executes every task in minimal time under every allocation.
• Thresholds made explicit: $n \ge 2$ in Claim 5.2, Theorem 5.1 and Theorem 5.4 (not printed; with one agent every declaration is dominant, and the construction of Theorem 5.4 needs a second agent).
• Printed slips: the displayed inequality prints >=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes $\tilde t_j = t_j$ for $\tilde t_j = t^i_j$.
• Running time is out of scope.
• A formalization in which dominance is checked only against truthful other agents, in which the mechanism ignores executions, in which strong truthfulness constrains only the declaration, or in which the implementation clause is stated only at the truthful profile, is not the theorem and is ruled out by the statements.

Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995.

Motivation

Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most $n$ against the optimum, and that no truthful mechanism can do better than a factor $2$. It then conjectures (Conjecture 4.9) that the factor $n$ cannot be improved by any truthful mechanism.

That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from $2$ to $1 + \sqrt 2$ (Christodoulou, Koutsoupias and Vidali), to $1 + \varphi \approx 2.618$ (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).

Setting

There are $k$ tasks $j \in \{1, \dots, k\}$ and $n$ agents $i \in \{1, \dots, n\}$. A type vector $t$ records, for every agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks of agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j \in X} t^i_j$. The make-span of $x$ is $g(x, t) = \max_i t^i(x^i)$.

A direct mechanism $(x, p)$ asks every agent for its type, computes an allocation $x(t)$ from the declarations, and hands agent $i$ the payment $p^i(t)$. Agent $i$'s utility is $p^i(t) - t^i(x^i(t))$ measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a $c$-approximation if $g(x(t), t) \le c \cdot g(y, t)$ for every type vector $t$ and every allocation $y$.

For a truthful mechanism the payment to agent $i$ depends only on the set it receives and on the declarations $t^{-i}$ of the others (Proposition 4.4). This gives the price offered to agent $i$ for a set $X$ (Definition 12):

A mechanism is local (Definition 14) if $p^i(X, t^{-i})$ depends only on the other agents' times $\{t^l_j : l \ne i, j \in X\}$ on the tasks of $X$. MinWork is local: its price for $X$ is $\sum_{j \in X} \min_{l \ne i} t^l_j$.

Formalization targets

Goal: Theorem 4.12

For every $n \ge 1$, every $k \ge n^2$ and every real $c < n$, no truthful local mechanism is a $c$-approximation:

The bound holds for every $c < n$, so together with MinWork it shows that $n$ is the exact best ratio for local truthful mechanisms.

Milestones

1. Proposition 4.4 (Independence). Payments depend only on the allocated set and on $t^{-i}$.
2. Proposition 4.5 (Maximization). $x^i(t)$ maximizes $p^i(X, t^{-i}) - t^i(X)$ over the sets $X$ that agent $i$ can obtain.
3. Lemma 4.13. Every type vector has type vectors arbitrarily close to it at which each agent's maximizing set is unique.
4. Claim 4.14, first step. If $x^i(t)$ is the unique maximizer, lowering agent $i$'s times on $x^i(t)$ keeps $x^i(t)$.
5. Ratio step. An allocation that gives one agent $n$ tasks of time about $1$, while every other agent's own tasks are nearly free, has make-span about $n$, while splitting those $n$ tasks gives make-span about $1$.

Significance

The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio $n$ must use prices that depend on the other agents' times on tasks outside the bundle.

Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.

Difficulty

An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price $0$. Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.

Formalization scope

Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).

Conventions and explicit thresholds:

• $k \ge n^2$. The theorem is printed without a bound on the number of tasks, and its proof begins "Let $k \ge n^2$". The goal carries $k \ge n^2$ as a hypothesis.
• Truthfulness is assumed. §4.3 assumes throughout that the mechanism is truthful (by the revelation principle this is no loss). The goal quantifies over all truthful local mechanisms.
• Prices use Definition 12 literally, including the value $0$ for sets the agent cannot obtain, and locality is Definition 14 applied to that price function over all sets $X$, not only single tasks. When several declarations give the same set, the price uses one chosen witness; by Proposition 4.4 the choice does not matter for truthful mechanisms.
• Proposition 4.5 is stated over the sets the agent can obtain. As printed, over all subsets, it is false for a truthful mechanism that never leaves an agent idle and pays it negative amounts. Uniqueness of maximizers (Lemma 4.13, Claim 4.14) refers to the same family.
• Lemma 4.13 uses Mathlib's norm on Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.
• Claim 4.14 is printed at $t^i_j = 1$ with $0 < \varepsilon < 1$. The first step is stated at any type vector, with $0 < \varepsilon \le t^i_j$ on the lowered tasks.
• Running time and computability are out of scope.

Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every $c < n$, not for some.

Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (pp. 876–880, basic properties of truthful mechanisms).
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Motivation

Algorithms deployed on the Internet often take their inputs from parties who own them and who may lie when lying pays. Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) proposed studying optimization problems in this setting: the algorithm designer may hand out payments, and must guarantee that the intended output is produced when every participant acts in its own interest. The paper's central test case is scheduling on unrelated machines, a standard problem of combinatorial optimization, in which the machines are the selfish participants and only they know how long each job takes them.

For this problem the paper shows that incentives cost a factor of two at least: with two or more machines, no mechanism can guarantee a make-span below twice the optimum. This was the first lower bound separating what incentive-compatible mechanisms can achieve from what ordinary approximation algorithms can achieve, and it started a line of work on the "Nisan–Ronen conjecture" (that the right factor for $n$ machines is $n$), with improved lower bounds by Christodoulou, Koutsoupias and Vidali (Algorithmica, 2009) and by Koutsoupias and Vidali (Algorithmica, 2013), and a resolution announced by Christodoulou, Koutsoupias and Kovács (STOC 2023).

Setting

There are $n$ agents (machines) $i = 1,\dots,n$ and $k$ tasks $j = 1,\dots,k$. Agent $i$'s private type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive real numbers, $t^i_j$ being the time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks given to agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j\in X} t^i_j$. The objective is the make-span

and an allocation rule is a $c$-approximation if its make-span is at most $c$ times that of every allocation, on every type vector.

A mechanism $m = (o,p)$ gives each agent $i$ a set $A^i$ of strategies. On a strategy profile $a = (a^1,\dots,a^n)$ it outputs an allocation $o(a)$ and hands agent $i$ a payment $p^i(a)$. An agent of type $t^i$ has utility $p^i(a) - t^i(o^i(a))$. A strategy is dominant if it maximizes the agent's utility whatever the others play. The mechanism implements a $c$-approximation if every agent of every type has a dominant strategy and every profile of dominant strategies yields a $c$-approximate allocation.

A direct mechanism $(x,p)$ has $A^i$ equal to the set of types, and is truthful if reporting the true type is dominant. For a truthful mechanism, the price $p^i(X,t^{-i})$ is the payment agent $i$ receives when, against the others' reports $t^{-i}$, some report of its own makes it receive exactly $X$ (and $0$ if none does); the price difference is $\Delta^i(A,B) = p^i(A\cup B,t^{-i}) - p^i(A,t^{-i})$.

Formalization targets

Goal: Theorem 4.6

For every $n\ge 2$, $k\ge3$ and $c<2$, no mechanism with any strategy sets implements a $c$-approximation:

Milestones

1. Proposition 2.1 (revelation principle): a mechanism implementing a $c$-approximation yields a truthful direct mechanism whose allocation rule is a $c$-approximation.
2. Theorem 4.6 for truthful mechanisms (§4.3): no truthful direct mechanism has a $c$-approximate allocation rule for $c<2$. With milestone 1 it gives the goal.
3. Proposition 4.4 (independence): for a truthful mechanism, $t_1^{-i}=t_2^{-i}$ and $x^i(t_1)=x^i(t_2)$ imply $p^i(t_1)=p^i(t_2)$.
4. Proposition 4.5 (maximization): $x^i(t)$ maximizes $p^i(X,t^{-i}) - t^i(X)$ over attainable $X$.
5. Lemma 4.7: the price-difference inequalities satisfied by $x^i(t)$, and the uniqueness statement for sets satisfying them strictly.
6. Claim 4.8: for two agents, all-ones types and $0<\varepsilon<1$, moving agent 1's times to $\varepsilon$ on its own bundle and $1+\varepsilon$ elsewhere leaves the allocation unchanged.
7. The even case of the ratio: at that perturbed instance the mechanism's make-span is $|x^2(t)|$ while some allocation achieves $\tfrac12|x^2(t)| + k\varepsilon$.

Significance

The result. Theorem 4.6 shows that the requirement of dominant-strategy incentive compatibility, by itself, rules out approximation ratios below $2$ for scheduling on unrelated machines, a problem for which polynomial-time $2$-approximation algorithms that ignore incentives exist (Lenstra, Shmoys, Tardos 1990) and for which the exact optimum is computable in exponential time. Combined with the MinWork mechanism of the same paper (an $n$-approximation), it determines the optimal ratio for two machines. It is the base case of the Nisan–Ronen conjecture and the prototype of the "characterize truthful mechanisms by prices" technique used throughout later work on the conjecture.

Formalizing it. The theorem has been proved since 1999, but no machine-checked version is known to exist. The mission produces a formal account of general mechanisms with arbitrary strategy sets, dominant-strategy implementation, the revelation principle in that generality, and the price characterization of truthful mechanisms (independence and maximization). These are reusable for every other lower bound in this paper and for the later literature on the conjecture.

Difficulty

The statement quantifies over all mechanisms, with arbitrary strategy sets and arbitrary payment functions, so no finite search settles it. The revelation principle reduces to truthful direct mechanisms, but even these are an infinite-dimensional family: the allocation rule may break ties in any way, and prices may be any functions of the other agents' reports.

The printed argument also has two places that need care. Proposition 4.5 and Lemma 4.7, as printed, range over all sets of tasks, while Definition 12 gives unattainable sets price $0$; the statements hold only over attainable sets, and are formalized that way. And the case where agent 2's bundle has odd size is dispatched in one sentence ("which still yields the same allocation"), which the preceding lemma does not justify when agent 2's best bundle at the perturbed prices is not unique. A complete formal proof of the goal must supply an argument for that case.

Formalization scope

• Agents are Fin n, tasks Fin k; an allocation is a function Fin k → Fin n; bundles may be empty. The make-span is a finite maximum and assumes $n\ge1$ (NeZero n).
• Types, declarations and misreports are strictly positive reals throughout (Definition 10). Utility is quasi-linear; payments are handed to the agent and may have either sign.
• A general mechanism has strategy sets A : Fin n → Type u (any universe), output $o$ and payments $p$ on dependent strategy profiles. Implements requires both that every agent of every positive type has a dominant strategy and that every profile of dominant strategies yields a $c$-approximate allocation. Dominance is against every profile of the others, not only dominant ones. Without the existence clause, a mechanism with no dominant strategies would implement vacuously; the definition excludes that.
• Thresholds made explicit: $n\ge2$ and $k\ge3$, both taken from the proof ("We prove the theorem for the case of two agents"; "Let $k\ge3$"). The goal holds for each fixed $n$ and $k$ and every $c<2$, for every mechanism, with no restriction on tie-breaking and no requirement of strong truthfulness. At $n=1$ the claim is false.
• Proposition 2.1 is stated for task scheduling with the $c$-approximation specification; "truthful implementation" is read as truth-telling dominant and the truthful output $c$-approximate.
• Printed slips: Proposition 4.5 and Lemma 4.7 are stated over attainable sets; the "Moreover" of Lemma 4.7 requires $Y$ attainable. The odd case of the ratio step is not a milestone.
• The reduction from $n>2$ to two agents ("having the other agents be much slower") is not a separate milestone; the goal covers every $n\ge2$.
• Running time ("polynomial-time computable") is out of scope and not modelled.

Contributions of any of the milestones are welcome, as are alternative proofs of the goal that avoid the terse odd case.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (revelation principle, p. 871).
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Why a reserve price, and why it does not matter which auction

Airlines selling last seats, Priceline's name-your-own-price, procurement of supply contracts: Chapter 6 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) treats auctions as pricing mechanisms and asks what revenue they earn and how to design them. Its centre is Myerson's (1981) theory for independent private values: whatever the mechanism, so long as bidders with higher valuations are more likely to win and the lowest type gains nothing, the firm's expected revenue is the expected virtual value $\sum_i J(v_i) y_i(v)$ of the winners, with $J(v) = v - (1 - F(v))/f(v)$ (Theorem 6.1, the revenue equivalence theorem). Maximizing that expression pointwise gives the optimal auction: the standard first- or second-price auction with a reserve price $v^*$ at the zero of $J$ (Theorem 6.2). This mission formalizes the second-price form of Theorem 6.2 as its goal, with the dominant-strategy and first-price equilibria of the informal analysis, Theorem 6.1, the optimal allocation and Proposition 6.1 on list prices as supporting results.

Setting

$N$ customers have i.i.d. valuations on $[0, \bar v]$ with a continuously differentiable, strictly increasing distribution $F$ and positive density $f$ (PrivateValues, IsRegular); the joint law is the product measure (joint). A direct-revelation mechanism (Mechanism) maps reported valuations to allocations $y_i(v) \in \{0, 1\}$, at most $C$ units in total, and payments $p_i(v)$. For a report $w$ by customer $i$, $P_i(w)$ is the win probability, $R_i(w)$ the expected payment and $S_i(w) = w P_i(w) - R_i(w)$ the surplus (winProb, expPayment, expSurplus); incentive compatibility, $S_i(w) \ge w P_i(w') - R_i(w')$, is the equilibrium condition of the direct mechanism (IsIncentiveCompatible). The chapter's mechanisms are the $C$-unit second-price auction with reserve price $r$ (secondPriceReserve: the $C$ highest valuations above $r$ win and pay the larger of $r$ and the highest losing valuation), the list-price mechanism for $N \le C$ (listPrice), and the single-unit first-price auction with its equilibrium bid $b^*(v) = v - \int_0^v P(s)\,ds / P(v)$, $P = F^{N-1}$ (firstPriceBid).

Formalization targets

Goal: Theorem 6.2

With $J$ strictly increasing (Assumption 7.2) and $v^*$ its zero, the $C$-unit second-price auction with reserve price $v^*$ is a feasible, incentive-compatible mechanism with monotone allocations and zero surplus at zero, and its expected revenue is at least that of every such mechanism: reserve_price_auction_optimal.

Supporting targets

Bidding one's valuation is dominant in the second-price auction (Sect. 6.2.2.1); the bid (6.4) solves the first-order condition (6.3), is a symmetric equilibrium of the first-price auction and shades below the valuation (Sect. 6.2.2.2); Theorem 6.1, revenue equals expected virtual surplus and each expected payment is $w P_i(w) - \int_0^w P_i$; the pointwise optimal allocation of Sect. 6.2.5; and Proposition 6.1, a list price at $v^*$ is optimal when $N \le C$.

Proposition 6.2 (asymptotic optimality of list prices, a law-of-large-numbers statement about scaled auctions), the first-price form of Theorem 6.2 with its equilibrium (6.9) stated without proof, and the dynamic, replenishment and network auctions of Sects. 6.3-6.5 (Propositions 6.3-6.11, from Vulcano, van Ryzin and Maglaras and from Cooper and Menich) are not targets of this mission.

Significance

Theorem 6.1 is the tool that lets revenue be computed from allocations alone, which is why the first- and second-price auctions of Examples 6.1-6.3 earn the same $(N-1)/(N+1)$ and why any dynamic pricing scheme that ends with the same winners earns the same as the optimal auction (Sect. 6.2.6.3). Theorem 6.2 says a firm with private-value customers cannot do better than a standard auction with the right reserve price, and Proposition 6.1 that with enough capacity a list price already does it: auctions are a small-numbers phenomenon. These are the foundations on which the chapter's dynamic auctions and the list-price comparisons of Sects. 6.3-6.4 rest, and Myerson's optimal auction has no machine-checked proof in its multi-unit form.

Difficulty

Theorem 6.1 is an envelope argument in measure-theoretic clothing: incentive compatibility gives the two-sided inequalities of Appendix 6.A, monotonicity of $P_i$ makes $S_i$ convex with derivative $P_i$ almost everywhere, so $S_i(w) = \int_0^w P_i$, and then an integration by parts against the density converts $\int (w P_i(w) - S_i(w)) f(w)\,dw$ into $\int J(w) P_i(w) f(w)\,dw$; the win probabilities are integrals over a product measure with one coordinate replaced, and Fubini is needed to return to $\mathbb E[J(v_i) y_i(v)]$. The goal then needs the reserve-price auction shown incentive compatible (a dominant-strategy argument on the threshold payment), measurable, monotone and with zero surplus at zero, and the pointwise optimal allocation integrated. The first-price item is calculus on an interval integral with a vanishing denominator at $0$ and a monotone comparative-statics argument for the equilibrium inequality.

Formalization scope

Mechanisms are direct-revelation mechanisms on $[0, \bar v]^N$, as the book reduces to in Sect. 6.2.3.1; expectations over the other customers are integrals over the joint law with customer $i$'s coordinate overwritten by the report. Payments are assumed bounded on reports in $[0, \bar v]^N$ (not on all of $\mathbb R^N$, where the second-price payment is unbounded) and the rules measurable. Ties in the second-price auction are broken by index, a null event, and when every customer wins the losing supremum is $0$ so the winner pays the reserve. Theorem 6.2 is stated for the second-price auction; the first-price version with reserve price, whose equilibrium (6.9) the book asserts without proof, is left out and noted. Optimality is over mechanisms satisfying conditions (i) and (ii) of Theorem 6.1 and incentive compatibility, which is the class the book compares against. The virtual value's zero $v^*$ is a parameter with $J(v^*) = 0$ rather than the maximum of (6.8), which under strict monotonicity is the same point.

Selected references

• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Kluwer/Springer, 2004, Chapter 6. https://doi.org/10.1007/b139000
• R. B. Myerson, Optimal auction design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• J. G. Riley and W. F. Samuelson, Optimal auctions, American Economic Review 71(3), 1981. https://www.jstor.org/stable/1802786
• P. Klemperer, Auction theory: a guide to the literature, Journal of Economic Surveys 13(3), 1999. https://doi.org/10.1111/1467-6419.00083
• 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
• E. Maskin and J. Riley, Optimal multi-unit auctions, in The Economics of Missing Markets, Information, and Games, Oxford University Press, 1989.

Algorithmic Game Theory V: Stable Matching and Trading without Money

Motivation

When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.

Setting

Marriage market (§10.4): finite sets $M$ of men and $W$ of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; $P\,i\,a\,b$ reads "$i$ strictly prefers $a$ to $b$"). Following the book's dummy-partner convention, $|M| = |W|$ and a matching is a bijection $\mu : M \simeq W$. A pair $(m, w)$ blocks $\mu$ if each prefers the other to their assigned partner; $\mu$ is stable if no pair blocks it. A stable $\mu$ is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates $\mu$ if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.

Housing market (§10.3): a finite set $N$ of agents, agent $i$ owning house $i$, each with a strict preference over all houses; an allocation is a permutation of $N$. A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.

Formalization targets

Goal (capstone) — Theorem 10.13

Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.

Theorem 10.10 — existence

Every marriage market has a stable matching.

Theorem 10.11 / Gale–Shapley 1962 — male-optimality

Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.

Theorem 10.12 — the core

A matching is stable iff it is in the core of the matching game.

Theorems 10.6 and 10.7 — housing

The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.

Significance

These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.

Difficulty

Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.

Formalization scope

Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's $|M| = |W|$ convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.

Selected references

• D. Gale, L. S. Shapley, College admissions and the stability of marriage, Amer. Math. Monthly 69 (1962), 9–15. DOI
• L. Shapley, H. Scarf, On cores and indivisibility, J. Math. Econ. 1 (1974), 23–37. DOI
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley algorithm, Amer. Math. Monthly 88 (1981), 485–494. DOI
• A. E. Roth, The economics of matching: stability and incentives, Math. Oper. Res. 7 (1982), 617–628. DOI
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Econ. Letters 9 (1982), 127–132. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 10. DOI

Motivation

Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — quasilinear utilities and payments — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Nisan, is the source text.

Setting

A set $A$ of alternatives and a finite set $\iota$ of players. Player $i$ holds a private valuation $v_i : A \to \mathbb{R}$ from a publicly known domain $V_i \subseteq \mathbb{R}^A$; utilities are quasilinear: choosing $a$ and charging $p_i$ gives $i$ utility $v_i(a) - p_i$. A (direct revelation) mechanism is a social choice function $f$ from valuation profiles to $A$ together with payment functions $p_i$ (Definition 9.14). The mechanism is incentive compatible if no unilateral misreport from the domain ever beats the truth (Definition 9.15).

A VCG mechanism (Definition 9.16) has $f$ maximizing social welfare $\sum_i v_i(a)$ and payments of the Groves form $p_i = h_i(v_{-i}) - \sum_{j\ne i} v_j(f(v))$; the Clarke pivot rule takes $h_i(v_{-i}) = \max_b \sum_{j \ne i} v_j(b)$. A rule is weakly monotone (Definition 9.28) if a unilateral change of valuation that moves the outcome from $a$ to $b$ satisfies $v_i'(b) - v_i'(a) \ge v_i(b) - v_i(a)$. A single-parameter domain (Definition 9.33) is given by a win set $W_i \subseteq A$ per player and bids $t \in [t_0, t_1]$: the valuation is $t$ on $W_i$ and $0$ elsewhere.

Formalization targets

Goal (capstone) — Theorem 9.36

A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible iff the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.

Theorem 9.17 — VCG is truthful

Every VCG mechanism is incentive compatible.

Lemma 9.20 — Clarke pivot

With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.

Theorem 9.29 — weak monotonicity

Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).

Significance

These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.

The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.

Difficulty

Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment c that is a least upper bound of the losing bids whenever losing bids exist — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.

Formalization scope

Valuations are functions A → ℝ; domains are sets V i : Set (A → ℝ); mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term hᵢ is a function of the full profile constrained to be invariant under changes of coordinate i — the standard rendering of "depends only on $v_{-i}$". The Clarke payment uses a Finset.sup' over a finite nonempty A, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is Set.indicator, bids live in Set.Icc t0 t1 with t0 ≤ t1, and the critical value is characterized by IsLUB guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk sSup. Weak monotonicity's sufficiency half carries Convex ℝ (V i) and finite A (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.

Selected references

• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, J. Finance 16 (1961), 8–37. DOI
• E. H. Clarke, Multipart pricing of public goods, Public Choice 11 (1971), 17–33. DOI
• T. Groves, Incentives in teams, Econometrica 41 (1973), 617–631. DOI
• M. Saks, L. Yu, Weak monotonicity suffices for truthfulness on convex domains, Proc. 6th ACM EC (2005), 286–293. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §§9.3, 9.5. DOI

A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue $Rev(v_S)$ is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective $\varpi(x)=N\,E[x(\mu)(\mu-\varphi(\mu))]$ — is profit-optimal up to a $1+O(N^{-1/3})$ factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap $|Rev(v)-E[v]|$ (Lemma 4.5).