Lean zatwierdził dowód Fermata Claude’a

Lean, używany przez matematyków na całym świecie system weryfikacji dowodów, zaakceptował pełną formalizację wielkiego twierdzenia Fermata. Opracowany przez system Claude firmy Anthropic i udostępniony w otwartym repozytorium zapis nie zawiera niewypełnionych luk, dodatkowych aksjomatów ani skrótów obliczeniowych wykraczających poza standardowe podstawy Lean (repozytorium). Projekt niezależnie skompilował Kevin Buzzard, matematyk z Imperial College London, który kierował własnymi pracami nad formalizacją twierdzenia. Potwierdził poprawność dowodu i nazwał go „niezwykłym osiągnięciem w automatycznej formalizacji” (Buzzard).

Sam problem matematyczny rozstrzygnięto już dawno. Andrew Wiles udowodnił twierdzenie w 1995 r. i żaden poważny matematyk nie podważał wyniku. Do wykonania pozostawała jednak żmudna praca: należało przepisać dowód jako zestaw instrukcji dla programu, który nie domyśla się pominiętych kroków, lecz wymaga każdej definicji i każdego ogniwa rozumowania. Według Anthropic dziesiątki agentów AI przeprowadziły tę operację w ciągu jedenastu sierpniowych dni. Pracowały równolegle na platformie Prove2Me (Anthropic).

Podany czas nie oznacza jednak, że niezależny zespół może powtórzyć cały proces. Anthropic nie udostępnił wewnętrznego modelu, infrastruktury koordynującej agentów, decyzji operatorów ani danych o wykorzystanej mocy obliczeniowej. Odtworzyć można rezultat: dysponując odpowiednim sprzętem, każdy może ponownie skompilować projekt w Lean i sprawdzić poprawność dowodu. Ten sam zapis zweryfikował też stworzony przez Anthropic odrębny mechanizm kontrolny w języku Rust, potwierdzając spójność wszystkich 1 052 234 deklaracji (raport techniczny). Była to druga kontrola gotowego tekstu, a nie niezależne powtórzenie jedenastodniowej pracy.

Jak pracowali agenci

Formalizacja polega na takim przepisaniu rozumowania matematyka, aby każdy krok mógł sprawdzić program pozbawiony matematycznej intuicji. Treść wielkiego twierdzenia Fermata wydaje się prosta: dla każdego całkowitego wykładnika równego co najmniej trzy nie istnieją trzy dodatnie liczby całkowite spełniające równanie aⁿ + bⁿ = cⁿ. Prowadzący do tego wniosku dowód przechodzi jednak przez głębokie obszary teorii liczb i zajmuje setki stron.

Claude nie odkrył nowej matematyki. Sformalizował znany ciąg wyników prowadzących do dowodu Wilesa, opierając się na wykładzie matematyków Henriego Darmona, Freda Diamonda i Richarda Taylora (Anthropic, raport techniczny). Twórczy przełom był dziełem Wilesa i jego poprzedników. Udział Claude’a polegał na przełożeniu ich rozumowania na około 10,5 mln wierszy kodu możliwego do sprawdzenia przez maszynę (raport techniczny).

Platforma Prove2Me, zaprojektowana przez badacza Anthropic Tianyiego Penga i jego współpracowników z Columbia University, podzieliła dowód na graf zależności obejmujący około 29 511 samodzielnych twierdzeń (raport techniczny). Agenci wybierali elementy, których założenia były już gotowe, zapisywali ich dowody w Lean i wzajemnie kontrolowali proponowane twierdzenia. Równoległa praca wymagała wygenerowania przez wewnętrzny model badawczy około 6 mld tokenów wyjściowych (raport techniczny).

Jak podaje Anthropic, podczas właściwej pracy operatorzy nie napisali ani jednego wiersza kodu Lean. To oni jednak wybrali twierdzenie, wskazali znaną drogę dowodową, zbudowali infrastrukturę agentową i sporadycznie zmieniali priorytety (Anthropic). Firma nie ujawniła pełnego zapisu ich działań ani kosztów obliczeniowych.

Na fundamencie wieloletniej pracy matematyków

Rezultat nie powstał od podstaw. Opiera się na Mathlib, rozwijanej społecznościowo bibliotece sformalizowanej matematyki, oraz bezpośrednio korzysta z dwóch wcześniejszych przedsięwzięć. Od końca 2023 r. zespół Buzzarda z Imperial College London pracował nad formalizacją wielkiego twierdzenia Fermata w Lean, korzystając z grantu EPSRC w wysokości 1 mln GBP, zaplanowanego do 2029 r. (grant EPSRC). Inny projekt społecznościowy wcześniej sformalizował twierdzenie dla części przypadków. W pliku źródłowym Anthropic wskazał 106 plików zawierających materiały zaczerpnięte z tych prac lub na ich podstawie zmodyfikowane (wykaz źródeł).

Równoległość pracy agentów sprawia, że jedenastu dni kalendarzowych nie sposób uczciwie zestawić z czasem poświęconym przez ludzi. Gdy Claude rozpoczął zadanie, finansowany projekt zespołu Buzzarda trwał od około 22 miesięcy (grant EPSRC). Anthropic nie podał ani liczby godzin pracy procesorów graficznych, ani zużycia energii.

Przed publikacją projektu wielkie twierdzenie Fermata pozostawało ostatnią niesformalizowaną pozycją na liście Freeka Wiedijka obejmującej 100 ważnych twierdzeń. Od dwóch dekad lista ta służy jako punkt odniesienia dla postępów w formalizacji matematyki (Buzzard).

O rzeczywistej uniwersalności tej metody przesądzi próba formalizacji nowszej i słabiej opisanej matematyki, dla której brakuje gotowego planu dowodu, dojrzałych bibliotek oraz wcześniejszych prac formalnych. Tym razem wybrano słynne twierdzenie, wokół którego istniało już rozbudowane zaplecze. Eksperyment dowodzi więc, że agenci AI potrafią stworzyć kompletną, akceptowaną przez Lean formalizację, jeśli otrzymają znaną drogę dowodową i dorobek poprzedników. Poprawność efektu mogą sprawdzić niezależni badacze; samej kampanii prowadzącej do jego powstania nie da się odtworzyć na podstawie opublikowanych materiałów.