Claude sformalizował Wielkie Twierdzenie Fermata w jedenaście dni. Matematyk, który sam próbował: "nic nowego, ale nadzwyczajne"

W tym samym tygodniu, w którym OpenAI ogłosiło "erę AGI" liczbą, która traci trzydzieści siedem punktów w neutralnych warunkach testowych, Anthropic pokazało coś dokładnie odwrotnego: wynik, który da się w pełni sprawdzić linia po linii, bez wiary na słowo. Firma ogłosiła, że Claude w jedenaście dni, w dużej mierze samodzielnie, stworzył pierwszy pełny, komputerowo zweryfikowany dowód Wielkiego Twierdzenia Fermata w języku Lean. Zanim ktokolwiek zdąży to przeczytać jako "AI udowodniło Fermata", trzeba postawić sprawę jasno: to twierdzenie udowodnił Andrew Wiles w 1995 roku, po ponad siedmiu latach pracy. Claude sformalizował istniejący dowód, czyli przełożył go na formę, którą komputer potrafi sprawdzić linia po linii, bez zaufania do żadnego człowieka po drodze, a nie odkrył cokolwiek nowego w samej matematyce.

Trzynaście milionów linii kodu w jedenaście dni

Zespół Anthropic pracował nad tym problemem dłużej, ale przełom przyszedł po przejściu na Prove2Me, otwartoźródłowy framework zbudowany specjalnie do formalizacji matematyki na dużą skalę. Z Prove2Me i zespołem agentów opartych na Claude Code, dowód domknięto w niecałe dwa tygodnie. Finalny kod w Lean liczy ponad 13,4 miliona linii, obejmuje 30 300 udowodnionych twierdzeń, z czego 29 500 trafiło do ostatecznego dowodu, i pochłonął około sześciu miliardów tokenów wyjściowych z ogólnego modelu badawczego Anthropic, porównywalnego mniej więcej z Claude Fable 5.1.

Skala nie jest jedynym miernikiem. Formalizacja domyka listę stu klasycznych wyzwań formalizacyjnych Freeka Wiedijka, prowadzoną od dwudziestu lat i traktowaną w tej dziedzinie jako nieoficjalny ranking najtrudniejszych twierdzeń do przełożenia na język komputerowo weryfikowalny. Fermat był na tej liście od początku najbardziej znanym i najtrudniejszym punktem.

Fermat czekał 358 lat na dowód, potem jeszcze trzydzieści na komputerowe potwierdzenie

Pierre de Fermat zapisał swoje twierdzenie na marginesie książki w 1637 roku, dodając słynną notatkę, że zna dowód zbyt długi, żeby zmieścił się na marginesie. Przez 358 lat nikt takiego dowodu nie znalazł, aż Andrew Wiles w 1993 roku, po siedmiu latach samotnej pracy, ogłosił rozwiązanie, w którym recenzenci szybko znaleźli lukę. Wiles łatał ją jeszcze przez rok z pomocą swojego byłego doktoranta, Richarda Taylora, zanim poprawiony dowód trafił do druku w 1995 roku. Ta historia sama w sobie pokazuje, jak trudno w matematyce mieć stuprocentową pewność, że dowód jest kompletny, dopóki nie przejdzie przez formalną, maszynową weryfikację.

Weryfikacja niezależna od samego Claude'a

Cały dowód sprawdziło nanoda, osobne jądro weryfikujące napisane w Rust, niezwiązane z narzędziami użytymi do jego stworzenia. Nanoda potwierdziło poprawność wszystkich 1 052 234 deklaracji w kodzie, a sam Lean zweryfikował wynik, opierając się wyłącznie na trzech standardowych aksjomatach systemu. Dwuwarstwowa weryfikacja, jedno narzędzie tworzy dowód, drugie, zupełnie inne, go sprawdza, to dokładnie taki poziom rygoru, jakiego oczekuje się od formalizacji matematycznej, a nie skrót, który AI mogłaby sobie ułatwić.

