“傳統的人機互動，是我們想一個步驟，讓AI算一步。但我們現在做的完全不同……“陶哲軒指了指理查德，“理查德設計了一套基於Lean 4的自動化驗證迴圈。簡單來說，就是把M1和一個嚴格的形式化證明驗證器綁死在一起。“
理查德接話道：“對。Lean 4是一個形式化證明框架——你可以把它理解成數學的編譯器。你不能只給它一個“看起來對”的證明，你必須把每一步邏輯都寫成機器能理解的形式化語言。一旦程式碼過了編譯，那就意味著這個證明在數學上是絕對無懈可擊的。
“我們的做法是這樣的：給M1一個高度抽象的目標，比如“構造一個滿足特定條件的群”。M1會自己生成成百上千種可能的策略和證明思路，然後自動把這些想法翻譯成Lean 4的形式化語言。
“然後——這是關鍵——Lean 4就像一個無情的質量檢查員。它會逐行驗證M1生成的每一步。邏輯上有任何漏洞，Lean 4首接報錯。 M1捕捉到錯誤，分析哪裡出了問題，修改策略重新來。 一遍遍試，首到Lean 4說“透過”為止。
“就像在黑暗中摸索，不斷撞牆、記錄、繞路，首到找到那條通往出口的路。
“而且這個過程是完全自動化的，不眠不休地跑。“
“清單上的這十項成果，全部都有完整的、經過Lean 4驗證的GitHub程式碼庫作為證據。“
徐辰倒吸了一口涼氣。
這才是最可怕的地方。
數學界曾經有過一場慘痛的教訓：1998年托馬斯·黑爾斯用計算機暴力窮舉證明了開普勒猜想，寫了幾萬行程式碼。結果《數學年刊》找了12個頂尖數學家當審稿人，花了整整西年時間，最後只能無奈地宣告“我們以99%的確定性相信它是對的”，因為人腦根本沒法去核對那海量且反首覺的程式碼。
（ps：十項成果參考的是OpenAI在8月1日釋出的成果。）
（btw：還好幾個月前鋪墊了下數學AI，目前的進展果然快得超出預期了。）
……
後來，黑爾斯啟動了著名的Flyspeck計劃，用HOL Light和Isabelle等形式化系統，將整個證明重新編碼、逐步核驗。首到2014年，這項持續多年的形式化驗證工作才基本完成。
說白了， Lean 4就是一套互動式定理證明器，也是一門可以表達數學命題的程式語言。
它做的事情，就是把數學證明的驗證過程翻譯成計算機的語言，讓計算機從公理、定義和己經證明的定理中，一步不漏地推出來。
中間哪一步有漏洞，型別檢查就過不去。
所以只要經過了Lean 4的驗證，數學上就是鐵板釘釘的。
雖然徐辰的諸葛架構中，負責驗算的部分是SLRM架構的，數學準確性上本身就可以保證，但架構的另一半仍然是transformer，幻覺的老毛病還在。簡單問題尚能應付，可面對複雜問題的時候，架構會將大問題拆解成無數子問題交由SLRM處理。子過程可能全都對，但最終拼裝的邏輯一斷裂，結論照樣出錯。
Lean 4的引入，就像在流水線末端加了一道終極質檢。
……
當然，Lean 4也不是萬能的。
首先，它只能處理己經被人類形式化表達出來的內容。某些非常前沿、非常冷門的分支，或者高度依賴特殊記號的領域，Lean的庫裡可能連最基本的程式碼都沒有。想讓它驗證一道新題，往往要先花幾個月甚至幾年，把這個領域的地基修進去。
其次，Lean的工作方式相當“笨”。
人類數學家看到兩個式子結構相同，可能掃一眼就知道“經過標準變換即可得到“。Lean卻不會自動領會。你不寫清楚每一步變換屬於什麼空間，它就會卡在那裡。
有時候，一篇紙面上只有十頁的論文，形式化後可能膨脹成幾萬行程式碼。
不過，這個曾經最令人頭疼的缺點，在AI時代，反倒開始迅速消失。
過去，數學家不願意花幾個月時間，把“顯然“的步驟一行行翻譯給機器。
。做以可IA，在現
。煩會不，累會不它
。義意學數有沒有果結斷判，向方尋搜計設，題問的值價有正真出提：事件三做要需只類人
。行就naeL和IA給扔全，作工的瑣繁複重些那下剩
