Proving TCS and Math Theorems in Lean
Instructor: Venkatesan Guruswami
Lecture time: Friday 13:00–15:00
Location: SODA 320
Guest Lecturer: Pritish Kamath
TA: Shilun (Allan) Li
Office hours:
Venkat: TBD
Shilun: Friday 15:00-16:00 (SODA 411)
Course Description
This course introduces the use of the Lean 4 proof assistant to formalize concepts and results from theoretical computer science and mathematics. The first part of the course covers the fundamentals of Lean 4, including its logical foundations, core syntax, and proof tactics, through guided exercises and examples.
Students will then form small groups and undertake a semester-long formalization project on a selected topic, such as automata theory, computability, complexity theory, or combinatorics. The course emphasizes hands-on engagement with Lean and aims to provide students with practical experience in mechanized reasoning and formal proof development.
Grading
Class Participation 10%
Homework 30%
Final Project 60%
Lectures
- (01/23) Lecture 1: Syntax, Formalization, Goals & Tactics [Slides] [Code]
- (01/30) Lecture 2: Terms vs Tactics, More Tactics, Induction [Slides] [Code]
- (02/06) Lecture 3: Proofs with Structure [Slides] [Code]
Problem Sets
- PS1 (Due 02/05): [Download]
Additional References
Installing / running Lean4:
- (Recommended) Via VSCode Extension.
- Online Lean4 IDE with latest mathlib4.
Books:
- Mathematics in Lean: Book by Jeremy Avigad, Patrick Massot.
- The Mechanics of Proof: Book by Heather Macbeth.
- Theorem Proving in Lean 4: Book by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich.
Other similar courses:
- Proving theorems in Lean: Course by Yuval Filmus.
- Proofs and Programs: Course on introduction to interactive theorem proving using Lean by Siddhartha Gadgil.
- EPFL Lean mini course: Adapted from Mathematics in Lean and the Lean for the Curious Mathematician 2023 workshop.
Miscellaneous:
- Loodle!: Search engine for Lean 4.
- mathlib4 documentation.
- Lean community Zulip channel for questions and discussions.
- ECClib Project by Venkatesan Guruswami, Shilun Li, Henry Li, Frederick Dehmel, Annie Yao et al.