Claude sformalizował Wielkie Twierdzenie Fermata. 13 mln linii w 11 dni

Claude dokonał czegoś, co jeszcze niedawno wyglądało jak projekt na wiele lat pracy całego zespołu matematyków. Agenci Anthropic w ciągu 11 dni stworzyli pierwszy kompletny, komputerowo zweryfikowany zapis dowodu Wielkiego Twierdzenia Fermata, generując około 13 mln linii kodu w języku Lean.

To ważne rozróżnienie: Claude nie odkrył nowego dowodu i nie rozwiązał problemu, z którym matematycy nie potrafili sobie wcześniej poradzić. System przełożył istniejącą matematykę opartą na dowodzie Andrew Wilesa i Richarda Taylora na formalny język, w którym komputer może rygorystycznie sprawdzić każdy etap rozumowania. Mimo tego skala i tempo pracy są bezprecedensowe.

Claude stworzył pierwszy kompletny komputerowo sprawdzony dowód Wielkiego Twierdzenia Fermata

Wielkie Twierdzenie Fermata należy do najbardziej znanych problemów w historii matematyki. Pierre de Fermat zapisał około 1637 roku, że równanie an+bn=cna^n+b^n=c^n nie ma rozwiązań w dodatnich liczbach całkowitych dla wykładników większych niż 2, ale nie pozostawił dowodu swojego twierdzenia. Problem przetrwał przez ponad trzy stulecia, zanim Andrew Wiles, przy późniejszej współpracy Richarda Taylora, doprowadził do powstania poprawnego dowodu opublikowanego w 1995 roku. Była to niezwykle zaawansowana konstrukcja wykorzystująca matematykę daleko wykraczającą poza narzędzia dostępne Fermatowi w XVII wieku.

Posiadanie zaakceptowanego przez matematyków dowodu nie jest jednak tym samym co posiadanie jego całkowicie formalnej wersji. Klasyczny artykuł matematyczny jest pisany dla specjalistów i pomija wiele kroków uznawanych za oczywiste, odwołując się również do ogromnego dorobku wcześniejszej matematyki. Formalny system dowodzenia nie może sobie na to pozwolić. Każda definicja, zależność i logiczny krok muszą zostać zapisane w taki sposób, aby program mógł sprawdzić, czy z wcześniejszych założeń rzeczywiście wynika kolejny element dowodu. Claude właśnie taką wersję stworzył – od początku do końca sprawdzalną przez Lean.

Może Cię zainteresować: Europejski rywal OpenAI dostał 3 mld euro. Mistral AI jest już wart 24 mld dolarów

Projekt formalizacji miał zajmować ludziom około 10 lat

Skala zadania była znana na długo przed pojawieniem się współczesnych modeli AI. Matematyk Kevin Buzzard, który od lat zajmuje się formalizacją matematyki w Lean, mówił wcześniej, że dysponując ogromnym budżetem i zespołem specjalistów, spodziewałby się formalizacji dowodu Wielkiego Twierdzenia Fermata w perspektywie około 10 lat. W 2024 roku w Imperial College London rozpoczął się również wieloletni projekt społecznościowy mający doprowadzić do pełnej formalizacji FLT.

Claude zakończył działający end-to-end zapis w 11 dni. Nie oznacza to oczywiście, że AI w jedenaście dni wykonała dokładnie tę samą pracę, którą człowiek wykonywałby przez dekadę od pustej kartki. Agenci korzystali z istniejących zasobów Mathlib, rezultatów wcześniejszego projektu Imperial College, projektu flt-regular oraz matematycznej ekspozycji dowodu autorstwa Henriego Darmona, Freda Diamonda i Richarda Taylora. Człowiek przygotował więc ogromny fundament, na którym system mógł pracować. Przewaga Claude’a ujawniła się w tempie łączenia tych elementów, uzupełniania brakujących formalnych kroków i równoległego rozwiązywania tysięcy problemów pośrednich.

13 mln linii Lean i ponad 30 tys. twierdzeń pośrednich

Sama wielkość końcowego projektu pokazuje, czym formalizacja różni się od tradycyjnego dowodu matematycznego. W trakcie prac Claude wygenerował około 13 mln linii kodu Lean, czyli ponad pięć razy więcej niż zawiera Mathlib – główna społecznościowa biblioteka formalnej matematyki, na której projekt sam się opierał. System stworzył komputerowo sprawdzalne dowody około 30,3 tys. twierdzeń pośrednich, z czego około 29,5 tys. znalazło zastosowanie w finalnej ścieżce prowadzącej do Wielkiego Twierdzenia Fermata.

