Theorem Proving in Lean

course notes
Mathcamp
lean
A fully interactive week-long class on the Lean theorem prover; you learn by solving exercises in the browser.
Published

July 1, 2020

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.