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