Google DeepMind veröffentlichte am 24. Mai eine Arbeit, in der ein LLM-Lean-Agenten-Zyklus beschrieben wird, der autonom 9 von insgesamt 353 offenen Erdős-Problemen löste – darunter einige, die seit über 50 Jahren ungelöst waren – sowie 44 von 492 offenen OEIS-Vermutungen bewies. Die Kosten pro Problem beliefen sich dabei lediglich auf einige hundert US-Dollar. Das System, das unter [2605.22763] Advancing Mathematics Research with AI-Driven Formal Proof Search detailliert beschrieben wird, kombiniert ein LLM zur Beweisgenerierung mit dem Lean-Verifikationscompiler, welcher jede logische Schrittfolge mechanisch überprüft. Erst nach Bestätigung durch Lean erfolgt eine menschliche Überprüfung. Zudem löste der Agent ein seit 15 Jahren offenes Problem aus der algebraischen Geometrie und entdeckte einen bisher unbekannten algorithmischen Parameter in der Optimierungstheorie.
Ein zentrales Ergebnis der Arbeit: Ein simpler Agent, der abwechselnd LLM-Generierungen und Compiler-Rückmeldungen nutzt, erreichte alle 9 Erfolge bei den Erdős-Problemen. Das vollständige System mit evolutionärer Suche und Reinforcement Learning übertraf ihn lediglich bei den schwierigsten Aufgaben – dies deutet darauf hin, dass Verbesserungen der Basis-Modelle wichtiger sind als komplexere Architekturen. Fehleranalysen zeigten, dass die KI häufig Lemmas „halluzinierte“ oder eigentliche Schwierigkeiten durch Umformulierungen als Hilfslemmas verschleierte; der Lean-Compiler erkannte diese Fehler automatisch, wo herkömmliche Beweismethoden versagt hätten. Aktuell konzentrieren sich die Erfolge auf Kombinatorik, Zahlentheorie und Optimierung – Bereiche, in denen die mathematische Bibliothek Mathlib von Lean am weitesten entwickelt ist; Probleme, die grundlegend neue Theorien erfordern, bleiben weiterhin unlösbar.
Gary Marcus bezeichnete den Ansatz als neurosymbolisch und nannte ihn „vorsichtiger und quantitativer“ als OpenAIs informelle Beweisarbeit; dies wirft die Frage auf, ob OpenAI seine eigene Ankündigung voreilig herausgab, weil man von DeepMinds Ergebnissen wusste. Nate Soares stellte fest, dass die Mainstream-Medien die Geschichte trotz ihres Ausmaßes weitgehend ignorierten – ein Zeichen für gesellschaftliches „Schlafwandeln“ angesichts transformativer KI-Entwicklungen. Der Beitrag erzielte innerhalb von 24 Stunden 2,6 Millionen Aufrufe.