David Roe ’06 und Andrew Sutherland ’90, PhD ’07, beide Forscher am MIT Department of Mathematics, sind unter den ersten Empfängern der AI for Math-Stipendien von Renaissance Philanthropy und XTX Markets. Zusammen mit Chris Birkbeck von der University of East Anglia erhalten sie Fördermittel, um die automatisierte Beweisführung zu stärken, indem sie die L-Functions and Modular Forms Database (LMFDB) mit der Lean4-Mathematikbibliothek mathlib verbinden. Weitere vier ehemalige MIT-Absolventen – Anshula Gandhi ’19, Viktor Kunčak SM ’01, PhD ’07, Gireeja Ranade ’07 und Damiano Testa PhD ’05 – wurden für eigene Projekte ausgezeichnet. Die ersten 29 geförderten Projekte zielen darauf ab, KI-Systeme zu entwickeln, die mathematische Entdeckungen voranbringen, insbesondere bei der Formalisierung von Beweisen, der Identifikation von Beweiszielen und der Nutzung großer mathematischer Datenbanken. Die LMFDB ist eine umfassende, gemeinsam entwickelte Online-Enzyklopädie moderner Zahlentheorie mit über 109 konkreten mathematischen Aussagen, während mathlib eine communitygetragene, formale Bibliothek für den Lean-Theorembeweiser darstellt, die etwa 105 mathematische Resultate enthält. Sutherland und Roe sind als Managing Editors der LMFDB tätig. Ihr Ziel ist es, Werkzeuge zu entwickeln, die es mathlib ermöglichen, direkt auf die LMFDB zuzugreifen. Dadurch wird ein riesiger Pool an bereits existierender, nicht formalisierter mathematischer Kenntnis für Beweissysteme nutzbar – ohne dass die gesamte Datenbank vorab formalisiert werden muss. „Automatisierte Theorembeweiser sind technisch aufwändig, aber unterfinanziert“, sagt Sutherland. Mit KI-Technologien wie großen Sprachmodellen sinkt die Einstiegshürde für solche formalen Systeme, sodass auch praktizierende Mathematiker sie nutzen können. Roe betont, dass die Menge an Fakten, die bei der Suche nach einem Beweis berücksichtigt werden könnten, exponentiell größer ist als die Menge, die tatsächlich formalisiert werden muss. Die Integration der LMFDB in mathlib ermöglicht es Beweisassistenten, gezielte Ansätze zu finden, basierend auf bereits verifizierten Berechnungen. Ein zentrales Argument für die Zusammenarbeit ist die Effizienz: Die LMFDB enthält Ergebnisse, die Tausende CPU-Jahre an Rechenzeit erforderten. Durch den Zugriff auf diese Daten spart man erhebliche Ressourcen und kann beispielsweise nach Beispielen oder Gegenbeispielen suchen, ohne vorher wissen zu müssen, wie groß der Suchraum ist. Zudem sind mathematische Datenbanken sorgfältig kuratiert – ein entscheidender Vorteil gegenüber zufälligen Datensätzen. Sutherland verweist auf den Erfolg von „murmurations“, einem mathematischen Entdeckungsergebnis, das durch maschinelles Lernen aus Daten der LMFDB gewonnen wurde, insbesondere durch die Berücksichtigung des „Conductors“ bei elliptischen Kurven. Zukünftige Schritte umfassen die Bildung eines Teams, die Zusammenarbeit mit den Communities der LMFDB und mathlib, die Formalisierung grundlegender Definitionen zu elliptischen Kurven, Zahlkörpern und modularen Formen sowie die Entwicklung von Schnittstellen, um LMFDB-Suchen direkt innerhalb von mathlib durchzuführen. Roe ruft MIT-Studenten dazu auf, sich zu beteiligen. Industrieexperten sehen in der Initiative eine Schlüsselrolle für die Zukunft der Mathematik: Die Kombination aus formaler Mathematik und KI könnte die Entdeckungsgeschwindigkeit erheblich steigern. Unternehmen wie XTX Markets und Stiftungen wie Renaissance Philanthropy setzen auf die langfristige Wirkung solcher Projekte, die nicht nur Forschung beschleunigen, sondern auch neue Standards für mathematische Sicherheit und Reproduzierbarkeit setzen. Die MIT-Verbindung unterstreicht die institutionelle Stärke in der Schnittstelle zwischen Mathematik, Informatik und KI.