From 4433e375ecb58fb1604f4074df9a5027518e1dff Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 21 May 2026 17:37:29 +0000 Subject: [PATCH] feat: add Nash equilibrium existence theorem eval problem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds Nash equilibrium existence (§33 of Knill's "Some Fundamental Theorems in Mathematics", the section's boxed main theorem) as a new eval problem: every finite n-player game in mixed strategies admits at least one Nash equilibrium. Mathlib has the standard simplex and finite-sum/product machinery but no game theory at all (no Mathlib/GameTheory/ module); no formalization of Nash equilibrium existence was found in any major proof assistant. Co-Authored-By: Claude Opus 4.7 (1M context) --- LeanEval/GameTheory/Nash.lean | 65 +++++++++++++++++++++++++++++++++++ manifests/problems.toml | 11 ++++++ 2 files changed, 76 insertions(+) create mode 100644 LeanEval/GameTheory/Nash.lean diff --git a/LeanEval/GameTheory/Nash.lean b/LeanEval/GameTheory/Nash.lean new file mode 100644 index 0000000..27ae547 --- /dev/null +++ b/LeanEval/GameTheory/Nash.lean @@ -0,0 +1,65 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace GameTheory + +/-! +# Nash equilibrium existence theorem + +§33 of Oliver Knill's *Some Fundamental Theorems in Mathematics*. Every +finite `n`-player game in mixed strategies admits at least one Nash +equilibrium. + +Nash gave two proofs: the 1950 one uses Brouwer's fixed-point theorem; the +1951 one uses Kakutani's set-valued generalization. + +mathlib has `stdSimplex ℝ S` (the natural model of a mixed strategy) and the +standard finite-sum/product machinery, but **no game theory at all** — +there is no `Mathlib/GameTheory/` module, and `grep -ri nash`, +`mixed.strategy`, `best.response` returns nothing relevant. No formalization +of Nash equilibrium existence was found in any major proof assistant. +-/ + +open Set Function + +/-- A **mixed strategy** for a player with finite pure-strategy set `S` is a +probability distribution on `S`: a non-negative function summing to `1`. -/ +abbrev MixedStrategy (S : Type*) [Fintype S] : Set (S → ℝ) := stdSimplex ℝ S + +/-- A **strategy profile** is a tuple assigning each of the `n` players a +pure strategy from their own set. -/ +abbrev StrategyProfile (n : ℕ) (S : Fin n → Type*) : Type _ := ∀ i, S i + +/-- The **expected payoff** to a player with payoff function `u` when each +player `j` plays the mixed strategy `σ j`. Sum over all pure-strategy +profiles, weighted by the product of marginal probabilities. -/ +noncomputable def expectedPayoff {n : ℕ} {S : Fin n → Type*} + [∀ i, Fintype (S i)] + (u : StrategyProfile n S → ℝ) (σ : ∀ i, S i → ℝ) : ℝ := + ∑ s : StrategyProfile n S, (∏ i, σ i (s i)) * u s + +/-- A profile of mixed strategies `σ` is a **Nash equilibrium** for the +payoff functions `u₀, …, uₙ₋₁` if (i) each `σ i` is a probability +distribution on `S i`, and (ii) no player `i` can strictly improve their +expected payoff by switching to a different mixed strategy `τ`, holding the +other players' strategies fixed. -/ +def IsNashEquilibrium {n : ℕ} {S : Fin n → Type*} [∀ i, Fintype (S i)] + (u : Fin n → StrategyProfile n S → ℝ) (σ : ∀ i, S i → ℝ) : Prop := + (∀ i, σ i ∈ MixedStrategy (S i)) ∧ + ∀ (i : Fin n) (τ : S i → ℝ), τ ∈ MixedStrategy (S i) → + expectedPayoff (u i) (Function.update σ i τ) ≤ + expectedPayoff (u i) σ + +/-- **Nash equilibrium existence theorem.** Every finite `n`-player game +with nonempty finite pure-strategy sets and arbitrary real payoffs admits +at least one mixed-strategy Nash equilibrium. -/ +@[eval_problem] +theorem nash_equilibrium_exists {n : ℕ} {S : Fin n → Type*} + [∀ i, Fintype (S i)] [∀ i, Nonempty (S i)] + (u : Fin n → StrategyProfile n S → ℝ) : + ∃ σ : ∀ i, S i → ℝ, IsNashEquilibrium u σ := by + sorry + +end GameTheory +end LeanEval diff --git a/manifests/problems.toml b/manifests/problems.toml index b9e42d1..e8223ed 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization" holes = ["uniformization"] submitter = "Junyan Xu" source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1." + +[[problem]] +id = "nash_equilibrium_exists" +title = "Nash equilibrium existence theorem" +test = false +module = "LeanEval.GameTheory.Nash" +holes = ["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."