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

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

Машина подтвердила правильность доказательства гипотезы Кеплера математиком Томасом Хейлзом (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, в рамках которого ему удалось создать программы, анализирующие непротиворечивость выводов компьютерной части доказательства гипотезы Кеплера. Автоматизация, формализация и совершенствование алгоритмов этих программ составили основную часть работы над проверкой машинного доказательства гипотезы Кеплера.

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

подписатьсяОбсудить
U.S. based cleric Fethullah Gulen at his home in Saylorsburg, Pennsylvania, U.S. July 29, 2016. REUTERS/Charles MostollerГидра Гюлена
Кого Эрдоган считает своим главным политическим противником
«Роль России и США в Сирии сильно преувеличивают»
Василий Кузнецов о происходящем в Сирии и других странах Ближнего Востока
uly 25, 2016 - Philadelphia, Pennsylvania, U.S - The March For Our Lives heads down Broad St. towards the Democratic National Convention at the Wells Fargo Center. The march is in protest to the nomination of Hillary Clinton at the DNC and is made up of a coalition of Green Party activists, Bernie Sanders supporters, anarchists, socialists, and othersДругой альтернативы нет
Что предлагают независимые кандидаты в президенты США
«Символ мощи и непредсказуемости — конечно же, медведь»
Турецкие эксперты объясняют, что их сограждане думают о России и русских
Шимон ПересЧеловек большой мечты
Памяти Шимона Переса
Rostov's Sardar Azmoun reacts leaving a pithc after the Champions League Group D soccer match between Rostov and PSV Eindhoven, in Rostov-on-Don, Southern Russia, Wednesday, Sept. 28, 2016. (AP Photo/Str)Дон, банан
Какое наказание грозит «Ростову» за расистскую выходку болельщиков
День за дном
Российские ЦСКА и «Ростов» после второго тура ЛЧ оказались на последних местах
Сэм ЭллардайсСтрасти по четвертой власти
Как журналисты уволили главного тренера футбольной сборной Англии
«Однажды мы пошли купаться в 40-градусный мороз»
Один из лучших сноубордистов мира о страхе, полетах над Камчаткой и зимних Играх
Рожать нельзя помиловать
Как живет страна, где за аборт можно получить 10 лет тюрьмы
Богат бедняк мечтами
Фотопроект о реальности и фантазиях бездомных людей
Джентльмен из песочницы
10 ярких поступков детей, поставивших на место знаменитостей и политиков
«Корейцы пьют даже больше русских»
История жителя Владивостока, поселившегося в Сеуле
Париж-2016
Репортаж с Парижского моторшоу: день первый
Великий увозитель
Все, что нужно знать о новом Land Rover Discovery, в 27 фотографиях
Лошади на литры
Самые вместительные машины с моторами мощностью 600 л.с. и больше
Народный успех
Как прошел первый сезон в РСКГ победителя третьего сезона «Народного пилота»
Стенка на стенку
Джоконда, покемон и Корлеоне с Чебурашкой — лучшее от уличных художников Москвы
«За годы ожидания мы выдохлись. Живем сейчас где попало»
История покупателей жилья, заселенных в недостроенные дома в Подмосковье
«Мне угрожали, обещали закатать в асфальт»
История валютной ипотечницы, которая прошла оба кризиса и ни о чем не пожалела
Что-то пошло не так
Как выглядят населенные насекомыми города, жизнь без неба и море над головой
Кто купил Америку
Десять человек, которым на самом деле принадлежат земли США