Algorithmic Game Theory

Motivation

A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.

Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.

Setting

Let $N=\{1,\dots,n\}$ be a finite set of players. A game is a function $v$ from subsets of $N$ to the reals with $v(\emptyset)=0$. It is convex if

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

A payoff vector is $a\in\mathbb R^N$, and $a(S)=\sum_{i\in S}a_i$. It is feasible if $a(N)\le v(N)$. The core $C$ is the set of feasible $a$ with $a(S)\ge v(S)$ for every $S\subseteq N$; in particular $a(N)=v(N)$ on $C$.

For a nonempty coalition $S$, the face $C_S$ is the set of core points with $a(S)=v(S)$; by convention $C_\emptyset=C$, and $C_N=C$. The family $\{C_S\}$ is the core configuration. It is complete if no $C_S$ is empty, and regular if $C_N\ne\emptyset$ and

$$C_S\cap C_T\subseteq C_{S\cup T}\cap C_{S\cap T}\qquad\text{for all } S,T\subseteq N.$$

For an ordering $\omega$ of the players, $S_{\omega,k}$ is the set of the first $k$ players, and the marginal vector $a^\omega$ pays each player $i$ its marginal contribution $v(S_{\omega,\omega(i)})-v(S_{\omega,\omega(i)-1})$.

A payoff vector $b$ is dominated by $a$ if some nonempty coalition $S$ has $a(S)\le v(S)$ and $a_i>b_i$ for all $i\in S$. A set $V$ of feasible vectors is stable if every feasible vector is either a member of $V$ or dominated by a member of $V$, but not both.

Formalization targets

Goal: Theorem 8

$$C \text{ is stable, and every stable set } V \text{ equals } C \qquad (v \text{ convex}).$$

The goal contains both halves of the page's statement: stability of the core, and uniqueness ("the unique von Neumann–Morgenstern solution").

Milestones, in the order the argument uses them

• Lemma 1 (p. 18) and Lemma 2 (p. 19): for a regular configuration, a point on two nested faces $C_S\cap C_T$ with $|T\setminus S|\ge2$ can be moved to a face $C_Q$ of an intermediate coalition, and a point of $C_S$ to $C_S\cap C_{S\cup\{j\}}$, keeping its coordinates on $S$.
• Theorem 2 (p. 18): in a regular configuration $C_{S_1}\cap\cdots\cap C_{S_m}\ne\emptyset$ for every strictly increasing chain $S_1\subset\cdots\subset S_m$; in particular a regular configuration is complete.
• Theorem 4 (p. 21): the core of a convex game is nonempty.
• Theorem 5 (p. 22): a game is convex if and only if its core configuration is regular.
• Two claims of §4.3 (p. 24): every stable set contains the core, and no stable set properly includes another.
• The claim that opens the proof of Theorem 8 (p. 24): in a convex game every feasible vector outside the core is dominated by a core point.

The mission also states Theorem 3 (p. 19), the vertices of a regular core are exactly the marginal vectors $a^\omega$, as a further item that is not on the path to the goal.

Significance

The result. Theorem 8 gives, for a natural and widely occurring class of games, a complete answer to the existence and uniqueness questions for von Neumann–Morgenstern solutions, which are open or negative in general. Theorems 3 and 5 describe the core of a convex game explicitly as the polytope spanned by the $n!$ marginal vectors, the combinatorial description that underlies later work on the Shapley value, the Weber set, and the polymatroid greedy algorithm. Theorem 5 is the geometric characterization of supermodularity through the face structure of the core.

Formalizing it. All results in this mission are proved in the paper; none has a machine-checked proof on the platform. Theorem 4 is already stated on the platform (as part of a statement that also puts every marginal vector and the Shapley value in the core) and enters the mission as an existing item. The remaining work is a formal development of face configurations of the core, of stable sets and domination, and of the passage from supermodularity to the geometry of the core. The definitions of stable set and domination are general and reusable for any transferable-utility game.

Difficulty

The internal half of stability is immediate from the definitions: a core point cannot be dominated by any vector satisfying a coalition constraint $a(S)\le v(S)$. Uniqueness also follows from two short observations. The substance is external stability: every feasible vector outside the core must be dominated by a core point, and the dominating vector has to be produced explicitly. The obvious attempt, raising the payoffs of one violated coalition and leaving the other coordinates of $b$ unchanged, does not in general produce a core point, and nothing in the definition of the core alone controls how the core meets the hyperplane of a given coalition; that control is what the face theory of §3 is about. For non-convex games the external half genuinely fails, so no argument that ignores convexity can succeed.

Formalization scope

Players are Fin n (a relabelling of the paper's finite set $N$), a game is f : Finset (Fin n) → ℝ, payoff vectors are Fin n → ℝ, and $a(S)$ is ∑ i ∈ S, a i. The existing platform definitions Supermodularity.Cooperative.IsConvexGame ($v(\emptyset)=0$ plus supermodularity on all subsets), Core, InitialCoalition and GreedyPayoff (the marginal vectors, orderings being permutations of Fin n) are reused; the reused Theorem 4 statement is Supermodularity.Cooperative.convex_game_core_and_shapley.

Conventions committed to:

• Wherever the page says "a game", the hypothesis is exactly $v(\emptyset)=0$; convexity is IsConvexGame.
• Faces satisfy $C_\emptyset=C$ literally: the tightness condition is imposed only for nonempty $S$.
• Regularity includes $C_N\ne\emptyset$, as on the page.
• Lemmas 1–2 and Theorems 2–3 assume a regular configuration, not convexity, as on the page.
• $S\subset\subset T$ is $S\subsetneq T$ with $|T|-|S|\ge2$; Lemma 1's two preassigned elements are distinct.
• An increasing sequence of $m\ge1$ coalitions is a strictly monotone map from Fin (m + 1).
• "Vertex" is Set.extremePoints ℝ.
• Domination requires a nonempty coalition and strict coordinate inequalities; stable sets consist of feasible vectors and the "either … or …, but not both" condition ranges over feasible vectors, following the page rather than the classical imputation-based variant.

A formalization in which the dominating coalition may be empty, in which regularity omits $C_N\ne\emptyset$, or in which the goal asserts stability without uniqueness does not state the paper's theorem and is ruled out.

Welcome contributions: proofs of the milestones in any order, general lemmas about faces of polytopes cut out by set-function inequalities, and reusable API for domination and stable sets.

Selected references

• L. S. Shapley, Cores of Convex Games, International Journal of Game Theory 1 (1971), 11–26. https://doi.org/10.1007/BF01753431
• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87. https://doi.org/10.1007/3-540-36478-1_2
• W. F. Lucas, A game with no solution, Bulletin of the American Mathematical Society 74 (1968), 237–239. https://doi.org/10.1090/S0002-9904-1968-12039-2
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998, §5.2.

Motivation

Fictitious play is the oldest model of learning in games: each player repeatedly best-responds to the empirical frequencies of the opponents' past play. Stochastic fictitious play adds random payoff disturbances before each choice, so that players choose smoothed ("perturbed") best responses. It is a standard model in economics and in the study of learning in games (Fudenberg and Levine, 1998), and its long-run behavior is described through a deterministic mean dynamic, the perturbed best response dynamic, using stochastic approximation theory (Benaïm and Hirsch, 1999).

Supermodular games model strategic complementarities: the gain from moving to a higher strategy increases when opponents move to higher strategies. They arise in coordination, oligopoly and macroeconomic models (Milgrom and Roberts, 1990; Vives, 1990). Hofbauer and Sandholm (Econometrica 2002) show that in such games stochastic fictitious play converges almost surely whenever its mean dynamic has a unique rest point. This mission formalizes that result and the chain of lemmas behind it (Section 5 and the Appendix of the paper).

Timeline. Benaïm and Hirsch (1999) observed that supermodular games with exactly two strategies per player yield strongly monotone perturbed best response dynamics. Hofbauer and Sandholm (2002) extended this to any number of strategies by introducing stochastic dominance coordinates, and proved Theorem 6.1(iv). Benaïm (2000) supplied the low-dimensional convergence theorem used for the dimension ≤ 2 clause.

Setting

A $p$ player normal form game gives player $\alpha$ an ordered finite strategy set $S^\alpha = \{0,\dots,n^\alpha - 1\}$ and a utility $u^\alpha$ on pure profiles. $\Sigma = \prod_\alpha \Delta S^\alpha$ is the set of mixed profiles, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\, s^\alpha = i} u^\alpha(s) \prod_{\beta \ne \alpha} x^\beta_{s^\beta}$.

