Skip to content

Nash's existence theorem

Every finite game has a Nash equilibrium in mixed strategies. This is the theorem most game theorists would name first, and these notes deliberately stop short of it. In this page we examine what a formal proof requires, and why the answer makes it a poor destination for a first encounter with Lean.

What the capstone did not need

The theorem of chapter 6 holds for any type of strategies and any payoff function, because its proof uses nothing but the two definitions and the fact that a strict inequality or an equality implies a weak one. That generality is also a limitation. It says that stable strategies are equilibria, but it says nothing about whether any equilibrium exists, and existence is where the mathematics becomes heavy.

The ingredients

Nash gave two proofs, one in 1950 using Kakutani's fixed point theorem and one in 1951 using Brouwer's. Formalising either needs four ingredients, and only the first is readily available.

The first is the space of mixed strategies. Mathlib provides the standard simplex:

stdSimplex : (𝕜 : Type u_2) → (ι : Type u_1) → [Semiring 𝕜] → [PartialOrder 𝕜] → [Fintype ι] → Set (ι → 𝕜)

A mixed strategy over a finite set of actions ι is then a function from actions to probabilities, lying in this set. Note that it is a Set, not a type, so a mixed strategy is a function together with a proof that it belongs to the simplex, and every definition built on top has to carry that proof along.

The second is expected payoff: a finite sum over action profiles, weighted by the product of each player's probabilities. It is multilinear, and the proof needs it to be continuous. Both facts are routine on paper and each takes real work in Lean.

The third is the best-response correspondence, which maps a profile to the set of profiles in which every player best responds. Kakutani's theorem needs its values to be nonempty and convex and its graph to be closed.

The fourth is the fixed point theorem itself, and here the path runs out. Mathlib, at the version these notes use, contains neither Brouwer's nor Kakutani's theorem. It has the contraction mapping theorem and the intermediate value theorem, which is the one-dimensional case of Brouwer, but the general result needs either algebraic topology or a combinatorial argument, such as Sperner's lemma or Scarf's theorem, and it has not yet been added.

Two formal proofs

Both of Nash's proofs now have independent Lean formalisations outside Mathlib. They take different routes to the fixed point, and comparing them shows how much of the work lies in choices of generality.

Through Kakutani

The elazarg/GameTheory library proves the theorem as exists_isNash_mixed, following the 1950 proof. It takes Kakutani's theorem from elazarg/fixed-point-theorems-lean4, which is a fork of harfe/fixed-point-theorems-lean4. There it is stated as:

theorem kakutani_fixed_point {V : Type*}
    [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    (s : Set V) (hcvx : Convex ℝ s) (hcmpct : IsCompact s) (hne : Set.Nonempty s)
    (f : s → Set V) (hcg : closedGraph f)
    (h1 : ∀ x, f x ⊆ s ∧ Convex ℝ (f x) ∧ (f x).Nonempty)
    : ∃ x : s, x.1 ∈ f x := by {

Read as a game theorist would, this is the textbook statement: a nonempty, compact, convex subset of a finite-dimensional real vector space, and a correspondence on it with a closed graph whose values are nonempty convex subsets, has a fixed point. Every hypothesis in the textbook appears as an argument, and the proof of Nash's theorem consists of supplying each one for the best-response correspondence.

The fixed point package proves a cubical version of Sperner's lemma, derives Brouwer's theorem from it for any compact convex set in a finite-dimensional space, and derives Kakutani's theorem from Brouwer's, in 3,275 lines of Lean. Turning Kakutani into Nash's theorem takes a further 341 lines in the library.

Through Scarf and Brouwer

Lyu and Li, of Xiamen University Malaysia, presented a second route at the AI for Math workshop of ICML 2026. Their formalisation starts from Scarf's theorem, in the indexed-order formulation of Ivanov, and proves it by a parity argument on an incidence structure of rooms and doors. Applying it to finite grids on the standard simplex and passing to the limit by compactness and continuity gives Brouwer's theorem for the simplex. An explicit embedding and projection extends this to finite products of simplices, which is exactly the space of mixed strategy profiles, and Nash's 1951 argument through the Nash map then gives existence.

The result is stated for finite games, with mixed strategies built from the same stdSimplex that Mathlib provides. The definition of equilibrium reads very close to the textbook one:

def mixedNashEquilibrium {G: FinGame} (x : G.mixedS) :=
  ∀ (i:G.I), ∀ (y : S (G.SS  i)),
     G.mixed_g i x ≥ G.mixed_g i (update  x i y)

For every player i and every mixed strategy y of that player, the expected payoff mixed_g i at the profile x is at least the payoff when i alone switches to y, which is what update x i y expresses. The theorem itself is ExistsNashEq : ∃ σ : G.mixedS , mixedNashEquilibrium σ. The repository also contains a file that runs #print axioms on every principal result each time it is built, the check described in Computation and the real numbers.

The paper reports 4,768 lines of Lean across five files, built with Lean 4.22.0. The maintained repository, math-xmum/Brouwer, has since grown to 7,840 lines and moved to Lean 4.33.0. As a by-product the authors also derive BrouwerBench, an 80-item benchmark for testing whether automated systems understand the structure of the proof.

The two compared

The two developments make opposite choices of generality. The first proves Brouwer's and Kakutani's theorems for any compact convex set and then specialises them to the game. The second proves Brouwer's theorem only for the simplex and its products, which is all that Nash's theorem needs, and never proves Kakutani's at all. This is the trade-off discussed in Definitions and proofs at a larger scale: a general statement serves more users, while a specialised one follows the argument the reader already has in mind.

The sizes are instructive either way. Both routes run to thousands of lines, almost all of them before a game is mentioned. The capstone of these notes is six.

Why these notes stop short

Almost none of those lines are game theory. They are convex analysis, topology and combinatorics, needed because the existence proof rests on a deep fact about the geometry of the simplex rather than on anything about incentives. A reader working through them would learn a great deal of Lean, but would learn it through problems that have little to do with the reason they came.

ESS implies Nash has the opposite profile. Its proof is short, its ideas are game-theoretic, and each step of the Lean proof matches a step of the argument on paper. That makes it the right place to learn the tools. Having learnt them, a reader who wants existence knows where to find it, and can read exists_isNash_mixed or ExistsNashEq as a sequence of recognisable steps rather than as an opaque wall of code.

With two independent developments now available, whether Brouwer's and Kakutani's theorems should enter Mathlib itself, and in what generality, is a natural open question for the community.

References

The formalisations discussed on this page are the following. All three repositories are still changing, so each is cited by commit, the identifier git gives to one saved version of a project; the links show the code exactly as it stood when we read it in September 2026, and the figures on this page refer to those versions.