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.
- 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.
Lean-in-the-cloud setups #
- Inserting the
.devcontainerdirectory 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
.docker/gitpod/Dockerfilewill enable Gitpod usage.