德國著名數(shù)學(xué)家、菲爾茲獎得主皮特?舒爾茨遇到了一個難題。
他和哥本哈根大學(xué)的數(shù)學(xué)家達(dá)斯汀?克勞森，多年來一直致力于一個名為“凝聚態(tài)數(shù)學(xué)”（Condensed Mathematics）的問題。
他倆發(fā)現(xiàn)，因?yàn)橥負(fù)鋵W(xué)的傳統(tǒng)概念，導(dǎo)致三個數(shù)學(xué)領(lǐng)域（幾何、泛函分析和 p 進(jìn)數(shù)）之間不兼容，如果創(chuàng)建一種新的基礎(chǔ)概念，就可以實(shí)現(xiàn)一個“大統(tǒng)一”理論。
但是，在研究這個問題過程中，舒爾茨遇到了一個特別重要且困難的證明。
2019 年 7 月的一周，舒爾茨開始在腦海中開始自己的證明，幾乎沒有借助紙筆。直到 11 月，舒爾茨才完整寫下了證明。
但是證明過程是如此復(fù)雜，連舒爾茨都不敢保證證明中是否有紕漏。
尋求計算機(jī)驗(yàn)證
一年后，舒爾茨聯(lián)系了倫敦帝國理工學(xué)院的數(shù)學(xué)家 Kevin Buzzard，他是“Lean”的布道者。
Lean 是微軟研究院在 2013 年推出的計算機(jī)定理證明器：數(shù)學(xué)家可以把數(shù)學(xué)公式轉(zhuǎn)換成代碼，再輸入到 Lean 中，讓程序來驗(yàn)證定理是否正確。
這是一項(xiàng)雙贏的合作。
舒爾茨把他的證明輸入到 Lean 中，可以驗(yàn)證自己是否正確。
對于 Buzzard 來說，這是為 Lean 揚(yáng)名的大好機(jī)會，如果能和舒爾茨這樣的天才數(shù)學(xué)家聯(lián)名，無疑對計算機(jī)輔助證明在數(shù)學(xué)界的合法化有很大幫助。
Buzzard 向 Lean 社區(qū)的其他成員分享了舒爾茨的證明，其中就包括弗萊堡大學(xué)的博士后 Johan Commelin。
“能夠在這樣一個項(xiàng)目上與彼得合作并附上他的名字，對 Lean 來說是一個巨大的宣傳?！盋ommelin 說。
但是，如果證明花的時間太長，數(shù)學(xué)界的人不會意識到這項(xiàng)工作的重要性，他們會說：“哦，我們已經(jīng)知道舒爾茨證明了這一點(diǎn)。”
因此，Commelin 問舒爾茨，是否愿意發(fā)表公開聲明，證明這項(xiàng)工作的重要性。舒爾茨答應(yīng)了。
舒爾茨公布實(shí)驗(yàn)結(jié)果
2020 年 12 月 5 日，舒爾茨在 Buzzard 的博客上公布了證明結(jié)果，在這篇 4000 多字的文章中，舒爾茨用通俗的語言證明計算機(jī)驗(yàn)證的重要性。
他們把這項(xiàng)驗(yàn)證實(shí)驗(yàn)叫做“液體張量實(shí)驗(yàn)”，這既是對液體實(shí)向量空間的證明中涉及的數(shù)學(xué)對象的一種致敬，也是對兩位數(shù)學(xué)家喜歡的搖滾樂隊(duì)“液體張力實(shí)驗(yàn)”的致敬。
舒爾茨說這個定理可能是他“迄今為止最重要的定理”。
Commelin 將舒爾茨的問題發(fā)布到一個名叫 Zulip 社區(qū)上，由十幾位數(shù)學(xué)家協(xié)力完成，每個人都在自己擅長的領(lǐng)域構(gòu)建證明代碼。
隨著工作的進(jìn)行，舒爾茨始終如一地出現(xiàn)在 Zulip 社區(qū)上，回答問題并解釋證明要點(diǎn)，有點(diǎn)像建筑師在工作現(xiàn)場為提供指導(dǎo)一樣。
5 月 29 日凌晨 1 點(diǎn) 10 分，Commelin 輸入了最后的回車鍵。Lean 編譯了整個證明，驗(yàn)證舒爾茨的工作是 100% 正確的。
雖然舒爾茨仍然喜歡在腦海中尋找證明，但 Lean 的能力給他留下了深刻的印象。
“這個實(shí)驗(yàn)徹底改變了我對（計算機(jī)輔助證明）能力的印象，”舒爾茨說。
日漸成熟的 Lean
幫助舒爾茨只是 Lean 這么多年中的一項(xiàng)工作而已，這個最初由微軟研究院開源的數(shù)學(xué)證明器，如今已經(jīng)得到許多數(shù)學(xué)家的支持。
聚集在 Zulip 上的數(shù)學(xué)家正在為 Lean 構(gòu)建一個數(shù)學(xué)知識庫 mathlib。截至今日，mathlib 已經(jīng)包含了 26492 條定義和 58738 條定理。
Buzzard 多年來一直在進(jìn)行一項(xiàng)計劃，就是將帝國理工學(xué)院的整個本科數(shù)學(xué)課程用 Lean 寫成代碼，目前只完成了一半。
但是正在為 Lean 完善數(shù)學(xué)庫的人幾乎可以肯定，在幾年內(nèi)，Lean 至少能夠理解本科高年級期末考試中的問題。
如今 Lean 已經(jīng)進(jìn)化到第四代，今年微軟還讓它參加了 IMO。不過，Lean 到底在剛剛結(jié)束的 IMO 中有怎樣的發(fā)揮，官方并未公布。
參考鏈接：
[1]https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/
[2]https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
[3]https://github.com/leanprover/lean4
廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。