How-to guides¶

These pages answer one question each. They assume that we have finished the tutorial, or at least that we can read Lean without help, and they do not build on one another.

Setup¶

These get an editor talking to Lean.

• Set up Neovim for Lean.
• Set up VS Code for Lean.
• Read a goal without an infoview, for a machine where no plugin can be installed.

Definitions and proofs¶

These cover the everyday tasks of writing game theory in Lean.

• Encode a new game, with named actions and a payoff function by cases.
• Write a new definition, and check that it means what was intended.
• Prove an inequality, with numbers, symbols or products.
• Prove a statement for every strategy.
• Split a proof into cases.
• Use a hypothesis.
• Find a lemma in Mathlib.
• Read an error message.

Mixed strategies¶

These extend the tutorial from pure to mixed strategies.

• Define expected payoffs for mixed strategies, using Mathlib's standard simplex.
• Verify a mixed ESS in Hawk-Dove, from the payoff matrix to the Nash property.