Game Theory Formalization in Lean

This repository contains a formalization of fundamental theorems in game theory using the Lean proof assistant. The main goal is to prove the existence of Nash Equilibria in finite games.

Core Concepts and Theorems

The proof of Nash's theorem relies on Brouwer's fixed-point theorem. This repository builds up the necessary mathematical framework from scratch.

Files

• Gametheory/Simplex.lean: Defines the standard simplex stdSimplex over a finite type. Includes constructors like pure, evaluation lemmas (pure_eval_eq, pure_eval_neq), and weighted-sum/typeclass instances needed later for continuity/compactness arguments.

• Gametheory/Scarf.lean: Develops the combinatorial framework culminating in Scarf. Constructs the combinatorial objects (triangulations/labelings in the formalized guise) and proves existence of a "colorful" simplex, which is used to derive fixed points.

• Gametheory/Brouwer.lean: From Scarf’s combinatorial lemma, proves Brouwer’s fixed-point theorem on a single simplex. Contains the main theorem Brouwer (existence of a fixed point for continuous self-maps on a simplex) and the supporting analytical lemmas (compactness, coordinate-wise continuity, convergence of constructed sequences).

• Gametheory/Brouwer_product.lean: Lifts the single-simplex result to finite products of simplices. Defines helper conversions between a big simplex and a product of simplices (BigSimplex, ProductSimplices), constructs the projection/embedding, proves continuity properties, and states the product fixed-point theorem Brouwer_Product.

• Gametheory/Nash.lean: Formalizes finite games FinGame, mixed strategies mixedS, payoffs, and mixed Nash equilibrium mixedNashEquilibrium. Builds a continuous nash_map on the product of simplices and applies Brouwer_Product to obtain existence: ExistsNashEq : ∃ σ : G.mixedS, mixedNashEquilibrium σ.

• GameTheory.lean: Umbrella file that imports Brouwer, Nash, and Simplex for convenience.

• Open any of the Lean files in an editor with the Lean server running to see goals and check proofs interactively.

Notation and Key Definitions

• stdSimplex ℝ α: the standard simplex over a finite type α with real coefficients.
• Brouwer_Product: theorem providing a fixed point on a finite product of simplices.
• FinGame: structure for finite games (finite players and finite pure strategy sets).
• mixedS: type of mixed strategy profiles for a FinGame.
• mixedNashEquilibrium σ: predicate that σ : G.mixedS is a mixed Nash equilibrium.
• ExistsNashEq: existence theorem for mixed Nash equilibria.

References

• N. V. Ivanov, "Beyond Sperner's Lemma" (source of the Scarf → Brouwer development).
• J. F. Nash, "Non-Cooperative Games", Annals of Mathematics (1951).