Кеплерову гіпотезу підтвердили остаточно

 

Як найщільніше спакувати кулі, 1611 року описав німецький астроном і математик Йоган Кеплер. Проте остаточний формальний доказ того, що його припущення годиться для всіх можливих множин куль і просторових масштабів, математики надали лише 1998 року. Проте цей доказ був настільки складний, що експерти зіткнулися з браком часу й енергії на його верифікацію. Лише тепер комп’ютерна програма остаточно підтвердила описаний 20 років тому доказ і Кеплерову теорію загалом.


Два розвязки Кеплерової гіпотези: кубічно-гранецентроване або гексагональне пакування. Зображення: Cdang/CC-by-sa 3.0.

 

Кеплерова гіпотеза – це класичний приклад геометрії: йдеться про питання, як найщільніше розмістити кулі в обмеженому просторі, наприклад апельсини в ящику. Інтуїтивно – розв’язок простий і його легко перевірити: найменше простору займають кулі, складені у формі піраміди – тобто кубічно-гранецентровано або гексагонально, коли кожна куля розташована в проміжках нижніх шарів. Це розв’язання виявив ще 1611 року Йоган Кеплер. Згідно з його гіпотезою, в результаті такого штабелювання можна досягнути щільності близько 74%.

 

Проте проблему становило математичне обґрунтування – воно мусило математично вивести і довести Кеплерову гіпотезу для всіх можливих просторових масштабів і послідовностей куль. Та власне в цьому науковці зазнавали невдачі століттями.

 

1998 року Томас Гейлс (Thomas Hales) з Піттсбурзького університету представив доказ, який так довго шукали. За допомогою комп’ютерної програми він вирахував 5 тисяч різних способів розташування куль і для кожного перевірив придатність Кеплерової гіпотези. Проблема полягала в тому, що обрахунки були завдовжки тисячі кодових цифр і заповнювали 250 друкованих сторінок.

 

«Висновок експертів тоді був такий: доказ здається функціональним, але в нас немає часу й енергії, аби все перевірити», – повідомив Генрі Кон (Henry Cohn), видавець журналу «Forum of Mathemathics Pi». Доказ Гейлса опублікували 2005 року, проте остаточної певності щодо його сили не було. «Ця ситуація не задовольняла», – сказав Кон.

 

У пошуках розв’язання проблеми в Гейлса та його колег з’явилася ідея використати комп’ютер для перевірки формул. І дві спеціальні програми для аналізу – HOL Light і Isabelle, – якими послуговуються зокрема для пошуку помилок у програмному забезпеченні, перевірили логічну частину Гейлсового доказу.

 

«Проект Flyspeck дав змогу встановити рекорд щодо перевірених цифр-кодів при верифікації», – сказав Гейлс. Науковці пояснили: перевірка основної частини Гейлсового доведення тривала приблино один день. Проте для одної з трьох підчастин програма потребувала 5000 годин на центральному процесорі. Цю процедуру вчені повторювали кілька разів. Тепер вони завершені, і Гейлс з колегами опублікували результати.

 

Згідно з їхніми висновками, Гейлсове формальне доведення гіпотези Кеплера є дійсним. Після понад 400 років можна стверджувати, що проблема розташування куль знайшла своє формальне математичне обґрунтування, тобто здобула статус цілком розв’язаної, пояснили математики.

 

 

Keplers Vermutung endgültig bewiesen

Cambridge University Press, 19/06/2017

Зреферувала Соломія Кривенко

26.06.2017