微軟用15年造了個"數學外掛"，程序員看完集體沉默

2006年，微軟研究院的一群人決定做件"蠢事"：用數學證明程序不會崩潰。當時沒人覺得這事能成——畢竟寫代碼已經夠累了，誰還想給代碼寫"數學作業"？

15年后，這個叫Lean的項目跑通了。不是跑在實驗室里，是跑在數學家證明龐加萊猜想的現場，跑在本科生的期末作業里，現在還要跑進你的VS Code。

從"沒人用"到"搶著用"：一個定理證明器的逆襲

Lean的誕生帶著典型的學術氣質。微軟研究院的Leonardo de Moura想解決一個老問題：怎么讓計算機幫忙驗證數學證明是對的。這活兒以前叫"形式化驗證"，屬于那種聽起來很酷、用起來很虐的工具——你得先把證明翻譯成機器能懂的語言，比寫證明本身還費勁。

Lean的前兩代（Lean 1和2）基本沒人記得。轉折點在Lean 3，團隊做了個關鍵決定：把定理證明器做成通用的函數式編程語言。數學家可以用它寫證明，程序員可以用它寫代碼，兩邊互不耽誤。

這個定位讓它意外破圈。2020年，菲爾茲獎得主Timothy Gowers在博客寫了一句：「Lean可能是未來數學家的標準工具。」同年，Kevin Buzzard帶著帝國理工的學生，用Lean形式化了整個本科數學課程體系。

到Lean 4發布時，事情變得更有趣了。它不再只是"數學家的IDE"，而是一個能編譯成C代碼、性能接近原生、還帶垃圾回收的通用語言。de Moura的原話是：「我們想造一個程序員真的想用的工具。」

函數式編程的"隱藏副本"：為什么選這條路

Lean的底層設計藏著個反直覺的選擇：純函數式（Pure Functional）。沒有可變狀態，沒有副作用，所有計算都是數學意義上的函數——輸入確定，輸出就確定。

這聽起來像自找麻煩。畢竟現實世界的程序要讀寫文件、要發網絡請求、要改數據庫狀態。但Lean的答案是：把這些"臟活"用Monad（單子）包起來，和純計算嚴格區分。

Monad這個從范疇論借來的概念，在Lean里成了安全邊界。你的核心算法可以保持"數學純凈"，副作用被隔離在類型系統的監管之下。編譯器會檢查：你是不是在純函數里偷偷干了不該干的事？

這種設計讓Lean特別適合一類場景：你需要絕對確定代碼沒bug，而且愿意為此付出額外成本。比如加密算法、金融合約、醫療設備的控制邏輯——或者，數學家那個長達幾百頁、審稿人看了三年的證明。

2021年，Peter Scholze（另一個菲爾茲獎得主）在Nature發文，宣布他和Dustin Clausen的"液態張量實驗"證明被Lean驗證。這個證明的復雜度讓傳統審稿流程幾乎不可能完成，Lean卻把它拆成10萬行形式化代碼，逐行檢查過了。

VS Code里的"證明即代碼"：產品化路徑

Lean 4的產品化做得相當克制。沒有新建IDE，而是做了VS Code插件；沒有造輪子，而是用LLVM做后端編譯。de Moura的團隊顯然明白：工具再強，用戶遷移成本太高也是白搭。

插件的體驗很產品經理思維。你寫證明的時候，編輯器實時顯示當前目標（Goal）和可用策略（Tactics），像在玩一個解謎游戲。錯誤不是紅字報錯，而是"這里還缺一步"的引導式提示。

更隱蔽的設計是Mathlib——社區維護的數學庫。這個庫現在有超過100萬行形式化代碼，覆蓋從線性代數到代數拓撲的標準內容。數學家寫新證明時，可以直接引用庫里的定理，像調用API一樣。

這種"可組合性"是函數式編程的老優勢，但Lean把它做成了學術基礎設施。2023年，Terence Tao用Lean驗證了一個關于多項式Freiman-Ruzsa猜想的證明，整個過程在GitHub公開，任何人可以復查每一步。

從學術玩具到工程工具的鴻溝

但Lean的野心不止于數學。團隊正在推的"Lean for the working programmer"路線，試圖解決一個更實際的問題：普通軟件能不能也用形式化驗證？

目前的答案是"能，但有條件"。Lean可以編譯成高效的C代碼，性能測試顯示某些場景接近手寫C。但形式化驗證的成本依然很高——你需要先寫規范（Specification），再寫實現，最后寫證明兩者等價。三倍代碼量起步。

de Moura的回應很直接：「不是每個函數都需要證明。但關鍵路徑上的代碼，比如密碼學的核心實現，值得這個投入。」

這種分層思路正在落地。AWS的加密工具包部分模塊用了形式化驗證，Google的Chrome有類似嘗試。Lean的優勢在于，它讓這種驗證可以用同一套語言完成——寫代碼和寫證明不需要切換上下文。

一個被反復提及的案例是seL4，一個經過形式化驗證的操作系統內核。它的驗證用了Isabelle/HOL，另一個定理證明器。但Lean社區有人在做類似嘗試，而且試圖把驗證成本降下來。

15年后的現在，誰在為確定性買單

Lean的GitHub倉庫現在有接近4000個Star，Mathlib的貢獻者超過300人。這些數字在開源世界不算顯眼，但用戶的含金量很高——菲爾茲獎得主、頂尖高校的數學系、對安全極度敏感的工業團隊。

微軟對這個項目的投入也很有意思。研究院的項目通常有"孵化期"，但Lean持續了15年，而且明顯在加大工程化力度。一個可能的解釋是：云服務的安全需求在升級，形式化驗證從"學術奢侈品"變成"工程可選項"的時機正在成熟。

de Moura最近在訪談里被問到：「Lean會取代傳統編程嗎？」他的回答很產品經理：「不會。但未來的關鍵系統，可能會默認包含形式化驗證的模塊，就像現在默認包含單元測試一樣。」

這個預測能不能兌現，取決于一個更底層的問題：程序員愿不愿意為"數學確定性"支付額外的認知成本？Lean把門檻降了很多，但還沒降到零。

你在寫代碼的時候，有沒有遇到過那種"要是能證明這沒bug就好了"的時刻？如果證明這個功能的成本，從"寫一篇論文"降到"寫三倍代碼"，你會用嗎？