Google DeepMind löst jahrzehntealte Matheprobleme
Google DeepMinds AlphaProof Nexus hat neun von 353 offenen Erdős Problemen selbstständig gelöst. Zwei der Aufgaben waren seit 56 Jahren ungelöst. Die Ergebnisse wurden in der Fachzeitschrift Science veröffentlicht.
Das System verbindet mehrere KI Agenten mit Gemini 3.1 Pro und der formalen Sprache Lean. Gemini erstellt die Beweise, Lean prüft jeden Schritt. Erst wenn der gesamte Code fehlerfrei kompiliert, wird ein Beweis akzeptiert. Nach Angaben der Forscher löste auch eine einfachere Variante dieselben neun Erdős Probleme, benötigte bei den schwierigsten Aufgaben aber mehr Rechenleistung.
Zusätzlich bewies AlphaProof Nexus 44 von 492 offenen Vermutungen aus der OEIS Datenbank. Außerdem 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 Beweise wurden in einem GitHub Repository veröffentlicht und teils auch in menschlich verfasster Form bereitgestellt.
