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

撰文?|?Davide Castelvecchi

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

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

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

計(jì)算機(jī)成功驗(yàn)證了一個(gè)復(fù)雜的數(shù)學(xué)證明丨來(lái)源：Fadel Senna/ AFP via Getty

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

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

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

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

計(jì)算機(jī)輔助

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

然而，一種稱為證明助手（proof assistant）的系統(tǒng)功能更為深入。用戶基于系統(tǒng)已知的簡(jiǎn)單對(duì)象，輸入命題來(lái)使系統(tǒng)理解數(shù)學(xué)概念（一個(gè)對(duì)象）的定義。輸入的命題可以只涉及已知對(duì)象，證明助手則會(huì)基于它現(xiàn)有的知識(shí)來(lái)判斷該命題是“明顯”正確或錯(cuò)誤。如果證明助手的回答是不“明顯”，用戶則需要輸入更多的信息來(lái)訓(xùn)練它。證明助手借此迫使用戶更加嚴(yán)密地展開(kāi)他們的論證邏輯，并填補(bǔ)數(shù)學(xué)家們有意無(wú)意省略的一些較簡(jiǎn)單步驟。
一旦研究人員完成了前期繁重的訓(xùn)練工作，使證明助手理解了一系列數(shù)學(xué)概念，系統(tǒng)就會(huì)生成一個(gè)計(jì)算機(jī)代碼庫(kù)。其他研究人員可以以此為基礎(chǔ)進(jìn)行研究，并定義更高級(jí)的數(shù)學(xué)對(duì)象。由此，證明助手就能夠幫助檢驗(yàn)?zāi)切┖臅r(shí)費(fèi)力，甚至是人力所不可及的數(shù)學(xué)證明。
證明助手一直都不乏擁護(hù)者，但這是它首次在領(lǐng)域前沿發(fā)揮重要作用，帝國(guó)理工學(xué)院的數(shù)學(xué)家Kevin Buzzard說(shuō)。他參與檢驗(yàn)了Scholze和Clausen的研究結(jié)果?！爸斑z留下來(lái)的一個(gè)重要問(wèn)題是：證明助手能否處理復(fù)雜的數(shù)學(xué)問(wèn)題？”Buzzard說(shuō)?！拔覀冏C明了它們可以?！?/span>
而且這一切來(lái)得太快，超乎任何人的想象。2020年12月，Scholze向證明助手領(lǐng)域的專家們尋求幫助。德國(guó)弗賴堡大學(xué)的數(shù)學(xué)家Johan Commelin帶領(lǐng)一隊(duì)志愿者開(kāi)始著手解決這一難題。五個(gè)多月后的2021年6月5日，Scholze就在Buzzard的博客中宣布，實(shí)驗(yàn)主體部分已經(jīng)成功。“這簡(jiǎn)直不可思議。交互式證明助手現(xiàn)在已經(jīng)達(dá)到了如此的高度：它能在合理時(shí)間內(nèi)邏輯完備地驗(yàn)證復(fù)雜的原創(chuàng)研究?！盨cholze寫道。
Scholze和Clausen指出，凝聚態(tài)數(shù)學(xué)的關(guān)鍵在于重新定義現(xiàn)代數(shù)學(xué)的基石之一——拓?fù)?/span>（topology）的概念。數(shù)學(xué)家們研究的很多對(duì)象都具有拓?fù)?。拓?fù)涫菍?duì)象的一種結(jié)構(gòu)，它決定對(duì)象的哪些部分相連，哪些不是。拓?fù)涮峁┝诵螤畹男畔ⅲ潜绕鹞覀兯煜さ慕?jīng)典幾何，拓?fù)涓哐诱剐裕涸谕負(fù)渲校我獠环指顚?duì)象的變換都是允許的。比如，一個(gè)三角形在拓?fù)渖系葍r(jià)于其他任意三角形，甚至等價(jià)于圓形，但是無(wú)法等價(jià)于一條直線。
拓?fù)洳粌H在幾何學(xué)，而且在泛函分析（functional analysis；一門研究函數(shù)的學(xué)科）中也發(fā)揮關(guān)鍵作用。函數(shù)空間通常是無(wú)窮維的（例如量子力學(xué)中基礎(chǔ)的波函數(shù)）。另外，拓?fù)鋵?duì)于p進(jìn)數(shù)（p-adic number）系統(tǒng)也非常重要，其具有一種與眾不同的“分形”拓?fù)洹?/span>

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

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

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

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

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

加深理解

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

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

本文經(jīng)授權(quán)轉(zhuǎn)載自微信公眾號(hào)“Nature Portfolio”。原文以Mathematicians welcome computer-assisted proof in ‘grand unification’ theory為標(biāo)題發(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