Google DeepMinds AlphaProof Nexus hat neun von 353 offenen Erdős-Problemen selbstständig gelöst. Zwei davon beschäftigten Mathematiker seit 56 Jahren, wie die nun im Fachblatt Science veröffentlichte Studie zeigt.
Gemini schreibt, Lean prüft
AlphaProof Nexus verbindet mehrere KI-Agenten mit Gemini 3.1 Pro und der formalen Sprache Lean. Das Modell entwirft Beweise, überarbeitet fehlerhafte Stellen und erhält nach jedem Schritt eine Rückmeldung vom Lean-Compiler.
Lean prüft dabei jeden logischen Schritt. Erst wenn kein unbewiesener Platzhalter übrig ist und der gesamte Code kompiliert, akzeptiert AlphaProof Nexus einen Beweis.
Die aufwendigste Variante koordiniert mehrere Agenten über ein evolutionäres Suchverfahren und kann AlphaProof als spezialisierten »Beweis-Agenten« aufrufen. Ein deutlich einfacherer Aufbau aus unabhängigen Gemini-Agenten und Lean-Prüfung löste im Nachtest dieselben neun Erdős-Probleme, benötigte bei den schwierigsten Aufgaben aber mehr Rechenaufwand.
Zu den gelösten Aufgaben gehört ein Problem aus dem Jahr 1970. Dafür konstruierte AlphaProof Nexus eine unendliche Menge von Zahlen, die strenge Regeln zur Teilbarkeit erfüllt und zugleich eine vorgegebene Dichte erreicht.
Anzeige
44 weitere Vermutungen bewiesen
Bei einer zweiten Prüfung bewies AlphaProof Nexus 44 von 492 offenen Vermutungen aus der Zahlenfolgen-Datenbank OEIS.
Darüber hinaus beantwortete es eine seit 15 Jahren offene Frage zu Hilbert-Funktionen in der algebraischen Geometrie und verbesserte eine bekannte Grenze in der Min-Max-Optimierung.
Die Forscher veröffentlichten sämtliche Lean-Beweise in einem GitHub-Repository. Ausgewählte Ergebnisse liegen zusätzlich als von Menschen geschriebene Beweise vor, sodass Mathematiker neben der formalen Prüfung auch den Lösungsweg nachvollziehen können.
Die Veröffentlichung fällt in eine hitzige Debatte über KI-generierte Mathematik. OpenAI stellte am 6. Oktober Hunderte Ergebnisse in mehr als 700 Dateien auf GitHub, worauf die Association for Human Mathematics zum Boykott des Unternehmens aufrief.
Die DeepMind-Arbeit durchlief dagegen das Begutachtungsverfahren von Science und liefert ihre Beweise in maschinell prüfbarer Form.
