Компьютер подтвердил доказательство теоремы Кеплера

Математики опубликовали формальное доказательство гипотезы Кеплера о плотнейшей упаковке шаров в трехмерном пространстве. Несмотря на совпадение правильного ответа с очевидным, доказательство оказалось весьма сложным с математической точки зрения. Статья с результатами опубликована в издании Forum of Mathematics, Pi.

Астроном Иоганн Кеплер впервые выдвинул гипотезу в работе «О шестиугольных снежинках» в 1611 году. Помимо рассуждений о структуре снежинок, пчелиных сот и расположении горошин, в трактате также рассматривается вопрос о наиболее выгодной упаковке пушечных ядер на корабле. Кеплер приходит к выводу, что наиболее выгодна гранецентрированная кубическая упаковка, однако не приводит доказательства.

Впервые такое доказательство опубликовали Хейлс и Фергюсон в 1998 году. Оно основывалось на минимизации функции 150 переменных, анализе 5000 различных конфигураций упаковок сфер и примерно 100 000 линейных вычислительных задач. Жюри из 12 экспертов проверяло это доказательство в течение нескольких лет и в 2003 году опубликовало заключение. «Вердикт экспертов заключался в том, что доказательство, по-видимому, правильное, но у них просто не хватило времени или энергии проверить каждый аспект всесторонне, — говорит редактор журнала Герни Кон. — Доказательство было опубликовано в 2005 году, никаких непоправимых изъянов найдено не было, но сама ситуация невозможности математического сообщества окончательно убедиться казалась неудовлетворительной».

Чтобы развеять все сомнения, Хейлс в 2003 году начал проект по компьютерному доказательству, в рамках которого программа, следуя строгому алгоритму формальной логики, должна проверить все выкладки оригинального доказательства и прийти к тому же выводу. Таким образом, новая работа не только завершает доказательство многовековой проблемы дискретной геометрии, но и является новым шагом в развитии компьютерных подтверждений решений сложных математических задач.