The game is strictly supermodular if for all distinct players $\alpha \ne \beta$ and all profiles $s, \hat s$ with $s^\alpha > \hat s^\alpha$ and $s^{-\alpha} = \hat s^{-\alpha}$, the difference $u^\alpha(s) - u^\alpha(\hat s)$ is strictly increasing in $s^\beta = \hat s^\beta$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$, strictly positive, whose choice function $C^\alpha_i(\pi) = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$ is continuously differentiable. The perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$, and the perturbed best response dynamic is

$$(\mathrm P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

$RP(\mathrm P)$ is its set of rest points in $\Sigma$ and $CR(\mathrm P)$ its chain recurrent set.

In standard stochastic fictitious play the shocks $\varepsilon^\alpha_t$ have densities $f^\alpha$ and are independent over time and across players. From an arbitrary initial pure profile $\zeta_1$, each player at time $t+1$ plays the pure strategy maximizing $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where $Z_t = \frac1t \sum_{u \le t} \zeta_u$ is the vector of empirical frequencies.

The stochastic dominance coordinates are $(T^\alpha x^\alpha)_i = \sum_{j > i} x^\alpha_j \in \mathbb R^{n^\alpha - 1}$, the mass on strategies above $i$; $T x \le T y$ means each $y^\alpha$ stochastically dominates $x^\alpha$. In these coordinates (P) becomes a dynamic (T) on $T(\Sigma)$.

Formalization targets

Goal: Theorem 6.1(iv), unique rest point clause

For a strictly supermodular game with $p \ge 2$ players and shock densities as above, if $RP(\mathrm P) = \{x^*\}$ then

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

on every probability space, for every independent shock family with the given densities and every initial profile.

Milestones

• Lemma A.2, eq. (14), Lemma A.3 and eqs. (17)–(18): the order-theoretic and differential facts behind monotonicity.
• Theorem 5.1: $T^{-\alpha} y^{-\alpha} \ge T^{-\alpha} x^{-\alpha} \Rightarrow T^\alpha \tilde B^\alpha(y^{-\alpha}) \ge T^\alpha \tilde B^\alpha(x^{-\alpha})$.
• Theorem 5.2: there are rest points $\underline x, \bar x$ with $RP(\mathrm P) \subseteq [\underline x, \bar x]$.
• Proposition 5.3: (P) and (T) are linearly conjugate.
• Theorem 5.4: (T) is cooperative and irreducible.
• Corollary 5.5(i)–(ii): (P) is strongly monotone, and $CR(\mathrm P) \subseteq [\underline x, \bar x]$, so $CR(\mathrm P) = \{x^*\}$ when the rest point is unique.

Significance

The result gives global almost-sure convergence of a stochastic learning process in a broad class of games with many strategies, where earlier results needed two strategies per player or specific payoff structures. It also shows which properties of the choice function matter: only eqs. (17)–(18), not the symmetry of its derivative used for potential and zero-sum games.

The paper's proof is complete but relies on outside results: stochastic approximation (Benaïm–Hirsch 1999, Benaïm 1999), monotone dynamical systems (Smith 1995), and the inclusion of the chain recurrent set in the global attractor (Robinson 1995). None of these, nor the Hofbauer–Sandholm theorem itself, is formalized in any proof assistant as far as known. The mission produces a machine-checked version of the theorem and of the Section 5 monotonicity theory.

Difficulty

The monotonicity lemmas are finite-dimensional calculus and summation by parts. The substantial steps are elsewhere. Strong monotonicity of a cooperative irreducible system (Corollary 5.5(i)) is a theorem of monotone dynamical systems that Mathlib does not have, and it must hold on the closed, non-open state space $T(\Sigma)$. The step from the ODE to the random process needs the stochastic approximation theorem: the empirical frequencies are an asymptotic pseudotrajectory of (P), and their limit set is almost surely internally chain transitive. Knowing that $x^*$ is globally asymptotically stable for (P) does not by itself give almost-sure convergence of $Z_t$. The limit set of the random process must be related to the chain recurrent set of (P), which is where Corollary 5.5(ii) enters.

Formalization scope

Players are Fin p, strategies Fin (n α) (0-based, same order as the paper), with every $n^\alpha \ge 1$. Mixed profiles live in the ambient space $\prod_\alpha \mathbb R^{n^\alpha}$ with the sup norm. The fields of (P) and (T) are defined on the whole ambient space, so partial derivatives are ordinary Fréchet derivatives. Densities are $[0,\infty]$-valued. Solutions are forward solutions staying in the state space. The chain recurrent set quantifies over solutions, which are unique here because the fields are $C^1$. The process $Z_t$ is defined pathwise from the shocks, with ties in the argmax broken by the smallest index (a null event). Densities may differ across players.

A statement about the ODE (P), or about a single noise law such as logit, would be a different and much weaker theorem. The goal is about the random process $Z_t$, on every probability space carrying independent shocks with the given densities. Irreducibility and strong monotonicity additionally assume that two distinct players each have at least two strategies; when one player owns every stochastic dominance coordinate and has at least two of them, supermodularity holds vacuously while irreducibility fails.

A complete development needs: random utility choice functions and their derivatives; monotone and cooperative ODE theory on convex sets; the chain recurrent set and the global attractor; stochastic approximation for processes with step size $1/t$. The last three are reusable well beyond this mission. Contributions to any milestone, and general-purpose lemmas on cooperative systems or stochastic approximation, are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70 (2002), 2265–2294. https://doi.org/10.1111/1468-0262.00376 (formalized from the authors' manuscript of February 21, 2002)
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Repeated Games, Games and Economic Behavior 29 (1999), 36–72. https://doi.org/10.1006/game.1997.0636
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer (1999). https://doi.org/10.1007/BFb0096509
• M. Benaïm, Convergence with Probability One of Stochastic Approximation Algorithms Whose Average is Cooperative, Nonlinearity 13 (2000), 601–616. https://doi.org/10.1088/0951-7715/13/3/305
• H. L. Smith, Monotone Dynamical Systems, AMS Mathematical Surveys and Monographs 41 (1995). https://doi.org/10.1090/surv/041
• P. Milgrom and J. Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58 (1990), 1255–1277. https://doi.org/10.2307/2938316
• D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press (1998).

Motivation

Fake accounts (purchased followers, likes and engagement) are a large part of influencer marketing on social media, and platforms say they invest in detecting and removing them. Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game. An influencer of unknown quality buys fake followers to look popular, consumers decide whether to follow, an advertiser pays for the real followers it expects, and the platform, which takes a share of the advertising revenue, chooses how much antifake effort to spend. A practical question for regulators and platform designers follows: does a platform that maximizes profit have any reason to fight fake accounts? This mission formalizes the paper's answer for the purely profit-driven platform: it does not.

The model draws on the signaling literature, in particular the undefeated equilibrium refinement of Mailath, Okuno-Fujiwara and Postlewaite (1993), and is close to the welfare analysis of social-learning manipulation in Chen and Papanastasiou (Management Science 67(11), 2021).

Setting

An influencer is of type $H$ (probability $\rho\in(0,1)$) or $L$, with content quality $q_H>q_L>0$, and $E[q]=\rho q_H+(1-\rho)q_L$. A fraction $l\in(0,1)$ of consumers (social media literacy) are informed and know the type. The platform picks an effort $d\ge0$. With technology level $\tau\in[0,1)$ and base price $p_0$, a fake account costs $p_f=p_0+d/(1-\tau)$ (1), and following costs a consumer $c=c_0+c_1(1-\tau)d$ (2), with $c_0,c_1\ge0$.

Informed followers of a $t$-type number $n^t_{in}=l(1-c/q_t)$ (8). Uninformed consumers see the early follower count $n_2^t$ and follow in number $n^t_{un}=(1-l)(1-c/E[q\mid n_2^t])$ (9). The real followers are $n^t_{r,ia}=n^t_{in}+n^t_{un}$ (10). An uninformed advertiser expects $E[n_{r,ua}]=\Pr(H\mid n)n^H_{r,ia}+\Pr(L\mid n)n^L_{r,ia}$ (11). From the $t$-type's side, the advertiser pays for $E[n^t_r]=l\,n^t_{r,ia}+(1-l)E[n_{r,ua}]$ real followers (12). Under a pooling equilibrium both types show the same count and the posterior is $\rho$. Under a separating equilibrium (costly or natural) the posterior is $1$ at the $H$-type's count and $0$ at the $L$-type's.

With advertising revenue $\mu>0$ per real consumer and platform share $\lambda_p$, the platform's profit under equilibrium type $r$ is (6)

$$\pi^r_p(d)=\lambda_p\mu E[n_r]-\frac{\gamma}{2}d^2,\qquad \gamma>0,$$

where $E[n_r]$ averages (12) over the type. Two thresholds, $d_1=(1-\tau)(\eta_1-p_0)$ (13) and $d_2=(1-\tau)(\eta_2-p_0)$ (16), with $\eta_1=\lambda_i\mu(1-l)\big[q_H(E[q]-q_L)/(lE[q](q_H-q_L))+\rho\big]$ and $\eta_2=\frac1l\lambda_i\mu(1-l^2)$, select the equilibrium (Proposition 1). If $d_1>0$ and $d\le d_1$ the equilibrium is pooling. Otherwise it is costly separating for $d\le d_2$ and naturally separating beyond. The equilibrium profit is $\pi_p(d)=\pi^{r(d)}_p(d)$.

Formalization targets

Goal: Proposition 4(a)

$$\pi_p(d)\le\pi_p(0)\quad(d\ge0),\qquad \pi_p(d)<\pi_p(0)\quad(d>0).$$

A purely profit-driven platform ($w=0$ in the objective $\Pi_p=(1-w)\pi_p+wU$ of (3)) optimally chooses zero antifake effort, and zero is the unique optimum.

Milestones

1. (18): $d_1<d_2$.
2. Lemma 7: each $\pi^{pool}_p,\pi^{csep}_p,\pi^{nsep}_p$ strictly decreases in $d\ge0$.
3. The concavity comparison after Lemma 8: for $c>0$, $\rho\,n_{un}(q_H)+(1-\rho)\,n_{un}(q_L)<n_{un}(E[q])$.
4. Advertising revenue is higher under pooling: $E[n^{csep}_r](d)\le E[n^{pool}_r](d)$, strictly if $c>0$.
5. Lemma 8(a): if $d_1\le0$, $\pi^{csep}_p(0)>\pi^{nsep}_p(d_2)$ (under Assumption 3, $p_0<\eta_2$).
6. Lemma 8(b)(1): if $d_1>0$, $\pi^{pool}_p(0)>\pi^{csep}_p(d_1)$.
7. Lemma 8(b)(2): if $d_1>0$, $\pi^{csep}_p(d_1)>\pi^{nsep}_p(d_2)$.

Significance

Proposition 4(a) separates two motives for antifake effort. Effort harms a profit-maximizing platform twice: it raises the consumers' following cost, which lowers participation and revenue, and it costs $\frac{\gamma}{2}d^2$. Pooling, in which low-quality influencers successfully mimic high-quality ones, also earns more revenue than separation, because uninformed consumers follow an average influencer more readily than the average of the two types. So any antifake effort a platform makes must come from its concern for consumer welfare (Proposition 4(b)), not from advertising profit. That is the paper's argument for external pressure or regulation.

The result is proved in the paper's Online Appendix. This mission formalizes the main-text claims behind it: the threshold ordering, Lemma 7, the concavity argument and Lemma 8, together with the goal. To our knowledge none of these has a machine-checked proof. The definitions of the follower and profit model are reusable for the companion mission on the influencer's defensive purchasing (Proposition 3).

Difficulty

The obvious argument is "effort only costs, so choose zero". It is incomplete, because effort changes which equilibrium is played, and the equilibrium profit $\pi_p$ is discontinuous at $d_1$ and $d_2$. Comparing profits across regimes needs two facts. First, pooling revenue dominates separating revenue at the same effort, a strict-convexity (Jensen) inequality for $x\mapsto 1/x$ applied to the uninformed followers through (11)–(12). Second, the thresholds are ordered, $d_1<d_2$, which uses the explicit $\eta_1,\eta_2$. The bookkeeping of (10)–(12), where the advertiser's expectation is nested inside the type-average, has to be unfolded exactly. The boundary case $d_1=0$ falls under Proposition 1(a), so zero effort then induces costly separation, not pooling.

Formalization scope

Parameters form a Lean structure with ASCII field names (mu, lamI, lamP, rho, l, qH, qL, c0, c1, tau, p0, gamma). A Standing predicate records the ranges: $\mu>0$; $\lambda_i,\lambda_p>0$ with $\lambda_i+\lambda_p<1$; $\rho,l\in(0,1)$; $0<q_L<q_H$; $c_0,c_1\ge0$; $\tau\in[0,1)$; $\gamma>0$. $p_0$ is unconstrained, and Assumption 3 ($p_0<\eta_2$) is a separate hypothesis, used only in Lemma 8(a). The model's expectations are the closed forms (8)–(12); no probability space is built. Follower formulas are untruncated, as in the paper. Assumptions 1–2 depend on $d$, are never stated for a range of $d$, and are not needed, so they are not imposed.

The equilibrium regime map is Proposition 1 taken as a definition: the belief systems, the undefeated refinement and the proofs of Lemmas 1–4 are in the Online Appendix, which this mission does not use. The regime test is "$d_1>0$ and $d\le d_1$" for pooling, which matches Proposition 1(a) at $d_1=0$. Lemma 7 is stated on all of $d\ge0$, a superset of each regime's range. The two separating profits are the same function, because real followers depend only on the information revealed. The concavity milestone assumes $c>0$, without which both sides are equal.

The goal is about the equilibrium profit computed from (6) and (8)–(12). It is not about abstract regime profits with Lemmas 7–8 as hypotheses, and pooling revenue is not defined by substituting $E[q]$ into a single-type formula, which would hide the Jensen step. Consumer welfare $U$ is not formalized: its formula is not in the main text, so Proposition 4(b) and Table 3 are out of scope. Contributions welcome: proofs of the milestones and the goal, and a formalization of the signaling game behind Proposition 1.

Selected references

• Z. Huang and D. Liu, Economics of Social Media Fake Accounts, Management Science 71(10):8865–8883, 2025. https://doi.org/10.1287/mnsc.2022.02616
• G. J. Mailath, M. Okuno-Fujiwara and A. Postlewaite, Belief-Based Refinements in Signalling Games, Journal of Economic Theory 60(2):241–276, 1993. https://doi.org/10.1006/jeth.1993.1022
• L. Chen and Y. Papanastasiou, Seeding the Herd: Pricing and Welfare Effects of Social Learning Manipulation, Management Science 67(11):6734–6750, 2021.

Motivation

In a road or communication network, traffic is routed by many independent users, each choosing a route that is fastest for itself given the congestion caused by everyone else. The resulting Nash flow (also called a Wardrop equilibrium, after Wardrop 1952) need not minimize the total delay experienced by all users: Braess's paradox shows that adding a road can make everyone slower. Network designers, transport economists and the designers of Internet congestion-control protocols therefore ask how much total delay is lost to selfish routing, compared with a centrally optimized routing of the same traffic.

Roughgarden and Tardos (J. ACM 2002) gave the first general answers. For linear latency functions they showed that the loss is at most a factor $4/3$. For general latency functions they showed that no such factor exists, and proved instead a bicriteria bound: selfish routing is never worse than optimal routing of twice the traffic. This mission formalizes that bicriteria bound (§3 of the paper) together with its variants for an arbitrary traffic increase (Theorem 3.2) and for approximate equilibria (§5.1).

Timeline:

• 1952: Wardrop states the equilibrium principle for traffic networks.
• 1968: Braess exhibits a network where adding an edge increases the equilibrium delay of every user.
• 2000–2002: Roughgarden and Tardos prove the $4/3$ bound for linear latencies and the bicriteria bound of Theorem 3.1 for all continuous nondecreasing latencies (conference version FOCS 2000, journal version 2002).

Setting

A network has edges $e$ and routes $P$; route $P$ is a set of edges. There are $k$ commodities $i = 1,\dots,k$; commodity $i$ is served by a set of routes $\mathcal P_i$ and has a rate $r_i > 0$, the amount of traffic it must send. A flow assigns an amount $f_P \ge 0$ to each route; it is feasible for the rates $r$ if $\sum_{P \in \mathcal P_i} f_P = r_i$ for every $i$. The flow on edge $e$ is $f_e = \sum_{P \ni e} f_P$.

Each edge has a latency function $\ell_e$, nonnegative, continuous and nondecreasing on $[0,\infty)$: the delay of one unit of traffic crossing $e$ when the edge carries $f_e$. The latency of a route is $\ell_P(f) = \sum_{e \in P} \ell_e(f_e)$, and the cost of a flow is the total delay

$$C(f) = \sum_P \ell_P(f)\, f_P = \sum_e \ell_e(f_e)\, f_e .$$

A feasible flow $f$ is at Nash equilibrium (Definition 2.1) if no amount $\delta > 0$ of the flow on a route $P_1 \in \mathcal P_i$, moved to another route $P_2 \in \mathcal P_i$, would find a latency on $P_2$ smaller than the latency it had on $P_1$. Lemma 2.2 shows this is equivalent to the Wardrop condition: every route carrying flow has minimum latency among the routes of its commodity. Definition 5.1 relaxes the equilibrium by a factor $1 + \epsilon$.

In the Lean development: pathLatency A ℓ x r is $\ell_P(f)$, cost A ℓ x is $C(f)$, IsNashFlow A s ℓ rate x is Definition 2.1, IsApproxNashFlow A s ℓ rate ε x is Definition 5.1, and barLatency is the auxiliary latency $\bar\ell$ of the proof of Theorem 3.1. Edge flows and feasibility are the published KellyStochasticNetworks.linkFlow and wardropFeasible.

Formalization targets

Goal: Theorem 3.1

If $f$ is a Nash flow for the rates $r$ and $f^*$ is any flow feasible for the rates $2r$, then

$$C(f) \le C(f^*).$$

The comparison is with every flow of twice the rates, not only an optimal one.

Milestones

The edge form of the cost (§2.1), Lemma 2.2 (Nash $\Leftrightarrow$ Wardrop), Lemma 2.3 ($C(f) = \sum_i L_i(f) r_i$ for the common latency $L_i(f)$ of the flow-carrying routes of commodity $i$), and the two displayed inequalities of the proof of Theorem 3.1:

$$\sum_e \bar\ell_e(f^*_e) f^*_e - C(f^*) \le C(f), \qquad \sum_P \bar\ell_P(f^*) f^*_P \ge 2C(f).$$

Stronger and related statements

Theorem 3.2: for $\gamma > 0$ and $f^*$ feasible for $(1+\gamma) r$,

$$C(f) \le \tfrac{1}{\gamma}\, C(f^*).$$

Lemma 5.2 (the approximate analogue of Lemma 2.2) and Theorem 5.3: for $0 < \epsilon < 1$, an $\epsilon$-approximate Nash flow $f$ and $f^*$ feasible for $2r$,

$$C(f) \le \frac{1+\epsilon}{1-\epsilon}\, C(f^*).$$

Significance

The price of anarchy, the ratio of the cost of a Nash flow to the minimum cost, is unbounded for general latencies: with two parallel links of latencies $1$ and $x^p$, the ratio tends to infinity as $p$ grows. Theorem 3.1 shows that the inefficiency of selfish routing can nevertheless always be offset by doubling capacity, in the sense that the optimal cost of twice the traffic is at least the Nash cost. Theorem 3.2 quantifies the trade-off for any traffic increase and is essentially tight. These results were among the first quantitative bounds of the price-of-anarchy programme and are a standard part of algorithmic game theory courses.

All statements here are proved in the paper (Theorem 5.3 with its proof omitted there as a close copy of Theorem 3.1). To our knowledge none has a machine-checked proof. This mission produces Lean proofs of Theorem 3.1, its supporting lemmas and its two variants, on top of the published Wardrop-equilibrium definitions of Kelly and Yudovina's chapter on road traffic; existence of a Wardrop equilibrium is already proved on the platform (KellyStochasticNetworks.wardrop_equilibrium_exists), so the goal's hypothesis is satisfiable.

Difficulty

The obvious comparison of $f$ with $f^*$ route by route fails: $f^*$ can place its traffic on edges whose latency is much lower than the Nash latencies, and nothing in the latency functions bounds how much lower, since they are only continuous and nondecreasing. A naive bound on the ratio $C(f)/C(f^*)$ is ruled out by the $x^p$ example above, so any proof must use the doubled rates essentially. In the Lean development, the passage from Definition 2.1 (a statement about perturbed flows) to the Wardrop condition needs a limit $\delta \to 0$ through continuity on $[0,\infty)$, and the cost manipulations need exchanges of finite double sums over routes and edges.

Formalization scope

• Routes, not graphs. Routes are arbitrary columns of a $0/1$ edge–route incidence matrix A, each assigned a commodity by s. The paper's family of simple $s_i$–$t_i$ paths is one instance; the statements therefore hold for every route family (a disclosed generalization; the proofs use no graph structure). Two copies of one edge set serving two commodities are two routes.
• Latencies are assumed nonnegative, nondecreasing and continuous on $[0,\infty)$ only. Continuity replaces the paper's differentiability, as licensed by footnote 3 (p. 7) and by §3 (p. 11).
• Rates are positive reals $r_i > 0$. The number of commodities may be $0$, the paper's $k = 0$, where all statements hold trivially.
• Definition 2.1 is formalized with $P_1 \ne P_2$ and $0 < \delta \le f_{P_1}$. The page writes $\delta \in [0, f_{P_1}]$ and does not exclude $P_1 = P_2$; read literally, $\delta = 0$ would force every route of a commodity, used or not, to have the same latency (contradicting Lemma 2.2), and $P_1 = P_2$ would make Nash flows fail to exist for strictly increasing latencies. Definition 5.1 follows the same convention.
• No ratios. Bounds are stated as $C(f) \le c\, C(f^*)$ for every feasible $f^*$, never as a quotient of costs, so a zero optimal cost cannot make a statement trivial. The constants $1/\gamma$ and $(1+\epsilon)/(1-\epsilon)$ carry $\gamma > 0$ and $0 < \epsilon < 1$.
• Feasibility for $2r$ is wardropFeasible s (fun i => 2 * rate i); for $(1+\gamma) r$ it is wardropFeasible s (fun i => (1 + γ) * rate i). Replacing $2r$ by $r$ would make the goal false (Pigou's example), and comparing only with an optimal $f^*$ would weaken it.
• $\bar\ell$ is a function of the Nash flow's edge flows, not a free parameter.

Needed infrastructure: finite double-sum exchanges, a one-sided limit argument for continuous functions on $[0,\infty)$, and bookkeeping of the perturbed flow $\tilde f$. The lemmas relating Definition 2.1 to the Wardrop condition are reusable by every later result on nonatomic routing games, including the other missions of this series. Contributions of proofs of any milestone are welcome.

Selected references

• T. Roughgarden and É. Tardos, How Bad is Selfish Routing?, Journal of the ACM 49(2), 236–259, 2002. https://doi.org/10.1145/506147.506153
• J. G. Wardrop, Some Theoretical Aspects of Road Traffic Research, Proceedings of the Institution of Civil Engineers 1(3), 325–378, 1952. https://doi.org/10.1680/ipeds.1952.11259
• D. Braess, A. Nagurney and T. Wakolbinger, On a Paradox of Traffic Planning (translation of Braess 1968), Transportation Science 39(4), 446–450, 2005. https://doi.org/10.1287/trsc.1050.0127
• F. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4. https://doi.org/10.1017/CBO9781107284722

Motivation

When many users share a network and each routes its own traffic selfishly, the outcome is a Nash equilibrium rather than a centrally optimized assignment. Koutsoupias and Papadimitriou, in Worst-case equilibria (STACS 1999; journal version 2009), proposed to measure the loss caused by this lack of coordination by the worst-case ratio between the social cost of an equilibrium and the social optimum. The ratio, first called the coordination ratio and now the price of anarchy, became a central quantity of algorithmic game theory, studied for routing, scheduling, congestion games, auctions and network design.

The paper analyses the simplest setting in which the question is nontrivial: agents sending traffic over parallel links, which is the same as scheduling independent jobs on parallel machines with the jobs choosing their machines. For two identical links it determines the price of anarchy exactly.

Timeline.

• 1999: Koutsoupias and Papadimitriou introduce the model and the measure; on two identical links the price of anarchy is $3/2$, and on $m$ identical links it is $\Omega(\log m/\log\log m)$, with a nonmatching upper bound in the conference version.
• 2002: Czumaj and Vöcking, and independently Koutsoupias, Mavronicolas and Spirakis, show that this lower bound is tight for $m$ identical links, $\Theta(\log m/\log\log m)$; Czumaj and Vöcking also give tight bounds for links of different speeds.

Setting

There are $n$ agents and $m$ identical parallel links. Agent $i$ has an amount of traffic $w_i>0$ to send over one link. A pure profile $s=(j_1,\dots,j_n)\in\{1,\dots,m\}^n$ assigns a link to each agent; the load of link $j$ is $\ell_j(s)=\sum_{k:\,j_k=j}w_k$, and the cost of agent $i$ is $\ell_{j_i}(s)$, the traffic on its own link.

A mixed strategy of agent $i$ is a probability distribution $(p_i^1,\dots,p_i^m)$ on the links; the agents randomize independently, so $s$ occurs with probability $\prod_i p_i^{j_i}$. The cost to agent $i$ of a mixed profile $p$ is its expected cost $c_i$. The profile $p$ is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution while the others keep theirs.

The expected traffic on link $j$ is $M^j=\sum_i p_i^jw_i$, and the cost of agent $i$ when its traffic is assigned to link $j$ is $c_i^j=w_i+\sum_{k\ne i}p_k^jw_k=M^j+(1-p_i^j)w_i$.

The social cost of $p$ is the expected maximum load,

$$\mathrm{cost}=\sum_{j_1=1}^m\cdots\sum_{j_n=1}^m\prod_{i=1}^n p_i^{j_i}\,\max_{j}\sum_{k:\,j_k=j}w_k ,$$

and the social optimum $\mathrm{opt}$ is the least maximum load over all pure assignments, the optimum of the $m$-way partition problem for $w_1,\dots,w_n$.

The proof of the main theorem uses two further quantities: the contribution probability $q_i$, the probability that agent $i$ is on the (lexicographically first) link of maximum load, and the collision probability $t_{ik}=\sum_jp_i^jp_k^j$ of agents $i$ and $k$.

Formalization targets

Goal: Theorem 3

For any number $n$ of agents with positive traffics and $m=2$ identical links, every Nash equilibrium $p$ satisfies

$$\mathrm{cost}(p)\ \le\ \frac32\,\mathrm{opt}.$$

Milestones

In the order the proof of Theorem 3 uses them:

1. Equation (2): $c_i^j=w_i+\sum_{k\ne i}p_k^jw_k=M^j+(1-p_i^j)w_i$ for every mixed profile.
2. The support property: at an equilibrium agent $i$ uses only links minimizing $c_i^j$, and $c_i=\min_jc_i^j$.
3. The lower bounds $\mathrm{opt}\ge\max\{w_i,\ \sum_kw_k/m\}$.
4. Theorem 2 with (6): at every equilibrium on $m$ identical links,

$$c_i\ \le\ \frac{\sum_kw_k}{m}+\frac{m-1}{m}\,w_i\ \le\ \Big(2-\frac1m\Big)\mathrm{opt}.$$

5. $\mathrm{cost}=\sum_iq_iw_i$.
6. Inequality (7): $q_i+q_k\le1+t_{ik}$ for distinct agents $i,k$.
7. $c_i=w_i+\sum_{k\ne i}t_{ik}w_k$.
8. On two links, at every equilibrium, $\sum_{k\ne i}q_kw_k\le\big(\tfrac32-q_i\big)\sum_{k\ne i}w_k$.

Companion items

The second sentence of Theorem 1 (on two links some equilibrium has $\mathrm{cost}=\tfrac32\,\mathrm{opt}>0$), which shows the goal is tight, and the fact from its proof that the uniform profile $p_i^j=1/m$ of $m$ unit agents on $m$ links is an equilibrium.

Significance

Theorem 3 and the instance of Theorem 1 show that on two identical links selfish randomized routing never costs more than $50\%$ above the optimum, whatever the number of agents and their traffics, and that this factor is attained. Theorem 2 gives a per-agent guarantee for any number of links: the expected cost an individual agent experiences at any equilibrium is within $2-1/m$ of the optimum, the same factor as Graham's list-scheduling bound. Together they separate the individual and the social view: individual costs stay within a constant, while the expected maximum load, the social cost, can be a factor $\Omega(\log m/\log\log m)$ above the optimum.

The results are proved in the paper. As far as is known they have not been machine-checked. Formalizing them produces a verified model of mixed equilibria in load balancing games, with the social cost as an expected maximum over the product distribution, which is the starting point of the later literature on links with speeds, on general congestion games and on smoothness arguments. The intermediate identities (the contribution and collision probabilities) are reusable for any expected-maximum bound over independent random assignments.

Difficulty

The social cost is an expectation of a maximum over $m^n$ outcomes, and the equilibrium probabilities are given only implicitly, as the solution of a linear system determined by the agents' supports. The natural first idea, to bound the expected maximum load by the maximum expected load $\max_jM^j$, fails: the expected maximum can be much larger, and bounding it is exactly what makes the problem hard (for $m$ links it grows like the maximum occupancy of $m$ balls in $m$ bins). Computing the equilibrium probabilities explicitly does not help either; the paper gives them for two links and notes it does not see how to use them to bound the social cost. The argument has to relate the per-agent expected costs, which the equilibrium condition controls, to the expected maximum, which it does not control directly.

Formalization scope

Agents are Fin n and links Fin m (the goal uses Fin 2); the paper's agent $i$ and link $j$ are indices $i-1$, $j-1$. A mixed profile is p : Fin n → Fin m → ℝ with p i j $=p_i^j$. The game is built on the published definitions agt_games (AGT.IsMixedNash, AGT.expectedPayoff, AGT.profileProb). That vocabulary maximizes payoffs, so the payoff of an agent is minus the load of its link, and the expected cost is minus the expected payoff. The equilibrium is the full mixed Nash condition, including that each $p_i$ is a probability distribution; the support description is a milestone, not the definition. The social cost is the expected maximum load over the product distribution, never the maximum expected load. $\mathrm{opt}$ is a minimum over pure assignments, with the number of links an explicit argument. The lexicographically first maximum link is the lowest-indexed link of maximum load.

Traffics are positive, as in the paper's model; some milestones need only nonnegative traffics or no sign condition, and say so. Statements over $m$ links assume $m\ge1$. Price-of-anarchy statements are inequalities $\mathrm{cost}\le c\cdot\mathrm{opt}$ for every equilibrium, never a quotient $\mathrm{cost}/\mathrm{opt}$, whose value at $\mathrm{opt}=0$ would be a junk $0$. A formalization in which the social cost is $\max_jM^j$, or in which the equilibrium is only a support condition without the requirement that the $p_i$ be distributions, would trivialize or falsify the goal and is ruled out by these definitions.

A complete development needs finite sums over the $m^n$ pure profiles, marginalization of product distributions, and the case analysis of the final step. The marginalization lemmas (summing out the other agents, collision probabilities of independent choices) are reusable beyond this mission. Proofs of the milestones, alternative arguments for Theorem 3, and a proof of Theorem 2 for its own sake are all welcome.

Page numbers are those of the PDF file of the journal version; it prints a page number only on its first page.

Selected references

• E. Koutsoupias and C. Papadimitriou, Worst-case equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38 (this mission cites the authors' journal version of 2009, Computer Science Review 3(2), 65–69, https://doi.org/10.1016/j.cosrev.2009.04.003)
• A. Czumaj and B. Vöcking, Tight bounds for worst-case equilibria, SODA 2002, pp. 413–420; ACM Transactions on Algorithms 3(1), 2007. https://doi.org/10.1145/1186810.1186814
• E. Koutsoupias, M. Mavronicolas and P. Spirakis, Approximate equilibria and ball fusion, Theory of Computing Systems 36, 683–693, 2003. https://doi.org/10.1007/s00224-003-1131-5
• R. L. Graham, Bounds on multiprocessing timing anomalies, SIAM Journal on Applied Mathematics 17(2), 416–429, 1969. https://doi.org/10.1137/0117039

Motivation

A committee that chooses one alternative by voting would like a voting procedure under which no member can gain by misreporting their preferences. Such a procedure is called strategy-proof. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) proved independently that, once at least three outcomes are possible, the only strategy-proof procedures are dictatorial. The result is the starting point of the theory of strategy-proof mechanisms: it is why mechanism design restricts preference domains (single-peaked preferences, quasi-linear utilities) or allows randomization.

This mission formalizes Theorem 1 of Satterthwaite's paper, in the version circulated as Northwestern University CMS-EMS Discussion Paper No. 122 (revised December 12, 1974). Its formulation has one feature that the textbook version lacks: the hypothesis is on the range of the procedure, not on the whole alternative set, and the dictatorship is accordingly relative to that range.

Setting

A committee has a finite set $I_n$ of $n\ge 1$ individuals and a finite set $S_m$ of $m$ alternatives. In a strict committee every individual's ballot $B_i$ is a strong order on $S_m$, a ranking without ties; $x\,\bar B_i\,y$ means that $B_i$ ranks $x$ strictly above $y$. The set of strong orders is $\rho_m$, and a ballot set is $B=(B_1,\dots,B_n)\in\rho^n_m$.

A strict voting procedure $v^{nm}$ assigns to each ballot set a single alternative $v^{nm}(B)\in S_m$. Its range $T_p$ is the set of alternatives it selects at some ballot set, and $p=|T_p|$, so $1\le p\le m$.

Individual $i$ can manipulate $v^{nm}$ at $B$ if some ballot $B_i'$ gives

$$v^{nm}(B_1,\dots,B_i',\dots,B_n)\ \bar B_i\ v^{nm}(B_1,\dots,B_i,\dots,B_n),$$

an outcome $i$ strictly prefers by the standard of the original ballot. The procedure is strategy-proof if no individual can manipulate it at any ballot set.

The procedure is dictatorial if some individual $i$ exists such that, at every ballot set $B$, $v^{nm}(B)$ is the element of the range $T_p$ that $B_i$ ranks highest. It is fully dictatorial if in addition $T_p=S_m$ and partially dictatorial if $T_p\subsetneq S_m$.

The proof uses three further notions. Condition U requires that if every $B_i$ ranks the same $x\in T_p$ above all other elements of $T_p$, then $v^{nm}(B)=x$. The procedure is weak alternative-excluding if $T_p\subsetneq S_m$, and strong alternative-excluding if in addition it satisfies Condition U. Finally $\theta_T(B_i)$ is the restriction of $B_i$ to a subset $T$.

Formalization targets

Goal: Theorem 1 (p. 11)

For a strict committee with $n\ge 1$ and $m\ge p\ge 3$,

$$v^{nm}\ \text{is strategy-proof}\iff v^{nm}\ \text{is dictatorial}.$$

Milestones

1. Lemma 1 (p. 13): a strategy-proof strict procedure satisfies Condition U.
2. Lemma 2 (p. 15): with one individual and three alternatives, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
3. Lemma 3 (pp. 16–17): for $n+1$ individuals and three alternatives, individuals $1,\dots,n$ cannot manipulate $v^{n+1,3}$ if and only if each of the procedures $B\mapsto v^{n+1,3}(B,B_{n+1})$, one for each ballot of individual $n+1$, is strategy-proof.
4. Lemma 4 (p. 22): the induction step from $n$ to $n+1$ individuals for three alternatives.
5. Lemma 5 (p. 25): for $n\ge 1$, $m\ge 3$, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
6. Lemma 6 (p. 26): for $n\ge 2$, if $\theta_{T}(C_i)=\theta_{T}(D_i)$ for all $i$, with $T=T_p$, then $v^{nm}(C)=v^{nm}(D)$.
7. Proof of Theorem 1, (27)–(28) (p. 27): in the case of a strategy-proof, strong alternative-excluding $v^{nm}$ with $m>p\ge 3$, it induces a strategy-proof procedure $v^{np}$ on the alternatives of its range with $v^{np}[\theta_T(B_1),\dots,\theta_T(B_n)]=v^{nm}(B)$.

Significance

Theorem 1 characterizes the strategy-proof strict voting procedures completely: given $p\ge 3$, they are exactly the procedures that let one individual pick, from a fixed menu $T_p$, their favourite element. The classical statement assumes the procedure can select every alternative; Theorem 1 shows that excluding alternatives from the menu does not help, since a procedure with any menu of at least three alternatives is still governed by one individual. The paper's correspondence theorem with Arrow's social welfare functions (its Theorem 2) and its extension to ballots with indifference (Theorem 1') build on this statement.

The full-range case is on the platform already: AGT.gibbard_satterthwaite (Theorem 9.8 of Nisan–Roughgarden–Tardos–Vazirani, Algorithmic Game Theory) is proved and states that an incentive compatible social choice function onto at least three alternatives has a dictator; it is included here as a reference item and is exactly the case $T_p=S_m$ of Lemma 5. The open item MechanismDesign.SocialChoice.gibbard_satterthwaite (Börgers, Proposition 8.1) poses the full-range equivalence. Theorem 1 contains both as the special case $T_p=S_m$. What this mission adds is the range-restricted statement and the paper's own route to it: the induction on the number of individuals for three alternatives (Lemmas 2–4) and the reduction of a procedure with a proper range to its range (Lemma 6 and (27)–(28)). The paper only sketches Lemma 4 and defers the induction on $m$ to Satterthwaite's dissertation, so the formal development fills these gaps.

Difficulty

The "if" direction is immediate. For the "only if" direction the natural first idea is to apply the full-range theorem to the procedure viewed as a map into $T_p$. This fails as stated: the procedure is still defined on rankings of all $m$ alternatives, and nothing yet says that its choice ignores how individuals rank alternatives outside $T_p$. That is the content of Lemma 6, which needs strategy-proofness and Condition U; only after it does the procedure factor through rankings of $T_p$, and only then is the factor itself strategy-proof. The full-range case itself is the classical theorem, whose known proofs (via Arrow's theorem, or by pivotal-voter arguments) are combinatorial and long.

Formalization scope

• Individuals and alternatives are finite types ι and A; $n$ = Fintype.card ι, $m$ = Fintype.card A, and the $n+1$ individuals of Lemmas 3–4 are Option ι, with none the individual $n+1$.
• Strict ballots and strategy-proofness come from the published definition agt_social (namespace AGT): a ballot is a relation r with IsStrictTotalOrder A r, r x y is the paper's $x\,\bar B_i\,y$, and strategy-proofness is AGT.IncentiveCompatible, which is the paper's definition (1) on $\rho^n_m$.
• The range is taken over strict ballot sets only, and $p$ is its Set.ncard. Theorem 1 assumes $n\ge 1$ and $p\ge 3$; $m\ge p$ holds automatically, so $m\ge 3$ is not a separate hypothesis.
• Dictatorial reads the paper's dictator function $f^i_T$ as "the $B_i$-maximal element of $T_p$", which for strong orders is unique.
• $\theta_T(C_i)=\theta_T(D_i)$ is encoded as agreement of the two strict relations on $T\times T$, and the procedure $v^{np}$ of (28) lives on the subtype of the range.
• Lemmas keep their printed hypotheses ($m\ge 3$, $p\ge 1$, Lemma 6's $n\ge 2$), even where the conclusion would hold without them. The range restriction milestone keeps the proof's case assumptions of strong alternative exclusion and $m>p\ge 3$.

Two encodings would trivialize the goal and are excluded: a range taken over all relation profiles (junk values would make $p\ge 3$ meaningless), and a dictatorship that only constrains ballot sets at which the dictator's overall favourite lies in $T_p$, or that asks for the dictator's favourite in all of $S_m$ (false whenever $T_p\subsetneq S_m$). The bound $p\ge 3$ is needed: a procedure with two possible outcomes, such as majority vote between two fixed alternatives, is strategy-proof and not dictatorial, and an imposed procedure ($p=1$) is dictatorial only vacuously.

Contributions are welcome at every milestone, and the restriction-to-range step (Lemma 6 and (27)–(28)) is reusable for any statement that transfers results from full-range to range-restricted procedures.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; published in J. Econ. Theory 10(2) (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41(4) (1973) 587–601. https://doi.org/10.2307/1914083
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), Chapter 9 of N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

A Nash equilibrium is a joint choice of strategies at which no player can improve their own expected payoff by changing their strategy alone. This gives a testable notion of stable behavior for a finite game, including games in which the players' aims differ. Nash's two-page 1950 note established the existence of such a point for finite games by organizing each player's best replies into a single correspondence and using a fixed-point theorem. The note identifies several properties of that correspondence and ends by comparing equilibrium payoffs in zero-sum and general games. Those claims, stated together in Nash's published note, are the subject of this mission.

The existence conclusion itself already has a proved formal statement, AGT.nash_existence, in the game vocabulary used here. The remaining claims explain what the fixed-point argument acts on: which profiles are related by countering, why countering sets are usable as values of a correspondence, and what their fixed points mean. Keeping those statements explicit makes the 1950 argument legible independently of the existence theorem's proof.

Setting

There is a finite set $I$ of players. Each player $i$ has a finite, nonempty set $S_i$ of pure strategies. A pure-strategy profile $s$ chooses one element of every $S_i$, and $u_i(s)\in\mathbb R$ is player $i$'s payoff. A mixed strategy $P_i$ assigns a nonnegative real weight to each element of $S_i$, with weights summing to one. The space $\Sigma$ of mixed profiles $P=(P_i)_{i\in I}$ is the product of these finite probability simplices.

Players randomize independently. Thus the probability of a pure profile $s$ under $P$ is $\prod_{j\in I}P_j(s_j)$, and player $i$'s expected payoff is

$$U_i(P)=\sum_{s\in\prod_j S_j}\left(\prod_{j\in I}P_j(s_j)\right)u_i(s).$$

For a strategy $\tau_i$ of player $i$, write $U_i(\tau_i,P_{-i})$ for the payoff obtained by replacing only coordinate $i$ of $P$. A profile $Q$ counters $P$ if $Q\in\Sigma$ and, for every player $i$, its coordinate $Q_i$ gives that player the highest expected payoff available against the other players' coordinates of $P$:

$$Q\in C(P)\quad\Longleftrightarrow\quad Q\in\Sigma\quad\text{and}\quad U_i(\tau_i,P_{-i})\le U_i(Q_i,P_{-i}) \quad\text{for every }i\in I\text{ and every mixed }\tau_i.$$

The countering correspondence $C$ assigns the set $C(P)$ to each $P\in\Sigma$. Its graph comprises the pairs $(P,Q)$ with $P\in\Sigma$ and $Q\in C(P)$. A fixed point is a profile $P$ belonging to $C(P)$; Nash calls it an equilibrium point.

Formalization targets

The goal states the three properties of $C$ that Nash uses, along with the identification of its fixed points:

$$\forall P\in\Sigma,\qquad \varnothing\ne C(P)\subseteq\Sigma, \qquad C(P)\text{ is convex};$$ $$P_k\to P,\ Q_k\to Q,\ Q_k\in C(P_k)\text{ for all }k \quad\Longrightarrow\quad Q\in C(P); \qquad P\in C(P)\ \Longleftrightarrow\ P\text{ is a Nash equilibrium}.$$

The milestone list follows the claims in the note: the payoff functions are polylinear and continuous; the correspondence maps mixed profiles to nonempty subsets of mixed profiles; its values are convex; its graph is closed in the sequential formulation Nash writes; and self-countering is equilibrium. A separate closed-set formulation records the graph property in the product topology.

The note also asserts a distinction about payoffs. In a two-person zero-sum game, where $u_0(s)+u_1(s)=0$ on every pure profile, any two equilibria have the same expected payoff for each player:

$$U_i(\sigma)=U_i(\sigma')\qquad(i=0,1).$$

For general games, this can fail. A companion target asks for a finite two-person game with two equilibria having different expected payoffs.

Significance

The correspondence theorem records the precise conditions on which Nash's application of Kakutani's fixed-point theorem rests. Nonempty convex values and a closed graph make the fixed-point route applicable to the mixed-strategy space; the fixed-point clause says why its output is an equilibrium of the game rather than only a topological point. The zero-sum companion separates the common value of a two-person zero-sum game from the possible range of equilibrium payoffs in a general game. These consequences and the comparison appear in Nash's note.

The equilibrium existence theorem is already proved as the referenced AGT.nash_existence. What remains here is to formalize the correspondence properties and the payoff comparison as their own auditable statements, using that theorem's published game definitions. The claims are known results from 1950; their appearance as goals means proofs of these particular statements are still to be supplied in this development.

Difficulty

The payoff of a player depends on every player's strategy, while countering compares only one changed coordinate at a time. The relevant set of maximizers is therefore indexed by the countered profile, and all players' choices must fit into one countering profile. Establishing closedness requires passing the payoff comparisons and the probability-vector conditions through limits of profiles. The zero-sum equality concerns arbitrary pairs of equilibria, which need not use the same strategies; an argument based only on the existence of an equilibrium cannot give it. For general games, a single equilibrium says nothing about whether another equilibrium has a different payoff.

Formalization scope

The Lean development uses a finite player type ι, finite pure-strategy types S i, real payoffs u, and the published definitions AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash. The goal and nonempty-value milestone require each S i to be nonempty. The note's probability distributions implicitly require this; the player type itself may be empty. A mixed profile is a tuple of finite real weight vectors, with no measure-theoretic integration or hidden normalization. In the two-person claim, players are 0, 1 : Fin 2.

Convergence is in the ordinary product topology of the real coordinate spaces. The sequence index is $k$ because the note also uses $n$ for the number of players. Counters u P Q requires $Q$ to be a mixed profile and compares $Q_i$ with every mixed deviation against $P_{-i}$; this rules out arbitrary weight vectors and comparisons against the wrong opponents. Neither continuity nor the existence of a best response is assumed in the goal: those properties are targets. The definition layer and the payoff continuity and polylinearity results can be reused by other finite-game formalizations.

Selected references

• J. F. Nash, Jr., Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49 (1950). DOI: 10.1073/pnas.36.1.48.
• S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8, 457–459 (1941), cited in Nash's footnote 1. DOI: 10.1215/S0012-7094-41-00838-4.

Motivation

In a finite game, a referee can recommend one action privately to each player according to a joint distribution. The recommendations may be correlated: learning one's own recommendation can convey information about the others'. A correlated equilibrium is a distribution for which no player gains, in expectation, by replacing a particular recommendation with another action. This solution concept uses the same payoff data as a strategic-form game but allows more joint distributions than independent mixed strategies. Hart and Schmeidler's Theorem 1 establishes that at least one such distribution exists for every finite game, with no assumptions on the payoffs beyond being real-valued. Their paper uses the finite result as the starting point for existence results with infinitely many players and, later, compact strategy spaces. Hart and Schmeidler (1989)

The authors explain that the standard route passes through a mixed Nash equilibrium: independent equilibrium strategies induce a correlated distribution. The finite theorem here is the same existence conclusion expressed directly through recommendation inequalities, which are linear in the joint distribution. That distinction matters for the later sections of the paper, where the authors examine games with infinitely many players, including an example with a countably additive correlated equilibrium but no Nash equilibrium. Hart and Schmeidler (1989), pp. 18, 21–22

Setting

Let $N$ be a finite player set. Each player $i\in N$ has a finite, nonempty set $S^i$ of pure strategies, and a pure profile is a tuple $s=(s^i)_{i\in N}$ in $S=\prod_{i\in N}S^i$. The real number $h^i(s)$ is player $i$'s payoff at $s$. For a player $i$, write $s^{-i}$ for all coordinates except $i$ and $(s^{-i},t^i)$ for the profile obtained by replacing the $i$th coordinate with $t^i$. A probability vector on $S$ is a function $p:S\to\mathbb R$ with $p(s)\ge0$ for every $s$ and $\sum_{s\in S}p(s)=1$. These are exactly the paper's finite-game and probability-vector conventions. Hart and Schmeidler (1989), pp. 18–19

Suppose the referee draws $s$ with probability $p(s)$ and privately tells player $i$ only $s^i$. For every recommended action $r^i\in S^i$ and alternative action $t^i\in S^i$, the incentive inequality is

$$\sum_{s^{-i}\in S^{-i}}p(s^{-i},r^i) \bigl[h^i(s^{-i},r^i)-h^i(s^{-i},t^i)\bigr]\ge0.$$

When the recommendation $r^i$ has zero probability, this inequality holds automatically. Thus no conditional probability needs to be defined in that case. A probability vector satisfying every such inequality is a correlated equilibrium. The inequalities include $r^i=t^i$, whose left-hand side is zero. Hart and Schmeidler (1989), p. 19, condition (1)

Formalization targets

Theorem 1: existence in every finite game

The mission's goal is the paper's Theorem 1, with its definition of correlated equilibrium kept explicit:

$$\forall (N,(S^i)_{i\in N},h),\quad \exists p\in\Delta(S)\quad \forall i\in N\ \forall r^i,t^i\in S^i,\quad \sum_{s^{-i}}p(s^{-i},r^i) \bigl[h^i(s^{-i},r^i)-h^i(s^{-i},t^i)\bigr]\ge0.$$

Here $\Delta(S)$ denotes the set of probability vectors on the finite set $S$. The quantified payoffs are arbitrary real functions; the result specifies neither a unique equilibrium nor a particular equilibrium distribution. The milestone list records the paper's auxiliary-game correspondence, its finite minimax criterion, the nonnegative-matrix lemma, equation (2), and the final product-strategy identity. The lemma is linked to the already proved platform theorem CalibratedCE.Forecast.flow_conservation_solvable, which states the equivalent balance equations for a nonnegative matrix indexed by a nonempty finite set. Hart and Schmeidler (1989), pp. 19–20

Significance

The result guarantees feasibility of the complete system of recommendation inequalities for every finite payoff table. It is stronger as a foundation than checking an equilibrium in one game: later arguments can invoke the result after restricting a larger game to finite strategy sets. Hart and Schmeidler do exactly that in their infinite-game existence theorems. The finite theorem is already known mathematically; the task here is to give its particular statement and proof structure reusable, machine-checked declarations. Hart and Schmeidler (1989), pp. 20, 22, 24

The platform already has the general finite-game lottery vocabulary in agt_games and a proved mixed Nash-existence theorem, AGT.nash_existence. It also has AGT.IsCorrelatedEquilibrium in swap-function cost notation, AGT.swap_regret_correlated_equilibrium for approximate equilibria, and Aumann 1987's finite-probability-space model. Those results provide related notions and consequences. With $\varepsilon = 0$ and costs $-h^i$, the swap-function form of AGT.IsCorrelatedEquilibrium is equivalent to condition (1), since a switching rule can be optimized separately for each recommendation; the mission nevertheless states condition (1) as printed. The finite Minimax Theorem invoked on p. 19 is proved on the platform as AGT.zero_sum_minimax (a saddle-point statement for matrices indexed by Fin (m+1) and Fin (n+1), in another Mathlib environment), so the minimax milestone is the consequence the paper draws from it rather than the theorem itself. This mission fixes Hart and Schmeidler's payoff-maximizing condition (1) directly, with its recommendation-specific inequalities and auxiliary-game steps. The linked flow-conservation theorem was formalized in the Foster–Vohra series; its balance equations have the same content as the lemma on p. 19 after expanding the coefficients of an arbitrary vector $u$. Hart and Schmeidler (1989), p. 19

Difficulty

The inequalities must hold simultaneously for every player and every recommended-action/deviation pair. Choosing a distribution that makes one inequality hold does not ensure the others: the same weights $p(s)$ occur in several constraints. An arbitrary product distribution can fail even in a two-player coordination game. Passing through an existing mixed Nash equilibrium proves existence, but gives no formal account of the paper's own finite minimax and nonnegative-matrix claims. The proof obligations here include the exact correspondence between the conditional recommendation constraints and an auxiliary two-person game, plus the algebra of a product of playerwise probability vectors. Hart and Schmeidler (1989), pp. 18–20

Formalization scope

Players are a finite Lean type $\iota$; $S^i$ is a finite, nonempty type, and $h^i:S\to\mathbb R$. The profile space is the dependent product $S=\prod_iS^i$. The expression $(s^{-i},t^i)$ is Function.update s i t, and summing over $S^{-i}$ with the $i$th coordinate fixed to $r^i$ is represented by summing over profiles satisfying $s^i=r^i$. Probability vectors use the published AGT.IsLottery: nonnegative real weights whose finite sum is one. No measure-theoretic integral or conditional probability appears in this finite mission. The auxiliary minimizing player's pure strategies form one set of triples $(i,r^i,t^i)$, with one probability vector over all triples. Hart and Schmeidler (1989), p. 19

Nonemptiness of each $S^i$ is required: an empty strategy set would leave no probability vector on $S$. The player set itself may be empty; then $S$ has one profile and the incentive conditions have no instances. The generic minimax milestone separately assumes that both of its pure-strategy sets are nonempty, so solvers must handle the playerless goal directly. Equality decisions are computational instances for finite enumeration, not restrictions on mathematical games. The correlated-equilibrium definition includes normalization and all incentive inequalities; it is not defined to hold automatically. The goal is the existence of a probability vector satisfying condition (1) itself, not a restatement through AGT.nash_existence that would make it a corollary of Nash's theorem. A sorry-free local check exhibits a correlated point mass in a two-player coordination game and another point mass that violates an incentive inequality. Contributions to the finite minimax criterion, its connection to the published balance theorem, and the sum rearrangement in the product-strategy milestone are all useful beyond this one goal.

Selected references

• Sergiu Hart and David Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 1989, pp. 18–25. DOI.
• Noam Nisan, Tim Roughgarden, Éva Tardos, and Vijay V. Vazirani, eds., Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. DOI.