Master-Praktikum: Formalization in Lean (FiL, WiSe 2026/27)
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
Lean is a functional programming language that doubles 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 formalize 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. It should be handed in before the start of the projects.
Homework
More information soon.
Deadline
The deadline for the homework is 04.12.2026 at 23:59.
To submit the homework, please do a private Github repository and invite me before the deadline.
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 formalize 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. Students 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 future 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., Gentzen'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;
- formalize a chapter of a textbook (e.g. An introduction to number theory);
Further information
You have, at the latest, until December 18th to lock in your project's topic. Please write on the "Projects" thread on the course's Zulip with your team's members and a summary of your project. Example:
@Name1 @Name2 and myself will be working on Formally real fields, with the goal of proving formally that such fields are orderable.
We intend to prove it by applying Zorn's lemma, to show that a formally real field contains a maximal positive cone, and that the latter defines a total positive cone in the sense of
mathlib. And then it is proved inmathlibthat such a cone defines an ordering.
During the middle of the project phase, there will be a mandatory meeting with me to review your progress in the projects. (End of January.) Otherwise, you will have the possibility to meet me weekly during class hours to ask questions. (See Schedule below.)
The projects are open ended, you can push them as far as you want. Even with mathematical theorems, there are often optimisations, related facts or generalization available as an open direction.
Deadline
TBA
Schedule for Part 1
Lecture : Monday 16:00 - 18:00 c.t. Oettingenstr. 67 - TBA
Group exercise : Thursday 10:00 - 12:00 c.t. Oettingenstr. 67 - L109, Floor Plan
Exceptions
Any irregularities in the meetings will be posted here.
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: TBA