Algorithmic Game Theory

Motivation

For games with three or more players, Nash equilibria can be irrational, so they cannot in general be computed exactly. Bubelis made this precise: any real root of any univariate polynomial arises as the probability of a particular strategy, or the payoff of a particular player, in a Nash equilibrium of a three-player game whose payoffs depend on the coefficients of the polynomial (Bubelis 1979).

Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) restate Bubelis's construction as Lemma 7, in a form that controls the equilibrium probabilities rather than a payoff, and that guarantees the equilibrium is unique. They use it, for linear polynomials, as the single gadget behind every arithmetic operation in their reduction from PosSLP and SQRT-SUM to deciding properties of the unique Nash equilibrium of a three- or four-player game (their Theorem 4). The uniqueness clause is what makes the composed game itself have a unique equilibrium.

• 1951: Nash proves every finite game has an equilibrium in mixed strategies.
• 1979: Bubelis shows that every real algebraic number is an equilibrium probability or payoff of some three-player game (Theorem 2 of the cited paper).
• 2007–2010: Etessami and Yannakakis restate the construction as Lemma 7, with uniqueness and full support of the equilibrium, and use it to prove PosSLP- and SQRT-SUM-hardness of Nash equilibrium problems (FOCS 2007; journal version 2010).

Setting

Fix an integer $m \ge 0$ and real coefficients $c_0, \dots, c_m$, and let

so $c_j$ is the coefficient of $x^{m-j}$; the leading coefficient may vanish.

The gadget $G_f$ is a game with three players. The primary player 1 has the strategies $0, 1$; the auxiliary players 2 and 3 each have the strategies $0, 1, \dots, m$. For a pure profile $s = (s_1, s_2, s_3)$, and with $\chi(P)$ the indicator of a predicate $P$, the payoffs are

The auxiliary payoffs do not depend on $f$ and take values in $\{0, 1, -1\}$.

A mixed profile $x = (x_1, x_2, x_3)$ assigns to each player $p$ a probability vector $x_p$ on its strategies; the players randomize independently. Player $p$'s expected payoff $u_p(x)$ is the expectation of its payoff under the product distribution, and $u_p((p:j); x_{-p})$ is its expected payoff when it switches to the pure strategy $j$. A Nash equilibrium is a mixed profile in which no player can raise its expected payoff by switching unilaterally to any other mixed strategy. A profile is fully mixed if every pure strategy of every player has positive probability. Throughout, $\xi = x_1(0)$, and $v_2$, $v_3$ are the equilibrium payoffs of players 2 and 3.

Formalization targets

Goal: Lemma 7

Assume $f(0) \le 0$, $f(1) \ge 0$, and that $f$ has a unique root $\alpha$ in $[0,1]$. Then every Nash equilibrium $x$ of $G_f$ satisfies

and if $\alpha \ne 0$ and $\alpha \ne 1$, then $G_f$ has exactly one Nash equilibrium, and it is fully mixed.

Milestones (proof of Lemma 7, p. 26)

1. In any finite game, at a Nash equilibrium, $u_p((p:j); x_{-p}) \le u_p(x)$, with equality when $x_p(j) > 0$.
2. In every Nash equilibrium of $G_f$: $v_2 > 0$ and $v_3 \ge 0$.
3. In every Nash equilibrium of $G_f$: $x_2(j) = \xi^{m-j} \big/ \sum_{i=0}^m \xi^i$ for all $j$.
4. In every Nash equilibrium of $G_f$: $u_1((1:1); x_{-1}) = f(\xi) \big/ \sum_{i=0}^m \xi^i$.
5. Under the hypotheses of Lemma 7 and $\alpha \ne 0$: $x_3(j) = 1/(m+1)$ for all $j$.

Milestones 2–4 hold for every coefficient vector; only milestone 5 and the goal use the hypotheses on $f$.

Significance

The lemma is the arithmetic engine of the hardness results of Etessami and Yannakakis: a polynomial equation in one unknown is solved, exactly and uniquely, by the equilibrium of a fixed-size game whose auxiliary payoffs do not depend on the equation. With $f$ linear, the gadget implements addition, multiplication and division of probabilities in $(0,1)$; with higher degree it implements roots and fractional powers. Without the uniqueness clause, the composed games of Theorem 4 could have spurious equilibria, and the reduction would not apply to games promised to have a unique equilibrium.

The result is proved in the paper (pp. 25–26, following Bubelis). As far as is known, no part of it is machine-checked: there is no formal statement of Bubelis's gadget, and the support property of Nash equilibria is not on the platform in this vocabulary. This mission produces the first formal statement and proof of the gadget's equilibrium characterization, including the existence half of "has a unique Nash equilibrium", which the paper takes from Nash's theorem but which here is a concrete profile to check.

Difficulty

