Claude Anthropic sformalizował dowód Wielkiego Twierdzenia Fermata w Lean

Anthropic ogłosił, że jego model Claude jako pierwszy system AI stworzył kompletny, sprawdzalny komputerowo dowód Wielkiego Twierdzenia Fermata w języku formalnym Lean. Cały proces, opisany jako w dużej mierze autonomiczny, zajął 11 dni i pozostawił po sobie największy jak dotąd plik dowodowy tego typu.

Co dokładnie zrobił Claude

Zadanie polegało nie na wymyśleniu nowego dowodu, lecz na przełożeniu istniejącego rozumowania matematycznego na formalny zapis, który komputer może zweryfikować krok po kroku, bez luk i bez zaufania na słowo. Twierdzenie Fermata, sformułowane w XVII wieku i udowodnione dopiero w 1995 roku przez Andrew Wilesa, od dekad uchodziło za jeden z najtrudniejszych kandydatów do pełnej formalizacji ze względu na długość i złożoność oryginalnego rozumowania.

Claude pracował w kilkudziesięciu równoległych agentach, korzystając z platformy Prove2Me, która utrzymuje graf zależności między twierdzeniami i pozwala poszczególnym instancjom modelu dzielić się już udowodnionymi fragmentami zamiast dowodzić ich od nowa. Według Anthropic pierwsza próba bez dostępu do tego narzędzia zakończyła się niepowodzeniem, a przełom nastąpił dopiero po integracji z systemem Penga.

Rola człowieka

Anthropic podkreśla, że udział ludzi ograniczał się do sporadycznych wskazówek wysokiego poziomu. Tianyi Peng miał kierować uwagę modelu krótkimi uwagami w rodzaju priorytetu dla schematu Jakobianu czy przyspieszenia pracy nad twierdzeniem Mazura, nie ingerując w szczegóły samego dowodzenia.

W zapisie rozumowania modelu, który Anthropic opublikował, Claude w pewnym momencie odnotował zakończenie kluczowego etapu krótkim wpisem po angielsku, sugerującym, że sam system rozpoznał wagę chwili. Około 7 procent linii kodu bez gotowych schematów pochodzi z nieudanych prób agentów, które ostatecznie nie weszły do finalnego dowodu, ale zostały zachowane w zapisie pracy.

Ocena środowiska matematycznego

Kevin Buzzard z Imperial College London, który od lat prowadzi społecznościowy projekt formalizacji Wielkiego Twierdzenia Fermata w Lean, zrecenzował powstały artefakt. Jego ocena, cytowana przez Anthropic, jest ostrożnie entuzjastyczna: dowód nie zakłada niczego poza aksjomatami matematyki, a sama technika autoformalizacji objęła po drodze algebrę, analizę harmoniczną, geometrię i teorię liczb.

To niezwykłe osiągnięcie autoformalizacji, które według badaczy Anthropic zajęło tylko 11 dni, dowodzi Wielkiego Twierdzenia Fermata bez żadnych założeń poza aksjomatami matematyki. Po drodze widzimy autoformalizację algebry, analizy harmonicznej, geometrii i teorii liczb, i uczymy się, że artefakty autoformalizacji AI są już wystarczająco solidne, by na nich budować - Kevin Buzzard, Imperial College London

Jeśli automatyczna formalizacja FLT jest teraz możliwa, zrobiliśmy duży krok w stronę automatycznej formalizacji współczesnej literatury matematycznej. Takie techniki autoformalizacji doprowadzą do nowych narzędzi, wyłapujących błędy w obecnym korpusie matematycznym i odciążających recenzentów - Kevin Buzzard, Imperial College London

Co to znaczy w praktyce

Formalizacja w Lean nie jest tym samym co odkrycie nowego twierdzenia. Claude nie znalazł nowej drogi dowodowej, lecz przepisał istniejące rozumowanie Wilesa w wersji doprecyzowanej później przez Darmona, Diamonda i Taylora na język, który maszyna może zweryfikować bez żadnej niepewności interpretacyjnej. To rozróżnienie jest istotne, bo odróżnia to osiągnięcie od twierdzeń o AI "tworzącej nową matematykę".

Buzzard zwraca jednak uwagę na praktyczną wartość takich narzędzi: rygorystyczne sprawdzanie dowodów generowanych przez modele językowe jest dziś zwykle bardzo kosztownym procesem prowadzonym ręcznie przez ludzi. Systemy zdolne do autoformalizacji na tę skalę mogłyby w przyszłości automatycznie weryfikować matematyczne twierdzenia produkowane przez inne modele AI, zamiast zostawiać tę pracę recenzentom.

Dla środowiska zajmującego się formalną weryfikacją matematyki to sygnał, że skala, jaką dotąd osiągały wyłącznie wieloletnie projekty społecznościowe, jest już w zasięgu pojedynczego uruchomienia modelu AI trwającego kilkanaście dni. Sama biblioteka Mathlib, budowana kolektywnie od lat, pozostaje wciąż mniejsza od samego dowodu wygenerowanego przez Claude'a dla tego jednego twierdzenia.

Koszt i ograniczenia

Projekt pochłonął około 6 miliardów tokenów wygenerowanych przez model porównywalny mocą do Claude Fable 5.1, co czyni go bardzo kosztownym obliczeniowo eksperymentem badawczym, a nie gotowym do powtarzania procesem produkcyjnym. Anthropic nie podał dokładnego kosztu w dolarach, ale skala zużycia tokenów sugeruje wydatek liczony w dziesiątkach tysięcy dolarów za pojedyncze uruchomienie.

Firma zaznacza też, że część kodu, około 7 procent linii bez gotowych schematów, powstała z nieudanych prób agentów i nie została w pełni oczyszczona z artefaktów procesu prób i błędów. Mimo to sam fakt, że tak duży formalny dowód w ogóle się skompilował i przeszedł weryfikację, traktowany jest w środowisku jako dowód dojrzałości metody, a nie tylko ciekawostka techniczna.