Użyteczne ogłoszenie o matematycznej AI powinno pozwalać odtworzyć wynik. Jakie zadania podjęto? Co system udowodnił? Kto sprawdził zgodność formalnego twierdzenia z pierwotnym pytaniem? AlphaProof Nexus dostarcza konkretnych materiałów do takiej oceny, ale pokazuje też, dlaczego liczba dowodów wymaga kontekstu.
Materiał źródłowy opisuje badanie opublikowane w Science 8 października 2026 roku, po majowym preprincie. Autorzy zgłaszają dziewięć rozwiązań w wybranym zbiorze 353 problemów Erdősa; dwa pozostawały otwarte przez 56 lat. Informują również o 44 dowodach spośród 492 hipotez OEIS. To wyniki na przygotowanych zbiorach, a nie skuteczność wobec dowolnego pytania matematycznego.
Zacznij od całego zbioru prób
Dziewięć z 353 to około 2,5 procent. Pozostałe 344 próby również należą do oceny, bo wskazują obecną granicę metody. Zadania musiały dać się zapisać w Lean i korzystać z dostępnych bibliotek formalnych. Dobór problemów, pokrycie bibliotek i nakład obliczeniowy wpływają więc na wynik obok możliwości modelu.
Dowody obejmują publikację w Science, preprint i publiczne repozytorium dowodów. Udane pliki umożliwiają kontrolę logiki, a nieudane formalizacje ujawniają zakres eksperymentu.
Rozdziel trzy rodzaje poprawności
Lean sprawdza, czy dowód wynika z zakodowanych definicji i założeń. Osobnym zadaniem pozostaje ustalenie, czy zapis wiernie oddaje pierwotny problem. Zmieniony kwantyfikator, pominięty warunek brzegowy lub silniejsze założenie mogą sprawić, że poprawny dowód odpowiada na słabsze pytanie.
Nowość wymaga kolejnej kontroli. Starsze twierdzenie może już implikować wynik niezależnie uzyskany przez system. Materiał źródłowy wspomina audyt kwestionujący nowość jednego przypadku. Nie unieważnia to formalnego rozumowania, ale zmienia zakres twierdzenia o nowym wkładzie naukowym. Reakcje ekspertów wyjaśniają tę różnicę.
Sprawdź wkład agenta
Podstawowy proces generuje kod Lean, sprawdza go i poprawia nieudane próby na podstawie komunikatów kompilatora. Bardziej rozbudowane konfiguracje dodają skoordynowane przeszukiwanie i wyspecjalizowany system AlphaProof. Co istotne, najprostsza opisana konfiguracja rozwiązała te same dziewięć problemów bez tego narzędzia.
Przed przypisaniem sukcesu złożonej architekturze warto więc obejrzeć eksperymenty ablacyjne. Bezpośrednia pętla modelu i weryfikatora może wyjaśniać znaczną część wyniku. Dodatkowe elementy mogą pomagać gdzie indziej, lecz powinny wykazać więcej sukcesów, niższy łączny koszt albo lepszą pomoc badaczom.
Uwzględnij cały proces badawczy
Udane uruchomienie modelu stanowi tylko część kosztu. Nieudane poszukiwania, formalizacja, utrzymanie bibliotek, ocena specjalistów i przełożenie formalnego dowodu na zrozumiałe wyjaśnienie również wymagają pracy. Cena udanej próby pomijająca te elementy nie określa pełnego kosztu odkrycia.
Zespół badawczy powinien zachowywać razem treść problemów, strategie, sprawdzalne maszynowo artefakty, koszty obliczeń i interwencje ludzi. Najpierw należy ocenić wierność formalizacji, następnie zweryfikować dowód, a później nowość i wartość wyjaśniającą. Dopiero wtedy można mówić o nowym rozwiązaniu.
Szerszą lekcją jest wzorzec projektowania agentów: łączyć generowanie probabilistyczne ze ścisłym weryfikatorem, zachowywać użyteczne wyniki pośrednie i kierować ekspertów tam, gdzie kończy się automatyczna kontrola. Pierwotny materiał wspiera taki ostrożnie określony wniosek. Postęp należy mierzyć niezależnymi audytami i poprawą wyników na wcześniej nierozwiązanych zadaniach, nie tylko liczbą dowodów.