Według Anthropic jego AI Claude wygenerowało pierwszy w pełni weryfikowalny komputerowo dowód Wielkiego Twierdzenia Fermata, kończąc pracę w 11 dni, w dużej mierze samodzielnie, tworząc przy tym najdłuższy dowód matematyczny w historii.

Projekt prowadzony przez ludzi na Imperial College London pracuje nad dokładnie tym samym zadaniem od 2024 roku i nie jest bliski ukończenia. Claude wyprzedziło go na finiszu. Kevin Buzzard, matematyk kierujący projektem na Imperial, przejrzał dowód Claude i potwierdził, że wytrzymuje on kontrolę, opierając się wyłącznie na najbardziej podstawowych regułach logicznych matematyki.

Zgodnie z informacją Anthropic Claude napisało najdłuższy dowód matematyczny w historii i użyło go do formalnego udowodnienia Wielkiego Twierdzenia Fermata — problemu, przez 358 lat stawiającego matematyków w zakłopotanie. Sztuczna inteligencja dokonała tego w 11 dni, w większości samodzielnie, generując 13 milionów wierszy kodu, które komputer może sprawdzić linijka po linijce, zamiast wymagać zaufania do słowa matematyka.

Wielkie Twierdzenie Fermata mówi, że nie istnieją trzy dodatnie liczby całkowite, które po podniesieniu każdej do potęgi wyższej niż 2 mogą spełniać równanie, w którym suma dwóch pierwszych równa się trzeciej. Pierre de Fermat zanotował to twierdzenie na marginesie książki matematycznej w 1637 roku, dodając, że ma „prawdziwie cudowny dowód”, który nie mieści się na zbyt małym marginesie. Potem zmarł. Matematycy przez następne 358 lat próbowali odtworzyć to, co miał na myśli.

Udowodnienie czegoś i sprawdzenie tego to dwa różne zadania

Dowód matematyczny to łańcuch logicznych kroków — jeśli jedno ogniwo jest wadliwe, całość się rozpada. Znalezienie tej jednej wady, ukrytej gdzieś w stu stronach gęstej argumentacji, może zająć innym matematykom lata życia.

Sformalizowanie dowodu oznacza przełożenie go na język tak dosłowny, że komputer może samodzielnie zweryfikować każdy krok, bez wchodzenia w subiektywne oceny.

Matematycy od dawna zmagają się z weryfikacją. Niemiecka nagroda z 1908 roku — warta w przeliczeniu na dzisiejsze pieniądze około 1 do 2 milionów dolarów, oferowana za pierwszy poprawny dowód twierdzenia — przyciągnęła 621 błędnych zgłoszeń już w pierwszym roku.

Jak napisało Anthropic na X:

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

Prawdziwy dowód pojawił się dopiero w 1995 roku, autorstwa brytyjskiego matematyka Andrew Wilesa, i miał on niespodziewany zwrot akcji. Wiles ogłosił swoje rozwiązanie podczas trzech wykładów w czerwcu 1993 roku, ale recenzent znalazł w nim później lukę. Prawie rok naprawiał ją wraz z byłym studentem, Richardem Taylorem, był bliski porażki i w końcu opublikował poprawiony, 129-stronicowy dowód w maju 1995 roku. Opierał się on na matematyce, która nie istniała za życia Fermata — to główny powód, dla którego matematycy dziś wątpią, czy „cudowny dowód” samego Fermata kiedykolwiek działał.

Matematyka weryfikowana komputerowo ma już dekady historii. Pierwszym znanym przypadkiem był wspomagany komputerowo dowód Twierdzenia o Czterech Kolorach z 1976 roku, który wywołał trwającą do dziś debatę, czy dowód, którego żaden człowiek nie jest w stanie w całości odczytać ręcznie, powinien się liczyć. Języki dowodów formalnych, takie jak Lean — stworzony przez Leonardo de Mourę, pierwotnie w Microsoft Research — narodziły się właśnie z tego napięcia, pozwalając oprogramowaniu dokonywać weryfikacji, by ludzie mogli i tak ufać wynikowi.

