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

Пушечные ядра
Пушечные ядра

Машина подтвердила правильность доказательства гипотезы Кеплера математиком Томасом Хейлзом (Thomas Hales) из Питтсбургского университета в США. Как считают специалисты, это демонстрирует широкие возможности компьютеров для проведения трудоемких вычислительных доказательств, позволяя человеку сконцентрироваться на концептуальных сторонах проверки, сообщается на сайте New Scientist.

Свою гипотезу Кеплер опубликовал еще в 1611 году в своем знаменитом исследовании «О шестиугольных снежинках». В нем он предположил, что наиболее плотная упаковка шаров одинаковых размеров (то есть такая, когда объем пространства между шарами минимален при заданном количестве шаров) достигается при их пирамидальном упорядочивании по отношению друг к другу. Постановке задачи ученый обязан военному вопросу об оптимальном расположении пушечных ядер на палубе корабля.

В современной формулировке гипотезы Кеплера предполагается, что n-мерные шары живут в n+1-мерном евклидовом пространстве. Наиболее явно такая упаковка выглядит в двумерном случае, для которой условия на ее максимальную плотность были доказаны еще в 1940 году.

Наилучшая упаковка кругов равных диаметров на плоскости выглядит так: плоскость полностью покрывают одинаковыми правильными шестиугольниками (образуя так называемый шестиугольный паркет), а в центре и на вершинах шестиугольников размещают круги, диаметр которых равен длине стороны многоугольников. Получается, что на один шестиугольник приходится семь кругов: один — в центре и шесть — вокруг.

Доказательством гипотезы Кеплера Хейлз занимался с 1992 года по 1998-ой. Последовательное изложение доказательства содержало около 300 страниц текста и три гигабайта компьютерных данных вместе с программами, поэтому только в 1999 году математик отправил свою статью на публикацию в журнал Annals of Mathematics. Доказательство гипотезы Кеплера ученый свел к машинной процедуре перебора конечного числа различных вариантов упаковки шаров и минимизации функций, реализующих условия такого компактного расположения — типичной задаче линейного программирования.

Проверкой статьи Хейлза занимались в течение четырех лет 12 рецензентов, которые смогли заключить, что она на 99 процентов верна. Оставшийся непроверенный процент связан с тем, что рецензентам удалось проверить не все детали компьютерных вычислений автора. Только в 2006 году в Annals of Mathematics ученый опубликовал статью на 120 страницах. Работа содержала часть доказательства, напрямую не связанную с компьютерными вычислениями.

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

Хейлз намерен еще больше формализовать алгоритм компьютерной проверки математического доказательства гипотезы Кеплера, в том числе для его использования в других областях дискретной (комбинаторной) геометрии и совершенствования методов линейного программирования.

Обсудить
Наука и техника
 — 
00:00 24 февраля 2017

Стрелять, Карл!

Подстреленный Гитлер и отпуск в фашистской Италии: обзор Sniper Elite 4
Наука и техника
 — 
13:52 21 февраля 2017
Александр Шестаков

«В развитии главное — масштаб цели»

Интервью с ректором ЮУрГУ Александром Шестаковым о науке, образовании и развитии
Без ствола
Российские власти сокращают число владельцев гражданского оружия
Тир во время чумы
Как тренировка в стрелковом клубе обернулась смертью инструктора и ученика
Недостаток ресурсов при избытке амбиций
Что не так с индийской системой закупок оружия
Научили родину бомбить
Как отец воспитал из сына-подростка боевика «Джабхат ан-Нусры»
Допрос обвиняемого - митрополита Петроградского Вениамина на судебном процессе по делу об изъятии церковных ценностей, проходившем в зале филармонииСидеть!
Как молодая советская власть карала своих граждан
Стрелять, Карл!
Подстреленный Гитлер и отпуск в фашистской Италии: обзор Sniper Elite 4
Геноцид во благо
Уничтожение всего живого стало возможным на генном уровне
Есть кто живой?
У близкой к Солнцу звезды обнаружили семь двойников Земли
Орхан Памук«Моя страна становится все более авторитарной»
Орхан Памук о современной Турции и противостоянии Востока и Запада
Pierre et Gilles, Sainte Marie MacKillop (Kylie Minogue), 1995, Collection privée (c) Pierre et GillesГолубо-розовое
Транссексуалы, проститутки и панки в латексе на снимках гей-пары Пьера и Жиля
Смерть вождя
Роли, по которым мы запомним Алексея Петренко
Дэвид Алмонд«Вырасти — это понять, что родители были неправы»
Дэвид Алмонд о том, как опасно быть взрослым
Гудбай, Берлин
Десять лучших фильмов главного фестиваля зимы
Руины господского дома в усадьбе Ольгово. Дмитровский район, Московская область
Призрак Пиковой дамы
Где в Подмосковье можно встретить привидение
Страна оленья
Почему Якутия — главное направление для путешествий в этом году
Северно-ледовитая Венеция
Почему российским туристам стоит заглянуть в немецкий Нюрнберг
Иранская жемчужина
Что делать путешественнику в городке Бендер-Конг
Бог простит
В церкви нашли квартиру с красной мебелью и портретами в стиле поп-арт
Дворянское гнездо
Один из самых шикарных в мире домов нашли в диком лесу
«Пусть меня захоронят в отравленную, но родную землю»
Почему люди отказываются покидать чернобыльскую зону: реальные истории
Поставили баком
Англичане сделали идеальный дом из резервуара для воды