輔助證明軟件能解決數(shù)學研究前沿的抽象理論問題，它們或?qū)⒃跀?shù)學中發(fā)揮更重要的作用。

撰文?|?Davide Castelvecchi

翻譯?|?施普林格·自然上海辦公室

Peter Scholze希望能夠從一個基礎理論開始，重構(gòu)現(xiàn)代數(shù)學的許多內(nèi)容。如今，Scholze構(gòu)想的核心理論之一獲得了意料之外的驗證者：計算機。

盡管大部分數(shù)學家認為，他們工作的創(chuàng)造性方面在短期內(nèi)不太可能被機器取代。但有些數(shù)學家承認，技術將在他們的研究中扮演日益重要的角色。而此次成功實踐可能成為數(shù)學家開始接納計算機輔助的轉(zhuǎn)折點。

計算機成功驗證了一個復雜的數(shù)學證明丨來源：Fadel Senna/ AFP via Getty

Scholze是德國波恩大學的數(shù)論學家。2019年，他與哥本哈根大學的Dustin Clausen一起，在波恩大學舉辦了一系列講座，期間他們提出了一個雄心勃勃的計劃——“凝聚態(tài)數(shù)學”（condensed mathematics）。他們表示，凝聚態(tài)數(shù)學將為從幾何到數(shù)論的各個領域注入全新的理解，并在各領域間建立起聯(lián)系。

其他學者對此頗為關注：Scholze被認為是數(shù)學界最耀眼的明星之一，曾提出過一些革命性的概念?；羝战鹚勾髮W的數(shù)學家Emily Riehl認為，如果Scholze和Clausen的構(gòu)想得以實現(xiàn)，50年后研究生的數(shù)學教學方式將與今天截然不同?！拔艺J為，許多數(shù)學領域在將來都會受到他的觀點影響?！彼f。

Peter Scholze，以算術代數(shù)幾何而聞名的德國數(shù)學家。因“在代數(shù)幾何學中發(fā)起的革命”，獲得2018年菲爾茲獎，成為最年輕的菲爾茲獎得主之一。圖片來源：https://www.quantamagazine.org

當時Scholze和Clausen大部分的構(gòu)想都停留在一個十分復雜的數(shù)學證明上。證明過程是如此復雜，甚至連他們自己也不確定是否正確。但2021年6月的早些時候Scholze宣布，專用計算機軟件幫助他成功檢驗了證明的核心部分。

計算機輔助

數(shù)學家使用計算機進行數(shù)值計算或者處理復雜方程已有很長時間。通過讓計算機進行大量重復運算，他們已經(jīng)證明了一些重要結(jié)論——最著名的例子便是上世紀70年代證明四色定理（只用四種顏色，就在任意地圖上給任意兩個相鄰的國家著上不同的顏色）。

然而，一種稱為證明助手（proof assistant）的系統(tǒng)功能更為深入。用戶基于系統(tǒng)已知的簡單對象，輸入命題來使系統(tǒng)理解數(shù)學概念（一個對象）的定義。輸入的命題可以只涉及已知對象，證明助手則會基于它現(xiàn)有的知識來判斷該命題是“明顯”正確或錯誤。如果證明助手的回答是不“明顯”，用戶則需要輸入更多的信息來訓練它。證明助手借此迫使用戶更加嚴密地展開他們的論證邏輯，并填補數(shù)學家們有意無意省略的一些較簡單步驟。
一旦研究人員完成了前期繁重的訓練工作，使證明助手理解了一系列數(shù)學概念，系統(tǒng)就會生成一個計算機代碼庫。其他研究人員可以以此為基礎進行研究，并定義更高級的數(shù)學對象。由此，證明助手就能夠幫助檢驗那些耗時費力，甚至是人力所不可及的數(shù)學證明。
證明助手一直都不乏擁護者，但這是它首次在領域前沿發(fā)揮重要作用，帝國理工學院的數(shù)學家Kevin Buzzard說。他參與檢驗了Scholze和Clausen的研究結(jié)果。“之前遺留下來的一個重要問題是：證明助手能否處理復雜的數(shù)學問題？”Buzzard說?！拔覀冏C明了它們可以?！?/span>
而且這一切來得太快，超乎任何人的想象。2020年12月，Scholze向證明助手領域的專家們尋求幫助。德國弗賴堡大學的數(shù)學家Johan Commelin帶領一隊志愿者開始著手解決這一難題。五個多月后的2021年6月5日，Scholze就在Buzzard的博客中宣布，實驗主體部分已經(jīng)成功。“這簡直不可思議。交互式證明助手現(xiàn)在已經(jīng)達到了如此的高度：它能在合理時間內(nèi)邏輯完備地驗證復雜的原創(chuàng)研究。”Scholze寫道。
Scholze和Clausen指出，凝聚態(tài)數(shù)學的關鍵在于重新定義現(xiàn)代數(shù)學的基石之一——拓撲（topology）的概念。數(shù)學家們研究的很多對象都具有拓撲。拓撲是對象的一種結(jié)構(gòu)，它決定對象的哪些部分相連，哪些不是。拓撲提供了形狀的信息，但是比起我們所熟悉的經(jīng)典幾何，拓撲更具延展性：在拓撲中，任意不分割對象的變換都是允許的。比如，一個三角形在拓撲上等價于其他任意三角形，甚至等價于圓形，但是無法等價于一條直線。
拓撲不僅在幾何學，而且在泛函分析（functional analysis；一門研究函數(shù)的學科）中也發(fā)揮關鍵作用。函數(shù)空間通常是無窮維的（例如量子力學中基礎的波函數(shù)）。另外，拓撲對于p進數(shù)（p-adic number）系統(tǒng)也非常重要，其具有一種與眾不同的“分形”拓撲。

