數學家喜迎“大統一”理論的計算機輔助證明
原文作者：Davide Castelvecchi
輔助證明軟件能解決數學研究前沿的抽象理論問題，它們或将在數學中發揮更重要的作用。
Peter Scholz希望能夠從一個基礎理論開始，重構現代數學的許多内容。如今，Scholz構想的核心理論之一獲得了意料之外的驗證者：計算機。
盡管大部分數學家認為，他們工作的創造性方面在短期内不太可能被機器取代。但有些數學家承認，技術将在他們的研究中扮演日益重要的角色。而此次成功實踐可能成為數學家開始接納計算機輔助的轉折點。
計算機成功驗證了一個複雜的數學證明。
Scholze是德國波恩大學的數論學家。2019年，他與哥本哈根大學的Dustin Clausen一起，在波恩大學舉辦了一系列講座，期間他們提出了一個雄心勃勃的計劃——“凝聚态數學”（condensed mathematics）。他們表示，凝聚态數學将為從幾何到數論的各個領域注入全新的理解，并在各領域間建立起聯系。
其他學者對此頗為關注：Scholze被認為是數學界最耀眼的明星之一，曾提出過一些革命性的概念。霍普金斯大學的數學家Emily Riehl認為，如果Scholze和Clausen的構想得以實現，50年後研究生的數學教學方式将與今天截然不同。“我認為，許多數學領域在将來都會受到他的觀點影響。”她說。 Peter Scholze，以算術代數幾何而聞名的德國數學家。因“在代數幾何學中發起的革命”，獲得2018年菲爾茲獎，成為最年輕的菲爾茲獎得主之一。圖片來源：https://www.quantamagazine.org當時Scholze和Clausen大部分的構想都停留在一個十分複雜的數學證明上。證明過程是如此複雜，甚至連他們自己也不确定是否正确。但2021年6月的早些時候Scholze宣布，專用計算機軟件幫助他成功檢驗了證明的核心部分。
計算機輔助
數學家使用計算機進行數值計算或者處理複雜方程已有很長時間。通過讓計算機進行大量重複運算，他們已經證明了一些重要結論——最著名的例子便是上世紀70年代證明四色定理（隻用四種顔色，就在任意地圖上給任意兩個相鄰的國家着上不同的顔色）。
然而，一種稱為證明助手（proof assistant）的系統功能更為深入。用戶基于系統已知的簡單對象，輸入命題來使系統理解數學概念（一個對象）的定義。輸入的命題可以隻涉及已知對象，證明助手則會基于它現有的知識來判斷該命題是“明顯”正确或錯誤。如果證明助手的回答是不“明顯”，用戶則需要輸入更多的信息來訓練它。證明助手借此迫使用戶更加嚴密地展開他們的論證邏輯，并填補數學家們有意無意省略的一些較簡單步驟。
一旦研究人員完成了前期繁重的訓練工作，使證明助手理解了一系列數學概念，系統就會生成一個計算機代碼庫。其他研究人員可以以此為基礎進行研究，并定義更高級的數學對象。由此，證明助手就能夠幫助檢驗那些耗時費力，甚至是人力所不可及的數學證明。
證明助手一直都不乏擁護者，但這是它首次在領域前沿發揮重要作用，帝國理工學院的數學家Kevin Buzzard說。他參與檢驗了Scholze和Clausen的研究結果。“之前遺留下來的一個重要問題是：證明助手能否處理複雜的數學問題？”Buzzard說。“我們證明了它們可以。”
而且這一切來得太快，超乎任何人的想象。2020年12月，Scholze向證明助手領域的專家們尋求幫助。德國弗賴堡大學的數學家Johan Commelin帶領一隊志願者開始着手解決這一難題。五個多月後的2021年6月5日，Scholze就在Buzzard的博客中宣布，實驗主體部分已經成功。“這簡直不可思議。交互式證明助手現在已經達到了如此的高度：它能在合理時間内邏輯完備地驗證複雜的原創研究。”Scholze寫道。
Scholze和Clausen指出，凝聚态數學的關鍵在于重新定義現代數學的基石之一——拓撲（topology）的概念。數學家們研究的很多對象都具有拓撲。拓撲是對象的一種結構，它決定對象的哪些部分相連，哪些不是。拓撲提供了形狀的信息，但是比起我們所熟悉的經典幾何，拓撲更具延展性：在拓撲中，任意不分割對象的變換都是允許的。比如，一個三角形在拓撲上等價于其他任意三角形，甚至等價于圓形，但是無法等價于一條直線。
拓撲不僅在幾何學，而且在泛函分析（functional analysis；一門研究函數的學科）中也發揮關鍵作用。函數空間通常是無窮維的（例如量子力學中基礎的波函數）。另外，拓撲對于p進數（p-adic number）系統也非常重要，其具有一種與衆不同的“分形”拓撲。
現代數學的大統一
2018年前後，Scholze和Clausen開始意識到，傳統的拓撲定義方法導緻了幾何學、泛函分析和p進數三個數學領域之間存在兼容性問題，但新的基礎概念或能彌合這些缺口。這三個領域明顯各自處理的是截然不同的概念，但似乎會出現與另外兩個領域中可類比的結果。兩位學者提出，一旦拓撲能被“正确”定義，不同領域之間的相似結果就成了同一個“凝聚态數學”中的各個實例。這是三個領域的“某種大統一”，Clausen說。
Scholze和Clausen稱，他們已經就一些重要幾何事實發現了一些更簡單、“凝聚”的證明，而且還能夠證明一些之前未知的定理。這些研究尚未公之于衆。
但還有一個問題。在納入幾何學之前，Scholze和Clausen還需要證明一個關于普通實數集直線拓撲結構的高度技術性的定理。Commelin解釋說，“這像是一個基礎定理，能将實數納入這個新框架。”
用戶基于證明助手包Lean中已有的較簡單命題和概念，輸入數學命題。在Scholze和Clausen的工作中，Lean輸出了一個複雜的網絡。圖中各個命題被标注了不同的顔色并按照數學中的子領域分組。來源：Patrick Massot
Clausen回憶說，Scholze堅持不懈、夜以繼日地工作，最終“憑借強大的意志”完成證明，在此過程中誕生了許多原創想法。“這是我見過的最驚人的數學成就。”他說。但是整個論證過于複雜，就連Scholze自己也擔心有什麼細微漏洞導緻功虧一篑。“論證看起來很可信，但實在太過新穎。”Clausen說。
為了檢查自己的工作，Scholze向數論學家Buzzard求助。Buzzard是助手軟件包Lean的專家。Lean起初由微軟研究院的一位計算機科學家發明，用于嚴格檢查計算機代碼中的錯誤。
Buzzard曾負責過一個為期數年的項目，項目内容是将帝國理工的所有本科數學課程編入Lean。他也曾試過将更高級的數學編入Lean，例如狀似完備空間（perfectoid space）的概念。Scholze正是憑借這個理論赢得了2018年的菲爾茲獎。
另一位數論學家Commelin帶隊驗證了Scholze和Clausen的證明。Commelin和Scholze決定将他們的Lean項目取名為“液體張力實驗”（Liquid Tensor Experiment），以此向前衛搖滾樂隊Liquid Tension Experiment緻敬，因為他倆都是這個樂隊的粉絲。
一場線上合作就此熱火朝天地展開了。十多位精通Lean的數學家加入團隊，研究人員還得到了計算機科學家們的協助。到六月初，這個團隊已經将Scholze證明的核心部分（也是他最沒有把握的部分）全部轉譯成了Lean代碼。證明全部得以檢驗！該軟件的确具有檢驗這部分數學證明的能力。
加深理解
Lean版本的Scholze的證明由成千上萬行的代碼組成，比原始版本長100多倍，Commelin說道。“如果單單看Lean的代碼，尤其是當前版本的代碼，你很難理解Scholze的證明。”但是研究者們說，将證明轉換為代碼在計算機裡運行的整個過程，同樣加深了他們對Scholze的證明的理解。
Riehl是試用過證明助手的數學家之一，她甚至在一些本科課程中教授相關内容。她說，雖然她沒有在自己的研究中系統地使用這些工具，但是它們已經開始改變她的思考方式，關于如何構建數學概念、以及呈現和證明相關定理的做法。“以前我覺得證明和構建是兩碼事，但現在我認為它們是一樣的。”
許多學者認為，短期内機器并不能代替數學家。證明助手讀不懂數學課本，需要人類的持續輸入，也不知道一個數學命題是否有趣或重要，它們隻能判斷命題正确與否，Buzzard說。但他補充說盡管如此，計算機或許馬上就能夠通過已知事實推導出被數學家們所忽視的結論了。
Scholze驚訝于證明助手的能力，但他不确定它們是否會繼續在自己的研究中扮演重要角色。“目前看來，我并不清楚它們對我作為數學家的創造性工作會有什麼幫助。”
原文以Mathematicians welcome computer-assisted proof in 'grand unification’ theory為标題發表在2021年6月18日《自然》的新聞版塊上
© nature
doi:10.1038/d41586-021-01627-2
最新文章
-
“豫西中醫界之泰鬥喬保均”治療疑難病60年經驗賞析
2小時前 -
回憶、健忘和灑脫
2小時前 -
弘一法師：“真的不忍心告訴你，這個世界隻是一個夢。你一輩子執
2小時前 -
心理學，準的讓你驚叫
2小時前 -
人生，成大器者有四識，知識、見識、膽識、遠識
3小時前 -
俞和：被遺忘的書法家，以古為師，創新在手！
3小時前 -
2024屆新高考II卷語文真題答案及解析
3小時前 -
生前隻是小人物，死後震驚史學界
3小時前
熱門文章
-
每日一誦傷寒論第241條
1周前 -
老張老李侃門球之140篇
1天前 -
這個穴位可以治療多種胃痛腹痛，還可以減肥
5天前 -
為什麼五點鐘要起床答案讓人吃驚！（現在知道還不晚）
1周前 -
治療坐骨神經痛藥酒５方
1周前 -
美麗中國-2870：中國最大的内陸河，塔裡木河
1天前 -
二十四山開門放水作竈真訣開門放水作竈直訣——子山
1天前 -
門球技巧 隻需五個字讓你打好門球
1天前
有話要說...