數學的電腦證明  

圖片出處: photo-ac.com

撰文|賴加翌

●數學家艾卡德的趣聞

有個叫艾卡德 (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問題等著名數學難題都是借助電腦來證明的。對於運算量非常大的數學問題,通常都需要電腦的幫忙,電子計算機已經成為數學研究不可或缺的輔助工具。但還是有些數學家認為電子計算機證明的檔案過於龐大,無法用人工進行檢驗,因此很難接受電腦證明的正確性。

另一方面,數學家總是形容一些獨特的證明方法很「優美」,這種情況通常是指一些極短的證明,或是由意外的方式推導出的證明,也就是從一些表面上無關的定理證明出另一結論。而用電腦證明被認為是「暴力」解法,或許和優美的證明永遠扯不上邊。普林斯頓大學康威教授說﹕「我不喜歡它們,因為不知道究竟發生了什麼。」然而數學家保羅。艾狄胥卻說﹕「如果四色問題有一個不依賴電腦的證明,我會更加開心,但我也願意接受阿佩爾和哈肯的證明——誰叫我們別無選擇呢?」

 

參考資料: 

  1. Lamb, Evelyn, Two-hundred-terabyte maths proof is largest ever. Nature, 534, 17–18. 2016
  2. 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
  3. V. Vilfred, The Four Color Theorem - A New Proof by Induction. Cornell University Library. 2017
  4. Marianne Freiberger, Why we want proof. +plus magzine. 2015

加入好友

2,171 人瀏覽過