(openPR) 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.
„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.
„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.
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.
wissenschaftliche Ansprechpartner: Prof. Dr. Christoph Thiele Mathematisches Institut Universität Bonn Tel. +49 (0) 228 73-62254 E-Mail:
Prof. Dr. Floris van Doorn Mathematisches Institut Universität Bonn Tel. +49 (0)228 73-2951 E-Mail:
Disclaimer: Für den obigen Pressetext inkl. etwaiger Bilder/ Videos ist ausschließlich der im Text angegebene Kontakt verantwortlich. Der Webseitenanbieter distanziert sich ausdrücklich von den Inhalten Dritter und macht sich diese nicht zu eigen. Wenn Sie die obigen Informationen redaktionell nutzen möchten, so wenden Sie sich bitte an den obigen Pressekontakt. Bei einer Veröffentlichung bitten wir um ein Belegexemplar oder Quellenennung der URL.
