ADAM
Anticipating the Digital Age of Mathematics

Das Projekt

Die Ansprüche, die Mathematiker:innen an Beweise stellen, haben sich über die Jahrhunderte immer wieder verändert. Wäre im digitalen Zeitalter nicht eine vollständige Formalisierung und algorithmische Überprüfung von Beweisen durch Computer angemessen? Diese Frage bleibt umstritten. Eines aber ist aus den bisherigen Erfahrungen klar: Eine solche Formalisierung hat überhaupt nur dann Aussicht auf Erfolg, wenn ein großer Teil der Formalisierung selbst, also der detaillierten formalen Ausformulierung von Beweisen, systematisch durch Computer unterstützt wird. Hier liegt die Aufgabe von interaktiven Beweisassistenten. Sie ermöglichen es uns Menschen, mathematische Beweise so zu formalisieren, dass ein Computer sie verifizieren kann.

Inzwischen haben computergestützte Beweisassistenten ein Niveau erreicht, das die vollständige Formalisierung, Verifizierung und digitale Weiterverarbeitung weiter Teile unseres mathematischen Kenntnisstandes greifbar nah erscheinen lässt. Erfolgreiche Formalisierungsprojekte wie das Sphere Eversion Project oder das Liquid Tensor Experiment zeigen, dass es inzwischen möglich ist, tiefliegende mathematische Sätze mit vertretbarem Aufwand digital abzubilden und zu verifizieren. Wir müssen davon ausgehen, dass für die nächste Generation Mathematiker:innen Beweisassistenten und digitale Beweisbibliotheken zu einem wichtigen Werkzeug avancieren werden.

Ziel des Projekts ADAM war es, einen Beitrag leisten, Mathematiker:innen für diesen bevorstehenden Wandel zu wappnen. Laufzeit des Projekts war September 2022 bis Dezember 2024. Diese Seite gibt einen Überblick über die Projektergebnisse und über Veranstaltungen, die im Rahmen des Projekts stattgefunden haben.

Vorlesung Computergestützte Beweisführung

In dieser Vorlesung trafen 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 bat eine bündige Einführung in die Funktionsweise von Beweisassistenten und ihre theoretischen Grundlagen. Dazu zählten zum Beispiel der Lambda-Kalkül, Typentheorie inklusive induktiver Typen und die Curry-Howard-Korrespondenz. Zudem schauten wir uns beispielhaft an, wie Beweisassistenten und Typentheorie für die oben genannten Anwendungen eingesetzt werden können.

In den Übungen wurde die Theorie erfahrbar anhand von Lean, einem modernen Beweisassistenten, der in der jüngsten Formalisierungswelle innerhalb der Mathematik eine maßgebende Rolle spielt.

Tutorium

Anfang September 2023 veranstalteten wir eine viertägige Einführung in den Beweisassistenten Lean mit erfahrenen, internationalen Tutoren.

Kolloquium

Im Anschluss an, aber inhaltich unabhängig vom gleichnamigen Tutorium, führten wir Anfang September 2023 ein zweitägiges Kolloquium durch. Internationale Vortragende beleuchteten aktuelle Entwicklungen in der Formalisierung aus verschiedenen Richtungen und luden zum Nachdenken über die zukünftige Rolle von Formalisierung in der Mathematik ein.