Algorithmic Game Theory

Motivation

Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".

Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.

Setting

A Bayesian routing game has a finite set of populations $\mathcal I$, one per TIS, a finite set of network states $\mathcal S$, and for each population $i$ a finite nonempty type space $\mathcal T^i$ of signals. A common prior $\pi$ is a probability distribution on $\mathcal S\times\mathcal T$, $\mathcal T=\prod_i\mathcal T^i$. A network with a single origin–destination pair has edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$; each edge has a state-dependent cost $c^s_e$ that is positive, strictly increasing and differentiable. The total demand is $D>0$, and population $i$ carries the fraction $\lambda^i$ of it, with $\lambda^i\ge0$ and $\sum_i\lambda^i=1$.

A strategy profile $q$ assigns to each population $i$ and type $t^i$ a split $q^i_r(t^i)\ge0$ of its demand $\lambda^iD$ over routes. It induces the route flow $f_r(t)=\sum_iq^i_r(t^i)$ and the edge load $w_e(t)=\sum_{r\ni e}f_r(t)$. With the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$, type $t^i$ evaluates route $r$ by its expected cost $\mathbb E[c_r(q)\mid t^i]$. A Bayesian Wardrop equilibrium (BWE) is a feasible $q$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is $C^{i*}(\lambda)=\sum_{t^i}\Pr(t^i)\min_r\mathbb E[c_r(q)\mid t^i]$ at a BWE $q$.

The game has a weighted potential $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$; its minimum over feasible profiles is the equilibrium potential value $\Psi(\lambda)$. For two populations $i\ne j$, the direction $z^{ij}$ moves demand share from $j$ to $i$, and $|\lambda^{-ij}|$ is the total share of the other populations. The impact of information $\widehat J^i(f)$ measures how much of population $i$'s demand is moved by its signal. Two thresholds $\underline\lambda^i\le\overline\lambda^i$ are computed from the optimal set $\mathcal F^{ij,\dagger}$ of an auxiliary convex program over route flows in which the separate information constraints of $i$ and $j$ are merged. They define three regimes: $\Lambda^{ij}_1$ ($\lambda^i<\underline\lambda^i$), $\Lambda^{ij}_2$ ($\underline\lambda^i\le\lambda^i\le\overline\lambda^i$) and $\Lambda^{ij}_3$ ($\lambda^i>\overline\lambda^i$). The relative value of information is $V^{ij*}(\lambda)=C^{j*}(\lambda)-C^{i*}(\lambda)$.

Formalization targets

Goal: Theorem 3

For $i\ne j$ and admissible $\lambda$ (in the simplex with $\lambda^i,\lambda^j>0$), and every BWE of $\Gamma(\lambda)$,

$$V^{ij*}(\lambda)>0 \text{ on } \Lambda^{ij}_1,\qquad V^{ij*}(\lambda)=0 \text{ on } \Lambda^{ij}_2,\qquad V^{ij*}(\lambda)<0 \text{ on } \Lambda^{ij}_3,$$

and $V^{ij*}$ is nonincreasing along $z^{ij}$: $V^{ij*}(\lambda+\varepsilon z^{ij})\le V^{ij*}(\lambda)$ for $\varepsilon>0$ with both endpoints admissible.

Milestones

The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of $\Phi$; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope $\mathcal F(\lambda)$), Proposition 2 (equilibrium route flows minimize $\widehat\Phi$ over $\mathcal F(\lambda)$), Lemma 4 ($0\le\underline\lambda^i\le\overline\lambda^i\le1-|\lambda^{-ij}|$), Theorem 2 (equilibrium flows in each regime), Proposition 3 ($\Psi$ decreases, stays constant, increases along $z^{ij}$ in the three regimes) and Lemma 5 ($\Psi$ is convex and directionally differentiable, and $V^{ij*}(\lambda)=-\frac1D\nabla_{z^{ij}}\Psi(\lambda)$).

Significance

Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate $\lambda^i$. The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.

The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.

Difficulty

The equilibrium strategy profile is not unique and changes discontinuously with $\lambda$. Differentiating equilibrium costs in $\lambda$ directly therefore fails. The paper instead works with the optimal value $\Psi(\lambda)$, whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint $\widehat J^i(f)\le\lambda^iD$, a minimum over types inside a sum over routes. Strict monotonicity of $\Psi$ in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.

