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: TBD
Course Description
This course introduces the use of the Lean 4 proof assistant to formalize concepts and results from theoretical computer science and related 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
TBD
Lectures
Problem Sets
TBD
Additional References
Some resources that could be useful for the course:
- Online Lean4 IDE with latest mathlib4.
- Proving theorems in Lean: Course by Yuval Filmus.
- Proofs and Programs: Course on introduction to interactive theorem proving using Lean by Siddhartha Gadgil.
- The Mechanics of Proof: Book by Heather Macbeth.
- Mathematics in Lean: Book by Jeremy Avigad, Patrick Massot.
- EPFL Lean mini course: Adapted from Mathematics in Lean and the Lean for the Curious Mathematician 2023 workshop.
- Loodle!: Search engine for Lean 4.
- mathlib4 documentation.
- Lean community Zulip channel for questions and discussions.