Künstliche Intelligenz hat ein 56 Jahre lang ungelöstes mathematisches Problem gelöst und die entsprechende Forschungsarbeit wurde in der Fachzeitschrift *Science* veröffentlicht. DeepMind hat es richtig gemacht, die Ergebnisse dem Peer-Review zu unterziehen.

Der Kreis der KI-Mathematik ist in letzter Zeit wirklich sehr lebhaft.

Kaum hat OpenAI auf einen Schlag 722 mathematische Beweise veröffentlicht und damit einen kollektiven Widerstand aus dem Mathematikerkreis ausgelöst, da erschien die mathematische Forschung von Google DeepMind bereits in 《Science》.

Die eine Seite wirft massenhaft zu prüfende Manuskripte heraus und überlässt die gesamte Last der Korrektur den Mathematikern;

Die andere Seite hat hingegen mehrere Monate geduldig gewartet, den Peer-Review-Prozess ordnungsgemäß durchlaufen und die Prüfung durch die Mathematikgemeinschaft akzeptiert.

Zwei Mathematiker der Carnegie Mellon University und der University of South Carolina haben eigens einen Kommentar im selben Heft von 《Science》 veröffentlicht: *KI für die mathematische Forschung ist angekommen*.

Nun gut, während die Seite von OpenAI noch heftig über die Veröffentlichungsmethode mathematischer Beweise streitet, hat DeepMind bereits die öffentliche Anerkennung von Mathematikern erhalten.

Der Hauptakteur von DeepMind diesmal ist AlphaProof Nexus, ein von Gemini angetriebenes KI-Framework für mathematische Beweismittel-Agenten.

Es hat 9 offene Probleme von Erdős gelöst, von denen zwei ganze 56 Jahre lang ungelöst geblieben sind.

Neben diesen 9 Problemen hat es nebenbei 44 Vermutungen in der Enzyklopädie der Ganzzahlenfolgen OEIS bewiesen, ein seit 15 Jahren ruhendes schwieriges Problem der algebraischen Geometrie gelöst und eine seit langem verwendete theoretische Grenze im Bereich der konvexen Optimierung verbessert.

Übrigens ist DeepMind bereits ein alter Bekannter von 《Science》.

Diese mathematische Arbeit hat insgesamt 20 Autoren, darunter Aja Huang, der auch einer der Kernforscher von AlphaGo in jenen Jahren war.

Überwindung eines 56 Jahre alten, mit Preisgeld ausgezeichneten Problems

DeepMind hat 353 Probleme aus den bereits formalisierten Versionen in Lean ausgewählt und sie AlphaProof Nexus zur Bearbeitung übergeben, wobei am Ende 9 Probleme erfolgreich gelöst wurden.

Eines davon, Erdős #12, wurde 1970 vorgeschlagen und ist bis heute 56 Jahre lang ungelöst geblieben.

Die Frage lautet:

Ist es möglich, eine unendlich große Menge ganzer Zahlen zu finden, sodass die Zahlen in der Menge strenge Teilbarkeitsbeschränkungen erfüllen und gleichzeitig eine ausreichend große Größe beibehalten?

Genauer gesagt: Wählt man beliebig drei geeignete ganze Zahlen aus, darf die kleinere die Summe der beiden größeren nicht teilen, und außerdem darf die Menge nicht zu dünn besiedelt sein.

Seit 1970 konnte niemand die vollständige Konstruktion dieser Menge angeben. Es gab zwar verschiedene lokale Fortschritte, aber es gelang nie, sie zu einer Gesamtlösung zusammenzufügen.

Die Lösung von AlphaProof Nexus diesmal erfolgt durch blockweise Konstruktion.

Zuerst teilt man die zu konstruierende unendliche Menge in einzelne Blöcke ganzer Zahlen auf;

Anschließend nutzt man den chinesischen Restsatz und kombiniert ihn mit der Eigenschaft von Mengen, die arithmetische Folgen mit drei Elementen vermeiden, sodass jeder Block die lokalen Teilbarkeitsbedingungen erfüllt;

Am Ende fügt man alle Blöcke wieder zu einer vollständigen unendlichen Menge zusammen.

Darüber hinaus gibt es noch Erdős #125, das 1996 vorgeschlagen wurde und seit 30 Jahren keine endgültige Lösung hat.

Stellen Sie sich zwei Mengen von Zahlen vor:

Die erste Menge enthält ausschließlich „ganze Zahlen, die im Dreiersystem nur aus den Ziffern 0 und 1 bestehen“;

Die zweite Menge enthält ausschließlich „ganze Zahlen, die im Vierersystem nur aus den Ziffern 0 und 1 bestehen“;

Bildet man die Summe aus je zwei beliebigen Zahlen aus diesen beiden Mengen, erhält man eine neue Menge.

Die Frage lautet: Ist die Häufigkeit, mit der die Zahlen dieser neuen Menge in den natürlichen Zahlen auftreten (mathematisch als untere Dichte bezeichnet), positiv?

Intuitiv könnte man annehmen, dass die in beiden Mengen enthaltenen Zahlen ohnehin nicht sehr zahlreich sind, sodass ihre Summe auch ziemlich dünn besiedelt sein sollte.

Aber wie dünn besiedelt ist sie genau? Ist sie so dünn, dass die Dichte auf Null sinkt, oder behält sie eine gewisse positive Dichte?

Der Unterschied dazwischen ist sehr subtil, und seit der Vorschlag im Jahr 1996 gab es keine endgültige Antwort.

Die Antwort von AlphaProof Nexus lautet: Die untere Dichte ist Null.

Der Schlüssel des Beweises liegt darin, dass log₄/log₃ eine irrationale Zahl ist.

