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.
Projektergebnisse
Wichtigstes und bleibendes Ergebnis des Projekts sind ein Webeditor für Lean4, ein Lean-Lernspielserver (Leane Game Server) und die dahinter liegende Software, sowie das Spiel Robo, das anhand typischer Aufgaben aus der Studienanfangsphase in das Arbeiten mit Beweisassistenten einführt.
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.
Wann?
Wintersemester 2023/24Wo?
Heinrich-Heine-Universität Düsseldorf
Wer?
Bachelor-Studierende der Mathematik, Informatik oder Computerlinguistik im 5./6. Semester
Seminar Game over oder QED?
In diesem Seminar lernten die Teilnehmer:innen, Beweise und typische Übungsaufgaben aus den ersten Mathematiksemestern mit Hilfe des modernen Beweisassistenten Lean zu formalisieren und zu verifizieren. Obwohl sich Lean noch in der aktiven Entwicklungsphase befindet, hat sich Lean bereits sowohl in der Formalisierung weiter Teile des Bachelor-Curriculums als auch bei der Formalisierung tiefliegender mathematischer Forschungsergebnisse bewährt.
Der Ansatz war „Learning by doing“. Als Einstieg diente das eigens entwickelte Browser-Game Robo. Die Teilnehmer:innen halfen, durch gezieltes Feedback dieses Lernspiel weiter zu verbessern. In der zweiten Seminarhälfte wurden die Teilnehmer:innen aktiv in die weitere Spielentwicklung eingebunden. Sie formalisieren selbständig Übungsaufgaben, die zukünftig in das Spiel integriert werden können.
Das Seminar richtete sich an Bachelor-Studierende der Studiengänge Mathematik und Anwendungsgebiete oder Finanz- und Versicherungsmathematik, ab dem vierten Semester.
Wann?
Sommersemester 2023 und 2024
Wo?
Heinrich-Heine-Universität Düsseldorf
Wer?
Bachelor-Studierende der Mathematik
Workshop Lean for the Curious Mathematician 2023
Tutorium
Anfang September 2023 veranstalteten wir eine viertägige Einführung in den Beweisassistenten Lean mit erfahrenen, internationalen Tutoren.
Wann?
04.– 07. September 2023
Wo?
Heinrich-Heine-Universität Düsseldorf
Wer?
angemeldete Teilnehmer
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.
Wann?
07.–08. September 2023
Wo?
Heinrich-Heine-Universität Düsseldorf
Wer?
alle Interessierten
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.
Wann?
Freitag, 12. Mai 2023
16:15 Uhr
Wo?
Hörsaal 5H, Heinrich-Heine-Universität Düsseldorf
Wer?
alle Interessierten
Personen
• Prof. Dr. Marcus Zibrowius (Projektleitung)
• Prof. Dr. Immanuel Halupczok (Projektleitung)
• Dr. Alexander Bentkamp (Lean4 Webeditor, Lean Game Server)
• Jon Eugster (Lean Game Server, Robo)
• Dr. Sina Hazratpour (Robo)
Träger
Das Projekt ADAM: Anticipating the Digital Age of Mathematics ist angesiedelt an der Heinrich-Heine-Universität Düsseldorf und wurde finanziert durch die Stiftung für Innovation in der Hochschullehre.

