„Vom 26. bis 30. Juni hatte ich das Privileg, an der Masterclass Formalisation of Mathematics an der University of Copenhagen teilzunehmen. Thema der Masterclass war die Formalisierung von Mathematik mithilfe von sogenannten Beweisassistenten. Diese dienen dazu, die Korrektheit mathematischer Ergebnisse computergestützt zu verifizieren und auf diese Weise zu digitalisieren. Anhand des Beispiels der Kondensierten Mathematik (Condensed Mathematics) von Dustin Clausen und Peter Scholze wurde den Teilnehmenden in kürzester Zeit nähergebracht, wie selbst brandneue mathematische Forschung mithilfe des Beweisassistenten Lean 4 formalisiert werden kann.
Das Programm der Masterclass setzte sich aus Vorträgen am Morgen und praktischen Coding Sessions am Nachmittag zusammen. Die Vorträge boten einführende Einblicke in die Kondensierte Mathematik sowie in Live-Coding mit wichtigen Hinweisen zur effektiven Nutzung von Lean. Die Coding-Sessions bestanden aus praktischen Übungen in Lean, in denen die Teilnehmenden die Möglichkeit hatten, an dem Projekt der Formalisierung der Kondensierten Mathematik in Lean aktiv mitzuwirken. Die Verwendung eines Beweisassistenten auf diesem Niveau war eine hochinteressante, aber auch fordernde Erfahrung. Vermeintlich „triviale“ Zwischenschritte erforderten nicht nur Kenntnisse im Umgang mit Lean, sondern teils auch substanzielle mathematisch Ideen. Lean lässt keine Lücken zu, keine Berufung darauf, dass etwas intuitiv offensichtlich ist. Alles muss bis ins letzte Detail begründet sein — und der dafür notwendige Detailgrad ist weit größer als es in nicht-formalisierter Mathematik der Fall ist.
Die Ergebnisse der Woche (gemeinsam erarbeitet von den Teilnehmenden und Organisatoren der Veranstaltung) sollen in mathlib, der mathematischen Bibliothek von Lean, einfließen. mathlib ist ein kollaboratives Projekt mit bisher über 200 Mitwirkenden und enthält bereits einen Großteil des Standard-Curriculums eines Mathematik-Grundstudiums. Gemeinschaftsprojekte von dieser Größe sind ein Novum in der Mathematik.
Neben den offiziellen Veranstaltungen boten die Mittagspausen und Pausengespräche wertvolle Gelegenheiten zum Austausch. Themen wie eine etwaige Interaktion von Künstlicher Intelligenz und Beweisassistenten wie Lean sowie das Potenzial der Digitalisierung von Mathematik wurden angeregt diskutiert. Aber was haben Beweisassistenten mit KI zu tun? Eine mögliche erste Antwort auf diese weitreichende Frage ist die folgende: Ein grundsätzliches Problem aktueller Modelle der KI, insbesondere von large language models (LLMs) wie ChatGPT, ist, dass sie für solche Aufgaben, die inhärent logisches Denken erfordern, im Wesentlichen ungeeignet sind. Das ist nicht überraschend, denn Ziel dieser Algorithmen ist schließlich das Modellieren natürlicher Sprache, und nicht von Logik. Beweisassistenten hingegen sind genau dafür entwickelt worden, logische Argumente (d.h. Beweise) auf ihre Richtigkeit zu überprüfen. Lean lässt keine „Halluzinationen“ zu, wie sie bei LLMs beobachtet werden.
Für mich persönlich war die Teilnahme eine inspirierende Erfahrung. Nicht nur erfährt die formalisierte Mathematik wachsende Bedeutung vor dem Hintergrund des Potenzials digitalisierter Mathematik. Sie ermöglicht auch einen frischen Blick auf das mathematische Beweisen selbst. Darüber hinaus verspricht die Kondensierte Mathematik (auf rein mathematischer Ebene) neue Methoden und Paradigmen im Bereich der Funktionalanalysis, in welchem ich aktuell meine Masterarbeit schreibe. Auch in dieser Hinsicht habe ich von der Masterclass profitiert. Diese wichtige Erfahrung wurde mir durch das Reisekostenstipendium der Bonner Universitätsstiftung ermöglicht.“
Ein Bericht von Benedikt Peterseim, 4. Juli 2023