Lean for Game Theorists¶

These notes teach the Lean theorem prover to readers who already know game theory. We assume that the reader is comfortable with normal-form games, mixed strategies, Nash equilibria and evolutionarily stable strategies, and has never written a line of Lean. Every Lean idea is earned as it appears; none of the game theory is explained.

The destination is a single theorem: an evolutionarily stable strategy is a symmetric Nash equilibrium. It is a result every game theorist already believes, and its proof is short enough to hold in mind, which makes it an honest place to find out what formalisation actually feels like.

The notes follow the Diátaxis split.

Tutorial¶

A single guided path from an empty directory to a proved theorem. This is the place to start, and it is meant to be followed in order, typing along the way.

How-to guides¶

Short answers to specific questions, for readers already comfortable with Lean: setting up an editor, encoding a new payoff matrix, reading an error message.

Reference¶

The definitions and lemmas these notes build, stated precisely and without commentary.

Explanation¶

Why formalisation behaves as it does. What Lean and Mathlib each are and where Lean came from, why decide fails on the reals, why definitions are harder than proofs, and where the road to Nash's existence theorem leads.

Versions¶

Everything here is built against Lean 4.33.1 and Mathlib v4.33.1. Both are pinned in the repository, and every Lean block on these pages is checked against a file that compiles.