Google: AI rozwiązała 9 problemów Erdősa, zapis zadań oceniali ludzie

8 października 2026 czasopismo Science opublikowało pracę zespołu Google DeepMind o agencie AlphaProof Nexus, który samodzielnie rozwiązał 9 z 353 otwartych problemów Erdősa. Na pytanie, czy AI potrafi rozwiązywać problemy matematyczne, wynik odpowiada: tak, w wąskim zakresie i pod kontrolą programu sprawdzającego. Dowody sprawdził komputer.

Problemy Erdősa to pytania matematyczne postawione przez Paula Erdősa i jego współpracowników, zebrane w bazie erdosproblems.com. Baza liczy ponad 1200 problemów. Agent dostał do rozwiązania 353 otwarte, zapisane już w ścisłym języku formalnym. Tylko taki zapis może sprawdzić komputer.

Agent, czyli program AI działający w kolejnych próbach, opiera się na modelu Gemini 3.1 Pro firmy Google. Model pisze szkic dowodu w Lean, programie do sprawdzania dowodów zapisanych w ścisłym języku formalnym, i poprawia go po każdym komunikacie o błędzie. Błędy prowadzą kolejną próbę.

Poza problemami Erdősa agent udowodnił 44 z 492 hipotez z bazy OEIS, internetowej encyklopedii ciągów liczbowych. Rozwiązał też otwarte pytanie z geometrii algebraicznej i poprawił znaną granicę w optymalizacji.

Lean gwarantuje poprawność dowodu względem zdania zapisanego w Lean. Josep Curto, dyrektor akademicki studiów magisterskich z analityki biznesowej na Otwartym Uniwersytecie Katalonii, zwraca uwagę, że nie gwarantuje on zgodności tego zdania z prawdziwym problemem. Błąd w zapisie dałby dowód innego zadania.

Po każdym rozwiązaniu eksperci z zespołu sprawdzali, czy zapis w Lean wiernie oddaje pierwotną hipotezę. Agent pomógł też wykrywać błędy zapisu. W problemach nr 125 i nr 741(i) znalazł dowody dla gęstości naturalnej, czyli udziału liczb zbioru wśród wszystkich liczb, więc autorzy zmienili pojęcie gęstości w pierwotnych opisach odpowiednio na dolną i górną. Po poprawce agent rozwiązał pytania ponownie.

Według autorów pracy formalna weryfikacja może służyć jako filtr wskazujący dowody warte przeglądu przez ludzi. Javier Aramayona, dyrektor Instytutu Nauk Matematycznych ICMAT w Hiszpanii, zwraca uwagę na powstanie ogromnego zbioru wyników uznanych za prawdziwe dzięki certyfikatowi poprawności. Nikt ich w pełni nie rozumie.

Wyniki DeepMind były publiczne przed publikacją w czasopiśmie: wersja robocza trafiła 21 maja 2026 na arXiv, serwer z pracami naukowymi. Serwis Science Media Centre Spain z komentarzami ekspertów oznacza pracę jako recenzowaną.

OpenAI opublikowało 6 października na GitHubie, platformie do przechowywania plików, repozytorium z 719 manuskryptami. Czasopisma ich nie dostały, pisze The Decoder.

Według OpenAI w Lean sformalizowano około 42 procent głównych wyników. Firma sama dopuszcza błędy w wynikach bez takiego zapisu. Trzy prace wycofała z powodu błędu znaku.

Oświadczenie organizacji Association for Human Mathematics ukazało się 7 października na blogu Terence'a Tao. Wzywa w nim matematyków do zakończenia pracy z OpenAI, a publikację ponad 700 plików naraz nazywa demonstracją siły.

Agent A, prosta pętla przemiennie generująca dowód i sprawdzająca go w Lean, rozwiązał według Curto te same dziewięć problemów Erdősa co rozbudowany agent D. Autorzy potwierdzają to, ale na najtrudniejszych problemach prosty agent wypadł drożej.

Autorzy podają koszt kilkuset dolarów na problem. Przy trudniejszych podproblemach agent może sięgnąć po AlphaProof, wyspecjalizowane narzędzie do dowodzenia. Według Curto podane koszty obejmują tylko udane przebiegi, a w kosztach agentów B i D brakuje obliczeń modułu AlphaProof. The Decoder, powołując się na Google DeepMind, pisze, że dziewięć problemów Erdősa agent rozwiązał także bez niego.