Co na to matematyk, który sam próbował to zrobić

Kevin Buzzard z Imperial College London prowadzi od lat własny, finansowany przez EPSRC projekt formalizacji Wielkiego Twierdzenia Fermata i jest jednym z najbardziej rozpoznawalnych głosów w tej dziedzinie. Jego reakcja na wynik Anthropic była wyjątkowo szczera: sam był już wcześniej "99,9% pewien", że dowód Wilesa jest poprawny, więc formalizacja Claude'a "po prostu wiernie podąża za wczesną literaturą i nie dodaje niczego" matematycznie nowego. Nazwał ją jednak nadzwyczajnym osiągnięciem z zupełnie innego powodu. Dla Anthropic, w drodze do rekordowego IPO wycenianego na dwa biliony dolarów, taka niezależnie zweryfikowana pochwała od czołowego eksperta w dziedzinie liczy się bardziej niż niejeden wewnętrzny benchmark.

Anthropic sformalizowało wersję dowodu opisaną przez Darmona, Diamonda i Taylora, opartą bezpośrednio na oryginalnej pracy Wilesa z 1995 roku, a nie nowocześniejsze podejście, nad którym pracuje sam Buzzard. Po drodze zespół musiał zbudować w Lean solidną infrastrukturę matematyczną, której wcześniej brakowało, w tym teorię Fontaine'a i pracę nad ideałem Eisensteina, co samo w sobie jest trwałym wkładem do biblioteki formalnej matematyki, niezależnie od tego, że sam dowód nie jest nowy. Formalny zakres dowodu obejmuje wykładniki od 17 wzwyż, bo mniejsze przypadki od dawna mają własne, osobne dowody formalne w tej samej bibliotece.

Dlaczego to jednak ma znaczenie

Prawdziwa wartość tego wyniku leży w tempie, nie w samym twierdzeniu. Buzzard wskazał to wprost: tysiące stron literatury matematycznej udało się sformalizować od początku do końca przez coś w rodzaju roju agentów AI w jedenaście dni. Ręczna formalizacja porównywalnych dowodów w przeszłości zajmowała zespołom badaczy lata, czasem dekadę. Jeśli tempo z tego eksperymentu da się powtórzyć na innych, współczesnych twierdzeniach, zmienia to fundamentalnie, jak szybko społeczność matematyczna może niezależnie zweryfikować nowe, skomplikowane dowody, zamiast czekać latami na recenzje i powtórne sprawdzenia przez ludzi.

To akurat problem realny i dobrze udokumentowany w samej matematyce. Klasyfikacja skończonych grup prostych, jeden z największych projektów dowodowych dwudziestego wieku, rozciąga się na kilkanaście tysięcy stron w dziesiątkach osobnych publikacji, a garstka ludzi na świecie rzeczywiście przeszła przez cały materiał krok po kroku. Dowód hipotezy ABC Shinichiego Mochizukiego pozostaje przedmiotem sporu wśród matematyków wiele lat po publikacji właśnie dlatego, że niewielu potrafi w pełni zweryfikować użyty przez niego aparat pojęciowy. Autoformalizacja w tempie z eksperymentu Anthropic adresuje dokładnie ten problem: usuwa zależność od tego, ilu ludzi na świecie ma czas i kompetencje, żeby ręcznie prześledzić każdy krok skomplikowanego dowodu.

Własny projekt Buzzarda się przez to nie kończy. Jego zespół nadal pracuje nad wkładem do mathlib, głównej biblioteki matematycznej Lean, i nad dynamicznymi dokumentami eksplorującymi bardziej współczesne podejścia do dowodu. Formalizacja Anthropic pokrywa się z celem tego projektu tylko częściowo, bo idzie inną, starszą ścieżką dowodową niż ta, którą Buzzard chciał ostatecznie sformalizować.