W 2024 roku Kevin Buzzard z Imperial College London rozpoczął projekt mający zrobić dokładnie to, co właśnie uczyniło Claude: przełożyć dowód Wilesa na Lean, język weryfikowalny przez komputery. To rodzaj pracy wymagający armii matematyków-ochotników — sam konspekt projektu liczy 86 stron, a jego finansowanie jest zabezpieczone do 2029 roku. Claude ukończyło całość w 11 dni.

Jak Claude naprawdę tego dokonało

Anthropic wyjaśnia w obszerniejszym wpisie, że Tianyi Peng, który wraz z zespołem na Columbia buduje narzędzia formalizacyjne oparte na AI, postanowił sprawdzić, jak daleko Claude zajdzie samodzielnie. Dziesiątki agentów Claude pracowały równolegle, zapisując definicje, dowodząc drobnych wyników i układając je w większe — przy niemal zerowym udziale człowieka, poza okazjonalnymi wskazówkami typu „nadaj temu twierdzeniu priorytet”.

Początkowo nie szło gładko. We wczesnej fazie agenci tracili rachunek tego, co już udowodnili, i przestawały współpracować; te fałszywe starty wciąż stanowią około 7% wierszy ostatecznego dowodu.

Rozwiązaniem okazało się narzędzie o nazwie Prove2Me, również zbudowane przez zespół Penga, które dawało każdemu agentowi tę samą aktualną listę zadań — które mniejsze dowody wciąż wymagają wykonania — dzięki czemu nikt nie dublował pracy ani nie zbaczał z toru. Narzędzie uporządkowało też pliki tak, by Lean mógł wszystko sprawdzać szybciej, oraz prowadziło notatki w prostym języku o każdym wyniku, by agenci mogli korzystać z pracy innych zamiast wymyślać ją od nowa.

Do momentu zakończenia Claude udowodniło ponad 30 000 twierdzeń pomocniczych i zużyło miliardy tokenów, działając na modelu badawczym, który według Anthropic jest mniej więcej porównywalny z Claude Fable 5.1, wersją udostępnioną później publicznie. Gotowy dowód liczy 13 milionów wierszy — ponad pięć razy więcej niż Mathlib, wspólna biblioteka, z której matematycy już korzystają w tego typu pracy.

Typowa powieść liczy 80 000 słów. Dowód Claude odpowiada 160 powieściom czystej argumentacji logicznej.

Czy to się w ogóle liczy?

Buzzard — którego własna wersja tego projektu pozostaje finansowana do 2029 roku — przejrzał dowód Claude i udzielił mu swojej aprobaty, stwierdzając, że dowodzi on twierdzenia „bez żadnych założeń poza aksjomatami matematyki”.

To nie to samo, co odkrycie przez Claude zupełnie nowej matematyki, czego Anthropic wcześniej twierdziło w przypadku swoich badań kryptograficznych. Wiles udowodnił twierdzenie Fermata trzy dekady temu — Claude stworzyło jedynie weryfikowalną maszynowo potwierdzenie tego wyniku. Ma to znaczenie, ponieważ matematycy coraz bardziej zalewa fala niezweryfikowanych dowodów, w tym pisanych przez AI, szybciej niż ludzie są w stanie sprawdzać je ręcznie. Takie sformalizowane dowody są też deterministyczne i niepodatne na ludzkie błędy, co w matematyce ma ogromne znaczenie.

Nie jest to nowy problem. Wspomagany komputerowo dowód hipotezy Keplera zajął cztery lata, zanim komisja recenzencka zdecydowała się jedynie na stwierdzenie „99% pewności”, a pełne zrozumienie dowodu hipotezy Poincarégo Grigorija Perelmana zajęło mniej więcej tyle samo czasu.

Kto nie chce wierzyć Anthropic na słowo, nie musi. Pełny, 13-milionowoliniowy dowód jest dostępny na GitHubie, za darmo dla każdego matematyka mającego dość czasu, by rozebrać go na części, linijka po linijce.