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.

Das Projekt ADAM möchte einen Beitrag leisten, Mathematiker:innen für diesen bevorstehenden Wandel zu wappnen.

[Archiv]Vorlesung Computergestützte Beweisführung

Wintersemester 2023/24

In dieser Vorlesung 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.

[Archiv]Kolloquiumsvortrag Why Explain Mathematics to Computers?

Am 12. Mai 2023 kam Patrick Massot (Paris-Saclay) an die HHU, um über seine Motivation für und Erfahrung mit der Formalisierung von Mathematik zu berichten. Massot hat insbesondere das umfangreiche und erst kürzlich abgeschlossene Sphere Eversion Project geleitet. Zu seinem Vortrag schreibt er:

A growing number of mathematicians are having fun explaining mathematics to computers using proof assistant software. This process is called formalization. In this talk, I will describe what formalization looks like, what kind of things it teaches us, and how it could even turn out to be useful (in our usual sense of "useful"). This will not be a talk about the foundations of mathematics, and I will assume no prior knowledge about formalization.