01
А
Астрономия
02
Б
Биология
03
Г
Гуманитарные науки
04
М
Математика и CS
05
Мд
Медицина
06
Нз
Науки о Земле
07
С
Сельское хозяйство
08
Т
Технические науки
09
Ф
Физика
10
Х
Химия и науки о материалах
Математика и Computer Science
19 июня

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

Пример гранецентрированной кубической упаковки шаров
Günter Lenz/Global Look Press

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

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

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

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

Комментарии

Все комментарии
Обсуждаемое