13 milionów linii dowodu: AI formalizuje twierdzenie Fermata

Jak zorganizowano formalizację

Według Anthropic Claude pracował nad formalizacją przez jedenaście dni, tworząc około 13 milionów linii Lean i ponad 30 tysięcy udowodnionych twierdzeń pośrednich. System korzystał z Prove2Me, infrastruktury rozbijającej duży cel na graf zależnych podproblemów, które można rozwiązywać i ponownie wykorzystywać. Około 29,5 tysiąca udowodnionych wyników zostało wykorzystanych dalej w konstrukcji. Skala pokazuje nie tylko zdolność generowania kodu, lecz także potrzebę zarządzania zależnościami, pamięcią i weryfikacją w bardzo długim zadaniu.

Lean pełnił rolę rygorystycznego sędziego. Każdy zaakceptowany fragment musiał zostać sprawdzony przez kernel wobec formalnie określonych reguł i dostępnych bibliotek. Model mógł proponować kroki, naprawiać błędy i szukać alternatyw, ale nie mógł przekonać systemu samym płynnym wyjaśnieniem. Źródło Anthropic opisuje wykonanie oraz statystyki projektu. Wniosek, że architektura zadania była równie ważna jak sam model, jest interpretacją redakcyjną Mateusza opartą na roli grafu Prove2Me i mechanizmu sprawdzającego.

Co naprawdę zostało sprawdzone

Rezultatem jest formalny artefakt, który ma przejść kontrolę Lean od założeń i dostępnych komponentów aż do twierdzenia końcowego. Anthropic raportuje, że projekt wytworzył bazę większą niż pięciokrotność ówczesnego Mathlib i zużył około sześciu miliardów tokenów wyjściowych. Duża część materiału służyła poszukiwaniu, próbom oraz infrastrukturze, a tylko niewielki odsetek nieszablonowego kodu z nieudanych podejść trafił do ostatecznej ścieżki. To pokazuje koszt selekcji ukryty za gotowym dowodem.

Komputerowa weryfikacja daje mocny dowód spójności formalnego zapisu z regułami systemu, ale zakres tej gwarancji jest precyzyjny. Kernel sprawdza, czy terminy mają wymagane typy i czy wnioski wynikają z zadeklarowanych założeń. Nie ocenia historycznej oryginalności, jakości ekspozycji ani tego, czy formalizator wybrał najbardziej pouczającą drogę. Zaufanie przesuwa się z pojedynczego tekstu modelu na mniejszy mechanizm sprawdzający, biblioteki i poprawność powiązania formalnej tezy z twierdzeniem, które chcieliśmy opisać.

Dlaczego nie jest to nowy dowód Fermata

Claude nie odkrył nowej matematycznej idei rozwiązującej Wielkie Twierdzenie Fermata. Formalizacja podąża za istniejącą teorią rozwiniętą wokół dowodu Andrew Wilesa i opiera się na wcześniejszych bibliotekach oraz pracy społeczności Lean. Nowością jest skala i stopień automatyzacji przenoszenia tego łańcucha do języka formalnego. Stwierdzenie „AI rozwiązała Fermata” byłoby więc mylące: twierdzenie było już udowodnione, a obecny projekt stworzył komputerowo kontrolowaną reprezentację znanej linii matematycznej.

Formalny sukces nie dowodzi również, że wygenerowane 13 milionów linii jest łatwe do audytu przez człowieka ani że wszystkie zastosowane definicje są pedagogicznie najlepsze. Artefakt może być logicznie poprawny, a jednocześnie bardzo trudny do czytania. Nie pokazuje też automatycznej zdolności do formalizowania dowolnego nieopisanego obszaru matematyki. Projekt korzystał z ogromnej ilości obliczeń, istniejącego ekosystemu i struktury konkretnego problemu. Generalizację trzeba mierzyć na nowych twierdzeniach o innej budowie.

Model publikacji: człowiek i maszyna

Autorski model Mateusza zakłada publikowanie dwóch powiązanych warstw. Pierwsza powinna wyjaśniać ludziom ideę dowodu, kluczowe zależności, intuicję i znaczenie wyniku. Druga dostarcza formalny artefakt, wersję bibliotek, instrukcję odtworzenia oraz wynik niezależnego sprawdzenia. Czytelnik może wtedy zrozumieć argument na właściwym dla siebie poziomie, a specjalista zweryfikować zapis maszynowy. Ten model nie jest deklarowanym standardem Anthropic; jest propozycją wykorzystania mocnej strony Lean bez rezygnacji z ludzkiej czytelności.

