Teaching

Courses

Here are some of the courses I have taught recently at Carnegie Mellon:

Logic and Mechanized Reasoning (15-321)
A course for third-year students in computer science, co-taught with Marijn Heule, based on our textbook with the same name. Course page: html.
Interactive Theorem Proving (21-321)
A course for third-year students in mathematics and computer science, based on Mathematics in Lean.

Here are some of the courses I have taught in the past.

The Nature of Reason (80-150)
A survey of philosophical views on the nature of reason, including deductive logic, inductive logic, the philosophy of mind, and computation.
Logic and Mathematical Inquiry (80-211)
An introduction to logic and mathematical proof.
Logic and Computation (80-310/610)
The syntax and semantics of first-order logic, completeness, compactness, and other topics.
Lecture notes (version: January 2002, 120 pages): pdf.
Computability and Incompleteness (80-311/611)
Formal models of computation, unsolvability, and Gödel's incompleteness theorems.
Lecture notes (version: January 2007, 128 pages): pdf.
David Gray's Wall of Logic: jpg.
Notes on the incompleteness theorems, and the halting problem: pdf.
Proof Theory (80-411/711)
An introduction to proof theory.

Here are some notes on classical and constructive logic: pdf.

Meetings and Workshops

These are some of the meetings and workshops I have organized or co-organized.

Machine Assisted Proof
IPAM, February 2023, co-organized with Terence Tao, Erika Abraham, Kevin Buzzard, Jordan Ellenberg, Timothy Gowers, and Marijn Heule. Web page: html.
Lean for the Curious Mathematician 2022
ICERM, July 2022, co-organized with Kevin Buzzard, Johan Commelin, Yury Kudryashov, Heather Macbeth, and Scott Morrison. Web page: html.
Formal Methods in Mathematics / Lean Together 2020
Carnegie Mellon, January 2020, co-organized with Robert Lewis. Web page: html.
Applications of Formal Methods to Control Theory and Dynamical Systems
Carnegie Mellon, June 2018. Web page: html.
Big Proof
Isaac Newton Institute, summer 2017, co-organized with Leonardo de Moura, Georges Gonthier, Ursula Martin, J Strother Moore, Lawrence Paulson, and Natarajan Shankar. Web page: html.
Logic and Analysis
AMS-ASL special session, January 2011, co-organized with Ulrich Kohlenbach and Henry Towsner. Web page: html

Seminars

These are some of the seminars I have taught.

In the fall of 2015, I taught a seminar on mathematical language.
In the spring of 2012, I taught the second semester of our core graduate seminar in philosophy, with the following syllabus: pdf.
In the fall of 2012, I taught a seminar on mathematical understanding and cognition.
In the fall of 2011, I taught a freshman seminar on the history and philosophy of mathematics.
In the fall of 2010, I taught a seminar on the history and philosophy of mathematics with Ken Manders.
In the spring of 2007, I taught a seminar on practical decision procedures with Ed Clarke.
In the fall of 2005, I taught a seminar on the history and philosophy of mathematics with Ken Manders.
In the summer of 2005, I taught a short course on proof theory with Henry Towsner at Notre Dame.
In the fall of 2002, I taught a seminar on the history and philosophy of mathematics with Ken Manders.

Other

With Teddy Seidenfeld, I founded the Carnegie Mellon Summer School in Logic and Formal Epistemology, and I served as co-director from 2006-2010.

I used to maintain a web page listing resources for using formal methods in education.

When I was in graduate school, I taught a summer course for high school students called An intuitive approach to higher mathematics, with the Academic Talent Development Program.