Tak ogromna liczba nie oznacza jednak, że ludzki dowód nagle liczy 13 mln „matematycznych linijek”. Lean wymaga zapisania szczegółów, które w publikacji dla matematyków mogą zostać skondensowane do pojedynczego zdania, ponieważ specjalista zna definicję, rozumie kontekst i potrafi samodzielnie odtworzyć brakujące kroki. Komputer potrzebuje znacznie większej precyzji. Formalizacja obejmuje więc całe warstwy definicji z algebry, geometrii, analizy harmonicznej i teorii liczb, które ostatecznie łączą się w jedno drzewo zależności. To właśnie możliwość automatycznego rozwijania takiej struktury na ogromną skalę jest największym osiągnięciem systemu.

Nad dowodem pracowały dziesiątki agentów Claude jednocześnie

Za rezultatem nie stoi pojedyncza sesja Claude’a trwająca jedenaście dni bez przerwy. Anthropic wykorzystało wieloagentowy system, w którym dziesiątki instancji współpracowały nad poszczególnymi elementami formalizacji. Jedni agenci definiowali potrzebne obiekty matematyczne, inni próbowali dowodzić twierdzeń pośrednich, a kolejne instancje korzystały z ukończonych rezultatów przy coraz bardziej zaawansowanych częściach głównego dowodu.

Kluczowym elementem okazała się platforma Prove2Me opracowana przez Tianyiego Penga i jego współpracowników z Columbia University. System utrzymywał graf zależności pomiędzy twierdzeniami, dzięki czemu agenci mogli zobaczyć, które elementy zostały już rozwiązane i gdzie warto skierować kolejne zasoby. Rozwiązanie ograniczało także problem utraty kontekstu podczas bardzo długiej pracy i ułatwiało ponowne wykorzystywanie już ukończonych dowodów. Wcześniejsze próby Anthropic kończyły się znacznie gorzej właśnie dlatego, że poszczególne agenty szybko traciły orientację w stanie gigantycznego projektu i przestawały skutecznie ze sobą współpracować. Dopiero odpowiednia infrastruktura organizująca pracę pozwoliła systemowi wykorzystać pełną skalę wieloagentowego podejścia.

Claude nie odkrył nowego dowodu Fermata – i to bardzo ważne

Nagłówek „AI udowodniła Wielkie Twierdzenie Fermata” byłby efektowny, ale wprowadzałby w błąd. Dowód istnieje od lat 90. i został stworzony przez ludzi. Claude nie wymyślił nowej matematycznej drogi prowadzącej do rozwiązania problemu, lecz przełożył znane rozumowanie na język formalny Lean, uzupełniając gigantyczną liczbę szczegółów wymaganych do tego, aby komputer mógł zaakceptować pełny dowód.

Nie umniejsza to jednak znaczenia rezultatu. Formalizacja tak rozbudowanej współczesnej matematyki sama w sobie jest niezwykle trudnym zadaniem wymagającym zrozumienia definicji i zależności pomiędzy wieloma dziedzinami. System nie kopiował po prostu zdań z artykułu Wilesa i nie przepisywał ich do innego formatu. Musiał wielokrotnie budować brakujące warstwy matematyczne, udowadniać twierdzenia pomocnicze oraz sprawdzać, czy kolejne konstrukcje dają się poprawnie połączyć. Dlatego rezultat jest tak ważny dla badań nad AI w matematyce: pokazuje, że modele potrafią prowadzić ogromny projekt formalny przez wiele dni, a nie jedynie rozwiązać pojedyncze zadanie olimpijskie albo wygenerować krótki dowód.

Lean sprawdził dowód bez zaufania do samego Claude’a

Najważniejszą cechą całego eksperymentu jest to, że ostatecznym arbitrem nie jest Claude ani Anthropic. Gotowy projekt został sprawdzony przez Lean, czyli system formalnego dowodzenia, który mechanicznie weryfikuje każdy krok i odrzuca konstrukcję, jeśli wyniki nie wynikają logicznie z użytych definicji oraz aksjomatów. Końcowy dowód korzysta wyłącznie ze standardowych aksjomatów dostępnych w Lean, a dodatkowe porównanie potwierdziło, że sformalizowane twierdzenie odpowiada definicji Wielkiego Twierdzenia Fermata znajdującej się w Mathlib.

To fundamentalna różnica względem sytuacji, w której model językowy po prostu generuje ładnie wyglądającą matematykę. LLM może popełnić subtelny błąd, wymyślić nieistniejący wynik albo przejść pomiędzy dwoma zdaniami w sposób, który wygląda przekonująco, ale nie jest logicznie poprawny. W formalnym środowisku taki błąd blokuje kompilację dowodu. AI nadal może tracić czas na błędne ścieżki, ale nie może „przegadać” weryfikatora. To właśnie połączenie kreatywnej zdolności modelu do proponowania kolejnych kroków z rygorystycznym sprawdzaniem przez Lean może stać się jednym z najważniejszych modeli wykorzystania AI w przyszłej matematyce.

