破解數學難題，計算機可靠嗎？

最近,美國史丹佛大學、卡內基-梅隆大學和羅切斯特理工學院的科學家澈底破解了一個被稱為凱勒猜想的數學難題。凱勒猜想是一個已存在了90年之久的謎題，它與不同空間維度上的密鋪問題有關。科學家直接將這個數學難題轉化成了對10億個結果進行「暴力搜索」；他們把相關代碼輸入40臺計算機組成的計算集群，30分鐘後，計算機給出了一個200GB大小的證明結果：凱勒猜想在不超過7維的空間上都是正確的。

計算機是20世紀最先進的科學技術發明之一，對人類的生產活動和社會活動產生了極其重大的影響，成為資訊社會中必不可少的重要工具。在當今互聯網時代，計算機已經應用於幾乎所有的領域，數學當然也不例外。目前，許多科學家正在藉助計算機來解決數學難題，相信不久的將來這方面將會有更多突破。

藉助計算機來解決數學難題，是很值得人們關注的。而計算機的應用，既改變了數學研究的方法，也提高了數學研究的效率。眾所周知,數學是一切現代科學的基礎，尤其是計算機科學的基礎理論；回顧計算機發展史,其中的每一次飛躍都離不開數學的貢獻。有趣的是，計算機的出現反過來給予人們另外一種探索數學規律的手段。

計算機的發明，是為計算而來，而計算能力始終是計算機的根本。計算機的介入，擴展了數學研究的領域，促進了計算數學的發展。尤其是運算量極其龐大的數學問題，大多數情況只能藉助計算機來解決。例如，四色問題、E8結構、費克特問題、開普勒猜想、凱勒猜想、埃爾德什差異問題、畢氏三元數問題、x^3+y^3+z^3=k方程等著名數學難題，都是藉助計算機來破解的。

從上世紀50年代中期起，數學家開始用計算機進行證明定理的嘗試。當年英國哲學家及數學家伯特蘭·羅素教授經年累月在《數學原理》一書中證明的定理,美籍中國數理邏輯學家王浩教授在1959年只用了9分鐘機器時間就證明瞭其中350條以上,當時引起了轟動,以致通常把1959年稱為機器證明的元年。藉助計算機來解決數學難題還可以改變了人們對數學以往的認識，產生了新的方法，發展了新的領域。

日前，美國微軟公司的研究人員嘗試藉助計算機，尤其是人工智慧進行自動定理證明：對數學中提出的定理或猜想，尋找一種證明或反證的方法；該方法不僅能根據假設進行演繹，還要有一定的判定技巧。他們的目標是讓計算機系統Lean參加國際奧數競賽（IMO），因為在2021年Lean可能也會加入這場金牌爭奪戰中，成為一名「種子選手」。

此外，當今的大素數只能藉助計算機來探究。例如，2018年美國一名數學愛好者就藉助計算機並通過一個名為「因特網梅森素數大搜索」(GIMPS)項目，成功發現了第51個梅森素數——2^82589933-1(即2的82589933次方減1)；該數有24862048位，是迄今為止人類發現的最大素數。如果用普通字號將它列印下來，其長度將超過100公里！

也許有人會問：藉助計算機破解數學難題，這樣「正確」的證明，還算不算是「數學」？由於數據的絕對量過於龐大，以至於沒有辦法由人工進行驗證，那麼這種證明能否被驗證真偽？如果數學家的工作是通過理論幫助人類更好地理解數學，那通過窮舉來解決問題的計算機究竟有什麼存在的意義？其實相對於傳統數學，新潮數學已經悄然出現，這種新潮數學最明顯的標誌就是邏輯推理加入計算機輔助運算，二者合併起來對數學難題進行破解。

也許我們只能希望早日有人能用傳統方式給出數學問題的邏輯推理。例如，2014年，英國計算機專家阿列克謝·利什特沙博士和鮑里斯·科涅夫博士藉助超級計算機證明瞭埃爾德什差異問題，其運算數據量達13GB之多。一年後，美國加州大學洛杉磯分校數學家陶哲軒教授就用傳統方式成功破解了這一難題，此事震動了全球數學界。藉助計算機破解數學難題，看來還是可靠的。

不過絕大部分複雜的數學問題，可能需要新的數學工具，甚至新的數學概念來解決；這些都是當前計算機無法完成的，因為目前的計算機不具備「自主意識」，也不具備真正能推理和解決深度問題的能力。但是也有例外，近代數學的三大難題之一的四色問題，目前就是計算機基本完成證明的，但關於染色數和圖結構的問題並沒有得到解決；而且這個用到計算機的證明，剛好能用窮舉法解決。這只是在數量上取得了成功，還沒有完成四色問題的邏輯證明。

美籍波蘭數學家斯塔尼斯拉夫·烏拉姆教授在1976年出版的《一個數學家的奇遇》一書中指出，展望將來會出現一個數學研究的新時代，那時候計算機將成為數學研究的不可缺少的工具。他認為，數學問題將會以遊戲的形式提出來,然後由計算機來玩這些遊戲，並證明什麼東西能成立，什麼東西不能成立。據他看來，這種數學 研究的新方式，會使數學家們能夠重新在一起進行思想交流。

計算機目前成為數學研究的有效工具已是大勢所趨，不可阻擋。正如中國科學家及未來學家周海中教授在1993年發表的經典論文《21世紀數學展望》中所言：計算機在數學研究中發揮的作用將越來越大；藉助計算機解決數學問題將激勵人們去尋求更好、更簡單的方法，也加深人們對數學本質特徵的認識，還推動以計算機為基礎的人工智慧發展。毫無疑問，在計算機的助力下，破解數學難題的成果今後會越來越多。

文/宋良(作者單位：新加坡南洋理工大學理學院)