The gadget's equilibria are those of a three-player game, so the payoffs are cubic in the probabilities and no linear-programming argument applies. The obvious first idea, writing down the indifference conditions of players 2 and 3 and solving them, presupposes that every strategy of player 2 is played; nothing guarantees that in advance, and the profiles in which some strategies are unplayed have to be excluded. The boundary cases $\xi = 0$ and $\xi = 1$ are not covered by an indifference argument for the primary player and need the sign conditions $f(0) \le 0$ and $f(1) \ge 0$ separately. The strategy of player 3 is pinned down only when $\alpha \neq 0$, which is why the uniqueness part of the lemma excludes the endpoints. Finally, existence of the equilibrium is part of the statement and cannot be delegated to Nash's theorem, which is not available on the platform.

Formalization scope

The game uses the published vocabulary agt_games (mixed profiles as weight functions, AGT.expectedPayoff, AGT.IsMixedNash with mixed deviations) and DGPNash.NashMap.purePayoff for $u_p((p:j); x_{-p})$. The players are a three-element type primary | aux2 | aux3; strategies are Fin 2 and Fin (m+1), 0-based as on the page. The coefficients are c : Fin (m+1) → ℝ and $f$ is the explicit sum $\sum_j c_j \xi^{m-j}$ with natural-number exponent; the congruence $s_2 + 1 \equiv s_3$ is addition in Fin (m+1); $\xi^0 = 1$ for every $\xi$, including $0$.

Explicit readings committed to:

• "has a unique root $\alpha$ in $[0,1]$" is a named $\alpha$ with $0 \le \alpha \le 1$, $f(\alpha) = 0$, and $\beta = \alpha$ for every root $\beta \in [0,1]$;
• "the game has a unique Nash equilibrium" is existence and uniqueness (∃! over mixed profiles);
• "the NE is fully mixed" applies to all three players;
• coefficients are real, generalizing the paper's rationals; the degree is at most $m$;
• the support property is stated for an arbitrary finite game;
• the last two clauses of Lemma 7 (auxiliary payoffs independent of $f$, values in $\{0,1,-1\}$; primary payoff $c_{s_2}$ or $0$) hold by the definition of the gadget and are not separate theorems.

The goal is not trivialized by a pure-strategy notion of equilibrium (deviations are mixed), by dropping uniqueness of the root (without it $x_1(0) = \alpha$ is false), or by reading "unique equilibrium" as uniqueness alone. For $m = 0$ the hypotheses cannot hold, as on the page.

A complete development needs the support property (reusable for any finite game), the linearity of expected payoff in one player's strategy, and finite-sum manipulations for the geometric weights $\xi^{m-j}$. Contributions of general lemmas about AGT.IsMixedNash and purePayoff are welcome and reusable well beyond this mission.

Selected references

• K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points, SIAM J. Comput. 39(6) (2010) 2531–2597 (author manuscript; Lemma 7, pp. 25–26). https://doi.org/10.1137/080720826
• K. Etessami and M. Yannakakis, On the complexity of Nash equilibria and other fixed points (extended abstract), Proc. FOCS 2007. https://doi.org/10.1109/FOCS.2007.48
• V. Bubelis, On equilibria in finite games, Int. J. Game Theory 8(2) (1979) 65–79. https://doi.org/10.1007/BF01768703
• J. Nash, Non-cooperative games, Ann. of Math. 54(2) (1951) 286–295. https://doi.org/10.2307/1969529

Motivation

That noncooperative play usually wastes something is part of the folklore of game theory, with the Prisoner's Dilemma as its emblem: each player's best reply leads to an outcome that both would trade for another. Pradeep Dubey's paper turns this folklore into a theorem about smooth games. For games whose payoffs are twice continuously differentiable, and for all payoffs outside a negligible (closed, nowhere dense) set, Nash equilibria are finite in number and are Pareto-inefficient unless some player sits at a vertex of his strategy set. The same conclusion applies to Nash's mixed extensions of finite games (Nash 1951), where a vertex is a pure strategy.

The question is basic to welfare analysis of strategic interaction: market games, oligopoly, public goods and trading mechanisms (Shapley and Shubik 1977) all ask whether equilibrium outcomes can be efficient. Dubey's answer is that efficiency of an equilibrium is non-generic, so a model that delivers it is exploiting special structure.

Timeline. Nash (1951) introduced equilibrium points and multi-matrix games. Smale (1973, "Optimizing several functions") gave the first-order condition for Pareto optimality of several smooth functions: at an efficient interior point the gradients are linearly dependent. Harsanyi (1973, IJGT 2:235–250) proved that generic finite games have finitely many, indeed an odd number of, mixed equilibria. Dubey's Cowles Foundation Discussion Paper 508R (1978) stated finiteness and inefficiency; the version formalized here is the rewrite IIASA WP-83-74 (1983), published as Mathematics of Operations Research 11(1):1–8 (1986).

