Robert Lewis I and organized a meeting in January 2020, Formal Methods in Mathematics / Lean Together 2020, and slides and videos of most of the talks are available.

In the summer of 2018, I organized a workshop, Applications of Formal Methods to Control Theory and Dynamical Systems.

I was a co-organizer of the Big Proof program at the Isaac Newton Institute in Cambridge, England. Most of the talks and seminars were recorded and are available online.

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

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 spring of 2007, I taught a seminar on practical decision procedures with Ed Clarke.

I have co-taught the following seminars with Ken Manders (Department of Philososphy, University of Pittsburgh):

- Fall 2010, On the way to structural mathematics
- Fall 2005, Algebraic structures and mathematical practice
- Fall 2002, Mathematical struturalism

From 2006-2010, I was co-director of the Carnegie Mellon Summer School in Logic and Formal Epistemology. I taught a week-long workshop on Logic and Formal Verification in 2007, 2008, and 2009.

Reed Solomon and I organized a special session on effective aspects of measure theory and analysis for the ASL meeting in Montreal in Spring 2006. Ulrich Kohlenbach, Henry Towsner, and I organized an ASL/AMS special session, Logic and Analysis, at the Joint Mathematical Meetings in 2011.

In the summer of 2005, I taught a short course on proof theory with Henry Towsner.

Here are some of the courses I teach regularly at Carnegie Mellon:

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. Course exercises incorporated the Isabelle proof assistant.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.

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.