Math 480b: Introduction to Mathematical Formalization

Spring quarter 2025

Lectures: Mon, Wed 10:30-11:50 am in MEB 242
Instructor: Jarod Alper (jarod@uw.edu), Office hours: Mon/Wed 3-4 pm in PDL C-549
TA: Vasily Ilin (vilin@uw.edu), Office hours: Fri 2:30-4 pm in PDL C-8K

Schedule:
  • Mar 31: Lean tutorial: lecture1.lean
  • Apr 2: Lean tutorial: lecture2.lean
  • Apr 7: Why formalize? A broad introduction to Math and AI: slides
  • Apr 9: Discussion of group projects and a Lean tutorial: lecture4.lean
  • Apr 14: Lean tutorial on limits of sequences and dependent type theory: lecture5.lean
  • Apr 16: Discussion of group projects
  • Apr 21: Lean tutorial by Vasily Ilin
  • Apr 23: no class
  • Apr 28: Lean tutorial on tactics lecture9.lean and group project discussion
  • Apr 30: Examples of tactics (where each student picked a tactic and demonstrated how it works in an example) and we decided on project groups
  • May 5: More tactics lecture11.lean and group work

  • Homework: There are weekly homework assignments. They should be submitted on Canvas by class time.
    Syllabus: This course will explore how mathematical theorems can be formalized in the interactive theorem prover Lean. We will focus on topics in undergraduate mathematics such as set theory, logic, functions, induction, number theory, and other topics typically encountered in Math 300: Introduction to Mathematical Reasoning. For each topic, we will review the mathematical foundations, and then attempt to formalize main theorems and exercises. As the course progresses, we will learn more and more sophisticated high-level tactics that can help automate the formalization. By the end of the quarter, we will have group projects, where each group chooses a mathematical statement to formalize, depending on the interests of the students.

    Online textbook: Mathematics in Lean by Jeremy Avigad and Patrick Massot

    Setting up a Lean environment
    Additional Lean resources


    Group projects


    Grading
    Course policies