Опубликовано окончательное доказательство гипотезы об упаковке шаров

В журнале Forum of Mathematics, Pi прошла научное рецензирование и опубликована статья с формальным доказательством теоремы Кеплера. Формулировка теоремы: среди всех упаковок шаров равного размера в трёхмерном пространстве наибольшую среднюю плотность имеет гранецентрированная кубическая упаковка и упаковки, равные ей по плотности. Это завершает почти 20-летний пласт работ, посвященных проверке доказательства Томаса Хейлза. Об этом сообщает блог Cambridge Core.

Гипотеза Кеплера была сформулирована в начале XVII века, более 400 лет назад. Она, отчасти, была связана с реальной практической задачей о лучшем способе упаковки пушечных ядер. Средней плотностью упаковки называется доля заполненного шарами объема в достаточно большом (по сравнению с размером шара) кубе пространства. Несмотря на кажущуюся простоту, гипотезу не удавалось доказать до конца XX века.

Первое доказательство гипотезы Кеплера было представлено Томасом Хейлзом в 1998 году. Оно включало в себя компьютерный перебор огромного количества вариантов касания шаров между собой. Однако в доказательстве была некоторая проблема, связанная с тем, что компьютеры оперируют целыми числами — требовалось доказать, что приближенные таким образом вычисления корректно использовать. Проверка работы Хейлза затянулась до 2005 года. Рецензенты отметили, что, скорее всего, доказательство верно, но перепроверить все частные случаи вручную было невозможно. Тем не менее, первая версия доказательства была опубликована.

Хейлз объединился с большой международной группой математиков для того, чтобы сделать доказательство полным и формальным. Для этого математикам снова пришлось использовать компьютерные методы. Работа продолжалась еще около десяти лет, пока в 2014 году математики не объявили о ее завершении. В 2015 году Хейлз опубликовал препринт финальной статьи — версию, не проверенную рецензентами.

Спустя два с половиной года, 29 мая статья окончательно прошла рецензирование и была опубликована в научном журнале. Код, «доказывающий» теорему Кеплера, опубликован в открытом доступе на сервисе GitHub. Как отмечает блог Cambridge Core, это самое крупное и сложное доказательство из всех, которые когда-либо были подтверждены с помощью компьютера.

Теорема Кеплера была сформулирована для трехмерного пространства, но известны результаты и для пространств высших размерностей. Так, задача об упаковке шаров в 8- и 24-мерных пространствах была решена Мариной Вязовской (за это ей была присуждена премия института Клэя). Стоит отметить, что эта задача имеет реальное практическое применение — для передачи информации. Плотнейшие упаковки определяют то, как следует кодировать информацию, чтобы небольшие случайные шумы при ее передаче не приводили к ошибкам при декодировании.

Ранее мы сообщали о компьютерном доказательстве, полный объем которого занял 200 терабайт. Таким образом была решена задача о булевых пифагоровых тройках.