19.06.2017

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

Группа математиков под руководством профессора Питтсбургского университета Томаса Хейлса (Thomas Hales) представила положительные результаты проверки сделанного ранее доказательства математической гипотезы об упаковке шаров. Статья об этом опубликована в журнале Forum of Mathematics, Pi.

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

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

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

Задачи об упаковки шаров имеют в наши дни практическое значение, о котором в XVII веке Кеплер не подозревал. Они помогают решить проблему передачи информации с сохранением передаваемого сигнала в условиях помех.

Источники:

1. polit.ru