有史以來最大的數學證明:資料多達200TB

類別: 新奇

有史以來最大的數學證明:資料多達200TB
(University of Texas)

德克薩斯大學的三位電腦科學家宣佈他們完成了世界上最大的數學證明:完整證明有200TB大小。公開供人檢驗的部分壓縮後也有68GB大。

目前已經有很多數學家使用計算機輔助證明數學問題,但這個200TB大小的證明還是讓數學家們吃了一驚。UCSD的數學家Ronald Graham表示,在此之前,世界上最大的數學證明是關於一個離散數學的問題,只有13GB大。

這幾位電腦科學家解決的問題有著近一個世紀的歷史,是拉姆齊定理中的舒爾平方數定理,也被稱為布林-畢達哥拉斯三元數問題(Boolean Pythagorean triples problem)。該問題在1917年由舒爾提出,問的是:能否將所有正整數分成兩個部分,其中所有畢達哥拉斯三元陣列(即滿足a^2+b^2=c^2的a, b, c三個數)都不處於同一部分?否則,最小的反例是什麼?

該類問題常被轉化為著色問題來解決。比如如果3和5被用紅色標記,那麼4必需用藍色標記。研究者發現,從1到7824的所有正整數都能被用這種方式歸類。

有史以來最大的數學證明:資料多達200TB

在這7824個方格中,沒有任何滿足a^2+b^2=c^2的三個數同為藍色或同為紅色。(白色數字不屬於畢達哥拉斯三元數。)

在Marijn Heule,Oliver Kullmann和Victor Marek三人發表在arXiv上的這篇論文裡,他們把該問題拆分稱了兩個SAT可滿足性問題,然後發現該問題達到 {1,…,7825} 時無解,最後展示了自己給7824個方格上色的方法。

有史以來最大的數學證明:資料多達200TB

有關拉姆齊定理的設想往往涉及著巨量的資料,這個問題更不例外。在有這麼多數字的情況下,給方格上色的可能方案達到了10^2300那麼多。但研究者藉助了對稱分析等技法,讓電腦只需要檢查10^12種可能方案。德克薩斯大學的Stampede超級計算機的800臺處理器共同連續運轉了兩天兩夜才完成了計算。

雖然計算機已經解決了這個布林-畢達哥拉斯三元數問題,但它並沒有告訴我們為什麼到了7825時問題就變得無解。這反映了電腦輔助證明中的一個常見的思想挑戰:這樣“正確”的證明,還算不算是“數學”?如果數學家的工作是通過理論幫助人類更好地理解數學,那通過窮舉來解決問題的計算機究竟有什麼存在的意義?

或許我們只能希望早日有人給出這個問題的邏輯推理。那個為解決埃爾德什差異問題(Erdős discrepancy problem)的13GB證明提出後僅過了一年,UCLA數學家陶哲軒(相關蛋文:《當今在世的智商最高的十位天才》)就用傳統方式成功破解了這一難題,真正震動了全球數學界。

[zzjeff via Nature & UT Austin]

有史以來最大的數學證明:資料多達200TB原文請看這裡

推薦文章