Zdjęcie: © Bozhin Karaivanov / Unsplash
Źródło: unsplash.com/photos/5z70PsbFCMM
Firma Anthropic poinformowała o stworzeniu formalnej wersji dowodu wielkiego twierdzenia Fermata. Według ogłoszenia projekt zajmował się zespół agentów AI pracujących z modelem Claude i został ukończony w ciągu 11 dni. Nie chodzi o znalezienie nowego dowodu, lecz o przepisanie znanego dowodu do postaci, którą komputer może sprawdzić krok po kroku.
Wielkie twierdzenie Fermata mówi, że dla całkowitego n większego od 2 nie istnieją dodatnie liczby całkowite a, b i c spełniające równanie aⁿ + bⁿ = cⁿ. Samo twierdzenie jest łatwe do zapisania, ale znalezienie pełnego dowodu okazało się wyjątkowo trudne. Pierre de Fermat sformułował problem w XVII wieku i zasugerował, że zna rozwiązanie, lecz rzekomy dowód miał być zbyt długi, by zmieścić się na marginesie księgi. Przez kolejne stulecia matematycy próbowali bez powodzenia rozwiązać zagadkę. Andrew Wiles pracował nad nią przez siedem lat w tajemnicy. Przełom ogłosił w 1993 roku, a po wykryciu błędu w dowodzie wspólnie z Richardem Taylorem potrzebował około roku na jego usunięcie. Dowód został uznany za zakończony w 1995 roku.
Słownik artykułu
Krótkie objaśnienia terminów występujących w tekście. Każde hasło prowadzi do szerszej definicji i przykładów użycia.
Język programowania i system używany do zapisywania oraz formalnego sprawdzania dowodów matematycznych.
Wspólne repozytorium sformalizowanej matematyki wykorzystywane przez użytkowników języka Lean.
Przepisanie twierdzenia i jego dowodu do postaci kodu, który może być sprawdzany przez komputer krok po kroku.
Automatyczne przekształcanie treści matematycznych, w tym dowodów, do postaci możliwej do sprawdzenia przez komputer.
Dowody matematyczne często składają się z wielu zależnych od siebie argumentów. Błąd w jednym kroku może podważyć całą konstrukcję, co pokazała historia dowodu Wilesa. Formalizacja matematyczna przenosi taki dowód z papieru do kodu. System sprawdzający może wtedy metodycznie kontrolować, czy każdy kolejny wniosek wynika z wcześniejszych założeń i reguł. Nie zastępuje to matematycznego znaczenia twierdzenia, ale ogranicza ryzyko przeoczenia błędu w długim łańcuchu rozumowania. W repozytorium Mathlib znajduje się już około 2 milionów linii sformalizowanej matematyki.
Anthropic podało, że model Claude działał przez 11 dni bez przerwy, a nad projektem pracowało wiele odrębnych agentów AI. Każdy z nich otrzymywał inne zadania związane z fragmentami dowodu. Ludzie przekazywali im tylko ogólne instrukcje, które miały utrzymać pracę we właściwym kierunku. Nie wszystko przebiegało sprawnie. Kilka razy agenci tracili orientację w stanie projektu i przestawali skutecznie współpracować. Przełom nastąpił po wykorzystaniu narzędzia Prove2Me, stworzonego pierwotnie z myślą o współpracy matematyków. Pomagało ono agentom śledzić wykonane zadania i ustalać, czym należy zająć się dalej.
Rezultat Anthropic wyprzedził pięcioletni projekt Kevina Buzzarda z Imperial College London. Jego celem było formalizowanie około 100 stron dowodu Wilesa i Taylora w języku Lean, tak aby można było sprawdzić jego poprawność i wykorzystywać go jako podstawę dalszych badań. Buzzard oceniał wcześniej, że postępy AI mogą znacząco skrócić czas potrzebny na realizację tego zadania. Po ogłoszeniu Anthropic stwierdził, że formalizacja nie opiera się na dodatkowych założeniach poza aksjomatami matematyki. W projekcie pojawiły się między innymi elementy algebry, analizy harmonicznej, geometrii i teorii liczb.
Bezpośrednim wynikiem jest więc sformalizowany i komputerowo sprawdzalny zapis istniejącego dowodu, a nie nowe rozwiązanie wielkiego twierdzenia Fermata. Szerszy wniosek, że AI będzie mogła automatycznie formalizować dużą część współczesnej literatury matematycznej, pozostaje perspektywą badawczą. Sam projekt pokazuje jednak, że automatyczna formalizacja może już obejmować bardzo długie, wielowarstwowe dowody, a przygotowany kod może stać się materiałem do dalszej pracy matematyków.
Brak komentarzy. Bądź pierwszy!
