Nash equilibrium existence theorem

nash_equilibrium_exists

Submitter: Kim Morrison.

Notes: §33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (the section's boxed main theorem). Every finite n-player game in mixed strategies admits at least one Nash equilibrium. Mathlib has stdSimplex ℝ S (the natural model of a mixed strategy) and finite-sum/product machinery but no game theory at all — no Mathlib/GameTheory/ module, and grep for nash/mixed.strategy/best.response returns nothing relevant. No formalization of Nash equilibrium existence was found in any major proof assistant.

Source: J. F. Nash, Equilibrium points in n-person games, Proc. Nat. Acad. Sci. U.S.A. 36 (1950), 48-49; Non-cooperative games, Ann. of Math. 54 (1951), 286-295. Listed as §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Nash's 1950 proof (via Brouwer): define the best-response function r : Δ → Δ on the product of mixed-strategy simplices Δ = ∏ᵢ Δ(Sᵢ), where r(σ)ᵢ(sᵢ) = (σᵢ(sᵢ) + max(0, gain_i(σ, sᵢ))) / (normalization), and gain_i(σ, sᵢ) is the improvement player i would get by playing the pure strategy sᵢ against σ_{-i}. r is continuous and Δ is nonempty compact convex; Brouwer gives a fixed point σ*, and a short calculation shows σ* must be a Nash equilibrium (the only fixed points of r are exactly the equilibria). Nash's 1951 proof uses Kakutani directly: the best-response correspondence (set-valued, not single-valued) is upper-hemicontinuous with nonempty convex values; apply Kakutani to get a fixed point.

theorem declaration uses `sorry`nash_equilibrium_exists {n : ℕ} {S : Fin n → Type*}
    [∀ i, Fintype (S i)] [∀ i, Nonempty (S i)]
    (u : Fin n → LeanEval.GameTheory.StrategyProfile n S → ℝ) :
    ∃ σ : ∀ i, S i → ℝ, LeanEval.GameTheory.IsNashEquilibrium u σ := byn:ℕS:Fin n → Type u_1inst✝¹:(i : Fin n) → Fintype (S i)inst✝:∀ (i : Fin n), Nonempty (S i)u:Fin n → StrategyProfile n S → ℝ⊢ ∃ σ, IsNashEquilibrium u σ
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 25, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 29, 2026