Zacznijmy od tego, że wielkie twierdzenie Fermata jest jednym z najbardziej znanych problemów w historii matematyki. Pierre de Fermat zapisał je około 1637 roku na marginesie egzemplarza dzieła Arithmetica. Twierdzenie mówi, iż dla liczb całkowitych dodatnich nie istnieją takie wartości a, b i c oraz wykładnik n większy od 2, dla których zachodzi równanie aⁿ + bⁿ = cⁿ.
Czytaj też: Matematycy pracowali nad tymi kośćmi 15 lat. Mają 60 ścian i niezwykłą właściwość
Przez ponad trzy stulecia matematycy nie potrafili znaleźć pełnego dowodu. Problem udało się rozwiązać dopiero w latach 90. XX wieku. Dokonał tego Andrew Wiles, który przedstawił światu dowód w 1994 roku. Jego ostateczna wersja doczekała się publikacji rok później i liczyła 129 stron. Sprawdzenie poprawności całego rozumowania wymagało miesięcy pracy matematyków.
To właśnie ten istniejący już dowód stał się punktem wyjścia dla sztucznej inteligencji. Nie chodzi więc o to, że Claude po raz pierwszy udowodnił twierdzenie Fermata. Matematycy znali jego dowód od ponad 30 lat. Nowością jest przekształcenie skomplikowanego rozumowania do postaci formalnej, którą może bezpośrednio zweryfikować komputer. To część tzw. formalizacji matematyki: zamiast pozostawiać część argumentacji doświadczeniu i intuicji matematyka, każdy krok musi zostać zapisany w sposób jednoznaczny dla systemu komputerowego. W tym przypadku wykorzystano Lean, czyli specjalistyczny język i system służący do formalnego zapisywania oraz sprawdzania dowodów matematycznych.
Claude podczas pracy wygenerował około 13 milionów linii kodu i udowodnił 29 500 twierdzeń pośrednich. Według Anthropic model działał w dużej mierze autonomicznie przez 11 dni. Ostateczny rezultat został sprawdzony przez Lean, dzięki czemu formalny dowód nie zawiera niezweryfikowanych luk.
Skala tego osiągnięcia pokazuje jednocześnie największą zaletę i jeden z problemów związanych z wykorzystaniem AI w matematyce. Z jednej strony komputer może przeprowadzić ogromną liczbę żmudnych operacji i sprawdzić poprawność argumentacji znacznie szybciej niż człowiek. Z drugiej strony rezultat stworzony przez Claude’a jest gigantyczny w porównaniu z klasycznym dowodem Wilesa.
To prowadzi do interesującego pytania: czy matematyczny dowód musi być zrozumiały dla człowieka, aby miał pełną wartość? Formalny zapis może być całkowicie poprawny, a jednocześnie niezwykle trudny do przeanalizowania przez matematyka. W przypadku dowodu Fermata problem ten jest szczególnie widoczny, ponieważ 13 milionów linii kodu stanowi ogromny materiał do ręcznego prześledzenia. Naukowcy widzą jednak w takim podejściu ogromny potencjał. Jeśli sztuczna inteligencja będzie w stanie automatycznie formalizować kolejne skomplikowane dowody, matematycy mogą poświęcać więcej czasu na poszukiwanie nowych idei, a mniej na żmudne sprawdzanie każdego technicznego szczegółu.
Źródło: Anthropic
