Proving TCS and Math Theorems in Lean

Course Logo

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

Final Projects

Please see the project ideas list for suggested topics.

Please see the final project repository for all class final projects.

Project Author(s)
A-infinity Categories Justin Mu
AC0[2] Circuit Lower Bounds Yichuan Wang
Formalising Two Quantum Coding Bounds in Lean 4 Frederick Dehmel
Formalizing Hypercontractivity for Boolean Functions Owen McGinty
Formalizing Karger’s MinCut in Lean4 Joon Kim
Formalizing NP-Completeness Reductions in Lean 4 Kobe Zou
Formalizing Online Learning and the Minimax Theorem Karim Abdel Sadek, Mark Bedaywi
Formalizing the BLR linearity Test in Lean Prastik Mohanraj
Formalizing the Halving Algorithm and Its Optimal Mistake Bound in Lean 4 Arhaan Aggarwal
Formalizing the Johnson-Lindenstrauss Lemma in Lean Ganesh Sankar
Formalizing the Joints Theorem Yuchen Liu
Formalizing the Kleene–Post Theorem in Lean 4 Jacob Parish, Yvette Ren
Formalizing the Optimality of Kruskal’s Algorithm Harsha Polavaram
Formulizing Communication Complexity in Lean4 Lucy Horowitz, Timothe Kasriel, Mihir Singhal
Lean Asymptotic Tactics Arnav Mehta
On the Efferent Lower Bounds of Kakeya Sets with Dvir-Saraf-Sudan Robert Ho
Poly-logarithmic independence fools AC0 circuits Jason Dong
Schnorr Identification Protocol Esha Garg

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]

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:

Books:

Other similar courses:

Miscellaneous:

  • Loogle!: Search engine for Lean 4.
  • mathlib4 documentation.
  • Lean community Zulip channel for questions and discussions.
  • TCSlib Project by Shilun Li, Venkatesan Guruswami, Frederick Dehmel, Jason Dong, Henry Li et al.