开普勒猜想

**克卜勒猜想**（英語：Kepler conjecture）是以十七世紀德國天文學家約翰內斯・克卜勒為名的一個數學猜想。此猜想是關於在三維歐幾里德空間中最佳的裝球方式（即留下的空隙最小的裝球方式）的。此猜想認為在每個球大小相同的狀況下，沒有任何裝球方式的「密度」大於面心立方與六方最密堆積的「密度」，即 $\pi /{\sqrt {18}}$ ≈74.048%。

在 1998 年，托馬斯・黑爾斯（Thomas Callister Hales）藉由費耶斯・托特（Fejes Tóth (1953)）所提出的方式，提出了一個關於此猜想的證明。黑爾斯利用窮舉法（Proof by exhaustion）的方式證明此猜想，其證明大量地使用電腦程式的運算。審稿者曾說他們對於黑爾斯證明的正確性有 99% 的確定性，故克卜勒猜想目前已幾乎可說是個定理了。2014 年由黑爾斯引導的 Project FlysPecK 完成了對克卜勒猜想的形式化證明。

## 背景

若將一個容積很大的容器，以大量體積很小且體積彼此相等的小球給填充（顯然不可能完全填滿，一定會有些空隙留下），那其密度就是指所有小球體積的總和對容器空間的比值。若欲使該容器中能放入儘可能多的小球，就必須尋找密度最高的排列法，也就是使這些被裝填的小球彼此間能盡可能緊密地排在一起。

有人做過實驗，並發現隨機裝填的密度大約有 65%，然而小心地排列球的位置，可達致更高的密度。若在第一層，先將球以六角形的方式排列（即每個球四周圍繞六顆球），然後下一層的球放在「於上一層球之上能讓球中心位置最低的點」上，然後其餘層以此類推。這就是在市場水果攤上橘子堆疊的方式。每個階段對於下一層該如何擺放，都有著兩種選擇，故若一直重複此法，到了最後，會有無限多的、密度相同的球的堆疊存在，此法最為人知的兩種形式，即是面心立方和六方最密堆積這兩種方法（這兩種方法的平均密度相同），此法的平均密度如下：

　
: ${\frac {\pi }{\sqrt {18}}}\simeq 0.74048$ （即大約 74% 左右的空間為球所佔據）

克卜勒猜想說，這是所有可能的裝球排列法所能達到的最高密度，沒有更高的了。

## 起源

此猜想最早在 1611 年，由約翰內斯・克卜勒在其文章「關於六角雪花」（On the six-cornered snowflake）中提出。他研究了球的排列，並於 1606 年將之寫在與英國數學家兼天文學家托馬斯・哈里奧特（Thomas Harriot）的信中。哈里奧特是華特・雷利（Sir Walter Raleigh）的朋友與助手，雷利給了哈里奧特「在船支甲板上該怎樣堆疊砲彈才是最好的」這個問題。哈里奧特曾在 1591 年出版一本關於各種堆疊問題的研究，並曾發展出某種早期的原子論來。

## 十九世紀的發展

克卜勒並未證明他的猜想，而此猜下的下一步發展則由卡爾・弗里德里希・高斯所推展，高斯在 1831 年證明了若球必須在規則格中進行排列，則克卜勒猜想是正確的。

這就表示任何可反證克卜勒猜想的球排列方式必然是不規則的排列方式。然而要排除任何可能的不規則排列法是非常困難的，而這也是克卜勒猜想之所以如此難以證明的原因。實際上，當裝球的空間足夠小時，確實是有些不規則排列法的密度是高於面心立方排列法的，但當這些不規則排列法被推廣至更大的空間時，其密度總會降低。

在高斯出手後，整個十九世紀就再也沒有人在此定理上做出更進一步的推展了。1900 年，希爾伯特將此問題包含在希爾伯特的 23 個問題中，做為希爾伯特第十八問題的一部份。

## 廿世紀的進展

克卜勒猜想的下一步進展，由匈牙利數學家拉斯羅・費耶斯・托特（László Fejes Tóth）展開，他在 1953 年證明了決定任何排列法密度的問題，可變為有限量的計算過程（唯需要的計算量非常大）。這表示至少在原則上，透過窮舉法證明此定理是可能的。就如托特所言，一臺運算速度足夠快的電腦，可使這個理論上的結果，轉化為對此問題實際的證明過程。

與此同時，人們也努力地尋找三維空間裡任何可能的裝球方法的上界。英國數學家在 1958 年給出了一個 78% 的上界，之後數學家的努力稍微縮減了此數值，唯此數值距離面心立方密度的數值，也就是上述的 74% 左右的數值，依舊有一段距離。

項武義在 1993 年和 2001 年曾宣稱自己藉由幾何的方法，證明了克卜勒猜想。然而嘉伯・費耶斯・托特（拉斯羅・費耶斯・托特的兒子）卻在看此文後，說道：「在考慮細節後，我認為其證明許多關鍵性的陳述都沒有可接受的證明。」

黑爾斯在 1994 年丟出了對項武義證明較為詳盡的批評，項武義則在 1995 年對此進行回應。現在一般的看法認為項武義的證明是不完善的。

