原文作者：Davide Castelvecchi

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

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

計算機成功驗證了一個復(fù)雜的數(shù)學(xué)證明。

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

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

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

然而，一種稱為證明助手（proof assistant）的系統(tǒng)功能更為深入。用戶基于系統(tǒng)已知的簡單對象，輸入命題來使系統(tǒng)理解數(shù)學(xué)概念（一個對象）的定義。輸入的命題可以只涉及已知對象，證明助手則會基于它現(xiàn)有的知識來判斷該命題是“明顯”正確或錯誤。如果證明助手的回答是不“明顯”，用戶則需要輸入更多的信息來訓(xùn)練它。證明助手借此迫使用戶更加嚴(yán)密地展開他們的論證邏輯，并填補數(shù)學(xué)家們有意無意省略的一些較簡單步驟。

一旦研究人員完成了前期繁重的訓(xùn)練工作，使證明助手理解了一系列數(shù)學(xué)概念，系統(tǒng)就會生成一個計算機代碼庫。其他研究人員可以以此為基礎(chǔ)進行研究，并定義更高級的數(shù)學(xué)對象。由此，證明助手就能夠幫助檢驗?zāi)切┖臅r費力，甚至是人力所不可及的數(shù)學(xué)證明。

證明助手一直都不乏擁護者，但這是它首次在領(lǐng)域前沿發(fā)揮重要作用，帝國理工學(xué)院的數(shù)學(xué)家Kevin Buzzard說。他參與檢驗了Scholze和Clausen的研究結(jié)果。“之前遺留下來的一個重要問題是：證明助手能否處理復(fù)雜的數(shù)學(xué)問題？”Buzzard說?！拔覀冏C明了它們可以?！?/p>

而且這一切來得太快，超乎任何人的想象。2020年12月，Scholze向證明助手領(lǐng)域的專家們尋求幫助。德國弗賴堡大學(xué)的數(shù)學(xué)家Johan Commelin帶領(lǐng)一隊志愿者開始著手解決這一難題。五個多月后的2021年6月5日，Scholze就在Buzzard的博客中宣布，實驗主體部分已經(jīng)成功。“這簡直不可思議。交互式證明助手現(xiàn)在已經(jīng)達到了如此的高度：它能在合理時間內(nèi)邏輯完備地驗證復(fù)雜的原創(chuàng)研究?！盨cholze寫道。

Scholze和Clausen指出，凝聚態(tài)數(shù)學(xué)的關(guān)鍵在于重新定義現(xiàn)代數(shù)學(xué)的基石之一——拓?fù)?span>（topology）的概念。數(shù)學(xué)家們研究的很多對象都具有拓?fù)洹Ｍ負(fù)涫菍ο蟮囊环N結(jié)構(gòu)，它決定對象的哪些部分相連，哪些不是。拓?fù)涮峁┝诵螤畹男畔ⅲ潜绕鹞覀兯煜さ慕?jīng)典幾何，拓?fù)涓哐诱剐裕涸谕負(fù)渲校我獠环指顚ο蟮淖儞Q都是允許的。比如，一個三角形在拓?fù)渖系葍r于其他任意三角形，甚至等價于圓形，但是無法等價于一條直線。

拓?fù)洳粌H在幾何學(xué)，而且在泛函分析（functional analysis；一門研究函數(shù)的學(xué)科）中也發(fā)揮關(guān)鍵作用。函數(shù)空間通常是無窮維的（例如量子力學(xué)中基礎(chǔ)的波函數(shù)）。另外，拓?fù)鋵τ?em>p進數(shù)（p-adic number）系統(tǒng)也非常重要，其具有一種與眾不同的“分形”拓?fù)洹?/p>

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

Scholze和Clausen稱，他們已經(jīng)就一些重要幾何事實發(fā)現(xiàn)了一些更簡單、“凝聚”的證明，而且還能夠證明一些之前未知的定理。這些研究尚未公之于眾。

但還有一個問題。在納入幾何學(xué)之前，Scholze和Clausen還需要證明一個關(guān)于普通實數(shù)集直線拓?fù)浣Y(jié)構(gòu)的高度技術(shù)性的定理。Commelin解釋說，“這像是一個基礎(chǔ)定理，能將實數(shù)納入這個新框架?！?/p>

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

Clausen回憶說，Scholze堅持不懈、夜以繼日地工作，最終“憑借強大的意志”完成證明，在此過程中誕生了許多原創(chuàng)想法?！斑@是我見過的最驚人的數(shù)學(xué)成就?！彼f。但是整個論證過于復(fù)雜，就連Scholze自己也擔(dān)心有什么細(xì)微漏洞導(dǎo)致功虧一簣?！罢撟C看起來很可信，但實在太過新穎。”Clausen說。

為了檢查自己的工作，Scholze向數(shù)論學(xué)家Buzzard求助。Buzzard是助手軟件包Lean的專家。Lean起初由微軟研究院的一位計算機科學(xué)家發(fā)明，用于嚴(yán)格檢查計算機代碼中的錯誤。

Buzzard曾負(fù)責(zé)過一個為期數(shù)年的項目，項目內(nèi)容是將帝國理工的所有本科數(shù)學(xué)課程編入Lean。他也曾試過將更高級的數(shù)學(xué)編入Lean，例如狀似完備空間（perfectoid space）的概念。Scholze正是憑借這個理論贏得了2018年的菲爾茲獎。

另一位數(shù)論學(xué)家Commelin帶隊驗證了Scholze和Clausen的證明。Commelin和Scholze決定將他們的Lean項目取名為“液體張力實驗”（Liquid Tensor Experiment），以此向前衛(wèi)搖滾樂隊Liquid Tension Experiment致敬，因為他倆都是這個樂隊的粉絲。

一場線上合作就此熱火朝天地展開了。十多位精通Lean的數(shù)學(xué)家加入團隊，研究人員還得到了計算機科學(xué)家們的協(xié)助。到六月初，這個團隊已經(jīng)將Scholze證明的核心部分（也是他最沒有把握的部分）全部轉(zhuǎn)譯成了Lean代碼。證明全部得以檢驗！該軟件的確具有檢驗這部分?jǐn)?shù)學(xué)證明的能力。

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

Riehl是試用過證明助手的數(shù)學(xué)家之一，她甚至在一些本科課程中教授相關(guān)內(nèi)容。她說，雖然她沒有在自己的研究中系統(tǒng)地使用這些工具，但是它們已經(jīng)開始改變她的思考方式，關(guān)于如何構(gòu)建數(shù)學(xué)概念、以及呈現(xiàn)和證明相關(guān)定理的做法?！耙郧拔矣X得證明和構(gòu)建是兩碼事，但現(xiàn)在我認(rèn)為它們是一樣的?！?/p>

許多學(xué)者認(rèn)為，短期內(nèi)機器并不能代替數(shù)學(xué)家。證明助手讀不懂?dāng)?shù)學(xué)課本，需要人類的持續(xù)輸入，也不知道一個數(shù)學(xué)命題是否有趣或重要，它們只能判斷命題正確與否，Buzzard說。但他補充說盡管如此，計算機或許馬上就能夠通過已知事實推導(dǎo)出被數(shù)學(xué)家們所忽視的結(jié)論了。

Scholze驚訝于證明助手的能力，但他不確定它們是否會繼續(xù)在自己的研究中扮演重要角色?！澳壳翱磥?，我并不清楚它們對我作為數(shù)學(xué)家的創(chuàng)造性工作會有什么幫助。”