Setting

There are $n\ge2$ players $N=\{1,\dots,n\}$. Player $i$'s strategy set is the unit simplex

whose vertices (extreme points) are the origin and the unit vectors. Profiles $s=(s^1,\dots,s^n)$ range over $S=S^1\times\dots\times S^n\subset\mathbb R^{r(n)}$, $r(n)=\sum_i k(i)$.

Fix open neighbourhoods $V^i\supseteq S^i$ and $V=V^1\times\dots\times V^n$. The space $U$ consists of the $C^2$ functions $f:V\to\mathbb R$ with finite $C^2$-norm $\|f\|=\sup\{\|f(s)\|,\|Df(s)\|,\|D^2f(s)\|: s\in V\}$. A game is $u=(u^1,\dots,u^n)\in(U)^n$. For $T\subseteq N$, $(s|e)$ replaces $s^i$ by $e^i$ for $i\in T$. A profile $s\in S$ is $T$-efficient if no $e\in\times_{i\in T}S^i$ gives $u^i(s|e)\ge u^i(s)$ for all $i\in T$ with strict inequality for some $j\in T$. It is a Nash equilibrium if it is $\{i\}$-efficient for each $i$, efficient if it is $N$-efficient, and a strong Nash equilibrium if it is $T$-efficient for every $T$. The three sets are $N(u)$, $E(u)$, $G(u)$.

In the proof, $D_u(s)$ is the $n\times r(n)$ matrix with rows $Du^i(s)$; $N^*$ is the subspace of matrices whose $i$-th row vanishes on player $i$'s block of columns; $E^*$ is the set of matrices with linearly dependent rows.

Formalization targets

Goal: the Theorem (p. 3)

There is an open dense set $U_0\subseteq(U)^n$ such that for $u\in U_0$:

Milestones (pp. 4–6)

For interior profiles ($s^i\in\operatorname{Int}S^i$ for all $i$):

$\operatorname{codim}N^*=r(n)$; the linear perturbation $u_t^i(x)=u_0^i(x)+t\sum_j y_{ij}x_j$ satisfies $\frac{d}{dt}D(u_t,s_0)|_{t=0}=y$ (the computation behind (**)); claim (*) for $M=N^*$: for an open dense set of games $D_u$ is transverse to $N^*$ on a compact neighbourhood $\underline V$ of $S$; under that transversality $S\cap D_u^{-1}(N^*)$ is finite; and the Theorem restricted to interior profiles.

Companions

The Theorem (Multi-Matrix) (p. 14): for an open dense set of payoff vectors $a\in(\mathbb R^K)^n$, the mixed Nash equilibria of $\Pi_a$ are finite, an efficient one has a player using a pure strategy, and a strong one is pure. From the example of §3: every game $(P,Q)$ on $[0,1]^2$ with payoffs $u_P(x,y)=-[(x-a)^2+(y-b)^2]$ has a unique Nash equilibrium (p. 9); Lemma 1, $E(P,Q)=r_X(L(P,Q))$ (p. 9); Lemma 2(a), an interior equilibrium is efficient iff $a=c$ or $b=d$ (p. 10).

Significance

The theorem gives the generic structure of equilibrium sets in smooth games: isolated and finitely many equilibria, and a sharp location of the only places where efficient equilibria can survive, namely the vertices. It explains why efficiency results for noncooperative models need boundary solutions or non-generic structure, and in its multi-matrix form it shows that strong equilibria of generic finite games are in pure strategies. It also supplies the finiteness of equilibria used in comparative-statics and index arguments.

On the formalization side, the result is proved on paper but has no machine-checked version. A complete development would give Lean its first generic-finiteness theorem for Nash equilibria of smooth games, a first-order Pareto condition in the form of Smale's lemma, and a parametric transversality argument in finite dimensions. The multi-matrix companion connects to the published vocabulary of finite games (agt_games), and the example of §3 is an elementary, fully explicit check of the general picture.

Difficulty

The interior case reduces, by (i) and (ii), to a dimension count: $D_u^{-1}(N^*)$ should be zero-dimensional and $D_u^{-1}(N^*\cap E^*)$ empty. Neither holds for every game: they hold only when $D_u$ is transverse to $N^*$ and to the strata of $N^*\cap E^*$, and the step that requires work is showing that transversality is an open and dense condition in the $C^2$ topology. Density is not obtained by adding linear functions to the payoffs: a linear function has finite $C^2$-norm on $V$ only when $V$ is bounded, so perturbations must be localized. The step from interior profiles to the whole of $S$ is a second difficulty. It requires repeating the argument on every product of faces of the simplices and on every subgame, and then intersecting finitely many open dense sets. Efficiency at a boundary point is not $T$-efficiency in a subgame, so the reduction has to be made with care.

