開普勒猜想

1611 年，開普勒提出，密堆積（立方密堆積或六方密堆積，兩者的最大密度均為）是可能的最高密度球體堆積，這一論斷被稱為開普勒猜想。 尋找最密（不一定是週期性的）球體堆積被稱為開普勒問題。

巴克敏斯特·富勒（Buckminster Fuller，1975 年）聲稱擁有一個證明，但那實際上是對面心立方堆積的描述，而不是對其最優性的證明（Sloane 1998）。 W.-Y. Hsiang（Cipra 1991，Hsiang 1992，1993，Cipra 1993）提出了第二個所謂的開普勒猜想證明，但隨後被確定為有缺陷的（Conway等人1994，Hales 1994，Sloane 1998）。 J. H. Conway 認為，任何讀過 Hsiang 證明的人都不會懷疑其有效性：那是胡說八道。

此後不久，Hales（1997a）發表了一份詳細的計劃，描述瞭如何使用與早期嘗試顯著不同的方法，並廣泛使用計算機計算來證明開普勒猜想。 Hales 隨後完成了一個完整的證明，該證明發表在一系列總計超過 250 頁的論文中（Cipra 1998）。 Hales（2002）發表了對該證明的通俗概述。 該證明廣泛依賴於全域性最佳化、線性規劃和區間算術理論的方法。 包含組合數學、區間算術和線性規劃的計算機程式碼和資料檔案的計算機檔案需要超過 3 GB 的儲存空間。

Hales 的證明被證實難以驗證。 2003 年，據報道，《數學年刊》的出版物將有一份不尋常的編輯註釋，指出儘管一個由 12 名審稿人組成的團隊花了四年多的時間來驗證該證明，並且審稿人有 99% 的把握認為它是正確的，但該論文的部分內容仍然無法檢查（Holden 2003，Szpiro 2003）。 然而，實際出版物中沒有這樣的註釋（Hales 2005）。

為了回應驗證其證明的困難，2003 年 1 月，Hales 發起了“Flyspeck 專案”（“開普勒的形式證明”），試圖使用計算機自動驗證證明的每個步驟。 該專案最初由 Hales 認為需要 20 人年的勞動（Holden 2003，Szpiro 2003），於 2014 年完成。