Skip to content

Tutorial

This is the guided path. It runs from an empty directory to a proved theorem, and it is meant to be followed in order, typing along the way. Nothing here is optional, and nothing here asks the reader to make a choice.

The path is six chapters.

  1. A first conversation with Lean. Installing the toolchain and confirming that Lean responds.
  2. A game as a Lean object. Writing down the Prisoner's Dilemma.
  3. The first proof. Showing that defection beats cooperation against a defector.
  4. Quantifiers. Defining strict dominance in general, then applying it.
  5. Two definitions. Symmetric Nash equilibrium and evolutionary stability.
  6. The capstone. Proving that an ESS is a symmetric Nash equilibrium.

By the end we will have met roughly ten tactics. That is a small fraction of Lean, and it is enough to state and prove a real theorem.