Przez tysiące lat matematycy próbowali rozwiązać jedną z największych zagadek matematycznych wszech czasów – Wielkie Twierdzenie Fermata. Aż do niedawna wydawało się to niemożliwe do osiągnięcia. Teraz jednak naukowcy twierdzą, że komputery mogą w końcu dostarczyć dowodu na prawdziwość tego twierdzenia.
Wielkie Twierdzenie Fermata, sformułowane w XVII wieku przez francuskiego matematyka Pierre’a de Fermata, głosi, że dla liczby naturalnej n większej od 2 nie istnieją takie liczby naturalne dodatnie x, y i z, które spełniałyby równanie xn + yn = zn. Innymi słowy, niemożliwe jest rozłożenie sześcianu na dwa sześciany, czwartej potęgi na dwie czwarte potęgi i tak dalej.
Przez stulecia matematycy bezskutecznie próbowali udowodnić to twierdzenie. Aż do 1993 roku, kiedy Andrew Wiles, brytyjski matematyk, ogłosił, że udało mu się dostarczyć pełnego dowodu. Jego 100-stronicowe notatki były jednak na tyle skomplikowane, że potwierdzenie poprawności dowodu zajęło kolejne lata.
Teraz naukowcy twierdzą, że komputery mogą pomóc w ostatecznym rozwiązaniu tej zagadki. Kevin Buzzard, matematyk i programista z Imperial College London, twierdzi, że jest w stanie wykorzystać maszynę do dostarczenia dowodów na prawdziwość Wielkiego Twierdzenia Fermata.
Buzzard pracuje nad wykorzystaniem narzędzia zwanego Lean do weryfikacji różnego rodzaju dowodów matematycznych. Jego zdaniem przekształcenie 100-stronicowego dowodu Wilesa w formalny język i reguły Lean mogłoby doprowadzić do sytuacji, w której dowody potwierdzające słuszność Wielkiego Twierdzenia Fermata zostaną dostarczone przez komputer.
Gdyby udało się przekształcić dowód Wilesa w formalny język, to kolejne pokolenia matematyków mogłyby z tego korzystać. Byłoby to ogromne wsparcie dla programistów, którzy mogliby lepiej zrozumieć dokonania matematyków. Postęp w tej dziedzinie mógłby również pomóc w upowszechnieniu matematyki wśród szerszej publiczności. Narzędzia takie jak Lean mogłyby ułatwić zrozumienie skomplikowanych dowodów matematycznych, co dotychczas było dostępne tylko dla wąskiego grona specjalistów.
Oczywiście, sama idea, że komputery mogą rozwiązać Wielkie Twierdzenie Fermata, brzmi dość rewolucyjnie. Przez stulecia ludzie nie mogli sobie z tym poradzić, a teraz maszyny miałyby dokonać tego, czego nie udało się ludziom? Czy to w ogóle możliwe?
Buzzard przyznaje, że jest to ogromne wyzwanie, ale twierdzi, że postęp technologiczny w ostatnich latach daje podstawy do optymizmu. “Komputery są coraz potężniejsze i coraz lepiej radzą sobie z rozwiązywaniem skomplikowanych problemów matematycznych” – mówi. “Jeśli uda nam się przekształcić dowód Wilesa w formalny język, to jest szansa, że komputery go zweryfikują i dostarczą ostatecznego rozwiązania”.
Jeśli naukowcom faktycznie uda się wykorzystać komputery do rozwiązania Wielkiego Twierdzenia Fermata, byłby to ogromny sukces nie tylko dla matematyki, ale także dla informatyki i sztucznej inteligencji. Byłby to dowód na to, że maszyny są w stanie radzić sobie z zadaniami, które przez stulecia pozostawały poza zasięgiem ludzkich możliwości.
Oczywiście, droga do tego celu wciąż jest długa i pełna wyzwań. Przekształcenie 100-stronicowego dowodu Wilesa w formalny język Lean to zaawansowane i czasochłonne przedsięwzięcie. Ale naukowcy są pełni optymizmu i wierzą, że komputery w końcu pomogą rozwiązać tę matematyczną zagadkę, która od wieków intryguje ludzkość.
Zgłoś naruszenie/Błąd
Pozytywnie
Neutralnie 
Negatywnie
Lubię to!
Super
Ekscytujący 
Ciekawy
Smieszny
Smutny
Wściekły
Przerażony
Szokujący
Wzruszający
Rozczarowany
Zaskoczony
Prawda
Manipulacja
Fake news
Oryginalne źródło ZOBACZ
Dodaj kanał RSS
Musisz być zalogowanym aby zaproponować nowy kanal RSS