Claude zamknął Fermata w 11 dni: 13,4 miliona linii Lean i ani jednego „oczywiście”

4 września firma Anthropic pokazała pierwszy w historii kompletny test maszynowy ostatniego twierdzenia Fermata. Claude w 11 dni, prawie bez pomocy ludzi, przetłumaczył dowód Andrew Wilesa na język Lean: 13,4 miliona linii kodu, około 30 tysięcy twierdzeń pośrednich, zero „oczywiste z tego, co zostało powiedziane”. Projekt, który matematycy planowali od lat – jedynie rysunek pierwszej fazy autorstwa Kevina Buzzarda z Imperial College w Londynie liczył 86 stron – ukończono w półtora tygodnia.

Natychmiast wyjaśnijmy, czego tu nie ma: nie ma nowych dowodów. Model nie wymyślił własnej ścieżki do twierdzenia. Zrobiła coś innego i, szczerze mówiąc, nie mniej skomplikowanego - wzięła ludzki dowód, w którym na każdej stronie znajdują się zastrzeżenia typu „to trywialnie” i przepisała go tak, aby kompilator sprawdzał każdy krok. Matematycy po 1995 roku mieli 99,9% pewności co do twierdzenia. Teraz można już na sto procent: Lean przeszło całe wyprowadzenie z trzech standardowych aksjomatów i nie ma już co wątpić.

Co dokładnie sprawdzał komputer?

Liczby są tu bardziej odpowiednie niż epitety.

• 13,4 miliona linii Lean to ponad pięć razy więcej niż cała Mathlib, główna formalna biblioteka matematyczna systemu.
• Udowodniono około 30 tysięcy twierdzeń pośrednich; ostateczna produkcja obejmowała około 29 500 sztuk.
• Kompilacja repozytorium na maszynie 96-rdzeniowej zajmuje około 20 razy dłużej niż kompilacja Mathliba. Na czas testu Buzzard otrzymał serwer z 500 GB RAM-u.
• Opieramy się tylko na trzech standardowych aksjomatach Lean. Żadnych „założeń dla prostoty”.

Kevin Buzzard, ten sam matematyk, który od 2024 roku prowadzi dla społeczności projekt formalizacji Fermata, pobrał repozytorium, zmontował je i uruchomił komparator: wyjściowe sformułowanie twierdzenia pokrywa się z referencyjnym z Mathliba, wszystkie kontrole są zielone. Jego recenzja: „niezwykłe osiągnięcie autoformalizacji”.

Jedna linijka na marginesie, trzy i pół wieku pracy

Około 1637 roku Pierre de Fermat umieścił to stwierdzenie na marginesie Arytmetyki Diofantusa: dla n większych niż dwa równanie aⁿ + bⁿ = cⁿ nie ma rozwiązań w liczbach naturalnych. Poniżej zdanie, które przeszło do legendy: „Znalazłem naprawdę wspaniały dowód, ale marginesy są dla niego za wąskie”. Pokolenia matematyków, od Eulera po Kummera, dążyły do ​​uzyskania wyniku w kawałkach. W 1908 roku za dowód przyznano nagrodę w wysokości 100 tysięcy złotych marek, a w pierwszym roku otrzymano 621 błędnych rozwiązań.

W czerwcu 1993 roku Andrew Wiles przedstawił swój dowód podczas serii wykładów w Cambridge. Dwa miesiące później recenzent zadał pytanie, które ujawniło lukę w jednym z projektów. Wiles przez rok wszystko łatał – najpierw sam, potem wspólnie z byłym studentem Richardem Taylorem – był już bliski porzucenia tego wszystkiego i w 1995 roku opublikował 129-stronicowy tekst. Pozostało ostatnie, „inżynierskie” pytanie: czy można zmusić komputer do potwierdzenia tego wszystkiego w całości?

Nie nowy dowód, ale nowa szansa

Opiera się na analizie Darmona, Diamonda i Taylora z 1995 r. dotyczącej argumentu Wilesa – Taylora na podstawie twierdzenia Langlandsa – Tunnella i zejścia na poziomie Ribeta. Pomysł sformalizowania Wilesa został zgłoszony już w 2000 roku przez holenderskiego informatyka Jana Bergstrę, ale do niedawna uważano to za dzieło dla całego kierunku naukowego. Przypadki indywidualne – czwartego stopnia, zwykłe proste – przesunięto wcześniej do Lean. Nowe repozytorium zamyka całą listę 100 zadań formalizacyjnych Weidika: punkt odniesienia, z którym porównywano ten obszar, ma dwadzieścia lat.

Buzzard zresztą szczerze pisze: matematycznie dzieło nie wnosi niczego nowego – już wierzył w Wilesa. Wartość leży gdzie indziej. Przeglądanie nowego artykułu z matematyki zajmuje miesiące, a nawet lata; Jeśli można poprosić maszynę o sformalizowanie dowodu w locie, recenzowanie skróci się i zaczną wychodzić na jaw ukryte założenia na poziomie eksperckim. Dla nauki, gdzie wszystko opiera się na uczciwości wniosków, jest to poważna zmiana.

Jak te 11 dni wyglądało od środka

Pracami kierował Tianyi Peng, badacz antropiczny, który wcześniej stworzył grupę narzędzi do formalizacji sztucznej inteligencji na Uniwersytecie Columbia. Według niego początkowo nie planował dotarcia do końca: chciał jedynie zobaczyć, jak bardzo Claude posunie naprzód projekt Buzzarda. Awans do finału.

Wielu agentów pracowało równolegle: niektórzy ukończyli definicje matematyczne, inni szturmem lematów pośrednich, inni przesuwali się w górę drzewa twierdzeń, a jeszcze inni składali części z powrotem w jeden wniosek. Pierwsze dni nie poszły dobrze – agenci stracili ogólny obraz projektu, a około siedem procent wczesnych prób pozostało w ostatecznym kodzie. Zwrot nastąpił, gdy zespół został przeniesiony na platformę Prove2Me: dowodem w nim jest wykres węzłów twierdzeń, na którym widać, co zostało już udowodnione, co oczekuje na warunki wstępne i co należy dalej zrobić. Twierdzenia oddzielono od dowodów, kompilacja została przyspieszona, a każde twierdzenie posiada opis tekstowy z możliwością przeszukiwania. Skala prac wynosi około sześciu miliardów tokenów wyjściowych, a podpowiedzi ludzkie zostały zredukowane do wysokiego poziomu: „ten kierunek jest priorytetem”.

Gdzie oglądać

Repozytorium umieszczone jest na GitHubie - jeśli chcesz, możesz sam przeprowadzić test, jeśli masz maszynę z 96 rdzeniami i mocnymi nerwami. Źródła pierwotne: analiza z Anthropic I Post Buzzarda na blogu Xena Project.

A jeśli po historii liczącej 13 milionów linii chcesz zobaczyć, jak współczesne modele radzą sobie z mniejszymi zadaniami – algorytmami, kodem, obliczeniami – zajrzyj do sekcji "Kod" I "Pogawędzić" w dniu NeuralSpace: tam możesz eksperymentować z modelami i łączyć je ze swoimi projektami poprzez API.