Christoph Thiele und Floris van Doorn von der Universität Bonn erhalten einen mit 6,4 Millionen Euro dotierten ERC Synergy Grant

Können Beweise aus mathematischer Spitzenforschung in Zukunft mit zumutbarem menschlichen Aufwand so aufbereitet werden, dass sie vom Computer in Echtzeit verifiziert werden können? Dazu wollen Prof. Dr. Christoph Thiele und Prof. Dr. Floris van Doorn vom Exzellenzcluster Hausdorff Center for Mathematics (HCM) der Universität Bonn beitragen. Beide Forschende haben gemeinsam einen begehrten Synergy Grant des Europäischen Forschungsrates (ERC) eingeworben. In den nächsten sechs Jahren fördert die Europäische Union das Projekt „Harmonic Analysis with Lean Formalization“ (HALF) mit insgesamt 6,4 Millionen Euro. Lean ist eine relativ neue Programmiersprache, die sich zunehmend als Standard für die mathematische Formalisierung etabliert.

HALF befasst sich mit zentralen und seit langem offenen Problemen der harmonischen Analysis, wobei der Schwerpunkt auf multilinearen und nichtlinearen Operatoren liegt. Diese grundlegenden Fragen finden auch Anwendung in anderen mathematischen und interdisziplinären Bereichen wie der Ergodentheorie und der Quanteninformationsverarbeitung. Die neuen Resultate von HALF sollen mit Hilfe von Computern in der Sprache Lean verifiziert werden.

„Als erstes Projekt seiner Art ist HALF ein Meilenstein auf dem Weg zur routinemäßigen Verwendung von Computerverifizierung in der mathematischen Forschung“, sagt Prof. Dr. Floris van Doorn vom Mathematischen Institut der Universität Bonn. Das Vorhaben produziere auch dringend benötigtes Trainingsmaterial für erwartete Anwendungen der künstlichen Intelligenz (KI), die in Zukunft den Verifizierungsprozess unterstützen und automatisierte Werkzeuge für rigorose Entdeckungen in der Mathematik bereitstellen soll.

Formalisierung ist wichtig für die mathematische Forschung und KI-Anwendungen

„Es ist im Prinzip möglich, einen mathematischen Beweis so sorgfältig auszuformulieren und zu kodieren, dass ein Computer die Korrektheit des Beweises zertifizieren kann“, erläutert van Doorns Instituts- und Projektleiterkollege Prof. Dr. Christoph Thiele. Von einer standardmäßigen Verwendung dieser Formalisierung ist man jedoch noch weit entfernt. „Im Rahmen der Schulmathematik kann man das schon ganz ordentlich praktizieren“, sagt Thiele. „In der mathematischen Forschung hingegen ist es bisher noch zu aufwändig, Beweise für die Computer-Verifizierung aufzuarbeiten.“

In den nächsten sechs Jahren will Prof. Thiele diese Forschung in der Harmonischen Analysis vorantreiben und in Zusammenarbeit mit den Experten in Prof. van Doorn's Arbeitsgruppe formalisieren. Die Forschenden ergänzen sich dabei hinsichtlich ihrer Expertise. Beide sind Mitglied im Exzellenzcluster Hausdorff Center for Mathematics (HCM) und stehen dem Transdisziplinären Forschungsbereich „Modelling“ der Universität Bonn nahe.

„Unser Ziel ist, dass eingereichte Forschungsergebnisse bereits auf Korrektheit geprüft sind, bevor ein Gutachter über die Qualität der Arbeit befinden muss“, sagt Prof. van Doorn. Möglicherweise wird KI in der Zukunft mathematische Beweise führen. Um diesen Beweisen ohne zusätzlichen Aufwand vertrauen zu können, ist eine Formalisierung durch die KI selbst unbedingt erforderlich. Weltweit in KI führende Unternehmen und viele Startups interessieren sich bereits für "Mathlib", die Standardbibliothek an existierendem mathematischen Schul- und grundlegendem Hochschulwissen, die van Doorn und Kollegen aufbauen, und die HALF durch Einträge in Harmonische Analysis erweitern wird.

Vielbeachtetes Pilotprojekt zeigt den Weg

„Wir haben im letzten Jahr ein Pilotprojekt durchgeführt, um die Machbarkeit unseres Vorhabens zu beweisen“, berichtet Thiele. Als seine Forschungsgruppe ein neues Resultat im Bereich der Harmonischen Analysis erzielt hatte, erkannte van Doorn, dass sich dieses besonders gut für ein Formalisierungsprojekt eignete. Damit würde ein berühmtes klassisches Resultat von L. Carleson aus dem Jahr 1966, das bisher nicht formalisiert war, ebenfalls verifiziert. Das Projekt erforderte eine enge Zusammenarbeit zwischen Thiele und van Doorn und wurde weltweit von vielen Mathematikern verfolgt. Auch dank eines Dutzend Freiwilliger aus der internationalen Lean-Gemeinschaft war das Projekt deutlich schneller fertig als gedacht. Im Projekt HALF werden solche Arbeiten in Zukunft innerhalb der Forschungsgruppe selbst durchgeführt. Die Prozesse sollen im Laufe der Zeit verbessert und beschleunigt werden.

Zu den Personen:

Christoph Thiele studierte Mathematik an den Universitäten Darmstadt und Bielefeld, promovierte an der Yale University und wurde an der Universität Kiel habilitiert. 1998 bis 2012 war er Professor an der University of California in Los Angeles. Seitdem ist er Hausdorff Chair an der Universität Bonn. Er wurde mehrfach ausgezeichnet, unter anderem mit dem Salem Prize und dem Humboldt-Forschungspreis, und wurde 2002 zum internationalen Mathematikerkongress als Sprecher eingeladen.

Floris van Doorn studierte Mathematik an der Utrecht University und promovierte an der Carnegie Mellon University. Nach Stationen in Pittsburgh und Paris-Saclay nahm er 2023 einen Ruf an die Universität Bonn an. Er ist einer der Pioniere der Formalisierung mit Lean und einer der Verantwortlichen des internationalen Mathlib-Projektes. Zu seinen Preisen zählt der Skolem Award, den er in diesem Jahr erhielt.