In this course, we will delve into the exciting field of interactive theorem proving, an area central to both formal methods in computer science and mathematical logic. Proof assistants help users construct and verify mathematical proofs interactively. They check each step of your reasoning for correctness, provide powerful automation to support proof development, and flag errors that might be difficult to spot manually. These tools are widely employed in both academic research and industry to verify critical software, hardware designs, and complex mathematical theorems where absolute certainty is needed.

We will begin by revisiting the foundations and consider different logics and reasoning systems. We will work with various proof techniques and apply them in the proof assistant Isabelle. Thereby, learning not just how to construct proofs, but also how to verify their correctness using the powerful interactive prover Isabelle/HOL.

A large part of the course will be dedicated to practical exercises. Along the way, we will also learn fundamentals of functional programming (used in Isabelle). Finally, we plan a multi-week project formalizing and verifying the classic result connecting deterministic and nondeterministic finite automata - a result you may recognize from GTI.

Join us to discover how computer-assisted proving opens new possibilities for mathematicians and computer scientists, and gain practical skills. Any questions regarding the course can be directed to Caroline Lemke.