Nowości
Magazyn Science publikuje AlphaProof Nexus od DeepMind, system rozwiązał 9 problemów Erdősa
Praca o systemie AlphaProof Nexus przeszła recenzję i ukazała się 8 października w czasopiśmie Science. System połączył model językowy z weryfikatorem Lean i rozwiązał 9 z 353 podejmowanych problemów Erdősa oraz 44 z 492 otwartych hipotez z bazy OEIS.
Google DeepMind opublikował w recenzowanym czasopiśmie Science pracę o AlphaProof Nexus, systemie, który łączy model językowy z kompilatorem Lean i szuka formalnych dowodów twierdzeń. Artykuł ukazał się 8 października 2026 roku, a The Decoder opisywał wyniki tej pracy już w maju 2026 roku.
Jak działa system
AlphaProof Nexus to szkielet, w którym model językowy proponuje dowód, a kompilator Lean sprawdza każdy krok logiczny i zwraca błędy do kolejnej próby. Według The Decoder w maju system opierał się na modelu Gemini 3.1 Pro. Człowiek weryfikuje dopiero końcowe wyniki.
Praca opisuje cztery warianty agentów. Pierwszy to model z informacją zwrotną z kompilatora, drugi dodaje zapytania do AlphaProof, trzeci wprowadza ewolucyjną populację szkiców dowodów ocenianych przez model Gemini 3.0 Flash w rankingu Elo, a czwarty łączy wszystkie te elementy.
Co udało się udowodnić
Według komunikatu AAAS system rozwiązał 9 z 353 podejmowanych problemów Erdősa, z czego dwa pozostawały bez odpowiedzi ponad 50 lat. The Decoder podaje, że chodzi o 56 lat. Udowodniono także 44 z 492 otwartych hipotez z bazy OEIS, czyli Internetowej Encyklopedii Ciągów Liczbowych.
Poza tym system rozstrzygnął pytanie z dziedziny funkcji Hilberta w geometrii algebraicznej, otwarte od 15 lat, oraz poprawił znane oszacowanie w optymalizacji wypukłej. Komunikat wymienia też problemy z optyki kwantowej i teorii grafów. Wszystkie dowody w Lean i wybrane dowody w języku naturalnym są dostępne na GitHubie.
Ograniczenia
9 z 353 to około 2,5 procent. The Decoder zauważa, że to zgodne z szacunkiem Terence'a Tao, według którego AI radzi sobie z 1-2 procentami problemów Erdősa, głównie łatwiejszych. Sukcesy skupiają się w kombinatoryce, optymalizacji wypukłej i teorii liczb, gdzie biblioteka Mathlib jest dobrze rozwinięta.
Późniejsza analiza, jak podaje The Decoder, wykazała też, że prostszy wariant z samym kompilatorem mógł udowodnić wszystkie dziewięć problemów, choć drożej w najtrudniejszych przypadkach. Agenci dziedziczą ponadto zawodność modeli, na których się opierają.
Weryfikacja formalna może służyć jako filtr określający, które dowody zasługują na przegląd przez człowieka. - autorzy pracy o AlphaProof Nexus, cytowani przez The Decoder
Dlaczego to ważne
Wartość podejścia leży w wiarygodności. Modele językowe popełniają subtelne błędy logiczne, więc ich dowody zwykle wymagają żmudnej kontroli ekspertów. Lean wyłapuje takie błędy automatycznie, co według komunikatu pozwala traktować narzędzie jako wsparcie badaczy, a nie tylko pokaz możliwości modelu.
Towarzyszący artykułowi komentarz Jeremy'ego Avigada z Carnegie Mellon i Matthew Ballarda z University of South Carolina przytacza relację autorów, według której nawet nieudane próby dowodzenia przez AI pomagały im lepiej zrozumieć problemy i robić postępy w ich rozwiązywaniu. Celem AI w matematyce ma być ich zdaniem wspieranie matematyków w poszukiwaniu wiedzy i zrozumienia. Komunikat zastrzega, że AI może stać się użytecznym narzędziem, nie opisuje więc tego jako ugruntowanej możliwości.