Formalization scope

The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, $D>0$, and costs are positive on nonnegative loads, strictly increasing and differentiable on $\mathbb R$. One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.

Conventions: $C^{i*}$ is the last form of eq. (7), which does not divide by $\lambda^iD$. $\widehat J^i$ is the maximum of eq. (16) over the reference profile, so that $\widehat J^i(f)\le\lambda^iD$ is exactly (14d). $\Psi$ and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.

Disclosed deviations: Lemma 2's $C^2$ clause assumes $C^1$ costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes $\lambda^j>0$; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.

Selected references

• M. Wu, S. Amin, A. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999
• W. H. Sandholm, Potential Games with Continuous Player Sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
• R. T. Rockafellar, Directional Differentiability of the Optimal Value Function in a Nonlinear Programming Problem, in Sensitivity, Stability and Parametric Analysis (Mathematical Programming Studies 21), Springer, 1984, pp. 213–226.
• A. V. Fiacco, J. Kyparisis, Convexity and Concavity Properties of the Optimal Value Function in Parametric Nonlinear Programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986.

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

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j, \qquad g(x,\tilde t) = \max_i \sum_{j\in x^i} \tilde t_j .$$

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

$$p^i(d,\tilde t) = \underbrace{\sum_{j \in x^i(d)} \tilde t_j}_{\text{compensation } c^i} \;\underbrace{-\, g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big)}_{\text{bonus } b^i},$$

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:

$$\text{strongly truthful} \quad\text{and}\quad g\big(x(D), \tilde t\big) \le \min_y g(y, t) \text{ whenever every agent plays a dominant strategy for its true type.}$$

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$,

$$-g\big(x(t), \mathrm{corr}^*(x(t), t)\big) \ge -g\big(x(t'^i, d^{-i}), \mathrm{corr}^*(x(t'^i, d^{-i}), t)\big).$$

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

Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.

The paper's test case is task scheduling on unrelated machines: $k$ tasks must be assigned to $n$ agents, agent $i$ needs time $t^i_j$ for task $j$, and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio $n$, and no mechanism achieves a ratio below $2$ (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio $7/4 < 2$.

Timeline.

• 1979: Roberts characterizes weighted (affine) maximizers; the weighted Vickrey–Groves–Clarke (VGC) mechanisms are truthful.
• 1999: Lehmann supplies the case analysis that improves the authors' original bound of $1.823$ to $7/4$ (acknowledged on p. 182).
• 2001: Nisan and Ronen publish the randomly biased min work mechanism and Theorem 4.16.

Setting

There are two agents, $1$ and $2$, and $k$ tasks. A type vector $t = (t^1, t^2)$ gives, for each agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$. The make-span of $x$ is

$$g(x, t) = \max_{i \in \{1,2\}} \sum_{j \in x^i} t^i_j .$$

A direct mechanism receives declared types $d$ and returns an allocation $x(d)$ and payments $p^i(d)$ handed to the agents. Agent $i$ with true type $t^i$ gets utility $p^i(d) - \sum_{j \in x^i(d)} t^i_j$. The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.

A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.

The biased min work mechanism with parameters $\beta \ge 1$ and $s \in \{1,2\}^k$ treats each task $j$ separately. With $i = s_j$ the favoured agent and $i' = 3 - i$ the other: if $t^i_j \le \beta \cdot t^{i'}_j$, task $j$ goes to $i$, who is paid $\beta \cdot t^{i'}_j$; otherwise it goes to $i'$, who is paid $\beta^{-1} \cdot t^i_j$. The randomly biased min work mechanism draws $s$ uniformly from $\{1,2\}^k$ and uses $\beta = 4/3$. Its expected make-span is

$$\mathbb{E}_s\, g(x_s(t), t) = \frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t).$$

Formalization targets

Goal: Theorem 4.16

For every $k$: the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector $t$ and every allocation $y$,

$$\frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t) \le \frac74\, g(y, t).$$

Milestones

