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 (link).

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/FAA2025. Course notes are to be updated shortly after each lecture. 

Performance Assessment

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

• Project: 60 % of the grade. The details will follow in due time.