Opublikowany 8 października 2026 r. artykuł w Science opisuje, że system AlphaProof Nexus rozwiązał 9 z 353 otwartych problemów Erdősa. W osobnym zbiorze dowiódł 44 z 492 otwartych hipotez z Online Encyclopedia of Integer Sequences (OEIS). Dwa z rozwiązanych problemów Erdősa pozostawały otwarte od 56 lat.
Jakie wyniki przedstawia artykuł w Science
Liczby dotyczą dwóch różnych kolekcji: 353 otwartych problemów Erdősa oraz 492 otwartych hipotez OEIS. AlphaProof Nexus rozwiązał 9 problemów z pierwszej puli i dowiódł 44 hipotez z drugiej.
Jak AlphaProof Nexus sprawdza dowody
System na przemian generuje formalne dowody z pomocą dużego modelu językowego (LLM) i weryfikuje je w Lean. To asystent dowodzenia, którego kompilator sprawdza formalne kroki dowodu.
Artykuł opisuje też prostego agenta, który naprzemiennie generował dowody za pomocą LLM i sprawdzał je w Lean. Odtworzył on dziewięć wyników dotyczących problemów Erdősa.
Dwa zbiory, dwa wyniki
Wyniki odnoszą się do tych konkretnych zbiorów zadań, a każda z podanych liczb ma własny mianownik: 9 z 353 problemów Erdősa oraz 44 z 492 hipotez OEIS.
Opis badania obejmuje również zastosowania w kombinatoryce, optymalizacji, teorii grafów, geometrii algebraicznej i optyce kwantowej. Wśród wymienionych rezultatów znalazło się rozstrzygnięcie otwartego pytania z geometrii algebraicznej oraz poprawienie znanego ograniczenia w optymalizacji min–max.
