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: By Appointment
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] [Solution]
- (01/30) Lecture 2: Terms vs Tactics, More Tactics, Induction [Slides] [Code] [Solution]
- (02/06) Lecture 3: Proofs with Structure [Slides] [Code] [Solution]
- (02/13) Lecture 4: Query Complexity of Boolean Functions [Slides] [Code] [Solution]
- (02/20) Lecture 5: Introduction to Graphs in Lean [Code] [Solution]
- (02/27) Lecture 6: Introduction to Coding Theory in Lean [Code] [Solution]
- (03/06) Lecture 7: Algorithm Verification and Cryptography in Lean [Code] [Solution]
- (03/13) Lecture 8: Reducibility among NP-complete problems [Code] [Solution]
Final Projects
Here is the List of Final Projects.
Please see the project ideas list for suggested topics.
Groups
Form groups of 1–3 people. In general, choose a harder project if you have more people in your group.
Deadlines
| Date | Milestone |
|---|---|
| March 17 | Project Proposal Due |
| March 20 | Pre-Project Presentations |
| April 10 | Project Presentations |
| April 17 | Project Presentations |
| April 24 | Project Presentations |
| May 1 | Project Presentations |
Project Proposal (Due March 17)
Submit a 1–2 page proposal describing what you plan to formalize and the proof strategy you intend to follow. Use the [proposal template] [Download].
Pre-Project Presentation (March 20)
An 8-minute short presentation covering:
- What you are trying to formalize
- The proof method or approach you plan to take
Problem Sets
Problem Set Mathlib Project Folder [Download]
- PS1 (Due 02/05): [View On Github] [Download] [Solutions]
- PS2 (Due 02/19): [View On Github] [Download] [Solutions]
- PS3 (Due 03/05): [View On Github] [Download]
AI policy
You are welcome to use any AI tool to ask general questions about Lean4 syntax, tactics, and mathlib theorem usage.
However, you may not copy homework problems into AI tools or ask AI to produce homework solutions, and you may not submit AI-generated homework answers as your own work.
For the final project, you are welcome to use any AI tool without restriction.
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.
- Logical Verification 2025 (Lean Forward): Course materials and repository for the Lean Forward Logical Verification 2025 program.
Miscellaneous:
- Loogle!: 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.