Die MIT-Mathematiker David Roe und Andrew Sutherland wurden zu Empf\u00e4ngern der AI for Math-Stipendien ernannt, einem von Renaissance Philanthropy und XTX Markets ins Leben gerufenen F\u00f6rderprogramm. Als Mitglieder des Fachbereichs Mathematik des MIT werden sie diese Gelegenheit nutzen, um k\u00fcnstliche Intelligenz mit bahnbrechender mathematischer Forschung zu verbinden.<\/p>\n
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\u00f6hen und die formale Argumentation in einer Vielzahl mathematischer Bereiche verbessern. <\/p>\n
Im Rahmen dieser beeindruckenden Einf\u00fchrung 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\u00fcr L-Funktionen und modulare Formen (LMFDB) und die Lean4-Mathematikbibliothek (mathlib).<\/p>\n
Einerseits verwendet die mathlib, eine umfassende Bibliothek, die von einer gro\u00dfen internationalen Gemeinschaft betrieben wird, den Lean-Theorembeweiser, um die G\u00fcltigkeit jedes logischen Schrittes in einem Beweis zu \u00fcberpr\u00fcfen. Mit etwa 100.000 mathematischen Ergebnissen ist sie im Grunde eine Goldgrube mathematischer Erkenntnisse. <\/p>\n
Auf der anderen Seite gibt es die LMFDB, eine riesige digitale Enzyklop\u00e4die der modernen Zahlentheorie. Mit mehr als einer Milliarde mathematischer Aussagen und Datenpunkten ist sie f\u00fcr professionelle und angehende Mathematiker gleicherma\u00dfen eine unverzichtbare Ressource. Es ist eine gewaltige Aufgabe, diesen kolossalen Datenberg zu bew\u00e4ltigen, aber mit Roe und Sutherland als leitende Redakteure der LMFDB haben wir genau die richtigen Leute f\u00fcr diese Aufgabe. <\/p>\n
Der traditionelle Lernweg zum Verst\u00e4ndnis automatischer Theorembeweiser ist steil, r\u00e4umt Sutherland ein. Aufgrund der zunehmenden Verf\u00fcgbarkeit und Effektivit\u00e4t von gro\u00dfen Sprachmodellen (LLMs) und anderen KI-Tools ist der Lernprozess jedoch weniger einsch\u00fcchternd geworden und l\u00e4dt ein breiteres Publikum von Mathematikern ein, diese Systeme zu nutzen. <\/p>\n
Das prim\u00e4re Ziel ist es, die umfangreichen zahlentheoretischen Fakten der LMFDB in mathlib zu nutzen. Diese Integration w\u00fcrde sowohl KI-Agenten als auch menschlichen Mathematikern eine uneingeschr\u00e4nkte Erkundung des mathematischen Universums erm\u00f6glichen. Um dies zu erreichen, plant das Team nicht, die gesamte LMFDB zu formalisieren - was extrem arbeitsintensiv w\u00e4re -, 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\u00fcr die Aufstellung neuer Theoreme erforderlich sind, formal bewiesen werden m\u00fcssen. <\/p>\n
Moderne mathematische Theoreme, wie Andrew Wiles' Beweis von Fermats letztem Satz, st\u00fctzen 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\u00e4tzbarem Wert und dienen als wichtige Ressourcen f\u00fcr Mathematiker. <\/p>\n
Die Bedeutung der Kuratierung von mathematischen Datenbanken kann gar nicht hoch genug eingesch\u00e4tzt werden. Der Fokus der LMFDB auf den Dirigenten in elliptischen Kurven war beispielsweise ausschlaggebend f\u00fcr die k\u00fcrzliche Identifizierung von Murmurationen elliptischer Kurven, ein Ph\u00e4nomen, das mit Hilfe von maschinellen Lernverfahren entdeckt wurde. <\/p>\n
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\u00fchrung von LMFDB-Suchen innerhalb von mathlib zu erm\u00f6glichen. Ihr Plan er\u00f6ffnet Studenten am MIT die M\u00f6glichkeit, an diesem gro\u00dfen mathematischen Abenteuer teilzunehmen. <\/p>\n
Neben Roe und Sutherland wurden vier weitere Pioniere der Mathematik vom MIT - Anshula Gandhi, Viktor Kun\u010dak, Gireeja Ranade und Damiano Testa - in Anerkennung ihrer innovativen Arbeit auf diesem Gebiet mit den AI for Math-Stipendien ausgezeichnet. <\/p>\n