Kolejne istotne testy powinny objąć reprodukcję repozytorium przez niezależne zespoły, utrzymanie dowodu po zmianach bibliotek oraz formalizacje, dla których brakuje gotowych komponentów. Warto mierzyć nie tylko liczbę rozwiązanych celów, lecz także koszt obliczeń, udział pracy ręcznej, wielkość ponownie użytecznej biblioteki i łatwość przeglądu. Prawdziwy przełom nastąpi wtedy, gdy formalny certyfikat będzie tańszy i bardziej dostępny, a jednocześnie nie odsunie na bok zadania wyjaśnienia, dlaczego dowód działa.

Cel, który dojrzewał przez stulecia i dekady formalizacji

Wielkie Twierdzenie Fermata zaczęło się od zapisu Pierre’a de Fermata z około 1637 roku, lecz jego współczesny dowód powstał dopiero dzięki teorii nieznanej autorowi. Andrew Wiles przedstawił argument w 1993 roku; podczas szczegółowej kontroli znaleziono lukę, którą naprawił z Richardem Taylorem, a poprawne prace ukazały się w 1995 roku. Ta historia wyjaśnia, dlaczego matematycy nie utożsamiają przekonującej narracji z dowodem. Nawet wybitny argument może wymagać miesięcy lektury, sprawdzania zależności i korekty jednego krytycznego połączenia.

Pomysł przełożenia dowodu Wilesa na język kontrolowany przez komputer pojawił się długo przed obecnymi modelami generatywnymi. Anthropic wskazuje propozycję Jana Bergstry sprzed dwóch dekad oraz rozpoczęty w 2024 roku społecznościowy projekt Imperial College London kierowany przez Kevina Buzzarda. Osiągnięcie Claude’a nie powstało więc w próżni. Weszło w dojrzały ekosystem Lean, Mathlib, blueprintów i formalnych komponentów tworzonych przez setki osób. Przełom dotyczy szybkości i skali integracji istniejącej matematyki, nie anulowania historii ludzkiego dowodu.

Co dokładnie obejmuje certyfikat Lean

Repozytorium Anthropic formalizuje twierdzenie dla liczb naturalnych: dla każdego wykładnika n co najmniej 3 nie istnieją dodatnie a, b i c spełniające aⁿ + bⁿ = cⁿ. Domyślny cel FinalCheck ma przestać się budować, jeśli wynik zależy od czegoś więcej niż trzech standardowych aksjomatów Lean używanych w projekcie. Autorzy przeszukali także moduły pod kątem mechanizmów, które mogłyby ominąć zwykłą kontrolę, takich jak sorry, dodatkowy axiom, unsafe lub native_decide. To opis precyzyjnego, formalnego obiektu, a nie jedynie deklaracja w komunikacie prasowym.

Kernel Lean sprawdza każdy zadeklarowany term względem systemu typów i odtwarza zależności aż do podstaw. Nie musi ufać stylowi wyjaśnienia, reputacji autora ani pewności modelu językowego. Gwarancja ma jednak warunki: dotyczy twierdzenia faktycznie zapisanego w kodzie, przy określonej wersji narzędzi i aksjomatach. Nie rozstrzyga automatycznie, czy wszystkie definicje najlepiej reprezentują intencję matematyczną ani czy dany dowód jest czytelny. Formalność zawęża miejsce na błąd logiczny, ale nie usuwa potrzeby zrozumienia zakresu certyfikatu.

Comparator i drugi kernel wzmacniają bazę zaufania

Autorzy nie poprzestali na jednym komunikacie „build przeszedł”. Narzędzie Comparator miało potwierdzić, że końcowe twierdzenie i wszystkie stałe wymienione w jego zapisie są identyczne z wyzwaniem sformułowanym wyłącznie przy użyciu Mathlib. Następnie środowisko zostało wyeksportowane i przyjęte przez nanoda, niezależny kernel Lean napisany w Rust. Repozytorium raportuje sprawdzenie ponad miliona deklaracji bez błędów. Dwie różne ścieżki kontroli ograniczają ryzyko, że wynik zależy od przypadkowej właściwości jednego narzędzia.

