W roku 1611 żył pewien niemiecki matematyk, astrolog i astronom o imieniu Johannes Kepler. Zasugerował on jak najwydajniej układać kule w taki sposób, aby zajmowały jak najmniej miejsca. Miało mieć to zastosowanie do pakowania przykładowo pomarańczy. Jego zdaniem idealną formacją do takiej czynności była piramida. Niestety nie był w stanie tego udowodnić, ale dzisiaj komputer potwierdził jego słowa kończąc tym samym wieki debat i rozmyślań.

Warto wspomnieć, iż Thomas Hales z Uniwersytetu w Pittsburgu, udowodnił to twierdzenie już w 1998 roku. Niestety jego dowód składał się z 300 stron, do sprawdzenia których powołano 12 osób. Po przebiciu się przez obszerną lekturę, matematycy byli tylko w 99% pewni, że metoda została potwierdzona. Hales nie poddał się i w 2003 roku rozpoczął pracę nad projektem Flyspeck – aplikacją komputerową, która sprawdzi jego dowód.

Closepacking.svg

Flyspeck wykorzystuje dwie części oprogramowania weryfikacji formalnej zwane „Isabelle” i „HOL Light”. Działają one w oparciu o serię łatwych do potwierdzenia oświadczeń logicznych. Mogą dzięki nim analizować inny zestaw oświadczeń logicznych takich jak matematyczny dowód. Wymaga to jednak czasu.

10 sierpnia 2014 roku, Hales i jego zespół ogłosili, iż przeanalizowano 300 stron przedstawiających domniemany dowód. Program potwierdził „formalnie” jego słuszność i pomysł Keplera z 1611 roku został potwierdzony.

Czuję się 10 lat młodszy… – komentuje Hales

Nie jest to tylko i wyłącznie dobra wiadomość dla Thomasa Halesa. Matematycy z całego świata będą mogli korzystać z jego programu, aby analizować własne równania.

 

źródło: Gizmodo,Wikipedia

Spodobał Ci się ten artykuł? Podaj dalej!