Lean for Algorithms

In this course, students learn the basics of formalizing mathematical and algorithmic results using the Lean proof assistant.

At the end of the course, students should be able to define data structures, write algorithms on those data structures, and proof the correctness and time bounds on those algorithms using the Lean proof assistant.

 

The course will be taught exclusively in English.

 

The course starts on 12 October 2026, and teaching ends on 7 February 2027. There won't be teaching on 9 November – 15 November, nor on 21 December – 3 January. In total, there will be 14 weeks of teaching.

 

We do not have formal prerequisites. However, familiarity with most of the following concepts is expected:

- Basics of programming, including functional programming.

- Formulating basic mathematical definitions, theorems and proofs, including using induction principle.

- Basic data structures and algorithms, like basic sorting algorithms and binary search trees.

The course consists of three modules, each 4–5 weeks long. There are assignments after each week. A student needs to get 40% of the points for the assignments in each of the three modules, and 50% of the total points over all assignments to register for the exam. The assignments consist of both writing Lean code and handwritten mathematical proofs.

At the end of the course, there is a final project and an oral exam focusing on the final project. The final exam may be retaken, but may require a second project at the discretion of the examiner.

One can learn computer-assisted formalization only by doing it. Therefore, we forbid the usage of AI tools for writing Lean code and for solving the assignments. One can use AI tools as a search engine at their discretion.