電腦輔助的「最長數學證明」誕生：文件大小達200TB
三位分別來自美國德克薩斯大学奥斯汀分校（The University of Texas at Austin）、肯塔基大學（University of Kentucky）和英國史雲斯大學（Swansea University）的電腦科學家近日在一篇論文中宣布：在德克薩斯先進計算中心（Texas Advanced Computing Center）超級電腦 Stampede 的幫助下，他們解決了著名的「布爾畢氏三元數問題」（Boolean Pythagorean triples problem）。
這個並不「優雅」的電腦輔助性證明，產生的文件大小達到200 TB——相當於美國國會圖書館所有數字化資料的總和，這也是人類迄今得到的最「長」的一個數學「證明」。
布爾畢氏三元數問題最早由美國數學家 Ronald Graham 在1980年代提出，其數學表述十分簡單：能否將正整數集合 N = { 1, 2, 3, 4,… } 中的每個數字分別以藍色或紅色染色，使得滿足畢達哥拉斯方程（即勾股定理）a^2 + b^2 = c^2 的任意三個數 a，b 和 c 不是同一種顏色？例如，對於滿足方程的3，4和5，若3和4是藍色，那麼5就必須是紅色。
顯而易見，如果這一問題的答案是肯定的，我們只需要知道數字的染色方式即可；而如果答案是否定的，那麼就必須給出一個證明。Ronald Graham 甚至為這個問題懸賞100美元，但經過三十餘年，直到上述電腦輔助性證明被公布後，他才終於給三位電腦科學家之一的 Marijn Heule 寄去了支票。
我們利用分塊攻克策略（Cube and Conquer）求解及驗證了布爾畢氏三元數問題……一個根本性的疑問是，它是否存在一個（人類可讀的）數學證明，還是只能通過電腦輔助判斷的方法來解決？
與純數學證明思路不同的是，三位電腦科學家利用對稱性和數論中的技巧，將需要交給電腦計算的可能染色方法減少到1萬億以內，然後利用 Stampede 的800個核心進行並行計算。在連續運算了大約2天的時間後，他們最終證明，正整數集合 N = { 1, 2,…, 7824 } 可以滿足問題的條件，但增加到7825（以及更大的數）時就不行——這意味着他們對布爾畢氏三元數問題給出了一個否定的答案。
不過，電腦不能解釋出“7825”這個數字有什麼特殊的意義，並且人類無法閱讀它給出的「證明」，這也是電腦輔助數學證明長久以來在哲學上帶給人們的困惑。
世界上第一個被電腦證明的著名數學定理是「四色定理」，它的通俗表述也很簡單：每個（無飛地的）地圖只需要不多於四種顏色來染色，以區分任意兩個鄰接的地區。這一原本被稱為「四色猜想」的問題最早由一位英國製圖員於1852年提出，但數學家在上百年內一直未找到答案。直到1976年，美國數學家 Kenneth Appel 和 德國數學家 Wolfgang Haken 才藉助電腦首次得到證明，將「四色猜想」變為「四色定理」。
這個證明最初並不被一些數學家所接受，因為他們認為其無法被人類直接驗證。隨着近年來計算技術的發展，電腦輔助證明越來越多地出現，數學界對其接受程度也有所提高，但仍有數學家希望能夠找到對這些問題更為簡潔或完全「人工」的證明。
需要指出的是，並非所有的電腦輔助證明都「不可讀」。在四色定理被電腦證明的同一年，中國結束長達十年的「文化大革命」，著名數學家吳文俊得以開展關於幾何定理自動證明的研究，並於1977年提出「吳特征列方法」。在此基礎之上，電腦科學家、數學家張景中於1992年提出基於幾何不變量的「消點法」，並與周咸青、高小山合作完善電腦程式，自動推理出大量非平凡的幾何定理，而且電腦生成的證明過程簡潔易讀，這被認為是電腦證明領域的一大突破。
聲音
計算機在像物理那樣的經驗科學中的作用早已被廣泛認可，一篇物理論文哪怕全部演算都靠計算機，也不會引起非議。數學卻不同，它對嚴謹性的要求在物理之上，結果則不像物理那樣受觀測檢驗， 因此特別注重推理的步驟。
如果四色問題有一個不依賴電腦的證明，我會更加開心，但我也願意接受阿佩爾和哈肯的證明——誰叫我們別無選擇呢？
為什麼窮舉證明越來越多？Simply because we can. 新工具的發明被用來解決之前解決不了的問題很正常……計算機是新的工具毋庸置疑，但是一個不提供新的抽象能力的工具，能發揮到底多大的作用是很值得懷疑的。一個值得注意的事實是：即使是做理論計算機或者計算機偏理論方向的人，幾乎都不會用計算機來輔助自己的研究，而是只依賴紙和筆的。
沒有留言:
張貼留言