AlphaProof Nexus rozwiązał dziewięć problemów Erdősa. Wyniki trafiły do „Science”
AlphaProof Nexus, system Google DeepMind oparty na modelu Gemini 3.1 Pro, rozwiązał 9 z 353 otwartych problemów Paula Erdősa. Dwa z nich pozostawały nierozstrzygnięte od 56 lat. Wyniki prac ukazały się w recenzowanym czasopiśmie „Science”, a zespół udostępnił opracowane rozwiązania także w sieci. Repozytorium z materiałami udostępniono jeszcze przed publikacją artykułu w „Science” – zawiera ono formalizacje dowodów w Lean oraz opisy wyników w języku naturalnym.
Poza problemami Erdősa system dowiódł 44 hipotez powiązanych z bazą ciągów liczbowych OEIS, rozwiązał otwarte zagadnienie z zakresu geometrii algebraicznej oraz poprawił znane ograniczenie w optymalizacji min-max. Według informacji podanych przez DeepMind model doszedł również samodzielnie do dziewięciu rozwiązań problemów Erdősa, bez wsparcia wyspecjalizowanego narzędzia AlphaProof.
Proces dowodzenia opiera się na interakcji ze środowiskiem formalnym. AlphaProof Nexus przygotowuje i modyfikuje zapis w języku Lean, który automatycznie weryfikuje poprawność logiczną kolejnych kroków i zwraca komunikaty o błędach. W przypadku trudniejszych podproblemów system może dodatkowo odwołać się do algorytmów przeszukiwania AlphaProof.
Praca w „Science” ilustruje też odmienne podejście do upubliczniania rezultatów generowanych przez AI. Podczas gdy OpenAI udostępniło niedawno setki matematycznych dowodów bezpośrednio na GitHubie bez zgłaszania ich do publikacji w pismach akademickich, DeepMind zdecydowało się poddać swój artykuł standardowej procedurze recenzenckiej.
