На корабле пушечные ядра можно было пересчитать по нижнему ряду пирамиды. Но Томас Харриот, научный советник сэра Уолтера Рэли, задал вопрос сложнее: действительно ли такая укладка использует пространство лучше всех возможных?

В 1606 году Харриот написал об этой задаче Иоганну Кеплеру. Речь шла не о конечной куче ядер, которую можно переставить руками, а о бесконечной упаковке одинаковых шаров в трёхмерном пространстве. Кеплер предположил, что плотнее всего шары укладываются в знакомой конфигурации: слои смыкаются так, как апельсины или ядра на прилавке. Плотность такой упаковки равна π/√18 ≈ 0,74, то есть пустым остаётся около 26% пространства.

Ответ казался очевидным только на рисунке. Доказательство потребовало свести бесконечное множество нерегулярных конфигураций к конечному набору геометрических случаев, а затем проверить этот набор с помощью вычислений и формальных средств.

Почему регулярной решётки недостаточно

В двух измерениях задача проще: одинаковые круги складываются в гексагональную решётку, и каждый круг окружён шестью соседями. В трёх измерениях аналогичная картина уже не исключает неожиданных локальных перестроек. Даже если гранецентрированная кубическая и гексагональная плотные упаковки выглядят оптимально, остаётся логическая возможность более плотной, но нерегулярной конфигурации.

Именно это отличало результат Карла Фридриха Гаусса 1831 года от полного решения. Гаусс доказал оптимальность гранецентрированной кубической упаковки среди регулярных решёток, но не мог исключить хаотическую укладку. Как объясняет Scientific American, при таком сценарии «каждый шар мог бы оказаться где угодно», а не только на месте, заданном повторяющимся узором.

Следующий важный шаг сделал Ласло Фейеш Тот. В 1953 году он предложил заменить вопрос о всей бесконечной упаковке вопросом о локальных областях вокруг центров шаров. Для этого пространство можно разделить на ячейки Вороного: каждая точка такой ячейки ближе к одному центру шара, чем к остальным. Если удастся показать, что каждая ячейка не меньше ячейки в упаковке Кеплера, глобальная плотность тоже не превысит кеплеровскую.

Это не означает, что нужно проверить буквально все бесконечные окрестности. Идея Фейеш Тота заключалась в сведении задачи к конечному числу локальных конфигураций. Но конечное число здесь всё ещё могло быть слишком большим для ручной проверки.

Как Томас Хейлс превратил геометрию в конечную задачу

Томас Хейлс начал работать над задачей в 1992 году, продолжив линию Фейеш Тота. В статье A proof of the Kepler conjecture он рассматривает бесконечную упаковку через локальные объекты, названные «звёздами разбиения». Такая звезда описывает геометрию вокруг одного центра и зависит только от шаров на ограниченном расстоянии.

Сначала пространство разбивается на геометрические элементы, в том числе тетраэдры и специальные симплексы. Затем каждой локальной конфигурации сопоставляется функция оценки. Доказательство должно показать, что ни одна конфигурация не даёт значения выше порога, соответствующего плотности гранецентрированной кубической и гексагональной упаковок.

В статье прямо сказано, что исходная задача является «задачей оптимизации в бесконечном числе переменных», тогда как максимизация соответствующей функции на пространстве звёзд разбиения становится «задачей оптимизации в конечном числе переменных». Это центральный переход: математики не перебирают все возможные вселенные из шаров, а строят конечное описание тех локальных случаев, которые могут нарушить гипотезу.

Далее локальные конфигурации кодируются плоскими графами. В тексте статьи такие графы называются допустимыми, или tame. Их классификация оставляет конечный архив вариантов. Для каждого графа строится линейная программа. Она является ослабленной версией исходной нелинейной задачи, поэтому её максимум даёт верхнюю оценку. Если эта оценка уже ниже критического значения, конфигурация исключается.

«Поскольку линейная программа получается ослаблением ограничений нелинейной задачи, её максимум является верхней границей максимума исходной нелинейной задачи».

Для случаев, где одной линейной оценки недостаточно, Хейлс применяет метод ветвей и отсечений. Исходный набор ограничений разбивается на более узкие подзадачи. Каждая из них проверяется отдельно, пока не будет исключена или не потребует специального геометрического анализа.

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

Что именно было доказано

Опубликованная статья Хейлса утверждает: никакая упаковка конгруэнтных шаров в евклидовом трёхмерном пространстве не имеет плотности выше, чем гранецентрированная кубическая упаковка. Точная граница равна π/√18.

