Hipoteza Keplera: problem ostatecznie rozwiązany po 400 latach

W 1611 r. Niemiecki fizyk, matematyk i astronom Johannes Kepler zaproponował, że najlepszym sposobem na układanie obiektów sferycznych - takich jak na przykład owoce - byłoby ułożenie ich w kształcie piramidy. Nie mógł jednak udowodnić, że ma rację, i ten zagadkowy problem ostatecznie stał się znany jako „hipoteza Keplera”.

Według New Scientist w 1998 r. Amerykański matematyk Thomas Hales ogłosił, że był w stanie udowodnić, że propozycja Keplera była poprawna. W tym czasie Hales polegał na matematycznej metodzie obliczania wszystkich możliwych możliwości twierdzenia, aby dojść do rozwiązania.

Konta i więcej kont

Opierając się na tej metodzie, Hales uznał, że chociaż istnieją nieskończone sposoby ustawiania obiektów sferycznych w nieskończoność, większość z nich jest w rzeczywistości jedynie wariantami kilku tysięcy możliwości. W ten sposób matematyk podzielił problem na tysiące sposobów organizacji obiektów sferycznych, które matematycznie reprezentują nieskończone możliwości aranżacji, i wrzucił wszystkie te informacje do oprogramowania, aby wykonać obliczenia.

W rezultacie powstał mały 300-stronicowy stos, którego sprawdzenie zajęło cztery lata przez 12 recenzentów! I nawet po tylu pracach matematycy nie byli do końca pewni, czy obliczenia są prawidłowe, twierdząc, że mieli tylko 99 procent pewności, że rozwiązanie Halesa naprawdę popiera propozycję Keplera.

Wreszcie 100% pewności

Wiesz, że „99% pewności” nie wystarcza do matematyki, prawda? W 2003 r. Hales rozpoczął projekt mający na celu udowodnienie swoich obliczeń, wykorzystując dwa formalne oprogramowanie weryfikacyjne - o nazwie Isabelle i HOL Light - do kontroli swojej pracy.

I to nie tak, że w końcu doszli do wniosku! W ostatnią niedzielę, 10 sierpnia, zespół Halesa ogłosił, że po przetłumaczeniu gęstej matematyki zawartej na 300 stronach obliczeń z 1998 r. Na język skomputeryzowany byli w stanie ustalić, że obliczenia były prawidłowe. Innymi słowy, po tylu wiekach - i latach wysiłków Halesa i jego zespołu - propozycja Keplera została udowodniona.

A fakt, że duch Keplera może wreszcie spoczywać w pokoju - a Hales może zwrócić uwagę na inny skomplikowany problem - nie jest jedyną dobrą wiadomością w tej całej historii. Tej technologii można użyć do zweryfikowania ogromnej ilości pracy, która pojawia się każdego roku, uwalniając matematyków od tego niewdzięcznego zadania i pozwalając im wykorzystać ten czas na skupienie się na innych zagadnieniach i uwolnić swoją kreatywność do eksploracji wszechświata liczb.