Formalization scope

Players are Fin n with 2 ≤ n; block sizes k : Fin n → ℕ with 1 ≤ k i; profiles are ∀ i, Fin (k i) → ℝ. The simplex is the paper's corner simplex {x ≥ 0, ∑ x ≤ 1}, not the probability simplex; "vertex" is Set.extremePoints. The neighbourhoods $V^i$ are taken open, and the goal is stated for every such choice, not assuming $V$ bounded or convex. Payoffs are total functions; a game is ContDiffOn ℝ 2 on $V$ with finite $C^2$-norm, which takes values in $[0,\infty]$, so no junk real supremum enters. "Open dense in $(U)^n$" is written in $\varepsilon$-form for the product of $C^2$-norm topologies; Lean's sup-type norms are equivalent to the Euclidean ones, so the open dense sets are the same. Deviations range over all strategies in $\times_{i\in T}S^i$, not only pure or vertex deviations.

Added hypotheses, all disclosed in the items: openness of $V^i$; interiority of every $s^i$ on milestones (i), (ii) and the finiteness step (the proof's standing case assumption); $M=N^*$ in claim (*). The printed "By (i), $N(u)\subset S\cap D_u^{-1}(N^*)$" is stated for interior equilibria, which is where (i) applies.

A trivializing formalization is ruled out: the open dense set must contain games arbitrarily close to every game (the zero game is a game, so it is never empty), interiority appears only in the milestones and not in the goal, and efficiency is with respect to all deviations in $S$.

Not stated: (*) for a general submanifold $M$, and the decomposition of $N^*\cap E^*$ into submanifolds of codimension $\ge r(n)+1$, both of which need embedded submanifolds of $\mathbb R^N$; Remarks 1–4 (Remark 4's openness claim for strictly concave payoffs is false as printed); Lemma 2(b); §5, which the author leaves as a conjecture. Contributions welcome: a finite-dimensional parametric transversality theorem, Smale's first-order Pareto condition, and the face-by-face reduction.

Selected references

• P. Dubey, Inefficiency of Nash Equilibria, IIASA Working Paper WP-83-74, 1983; Mathematics of Operations Research 11(1):1–8, 1986. https://doi.org/10.1287/moor.11.1.1
• J. F. Nash, Non-Cooperative Games, Annals of Mathematics 54:286–295, 1951. https://doi.org/10.2307/1969529
• J. C. Harsanyi, Oddness of the Number of Equilibrium Points: A New Proof, International Journal of Game Theory 2:235–250, 1973. https://doi.org/10.1007/BF01737572
• S. Smale, Optimizing Several Functions, Manifolds — Tokyo 1973, Proceedings of the International Conference on Manifolds, University of Tokyo Press, 1975.
• R. Abraham and J. Robbin, Transversal Mappings and Flows, W. A. Benjamin, New York, 1967.
• L. S. Shapley and M. Shubik, Trade Using One Commodity as a Means of Payment, Journal of Political Economy 85:937–968, 1977. https://doi.org/10.1086/260617

Motivation

Mean-payoff games ask which starting positions allow a player to guarantee a nonnegative long-run average reward. Binary-encoded weights make the bit cost of solving the complete winning set a central part of the question. The source manuscript presents the surrounding research claim.

Setting

A game is a finite nonempty directed multigraph with integer edge weights, an owner for each vertex and an outgoing edge everywhere. Winning means that a history-dependent maximizer strategy guarantees liminf average payoff at least zero against every opponent strategy.

Formalization target

Construct one randomized three-tape machine and C>0 such that every encoded game of length L has a time bound

all T-bit random tapes halt by T, and at least 7/8 of them output the exact winning-set indicator, with all other output cells blank.

The selected formal target is OAI.randomized_quasipolynomial_mean_payoff.

Significance and status

The target makes the input encoding, computation model, success fraction and complete output explicit. It is an existence theorem for a uniform machine, not a separate solver for each game. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The running time must hold on every random tape, while correctness holds on the specified fraction. Signed weights and the full binary input length cannot be replaced by unary magnitude bounds.

Formalization scope

The published definitions specify games, strategies, plays, liminf payoffs, serialization and tape transitions. The independent finite Truffet elimination counterexample is retained as contextual reference; it is not a prerequisite or an asserted proof of the randomized algorithm. The manuscript’s certification/always-correct consequence is not an additional attached goal.

Selected references

• OpenAI, Randomized quasipolynomial-time mean-payoff games, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Finite games in strategic form are the basic model of strategic interaction in economics, engineering and computer science. Potential games (Monderer and Shapley, 1996, DOI 10.1006/game.1996.0044) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics converge to one.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) decompose every finite game canonically into a potential, a harmonic and a nonstrategic component, by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games are the complement of potential games, and their equilibria behave in the opposite way: they generically have no pure Nash equilibrium. This mission formalizes the paper's positive result on the harmonic side. In every harmonic game, whatever the number of players and strategies, the profile in which every player randomizes uniformly over its strategies is a mixed Nash equilibrium. Rock–paper–scissors and matching pennies are the familiar two-player instances.

Setting

A finite game has a finite set of players $\mathcal M$ and, for each player $m$, a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$. We write $p^{-m}$ for the strategies of the players other than $m$, $E^{-m} = \prod_{k\ne m}E^k$, and $(q^m, p^{-m})$ for $p$ with player $m$'s strategy replaced by $q^m$. A game is identified with its utilities $u = (u^m)_m$, $u^m : E \to \mathbb R$, which form an element of $C_0^M$, where $C_0 = \{f : E\to\mathbb R\}$ carries $\langle\varphi_1,\varphi_2\rangle_0 = \sum_p\varphi_1(p)\varphi_2(p)$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges. The space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A}X(p,q)Y(p,q)$. The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$-comparable pairs gives $D_m : C_0\to C_1$, and $Du = \sum_m D_m u^m$ is the flow of payoff differences of $u$. With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$, Definition 4.2 of the paper sets

A game is a harmonic game if $u\in\mathcal H\oplus\mathcal N$, and a normalized harmonic game if $u\in\mathcal H$.

A mixed strategy of player $m$ is a probability vector $x^m\in\Delta E^m$, and a mixed strategy profile is $x = \{x^m\}_m\in\prod_m\Delta E^m$. The mixed extension is $u^m(x) = \sum_{p\in E}u^m(p)\prod_k x^k(p^k)$ (34). The payoff of the pure strategy $q^m$ against $x^{-m}$ is $u^m(q^m,x^{-m}) = \sum_{p^{-m}}u^m(q^m,p^{-m})\prod_{k\ne m}x^k(p^k)$ (35). A mixed Nash equilibrium (Definition 5.1.1) is a mixed profile with $u^m(x^m,x^{-m})\ge u^m(p^m,x^{-m})$ for every $m$ and $p^m\in E^m$. A probability distribution $x\in\Delta E$ on profiles is a correlated equilibrium (Definition 5.1.2) if $\sum_{p^{-m}}(u^m(p^m,p^{-m})-u^m(q^m,p^{-m}))\,x(p^m,p^{-m})\ge 0$ for all $m$ and $p^m,q^m$. The uniformly mixed strategy profile (Definition 5.2) has $x^m(q^m) = 1/h_m$ for every $m$ and $q^m$.

Formalization targets

Goal: Theorem 5.4

For every harmonic game $u\in\mathcal H\oplus\mathcal N$, the uniformly mixed strategy profile $x$ is a mixed Nash equilibrium:

Milestones

1. Lemma A.1: for every edge flow $\hat X$ and every set of profiles $\hat S$, $\sum_{p\in\hat S}(\delta_0^*\hat X)(p) = -\sum_{p\in\hat S}\sum_{q\in\hat S^c}\hat X(p,q)$.
2. Lemma 5.2: in a harmonic game, $\sum_{p^{-m}\in E^{-m}}\big(u^m(r^m,p^{-m}) - u^m(q^m,p^{-m})\big) = 0$ for all $m$ and $q^m, r^m$.
3. Proposition 5.2: in a normalized harmonic game, a distribution $x\in\Delta E$ is a correlated equilibrium iff all the inequalities of Definition 5.1.2 hold with equality (36), iff $\sum_{p^{-m}}u^m(q^m,p^{-m})\,x(p^m,p^{-m}) = 0$ for all $m,p^m,q^m$ (37).
4. Remark after Proposition 5.2: the equivalence of correlated equilibrium with (36) holds for all harmonic games.
5. Corollary 5.2: in a harmonic game, a mixed profile is a mixed Nash equilibrium iff $u^m(x^m,x^{-m}) = u^m(p^m,x^{-m})$ for all $m$ and $p^m$ (42).

Significance

Theorem 5.4 is the counterpart, for harmonic games, of the existence of pure equilibria in potential games. It exhibits an explicit equilibrium that does not depend on the payoffs at all, only on the strategy counts $h_m$. Corollary 5.2, a milestone here, adds that at any mixed equilibrium of a harmonic game every player is indifferent among all its pure strategies, including those outside the support. That is much stronger than the usual support condition. Proposition 5.2 shows that the correlated equilibria of a normalized harmonic game are the points of the probability simplex in a linear subspace determined by the utilities. The paper uses that description in its later analysis of two-player harmonic games.

The results are proved in the paper; none of them is machine-checked. The formalization connects the paper's operator layer (flows on the game graph, the gradient and its adjoint with the $\tfrac12$-weighted inner product, pseudoinverses) with standard equilibrium notions on finite games. It reuses published definitions of lotteries, the mixed extension and correlated equilibria.

Difficulty

The equilibrium statement follows quickly once Lemma 5.2 is available. The difficulty lies in translating the harmonic condition, a statement about the adjoint of an operator on edge flows, into an identity about payoffs. That needs the explicit form of $\delta_0^*$, which depends on the $\tfrac12$ in the inner product of $C_1$. It also needs the fact that $D$ kills the nonstrategic component, and a computation of the flow of $Du$ across the boundary of the set of profiles in which player $m$ plays $r^m$. Corollary 5.2 needs the passage from mixed profiles to product distributions on profiles and a careful accounting of sums over $p^{-m}$ against sums over full profiles.

The first idea, to use the normalization $\sum_{q^m}u^m(q^m,p^{-m}) = 0$, is not available. The goal concerns all harmonic games, not only normalized ones, and normalization alone does not give indifference against uniform opponents: the harmonic condition is essential.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ($E^m = \{1,\dots,h_m\}$). The hypothesis [∀ m, Nonempty (E m)] is stated explicitly on the game theorems, because the uniform profile $1/h_m$ is a probability vector only if $h_m\ge1$. A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)) with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly. $\mathcal H$ and $\mathcal N$ are defined by (28), and harmonic games are the submodule H ⊔ N. Lotteries, mixed profiles and the mixed extension (34) come from the published agt_games definitions; correlated equilibrium is the published HartSchmeidler.Finite.IsCorrelatedEq. The pure-deviation payoff (35), mixed Nash equilibrium with pure deviations (Definition 5.1.1, as printed), and the uniform profile are defined in the mission. Sums over $p^{-m}$ are written as sums over the profiles with player $m$'s strategy fixed, so each $p^{-m}$ is counted once.

