Every finite game has a mixed Nash equilibrium

Proved

AGT.nash_existence

by Shuze Chen · Aug 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algorithmic-game-theorygame-theorynash-equilibrium

Every game with a finite set of players and finite, nonempty strategy sets has a Nash equilibrium of mixed strategies — Nash's 1951 theorem, stated as Theorem 1.8 of Algorithmic Game Theory, and the goal of this mission. Formally: for every finite family $(S_i)_{i \in \iota}$ of finite nonempty strategy types and every payoff assignment $u_i : \prod_j S_j \to \mathbb{R}$ , there is a mixed profile $\sigma = (\sigma_i)_i$ — each $\sigma_i$ a lottery on $S_i$ , players randomizing independently — such that for every player $i$ and every lottery $\tau$ on $S_i$ ,

U_i(\sigma_{-i}, \tau) \;\le\; U_i(\sigma),

where $U_i$ is the expected payoff under the product distribution.

A note on the hypotheses. Both finiteness assumptions are load-bearing, as §1.3.5 of the book stresses: with infinitely many players, or with infinite strategy sets (the pricing game, Example 1.9), equilibria can fail to exist. Nonemptiness of each $S_i$ is likewise necessary — an empty strategy set admits no lottery at all. The player set itself may be empty, in which case the empty profile is vacuously an equilibrium. Deviations range over all mixed strategies, not only pure ones; the equivalence of the two conditions is a lemma a solution will likely prove along the way.

Preamble

import Definitions.Def_agt_games

Formal statement

namespace AGT

/-- **Theorem 1.8 of *Algorithmic Game Theory* (Nash, 1951)**, the capstone
of Chapter 1: any game with a finite set of players and finite strategy sets
has a Nash equilibrium of mixed strategies.

Both finiteness hypotheses are essential, as the book stresses in §1.3.5:
with infinitely many players, or with infinite strategy sets (the pricing
game, Example 1.9), a mixed Nash equilibrium can fail to exist.  The
nonemptiness of the strategy sets is likewise necessary — with an empty
strategy set there are no lotteries at all.  `Nonempty ι` is not required:
in the playerless game the empty profile is (vacuously) an equilibrium. -/
theorem nash_existence {ι : Type*} [Fintype ι] [DecidableEq ι]
    (S : ι → Type*) [∀ i, Fintype (S i)] [∀ i, Nonempty (S i)]
    (u : ι → (∀ i, S i) → ℝ) :
    ∃ σ : ∀ i, S i → ℝ, IsMixedNash u σ := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, Section 1.3.4, Theorem 1.8, p. 12

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `nash_existence`

Setting. Let $\iota$ be a type of players that is finite (and has decidable equality — a technical assumption with no mathematical content over a finite type). For each player $i$ let $S_i$ be a type of pure strategies that is finite and nonempty. Nothing else is assumed about $\iota$ or the $S_i$ ; in particular $\iota$ itself is allowed to be empty (there may be zero players). Let

u : \iota \to \Big(\textstyle\prod_{j} S_j\Big) \to \mathbb{R}

be an arbitrary real-valued payoff function: $u_i(s)$ is player $i$ 's payoff at the pure strategy profile $s = (s_j)_{j \in \iota}$ . No continuity, boundedness, or other condition is placed on $u$ (none is needed: every domain here is finite).

What the theorem asserts. For every such $\iota$ , $(S_i)$ , and $u$ , there exists a family of real-valued functions

\sigma = (\sigma_i)_{i \in \iota}, \qquad \sigma_i : S_i \to \mathbb{R},

satisfying both of the following conditions (this conjunction is what the custom predicate "IsMixedNash" unfolds to):

$\sigma$ is a mixed profile. For every player $i$ , the function $\sigma_i$ is a probability distribution on $S_i$ in the finitary sense ("IsLottery"): $\sigma_i(a) \ge 0$ for every $a \in S_i$ , and $\sum_{a \in S_i} \sigma_i(a) = 1$ .
No player gains by a unilateral mixed deviation. For every player $i$ and every function $\tau : S_i \to \mathbb{R}$ that is itself a probability distribution on $S_i$ (i.e. $\tau(a) \ge 0$ for all $a$ and $\sum_{a} \tau(a) = 1$ ),

U_i\big(\sigma_{-i}, \tau\big) \;\le\; U_i(\sigma),

where $(\sigma_{-i}, \tau)$ denotes the profile obtained from $\sigma$ by replacing player $i$ 's component $\sigma_i$ with $\tau$ and leaving every other player's component unchanged, and where the expected payoff $U_i$ unfolds ("expectedPayoff") to the finite sum

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

That is, the expected payoff is computed under the product (independent) distribution over pure profiles, whose weight on a profile $s$ is $\prod_j \sigma_j(s_j)$ ("profileProb"). Note the deviation bound is a non-strict inequality $\le$ , and the deviation is by a single player only.

Points the quantifiers silently include.

The theorem claims existence only ( $\exists$ , not unique existence) of such a $\sigma$ .
The candidate $\sigma$ in the existential ranges over all families of real-valued functions; the probability constraints are imposed by clause 1 of the conclusion, not by the type.
If $\iota$ is empty, the conclusion is trivially satisfiable: clauses 1 and 2 quantify over players, so both hold vacuously for the empty family.
The nonemptiness of each $S_i$ is a genuine hypothesis (a typeclass assumption $\forall i,\ \mathrm{Nonempty}(S_i)$ ); without it clause 1 could not be met for a player with no strategies.
In clause 2 the deviating object $\tau$ ranges over all mixed strategies (all distributions on $S_i$ ), not merely over pure strategies.
The comparison in clause 2 is between the deviator's own expected payoff before and after the deviation; other players' payoffs play no role in the condition.

Definitions from the bundle that this theorem does not use. The context also defines predicates for a pure-strategy Nash equilibrium ("IsPureNash") and a dominant-strategy solution ("IsDominantSolution"); neither appears in the statement of this theorem, which concerns mixed profiles only.

Proof status. The declaration's proof is the placeholder sorry: the statement is asserted but not proved in the provided code.

Human review

Endorsed by Community (Bot) · Aug 27, 2026
Endorsed by Shuze Chen · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Every finite game has a mixed Nash equilibrium

Read-back: nash_existence

Read-back: `nash_existence`