• Theorem 3.2 (Roberts): for positive weights $\beta^i$, a mechanism whose output maximizes $\sum_i \beta^i v^i(t^i, o)$ and whose payments are $p^i = \frac{1}{\beta^i}\sum_{j \ne i}\beta^j v^j(t^j, o) + h^i(t^{-i})$ is truthful.
• Lemma 4.15: for every $\beta \ge 1$ and every $s$, the biased min work mechanism is strongly truthful.
• Lemma 4.17: the randomly biased min work mechanism is universally strongly truthful.
• Claim 4.19, part 5: allocating two tasks independently at random gives an expected make-span no larger than allocating their merge at random.
• Reduced case (Fig. 2, Cases 1–3): for $a, b, c, d \ge 0$ with $a + c = \frac43 b + d$,

$$\tfrac14\Big(\max(a+b+c+\tfrac43 d, 0) + \max(a+b+c, d) + \max(a+b+\tfrac43 d, \tfrac43 c) + \max(a+b, \tfrac43 c + d)\Big) \le \tfrac74 (a+c).$$

• Lemma 4.18: the $7/4$ bound on the expected make-span.

Significance

The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: $7/4$ against the deterministic lower bound of $2$. The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.

Difficulty

Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over $2^k$ coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to $\beta$" by $\beta$, and under the mechanism's tie rule a task with ratio exactly $\beta$ is allocated by the coin rather than to the efficient agent.

Formalization scope

