Motivation

The strategic-form game is the basic object of noncooperative game theory, and the Nash equilibrium — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium (Nash, Non-cooperative games, Ann. Math. 54 (1951)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).

A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.

Setting

A finite strategic-form game consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of pure strategies, and for each player a payoff function $u_i : \prod_j S_j \to \mathbb{R}$; all players are utility maximizers. A mixed strategy for player $i$ is a probability distribution on $S_i$, represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a lottery). Players randomize independently, so a mixed profile $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$'s expected payoff is

$$U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).$$

A mixed profile $\sigma$ is a (mixed) Nash equilibrium if for every player $i$ and every lottery $\tau$ on $S_i$, replacing $\sigma_i$ by $\tau$ does not increase $U_i$.

A two-person zero-sum game is given by a matrix $A \in \mathbb{R}^{m \times n}$: the row player picks a row distribution $p$, the column player a column distribution $q$, and the column player pays the row player $p^{\mathsf T} A q$ in expectation.

The market of §1.8.1 of the source has finitely many divisible goods, good $a$ in $s_a$ units, and finitely many buyers, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. Market-clearing prices are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.

Formalization targets

Goal (capstone) — Theorem 1.8

$$\text{Every finite strategic-form game has a mixed Nash equilibrium.}$$

Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.

Supporting — Brouwer fixed-point theorem

$$K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.$$

Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.

Theorem 1.11 — zero-sum games

$$\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}$$

of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.

Theorem 1.17 (existence form)

$$\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}$$

The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.

Significance

The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (IsLottery, IsMixedProfile, expectedPayoff, IsMixedNash) from this mission.

Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.

Difficulty

The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.

Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (Mathlib.Topology.Sion) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.

Formalization scope

Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$; mixed strategies are weight functions with a IsLottery predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (Fin (m+1), Fin (n+1)), payoffs flow from the column player to the row player, stdSimplex plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by matrixGameStrat/zeroSumPayoff/matrixGameProfile from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.

Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).

Selected references

• J. F. Nash, Non-cooperative games, Annals of Mathematics 54 (1951), 286–295. DOI
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928), 295–320. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. DOI
• C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The complexity of computing a Nash equilibrium, SIAM J. Computing 39 (2009), 195–259. DOI