Math 222: Interactive Theorem Proving (Fall 2026)

A proof assistant is a computer program that verifies the integrity of mathematical reasoning. Such software addresses an aspiration predating the invention of computers: can we find certainty in our arguments by fully mechanizing them? Rather than writing every detail, the user specifies tactics and techniques to apply, and the software replies with what it could formalize and verify. This course uses a proof assistant called Lean 4, which is powerful and usable enough to verify theorems at the cutting edge of mathematical research. The course emphasizes how the interactive window provided by Lean can help students learn to write and understand human-written proofs. Students will practice formalizing theorems from a variety of mathematical topics, some of which may be drawn from their other interests and coursework.

More course information will be posted here soon.

Help hours

  • My tentative office hours in SMUD 401:
    • Tuesday 2:30-4:00
    • Wednesday 9:30-11:00
    • Friday 1:00-2:00
    • Please notify me if these don’t work well for you. I may revise them.

Handouts

Problem Sets

  • PSet 1 (due Friday 9/11 at 10pm).
  • PSet 2 (due Wednesday 9/23 at 10pm).
  • PSet 3 (due Wednesday 9/30 at 10pm). Just lean exercises this week.
    • Click here to work on these in a browser.
  • PSet 4 (due Wednesday 10/14 at 10pm). Just lean exercises this week.
    • Click here to work on these in a browser.
  • PSet 5 (due Wednesday 10/21 at 10pm).
    • Click here to work on these in a browser.

Midterm exam

  • The midterm exam will be held in class on Thursday, October 29.
  • You may bring a one-page notesheet (front and back) to the exam.
  • The exam may cover any material up to and including material introduced on October 22, and on the first five problem sets.
  • Some sample problems and solutions. I may add to this list over time.