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

Die MIT-Mathematiker David Roe und Andrew Sutherland wurden zu Empfängern der AI for Math-Stipendien ernannt, einem von Renaissance Philanthropy und XTX Markets ins Leben gerufenen Förderprogramm. Als Mitglieder des Fachbereichs Mathematik des 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 bahnbrechende Projekte finanziert werden, bei denen KI die Aufgabe hat, das Gebiet der Mathematik neu zu gestalten. Es geht darum, Mathematikern die Werkzeuge an die Hand zu geben, um KI-Systeme zu entwickeln, die die Entdeckungsgeschwindigkeit erhöhen und die formale Argumentation 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 verwendet die mathlib, eine umfassende Bibliothek, die von einer großen internationalen Gemeinschaft betrieben wird, den Lean-Theorembeweiser, um die Gültigkeit jedes logischen Schrittes in einem Beweis zu überprüfen. Mit etwa 100.000 mathematischen Ergebnissen ist sie im Grunde eine Goldgrube mathematischer Erkenntnisse.

Auf der anderen Seite gibt es die LMFDB, eine riesige digitale Enzyklopädie der modernen Zahlentheorie. Mit mehr als einer Milliarde mathematischer Aussagen und Datenpunkten ist sie für professionelle und angehende Mathematiker gleichermaßen eine unverzichtbare Ressource. Es ist eine gewaltige Aufgabe, diesen kolossalen Datenberg zu bewältigen, aber mit Roe und Sutherland als leitende Redakteure der LMFDB haben wir genau die richtigen Leute für diese Aufgabe.

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 primäre Ziel ist es, die umfangreichen zahlentheoretischen Fakten der LMFDB in mathlib zu nutzen. Diese Integration würde sowohl KI-Agenten als auch menschlichen Mathematikern eine uneingeschränkte Erkundung des mathematischen Universums ermöglichen. Um dies zu erreichen, plant das Team nicht, die gesamte LMFDB zu formalisieren - was extrem arbeitsintensiv wäre -, sondern will Werkzeuge entwickeln, die selektiv auf ihren Inhalt zugreifen. Diese Taktik, mit der die Kosten gesenkt werden sollen, bedeutet, dass nicht alle Informationen, die für die Aufstellung neuer Theoreme erforderlich sind, formal bewiesen werden müssen.

Moderne mathematische Theoreme, wie Andrew Wiles' Beweis von Fermats letztem Satz, stützen sich stark auf Rechenschritte, die nicht so einfach von Hand zu formalisieren sind. Genau aus diesem Grund sind mathematische Datenbanken wie die LMFDB von unschätzbarem Wert und dienen als wichtige Ressourcen für Mathematiker.

Die Bedeutung der Kuratierung von mathematischen Datenbanken kann gar nicht hoch genug eingeschätzt werden. Der Fokus der LMFDB auf den Dirigenten in elliptischen Kurven war beispielsweise ausschlaggebend für die kürzliche Identifizierung von Murmurationen elliptischer Kurven, ein Phänomen, das mit Hilfe von maschinellen Lernverfahren entdeckt wurde.

Die Zukunft der Mathematik gestalten

Roe und sein Team beabsichtigen, das ganze Unterfangen mit der Formalisierung der Definitionen zu beginnen, die die elliptischen Kurven-, Zahlenfeld- und Modulformabschnitte der LMFDB untermauern, und die Ausführung von LMFDB-Suchen innerhalb von mathlib zu ermöglichen. Ihr Plan eröffnet Studenten am MIT die Möglichkeit, an diesem großen mathematischen Abenteuer teilzunehmen.

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.