Lehrveranstaltung: 2.01.803 Interactive Theorem Proving

Dieser Kurs findet auf Englisch statt - Deutsche Übersetzung findet sich weiter unten.

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.

-

In diesem Kurs widmen wir uns dem interaktiven Theorembeweisen, relevant sowohl für formale Methoden in der Informatik als auch für die mathematische Logik. Beweisassistenzen helfen Nutzer*innen, mathematische Beweise interaktiv zu erarbeiten und zu verifizieren. Sie überprüfen jeden Argumentationsschritt, bieten eine leistungsstarke Automatisierung für die Beweisentwicklung und weisen auf Fehler hin, die manuell nur schwer zu erkennen wären. Diese Werkzeuge werden sowohl in der akademischen Forschung als auch in der Industrie häufig eingesetzt, um kritische Software, Hardware-Designs und mathematische Theoreme zu verifizieren.

Wir starten mit (der Wiederholung von) Grundlagen, indem wir verschiedene Logiken betrachten. Wir werden verschiedene Beweistechniken kennenlernen und in der Beweisassistenz Isabelle anwenden. Dabei lernen wir nicht nur, wie Beweise konstruiert werden, sondern auch wie ihre Korrektheit mit Hilfe von Isabelle/HOL überprüft werden kann.

Ein großer Teil des Kurses wird praktischen Übungen gewidmet sein. Nebenbei werden wir auch die Grundlagen der funktionalen Programmierung (die in Isabelle verwendet wird) lernen. Am Ende planen wir ein mehrwöchiges Projekt zur Formalisierung und Verifizierung des klassischen Ergebnisses zu Korrespondenz von deterministischen und nicht-deterministischen endliche Automaten - vielleicht erkennen Sie dies aus GTI.

Entdecken Sie mit uns, wie computergestütztes Beweisen neue Möglichkeiten für Mathematiker*innen und Informatiker*innen eröffnet, und erwerben Sie praktische Fähigkeiten. Fragen zum Kurs richten Sie bitte an Caroline Lemke.