現(xiàn)代數(shù)學的大統(tǒng)一

2018年前后，Scholze和Clausen開始意識到，傳統(tǒng)的拓撲定義方法導致了幾何學、泛函分析和p進數(shù)三個數(shù)學領域之間存在兼容性問題，但新的基礎概念或能彌合這些缺口。這三個領域明顯各自處理的是截然不同的概念，但似乎會出現(xiàn)與另外兩個領域中可類比的結(jié)果。兩位學者提出，一旦拓撲能被“正確”定義，不同領域之間的相似結(jié)果就成了同一個“凝聚態(tài)數(shù)學”中的各個實例。這是三個領域的“某種大統(tǒng)一”，Clausen說。

Scholze和Clausen稱，他們已經(jīng)就一些重要幾何事實發(fā)現(xiàn)了一些更簡單、“凝聚”的證明，而且還能夠證明一些之前未知的定理。這些研究尚未公之于眾。
但還有一個問題。在納入幾何學之前，Scholze和Clausen還需要證明一個關于普通實數(shù)集直線拓撲結(jié)構(gòu)的高度技術性的定理。Commelin解釋說，“這像是一個基礎定理，能將實數(shù)納入這個新框架?！?/span>

用戶基于證明助手包Lean中已有的較簡單命題和概念，輸入數(shù)學命題。在Scholze和Clausen的工作中，Lean輸出了一個復雜的網(wǎng)絡。圖中各個命題被標注了不同的顏色并按照數(shù)學中的子領域分組。丨來源：Patrick Massot

Clausen回憶說，Scholze堅持不懈、夜以繼日地工作，最終“憑借強大的意志”完成證明，在此過程中誕生了許多原創(chuàng)想法?！斑@是我見過的最驚人的數(shù)學成就?！彼f。但是整個論證過于復雜，就連Scholze自己也擔心有什么細微漏洞導致功虧一簣。“論證看起來很可信，但實在太過新穎?！盋lausen說。
為了檢查自己的工作，Scholze向數(shù)論學家Buzzard求助。Buzzard是助手軟件包Lean的專家。Lean起初由微軟研究院的一位計算機科學家發(fā)明，用于嚴格檢查計算機代碼中的錯誤。
Buzzard曾負責過一個為期數(shù)年的項目，項目內(nèi)容是將帝國理工的所有本科數(shù)學課程編入Lean。他也曾試過將更高級的數(shù)學編入Lean，例如狀似完備空間（perfectoid space）的概念。Scholze正是憑借這個理論贏得了2018年的菲爾茲獎。
另一位數(shù)論學家Commelin帶隊驗證了Scholze和Clausen的證明。Commelin和Scholze決定將他們的Lean項目取名為“液體張力實驗”（Liquid Tensor Experiment），以此向前衛(wèi)搖滾樂隊Liquid Tension Experiment致敬，因為他倆都是這個樂隊的粉絲。
一場線上合作就此熱火朝天地展開了。十多位精通Lean的數(shù)學家加入團隊，研究人員還得到了計算機科學家們的協(xié)助。到六月初，這個團隊已經(jīng)將Scholze證明的核心部分（也是他最沒有把握的部分）全部轉(zhuǎn)譯成了Lean代碼。證明全部得以檢驗！該軟件的確具有檢驗這部分數(shù)學證明的能力。

加深理解

Lean版本的Scholze的證明由成千上萬行的代碼組成，比原始版本長100多倍，Commelin說道?！叭绻麊螁慰碙ean的代碼，尤其是當前版本的代碼，你很難理解Scholze的證明?！钡茄芯空邆冋f，將證明轉(zhuǎn)換為代碼在計算機里運行的整個過程，同樣加深了他們對Scholze的證明的理解。

Riehl是試用過證明助手的數(shù)學家之一，她甚至在一些本科課程中教授相關內(nèi)容。她說，雖然她沒有在自己的研究中系統(tǒng)地使用這些工具，但是它們已經(jīng)開始改變她的思考方式，關于如何構(gòu)建數(shù)學概念、以及呈現(xiàn)和證明相關定理的做法?！耙郧拔矣X得證明和構(gòu)建是兩碼事，但現(xiàn)在我認為它們是一樣的。”
許多學者認為，短期內(nèi)機器并不能代替數(shù)學家。證明助手讀不懂數(shù)學課本，需要人類的持續(xù)輸入，也不知道一個數(shù)學命題是否有趣或重要，它們只能判斷命題正確與否，Buzzard說。但他補充說盡管如此，計算機或許馬上就能夠通過已知事實推導出被數(shù)學家們所忽視的結(jié)論了。
Scholze驚訝于證明助手的能力，但他不確定它們是否會繼續(xù)在自己的研究中扮演重要角色?！澳壳翱磥恚也⒉磺宄鼈儗ξ易鳛閿?shù)學家的創(chuàng)造性工作會有什么幫助?！?/span>

本文經(jīng)授權(quán)轉(zhuǎn)載自微信公眾號“Nature Portfolio”。原文以Mathematicians welcome computer-assisted proof in ‘grand unification’ theory為標題發(fā)表在2021年6月18日《自然》的新聞版塊上。原文鏈接：https://www.nature.com/articles/d41586-021-01627-2?utm_source=wechat&utm_medium=social&utm_campaign=CONR_AUTCC_ENGM_CN_CNCM_NFHCN