Teaching
At Brown:
- 2022 Fall: Formal Proof and Verification
- 2022 Fall: Compilers and Program Analysis
- 2022 Spring: Discrete Structures and Probability
- 2021 Fall: Formal Proof and Verification
- 2021 Fall: Computing Foundations: Program Organization (second instructor)
at VU Amsterdam:
- 2021 Spring: Logic and Modeling (held online due to COVID-19)
- 2020 Spring: Logic and Modeling (held online due to COVID-19)
- 2019 Spring: Logic and Modeling
- 2018 Spring: Logic and Modeling (teaching assistant)
at Carnegie Mellon:
- 2016 Fall: Logic and Mathematical Inquiry
- 2015 Spring: Nature of Mathematical Reasoning
- 2014 Fall: Models and Methods of Optimization (teaching assistant)
- 2014 Summer: Nature of Mathematical Reasoning
- 2014 Spring: Undecidability and Incompleteness (grader and guest lecturer)
- 2013 Fall: Formal Logic (grader and guest lecturer)
at St. Agnes Academy:
- 2011-2012: Geometry, Pre-calculus, AP Calculus AB
- 2010-2011: Geometry, AP Calculus AB
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.