Master-Praktikum: Formalization in Lean (FiL, WiSe 2025/26)
Instructor: Xavier Généreux
2+2 hours per week
Prerequisites
The lecture on ITP is a prerequisite for this praktikum. This prerequisite is not strict but we will expect students to have seen and understood the material from the ITP course.
Overview
The Lean Theorem Prover is a functional programming language that double as an interactive theorem prover (ITP). In this Praktikum, we will explore how to use the Lean Theorem Prover to formalize non-trivial theories. Your objective will be to formalise some fact in mathematics or computer science.
Organization
The semester will be split into two parts:
Part 1 : Background
In the first part of this Praktikum, we will review the material needed for your formalization projects. This will take the form of weekly lectures where we will make an overview of the different subjects possible for the projects and introduce the technicalities of each one. These will cover different topics in mathematics and also computer science. During this time, students will be required to complete homework. These should be handed in before the start of the projects.
Part 2 : Projects
In the second part, the project phase will commence, with students working in teams of 2 or 3. The main goal of the projects should be to formalise a series of mathematical results, the correctness of an algorithm or properties for some semantic.
Evaluation
Each team will also be tasked with delivering a presentation on their project. Evaluation will be based on the complexity of the theory, the technical difficulty of its formalisation, the readability of the code and the documentation. Student are also expected to produce a text with the following content:
- Review of the target theory and motivation
- Highlight and main challenges of the formalisation and their solutions
- Design decisions taken during the development and their motivation
- Shortcomings of the project and possible futur work
The text should be between 7.000 and 14.000 characters. (~4 to 7 pages)
Topics
Here you can find some general directions that you can take for the projects. If you choose to formalize a theory that follows a textbook, you should formalize at least some of the exercises and their solutions.
Computer science:
- extended WHILE language with static arrays or other features;
- functional data structures (e.g., balanced trees);
- functional algorithms (e.g., bubble sort, merge sort, Tarjan’s algorithm);
- type systems (e.g., Benjamin Pierce’s __Types and Programming Languages__);
- security properties (e.g., Volpano–Smith-style noninterference analysis);
- theory of first-order terms, including matching, term rewriting;
- automata theory;
- normalization of context-free grammars or regular expressions;
- chapters of concrete semantics;
- soundness and completeness of proof systems (e.g., Genzen’s sequent, calculus, natural deduction, tableaux);
- separation logic;
- verified program using Hoare logic;
- model a language like SQL and prove facts about it;
Mathematics:
Any kind of mathematical project is possible. It must, however, be significantly different from existing lean formalisations.
- Port formalized problems from another language to Lean;
- Formalise a chapter of a textbook (e.g. Understanding Analysis);
Chat
There is a Zulip chat room associated with the lecture where you can ask organizational and content-related questions. Please use it if possible, instead of sending me emails, so that your fellow students can also benefit from the answers.
Zulip-Stream: Formalization in Lean chat
Material
Getting started
Main ressources
Search engines
Other
Artikelaktionen