德國著名數(shù)學(xué)家，菲爾茲獎(jiǎng)獲得者彼得舒爾茨遇到了一個(gè)難題

他和哥本哈根大學(xué)的數(shù)學(xué)家達(dá)斯汀克勞森多年來一直在研究一個(gè)名為濃縮數(shù)學(xué)的問題

他們發(fā)現(xiàn)，由于傳統(tǒng)的拓?fù)涓拍睿@三個(gè)數(shù)學(xué)領(lǐng)域是不相容的如果創(chuàng)造一個(gè)新的基本概念，就可以實(shí)現(xiàn)大統(tǒng)一理論

可是，在研究這個(gè)問題的過程中，舒爾茨遇到了一個(gè)特別重要和困難的證明。

2019年7月的那一周，舒爾茨開始在腦海中證明自己，幾乎沒有紙和筆的幫助直到11月份，舒爾茨才完整地寫出了證明

但證明過程如此復(fù)雜，連舒爾茨都無法保證證明中是否有瑕疵。

尋求計(jì)算機(jī)驗(yàn)證

一年后，舒爾茨聯(lián)系了凱文布扎德，他是倫敦帝國理工學(xué)院的數(shù)學(xué)家，也是精益思想的傳播者。

Lean是微軟研究院2013年推出的一款計(jì)算機(jī)定理證明器:數(shù)學(xué)家可以將數(shù)學(xué)公式轉(zhuǎn)換成代碼，輸入到Lean中，讓程序驗(yàn)證定理是否正確。

這是一個(gè)雙贏的合作。

舒爾茨可以通過將他的證明輸入Lean來驗(yàn)證他的正確性。

對(duì)于Buzzard來說，這是Lean揚(yáng)名立萬的絕佳機(jī)會(huì)如果他能加入像舒爾茨這樣的天才數(shù)學(xué)家，無疑將有助于計(jì)算機(jī)輔助數(shù)學(xué)認(rèn)證的合法化

Buzzard與精益社區(qū)的其他成員分享了舒爾茨的證明，包括弗萊堡大學(xué)博士后Johan Commelin。

能夠在這樣一個(gè)項(xiàng)目上與彼得合作，并附上他的名字，對(duì)Lean來說是一個(gè)很大的宣傳鴨跖草說

但是，如果證明的時(shí)間太長(zhǎng)，數(shù)學(xué)界的人不會(huì)意識(shí)到這項(xiàng)工作的重要性，他們會(huì)說:哦，我們已經(jīng)知道舒爾茨證明了這一點(diǎn)。

因此，Commelin詢問舒爾茨是否愿意發(fā)表公開聲明來證明這項(xiàng)工作的重要性舒爾茨同意了

舒爾茨宣布了實(shí)驗(yàn)結(jié)果

日前，舒爾茨在Buzzard的博客上公布了證明結(jié)果在這篇4000字的文章中，舒爾茨用通俗易懂的語言證明了計(jì)算機(jī)驗(yàn)證的重要性

他們把這個(gè)驗(yàn)證實(shí)驗(yàn)稱為液體張量實(shí)驗(yàn)，這不僅是對(duì)液體實(shí)向量空間證明所涉及的數(shù)學(xué)對(duì)象的致敬，也是對(duì)兩位數(shù)學(xué)家喜歡的搖滾樂隊(duì)液體張力實(shí)驗(yàn)的致敬。

舒爾茨說，這個(gè)定理可能是他迄今為止最重要的定理。

Commelin向一個(gè)名為Zulip的社區(qū)發(fā)布了舒爾茨的問題，這個(gè)社區(qū)由十幾個(gè)數(shù)學(xué)家完成，他們每個(gè)人都在自己的領(lǐng)域構(gòu)建了證明代碼。

伴隨著工作的進(jìn)行，舒爾茨一直出現(xiàn)在Zulip社區(qū)，回答問題并解釋證明的關(guān)鍵點(diǎn)，這有點(diǎn)像建筑師在工作現(xiàn)場(chǎng)提供指導(dǎo)。

5月29日凌晨1點(diǎn)10分，Commelin輸入了最后一個(gè)回車鍵Lean整理了整個(gè)證明，驗(yàn)證了舒爾茨的工作是100%正確的

雖然舒爾茨還是喜歡在腦子里找證據(jù)，但Lean的能力給他留下了深刻的印象。

舒爾茨說:這個(gè)實(shí)驗(yàn)徹底改變了我對(duì)能力的印象。

成熟的瘦肉

幫助舒爾茨只是精益這么多年的工作之一這個(gè)數(shù)學(xué)證明器最初由微軟研究院開放，得到了很多數(shù)學(xué)家的支持

聚集在祖利普的數(shù)學(xué)家們正在為L(zhǎng)ean建立一個(gè)數(shù)學(xué)知識(shí)庫mathlib到目前為止，mathlib已經(jīng)包含了26492個(gè)定義和58738個(gè)定理

Buzzard多年來一直在執(zhí)行一個(gè)計(jì)劃，就是把倫敦帝國理工學(xué)院的整個(gè)本科數(shù)學(xué)課程寫成Lean代碼，目前只完成了一半。

可是，那些正在完善精益數(shù)學(xué)庫的人幾乎可以肯定，精益至少會(huì)在幾年后理解高年級(jí)本科生期末考試中的問題。

現(xiàn)在Lean已經(jīng)進(jìn)化到第四代了，今年微軟也讓它參加了IMO可是，這位官員還沒有宣布精益在剛剛結(jié)束的國際海事組織中到底是如何發(fā)揮作用的

參考鏈接: