A course on logic and proof theory using the Lean theorem prover.

Currently uses Lean 3, which is a bit different from Lean 4.