fbpx

Каталог статей

Каталог статей для размещения статей информационного характера

Технології

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

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

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *