Theorem Proving in Lean

A fully interactive week-long class on the Lean theorem prover — you learn by solving exercises in the browser.

Notes Source code

A completely interactive class on the Lean theorem prover from Mathcamp 2020 — you learn by solving exercises online, in the browser, with no local setup.

The prerequisites are basic proof techniques.