19207219
Seminaristische Übung
Formale Beweisverifikation
Christoph Spiegel
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
20 Termine
Regelmäßige Termine der Lehrveranstaltung
Mo, 10.03.2025 09:00 - 12:00
Di, 11.03.2025 09:00 - 12:00
Mi, 12.03.2025 09:00 - 12:00
Do, 13.03.2025 09:00 - 12:00
Fr, 14.03.2025 09:00 - 12:00
Mo, 17.03.2025 09:00 - 12:00
Di, 18.03.2025 09:00 - 12:00
Mi, 19.03.2025 09:00 - 12:00
Do, 20.03.2025 09:00 - 12:00
Fr, 21.03.2025 09:00 - 12:00
Mo, 10.03.2025 13:30 - 16:30
Di, 11.03.2025 13:30 - 16:30
Mi, 12.03.2025 13:30 - 16:30
Do, 13.03.2025 13:30 - 16:30
Fr, 14.03.2025 13:30 - 16:30
Mo, 17.03.2025 13:30 - 16:30
Di, 18.03.2025 13:30 - 16:30
Mi, 19.03.2025 13:30 - 16:30
Do, 20.03.2025 13:30 - 16:30
Fr, 21.03.2025 13:30 - 16:30