Badanie Google DeepMind opublikowane 8 października 2026 r. podaje, że AlphaProof Nexus rozwiązał 9 z 353 sformalizowanych problemów Erdősa oraz udowodnił 44 z 492 wybranych hipotez OEIS. To dwa osobne zestawy testowe, a system rozpoczyna pracę od twierdzenia zapisanego w Lean i szkicu dowodu.
Czym zajmuje się AlphaProof Nexus
AlphaProof Nexus to framework do wyszukiwania dowodów matematycznych: modele językowe proponują i poprawiają dowody, a Lean — asystent dowodzenia — mechanicznie sprawdza ich formalny zapis. W odróżnieniu od zwykłego opisu rozwiązania dowód formalny jest zapisany w języku, którego reguły można zweryfikować automatycznie.
Wyniki przedstawili autorzy badania. Wśród dziewięciu rozwiązanych problemów Erdősa dwa pozostawały otwarte od 56 lat.
Co mierzą opublikowane wyniki
Liczby dotyczą dwóch odrębnych ocen: zbioru sformalizowanych problemów Erdősa oraz wybranych hipotez z Online Encyclopedia of Integer Sequences (OEIS). Każda ma własny mianownik i zakres.
| Oceniany zbiór | Udowodnione problemy lub hipotezy | Ocenione pozycje | Zakres |
| Problemy Erdősa | 9 | 353 | Sformalizowane twierdzenia z repozytorium Formal Conjectures; szerszy katalog problemów Erdősa obejmuje ponad 1200 pozycji. |
| Hipotezy OEIS | 44 | 492 | Wybrane otwarte hipotezy z Online Encyclopedia of Integer Sequences. |
Zbiór Erdősa obejmował dostępne w repozytorium Formal Conjectures formalizacje, a nie cały szerszy katalog. Wyniku 9 z 353 nie należy łączyć z wynikiem OEIS: w tym drugim teście oceniano inny zbiór pytań.
Jak działa wyszukiwanie dowodów
Agent otrzymuje twierdzenie zapisane w Lean oraz szkic dowodu. Dodatkowym kontekstem może być opis w języku naturalnym lub wiedza dziedzinowa zakodowana w Lean. Następnie modele językowe wprowadzają poprawki do szkicu, a informacja zwrotna z kompilatora Lean pomaga kierować kolejnymi próbami.
Pełna konfiguracja rozszerza ten proces o wyszukiwanie ewolucyjne: utrzymuje pulę szkiców, ocenia je i wybiera do dalszych prób. Może też wywoływać AlphaProof, wyspecjalizowany system dowodzenia, aby pracował nad podcelami — mniejszymi twierdzeniami składającymi się na większy dowód.
Co wyniki pokazują
Lean sprawdza, czy dowód wynika z twierdzenia zapisanego formalnie. Zgodność tego formalnego twierdzenia z pierwotnym pytaniem matematycznym to osobna kwestia. W przypadku twierdzeń Erdősa ich formalizacje sprawdzili eksperci.
Większość ocenianych problemów Erdősa pozostała nierozwiązana. Autorzy wskazują, że dotychczasowe sukcesy koncentrowały się między innymi w kombinatoryce, optymalizacji wypukłej i teorii liczb, gdzie biblioteki matematyczne Lean są bardziej rozwinięte.
