2014 克卜勒懸案落幕：Flyspeck 用 50 萬行證明封印球體堆積#

報案人：Johannes Kepler（1611）。案情：水果攤的堆法是否最省空間？四百年無人能定罪。偵探：Thomas Hales 及其 Flyspeck 團隊。兇器：HOL Light ＋ Isabelle ＋區間算術。

案發現場#

1611 年，Kepler 在《論六角雪花》中隨手寫下一句猜想：把等大球體堆起來，沒有比面心立方堆積更密的方法。其密度為：

\[ \delta_{fcc} = \frac{\pi}{\sqrt{18}} \approx 0.74 \]

換句話說，無論你怎麼堆，球體佔據空間的比例 \(\delta\) 都滿足 \(\delta \le \pi / \sqrt{18}\) 。水果攤老闆早就知道，數學家卻證明不出來。

時間快轉到 1998 年。密西根大學的 Hales 宣布：他與 Samuel Ferguson 用計算機證明了克卜勒猜想。證明長達 300 頁紙本加上 3GB 程式，包含 5000 多個線性規劃問題與上萬個非線性不等式。

期刊《Annals of Mathematics》派出 12 位審稿人，耗時 6 年，最後給出史上最無奈的審查意見：「我們 99% 相信證明是對的，但無法完全確定所有計算都正確。」審稿困境本身成了案件的一部分：當證明依賴成千上萬行 C 程式與浮點運算時，同行評審已經失效。

Hales 的反應是偵探式的：既然人類陪審團判不了，那就請機器法官。他在 2003 年啟動 Flyspeck 計畫（Formal Proof of Kepler），發誓要用證明助理把整個證明重做一遍，一行程式都不放過。

偵查過程#

線索一：把幾何變成組合——Tame 圖的包圍網#

Hales 原證明的戰略是把無窮多種堆積方法，化約為有限個可檢查的案件。關鍵步驟是引入「tame 圖」：

對每個球心作 Voronoi 分解，把空間切成多面體胞腔。
將每個胞腔的鄰接關係編碼為平面圖 \(G\) ，其頂點是鄰近球心，邊是接觸關係。
證明只需檢查滿足特定組合條件的 tame 圖，其數量約為 5000 種。

這一步把連續幾何問題變成了離散列舉問題。用偵探的話說：先把全城的可疑住所列成名單，再逐家搜查。

形式化時，團隊必須在 HOL Light 中重建平面圖理論、歐拉公式 \(V - E + F = 2\) ，以及 tame 性的全部定義，單是這部分就耗費數年。

線索二：區間算術——給浮點計算戴上手銬#

全案最棘手的是數萬個不等式，例如需要證明某個 6 變元函數 \(f(x)\) 在矩形區域 \(D\) 上恆小於某個界 \(M\) ，即 \(\forall x \in D, f(x) < M\) 。

傳統的浮點計算會有捨入誤差，不能作為證據。Flyspeck 採用的兇器是區間算術（interval arithmetic）：每個實數 \(x\) 都用一個保證包含它的區間 \([a, b]\) 表示，運算規則為：

\[ [a, b] + [c, d] = [a + c, b + d] \]

\[ [a, b] \times [c, d] = [min(ac, ad, bc, bd), max(ac, ad, bc, bd)] \]

只要區間運算的結果整體落在 \((- \infty, M)\) 內，原不等式就得證。為了處理捨入，區間端點使用可驗證的浮點上下界，必要時自動細分區域 \(D\) ，直到精度足夠。

團隊在 HOL Light 中形式化了完整的區間算術函式庫，並用它驗證了超過 23000 條非線性不等式。這是整個 Flyspeck 耗時最久、CPU 時間最長的部分，動用了大量雲端運算。

線索三：HOL Light ＋ Isabelle 的雙法庭#

Flyspeck 採用了雙證明器戰略，分工如下：

戰場	證明器	內容
幾何與圖論	HOL Light	tame 圖列舉、線性規劃驗證主體
組合列舉	Isabelle	圖同構分類、tame 圖完備性
不等式	HOL Light	區間算術、非線性優化
整體串接	HOL Light	最終定理 \(\delta \le \pi / \sqrt{18}\)

最終的定理陳述在 HOL Light 中的模樣大致是：對任意有限球堆積 \(V\) ，其密度上界成立。總計約 50 萬行形式化證明腳本，包含數千個引理。

2014 年 8 月，HOL Light 的核心檢查器對整個證明輸出成功訊息。Hales 宣布 Flyspeck 完工，並把審稿人的難題丟回給期刊：現在你們可以 100% 相信了。

結案報告#

克卜勒猜想從 1611 年立案，到 2014 年才算真正結案，歷時 403 年。此案的意義遠超一個堆球問題：

審稿制度的警鐘：6 年審稿困境證明了超大計算證明的紙本時代已經結束，機器檢驗是唯一出路。
驗證技術的試金石：區間算術、線性規劃驗證、圖列舉的形式化，成為後來驗證編譯器、數值軟體的通用工具。
規模的里程碑：50 萬行證明在當時是僅次於 Odd Order 的巨案，證明了 HOL Light 與 Isabelle 都能扛住工業級負載。
與 Odd Order 的呼應：2012 年的群論大案與 2014 年的幾何大案，前後腳完成，標誌著「大定理形式化」時代的到來，直接鼓舞了後來的 Lean mathlib 與 AI 證明。

Hales 本人則轉向了下一個理想：讓形式化證明像 LaTeX 一樣普及，人人可寫，人人可驗。

證據與工具#

證據一：密度上界的最終形式

let KEPLER_CONJECTURE = `!V. packing V
  ==> (?c. !r. &1 <= r ==> &(CARD (V INTER ball (vec 0) r)) <= pi * r pow 3 / sqrt (&18) + c * r pow 2)`;;

其中 \(packing(V)\) 表示 \(V\) 為球堆積， \(ball\) 為球體，右端第一項正是 \(\pi r^{3} / \sqrt{18}\) 的體積界。

證據二：區間算術示意表

運算	區間版本	保證
\(x + y\)	\([a, b] + [c, d]\)	真值必在結果區間內
\(x \times y\)	端點四種組合取極值	含捨入誤差上界
\(exp(x)\)	單調函數端點映射	誤差可控
細分策略	\(D = D_{1} \cup D_{2}\) 遞迴驗證	精度不足就切半

證據三：偵探工具箱

工具	作用
HOL Light	John Harrison 的輕量高階邏輯證明器，主戰場
Isabelle	Nipkow 等人的通用框架，負責圖列舉交叉驗證
區間算術庫	把浮點計算變成法庭可接受的證據
線性規劃驗證器	5000 多個 tame 圖案件的逐一搜查令

延伸閱讀：Hales et al., "A Formal Proof of the Kepler Conjecture"（Forum of Mathematics, Pi，2017）；Hales "A Proof of the Kepler Conjecture"（Annals of Mathematics，2005）。