Lean 4 從哪裡來：一個證明器決定「自己寫自己」的故事

Lean 維基百科

--

底下為 Grok AI 所寫 

--

Lean 4 從哪裡來：一個證明器決定「自己寫自己」的故事

數學家最怕什麼？不是題目難。是證明寫完了，過了半年，忽然有人舉手：「第 17 頁那個『顯然』，好像沒那麼顯然。」

電腦最怕什麼？不是算得慢。是程式跑了三年，某天半夜悄悄錯一次，沒人發現。

Lean 4 這套東西，就是有人受不了這兩種恐懼，決定做一個系統：你寫下來的每一步，機器都要能檢查；而且這套系統後來還任性到，連自己都用自己重寫了一遍。

聽起來很狂。故事卻是從一位巴西工程師，對自己舊工具的不滿開始的。

先有一台太聰明、也太黑盒的機器

主角叫 Leonardo de Moura。他不是那種站在黑板前講「存在一個 ε」的數學家，比較像把邏輯做成引擎的人。在微軟研究院的那些年，他做出過很有名的自動推理工具 Z3——你可以把它想成一位極會考試的學霸：給它一堆條件，它常常能自己推出答案。

問題是，學霸有學霸的毛病。它很快，但你問它「你剛剛怎麼想的」，它常常給你一臉茫然。證明不穩定、失敗原因不透明，再加上邏輯世界裡有些事本質上就不可判定——再聰明的自動機器，也會撞上天花板。

de Moura 後來自己講過，Lean 的起點，就是他受不了這種「黑盒子自動化」。他想要一種白盒子：自動化可以有，但每一步都得留下可檢查的證明，人也能插手。

2013 年，專案在微軟研究院開張。最早一筆程式碼落在那年 7 月 15 日。2014 年 6 月 16 日，Lean 0.1 正式露面。名字取得很直白：Lean，精瘦。意思大概是——可信的核心要小，別把整座教堂先蓋起來再找地基。

那時候它還不像今天這樣，既是程式語言又是證明助手。比較像一個實驗場：依賴類型論當地基，構造歸納演算當骨架，目標是把「互動式證明」和「自動推理」硬拗到同一張桌子上吃飯。

實驗期：Lean 1、Lean 2，以及一度很潮的同倫

接下來兩年，系統長得很快，也改得很快。後來被叫作 Lean 1、Lean 2 的那些版本，帶著實驗室該有的好奇心，甚至一度支援以同倫類型論為基礎的設定。同倫類型論當時很紅，像數學界突然流行一種新眼鏡，戴上去空間和等式看起來都不一樣。

後來這副眼鏡被拿掉了。不是因為同倫不漂亮，而是專案必須做選擇：要當一個能長期養大圖書館的系統，就不能永遠同時開十扇門。2015 年 Lean 2 比較像第一次對外人說「來用用看」；卡內基美隆也開始拿它上課。Jeremy Avigad 這類願意把哲學、數學和形式化縫在一起的人，開始幫忙堆標準庫。

若你覺得這段聽起來有點像新創公司前兩年的產品定位會，那你的直覺是對的。證明助手這一行，本來就很像同時在發明語言、發明編輯器、發明數學圖書館，還得說服全世界最挑的一群使用者：數學家。

Lean 3：數學家忽然成群結隊過來了

真正讓 Lean 從「研究室玩具」變成「有人願意拿真實數學去賭」的，是 2017 年 1 月 20 日的 Lean 3。

Lean 3 仍然主要用 C++ 寫，但做了一件當時很大膽的事：讓使用者用 Lean 自己寫戰術（tactic）、寫符號、寫指令。以前你想幫證明器加新招，常常得去改核心、學另一套語言。Lean 3 等於說：你會寫 Lean，就可以幫 Lean 變強。

這招很有效。同年，社群開始做 Mathlib——後來那座越來越不像「函式庫」、越來越像「用程式碼蓋的數學城」的計畫。代數、拓樸、分析、範疇，一塊塊被搬進去，每條定理都要過機器這關。到 Lean 3 末期，Mathlib 已經超過一百萬行，而且每一行都被核對過。

也是在這段時間，Lean 開始有了自己的江湖地位。Kevin Buzzard 在英國賣力傳教，年輕學生把形式化當成一種新的做數學方式。2020 年底，菲爾茲獎得主 Peter Scholze 丟出一個幾乎像挑戰書的問題：他和 Dustin Clausen 關於液態向量空間的核心定理，人審會不會看走眼？社群用後來稱為 Liquid Tensor Experiment 的計畫接招，2022 年 7 月做完。Scholze 中途說過一句很誠實的話，大意是：證明助手現在能在合理時間內核對這種原創研究，他覺得簡直瘋了。

