Anthropic: agenci Claude’a sformalizowali Wielkie Twierdzenie Fermata w Lean 4

Wielkie Twierdzenie Fermata zapisane tak, by mógł je sprawdzić komputer

Anthropic poinformowało 4 września 2026 roku, że agenci Claude’a przygotowali w Lean 4 kompletną formalizację Wielkiego Twierdzenia Fermata, sprawdzoną przez komputer. Według firmy jest to pierwsze takie osiągnięcie, a zasadnicza praca agentów trwała około 11 dni i przebiegała w dużej mierze samodzielnie. Oba zastrzeżenia są ważne: pierwszeństwo i stopień samodzielności opisuje samo Anthropic, natomiast opublikowany materiał formalizuje znaną drogę dowodową. Nie jest nowym dowodem ani rozwiązaniem problemu, który pozostawałby dotąd otwarty.

Różnica nie umniejsza znaczenia przedsięwzięcia. Dowód matematyczny zapisany dla ludzi opiera się na wspólnej wiedzy, skrótach oraz umiejętności odtwarzania pominiętych kroków. System formalny nie może przyjąć, że „reszta jest oczywista”. Każda definicja, zależność i przejście muszą zostać przedstawione w postaci, którą jądro programu sprawdzającego potrafi zweryfikować zgodnie z regułami logiki. Dlatego formalizacja dobrze znanego twierdzenia jest osobnym zadaniem inżynieryjnym i matematycznym: nie odkrywa nowego twierdzenia, lecz przekształca istniejący dorobek w drobiazgowo kontrolowany zapis.

W udostępnionej wersji twierdzenie mówi, że dla liczby naturalnej n nie mniejszej niż 3 oraz dodatnich liczb naturalnych a, b i c równość aⁿ + bⁿ = cⁿ nie zachodzi. Repozytorium wskazuje drogę wytyczoną przez Freya, Serre’a, Ribeta, Wilesa oraz Taylora i Wilesa. Konstrukcja opiera się na klasycznym ujęciu Darmona, Diamonda i Taylora. Jest więc komputerowo sprawdzalnym zapisem rozbudowanej, już znanej matematyki, powstałej dzięki pracy wielu osób, a także dzięki wcześniejszym zasobom bibliotek formalnych.

Skala, której nie należy sprowadzać do jednej liczby

Anthropic podaje 13 milionów wierszy kodu Lean, około sześciu miliardów wygenerowanych tokenów oraz 30 300 udowodnionych wyników pośrednich. W ostatecznym dowodzie wykorzystano około 29 500 z nich. Inwentarz repozytorium przedstawia inne, precyzyjniej zdefiniowane wielkości: 29 511 stron twierdzeń, 1450 modułów definicji oraz 60 475 zbudowanych modułów.

Tych wartości nie powinno się bezpośrednio ze sobą porównywać ani przedstawiać jako sprzecznych. Opisują różne elementy i etapy przedsięwzięcia. Liczba wyników pośrednich nie jest tym samym co liczba stron twierdzeń, a liczba modułów zbudowanych nie oznacza liczby niezależnych odkryć matematycznych. Zestawienie pokazuje natomiast, jak rozległe zaplecze trzeba było uporządkować, aby końcowe stwierdzenie dało się przeprowadzić przez rygorystyczną kontrolę systemu.

Także sześć miliardów tokenów jest miarą aktywności modelu, nie rachunkiem ekonomicznym. Na tej podstawie nie da się wiarygodnie wyliczyć kosztu pieniężnego ani zużycia energii całego przedsięwzięcia. W publicznie opisanych danych nie ma pełnego rozliczenia, które pozwalałoby na takie wnioski. Odpowiedzialna ocena powinna zatem oddzielać imponującą skalę obliczeń od kosztów, których dotąd nie ujawniono w kompletnej postaci.

Co właściwie sprawdza Lean

