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