The goal concerns mixed Nash equilibria. Stating it for the uniform product distribution as a correlated equilibrium, or for normalized games only, would be a weaker statement and is not the target. No hypothesis is added beyond the nonemptiness of the strategy sets.

Contributions welcome: proofs of the milestones, and general lemmas on adjoints of graph gradients and on product distributions that are reusable beyond this mission.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3), 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14, 1996. https://doi.org/10.1006/game.1996.0044
• S. Hart, D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 1989. https://doi.org/10.1287/moor.14.1.18

Motivation

Finite games in strategic form are the basic model of interaction between self-interested agents in economics, engineering and computer science. Among them, potential games (Monderer and Shapley, 1996) are the class with the most tractable equilibrium behaviour: every finite potential game has a pure Nash equilibrium, and simple learning dynamics such as best response and fictitious play converge to one. A natural question is what lies at the opposite end of the space of games, and how far a general game is from that tractable class.

Candogan, Menache, Ozdaglar and Parrilo (arXiv:1005.2405; Mathematics of Operations Research 36(3), 2011, DOI 10.1287/moor.1110.0500) answer this with a canonical decomposition of every finite game into a potential, a harmonic and a nonstrategic component, obtained by viewing the payoff differences of a game as a flow on a graph and applying the combinatorial Helmholtz decomposition. Harmonic games, those whose potential component vanishes, are the complement of potential games, and the paper shows that their equilibrium behaviour is opposite as well. This mission formalizes the first such result: harmonic games generically have no pure Nash equilibrium, so the guaranteed existence of pure equilibria in potential games has no counterpart on the harmonic side. The decomposition has since been used to study near-potential games and the convergence of learning dynamics in them.

