Хотите видеть только хорошие новости?

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

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

Машина подтвердила правильность доказательства гипотезы Кеплера математиком Томасом Хейлзом (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:02 Сегодня

Адский пепел

Что сотворило с человечеством мощнейшее в истории извержение вулкана
00:03 17 января 2017

Чужой внутри

Как раковые клетки обретают неуязвимость и медленно уничтожают человека
00:06 25 ноября 2016
Адольф Гитлер в окружении девушек

Блудливый рейх

Как проституция поднимала боевой дух нацистов
Face masks depicting Russian President Vladimir Putin and U.S. President-elect Donald Trump hang for sale at a souvenir street shop in St.Petersburg, RussiaВеликий и ужасный
Почему пресса Британии и США демонизирует образ Путина
Министр обороны Саудовской Аравии принц Мухаммед объявляет о создании блокаНАТО с Кораном и гуриями
Саудовская Аравия строит собственный военный блок
People walk past the walls of Jerusalem's Old City lit in blue, white and red, colours of the French flag, in solidarity with Paris, in Jerusalem November 15, 2015Французский исход
Что заставляет евреев бежать из Пятой Республики в Израиль
Монастырь Мар Маттай«Саддам покончил бы с этим бардаком за пару недель»
Рассказ монаха древнего иракского монастыря о жизни по соседству с террористами
Лошадиные силы
Мустанги, воспитанные за решеткой, несут службу на границе
Заложники ситуации
Зачем США разворачивают бригаду в Восточной Европе
Достучаться до небес
Как в криминальной России разбираются с доносчиками
CH-53K King StallionСколько стоит вертолет
В поисках шеста для технологического барьера
Дональд ТрампБомбы не получилось
Что может помешать Трампу обменять ядерное оружие на санкции
Адский пепел
Что сотворило с человечеством мощнейшее в истории извержение вулкана
Чужой внутри
Как раковые клетки обретают неуязвимость и медленно уничтожают человека
Спиральная галактика NGC 3521Их взрывы
Найден источник инопланетных сигналов
Пироманы из Луганска
Как сумасшедшие изобретатели из ЛНР стали новыми «разрушителями легенд»
Кулер задымился
Как прекрасные девушки заставили югославов полюбить компьютеры
«У меня во дворе переодетые дипломаты пьют водку под окном»
В сети высмеяли облачавшихся в прекрасных дам и бомжей американских дипломатов
Дональд Трамп с женой Меланией и моделью Хайди Клум в 2008 годуБойкот по-голливудски
На инаугурации Трампа не будет звезд?
«Этим парням не нужен от меня секс»
История феминистки из Абу-Даби, которая живет за счет мужчин
«Живу обычно, ем летучих мышей»
История москвича, переехавшего в Камбоджу
Хейтеры возненавидят
Обычные женщины, прославившиеся в Instagram благодаря лишнему весу
Тест седана с динамикой суперкара
Тест Audi S8 Plus — представительского седана с максималкой 305 км/ч
Тест: угадай автомобиль под камуфляжем
Получится ли у автопроизводителей провести настоящего знатока? Давайте проверять
5 провалов Детройта
Засекреченный блогер о главных премьерах первого моторшоу 2017 года
Бандитские тачки суровых времен
Самые известные машины 1990-х
«Теперь она бомж и живет в закутке под лестницей»
История преподавательницы, лишившейся трех квартир в Москве
«Мы начали решать свои проблемы, как в 90-х»
За потребительские кредиты смогут отбирать квартиры
Развели тут бордель
Экскурсия по самому большому публичному дому Южного полушария
Война дворцам
Каких домов лишились в 2016 году звезды Голливуда