At Brown:

at VU Amsterdam:

at Carnegie Mellon:

at St. Agnes Academy:

Logic and Proof

I am helping develop an open-source course and text on mathematical proof and argument. The course uses examples from the Lean proof assistant. We have designed the course to encourage students to think about mathematics from three perspectives: the formal (logic and natural deduction), the informal (natural-language concepts and proofs), and the semi-formal (exemplified by Lean).

The most recent version of the text can be found here (interactive) or here (pdf), and the development is tracked on GitHub.

In Fall 2016, Jeremy Avigad and I co-taught a sophomore-level course at CMU using these notes. In 2019 and 2020 I taught a second-year CS course at the VU using these notes. The 2020 edition of this class is being held online; I am recording video lectures that will cover the first ~10 chapters of the text.