Google DeepMind hat mit seinem System AlphaProof Nexus nach eigenen Angaben neun bislang ungelöste Erdős-Probleme gelöst. Wie der Bericht von updater.news zusammenfasst, untersuchte das Team 353 offene Fragestellungen aus dem Umfeld des ungarischen Mathematikers Paul Erdős und erzielte bei neun davon einen vollständigen Beweis. Zusätzlich will das System 44 Vermutungen aus der OEIS, der Online-Encyclopedia of Integer Sequences, formal bewiesen haben. Das klingt spektakulär – und ist es in Teilen auch. Doch die nüchterne Zahl dahinter lautet: 344 der getesteten Probleme blieben ungelöst.
Wie das System arbeitet
Der Ansatz kombiniert zwei Komponenten. Zunächst schlägt das Sprachmodell Gemini 3.1 Pro Beweisschritte vor – also informelle mathematische Argumente, wie sie auch ein Mensch skizzieren würde. Diese Vorschläge werden anschließend an den Beweisassistenten Lean übergeben. Lean ist ein formaler Prüfer: Er akzeptiert nur Beweise, die sich lückenlos in maschinell überprüfbare Schritte zerlegen lassen. Reicht das Modell einen Beweis mit einer Lücke ein, verwirft Lean ihn automatisch. Dieses Zusammenspiel aus kreativem Vorschlagen und strenger maschineller Kontrolle ist der eigentliche methodische Kern der Arbeit.
Die Forschenden beschränkten sich jedoch nicht auf die automatische Prüfung. Bei den OEIS-Beweisen kontrollierten sie zusätzlich manuell, ob die Probleme korrekt formalisiert wurden und ob es sich tatsächlich um zuvor ungelöste Fragestellungen handelte. Dieser Schritt ist wichtig, denn ein formaler Beweis nützt wenig, wenn das zugrunde liegende Problem falsch übersetzt wurde. Die Kombination aus maschineller Verifikation und menschlicher Nachprüfung unterscheidet die Arbeit von reinen Benchmark-Erfolgen.
Was das Ergebnis bedeutet
Bemerkenswert ist vor allem die Verbindung von KI-generierter Vermutung und maschinell überprüfbarem Beweis. In der Mathematik zählt nicht die Plausibilität einer Argumentation, sondern ihre lückenlose Gültigkeit. Indem Lean jeden Schritt mechanisch prüft, sinkt das Risiko, dass ein Sprachmodell einen überzeugend klingenden, aber fehlerhaften Beweis liefert. Genau dieses Risiko ist bei rein textbasierten Modellen bekannt und berüchtigt.
Zugleich zeigt die Zahl der gelösten Fälle die Grenzen auf. Neun von 353 Aufgaben sind ein kleiner Anteil. Viele der verbleibenden Probleme dürften deutlich komplexer sein oder Beweistechniken erfordern, die sich nicht ohne Weiteres in kurze formale Schritte übersetzen lassen. Der Bericht nennt zudem die Rechenkosten: Für einen gelösten Erdős-Fall fielen einige hundert Dollar an Rechenleistung an. Das ist für einen einzelnen Beweis nicht wenig, auch wenn es die Größenordnung klassischer Forschungsbudgets nicht sprengt.
Menschliche Anleitung bleibt zentral
Die Autoren selbst betonen, dass menschliche Anleitung und sorgfältige Prüfung weiterhin wichtig bleiben. Das Modell liefert Vorschläge, Lean filtert Fehler heraus, und Menschen entscheiden, welche Probleme überhaupt untersucht werden und ob die Formalisierung stimmt. Von einem autonom forschenden Mathematiker ist das System damit weit entfernt. Es ist eher ein Werkzeug, das die Beweissuche beschleunigen kann, ohne die Verantwortung für Korrektheit abzugeben.
Für die Mathematik könnte der Ansatz dennoch langfristig interessant sein: Formale Beweisassistenten wie Lean gewinnen seit Jahren an Bedeutung, und wenn Sprachmodelle zuverlässig brauchbare Beweisskizzen liefern, ließe sich der aufwendige Formalisierungsprozess teilweise automatisieren. Ob sich dieser Nutzen auf große offene Probleme überträgt, ist offen.
Fazit
DeepMind zeigt mit AlphaProof Nexus einen sauberen methodischen Fortschritt: KI schlägt vor, ein formaler Prüfer kontrolliert, Menschen verifizieren. Neun gelöste Erdős-Probleme und 44 OEIS-Beweise sind ein reales Ergebnis, aber kein Durchbruch, der die Mathematik neu ordnet. Die eigentliche Botschaft ist die Verlässlichkeit der Verifikation – und die bleibt vorerst an menschliche Sorgfalt gekoppelt.