Setting

A finite game has a finite set of players $\mathcal M$ with $M = |\mathcal M|$ and, for each player $m$, a nonempty finite strategy set $E^m$ with $h_m = |E^m|$ elements. A strategy profile is $p = (p^m)_m \in E = \prod_m E^m$, and $(q^m, p^{-m})$ denotes $p$ with player $m$'s strategy replaced by $q^m$. The utilities $u = (u^m)_m$ assign to each player a function $u^m : E \to \mathbb R$; for fixed $\mathcal M$ and $E$ a game is identified with its utilities, an element of $C_0^M$, where $C_0 = \{f : E \to \mathbb R\}$ carries the inner product $\langle \varphi_1,\varphi_2\rangle_0 = \sum_p \varphi_1(p)\varphi_2(p)$.

A profile $p$ is a pure Nash equilibrium if $u^m(p^m, p^{-m}) \ge u^m(q^m, p^{-m})$ for every player $m$ and every $q^m \in E^m$.

Two profiles are $m$-comparable if they are distinct and differ only in player $m$'s strategy. The game graph has the profiles as nodes and joins every comparable pair. An edge flow is a function $X$ on ordered pairs of profiles with $X(p,q) = -X(q,p)$ on edges and $X = 0$ off edges; the space $C_1$ of edge flows carries $\langle X,Y\rangle_1 = \tfrac12\sum_{(p,q)\in A} X(p,q)Y(p,q)$. The combinatorial gradient is $(\delta_0\varphi)(p,q) = W(p,q)(\varphi(q)-\varphi(p))$, with $W$ the edge indicator, and $\delta_0^*$ is its adjoint. Restricting to $m$-comparable pairs gives $D_m : C_0 \to C_1$, and $D u = \sum_m D_m u^m$ is the flow of payoff differences of the game $u$. With $\Pi_m = D_m^\dagger D_m$ (Moore–Penrose pseudoinverse) and $\Pi = \operatorname{diag}(\Pi_1,\dots,\Pi_M)$, the paper's Definition 4.2 sets