Das bedeutet, dass Potenzen von 3 und Potenzen von 4 in geeigneten Skalen beliebig nah beieinander liegen können.

Unter Ausnutzung dieser Tatsache hat die KI ein induktives Argument zur Verdünnung konstruiert: Man findet ständig zwei fast ausgerichtete Skalen, sodass die Dichte der Menge schrittweise abnimmt, bis sie vollständig auf Null sinkt.

Damit wird schließlich bewiesen, dass die untere Dichte dieser Menge tatsächlich Null ist.

Erdős #846, vorgeschlagen 1992, hat Menschen 34 Jahre lang blockiert.

Dies ist ein Problem über ebene Punktmengen.

Ist es möglich, eine unendlich große ebene Punktmenge zu konstruieren, die eine sehr seltsame Eigenschaft hat:

Wählt man beliebig endlich viele Punkte daraus aus, kann man immer eine ausreichend große Teilmenge finden, in der keine drei Punkte auf einer Geraden liegen.

Aber wenn man versucht, die gesamte unendliche Punktmenge in endlich viele Mengen aufzuteilen, in denen überhaupt keine drei Punkte auf einer Geraden liegen, gelingt das nicht.

Einfach ausgedrückt: Lokal wirkt alles recht ordentlich, aber insgesamt lässt es sich nie vollständig sauber aufteilen.

Der von AlphaProof Nexus vorgelegte Beweis verwendet eine raffinierte mathematische Konstruktion.

Es bildet die Kanten eines unendlichen vollständigen Graphen auf Punkte in der Ebene ab, kodiert die Koordinaten mit Polynomausdrücken und kombiniert sie mit relevanten Ergebnissen aus der unendlichen Kombinatorik, um den Beweis abzuschließen.

Ein Problem der ebenen Geometrie wurde schließlich in ein Problem der Graphentheorie und Kombinatorik umgewandelt und gelöst.

Neben diesen drei Problemen gibt es sechs weitere in Bereichen wie der Konstruktion von Teilbarkeitsmengen, den Lücken der Van-der-Waerden-Zahlen, isolierten Punkten von Sidon-Mengen und der Dichte von Mengenaufteilungen.

Nachdem es die Probleme von Erdős gelöst hatte, ging es weiter zur Enzyklopädie der Ganzzahlenfolgen OEIS und bewies dort 44 offene Vermutungen.

Sogar die algebraische Geometrie und die konvexe Optimierung wurden nicht ausgelassen.

Es löste zudem ein seit 15 Jahren offenes Problem über die logarithmische Konkavität der Hilbert-Funktion in der algebraischen Geometrie und verbesserte eine theoretische Grenze für die verankerte Gradientenabstiegsmethode in der konvexen Optimierung.

Gemini schreibt Beweise, Lean korrigiert

Die zentrale Arbeitsweise von AlphaProof Nexus lautet:

Gemini 3.1 Pro schreibt Beweise → Lean prüft → Fehlermeldung wird an Gemini zurückgespielt → Beweis wird geändert → erneute Prüfung, bis alle Beweise vollständig bestanden sind.

Um diesen Prozess herum hat DeepMind vier Agent-Konfigurationen entwickelt.

Der einfachste Agent A besteht aus mehreren unabhängigen Sub-Agenten, die gleichzeitig versuchen, Beweise zu erstellen.

Jeder Sub-Agent generiert über Gemini Lean-Code und ändert ihn ständig anhand der Rückmeldungen des Compilers.

Während des gesamten Prozesses gibt es keine zusätzlichen Hilfswerkzeuge, es wird rein durch den Zyklus aus Code-Schreiben und Fehlerprüfung gearbeitet.

Agent B ergänzt um AlphaProof.

Dies ist ein spezielles mathematisches Beweissystem, das DeepMind zuvor entwickelt hat.

Bei schwierig zu lösenden Teilproblemen kann der Agent AlphaProof aufrufen, um gezielt zu suchen.

Agent C führt eine evolutionäre Suche ein.

Mehrere Agenten legen verschiedene Beweisentwürfe in eine gemeinsame Datenbank ein, danach vergleicht ein Bewertungs-Agent auf Basis von Gemini 3.0 Flash die Entwürfe hinsichtlich ihrer Plausibilität, Klarheit und Neuartigkeit.

Das System fasst die Vergleichsergebnisse zu einer Elo-Bewertung zusammen und wählt daraufhin die Beweiswege aus, die es wert sind, weiter erforscht zu werden.

Agent D ist die vollständige Version.

Er integriert sowohl AlphaProof als auch die evolutionäre Suche und war die Hauptkonfiguration, die bei dieser Massenexploration offener Probleme verwendet wurde.

Eigentlich sollte mit mehr Funktionen die Leistung besser werden.

Aber DeepMind hat später eine Reihe von kontrollierten Experimenten durchgeführt und festgestellt, dass der einfachste Agent A tatsächlich alle 9 Erdős-Probleme lösen kann.

Ohne evolutionären Algorithmus, ohne AlphaProof, nur mit einem Agenten A, der aus einem LLM-Zyklus plus Compiler-Rückmeldungen besteht, ist es bei schwierigen Problemen nur etwas kostspieliger.

Bei schwierigen Problemen wie #125 und #138 ist die Kosteneffizienz der vollständigen Version des Agenten etwa 2 bis 5 Mal höher als die der Basisversion.

Zusammengerechnet liegen die Kosten für die Lösung eines Problems durch AlphaProof Nexus diesmal bei etwa mehreren hundert Dollar…

Der gesamte Lean-Beweiscode diesmal ist öffentlich zugänglich und kann von außen direkt eingesehen werden.