Interactive Theorem Proving (ITP, SoSe 2026)

Lecture 2 hours, Xu; exercises 2 hours, Blanchette, Graß

For BSc students, the course is officially called "Interactive Theorem Proving for Bachelor".

Overview

This course introduces the proof assistant Lean 4, its type-theoretic foundations, and its applications to computer science and mathematics.

Proof assistants are pieces of software that can be used to check the correctness of a specification of a program or the proof of a mathematical theorem. In the practical work, we learn to use Lean. We will see how to use the system to prove mathematical theorems in a precise, formal way, and how to verify small functional programs. In the course, we focus on Lean's dependent type theory and on the Curry–Howard correspondence between proofs and functional programs (λ-terms). These concepts are the basis of Lean but also of other popular systems, including Agda, Matita, and Rocq.

There are no formal prerequisites, but familiarity with functional programming (e.g., Haskell) and basic algebra is an asset. If you are new to functional programming, we recommend that you read the first chapters of Learn You a Haskell for Great Good!, stopping at the section "Only folds and horses."

Organization

To top