Dotyczy to tytułowego wielkiego twierdzenia Fermata. Jego autorem był Pierre de Fermat, który ogłosił, że dla liczby naturalnej (n) większej od 2 nie istnieją takie liczby naturalne dodatnie (x, y, z), które spełniałyby równanie xn + yn = zn Opisał ten fenomen słowami: jest niemożliwe rozłożyć sześcian na dwa sześciany, czwartą potęgę na dwie czwarte potęgi i ogólnie potęgę wyższą niż druga na dwie takie potęgi.
Czytaj też: Sztuczna inteligencja osiąga nieziemską szybkość – generuje 20 grafik na sekundę
Twierdzenie pojawiło się w XVII wieku i było przedmiotem rozważań wśród matematyków. O ile ludzie byli w stanie je udowodnić, tak komputery nie poradziły sobie z tym zadaniem. Aż do teraz. Tak przynajmniej twierdzi Kevin Buzzard, który rzekomo jest w stanie wykorzystać maszynę do dostarczenia dowodów na prawdziwość wielkiego twierdzenia Fermata. Matematyk i programista ma już konkretny plan działania.
Komputery do tej pory miały problem z wielkim twierdzeniem Fermata. Kevin Buzzard przekonuje, że wkrótce się to zmieni
Przełomowy w tym zakresie okazał się rok 1993, kiedy to Andrew Wiles wykazał matematycznie, że twierdzenie Fermata ma rację bytu. O złożoności tego wyzwania najlepiej świadczy fakt, iż notatki poświęcone dowodowi liczyły aż 100 stron. Buzzard, powiązany z Imperial College w Londynie, wykorzystuje narzędzie znane jako Lean do weryfikowania różnego rodzaju dowodów.
Czytaj też: Za układaniem puzzli kryje się matematyka. Naukowcy rozwiązali odwieczny problem
Jak przekonuje naukowiec, przekształcenie 100-stronicowego dowodu Wilesa w formalny język i reguły mogłoby doprowadzić do sytuacji, w której dowody potwierdzające słuszność wielkiego twierdzenia Fermata zostaną dostarczone przez komputer, co mogłoby pomóc kolejnym pokoleniom matematyków. Powinno to stanowić także wsparcie dla programistów. Postępy w tym zakresie mogłyby doprowadzić do sytuacji, w której narzędzia pokroju Lean pozwalałyby otoczeniu na łatwiejsze zrozumienie dokonań matematyków. Ale czy faktycznie tak się stanie? Kluczową próbą może okazać się starcie komputerów z wielkim twierdzeniem Fermata.
