| 作者 連 以婷 | 發布日期 2014 年 08 月 14 日 | 分類 科技教育 |
「如何在有限的空間堆放最多的球型物體？」德國天文學家克卜勒（Johannes Kepler）在 1611 年提出沒有任何一種堆疊方式比面心立方與六方最密堆積還要來得緊密，這兩種方式就如同現今市場中常見的堆水果法，上下層交錯排列，最後會堆成一座金字塔。雖然克卜勒提出解答，卻無法證明它，而他的答案也就成為後來有名的克卜勒猜想（Kepler conjecture），四百年來數學家前仆後繼想要解開，如今藉由一台電腦的幫忙，這道百年猜想終於被證實是真的。
（圖片來源：Wikipedia）
解開此猜想的數學家為匹茲堡大學的黑爾斯（Thomas Hales），曾在 1998 年以長達三百頁的論文篇幅提出證明，為了審查論證是否無誤，12 名審稿者花了四年的時間檢查，但最終只能肯定 99％ 是正確的，為此黑爾斯開發了一套計算工具，稱為「汙點計畫」（Flyspeck project），希望能將最後一哩路填補起來。
汙點計畫使用兩種形式驗證軟體（formal verification software），Isabelle 和 HOL Light，能夠以簡單、小片段的方式驗證一連串的邏輯語句，因此黑爾斯就可以藉由這兩套軟體，將所有論文中的邏輯語句完整地檢查一遍。
就在上週日，汙點計畫的小組宣布那份長達三百頁的論文已成功通過兩個軟體的審查，證實他之前所提出的論證為正確的，也就是說電腦證實四百年前克卜勒提出的猜想為真。黑爾斯在接受《新科學人》（New Scientist）的採訪表示：「我擺脫了肩頭上沉重的負擔，突然之間我好像年輕十歲。」
汙點計畫不僅為黑爾斯帶來好消息，同時也可幫數學家省下許多麻煩，有了 Isabelle 和 HOL Light 從旁協助，每年由數學家推導出來的密密麻麻數學證明，不再需要人腦逐條審查，只需要電腦就可以確認，而數學家能將更多心力放在解決其他問題上。
（首圖來源：Wikimedia Commons）
延伸閱讀：
全站熱搜
留言列表