Projekt dokładnie określa używane wersje: Lean 4.33.1 oraz Mathlib v4.33.0. To szczegół o praktycznym znaczeniu, ponieważ odbiorca nie pozostaje z ogólnym zapewnieniem, że kod „działa w Lean”. Domyślna kontrola wymaga ponadto, aby końcowe twierdzenie zależało dokładnie od trzech wskazanych składników logicznych: propext, Classical.choice i Quot.sound.

Nie oznacza to, że maszyna samodzielnie oceniła prawdziwość dowolnej opowieści matematycznej. Lean sprawdza formalny zapis względem określonych reguł, definicji i zależności. Wartość publikacji bierze się więc z połączenia dwóch rzeczy: ogromnego materiału przełożonego na język systemu oraz niewielkiego, rygorystycznego mechanizmu kontroli, który odrzuca kroki nieuzasadnione w tym środowisku. Przypięcie wersji pomaga też ustalić, czego dokładnie dotyczy deklaracja o pomyślnym sprawdzeniu.

Dla osób chcących ocenić wynik najważniejszy jest opublikowany zapis, nie sama liczba tokenów ani efektowne określenie „autonomiczny”. Można zacząć od treści końcowego twierdzenia, następnie sprawdzić opis zastosowanej drogi dowodowej, wykaz modułów oraz wymagane wersje Lean i Mathlib. Taka kolejność chroni przed dwoma skrajnymi odczytaniami: uznaniem, że model odkrył nową matematykę, albo przeciwnie — że formalne zapisanie znanego dowodu jest tylko mechanicznym przepisywaniem.

Dlaczego to jest użyteczny postęp

Najbardziej obiecujący aspekt nie polega na zastąpieniu matematyków. Rezultat pokazuje raczej, że agenci mogą podjąć długie, wieloetapowe zadanie formalizacyjne, w którym trzeba tworzyć tysiące wyników pomocniczych i doprowadzić je do jednego sprawdzalnego finału. Jeżeli podobne metody okażą się powtarzalne, mogą zmniejszyć nakład żmudnej pracy potrzebnej do przenoszenia istniejącej matematyki do bibliotek dowodów formalnych. To z kolei może ułatwić kontrolowanie zależności, wykrywanie luk w zapisie i ponowne wykorzystywanie precyzyjnie opisanych wyników.

Nie jest to jednak jeszcze dowód na to, że każdy obszerny argument matematyczny można w ten sposób szybko sformalizować. Jeden imponujący projekt nie określa kosztu kolejnych realizacji, ich niezawodności ani nakładu nadzoru potrzebnego w innych dziedzinach. Sam opis „w dużej mierze samodzielnej” pracy również wymaga zachowania przypisania do źródła: tak przebieg przedsięwzięcia przedstawia Anthropic. Dodatkowo końcowa formalizacja korzysta z wieloletniego dorobku autorów klasycznego dowodu, jego późniejszych opracowań oraz twórców bibliotek formalnych.

Właśnie te ograniczenia pozwalają właściwie nazwać dobrą wiadomość. Nie otrzymaliśmy nowego dowodu Wielkiego Twierdzenia Fermata ani rozwiązania otwartego problemu. Otrzymaliśmy według Anthropic pierwszą kompletną, komputerowo sprawdzoną formalizację tego twierdzenia w Lean 4, wraz z publicznym repozytorium i konkretnie wskazanym środowiskiem kontroli. Rezultat można więc badać bezpośrednio, a nie przyjmować wyłącznie jako zapowiedź producenta modelu.

To istotny krok dla współpracy między matematyką, automatyką dowodzenia i modelami językowymi. Jego miarą nie jest wyłącznie rozmiar wygenerowanego kodu, lecz to, czy rozległy zapis daje się sprowadzić do jasno określonego twierdzenia i przejść formalną kontrolę. Dopiero kolejne projekty pokażą, jak często taki wynik można odtworzyć i przy jakich kosztach. Już teraz publikacja dostarcza jednak konkretnego materiału do sprawdzania, porównywania i rozwijania — a to znacznie więcej niż demonstracja zakończona samą deklaracją sukcesu.