數學的電腦證明
撰文｜賴加翌
●數學家艾卡德的趣聞
有個叫艾卡德 （Shalosh B. Ekhad） 的數學家發表了幾十篇論文，有一些是艾卡德自己獨立署名，另一些是艾卡德和羅格斯大學的數學家齊伯格聯合署名。 但在任何大學的教職員名單上都找不到艾卡德的名子，因為他並不是一個人， 而是一台電腦。齊伯格說自己是艾卡德的「導師」，其實艾卡德是齊伯格操作的一台電腦。
為電腦命名的現象聽起來很有趣，但它的確是具有這個時代的象徵意義。 因為它的「導師」齊伯格堅持讓計算機獨立署名， 是為了顯示它在數學中越來越高的重要性。以下介紹幾個近代用電腦完成的著名數學證明：
●布爾畢氏三元數
數學家 Ronald Graham 在1980年代提出布爾畢達哥拉斯三元數問題：是否可以將正整數集合 N＝｛ 1，2，3，… ｝裡面的數字用藍色或紅色著色，使任意滿足畢達哥拉斯方程式a^2 ＋ b^2 ＝ c^2 的三個數必然包含兩種顏色？也就是說，這三個數不是全部藍色，也不是全部紅色，其中一個跟另外兩個的顏色不同。
經過三十多年，三位電腦科學家利用德克薩斯先進計算中心的超級電腦輔助，解決了這個問題。這個電腦證明文件一發布就被稱為「史上最長的數學證明」，檔案大小有200TB，比美國國會圖書館數字化資料的總和還多。如果每個硬碟有2TB，就需要100個硬碟才裝得完，因此無法把完整的證明放在網絡上。他們只把運算所需的檔案壓縮成68GB後公開，讓學界自行下載。
這三位電腦科學家用對稱性和數論方法，把可能的染色情況減到1萬億種，再用800核心的超級電腦連續運算了兩天，證明了正整數集合N ＝｛ 1， 2，…， 7824 ｝可以滿足布爾畢達哥拉斯三元數問題，但數字到了7825以上時，就總會有同一顏色的三個數字a、b及c滿足方程a^2 ＋ b^2 ＝ c^2。但電腦不能解釋數字7825代表的意義，只能讓人頭腦放空地接受這個結果，好像在告訴你：「事情就是這樣，沒有為什麼。」
●克卜勒猜想
天文學家約翰尼斯·克卜勒提出的克卜勒猜想認為，在三維歐幾里德空間裡，每個球大小相同的狀況下，沒有任何裝球方式的「密度」比面心立方與六方最密堆積要高。也就是說，這個猜想認為雜貨店堆柳丁的方式是最省空間的，因為留下的空隙最小。
1998年，托馬斯·黑爾斯用窮舉法證明這個猜想，論文裡面大量使用電腦程式運算。黑爾斯宣告證明成功之後，幾乎被所有的報紙報導了出來，但他投稿的《數學年刊》審稿者卻認為這個證明缺乏可驗證的程序，因此在文章中附上罕見的編輯附註：這篇論文的部分內容無法審查。
●四色定理
世界上第一個用電腦證明的著名數學問題是「四色定理」：在沒有飛地的地圖上，只需要不多於四種顏色來著色，使任意兩個相接的地區顏色都不同。「四色定理」本來被稱作「四色猜想」，由英國數學家法蘭西斯·古德里於1852年提出，上百年來有許多人發表證明或反例，都被證實是錯誤的。到了1976年，數學家凱尼斯·阿佩爾和沃夫岡·哈肯藉由電腦首次得到一個完全的證明，於是「四色猜想」就成為「四色定理」。
這個證明一開始不被許多數學家接受，因為它無法用人來驗證。但隨著電腦技術的運用越來越廣泛，電腦輔助證明出現率變高，數學界對其接受程度也越來越進步，但仍有數學家希望能夠找到更簡單的證明。
●電腦證明的趨勢
除了上面列出的三個有名的例子，E8結構、Fekete問題等著名數學難題都是借助電腦來證明的。對於運算量非常大的數學問題，通常都需要電腦的幫忙，電子計算機已經成為數學研究不可或缺的輔助工具。但還是有些數學家認為電子計算機證明的檔案過於龐大，無法用人工進行檢驗，因此很難接受電腦證明的正確性。
另一方面，數學家總是形容一些獨特的證明方法很「優美」，這種情況通常是指一些極短的證明，或是由意外的方式推導出的證明，也就是從一些表面上無關的定理證明出另一結論。而用電腦證明被認為是「暴力」解法，或許和優美的證明永遠扯不上邊。普林斯頓大學康威教授說﹕「我不喜歡它們，因為不知道究竟發生了什麼。」然而數學家保羅。艾狄胥卻說﹕「如果四色問題有一個不依賴電腦的證明，我會更加開心，但我也願意接受阿佩爾和哈肯的證明——誰叫我們別無選擇呢？」
參考資料：
- Lamb, Evelyn, Two-hundred-terabyte maths proof is largest ever. Nature, 534, 17–18. 2016
- Marijn J. H. Heule, Oliver Kullmann, &Victor W. Marek, Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. Cornell University Library. 2016
- V. Vilfred, The Four Color Theorem - A New Proof by Induction. Cornell University Library. 2017
- Marianne Freiberger, Why we want proof. +plus magzine. 2015
