Course Objective:  Participants will learn new techniques for writing formal proofs about algorithms and will be able to use interactive theorem provers to verify algorithm correctness and analyze their runtime.

Course Content:  The first part of the course introduces interactive theorem provers and their use in formalizing hand-written mathematical proofs. Participants will learn essential proof techniques, including basic tactics, recursion, and induction principles. The course will also cover how to work with inductive types, providing a foundation for formally expressing and reasoning about mathematical structures. In the second part of the course, the focus shifts to the formal verification of algorithms. Students will learn to specify algorithms using functional programming and utilize theorem provers to verify their correctness and analyze their runtime formally. This section includes the formalization of basic algorithmic paradigms such as divide-and-conquer and greedy algorithms.

Prerequisites: This course is targeted towards master's and doctoral students with an interest in theoretical computer science and formal verification in Lean 4. Students should be comfortable with the design and analysis of algorithms, as well as functional programming. If you are unsure whether you are ready for this class, please consult the lecturers.

Literature

• Theorem Proving In Lean 4  by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. 

  • This book serves as a helpful reference on how Lean 4 works.  

• Mathematics in Lean by Jeremy Avigad, Patrick Massot. 

  • This book walks through mathematical proofs without going into too much detail about how Lean 4 works. 

• Functional Programming in Lean by David Thrane Christiansen

  • This book serves as a helpful reference for functional programming in Lean. 

Course Moodle 

You can ask the course TAs and instructors about the course materials, exercises, and any other issues on the course Moodle page.

Please make sure you receive Moodle notifications from this course, as some announcements will be made exclusively through Moodle.

Course Note

The lecture will be based on the following GitHub repository: https://github.com/sorrachai/FAA2026. Course notes will be updated shortly after each lecture. 

Performance Assessment

• Graded Homework: 40 % of the grade.  The homework consists of weekly problems. 

  • Oral Defense:  Each week, a subset of homework submissions will be selected through a semi-random process for an oral defense. If your submission is selected, you will be required to schedule a short Zoom meeting with a teaching assistant to explain your work and demonstrate your understanding. If you do not demonstrate sufficient understanding, you will receive a zero on that assignment, and your next submission will be selected for the defense. Submissions that raise concerns about academic integrity will also be selected for an oral defense.

• Project: 60 % of the grade.  Key points:  

  • A group of 3 - 4 students. 

  • Proposal Deadline: 13 November 2026. 

  • Progress Presentation in the last two classes.

  • Project Submission Deadline: 15 January 2027.