AI and the Future of Mathematics – Mathlog

An der Universität Münster findet im 14-tägigen Rhythmus dienstagabends um 20 Uhr ein Online-Seminar AI and the Future of Mathematics statt, das nächste Mal am kommenden Dienstag. (Die Veranstaltung findet auf Zoom statt, anmelden kann man sich hier.)

An den Veranstaltungen nehmen etwa 250 Leute teil und es gibt zwischendurch immer Pausen, in denen Gruppen von ca. 6 Teilnehmern jeweils zusammengeschaltet werden um über vorgegebene Themen zu diskutieren.

Den Vortrag in der vergangenen Woche hielt Ken Ono, der sich von seiner Professor an der University of Virginia hat beurlauben lassen um als leitender Mathematiker für das AI-Startup Axiom Math zu arbeiten, ein Unternehmen, dass sich hauptsächlich der Verifizierung KI-erzeugter (oder auch menschlich erzeugter) Beweise zu widmen scheint. (Er erwähnte, dass die Kosten der Lean-Verifizierung eines durchschnittlichen Papers bei etwa 150 Dollar liegen. Die Verifizierung eines gesamten Lehrbuchs habe vor einem Jahr noch etwa 100000 Dollar gekostet, inzwischen sei man eher bei 10000 Dollar.)

Er erzählte einiges Interessantes aus dem Inneren solcher KI-Unternehmen. Etwas überraschend fand ich, dass auch bei einem solchen explizit auf die Mathematik ausgerichteten Unternehmen nur wenige Mathematiker, dafür überwiegend Ingenieure arbeiten.

Zu den in jüngerer Zeit von KIs gelösten mathematischen Problemen meinte er, dass dort vor allem einfache Querverbindungen entdeckt worden wären und scheinbar schwere Probleme sich dank KI im Nachhinein als gar nicht so schwer herausgestellt hätten. Der Beweis von Erdös’s unit distance conjecture beruhe auf einer Verbindung von diskreter Geometrie und analytischer Zahlentheorie, die früher hätte gefunden werden können, wenn Forscher dieser beiden Gebiete miteinander zu tun gehabt hätten. Und bei der quasi-Riemannschen Vermutung müsse man im Nachhinein feststellen, dass der Beweis seit Jahrzehnten in Reichweite gewesen und die benötigten Methoden vorhanden gewesen seien, erst die KI habe die losen Enden verknüpft.

Häufig handele es sich um “constructions in mathematics with a little help from AI”. Die Verbesserung von 41% auf 67% bei den Nullstellen der Riemannschhen Zetafunktion, die auf der kritischen Geraden liegen, sei zwar ein beeindruckendes Resultat, verwende aber keine superneuen Ideen.

Als ein Beispiel brachte er die Entwicklungen zu beschränkten Lücken in Primzahlen. Die Goldbach-Vermutung sagt bekanntlich, dass es unendlich viele Paare von Primzahlen im Abstand 2 geben sollte. Das erste Resultat in dieser Richtung fand 2013 Yitang Zhang – er bewies, dass es unendlich viele Paare von Primzahlen im Abstand kleiner 70 Millionen gibt.
Die 70 Millionen waren nur eine griffige Zahl, tatsächlich rechnete jemand nach, dass die Arbeit einen Abstand 63374611 gibt. Innerhalb weniger Tage nach Erscheinen der Arbeit wurde dann von verschiedenen Autoren gezeigt, dass man mit deren Methoden noch deutlich bessere Werte bekommen kann. Zunächst verbesserte Tim Trudgian in einer 2-seitigen Arbeit den Wert auf knapp 60 Millionen und ein Beitrag von Terence Tao am folgenden Tag auf seinem Blog ergab sogar 4,88 Millionen. Einen weiteren Tag später startete dann ein Polymath-Projekt mit dem Ziel, diesen Wert weiter zu verbessern. Das gelang auch innerhalb von 2 Monaten mit einer Verbesserung auf 5414, später auf 4680, woraus eine Veröffentlichung des Autors D.H.J. Polymath resultierte.
Der spektakulärste Durchbruch kam dann aber nicht vom Polymath-Projekt, sondern fünf Monate später von James Maynard, einem Doktoranden aus Oxford. Er reduzierte den Wert auf 600. Anders als Zhang und die ihm folgenden Arbeiten des Polymath-Projekts benötigte er keine Verbesserung des Satzes von Bombieri und Winogradow über die Verteilung der Primzahlen in Restklassen, und er bewies nicht nur , sondern auch, dass für jedes h der Abstand zwischen h+1 aufeinanderfolgenden Primzahlen unendlich oft beschränkt bleibt. Tao nahm dies prompt zum Anlass, ein neues Polymath-Projekt zu starten, was den bewiesenen Wert auf 246 reduzierte.
Die neueste Entwicklung ist nun, dass Julia Stadlmann in einem am 31. August auf dem ArXiv erschienenen Artikel (nach zweijähriger Arbeit ohne Verwendung von KI) diesen Wert auf 240 reduzierte. Dieser Wert wurde danach von GPT-6 Astra innerhalb von drei Tagen – ohne neue Ideen gegenüber Stadlmanns Arbeit – auf 186 verbessert. Kurz: die neuen Ideen kamen immer noch von einem Menschen, die KI optimierte dann die Argumente um das mit diesen Ideen bestmögliche Resultat zu finden.