Overview

  • Responsible professor / supervisor: Dominique Unruh
  • Semester: Winter 2026/27
  • Level: Master

About

Theorem proving is a way to explain mathematical proofs to a computer. The benefit of this is that the proofs are much more reliable; human error is excluded (up to some caveats) because a computer checks every step of the proof. One theorem prover that has gained much popularity in recent years is Lean. It uses a dependently typed programming language to create mathematical proofs. Mathematical proofs can be either “traditional” mathematical statements, or proofs of correctness of software, etc.

In this lab, you will explore how theorems are proven in Lean by hands-on proving of some theorems. This will involve some guided self-learning how Lean and dependent types work. The theorems that will be proven will be agreed upon which each student/group individually, based on their interests.

AI (LLMs) has become a very powerful tool in theorem proving. However, to make productive use of AI here, free commercial offers or small self-hosted systems are not very useful. We cannot offer paid AI use for the seminar. To be inclusive, we will allow you to choose whether you wish to use AI in your project, or not. We will find suitable topics in both cases.

Prerequisites

The following courses, or a comparable background:

  • Foundations of Functional Programming
  • Mathematical Logic II – and/or – Fixpoints and Induction in Logic and Computer Science