Intro
When humans prove the correctness of mathematical theorems, they naturally make mistakes. Subtle mistakes can stay unnoticed for a long time, while other works build on incorrect theorems. Every person who wants to make sure that a result is correct needs to check the whole proof in detail, leading to a huge duplication of effort.
(Computer-aided) theorem proving seeks to alleviate those issues. Once the computer has verified a proof, we do not manually verify it over and over, and we do not need to rely on humans not making mistakes.
There are roughly speaking two kinds of theorem proving: automated theorem proving where the computer fully automatically proves the theorem (or fails), and interactive theorem proving where a human guides the computer through the proof until the computer is satisfied.
This course aims to introduce the latter:
- How to use an interactive theorem prover (using Isabelle/HOL as the working example)
- How an interactive theorem prover works
The course consists of two parts:
- The first half of the semester, we introduce the interactive theorem proving using Isabelle/HOL. (Lectures and homeworks and practice sessions.)
- The second half is project group work, working on individual topics. Those topics can either be proving some interesting theorem in Isabelle/HOL, or implementing some small theorem proving related project. Lectures will continue with the goal of supporting the projects.
Lecture data
- Lecturer: Dominique Unruh
- Lecture: Mondays, 14:15–15:45. Δ-2045
- Practice: Wednesdays, 10:15–11:45. Δ-2010
- Volume: 6 ECTS