Interactive Theorem Proving course
This is a course on Interactive Theorem Proving with Lean 4.
Main features
-
Our main focus is on the foundations of Lean. We discuss the key ideas of the underlying type theory in a semi-formal way, aiming to provide some intuition on the inner workings.
-
We follow a bottom-up approach, aiming to introduce each feature of Lean before using it. We make a few exceptions in our examples when we feel that the reader should still be able to intuitively understand the features we use, even when we have not yet formally introduced them.
-
The course material is divided by topic rather than by lesson. Some files are therefore significantly longer than others.
-
We suggest exercises on each topic.
How to get started with Lean 4
The material in this course can be used in several alternative ways:
-
Use Lean 4 in your browser right now via Lean 4 web. Choose this if you are in a hurry and do not have time to do a proper installation. (Remember to save your code locally before closing the web page.)
-
Install Lean 4 locally on your own computer. Following the instructions requires some time and patience, as well as some free disk space (~15GB should be enough). Probably the best choice, once it is set up.
-
Use GitHub codespaces on this repository. A full Lean 4 remote server will be automatically set up for you, and you will be able to work in your browser and save your changes. Almost as good as a local installation. Currently (in 2025) GitHub gives you 60 server hours for free each month (more if you become a verified student). (Note that saved but uncommitted changes will be lost if a codespace is inactive for more than 30 days.)
Lean 4 documentation
- Lean Language Reference -- the ultimate authority on Lean syntax, features, and tactics.
- Mathlib4 Documentation -- the standard library formalizing large areas of mathematics.
- Theorem Proving in Lean 4 -- a convenient tutorial.
- Mathematics in Lean -- a book on how to formalize mathematics in Lean.
- Loogle -- a search engine for the Lean libraries, based on formulas.
- LeanSearch -- a search engine for the Lean libraries, based on natural language.
- Cheatsheet -- a summary of the most common terms and tactics.
- 100 theorems -- a list of famous results.
- Lean Game Server -- browser games involving Lean proofs.