Ta warstwa wymaga właściwej etykiety. Testy i ich wyniki opublikował zespół tworzący artefakt; publiczny kod umożliwia niezależne powtórzenie, ale sama publikacja logów nie jest jeszcze pełną, zewnętrzną replikacją. Projekt użył czterech drobnych poprawek nanoda, opisanych jako zmiany wydajności i raportowania bez osłabienia reguł typowania. Recenzent powinien obejrzeć te poprawki, wersje zależności i skrypty, a nie tylko końcowe zdanie. Wiarygodność rośnie dzięki małej, jawnej bazie zaufania, a nie dzięki założeniu, że każde narzędzie jest nieomylne.

Kręgosłup argumentu prowadzi do niemożliwej formy modularnej

Formalizacja prowadzi dowód nie wprost. Potencjalny kontrprzykład redukuje się do przypadku pierwszego wykładnika co najmniej 5, a następnie pakuje go w znormalizowane dane i krzywą Freya. Dalsze węzły pokazują, że związana z nią reprezentacja Galois jest nierozkładalna oraz że sama krzywa jest modularna. To właśnie tutaj wchodzą wyspecjalizowane wersje rezultatów Mazura, Langlandsa–Tunnella i twierdzeń o podnoszeniu modularności. Repozytoryjna mapa dowodu wskazuje konkretny typ Lean dla każdego z tych połączeń, dzięki czemu nazwa wielkiego twierdzenia nie zastępuje jego faktycznie użytej treści.

Następnie obniżanie poziomu w stylu Ribeta prowadziłoby od krzywej Freya do niezerowej formy parabolicznej wagi 2 dla grupy Γ₀(2). Ostatni krok formalnie dowodzi, że przestrzeń takich form jest zerowa, co daje sprzeczność i wyklucza kontrprzykład. Dokument `PROOF-PATH.md` rozdziela także dokładną siłę nazwanych twierdzeń od ich szerszych podręcznikowych wersji. Projekt nie twierdzi na przykład, że formalizuje każde twierdzenie Mazura lub każdą postać obniżania poziomu; udowadnia wariant potrzebny na tej konkretnej ścieżce. To ograniczenie jest zaletą audytu, bo pozwala sprawdzić faktyczny zakres zależności.

Pochodzenie odziedziczonego kodu jest częścią wyniku

Osobny plik `ATTRIBUTION.md` identyfikuje 106 plików zawierających materiał zaczerpnięty lub zaadaptowany z projektu Imperial College London albo z `flt-regular`: 54 w katalogu definicji i 52 w rozwiązaniach. Kolejne 23 pliki odtwarzają tekst Mathlib. Zestawienie podaje plik źródłowy, autorów i przybliżony zakres zapożyczenia. Te liczby nie umniejszają integracji wykonanej przez agentów; pokazują, z jakiego istniejącego kapitału formalnego mogły skorzystać oraz które fragmenty nie powinny być przypisywane nowemu systemowi.

Ta warstwa była potrzebna, ponieważ pliki złożone przez agentów opublikowano bez komentarzy, a nagłówki części materiału źródłowego nie przetrwały w miejscu użycia. Autorzy odtworzyli więc pochodzenie przez porównanie kodu, wcześniejsze notatki i tabelę licencyjną. Przy przenoszeniu do Lean 4.33.1 w 65 ze 106 odziedziczonych plików mechanicznie zmieniono nazwy lematów lub dowody, a 41 pozostało identycznych bajtowo. Audyt formalnej poprawności i audyt autorstwa odpowiadają na różne pytania; wiarygodny artefakt potrzebuje obu, zwłaszcza gdy model składa wynik z wielu bibliotek.

Reprodukowalność jest możliwa, lecz kosztowna

Repozytorium przypina Lean 4.33.1 i konkretną wersję Mathlib oraz opisuje budowę od zera. To mocniejszy punkt startu niż nieweryfikowalny zrzut ekranu, ale próba nie jest lekka. Instrukcja przewiduje dziesiątki gigabajtów przestrzeni, dużą pamięć na zadanie równoległe oraz dodatkowe zasoby dla Comparatora i eksportu do nanoda. Zespół raportuje wielogodzinny build na maszynie z 96 zadaniami równoległymi. Podane czasy i zużycie pochodzą z infrastruktury autorów, więc są wskazówką, nie gwarancją dla każdej maszyny.

