feat: add Nash equilibrium existence theorem eval problem

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

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."