• Agents are Fin 2 (agent $1$ is 0, agent $2$ is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every $k$, including $k = 0$.
• Types are positive: every truthfulness quantifier ranges over positive declarations, true types and misreports, and the approximation bound is stated on positive type vectors. The reduced-case and merging milestones are pure real inequalities with nonnegative times, since the paper represents missing tasks by zero times.
• Payments are handed to the agent; utility is quasi-linear.
• The make-span is a finite maximum (Finset.sup') over the two agents. The expected make-span is the average over all $2^k$ vectors $s$, which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.
• Universal (strong) truthfulness quantifies over all $s \in \{1,2\}^k$, the support of the uniform distribution. Truthfulness in expectation over $s$ is weaker and is not the notion stated.
• The tie rule of Fig. 1 ($\le$: ties go to the favoured agent) is kept.
• The goal fixes $\beta = 4/3$; only Lemma 4.15 is stated for every $\beta \ge 1$. The ratio is compared with every allocation $y$, not with one fixed allocation, and the average is over all $s$, not the best $s$.
• Roberts' theorem is stated for arbitrary output sets, type sets and valuations, with positive weights.
• "Polynomial time computable" in Theorem 4.16 is not formalized; running time is out of scope.
• Claim 4.19 (the reduction to the four-task case) is not a separate item beyond its part 5, because its parts are instance transformations with a limiting step, not a single statement; a solver may formalize the reduction in any form that proves Lemma 4.18.

Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.

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
• K. Roberts, The characterization of implementable choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–349.
• T. Groves, Incentives in teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085

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):

$$p^i(X, t^{-i}) = \begin{cases} p^i(t'^i, t^{-i}) & \text{if some } t'^i \text{ gives } x^i(t'^i, t^{-i}) = X, \\ 0 & \text{otherwise.} \end{cases}$$

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:

$$\forall (x, p) \text{ truthful and local},\ \forall c < n:\quad \exists\, t,\ y \quad g(x(t), t) > c \cdot g(y, t).$$

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

$$g(x,t) = \max_{i} t^i(x^i),$$

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:

$$\forall\, (A, o, p):\quad \neg\ \mathrm{Implements}(o,p,c).$$

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.

Motivation

Fictitious play is the oldest model of learning in games: players repeatedly play a fixed normal form game, and each round every player best-responds to the empirical frequencies of the opponents' past play. Brown (1951) proposed it as an algorithm for computing the value of a zero-sum game, and Robinson (1951) proved that the empirical frequencies converge to the set of equilibria in that case. In stochastic fictitious play (Fudenberg and Kreps 1993) each player's payoffs are perturbed by fresh random shocks before every choice. The shocks make best responses single-valued and smooth in beliefs, which puts the process within reach of stochastic approximation theory: its long-run behaviour is governed by a deterministic perturbed best response dynamic.

Before Hofbauer and Sandholm (2002), convergence of stochastic fictitious play was known only for 2×2 games (Fudenberg and Kreps 1993; Kaniovski and Young 1995) and for certain games with two strategies per player (Benaïm and Hirsch 1999). The difficulty was the perturbed dynamic itself, whose vector field involves choice probabilities with no closed form for general noise distributions. Hofbauer and Sandholm showed that every such dynamic can be rewritten with a deterministic payoff perturbation (their Theorem 2.1), and used that to carry Lyapunov functions over to arbitrary noise distributions. This mission covers the first two classes of games in their main convergence theorem: symmetric games with an interior evolutionarily stable strategy, and two player zero-sum games.

Setting

A two player normal form game has strategy sets $S^1 = \{1,\dots,n^1\}$ and $S^2 = \{1,\dots,n^2\}$ and utilities $u^\alpha : S^1 \times S^2 \to \mathbb R$. Player $\alpha$'s mixed strategies form the simplex $\Delta S^\alpha$, and $\Sigma = \Delta S^1 \times \Delta S^2$. The payoff vector $U^\alpha(x^{-\alpha}) \in \mathbb R^{n^\alpha}$ lists the expected payoff of each pure strategy of $\alpha$ against the opponent's mixed strategy. The game is zero-sum if $u^1(s) = -u^2(s)$ for every profile $s$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function $C^\alpha(\pi)_i = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$, for $\varepsilon$ with density $f^\alpha$, gives the perturbed best response $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$. The densities are required to be strictly positive with continuously differentiable choice functions ("the conditions of Theorem 2.1").

Standard stochastic fictitious play. Pure strategies are identified with basis vectors $e_i$. Choices $\zeta_1$ are arbitrary. At every time $t \ge 1$ each player $\alpha$ draws a shock $\varepsilon^\alpha_t$ with density $f^\alpha$ and plays at time $t+1$ the pure strategy maximizing $U^\alpha_k(Z^{-\alpha}_t) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t \sum_{u=1}^t \zeta_u \in \Sigma .$$

The shocks are independent over time and across players. The expected motion of $Z_t$ is the perturbed best response dynamic

$$\text{(P)}\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha \quad\text{on } \Sigma .$$

Symmetric games. A two player game is symmetric if $S^1 = S^2 = \{1,\dots,m\}$ and $u^1(i,j) = u^2(j,i)$; it is described by the matrix $A_{ij} = u^1(i,j)$, and $U^1(z) = Az$. In symmetric stochastic fictitious play two players in roles 1 and 2 play at every time, their shocks are independent and identically distributed with one density $f$, and the state is the average of all past plays in both roles,

$$\hat Z_t = \frac1{2t}\sum_{u=1}^t \big(\hat\zeta^1_u + \hat\zeta^2_u\big) \in \Delta S^1 .$$

Its mean dynamic is $\text{(SP)}\ \dot x = C(Ax) - x$ on $\Delta S^1$. A mixed strategy $x^*$ in the interior of $\Delta S^1$ is an interior evolutionarily stable strategy (ESS) if $x^*\cdot Ax > x\cdot Ax$ for all mixed $x \ne x^*$ near $x^*$.

Rest points and chain recurrence. For a dynamic $\dot x = F(x)$ on a compact set $X$, the rest points are the zeros of $F$ in $X$. A point $x$ is chain recurrent if for every $\varepsilon > 0$ one can return from $x$ to $x$ by following solution segments of length at least $1$, with jumps of size less than $\varepsilon$ between segments.

Formalization targets

Goal: Theorem 6.1 (i) and (ii)

(i) If $A$ has an interior ESS, then (SP) has a unique rest point $\hat x$ and

$$P\Big(\lim_{t\to\infty} \hat Z_t = \hat x\Big) = 1 .$$

(ii) If the two player game is zero-sum, then (P) has a unique rest point $x^*$ and

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1 .$$

Both hold for all shock densities meeting the conditions of Theorem 2.1, all probability spaces carrying the shocks, and all initial choices.

Milestones

1. Theorem 2.1: for such a density, the choice function $C$ is the unique maximizer $C(\pi) = \operatorname{argmax}_{y \in \operatorname{int}\Delta}(y\cdot\pi - V(y))$ for one admissible deterministic perturbation $V$.
2. With an interior ESS, $\hat\Lambda(x) = x\cdot Ax - V(x) - W(Ax)$, where $W(\pi) = \max_y (y\cdot\pi - V(y))$, is strictly concave and a strict Lyapunov function for the deterministically perturbed dynamic (SPV).
3. Its maximizer is the unique chain recurrent point of (SPV).
4. In zero-sum games, $\Lambda(x^1,x^2) = -V^1(x^1) - W^1(U^1(x^2)) - V^2(x^2) - W^2(U^2(x^1))$ is strictly concave and a strict Lyapunov function for (PV).
5. Its maximizer is the unique chain recurrent point of (P).
6. The maximizer of $\hat\Lambda$ is the unique chain recurrent point of (SP).

Significance

The theorem gives global, almost sure convergence of a learning process for arbitrary noise distributions, not only for the logit (Gumbel) noise under which the perturbed dynamic has a closed form. For zero-sum games it is the stochastic counterpart of Robinson's theorem. For symmetric games with an interior ESS it shows that a population learning by stochastic fictitious play settles at a single mixed state. Since the choice functions are continuous, the players' choice probabilities converge as well. The limit is the rest point of the perturbed dynamic, which approximates a Nash equilibrium (in case (i), the ESS) as the noise vanishes.

On the formal side, the paper's results are proved, but no part of them is machine-checked, and the platform has no model of learning in games, of chain recurrence, or of stochastic approximation. The mission produces a formal model of stochastic fictitious play as a random process, formal statements of the Hofbauer and Hofbauer–Hopkins Lyapunov functions, and the chain recurrence characterizations that connect them to the process.

Difficulty

The obvious route replaces the process $Z_t$ by the ODE (P) and argues that (P) converges. That step is where the argument is incomplete: convergence of every solution of (P) does not give convergence of the stochastic process, because a stochastic approximation can in principle circulate near a set of orbits the ODE never follows. The right invariant is the chain recurrent set, and the limit sets of the process lie in a connected component of it (Benaïm and Hirsch 1999; Benaïm 1999). The characterization therefore has to be of chain recurrence, which is strictly weaker than asymptotic stability of individual orbits.

The second obstacle is that (P) itself is defined through the noise distribution and admits no useful Lyapunov function in general. The Lyapunov functions exist for the deterministic form (PV)/(SPV), and moving between the two forms requires the representation of Theorem 2.1, whose perturbation $V$ has no closed form either.

Formalization scope

Players and strategies are indexed from $0$. Mixed profiles live in $\prod_\alpha \mathbb R^{n^\alpha}$ and every vector field is defined on that ambient space. The processes are defined pathwise from a family of shock vectors on an arbitrary probability space. Ties in the argmax are broken by the smallest index, an event of probability zero because the shocks have densities. The shock drawn at time $t$ produces the choice at time $t+1$. Shock densities are arbitrary strictly positive densities with continuously differentiable choice functions; no noise law is fixed, and the two players' densities in (ii) may differ. Independence is joint over times and players (and roles in (i)). The symmetric process has its own state in one simplex and is not the standard process applied to a symmetric game.

Deterministic perturbations are functions defined on the whole space whose values off the open simplex are ignored; derivatives are taken of their composition with the projection onto the affine plane $\{\sum_i y_i = 1\}$. Perturbed best responses in (PV) and (SPV) are supplied as maps together with the hypothesis that they are the unique maximizers. A strict Lyapunov function must increase strictly along every non-constant solution on $(0,\infty)$. The ESS definition includes $x \ne x^*$, which the source omits.

The conclusions assert existence and uniqueness of the rest point; they are not hypotheses. A statement for the ODE (P) in place of the process $Z_t$, for one fixed noise law, or with the ESS as the limit point would be a different theorem.

A complete development needs Theorem 2.1 (convex duality and the Legendre transform on the simplex), existence and uniqueness of solutions of (P), basic chain recurrence theory, and the stochastic approximation results of Benaïm and Hirsch, which are not restated here and are welcome as independent contributions. The model layer (games, payoff vectors, choice functions, stochastic fictitious play) is shared with the other missions of this series.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• Y. M. Kaniovski and H. P. Young, Learning Dynamics in Games with Stochastic Perturbations, Games and Economic Behavior 11, 330–363, 1995. https://doi.org/10.1006/game.1995.1054
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54, 296–301, 1951. https://doi.org/10.2307/1969530
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

$$\sum_p |\rho(p,j,t)-p_j|\,\frac{N(p,t)}{t}\ \longrightarrow\ 0 \qquad (t\to\infty).$$

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982), 605–610. https://doi.org/10.1080/01621459.1982.10477856
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153