In dieser Vorlesung über Beweisassistenten treffen sich Studierende der Informatik, Mathematik und Computerlinguistik.
Beweisassistenten werden in der Chipherstellung und Softwareentwicklung eingesetzt, um die Fehlerfreiheit von Soft- und Hardware zu verifizieren. Sie geben MathematikerInnen letzte Gewissheit, wenn sie ihren eigenen Beweisen nicht trauen. Für LinguistInnen sind sie eine Möglichkeit mit Typentheorie zu experimentieren - einem Formalismus, der auch zur Modellierung der Semantik natürlicher Sprache verwendet wird.
Die Vorlesung bietet eine bündige Einführung in die Funktionsweise von Beweisassistenten und ihre theoretischen Grundlagen. Dazu zählen zum Beispiel der Lambda-Kalkül, Typentheorie inklusive induktiver Typen und die Curry-Howard-Korrespondenz. Zudem schauen wir uns beispielhaft an, wie Beweisassistenten und Typentheorie für die oben genannten Anwendungen eingesetzt werden können.
In den Übungen wird die Theorie erfahrbar anhand von Lean, einem modernen Beweisassistenten, der in der jüngsten Formalisierungswelle innerhalb der Mathematik eine maßgebende Rolle spielt.
Im Studiengang "Mathematik und Anwendungsgebiete" wird diese Veranstaltung im Rahmen des Moduls "Ausgewählte Kapitel der Algebra/Geometrie" angeboten.