Anthropic formalizuje Wielkie Twierdzenie Fermata
Firma Anthropic poinformowała o pierwszym w historii pełnym, zweryfikowanym komputerowo dowodzie, którego przedmiotem jest Wielkie Twierdzenie Fermata. Autonomiczna praca prowadzona głównie przez rodzinę modeli sztucznej inteligencji Claude w systemie dowodzącym Lean zakończyła się sukcesem po zaledwie 11 dniach. Sukces ten demonstruje, że sztuczna inteligencja jest zdolna nie tylko do rozwiązywania problemów tekstowych, ale też do prowadzenia niezwykle złożonych procesów formalizacji w rygorystycznych ramach nowoczesnej matematyki.
13 milionów linii w języku Lean
Projekt badawczy zainicjował Tianyi Peng, naukowiec Anthropic z Uniwersytetu Columbia. Modele Claude działały za pośrednictwem systemu opartego na narzędziu Claude Code oraz otwartej platformy Prove2Me, generując we współpracy łącznie 13 milionów linii kodu w języku Lean. Jest to objętość ponad pięciokrotnie większa niż Mathlib, czyli główna biblioteka matematyczna tego ekosystemu.
Na przestrzeni niespełna dwóch tygodni algorytmy Anthropic zużyły około 6 miliardów tokenów wyjściowych z wewnętrznego modelu badawczego, porównywalnego parametrami z wersją Claude Fable 5.1. Sztuczna inteligencja dowiodła w tym czasie 30 300 twierdzeń pobocznych, z czego ostatecznie 29 500 zostało faktycznie wykorzystanych do sfinalizowania dowodu.
W toku prac zespoły sztucznych agentów wielokrotnie obierały złe ścieżki badawcze i ponosiły porażki. Jak podaje Anthropic, błędne próby nie poszły jednak całkowicie na marne – złożyły się one na około 7% docelowych, spersonalizowanych linii kodu. Utrzymanie spójności i pamięci w tak przepastnym środowisku ułatwiła właśnie platforma Prove2Me. Utrzymywała ona skierowany graf acykliczny (DAG) twierdzeń oraz przyspieszała kompilację kodu z użyciem języka Lean, oddzielając żmudne deklaracje od faktycznych dowodów. Rola człowieka w tym ogromnym przedsięwzięciu ograniczała się głównie do rzadkich wskazówek wysokiego poziomu zlecanych przez Tianyi Penga – poleceń w stylu: „Jacobian as a scheme sounds high priority” czy „push [the] Mazur [theorem] to be done soon”.
Od prac Wilesa po Mathlib
Wielkie Twierdzenie Fermata pozostawało zagadką z gatunku nieudowodnionych przez ponad 350 lat. Dopiero w 1995 roku pierwszą poprawną pracę przedstawił Andrew Wiles (choć za rozwiązanie tego problemu już w 1908 roku ufundowano nagrodę w wysokości 100 000 marek w złocie). Projekt udostępniony przez Anthropic oparł się precyzyjnie na uproszczonej wersji dowodu Wilesa, którą wcześniej opublikowali badacze tacy jak: Darmon, Diamond and Taylor.
Dowód wygenerowany przez algorytmy Claude bazuje na zaledwie trzech standardowych aksjomatach systemu Lean, a automatyczny komparator poświadczył, że ostateczne sformułowanie twierdzenia wprost pokrywa się z zapisem używanym w społecznościowej bibliotece Mathlib. Triumf Anthropic jest w rzeczywistości blisko powiązany z długofalową wizją środowiska akademickiego. Wysiłek formalizacyjny wokół tego zagadnienia wywodzi się bezpośrednio ze społecznościowego projektu z 2024 roku, któremu przewodzi Kevin Buzzard z Imperial College London.
Buzzard, po weryfikacji cyfrowych rezultatów prac zespołu z użyciem sztucznej inteligencji, skomentował: „This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered”.
Przyszłość recenzowania matematyki
Obecnie rzetelna weryfikacja nowych twierdzeń matematycznych nierozerwalnie łączy się z drobiazgową, żmudną i często trwającą całe lata pracą ludzi. Pełna autoformalizacja z asystentem AI drastycznie obniżyłaby barierę wejścia i pozwoliła na ominięcie „wąskich gardeł” dla nowoczesnego, globalnego środowiska recenzenckiego. Warto podkreślić, że Claude udowodnił swoje predyspozycje nie tylko w przypadku Fermata. Podjęto też mniejszy eksperyment, w którym wykorzystano wyłącznie trzy standardowe konta subskrypcyjne w planie Claude Max. Maszyny te doprowadziły do bezbłędnej formalizacji zadania znanego jako Vinogradov's Three Primes Theorem w oparciu o popularne w tych kręgach narzędzie Hardy-Littlewood Circle Method. Tak obszerne wyzwanie zrealizowano w imponującym czasie 3 dni.
Zarówno badacze z ramienia Anthropic, jak i zewnętrzni analitycy ze świata matematyki zgadzają się ze sobą: unikalna zdolność potężnych LLM-ów do autoformalizacji to najpoważniejszy dotąd krok na drodze do stworzenia w pełni zautomatyzowanych metod weryfikacji prac naukowych. W jednej z notatek zapisanych w trakcie pracy podsumował to model Claude – który po znalezieniu finalnego dowodu wygenerował na swój użytek następujący wpis: „!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign's goal: e2e FLT on prove2me”.
