Гіпотезу Кеплера підтвердили остаточно
Як найщільніше упакувати кулі, в 1611 році описав німецький астроном і математик Йоганн Кеплер. Однак остаточне доказ того, що його припущення годиться для всіх можливих множин куль і просторових масштабів, математики надали тільки в 1998 році.
Однак цей аргумент був настільки складний, що експерти зіткнулися з браком часу і енергії на його верифікацію. Тільки тепер комп’ютерна програма остаточно підтвердила описане 20 років тому доказ і теорію Кеплера в цілому.
Гіпотеза Кеплера – це класичний приклад геометрії: йдеться про питання, як найбільш щільно розмістити кулі в обмеженому просторі, наприклад апельсини в ящику. Інтуїтивно – рішення просте і його легко перевірити: менше простору займають кулі, складені у формі піраміди – тобто кубично-гранецентрованые або гексагональні, коли кожен шар розташований у проміжках нижніх шарів. Це рішення виявив ще в 1611 році Йоганн Кеплер. Згідно з його гіпотезою, в результаті такого штабелювання можна досягти щільності близько 74%.
Однак проблему становило математичне обґрунтування – воно повинно було математично і вивести довести гіпотезу Кеплера для всіх можливих просторових масштабів і послідовностей куль. І власне в цьому вчені терпіли невдачу століттями.
У 1998 році Томас Гейлс (Thomas Hales) з Піттсбурзького університету представив доказ, який так довго шукали. За допомогою комп’ютерної програми він обчислив 5 тисяч різних способів розташування куль і для кожного перевірив придатність гіпотези Кеплера. Проблема полягала в тому, що розрахунки були довжиною тисячі кодових цифр і заповнювали 250 друкованих сторінок.
«Висновок експертів тоді був такий: доказ здається функціональним, але у нас немає часу і енергії, щоб все перевірити», – повідомив Генрі Кон (Cohn Henry), видавець журналу «Forum of Mathemathics Pi». Доказ Гейлса опублікували в 2005 році, однак остаточної впевненості щодо його сили не було. «Ця ситуація не задовольняла», – сказав Кон.
У пошуках вирішення проблеми у Гейлса і його колег з’явилася ідея використовувати комп’ютер для перевірки формул. І дві спеціальні програми для аналізу – HOL Light і Isabelle, – якими користуються, зокрема, для пошуку помилок в програмному забезпеченні, перевірили логічну частину Гейлсового докази.
«Проект Flyspeck дав можливість встановити рекорд щодо перевірених цифр-кодів при верифікації», – сказав Гейлс. Вчені пояснили: перевірка основної частини Гейлсового докази триває приблино один день. Однак для однієї з трьох подчастей програма вимагала 5000 годин на центральному процесорі. Цю процедуру вчені повторювали кілька разів. Тепер вони завершені, і Гейлс з колегами опублікували результати.
Згідно з їх висновками, Гейлсовое формальне доведення гіпотези Кеплера є дійсним. Після понад 400 років можна стверджувати, що проблема розташування куль знайшла своє формальне математичне обґрунтування, тобто отримала статус цілком розв’язаної, пояснили математики.