Game Theory in Lean4

A Lean 4 library for finite and discrete game theory, built on Mathlib. Static and sequential games share one semantic core: a single deviation API carries Nash, correlated, Bayesian, and refinement results; the language encodings compile into that core; and the executable algorithms are tied to their specifications by correctness theorems. An optional complexity package proves NP- and PPAD-completeness results for explicit game and fixed-point encodings.

Getting started

GameTheory follows Mathlib releases. The Lean toolchain it builds with is in lean-toolchain, and the Mathlib revision is in lakefile.lean. Use the same toolchain in your project, and match any Mathlib requirement you declare yourself to GameTheory's.

Add the library to your lakefile.lean. Pin it to a release tag or a commit. Release tags are named after the Lean version they build with.

require "elazarg" / "GameTheory" @ git "<tag-or-commit>"

Then fetch the dependencies and the prebuilt Mathlib cache, and build:

lake update
lake exe cache get
lake build

Lake also fetches the other dependencies, including the fixed-point theorem library used by GameTheory.Analysis.

import GameTheory gives the static, sequential, epistemic, evolutionary, and executable foundations. Everything else is an explicit import, which keeps each family's assumptions out of the basic one:

GameTheory.Math is its own Lake target and stands alone, without any game definitions:

import GameTheory.Math.Probability.Bounds

open GameTheory.Math.Probability

#check eventMass_toReal_le_expect_div

Examples

The examples are executable documentation. The classic finite games connect a table frontend to the semantic equilibrium predicates:

import GameTheory.Examples.Classic

open GameTheory GameTheory.Examples

#check prisonersDilemma_bothDefect_isNash
#check matchingPennies_noPureNash

Good entry points:

• Examples/Classic.lean — Prisoner's Dilemma, Matching Pennies, Battle of the Sexes, and a potential game;
• Examples/NFG.lean — a countably infinite action carrier, handled without enumeration;
• Examples/StochasticUniform.lean — a nonconstant finite stochastic payoff and its uniform bound;
• Tests/StochasticContinuation.lean — chronological histories, continuation, and restart;
• Tests/Bayesian.lean — direct Bayesian and protocol-form Nash agreeing.

The capability matrix indexes the public workflows with their exact imports and compiled consumers.

Computational complexity

The separate GameTheoryComplexity package provides machine-checked complexity classifications:

These results include polynomial-time verifier and reduction machines. Search reductions decode every accepted target answer; exact rational Nash certificates are connected to the library's mixed-equilibrium semantics.

Add the optional package to your lakefile.lean, pinning a commit containing it:

require GameTheoryComplexity from git
  "https://github.com/elazarg/GameTheory" @ "<extension-commit>" / "extensions/complexity"

Then import the result you need:

import GameTheoryComplexity.BimatrixNash

#check GameTheory.Complexity.bimatrixNashRelation_PPADComplete

ComplexityLib and CSLib dependencies belong to this optional package; base GameTheory clients do not fetch them. The package README documents the precise encodings, dependency pins, and further probability and machine-composition APIs. The computational roadmap tracks remaining results.

Organization

GameTheory.Math owns the reusable mathematics, including products, conditioning, and guarded expectation for ordinary Mathlib PMF laws. GameTheory.Core owns static forms, utility, deviations, preferences, and solution concepts. GameTheory.Protocol owns the single execution and behavioral-policy semantics the sequential languages share. GameTheory.Analysis owns analytic existence and convergence arguments and is the only root allowed to import the external fixed-point library. Architecture audits check these project dependency boundaries.

Assumptions sit on the theorem or operation that needs them: finite support, finite player/action carriers, and payoff integrability are requested locally. Executable modules use explicit enumerations and computable scalars; correctness modules connect them to the real-valued semantics.

Scope

Discrete semantics uses PMF on arbitrary carriers; each law may have countably infinite support. Expected-utility comparisons use the extended-real expectation, so a law with infinite expected gains or losses is worth +∞ or −∞ and is compared like any other. Only a law whose gains and losses are both infinite has no expectation; such an alternative fails its equilibrium comparison, rather than disappearing from the deviation quantifier. Theorems that compute with real expected utilities request integrability of the laws they compute with; finite support and bounded payoffs are sufficient ways to discharge it.

Ordinary measures represent infinite policy products and arbitrary independent per-player policy laws, with exact finite-prefix behavioral correspondences. General measurable games and infinite-play outcome laws are outside the core; focused experiments with infinite-play laws live under GameTheory.Experimental.

The delivery ledger lists theorem families that are partial or planned.

Development

lake build      # library, examples, tests, and experiments, warnings as errors
lake lint       # Batteries environment linters over the public library
pwsh -NoProfile -File scripts/phase1-audit.ps1 -VerifyExpected
pwsh -NoProfile -File scripts/phase2-audit.ps1 -VerifyExpected
pwsh -NoProfile -File scripts/phase3-audit.ps1 -VerifyExpected

Before tagging a release, set the package version in lakefile.lean to the tag's version number (without the v prefix).

Architecture and contribution rules live in docs/GameTheory2Design.md and AGENTS.md. The predecessor library is at tag v1-final, with its workflows mapped in the v1 capability map.

Licensed under the Apache License 2.0.