Группа математиков под руководством профессора Питтсбургского университета Томаса Хейлса (Thomas Hales) представила положительные результаты проверки сделанного ранее доказательства математической гипотезы об упаковке шаров. Статья об этом опубликована в журнале Forum of Mathematics, Pi.
Гипотезу о наиболее плотном размещении шаров в пространстве высказал в 1611 году Иоганн Кеплер. Появление подобных задач в математике было вызвано практическими задачами по оптимальному размещению пушечных ядер. Согласно Кеплеру, среди всех упаковок шаров равного размера в трехмерном пространстве наибольшую среднюю плотность будет иметь гранецентрированная кубическая упаковка и упаковки, равные ей по плотности.
Профессор Хейлз и его ученик Сэм Фергюсон объявили о доказательстве гипотезы Кеплера в 1998 году, но решение было настолько длинным и сложным, что проверяющая его группа из двенадцати математиков работала пять лет и в итоге пришла к выводу, что доказательство «скорее всего, верно». «У них просто не было времени или сил, чтобы полностью проверить всё, – говорит редактор журнала Forum of Mathematics, Pi Генри Кон (Henry Cohn). – Никаких непоправимых изъянов не было выявлено, но не удовлетворяла ситуация, когда доказательство, казалось бы, было недоступным для тщательной проверки математическим сообществом».
Тогда профессор Хейлз решил обратиться к компьютерам и использованию формальных методов проверки. Он и группа его соавторов изложили доказательство необычайно подробно, используя строгую формальную логику, а затем компьютерная программа проверила их рассуждения. В 2015 году Хейлз опубликовал препринт с результатами проверки, подтвердившими его правоту, а теперь вышла официальная публикация в рецензируемом журнале. Доказательство гипотезы Кеплера стало самым сложным математическим доказательством, подтвержденным при помощи компьютера.
Задачи об упаковки шаров имеют в наши дни практическое значение, о котором в XVII веке Кеплер не подозревал. Они помогают решить проблему передачи информации с сохранением передаваемого сигнала в условиях помех.