## 黑爾斯的證明

托馬斯・黑爾斯決定根據費耶斯・托特在 1953 年提出的思路來證明此猜想，他認為可透過一個有著 150 個變數的方程式式的最小值，來找出任何可能裝球排法的最大密度。在 1992 年，在其研究生山謬爾・費爾古生（Samuel Ferguson）的幫助下，他開始了一個藉由系統化地應用線性規劃的方法，對超過五千種不同的裝球法的每一個，找出其所提出的方程式式的下界的研究。如果此方程式式對於這些裝球法的下界都超過（此方程式式對於）面心立方的值的話，那克卜勒猜想就可得證。若要尋找每種情況的下界，則需要解超過十萬個線性規劃問題。

當托馬斯・黑爾斯在 1996 年公開其計劃時，他說這證明的結果近了，然而依舊需要「一兩年的時間」來完成它。在 1998 年，托馬斯・黑爾斯宣佈他的證明已經完成了。在此階段，其證明包含了 250 頁的註解與 3GB 的電腦檔案，其中包括了電腦程式、資料和結果等。

雖然這證明在本質上是不尋常的，但因一個由 20 名裁判員組成的小組接受其內容，《數學年報》（Annals of Mathematics）依舊同意了此論文在其上的發表。2003 年，在經過四年的努力後，裁判員小組的頭領嘉伯・費耶斯・托特報告道他們小組「99% 確定了」此證明的正確性，然而他們不能完全確定所有電腦計算的正確性。

托馬斯・黑爾斯在 2005 年出版了一份超過一百頁的文檔以說明其證明的非電腦部份的細節。費爾古生在 2006 年及數篇之後發的文則描述了其電腦運作的部份。黑爾斯與費爾古生在 2009 年，獲得了福爾克生獎在離散數學方面傑出論文的獎項（Fulkerson Prize for outstanding papers in the area of discrete mathematics）。

## 形式證明

在 2003 年一月，黑爾斯宣佈將要開始一個以完成克卜勒猜想的形式證明為目標的協作計劃。此計劃的目標，是要藉由產生可由 HOL 等自動證明檢定（Automated proof checking）軟體確認其正確性的證明，來移除所有剩餘的、和證明有效性相關的不確定成份。這個計劃被稱作「Project FlysPecK」，其中的 F、P 和 K 代表「Formal Proof of Kepler」，也就是「克卜勒猜想的形式證明」。黑爾斯認為此計劃需要大約 20 年的時間才能完成。該計劃在 2014 年 8 月 10 日宣告完成。在 2015 年月，黑爾斯和 21 位協作者共同發表了「克卜勒猜想的形式化證明」。

## 相關問題

**杜厄（Axel Thue）定理：**
: 正六邊形排列法（每個球旁邊都圍六顆球的排列法）是平面上密度最高的裝球法（1890）。

　
: 這是克卜勒問題在二維空間上的版本；其證明是較簡易的。

**六角蜂巢猜想：**
: 若要將平面分割成彼此大小相同的區塊，則最有效的分法是將之分成由正六邊形組成的區塊。黑爾斯對此猜想的證明（1999）。

　
: 此問題與杜氏定理相關。

**正十二面體猜想：**
: 在相等的球的裝載之中，一個球的沃羅諾伊圖多邊形的體積至少與內徑為 1 的正十二面體相等。麥克勞林（McLaughlin）的證明可點此見，他也因此證明而得到 1999 年的摩根獎（Frank and Brennie Morgan Prize for Outstanding Research in Mathematics by an Undergraduate Student）。

　
: 這是一個相關的問題，證明者使用的證明技巧與黑爾斯對克卜勒猜想使用的技巧類似。此猜想在 1950 年代由拉斯羅・費耶斯・托特提出。

**韋爾 — 費倫結構（Weaire–Phelan structure）上的克爾文問題（Kelvin problem/Kelvin conjecture）：**
: 在三維空間中，最有效率的泡沫為何？在韋爾 — 費倫結構被發現前，有一百多年的時間，人們認為此問題可透過克爾文結構（Kelvin structure）來證明。然而韋爾 — 費倫結構的發現，使得克爾文猜想被否證，而這件事，也是一個可用於警示人們當小心接受黑爾斯對克卜勒猜想的證明的理由。

**高維空間的裝球問題：**
: n 維空間（n > 3）的最佳裝球方式，至今依舊未完全被證實。

## 參考書目

## 外部連結

* 埃里克・韋斯坦因. Kepler Conjecture. MathWorld.
* Front page of 'On the six-cornered snowflake'（頁面存檔備份，存於網際網路檔案館）
* Thomas Hales' home page（頁面存檔備份，存於網際網路檔案館）
* Overview of Hales' proof（頁面存檔備份，存於網際網路檔案館）
* Article in American Scientist by Dana Mackenzie
* Flyspeck I: Tame Graphs, verified enumeration of tame plane graphs as defined by Thomas C. Hales in his proof of the Kepler Conjecture（頁面存檔備份，存於網際網路檔案館）