德國著名數學家、菲爾茲獎得主皮特・舒爾茨遇到了一個難題。

他和哥本哈根大學的數學家達斯汀・克勞森，多年來一直致力於一個名為“凝聚態數學”（Condensed Mathematics）的問題。

他倆發現，因為拓撲學的傳統概念，導致三個數學領域（幾何、泛函分析和 p 進數）之間不相容，如果建立一種新的基礎概念，就可以實現一個“大統一”理論。

但是，在研究這個問題過程中，舒爾茨遇到了一個特別重要且困難的證明。

2019 年 7 月的一週，舒爾茨開始在腦海中開始自己的證明，幾乎沒有藉助紙筆。直到 11 月，舒爾茨才完整寫下了證明。

但是證明過程是如此複雜，連舒爾茨都不敢保證證明中是否有紕漏。

尋求計算機驗證

一年後，舒爾茨聯絡了倫敦帝國理工學院的數學家 Kevin Buzzard，他是“Lean”的佈道者。

Lean 是微軟研究院在 2013 年推出的計算機定理證明器：數學家可以把數學公式轉換成程式碼，再輸入到 Lean 中，讓程式來驗證定理是否正確。

這是一項雙贏的合作。

舒爾茨把他的證明輸入到 Lean 中，可以驗證自己是否正確。

對於 Buzzard 來說，這是為 Lean 揚名的大好機會，如果能和舒爾茨這樣的天才數學家聯名，無疑對計算機輔助證明在數學界的合法化有很大幫助。

Buzzard 向 Lean 社群的其他成員分享了舒爾茨的證明，其中就包括弗萊堡大學的博士後 Johan Commelin。

“能夠在這樣一個專案上與彼得合作並附上他的名字，對 Lean 來說是一個巨大的宣傳。”Commelin 說。

但是，如果證明花的時間太長，數學界的人不會意識到這項工作的重要性，他們會說：“哦，我們已經知道舒爾茨證明了這一點。”

因此，Commelin 問舒爾茨，是否願意發表公開宣告，證明這項工作的重要性。舒爾茨答應了。

舒爾茨公佈實驗結果

2020 年 12 月 5 日，舒爾茨在 Buzzard 的部落格上公佈了證明結果，在這篇 4000 多字的文章中，舒爾茨用通俗的語言證明計算機驗證的重要性。

他們把這項驗證實驗叫做“液體張量實驗”，這既是對液體實向量空間的證明中涉及的數學物件的一種致敬，也是對兩位數學家喜歡的搖滾樂隊“液體張力實驗”的致敬。

舒爾茨說這個定理可能是他“迄今為止最重要的定理”。

Commelin 將舒爾茨的問題釋出到一個名叫 Zulip 社群上，由十幾位數學家協力完成，每個人都在自己擅長的領域構建證明程式碼。

隨著工作的進行，舒爾茨始終如一地出現在 Zulip 社群上，回答問題並解釋證明要點，有點像建築師在工作現場為提供指導一樣。

5 月 29 日凌晨 1 點 10 分，Commelin 輸入了最後的回車鍵。Lean 編譯了整個證明，驗證舒爾茨的工作是 100% 正確的。

雖然舒爾茨仍然喜歡在腦海中尋找證明，但 Lean 的能力給他留下了深刻的印象。

“這個實驗徹底改變了我對（計算機輔助證明）能力的印象，”舒爾茨說。

日漸成熟的 Lean

幫助舒爾茨只是 Lean 這麼多年中的一項工作而已，這個最初由微軟研究院開源的數學證明器，如今已經得到許多數學家的支援。

聚集在 Zulip 上的數學家正在為 Lean 構建一個數學知識庫 mathlib。截至今日，mathlib 已經包含了 26492 條定義和 58738 條定理。

Buzzard 多年來一直在進行一項計劃，就是將帝國理工學院的整個本科數學課程用 Lean 寫成程式碼，目前只完成了一半。

但是正在為 Lean 完善數學庫的人幾乎可以肯定，在幾年內，Lean 至少能夠理解本科高年級期末考試中的問題。

如今 Lean 已經進化到第四代，今年微軟還讓它參加了 IMO。不過，Lean 到底在剛剛結束的 IMO 中有怎樣的發揮，官方並未公佈。

參考連結：

[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