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

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