Aktuelle Lehre
Sommersemester 2026
Arbeiten mit Beweissystemen am Beispiel von Lean mit Michael Junk und Maik Fücks
4,5 ECTS credits, 2V+1Ü
Wie unterscheidet sich eigentlich ein Beweis am Computer von einem Beweis auf Papier?
Muss man mehr oder weniger schreiben? Hilft der Computer oder stört er?
Wie wichtig wird das assistierte Beweisen in der Zukunft sein?
Formale Beweise gewinnen in der modernen Mathematik zunehmend an Bedeutung. In dieser Vorlesung lernen wir den mathematischen Beweisassistenten Lean kennen und sehen, wie mathematische Aussagen präzise formalisiert und maschinell überprüft werden können.
Anhand einfacher Beispiele aus verschiedenen Bereichen der Mathematik erarbeiten wir schrittweise die Grundlagen von Lean: von der Syntax über Taktiken bis hin zum Aufbau eigener formaler Beweise. Ziel ist es, ein Gefühl dafür zu entwickeln, wie mathematisches Denken mit computergestützter Verifikation zusammenwirkt.
Die Vorlesung richtet sich an Mathematikstudierende ohne Vorkenntnisse in Lean. Programmierkenntnisse sind nicht erforderlich.
Übungen zur Computergestützte Mathematik mit Stefan Frei
Frühere Lehre
Wintersemester 2025/26
Numerische Mathematik Übung
