Der Agent lässt ein Sprachmodell, Gemini 3.1 Pro, Beweisentwürfe in Lean schreiben und überarbeiten; nach jedem Schritt prüft der Lean-Compiler, seine Fehlermeldungen fließen in den nächsten Versuch. Gemini 3.0 Flash bewertet Zwischenstände, bei Bedarf hilft der spezialisierte Beweiser AlphaProof. Die stärkste Konfiguration kostete laut Paper einige hundert Dollar je Problem. Ein Vorabdruck stand seit dem 21. Mai 2026 auf arXiv; neu ist die begutachtete Fassung in Science.
Zwei der gelösten Fragen hatten Erdős und Sárközy 1970 gestellt, sie waren also 56 Jahre offen; Problem 125 war seit 1996 ungelöst. Neben den OEIS-Vermutungen nennt das Paper Einsätze in laufender Forschung zu Kombinatorik, Optimierung, Graphentheorie, algebraischer Geometrie und Quantenoptik. Ein einfacher Agent, der nur zwischen Modellentwurf und Lean-Prüfung wechselt, löste dieselben neun Erdős-Probleme, war bei den schwersten aber teurer.
Lean sichert nur, dass ein Beweis die formalisierte Aussage trifft, nicht, dass diese dem ursprünglichen Problem entspricht. Das Team berichtet selbst, Formalisierungen korrigiert zu haben, etwa die Deutung von „Dichte“; Fachleute aus dem Team prüften jede Lean-Aussage gegen die ursprüngliche Vermutung. An 344 der 353 Erdős-Probleme scheiterte der Agent.
Josep Curto (Universitat Oberta de Catalunya) folgert gegenüber dem Science Media Centre Spanien, nicht die aufwendige Architektur treibe die Ergebnisse, sondern das Grundmodell zusammen mit der strengen Rückmeldung des Compilers; das System brauche weiter intensive Kontrolle durch Fachleute. Teodoro Calonge (Universität Valladolid) sieht noch erheblichen Raum für Verbesserungen.