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.

Seminar Game over oder QED?

In diesem Seminar lernen 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 ist „Learning by doing“. Als Einstieg dient ein eigens entwickeltes Browser-Game. Die Teilnehmer:innen helfen, durch gezieltes Feedback dieses Lernspiel weiter zu verbessern. In der zweiten Seminarhälfte werden die Teilnehmer:innen aktiv in die weitere Spielentwicklung eingebunden. Sie formalisieren selbständig Übungsaufgaben, die zukünftig in das Spiel integriert werden werden.

Das Seminar richtet sich an Bachelor-Studierende der Studiengänge Mathematik und Anwendungsgebiete oder Finanz- und Versicherungsmathematik, ab dem vierten Semester.

Update 04. April 2023: Die maximale Teilnehmerzahl wurde bereits erreicht. Eine Anmeldung ist nicht mehr möglich.


Wann?

Dienstags, 14:30 Uhr,
Sommersemester 2023

Wo?

Seminarraum 25.22.02.81, Heinrich-Heine-Universität Düsseldorf

Wer?

zugelassene Teilnehmer

Kolloquiumsvortrag Why Explain Mathematics to Computers?

Am 12. Mai kommt 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

Workshop Lean for the Curious Mathematician 2023

Tutorium

Anfang September organisieren 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

Link

LftCM 2023


Kolloquium

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


Wann?

07.–08. September 2023

Wo?

Heinrich-Heine-Universität Düsseldorf

Wer?

alle Interessierten

Link

LftCM 2023

Träger

Das Projekt ADAM: Anticipating the Digital Age of Mathematics ist angesiedelt an der Heinrich-Heine-Universität Düsseldorf und wird finanziert durch die Stiftung für Innovation in der Hochschullehre.

Ansprechpartner:
Prof. Dr. Marcus Zibrowius
Prof. Dr. Immanuel Halupczok
Jon Eugster