MIT-Mathematiker erhalten AI for Math Grant für die Verbindung von Datenbanken und Theorembeweisern

Die MIT-Mathematiker David Roe und Andrew Sutherland wurden als Empfänger der „AI for Math“-Fördermittel ausgewählt, einem erstmals von Renaissance Philanthropy und XTX Markets ins Leben gerufenen Förderprogramm. Als Mitglieder des Fachbereichs Mathematik am MIT werden sie diese Gelegenheit nutzen, um künstliche Intelligenz mit bahnbrechender mathematischer Forschung zu verbinden.

Diese neue Initiative zielt darauf ab, mathematische Entdeckungen voranzutreiben, indem 29 wegweisende Projekte gefördert werden, bei denen jeweils KI eingesetzt wird, um das Fachgebiet der Mathematik neu zu gestalten. Dabei geht es darum, Mathematikern die Werkzeuge an die Hand zu geben, mit denen sie KI-Systeme entwickeln können, die die Geschwindigkeit neuer Entdeckungen steigern und das formale Denken in einer Vielzahl mathematischer Bereiche verbessern.

Im Rahmen dieser beeindruckenden Einführung planen Roe und Sutherland in Zusammenarbeit mit Chris Birkbeck von der University of East Anglia, ihren Zuschuss zu nutzen, um zwei wichtige mathematische Ressourcen miteinander zu verbinden: die Datenbank für L-Funktionen und modulare Formen (LMFDB) und die Lean4-Mathematikbibliothek (mathlib).

Mathematische Bereiche mit KI überbrücken

Einerseits nutzt die „mathlib“, eine umfassende Bibliothek, die von einer riesigen internationalen Community gepflegt wird, den Lean-Theorembeweiser, um die Gültigkeit jedes logischen Schritts in einem Beweis zu überprüfen. Mit rund 100.000 mathematischen Ergebnissen ist sie im Grunde eine Fundgrube für mathematische Erkenntnisse.

Auf der anderen Seite gibt es die LMFDB, eine gigantische digitale Enzyklopädie der modernen Zahlentheorie. Mit über einer Milliarde mathematischer Aussagen und Datenpunkten ist sie eine unverzichtbare Quelle für professionelle und angehende Mathematiker gleichermaßen. Sich in diesem kolossalen Datenberg zurechtzufinden, ist eine gewaltige Aufgabe, aber mit Roe und Sutherland als leitenden Redakteuren der LMFDB sind sie genau die richtigen Leute für diesen Job.

Entmystifizierung der Mathematik mit AI

Der traditionelle Lernweg zum Verständnis automatischer Theorembeweiser ist steil, räumt Sutherland ein. Aufgrund der zunehmenden Verfügbarkeit und Effektivität von großen Sprachmodellen (LLMs) und anderen KI-Tools ist der Lernprozess jedoch weniger einschüchternd geworden und lädt ein breiteres Publikum von Mathematikern ein, diese Systeme zu nutzen.

Das vorrangige Ziel besteht darin, die umfangreichen zahlentheoretischen Fakten der LMFDB für mathlib nutzbar zu machen. Diese Integration würde sowohl KI-Agenten als auch menschlichen Mathematikern eine uneingeschränkte Erforschung des mathematischen Universums ermöglichen. Um dies zu erreichen, plant das Team nicht, die gesamte LMFDB zu formalisieren – was äußerst arbeitsintensiv wäre –, sondern strebt vielmehr die Entwicklung von Werkzeugen an, die selektiv auf deren Inhalte zugreifen. Diese Vorgehensweise, von der man sich Kosteneinsparungen verspricht, bedeutet, dass nicht alle Informationen, die zur Aufstellung neuer Theoreme erforderlich sind, formal bewiesen werden müssen.

Moderne mathematische Theoreme, wie beispielsweise Andrew Wiles’ Beweis des letzten Satzes von Fermat, stützen sich in hohem Maße auf Rechenschritte, die sich von Hand nicht so einfach formalisieren lassen. Genau aus diesem Grund sind mathematische Datenbanken wie die LMFDB von unschätzbarem Wert und dienen Mathematikern als unverzichtbare Ressourcen.

Die Bedeutung der Kuratierung in mathematischen Datenbanken kann gar nicht hoch genug eingeschätzt werden. So war beispielsweise der Fokus der LMFDB auf den Leiter in elliptischen Kurven entscheidend für die kürzlich erfolgte Identifizierung von „Murmurationen“ in elliptischen Kurven – ein Phänomen, das mithilfe von Techniken des maschinellen Lernens entdeckt wurde.

Die Zukunft der Mathematik gestalten

Roe und sein Team beabsichtigen, das gesamte Vorhaben damit zu beginnen, die Definitionen zu formalisieren, die den Abschnitten „Elliptische Kurven“, „Zahlenkörper“ und „Modulformen“ der LMFDB zugrunde liegen und die Durchführung von LMFDB-Suchen innerhalb von mathlib ermöglichen. Ihr Plan eröffnet den Studierenden am MIT die Möglichkeit, Teil dieses großartigen mathematischen Abenteuers zu werden.

Neben Roe und Sutherland wurden vier weitere Pioniere der Mathematik vom MIT - Anshula Gandhi, Viktor Kunčak, Gireeja Ranade und Damiano Testa - in Anerkennung ihrer innovativen Arbeit auf diesem Gebiet mit den AI for Math-Stipendien ausgezeichnet.

Weitere Informationen über die KI für Mathematik-Stipendien finden Sie im vollständigen Artikel hier.