Работа вышла в Annals of Mathematics, том 162, выпуск 3, страницы 1065–1185. Страница журнала указывает, что рукопись получили 4 сентября 1998 года, исправленную версию приняли 16 августа 2005 года, а онлайн-публикация состоялась 1 марта 2009 года. Автором статьи указан Thomas C. Hales. Важный фрагмент доказательства был выполнен вместе с Самюэлем Фергюсоном, чья работа включена в структуру доказательства и отдельно отражена в статье.

По пересказу Scientific American, рукопись занимала около 250 страниц и сопровождалась примерно тремя гигабайтами компьютерных файлов. Редакционное рецензирование заняло ещё четыре года, а рецензенты оценили свою уверенность в корректности как 99%. Это число относится к журналистскому материалу, а не к точной вероятностной оценке математической ошибки, опубликованной на странице Annals of Mathematics.

Такая ситуация показывает предел обычного экспертного чтения. Рецензенты могли проверить логику текста и отдельные вычисления, но объём доказательства делал полную независимую проверку особенно трудной. Сам Хейлс не счёл публикацию окончательной точкой.

Что изменила формальная проверка Flyspeck

В 2003 году Хейлс начал проект Flyspeck. Его цель состояла не в том, чтобы заново найти доказательство автоматически, а в том, чтобы перевести его утверждения и промежуточные шаги в форму, которую можно проверить в системе-помощнике доказательств HOL Light.

Репозиторий проекта формулирует это прямо: Flyspeck должен был создать «формальное доказательство гипотезы Кеплера» в HOL Light. Проект завершили 10 августа 2014 года. В его материалах есть формализация текстовой части доказательства, проверка линейных программ, интервальной арифметики и классификации графов. Страница дополнительных материалов к статье также содержит код генерации графов, исходные данные линейного программирования и спецификацию неравенств интервальной арифметики.

Здесь важно различать два вида компьютерной работы. В первом случае программа выполняет расчёты, например решает линейную программу или проверяет численную границу. Во втором случае помощник доказательств проверяет, что формализованная последовательность логических шагов действительно следует из заданных аксиом и правил вывода.

Формальная проверка изменила не математический результат, а способ его аудита. До Flyspeck уверенность зависела от чтения очень объёмного текста, проверки компьютерных расчётов и доверия к корректности программ. После формализации существенная часть утверждений стала объектом машинной проверки внутри HOL Light.

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

Именно поэтому формальное доказательство полезно рассматривать не как «машину, которая думает вместо математика», а как дополнительный слой контроля. Обычный текст объясняет идею человеку. Формальная система проверяет множество точных переходов по правилам, которые нельзя пропустить из-за усталости или масштаба материала. Подробнее о границах такого подхода можно прочитать в статье почему формальная проверка математических доказательств не гарантирует абсолютной защиты.

Почему эта история важна для математики

Задача об укладке сфер оказалась сложной не потому, что в ней трудно нарисовать плотную упаковку. Трудность состояла в слове «любая». Нужно было исключить не только очевидные решётки, но и каждую возможную нерегулярную конфигурацию, включая те, которые нельзя описать одним повторяющимся узором.

Доказательство Хейлса решило эту проблему через цепочку редукций: бесконечная упаковка, локальная геометрия, конечное пространство конфигураций, классификация графов, линейные оценки и ветвление. Flyspeck добавил к этой цепочке формальную проверку.

Оставшийся урок практичен. В сложном вычислительном доказательстве важно отдельно спрашивать, где находится математическая идея, где выполняется численный расчёт и где проверяется логический переход. Эти уровни связаны, но не заменяют друг друга. История гипотезы Кеплера показывает, как компьютер может сделать доказательство проверяемее, не превращаясь в его автора.

Источники

  1. Thomas C. Hales. A proof of the Kepler conjecture. Annals of Mathematics, 2005. DOI: 10.4007/annals.2005.162.1065.
  2. PDF статьи Thomas C. Hales.
  3. Computer resources for the Kepler conjecture.
  4. Репозиторий проекта Flyspeck.
  5. Manon Bischoff, Daisy Yuhas. How a 16th century pirate accidentally spawned a centuries-old math problem. Scientific American, 27 октября 2026 года. Журналистский материал, использованный для исторического контекста и описания масштаба проекта.
Схема показывает последовательное сведение задачи о плотности любой упаковки шаров к конечным локальным конфигурациям, вычислительным оценкам и машинно проверяемому доказательству.

Фото: A G / Pexels