數學家願意把還沒涼透的研究丟進機器裡，這在十年前幾乎是科幻。

可是成功也會暴露牆在哪裡。

那堵牆：C++ 寫的心臟，Lean 寫的手腳

Lean 3 的可擴充性很迷人，但有兩個現實問題。

第一，很多關鍵部位仍在 C++ 裡。你想改解析器、闡釋器、印得好看的那層，常常得會兩種完全不同的手藝。這對開源社群不友善——數學家不一定想當 C++ 工程師，C++ 工程師也不一定想半夜除「宇宙層級」的類型錯誤。

第二，用 Lean 寫的自動化，跑在直譯器上，慢。你寫的戰術再聰明，若每次展開都像在泥地裡跑步，複雜的數學庫一膨脹，系統就會喘。

於是 2018 年，de Moura 和 Sebastian Ullrich 開始做一件聽起來不合理的事：把 Lean 變成夠快、夠完整的通用程式語言，然後用 Lean 重寫 Lean。

這就是 Lean 4。

用自己重寫自己，在程式語言圈叫 self-hosting，自宿主。好處很具體：改系統的人，和用系統的人，開始說同一種語言；新功能不必永遠排隊等核心團隊在 C++ 裡開刀；編譯成 C 再往下走，自動化終於可以跑得像真正的程式，而不是像被解釋的草稿。

他們後來承認，這次改造花的時間，幾乎等於前面所有版本加起來。過程也不全然浪漫。倉庫一度不公開，社群和核心之間有過緊繃，Gabriel Ebner 等人還得在過渡期把 Lean 3 撐著。Mathlib 開始做 Lean 4 時還不算巨大，有人樂觀估計「用手搬一個月就好」——然後圖書館自己長成百萬行怪獸。遷移變成一場集體搬家，不是一個人的週末專案。

2021 年初，Lean 4 開始對外釋出。2023 年 9 月 8 日，4.0.0 正式定案。官方後來寫得很乾脆：設計他們滿意了，不打算再來一次大重寫。

對使用者來說，這句話的潛台詞是：請把行李留在 Lean 4。Lean 3 不相容，語法、戰術、建置方式都不一樣。搬家很痛，但痛完之後，檢查同一個更大的 Mathlib，速度反而比舊系統檢查較小的庫還快。

2023 之後：從專案變成機構，從數學伸向程式

同年 7 月，de Moura 和 Ullrich 成立非營利的 Lean FRO（Focused Research Organization），把「把這套語言養到能長期用」當成正職。資助來自 Simons、Sloan 等基金會，de Moura 本人後來也在 Amazon 的自動推理組。系統不再只靠一間公司研究室裡的熱情續命。

Mathlib 在 2023 年完成搬遷，之後繼續漲，有統計從一百五十萬行往兩百萬行走。Terence Tao 帶人把剛證完的多項式 Freiman–Ruzsa 猜想形式化，後來還有大規模的等式理論眾包。再後來，人工智慧研究開始把 Lean 當成「數學答案要交機器收據」的考場——模型可以很會聊天，但 Lean 核對通過，才算這題真的寫完。

de Moura 自己的說法一直相當清楚：數學是試煉場，不是終點。軟體驗證、硬體、控制器、翻譯器，這些才是他心裡那條更長的路。數學夠硬、夠吹毛求疵，系統若能在這裡活下來，去檢查程式時比較不會一碰就散。

所以 Lean 4 到底是什麼？

若只記一句：它是一個依賴類型的函數式語言，也是一個互動式定理證明器。你可以拿它寫普通程式，也可以拿它寫「這段推論在邏輯上無漏洞」的證明。從第四版起，實現它的程式碼大約九成也是 Lean，核心小、外圍能長、使用者能改解析、能改戰術、能改印出來的樣子。

若再記一句：它不是突然從天上掉下來的天才玩具。它是 Z3 那種自動推理走不下去之後的轉向，是 Lean 3 把數學家吸引進來之後，被成功逼出來的一次自我手術。

證明助手這一行從來不缺前輩。Coq（現在常改稱 Rocq）、Isabelle、HOL 家族都比它老，也各有偉大的成績。Lean 比較特別的地方，是它剛好趕上三件事疊在一起：社群願意共建一座活的數學庫、語言願意把自己變成可編譯的程式語言、以及後來 AI 需要一種「不能靠語氣取勝」的檢查器。

當然，它仍然不是魔法。機器只檢查你寫進去的東西；你沒說的假設，它不會幫你發明。形式化很慢，搬家很煩，錯誤訊息有時像一位過於誠實的老師。可是「顯然」這兩個字，在 Lean 裡沒有特權。這點，對數學和對程式，其實是同一種美德。