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

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 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. It should be handed in before the start of the projects.

Homework

To access the homework follow these steps (see Lean projects for more info):

  • Go the the directory where you would like this package to live.
  • Run git clone https://github.com/xgenereux/formalization_in_lean_2025.git.
  • Run cd formalization_in_lean_2025.
  • Run lake exe cache get. (This takes a little while)
  • Run code . to open the project. If you open it from a menu, you need to open the formalization_in_lean_2025 folder.

Deadline

The deadline for the homework is 05.12.2025 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 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. An introduction to number theory);

Schedule for Part 1

Lecture : Monday 16:00 - 18:00 c.t. Oettingenstr. 67 - 027, Floor Plan

Group exercise : Thursday 10:00 - 12:00 c.t. Oettingenstr. 67 - L109, Floor Plan

Note: There will be no group exercise session on Thursday 16.10.2025.

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

News

To top