Monday September 22
Introductions and the Natural Number Game
Monday September 29
Getting started with a Lean editor
Lean functions including: intro, unfold, exact, use, rw, linarith/ring/simp
Monday October 6
More on intro/unfold/use. Proof structuring and cases