# Teaching

## Courses

Here are some of the courses I have taught recently at Carnegie Mellon:Logic and Mechanized Reasoning (15-217)

A course for second-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.

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, based on Logic and 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.