Teaching resources #

We've collected different kinds of resources that might be helpful for running courses using Lean.

Notes and Textbooks #

There are various learning resources collected on this website. Here we list texts that are explicitly designed for university courses.

• The Mechanics of Proof by Heather Macbeth is a set of lecture notes dealing with how to write careful, rigorous mathematical proofs, paired with material in Lean.
• How To Prove It With Lean by Daniel Velleman is a supplement to the book How To Prove It.
• The Hitchhiker's Guide to Logical Verification by Jasmin Blanchette is a textbook that introduces the reader to interactive theorem proving using the Lean 4 proof assistant as its vehicle. The textbook is accompanied by Lean demonstration and exercise files.

Games #

• The Natural Number Game by Kevin Buzzard, Jon Eugster, and Mohammad Pedramfar is a popular introduction to Lean.
• The engine behind the NNG can be used to design custom games for courses.

Autograders #

• A Gradescope autograder for Lean 4
• A GitHub Classrooms autograder for Lean 4

Lean-in-the-cloud setups #

• Inserting the mathlib4 .devcontainer directory into your course project will enable GitHub Codespaces for your project. Encourage students to sign up for a (free) pro account through GitHub's education benefits in order to get more Codespaces hours.
• Similarly, inserting the mathlib4 .gitpod.yml and .docker/gitpod/Dockerfile will enable Gitpod usage.