Математики разобрались с плотной упаковкой шаров

Nq9R-bHjXDs1

Доказательство гипотезы Кеплера проверили на компьютере.

На фото: плотнейшая упаковка апельсинов. Изображение: JJ Harrison

Математик Том Хейлз с коллегами из Flyspeck завершил доказательство гипотезы Кеплера о максимально плотной шаровой упаковке. Об этом сообщается на сайте проекта.

Гипотеза Кеплера формулируется следующим образом: самая плотная упаковка шаров в евклидовом пространстве соответствует расположению центров шаров в узлах кубической гранецентрированной решетки или аналогичной ей по плотности. Под плотностью упаковки понимается отношение объема шаров, попавших в достаточно большой куб, к объему этого куба. С ростом ребра куба отношение стремится к некоторому значению, которое и называется плотностью.

Считается, что Кеплер увлекся этой проблемой, когда к нему обратились с вопросом о том, как раскладывать пушечные ядра на кораблях, чтобы они занимали меньше места. Гипотезу Кеплера доказал Карл Гаусс в 1831 году, но только для случая регулярных периодических упаковок, то есть упаковок, строение которых в пространстве повторяется.

Задача о непереодических упаковках оказалась сложнее. Максимально приблизились к решению этой проблемы с развитием компьютерных методов. Том Хейлз математически свел бесконечное число возможных упаковок к конечному перебору нескольких тысяч вариантов. Для их перебора использовался компьютер.

Манускрипт, содержащий в себе доказательство на 300 страницах, был представлен в 1998 году, но потребовалось еще 4 года на его проверку коллективом рецензентов. По итогам они сообщили, что на 99% доказательство верно. Таким образом, формально гипотеза еще не стала доказанной теоремой.

Еще около 15 лет потребовалось ученому на то, чтобы при помощи компьютерных же методов, но на этот раз логических, а не вычислительных, проверить собственное доказательство. Сейчас эта работа завершилась, и автор утверждает, что проверяющие пакеты Isabelle и HOL Light нашли доказательство верным. На этом основании он делает вывод, что гипотеза отныне может официально считаться теоремой, так как мнение рецензентов уже по существу не играет никакой роли.

Компьютерные методы доказательства — это относительно новое явление в математике, однозначного отношения к которому до сих пор нет. Тем не менее, этот подход позволил расквитаться с некоторыми старыми математическими проблемами, доказать которые один человек или даже группа ученых вручную не могли из-за чрезвычайно большого объема вычислений. К решенным проблемам можно отнести задачу о четырех красках, «алгоритм Бога» — минимальное число поворотов для сборки кубика Рубика из любого состояния (20), а теперь, по-видимому, еще и гипотезу Кеплера.