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