A game is a harmonic game if $u \in \mathcal H \oplus \mathcal N$: its payoff differences form a flow with no source or sink at any profile.

Formalization targets

Goal: Proposition 5.1

For finite games in which at least two players have at least two strategies each, and for any additive Haar measure $\mu$ on the finite-dimensional space $\mathcal H \oplus \mathcal N$,

This is the paper's "harmonic games generically do not have pure Nash equilibria", with "generically" read as the paper defines it: true except on a set of measure zero within the harmonic games.

Stronger structural form

For each profile $p$, the harmonic games having $p$ as a pure Nash equilibrium form a proper linear subspace of $\mathcal H \oplus \mathcal N$. The exceptional set of the goal is then a finite union of lower-dimensional subspaces.

Milestones

1. Lemma 5.1: at a pure Nash equilibrium of a harmonic game, every player is indifferent among all of their strategies.
2. Proposition 4.1: $\dim\mathcal P = \prod_m h_m - 1$, $\dim\mathcal H = (M-1)\prod_m h_m - \sum_m\prod_{k\ne m}h_k + 1$, $\dim\mathcal N = \sum_m\prod_{k\ne m}h_k$.

Significance

The result separates harmonic games sharply from potential games. A finite potential game always has a pure equilibrium; a harmonic game almost never has one. Together with the decomposition theorem, it says that the obstruction to pure equilibria in a general game is carried by its harmonic component, and it motivates the paper's later results on mixed equilibria of harmonic games (the uniformly mixed profile is always a mixed equilibrium). Proposition 4.1, a milestone here, also gives the dimension of the harmonic games, $(M-1)\prod_m h_m + 1$, and so measures how large that class is.

The results are proved in the paper; none of them is machine-checked. Formalizing them requires the paper's operator layer (flows on the game graph, the gradient with its adjoint, pseudoinverses) in Lean for the first time, and pins down two points the paper leaves informal: the measure with respect to which "generically" is meant, and the shape condition on the game under which the statement holds.

Difficulty

Lemma 5.1 is a short counting argument once the divergence-free condition $\delta_0^* D u = 0$ is unpacked, but unpacking it requires knowing that $D$ kills $\mathcal N$ and computing $\delta_0^*$ from the $\tfrac12$-weighted inner product. The main obstacle of the goal is showing that the exceptional subspaces are proper. The proof needs a harmonic game with nonzero payoff differences, that is $\dim\mathcal H > 0$, and the only route the paper offers is the dimension count of Proposition 4.1. That count rests on the full decomposition $C_0^M = \mathcal P\oplus\mathcal H\oplus\mathcal N$, on the kernel of each $D_m$ and on the connectivity of the game graph, all of which must be built in Lean. The measure-theoretic last step, that a finite union of proper subspaces is Haar-null, is in Mathlib.

A tempting shortcut fails: placing Lebesgue measure on all of $C_0^M$ and observing that $\mathcal H \oplus \mathcal N$ is a proper subspace would prove the goal without saying anything about equilibria.

Formalization scope

Players form a finite type ι with decidable equality, and the strategy sets E m are nonempty finite types, as in the paper ($E^m = \{1,\dots,h_m\}$). A game is an element of PiLp 2 (fun _ => EuclideanSpace ℝ (∀ k, E k)), with the unweighted sum inner product of p. 14. $C_1$ is the subspace of edge flows with the inner product $\tfrac12\sum$ of (7). $\delta_0^*$ is Mathlib's adjoint, and the pseudoinverse is defined directly as the inverse of $L$ on $(\ker L)^\perp$ composed with the orthogonal projection onto $\operatorname{im} L$. $\mathcal P,\mathcal H,\mathcal N$ are defined by (28), not by the alternative description (29). Harmonic games are the submodule H ⊔ N, and pure Nash equilibrium is AGT.IsPureNash from the published agt_games definitions.

