Anthropic ogłosił 4 września 2026 roku, że Claude, pracując w dużej mierze samodzielnie przez 11 dni, napisał pierwszy kompletny, sprawdzony przez komputer dowód Wielkiego Twierdzenia Fermata w języku Lean. Formalizacja liczy ponad 13 milionów linii kodu i 29 500 twierdzeń pomocniczych, a Kevin Buzzard z Imperial College London, który od 2024 roku prowadzi społecznościowy projekt formalizacji tego samego twierdzenia, samodzielnie skompilował repozytorium i potwierdził, że dowód przechodzi weryfikację.
- Claude, pracując w dużej mierze samodzielnie przez 11 dni, napisał pierwszy kompletny, sprawdzony przez komputer dowód Wielkiego Twierdzenia Fermata w języku Lean – formalizacja liczy ponad 13,4 miliona linii kodu i 29 500 twierdzeń pomocniczych, a Kevin Buzzard z Imperial College London samodzielnie skompilował repozytorium i potwierdził, że dowód przechodzi weryfikację.
- Cały proces pochłonął około sześciu miliardów tokenów wyjściowych, a pełna budowa zajęła 5 godzin i 32 minuty przy 96 zadaniach równoległych ze szczytowym zużyciem 153 GB pamięci; dla porównania Buzzard przez pięć lat realizował analogiczny projekt z grantem EPSRC wynoszącym milion funtów.
- Buzzard ocenił, że „matematycznie ta praca Anthropic nie mówi nam w zasadzie nic", ponieważ formalizacja wiernie podąża za wczesną literaturą i nic do niej nie dodaje, a wartość wyniku leży w tym, że – jego zdaniem – „artefakty autoformalizacji tworzone przez AI są już na tyle solidne, że można na nich budować".
Chcesz czytać więcej treści związanych z AI?
Dodaj AIPORT.pl do preferowanych źródeł Google
Jedenaście dni zamiast lat: skala projektu w liczbach
Dziesiątki agentów Claude’a udowodniło po drodze 30 300 twierdzeń, z czego 29 500 trafiło do finalnego dowodu. Cały proces pochłonął około sześciu miliardów tokenów wyjściowych z wewnętrznego modelu badawczego Anthropic, który firma opisuje jako z grubsza porównywalny z Claude Fable 5.1. Sam moment zamknięcia dowodu jest udokumentowany: z opublikowanych przez Anthropic fragmentów rozumowania modelu wynika, że korzeń dowodu na platformie Prove2Me uzyskał status „PROVED” 18 sierpnia 2026 roku o godzinie 02:00 czasu UTC.
Skala jest bezprecedensowa. Anthropic podaje, że jego formalizacja jest ponad pięciokrotnie większa od Mathlib, głównej biblioteki sformalizowanej matematyki społeczności Lean, na której się opiera. Buzzard, który pobrał kod, doprecyzował, że mówimy o ponad 13,4 miliona linii, a kompilacja całości trwa niemal dwudziestokrotnie dłużej niż kompilacja Mathlib, i to na maszynie ze 96 rdzeniami. W przypisie do własnego komunikatu Anthropic przyznaje, że jego dowód jest prawdopodobnie znacznie dłuższy, niż musiałby być.
Dowód sprawdziły dwa niezależne jądra, a Buzzard powtórzył weryfikację u siebie
Weryfikowalność jest tu ważniejsza od samego rekordu, bo nikt nie przeczytał 13 milionów linii. Repozytorium anthropics/fermats-last-theorem opublikowane na licencji Apache 2.0 dokumentuje, co dokładnie sprawdzono:
- Lean 4.33.1 zbudował wszystkie 60 475 modułów repozytorium, a jądro systemu sprawdziło każdą deklarację.
- Narzędzie comparator w wersji 4.33.0 potwierdziło, że udowodnione twierdzenie jest identyczne z twierdzeniem sformułowanym wyłącznie w Mathlib, i wydało werdykt „Your solution is okay!”.
- Drugie, niezależne jądro Lean o nazwie nanoda, napisane w Rust, zaakceptowało eksport środowiska i sprawdziło 1 052 234 deklaracje bez błędów.
- Dowód opiera się wyłącznie na trzech standardowych aksjomatach Lean, a w kodzie nie ma
sorry, dodanych aksjomatów ani obejść typunative_decide. - Odtworzenie wyniku jest kosztowne, ale możliwe: pełna budowa zajęła Anthropic 5 godzin i 32 minuty przy 96 zadaniach równoległych, ze szczytowym zużyciem 153 GB pamięci.
Buzzard zrobił to samo we własnym zakresie. Napisał na blogu Xena Project, że skompilował kod, uruchomił comparator i wynik się zgadza. Anthropic udostępnił mu maszynę z 500 GB pamięci RAM oraz zestaw dokumentów HTML, które w praktyce łatwiej przeglądać niż samo repozytorium.
Pierwsze podejście się nie udało. Przełomem była zewnętrzna platforma Prove2Me
Anthropic przyznaje, że początkowe próby zakończyły się porażką: agenci mieli wczesne sukcesy, ale szybko tracili orientację w stanie projektu i przestawali skutecznie współpracować. Nieudane próby odpowiadają za około 7 procent linii w finalnym dowodzie, jeśli pominąć kod szablonowy.
Sytuacja zmieniła się po przejściu na Prove2Me, otwartą platformę do wspólnej formalizacji matematyki zaprojektowaną przez Tianyi Penga, badacza Anthropic, i jego współpracowników z Uniwersytetu Columbia. Platforma utrzymuje skierowany graf acykliczny twierdzeń, dzięki czemu agenci wiedzą, co warto udowodnić w następnej kolejności, rozdziela treści twierdzeń i dowodów do osobnych plików, co przyspiesza kompilację, oraz przechowuje opis każdego twierdzenia w języku naturalnym, co ułatwia ponowne wykorzystanie gotowych fragmentów. Wkład człowieka ograniczał się do sporadycznych podpowiedzi wysokiego poziomu od Penga, w rodzaju sugestii, żeby priorytetowo potraktować jakobian jako schemat.
Nie mam wątpliwości, że to moment przełomowy, ale przełom dotyczy inżynierii weryfikacji, a nie teorii liczb. Anthropic nie udowodnił niczego nowego. Pokazał, że tysiące stron literatury matematycznej da się przełożyć na kod sprawdzalny maszynowo w tempie, o jakim społeczność Lean nie mogła dotąd myśleć.
Dwie rzeczy każą mi jednak studzić entuzjazm. Po pierwsze, ten wynik nie powstał w próżni: repozytorium Anthropic zawiera 106 plików z materiałem pochodzącym z projektu FLT prowadzonego na Imperial College London i z projektu flt-regular. Bez lat pracy społeczności nie byłoby jedenastu dni. Po drugie, maszyna sprawdza logikę, ale nie sprawdza sensu nazw. Anthropic sam pisze w dokumentacji, że żadne narzędzie nie zweryfikuje, czy pojedyncze twierdzenie pośrednie znaczy to, co sugeruje jego nazwa. To zadanie zostaje po stronie człowieka.
Pytanie, które zadaję sobie po lekturze repozytorium, brzmi tak: czy za dwa lata recenzent artykułu matematycznego będzie wymagał dołączenia formalizacji, tak jak dziś wymaga danych do eksperymentu? Jeśli tak, to najciekawsze skutki tej historii dopiero nadejdą.
Piotr Wolniewicz, Redaktor Naczelny AIPORT.pl
Opisz krótko, czego potrzebujesz. Jesteśmy największym HUB-em AI w Polsce — w naszej bazie znajdziesz blisko 500 zweryfikowanych firm specjalizujących się w AI. W Twoim imieniu poprosimy 3-5 dopasowanych wykonawców o kontakt w ciągu 48 godzin.
Buzzard: matematycznie ta praca nie mówi nam nic nowego
Recenzent dowodu ocenia jego wartość zaskakująco chłodno. „Matematycznie ta praca Anthropic nie mówi nam w zasadzie nic” / „mathematically this work of anthropic tells us essentially nothing”, napisał Buzzard, dodając, że jest w 99,9 procent pewien poprawności dowodu Wilesa, a większość społeczności teorii liczb jest pewna w stu procentach. Formalizacja wiernie podąża za wczesną literaturą i, jego zdaniem, nic do niej nie dodaje.
Wartość leży gdzie indziej. W komentarzu przekazanym Anthropic Buzzard stwierdził, że „artefakty autoformalizacji tworzone przez AI są już na tyle solidne, że można na nich budować” / „AI autoformalization artefacts are now robust enough to be built upon”. Na blogu rozwinął tę myśl: skoro tysiące stron da się sformalizować w 11 dni, to w przyszłości formalizacja współczesnych badań będzie się odbywać na bieżąco, a maszyny bezlitośnie wskażą argumenty, które są niekompletne. Buzzard od lat powtarza, że formalizacja uczyniła go bardziej podejrzliwym wobec literatury matematycznej niż większość kolegów.
Jest też różnica techniczna, o której nie wspomina komunikat Anthropic. Dowód nie idzie drogą nowoczesną, którą formalizuje zespół Buzzarda, tylko za wykładem Darmona, Diamonda i Taylora z 1995 roku, przez twierdzenie Langlandsa-Tunnella i twierdzenie Ribeta o obniżaniu poziomu. Sama ścieżka Anthropic działa dla liczb pierwszych p ≥ 17, ale przypadki mniejsze były już wcześniej sformalizowane dla nieparzystych liczb pierwszych regularnych, a najmniejsza liczba nieregularna to 37, więc całość się domyka. Repozytorium jawnie korzysta z projektu flt-regular obejmującego twierdzenie Kummera.
Sześć miliardów tokenów kontra milion funtów grantu
Koszt tej operacji jest jedną z najciekawszych niewiadomych. Buzzard napisał wprost, że na swój pięcioletni projekt dostał od brytyjskiej agencji EPSRC milion funtów, a Anthropic potrzebowało 11 dni, i zastanawia się, czy firma nie wydała więcej. Anthropic nie ujawnił kosztu, podał jedynie zużycie około sześciu miliardów tokenów wyjściowych.
Skala nie musi jednak oznaczać poziomu dostępnego wyłącznie dla laboratoriów frontierowych. W ramach mniejszego eksperymentu badacze Anthropic użyli trzech zwykłych, indywidualnych subskrypcji Claude Max i przez samą platformę Prove2Me sformalizowali twierdzenie Winogradowa o trzech liczbach pierwszych w trzy dni. Firma uważa, że przy odpowiednim rusztowaniu wspólna formalizacja poważnych wyników jest osiągalna na konsumenckich abonamentach. To odróżnia ten projekt od wcześniejszych głośnych wyników z udziałem modeli Anthropic, takich jak obalenie hipotezy Jacobiego przez Claude Fable 5, gdzie liczyła się pojedyncza, trafna intuicja, a nie przemysłowa skala.
Wielkie Twierdzenie Fermata było ostatnią pozycją na słynnej liście stu wyzwań formalizacyjnych Freeka Wiedijka. Zdaniem Buzzarda wynik Anthropic zamyka ten dwudziestoletni benchmark.
Za każdą polską firmą AI stoi konkretny człowiek z imieniem i nazwiskiem, często ten sam w kilku miejscach naraz, i to właśnie ludzie, nie tabelki finansowania, są prawdziwym bohaterem tego artykułu.
Polska ma własny system dowodzenia twierdzeń. Mizar działa od 1973 roku
Polski czytelnik ma w tej historii mocniejszy punkt zaczepienia, niż mogłoby się wydawać. Formalizacja matematyki nie zaczęła się od Lean, tylko w dużej mierze od systemu Mizar, projektu zapoczątkowanego w 1973 roku w Płocku przez Andrzeja Trybulca i koordynowanego dziś przez zespół na Uniwersytecie w Białymstoku.
Mizar Mathematical Library, czyli baza budowana wokół tego systemu, jest jedną z najstarszych i największych kolekcji tego typu na świecie. Według Wydziału Informatyki Uniwersytetu w Białymstoku zawiera ponad 65 tysięcy twierdzeń i ponad 13,5 tysiąca definicji w ponad 1400 artykułach, a złożyło się na nią ponad 260 autorów, głównie z Polski, Japonii, Kanady, Chin, Włoch i Niemiec. Uczelnia od 1990 roku wydaje kwartalnik „Formalized Mathematics”, w którym publikowane są streszczenia artykułów zweryfikowanych przez system.
Znaczenie tego kontekstu jest praktyczne. Jeśli autoformalizacja przy pomocy modeli językowych stanie się standardowym narzędziem recenzji naukowej, polskie ośrodki mają kompetencje, doświadczenie i infrastrukturę, żeby uczestniczyć w tej zmianie od strony merytorycznej, a nie tylko jako odbiorcy narzędzi budowanych w Kalifornii. Trudno jednocześnie nie zauważyć, że tempo narzucone przez Anthropic pokazuje różnicę zasobów: pięcioletni grant kontra 11 dni pracy floty agentów.
Źródła i metodologia
Artykuł powstał na podstawie analizy redakcji AIPORT.pl oraz źródeł pierwotnych, w tym komunikatu badawczego Anthropic „Formalizing Fermat’s Last Theorem” z dnia 04.09.2026, dokumentacji technicznej opublikowanej w repozytorium anthropics/fermats-last-theorem oraz wpisu Kevina Buzzarda na blogu Xena Project z dnia 04.09.2026. Dane o polskim systemie Mizar pochodzą ze strony Wydziału Informatyki Uniwersytetu w Białymstoku.
Cytaty Kevina Buzzarda, profesora matematyki czystej w Imperial College London, zostały zweryfikowane z oryginalnym anglojęzycznym materiałem źródłowym.
Komentarz redakcyjny i ocena kontekstu branżowego: Piotr Wolniewicz, Redaktor Naczelny AIPORT.pl.
Artykuł będzie aktualizowany w miarę pojawiania się nowych informacji na temat autoformalizacji matematyki i weryfikacji dowodów generowanych przez modele AI.