To może zmienić sposób sprawdzania matematyki tworzonej przez AI

Znaczenie formalizacji rośnie szczególnie szybko właśnie dlatego, że modele AI zaczynają generować coraz więcej nowych rezultatów matematycznych. Jeżeli liczba potencjalnych twierdzeń i dowodów tworzonych przez systemy będzie rosła znacznie szybciej niż liczba matematyków mogących je ręcznie sprawdzić, klasyczna recenzja może stać się wąskim gardłem. Formalny dowód daje rozwiązanie tego problemu: wynik można opublikować w formie czytelnej dla człowieka, a równolegle dostarczyć jego wersję, którą komputer może sprawdzić z matematyczną precyzją.

Nie oznacza to końca tradycyjnych publikacji. Gigantyczny plik Lean o milionach linii jest kiepskim sposobem wyjaśniania matematycznej idei człowiekowi, ponieważ poprawność logiczna i zrozumiałość są dwoma różnymi problemami. Dobry dowód dla matematyka pokazuje przede wszystkim dlaczego coś działa, odkrywa strukturę problemu i pozwala wykorzystać daną ideę w kolejnych badaniach. Formalny zapis odpowiada natomiast na pytanie, czy wszystkie kroki są poprawne. Najbardziej użyteczny model przyszłości prawdopodobnie będzie więc łączył obie wersje: zwięzłą i zrozumiałą argumentację dla ludzi oraz automatycznie sprawdzalną warstwę formalną działającą w tle.

Największy sygnał może dotyczyć tego, co Claude zrobi następnym razem

Wielkie Twierdzenie Fermata było idealnym testem, ponieważ jego poprawność jest znana, a istniejąca literatura pozwala ocenić, czy AI faktycznie poradziła sobie z ogromnym projektem. Kolejnym krokiem będzie jednak wykorzystanie tej samej technologii do matematyki, której kompletnego rozwiązania jeszcze nie znamy. Anthropic informuje już o eksperymentach, w których Claude równolegle tworzył formalny zapis podczas pracy nad nowymi rezultatami, traktując Lean podobnie jak programista testy jednostkowe – jako mechanizm pozwalający natychmiast sprawdzać, czy kolejna hipoteza rzeczywiście działa.

To może okazać się znacznie ważniejsze niż sam rekord 13 mln linii. Agent może proponować pomysł, próbować formalnie go udowodnić, natychmiast znaleźć miejsce, w którym argument się rozpada, zmienić hipotezę i rozpocząć kolejną próbę. Zamiast generować potencjalny dowód, który człowiek musi później przez tygodnie weryfikować, system otrzymuje automatyczną informację zwrotną podczas samego procesu badawczego. Jeśli modele zachowają zdolność pracy nad tak dużymi strukturami również przy problemach bez gotowej mapy rozwiązania, matematyka może stać się jednym z pierwszych obszarów nauki, w których autonomiczne agenty rzeczywiście zaczną uczestniczyć w odkrywaniu nowych wyników.

Podsumowanie

Claude stworzył pierwszą kompletną komputerowo zweryfikowaną formalizację Wielkiego Twierdzenia Fermata, pracując w dużej mierze autonomicznie przez 11 dni. Wieloagentowy system wygenerował około 13 mln linii Lean, stworzył ponad 30 tys. komputerowo sprawdzalnych twierdzeń pośrednich i doprowadził cały łańcuch argumentacji do wyniku, który Lean zaakceptował jako poprawny.

Nie jest to nowy dowód twierdzenia Fermata i nie zastępuje matematyki stworzonej przez Andrew Wilesa, Richarda Taylora oraz całe pokolenia badaczy, na których pracy opiera się rezultat. Jest natomiast demonstracją czegoś innego: AI potrafi już autonomicznie organizować i formalizować matematykę w skali, która jeszcze kilka lat temu wydawała się projektem dla dużego zespołu pracującego przez lata.

I właśnie dlatego 11 dni oraz 13 mln linii są ważniejsze niż efektowny rekord. Jeśli podobne systemy zaczną automatycznie tworzyć formalnie weryfikowalne wersje nowych wyników naukowych, problemem matematyki przyszłości może przestać być samo sprawdzanie, czy dowód jest poprawny. Znacznie ważniejsze stanie się pytanie, które spośród tysięcy poprawnych wyników generowanych przez AI są naprawdę interesujące i warte zrozumienia przez człowieka.

Źródło: Anthropic – Formalizing Fermat’s Last Theorem, 4 września 2026 roku. Opracowanie własne.

Dziękujemy za przeczytanie artykułu na Techoteka.pl.
Publikujemy codziennie informacje o sztucznej inteligencji, nowych technologiach, IT oraz rozwoju agentów AI.
Obserwuj nas na Facebooku, aby nie przegapić kolejnych artykułów.