В 1998 году Томас Хейлз , следуя подходу, предложенному Фейешем Тотом (1953), объявил, что у него есть доказательство гипотезы Кеплера. Доказательство Хейлза — это доказательство исчерпыванием, включающее проверку многих отдельных случаев с использованием сложных компьютерных вычислений. Рецензенты заявили, что они «на 99% уверены» в правильности доказательства Хейлза, и гипотеза Кеплера была принята в качестве теоремы . В 2014 году команда проекта Flyspeck во главе с Хейлзом объявила о завершении формального доказательства гипотезы Кеплера с использованием комбинации помощников доказательства Isabelle и HOL Light . В 2017 году формальное доказательство было принято журналом Forum of Mathematics, Pi . [1]
Фон
Схемы кубической плотнейшей упаковки (слева) и гексагональной плотнейшей упаковки (справа).
Представьте себе, что вы заполняете большой контейнер маленькими одинаковыми по размеру сферами: скажем, фарфоровый галлонный кувшин одинаковыми шариками. «Плотность» расположения равна общему объему всех шариков, деленному на объем кувшина. Чтобы максимизировать количество шариков в кувшине, нужно создать расположение шариков, сложенных между стенками и дном кувшина, которое имеет максимально возможную плотность, так что шарики будут упакованы как можно плотнее.
Эксперимент показывает, что если бросать шарики хаотично, не прилагая усилий, чтобы расположить их плотнее, то можно достичь плотности около 65%. [2] Однако более высокую плотность можно получить, аккуратно расположив шарики следующим образом:
Для первого слоя шариков расположите их в виде шестиугольной решетки ( узор в виде сот ).
Поместите следующий слой шариков в самые нижние зазоры, которые вы можете найти над и между шариками первого слоя, независимо от рисунка.
Продолжайте ту же процедуру заполнения самых нижних промежутков в предыдущем слое для третьего и остальных слоев, пока шарики не достигнут верхнего края кувшина.
На каждом шаге есть по крайней мере два варианта размещения следующего слоя, поэтому этот в противном случае не запланированный метод укладки сфер создает несчетное бесконечное число одинаково плотных упаковок. Самые известные из них называются кубической плотной упаковкой и гексагональной плотной упаковкой . Каждая из этих упаковок имеет среднюю плотность
Гипотеза Кеплера гласит, что это лучшее, что можно сделать — никакая другая расстановка шариков не имеет более высокой средней плотности: несмотря на то, что существует поразительно много различных возможных расстановок, которые следуют той же процедуре, что и шаги 1–3, никакая упаковка (согласно процедуре или нет) не может вместить больше шариков в тот же кувшин.
Происхождение
Одна из диаграмм из Strena Seu de Nive Sexangula , иллюстрирующая гипотезу Кеплера
Впервые гипотеза была высказана Иоганном Кеплером (1611) в его работе «О шестиугольной снежинке». Он начал изучать расположение сфер в результате своей переписки с английским математиком и астрономом Томасом Харриотом в 1606 году. Харриот был другом и помощником сэра Уолтера Рэли , который попросил Харриота найти формулы для подсчета сложенных пушечных ядер, задание, которое, в свою очередь, привело знакомого математика Рэли к размышлению о том, какой наилучший способ складывать пушечные ядра. [3] Харриот опубликовал исследование различных схем укладки в 1591 году и продолжил разработку ранней версии атомной теории .
Девятнадцатый век
У Кеплера не было доказательства этой гипотезы, и следующий шаг был сделан Карлом Фридрихом Гауссом (1831), который доказал, что гипотеза Кеплера верна, если сферы должны быть расположены в правильной решетке .
Это означало, что любая упаковка, которая опровергала бы гипотезу Кеплера, должна была бы быть нерегулярной. Но исключить все возможные нерегулярные упаковки очень сложно, и именно это сделало гипотезу Кеплера столь труднодоказуемой. На самом деле существуют нерегулярные упаковки, которые плотнее кубической плотной упаковки в достаточно малом объеме, но любая попытка расширить эти упаковки, чтобы заполнить больший объем, как теперь известно, всегда уменьшает их плотность.
Следующий шаг к решению был сделан Ласло Фейешем Тотом . Фейеш Тот (1953) показал, что задача определения максимальной плотности всех расположений (регулярных и нерегулярных) может быть сведена к конечному (но очень большому) числу вычислений. Это означало, что доказательство исчерпыванием , в принципе, возможно. Как понял Фейеш Тот, достаточно быстрый компьютер мог бы превратить этот теоретический результат в практический подход к проблеме.
Между тем, были предприняты попытки найти верхнюю границу для максимальной плотности любого возможного расположения сфер. Английский математик Клод Эмброуз Роджерс (см. Rogers (1958)) установил верхнюю границу около 78%, а последующие усилия других математиков немного снизили это значение, но оно все еще было намного больше, чем кубическая плотность плотной упаковки около 74%.
В 1990 году У-И Сян заявил, что доказал гипотезу Кеплера. Доказательство было высоко оценено Encyclopaedia Britannica и Science , а Сян также был отмечен на совместных заседаниях AMS-MAA. [4] У-И Сян (1993, 2001) заявил, что доказал гипотезу Кеплера с помощью геометрических методов. Однако Габор Фейеш Тот (сын Ласло Фейеш Тота) заявил в своем обзоре статьи: «Что касается деталей, то, по моему мнению, многие ключевые утверждения не имеют приемлемых доказательств». Хейлз (1994) дал подробную критику работы Сяна, на которую Сян (1995) ответил. Текущий консенсус заключается в том, что доказательство Сяна неполное. [5]
Доказательство Хейлза
Следуя подходу, предложенному [ 6] Ласло Фейешем Тотом , Томас Хейлз , тогда работавший в Мичиганском университете , определил, что максимальную плотность всех расположений можно найти, минимизируя функцию со 150 переменными. В 1992 году при содействии своего аспиранта Сэмюэля Фергюсона он приступил к исследовательской программе по систематическому применению методов линейного программирования для нахождения нижней границы значения этой функции для каждой из набора из более чем 5000 различных конфигураций сфер. Если бы для каждой из этих конфигураций можно было найти нижнюю границу (для значения функции), которая была бы больше значения функции для кубической плотной упаковки, то гипотеза Кеплера была бы доказана. Чтобы найти нижние границы для всех случаев, потребовалось решить около 100 000 задач линейного программирования.
Представляя ход своего проекта в 1996 году, Хейлз сказал, что конец уже виден, но на его завершение может уйти «год или два». В августе 1998 года Хейлз объявил, что доказательство завершено. На том этапе оно состояло из 250 страниц заметок и 3 гигабайт компьютерных программ, данных и результатов.
Несмотря на необычный характер доказательства, редакторы Annals of Mathematics согласились опубликовать его при условии, что оно будет принято коллегией из двенадцати рецензентов. В 2003 году, после четырех лет работы, глава коллегии рецензентов Габор Фейеш Тот сообщил, что коллегия была «на 99% уверена» в правильности доказательства, но они не могли подтвердить правильность всех компьютерных вычислений.
Hales (2005) опубликовал 100-страничную статью, подробно описывающую некомпьютерную часть своего доказательства. Hales & Ferguson (2006) и несколько последующих статей описали вычислительные части. Hales и Ferguson получили премию Фулкерсона за выдающиеся работы в области дискретной математики за 2009 год.
Формальное доказательство
В январе 2003 года Хейлз объявил о начале совместного проекта по созданию полного формального доказательства гипотезы Кеплера. Целью было устранить любую оставшуюся неопределенность относительно действительности доказательства путем создания формального доказательства, которое может быть проверено автоматизированным программным обеспечением для проверки доказательств, таким как HOL Light и Isabelle . Этот проект назывался Flyspeck — расширение аббревиатуры FPK, означающей формальное доказательство Кеплера . В начале этого проекта, в 2007 году, Хейлз подсчитал, что создание полного формального доказательства займет около 20 лет работы. [7] Хейлз опубликовал «чертеж» формального доказательства в 2012 году; [8] о завершении проекта было объявлено 10 августа 2014 года. [9] В январе 2015 года Хейлз и 21 соавтор опубликовали статью под названием «Формальное доказательство гипотезы Кеплера» на arXiv , заявив, что доказали гипотезу. [10] В 2017 году формальное доказательство было принято журналом Forum of Mathematics . [1]
Связанные проблемы
Теорема Туэ
Правильная гексагональная упаковка — самая плотная упаковка кругов на плоскости (1890). Плотность составляет π ⁄ √ 12 .
Двумерный аналог гипотезы Кеплера; доказательство элементарное. Хенк и Циглер приписывают этот результат Лагранжу в 1773 году (см. ссылки, стр. 770).
Простое доказательство Чау и Чанга от 2010 года использует триангуляцию Делоне для множества точек, являющихся центрами окружностей в насыщенной упаковке окружностей. [11]
Объем многогранника Вороного сферы в упаковке равных сфер не меньше объема правильного додекаэдра с радиусом вписанной окружности 1. Доказательство Маклафлина [13] , за которое он получил премию Моргана 1999 года .
Связанная проблема, доказательство которой использует методы, схожие с доказательством гипотезы Кеплера Хейлза. Гипотеза Л. Фейеша Тота, выдвинутая в 1950-х годах.
Какая пена является наиболее эффективной в 3 измерениях? Предполагалось, что это может быть решено структурой Кельвина , и это широко считалось более 100 лет, пока не было опровергнуто в 1993 году открытием структуры Уэйра–Фелана . Удивительное открытие структуры Уэйра–Фелана и опровержение гипотезы Кельвина является одной из причин осторожности в принятии доказательства Хейлза гипотезы Кеплера.
В 2016 году Марина Вязовская объявила о доказательстве оптимальной упаковки сфер в размерности 8, что быстро привело к решению в размерности 24. [14] Однако вопрос оптимальной упаковки сфер в размерностях, отличных от 1, 2, 3, 8 и 24, все еще остается открытым.
^ Хейлз, Томас С. (2012). Плотные упаковки сфер: план формальных доказательств . Серия заметок лекций Лондонского математического общества. Том 400. Издательство Кембриджского университета. ISBN978-0-521-61770-3.
Гаусс, Карл Ф. (1831), «Untersuruchungen über die Eigenschaften der Positiven ternären Quadatischen Formen von Ludwig August Seeber», Göttingische gelehrte Anzeigen (108): 1065–1077
Хейлз, Томас С. (2000), «Пушечные ядра и соты», Notices of the American Mathematical Society , 47 (4): 440–449, ISSN 0002-9920, MR 1745624Элементарное изложение доказательства гипотезы Кеплера.
Хейлз, Томас К. (2005), «Доказательство гипотезы Кеплера», Annals of Mathematics , вторая серия, 162 (3): 1065–1185, arXiv : math/9811078 , doi :10.4007/annals.2005.162.1065, ISSN 0003-486X, MR 2179728
Хейлз, Томас К. (2006), «Исторический обзор гипотезы Кеплера», Дискретная и вычислительная геометрия , 36 (1): 5–20, doi : 10.1007/s00454-005-1210-2 , ISSN 0179-5376, MR 2229657
Хейлз, Томас К.; Фергюсон, Сэмюэл П. (2006), «Формулировка гипотезы Кеплера» (PDF) , Дискретная и вычислительная геометрия , 36 (1): 21–69, arXiv : math/9811078 , doi :10.1007/s00454-005-1211-1, ISSN 0179-5376, MR 2229658, S2CID 6529590
Хейлз, Томас С.; Фергюсон, Сэмюэл П. (2011), Гипотеза Кеплера: Доказательство Хейлза-Фергюсона , Нью-Йорк: Springer, ISBN 978-1-4614-1128-4
Хейлз, Томас С. (2012), «Плотные упаковки сфер: план формальных доказательств», серия лекций Лондонского математического общества , 400 , Cambridge University Press, ISBN 978-0-521-61770-3
Хенк, Мартин; Циглер, Гюнтер (2008), La congettura di Keplero , La matematica. Проблемы и теории, том. 2, Турин: Эйнауди
Сян, У-И (1993), «О проблеме упаковки сфер и доказательстве гипотезы Кеплера», Международный журнал математики , 4 (5): 739–831, doi :10.1142/S0129167X93000364, ISSN 0129-167X, MR 1245351
Сян, У-И (1995), «Возражение на статью Т. К. Хейлза: статус гипотезы Кеплера », The Mathematical Intelligencer , 17 (1): 35–42, doi :10.1007/BF03024716, ISSN 0343-6993, MR 1319992, S2CID 119641512
Hsiang, Wu-Yi (2001), Принцип наименьшего действия образования кристаллов плотной упаковки и гипотеза Кеплера , Nankai Tracts in Mathematics, т. 3, River Edge, NJ: World Scientific Publishing Co. Inc., doi : 10.1142/9789812384911, ISBN 978-981-02-4670-9, МР 1962807
Кеплер, Иоганн (1611), Strena seu de nive sexangula [ Шестиугольная снежинка ] (на латыни), Paul Dry Books, ISBN 978-1-58988-053-5, МР 0927925
"О шестиугольной снежинке". Открытие Кеплера . Архивировано из оригинала 2007-12-19.
Fejes Tóth, L. (1953), Lagerungen in der Ebene, auf der Kugel und im Raum , Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Band LXV, Berlin, New York: Springer-Verlag , doi :10.1007/ 978-3-642-65234-9, ISBN 978-3-642-65235-6, МР 0057566
