Гипотеза Кеплера об оптимальной плотности упаковки шаров
Эта задача возникла из-за военного вопроса об оптимальном расположении пушечных ядер на палубе корабля. Свою гипотезу немецкий ученый Кеплер опубликовал еще в 1611 году. Он предположил,
что наиболее плотная упаковка шаров
одинаковых размеров достигается при их
пирамидальном упорядочивании по отношению
друг к другу:
Главное условие, чтобы куча ядер не раскатилась во время качки. Выкладываем ядра в ряд на палубе. В следующий ряд кладем ядра так, чтобы шары размещались в щелях между сферами первого ряда. Если в первом ряду n шаров, то во втором n - 1 (потому что щелей между шарами на единицу меньше, чем самих шаров). Следующий ряд будет еще на единицу меньше ядер. И так далее, до тех пор, пока не получим слой из одного шара. Тогда получаем треугольную пирамиду из ядер.
Математически доказать гипотезу не удавалось на протяжении 400 лет.
В 1998 году математик Томас Хейлс представил компьютерное подтверждение гипотезы Кеплера с помощью линейного программирования. Изложение доказательства содержало около 300 страниц текста и три гигабайта компьютерных данных вместе с программами.
Проверкой его статьи занимались в течение четырех лет 12 рецензентов, которые смогли заключить, что она на 99 процентов верна.
И только в 2014 доказат ельство гипотезы было проверено при помощи компьютерной системы проверки доказательств.