Войти
Гипотеза Кеплера, названная в честь 17-го века математик и астроном Иоганн Кеплер, представляет собой математическую теорему о упаковке сфер в трехмерном евклидовом пространстве. В нем говорится, что никакое расположение сфер одинакового размера, заполняющего пространство, не имеет большей средней плотности, чем у плотной кубической упаковки (гранецентрированный куб ) и гексагональная плотная упаковка устройства. Плотность этих размещений составляет около 74,05%.
В 1998 году Томас Хейлз, следуя подходу, предложенному Фейесом Тотом (1953), объявил, что у него есть доказательство гипотезы Кеплера. Доказательство Хейлза - это доказательство исчерпания, включающее проверку многих отдельных случаев с использованием сложных компьютерных вычислений. Рецензенты заявили, что они были «на 99% уверены» в правильности доказательства Хейлза, и гипотеза Кеплера была принята как теорема. В 2014 году команда проекта Flyspeck во главе с Хейлсом объявила о завершении формального доказательства гипотезы Кеплера с использованием комбинации помощников доказательства Изабель и HOL Light. В 2017 г. формальное доказательство было принято журналом Forum of Mathematics, Pi.
Диаграммы кубической плотной упаковки (слева) и гексагональной плотной упаковки (справа). Представьте, что вы заполняете большой контейнер маленькими сферами одинакового размера. Плотность расположения равна совокупному объему сфер, деленному на объем контейнера. Максимальное количество сфер в контейнере означает создание конструкции с максимально возможной плотностью, так чтобы сферы были упакованы вместе как можно плотнее.
Эксперимент показывает, что при случайном падении сфер достигается плотность около 65%. Однако более высокой плотности можно достичь, осторожно расположив сферы следующим образом. Начните со слоя сфер в гексагональной решетке, затем поместите следующий слой сфер в самые нижние точки, которые вы можете найти над первым слоем, и так далее. На каждом этапе есть два варианта размещения следующего слоя, поэтому этот естественный метод укладки сфер создает бесчисленное множество одинаково плотных упаковок, самые известные из которых называются кубической плотной упаковкой и гексагональной плотной упаковкой. Каждая из этих конфигураций имеет среднюю плотность
Гипотеза Кеплера говорит, что это лучшее, что можно сделать - никакое другое расположение сфер не имеет более высокой средней плотности.
Одна из диаграмм из Strena Seu de Nive Sexangula, иллюстрирующая гипотезу Кеплера Гипотеза впервые была высказана Иоганном Кеплером (1611) в своей статье «О шестигранной снежинке». Он начал изучать расположение сфер в результате своей переписки с английским математиком и астрономом Томасом Харриотом в 1606 году. Харриот был другом и помощником сэра Уолтера Рэли, который имел поставил перед Харриотом задачу определить, как лучше всего складывать пушечные ядра на палубах его кораблей. Харриот опубликовал исследование различных схем укладки в 1591 году и продолжил разработку ранней версии атомной теории.
У Кеплера не было доказательства своей гипотезы, и следующий шаг был взят Карлом Фридрихом Гауссом (1831), который доказал, что гипотеза Кеплера верна, если сферы должны быть расположены в правильной решетке.
. Это означало, что любая упаковка, опровергающая гипотезу Кеплера, должна быть неправильной. Но исключить все возможные нерегулярные схемы очень сложно, и именно поэтому гипотеза Кеплера так трудно доказать. Фактически, существуют нерегулярные устройства, более плотные, чем кубические, плотно упакованные в достаточно небольшом объеме, но теперь известно, что любая попытка расширить эти устройства для заполнения большего объема всегда снижает их плотность.
После Гаусса не было сделано никакого дальнейшего прогресса в доказательстве гипотезы Кеплера в девятнадцатом веке. В 1900 Дэвид Гильберт включил его в свой список двадцати трех нерешенных проблем математики - это часть восемнадцатой проблемы Гильберта.
Следующий шаг к решению был сделан Ласло Фейес Тот. Фейес Тот (1953) показал, что проблема определения максимальной плотности всех расположений (регулярных и нерегулярных) может быть сведена к конечному (но очень большому) количеству вычислений. Это означало, что доказательство путем исчерпания в принципе возможно. Как понял Фейес Тот, достаточно быстрый компьютер может превратить этот теоретический результат в практический подход к проблеме.
Между тем были предприняты попытки найти верхнюю границу максимальной плотности любого возможного расположения сфер. Английский математик Клод Амброуз Роджерс (см. Rogers (1958)) установил верхнюю границу около 78%, и последующие усилия других математиков немного снизили это значение, но это все еще было очень много. больше, чем плотность кубической плотной упаковки около 74%.
В 1990 году утверждал, что доказал гипотезу Кеплера. Доказательство получило похвалу от Encyclopdia Britannica и Science, а Сян был также удостоен чести на совместных заседаниях AMS-MAA. У-И Сян (1993, 2001) утверждал, что доказал гипотезу Кеплера с помощью геометрических методов. Однако (сын Ласло Фейеса Тота) заявил в своем обзоре статьи: «Что касается деталей, я считаю, что многие ключевые утверждения не имеют приемлемых доказательств». Хейлз (1994) ошибка harvtxt: несколько целей (2 ×): CITEREFHales1994 (help ) дал подробную критику работы Сяна, на которую Сян (1995) ответил. Сегодняшний консенсус состоит в том, что доказательство Сяна является неполным.
Следуя подходу, предложенному Фейесом Тотом (1953), Томасом Хейлзом, затем на Мичиганский университет определил, что максимальную плотность всех расположений можно найти, минимизируя функцию со 150 переменными. В 1992 году при содействии своего аспиранта Сэмюэля Фергюсона он приступил к исследовательской программе по систематическому применению методов линейного программирования, чтобы найти нижнюю границу значения этой функции для каждого из набора из более чем 5000 различных конфигурации шаров. Если бы нижняя граница (для значения функции) могла быть найдена для каждой из этих конфигураций, которая была бы больше, чем значение функции для кубической конструкции с плотной упаковкой, тогда гипотеза Кеплера была бы доказана. Для нахождения оценок снизу для всех случаев было решено около 100 000 задач линейного программирования.
Представляя прогресс своего проекта в 1996 году, Хейлз сказал, что конец близок, но это может занять «год или два». В августе 1998 года Хейлз объявил, что доказательство завершено. На этом этапе он состоял из 250 страниц заметок и 3 гигабайт компьютерных программ, данных и результатов.
Несмотря на необычный характер доказательства, редакторы Annals of Mathematics согласились опубликовать его при условии, что оно будет принято группой из двенадцати рецензентов. В 2003 году, после четырех лет работы, глава судейской коллегии Габор Фейес Тот сообщил, что комиссия «на 99% уверена» в правильности доказательства, но не может подтвердить правильность всех компьютерных расчетов..
Хейлз (2005) опубликовал статью на 100 страниц, в которой подробно описывалась некомпьютерная часть его доказательства. Hales Ferguson (2006) и несколько последующих статей описали вычислительные части. Хейлз и Фергюсон получили Премию Фулкерсона за выдающиеся работы в области дискретной математики за 2009 год.
В январе 2003 года Хейлз объявил о начале совместный проект по созданию полного формального доказательства гипотезы Кеплера. Цель состояла в том, чтобы устранить любую оставшуюся неуверенность в достоверности доказательства путем создания формального доказательства, которое может быть проверено с помощью автоматизированной проверки программного обеспечения, такого как HOL Light и Isabelle. Этот проект называется Flyspeck - буквы F, P и K означают формальное доказательство Кеплера. Хейлз подсчитал, что создание полного формального доказательства потребует около 20 лет работы. Хейлз впервые опубликовал «план» формального доказательства в 2012 году; проект был объявлен завершенным 10 августа 2014 года. В январе 2015 года Хейлз и 21 сотрудник представили в arXiv документ под названием «Формальное доказательство гипотезы Кеплера», утверждая, что это предположение доказано. В 2017 году формальное доказательство было принято в журнал Forum of Mathematics.
