Keplerova domnienka: problém sa konečne vyriešil po 400 rokoch

V roku 1611 navrhol nemecký fyzik, matematik a astronóm Johannes Kepler, že najlepším spôsobom, ako stohovať sférické objekty - napríklad ovocie - by bolo usporiadať ich do podoby pyramídy. Nedokázal však dokázať, že mal pravdu, a tento záhadný problém sa nakoniec stal známy ako „Keplerova domnienka“.

Podľa New Scientist v roku 1998 americký matematik Thomas Hales oznámil, že dokázal, že Keplerov návrh bol správny. V tom čase sa Hales spoliehal na matematickú metódu výpočtu všetkých možných možností vety, aby sa dospelo k riešeniu.

Účty a ďalšie účty

Na základe tejto metódy Hales usúdil, že hoci existuje nekonečné množstvo spôsobov, ako nekonečne ukladať sférické objekty, väčšina z nich je v skutočnosti iba variáciami niekoľkých tisíc možností. Matematik teda rozdelil problém na tisíce spôsobov usporiadania sférických objektov, ktoré matematicky predstavovali nekonečné možnosti usporiadania, a všetky tieto informácie hodil do softvéru na vykonávanie výpočtov.

Výsledkom bol malý stoh strán 300 strán, ktorého kompletná kontrola 12 recenzentmi trvala štyri roky! A aj po toľkých prácach si matematici neboli úplne istí, či sú výpočty správne, pričom tvrdili, že si boli len 99% istí, že Halesovo riešenie skutočne podporilo Keplerov návrh.

Nakoniec, 100% istý

No, viete, že „99% istí“ nestačí na matematiku, však? V roku 2003 začal Hales projekt na overenie svojich výpočtov. Na kontrolu svojej práce použil dva formálne verifikačné programy - Isabelle a HOL Light.

A nie je to tak, že konečne dospeli k záveru! Minulú nedeľu 10. augusta Halesov tím oznámil, že po prepočte hustej matematiky prítomnej na výpočtoch na 300 stranách 1998 do počítačového jazyka sa im podarilo zistiť, či sú výpočty správne. Inými slovami, po toľkých storočiach a rokoch úsilia Halesa a jeho tímu sa Keplerov návrh osvedčil.

A skutočnosť, že Keplerov duch môže konečne zostať v pokoji - a Hales môže obrátiť svoju pozornosť na ďalší komplikovaný problém - nie je jedinou dobrou správou v tomto celom príbehu. Táto technológia sa môže použiť na kontrolu obrovského množstva práce, ktorá sa každý rok vynára, čo matematikom oslobodzuje od tejto nevyslovenej úlohy a umožňuje im využiť tento čas na zameranie sa na iné problémy a uvoľnenie tvorivosti na preskúmanie vesmíru čísel.