19207219
Seminaristische Übung
Formale Beweisverifikation
Tibor Szabo
Kommentar
Ausgewählte Themen aus:
- Installation von LEAN, Verwendung des Beweisassistenten und Einrichtung eines eigenen Projektes
- Grundlagen der Dependent Type Theory und Propositions as Types
- Funktionelle Beweise und Tactics
- Grundlagen der Logik in LEAN
- Induktive Typen und Beweise durch Induktion
- Selektion an bekannten mathematischen Konzepten in LEAN (Mengenlehre, Ganze Zahlen, Vektorräume, Konvergenz, …)
- Selektion einfacher Beweise und Beweisstrategien (Unendlich viele Primzahlen, stabile Mengen im Hyperwürfel, …)
- Die mathlib Bibliothek
Bei allen Themen steht das praktische Arbeiten mit eine konkreten Beweisassistenten (z.B. LEAN) im Vordergrund.
Voraussetzungen: Lineare Algebra I und Analysis I
Literaturhinweise
Literatur:
- The Hitchhiker’s Guide to Logical Verification von Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl und Jannis Limperg
- The Mechanics of Proof by Heather Macbeth
- Functional Programming in Lean von David Thrane Christiansen
- Theorem Proving in Lean 4 von Jeremy Avigad, Leonardo de Moura, Soonho Kong und Sebastian Ullrich
- Mathematics in Lean