Autorzy ostrzegają również, że część ścieżek jest zbyt długa dla Windows, dlatego pełny proces przewidziano dla Linuxa lub macOS. Ograniczenie operacyjne ma znaczenie dla otwartej weryfikacji: artefakt może być publiczny, a mimo to pozostawać poza zasięgiem zwykłego laptopa. Dobry program replikacji powinien więc publikować skróty plików, obrazy środowiska lub jasne instrukcje odtwarzania, logi z niezależnych maszyn i wyniki etapowe. Najbardziej przekonujący certyfikat to taki, który wiele zespołów potrafi sprawdzić bez dostępu do infrastruktury twórcy.

Certyfikat jest migawką wersji, a nie wiecznym buildem

Repozytorium przypina Lean 4.33.1 oraz Mathlib 4.33.0 i określa się jako artefakt badawczy, który nie jest utrzymywany ani otwarty na wkład. Taka decyzja wzmacnia możliwość odtworzenia opublikowanego stanu: recenzent wie, które definicje, poprawki kernela i zależności mają wejść do kontroli. Nie gwarantuje jednak, że ten sam kod zbuduje się bez zmian w przyszłej wersji Lean. Awaria po aktualizacji narzędzi nie unieważnia automatycznie wcześniejszego certyfikatu, ale wymaga rozróżnienia między odtworzeniem historycznego środowiska a przeniesieniem dowodu do nowego ekosystemu.

Jeżeli formalizacja ma zasilać dalszą matematykę, potrzebuje drugiego życia poza zamrożonym artefaktem: opiekunów, testów regresji, jawnych zmian semantycznych i planu przenoszenia użytecznych komponentów do bibliotek społeczności. To wniosek redakcyjny, nie deklarowany harmonogram Anthropic. Jednorazowy build odpowiada na pytanie, czy określony term przeszedł określone kontrolery. Utrzymanie odpowiada na inne: czy kolejne zespoły potrafią bezpiecznie importować, wyjaśniać i rozwijać tę wiedzę po zmianie zależności. Długoterminowy wpływ będzie zależał nie tylko od liczby wygenerowanych linii, lecz także od jakości tej migracji.

Czytelna ekspozycja musi rozwijać się obok formalnego artefaktu

Zweryfikowany przez kernel artefakt i tekst przeznaczony dla człowieka pełnią odmienne funkcje. Pierwszy ma umożliwić maszynowe sprawdzenie, czy każdy krok wynika z zadeklarowanych definicji, aksjomatów i wcześniej udowodnionych twierdzeń. Drugi ma pomóc czytelnikowi zobaczyć strategię: dlaczego wybrano właśnie ten lemat, gdzie znajduje się główna trudność i jak lokalny krok łączy się z większą konstrukcją. Nie należy traktować prozy jako luźnej reklamy pliku formalnego ani pliku jako substytutu wyjaśnienia. Wiarygodna publikacja utrzymuje oba tory razem, z jasno opisanym zakresem tego, co dokładnie zostało sprawdzone.

Praktycznym łącznikiem jest mapa ekspozycji. Zawiera stabilne definicje pojęć, szkic zależności między głównymi twierdzeniami oraz odnośniki do konkretnych nazw deklaracji w repozytorium. Każdy rozdział prozy może wskazywać odpowiadający mu fragment artefaktu, wersję środowiska i założenia wprowadzone z zewnątrz. Tam, gdzie formalizacja wykorzystuje techniczny zabieg wygodny dla systemu, komentarz powinien wyjaśnić jego rolę bez udawania, że jest to jedyny matematycznie naturalny sposób rozumowania. Z kolei intuicja, której nie obejmuje dowód, musi pozostać oznaczona jako interpretacja, a nie wynik zweryfikowany przez kernel.

Oba materiały powinny być wersjonowane wspólnie. Zmiana definicji, zależności albo struktury dowodu uruchamia kontrolę odnośników i przegląd ekspozycji, ponieważ poprawny tekst może stać się nieaktualny mimo nadal kompilującego się kodu. Recenzent potrzebuje krótkiej ścieżki od twierdzenia w artykule do deklaracji formalnej oraz z powrotem do wyjaśnienia jej znaczenia. Dobra ekspozycja nie upraszcza przez pominięcie odpowiedzialności. Redukuje koszt wejścia dla kolejnych odbiorców i niezależnych recenzentów, zachowując granicę między motywacją, matematycznym argumentem i tym, co rzeczywiście poświadcza mechaniczna weryfikacja.