Added hypothesis. The paper leaves implicit that at least two distinct players have at least two strategies each. Its proof uses this through "dimension of $\mathcal H$ is larger than zero". Without it Proposition 5.1 is false: with two players having $1$ and $h$ strategies, $\dim\mathcal H = (2-1)h - (h+1) + 1 = 0$, every harmonic game is nonstrategic, and every profile is a pure equilibrium of every harmonic game. The goal and the structural theorem therefore carry this hypothesis explicitly.

The measure. The measure is an arbitrary additive Haar measure on the subspace $\mathcal H\oplus\mathcal N$ itself, with the Borel σ-algebra of its subspace topology. A measure on the ambient $C_0^M$ would make the statement trivial, because the whole subspace is null there. Proposition 4.1 is stated as equalities in $\mathbb Z$, so that $M-1$ and the subtraction in part 2 are not truncated.

Needed infrastructure: kernels of the $D_m$ (the paper's Lemma 4.2), the projection property of $D^\dagger D$, the decomposition theorem, and the connectivity of the game graph. The operator layer is shared with the other missions of this series and is reusable for any work on flows on graphs. Proofs of the milestones, and of the structural form independently of the goal, are welcome.

Selected references

• O. Candogan, I. Menache, A. Ozdaglar, P. A. Parrilo, Flows and Decompositions of Games: Harmonic and Potential Games, arXiv:1005.2405v2, 2010; Mathematics of Operations Research 36(3):474–503, 2011. https://arxiv.org/abs/1005.2405, https://doi.org/10.1287/moor.1110.0500
• D. Monderer, L. S. Shapley, Potential Games, Games and Economic Behavior 14(1):124–143, 1996. https://doi.org/10.1006/game.1996.0044
• X. Jiang, L.-H. Lim, Y. Yao, Y. Ye, Statistical ranking and combinatorial Hodge theory, Mathematical Programming 127(1):203–244, 2011. https://doi.org/10.1007/s10107-010-0419-x

Motivation

In a road or communication network, traffic is routed by its users, not by a central planner. Each user picks the route that is cheapest for itself, and the resulting equilibrium can be much more expensive for the network as a whole than the best centrally planned routing. Roughgarden and Tardos, How Bad is Selfish Routing? (J. ACM 2002), quantified this loss. Their basic model is nonatomic: infinitely many users, each controlling a negligible amount of traffic. There, the cost of a Nash flow can exceed the optimum by an unbounded factor, but it never exceeds the cost of an optimal flow that routes twice as much traffic (their Theorem 3.1).

Many networks are not like that. A few large operators (internet service providers, freight companies, a navigation app routing its whole user base) each control a strictly positive share of the traffic and can split it over many paths. Section 5.2 of the paper treats this finite splittable model and proves the analogue of the bicriteria bound, Theorem 5.4. This mission formalizes that theorem and the three steps of its proof.

Setting

A network has a finite set $E$ of edges. Each edge $e$ carries a latency function $\ell_e$, nonnegative, nondecreasing and continuous on $[0,\infty)$: the delay on $e$ when $x$ units of flow use it is $\ell_e(x)$.

There are $k$ agents. Agent $i$ must send $r_i>0$ units of flow from a source $s_i$ to a destination $t_i$, over its set $\mathcal P_i$ of paths. Distinct agents may have the same source and destination; their path sets are then separate copies. A flow $f$ assigns a nonnegative amount $f_P$ to each path; agent $i$'s part is $f^{(i)}$, the restriction of $f$ to $\mathcal P_i$. The flow is feasible for the rates $r$ if $\sum_{P\in\mathcal P_i} f_P = r_i$ for every $i$, and feasible for $2r$ if each agent instead sends $2r_i$.

The edge flow $f_e=\sum_{P\ni e} f_P$ is the flow of all agents through $e$. The latency of a path is $\ell_P(f)=\sum_{e\in P}\ell_e(f_e)$, and

are the cost of the flow (its total latency) and the cost of agent $i$. A feasible flow $f$ is at Nash equilibrium if no agent can lower its own cost by rerouting its own flow: for each $i$, $f^{(i)}$ minimizes $C_i$ given $f^{(j)}$ for $j\neq i$.

In Lean, edges, paths and agents are Fin J, Fin R and Fin Sd; a path is a $0/1$ incidence column A j r, s r is the agent owning path r, and rate i is $r_i$. The edge flow linkFlow and the feasible set wardropFeasible come from the published definition KellyStochasticNetworks_Wardrop; pathLatency, cost and the modified latencies barLatency come from the series' shared model definitions (SelfishRouting.Bicriteria), and agentCost and IsSplittableNash are defined in this mission.

Formalization targets

Goal: Theorem 5.4 (p. 20)

If $x\cdot\ell_e(x)$ is convex on $[0,\infty)$ for every edge, $f$ is at Nash equilibrium for the finite splittable instance $(G,r,\ell)$, and $f^*$ is feasible for $(G,2r,\ell)$, then