2026年8月1日，OpenAI宣布其未發布的下一代模型Astra在10個懸而未決的數學和理論電腦科學問題上取得了新結果，涵蓋高維幾何、編碼理論、群論、算子代數等8個領域。每一個結果都附帶了可以被機器逐行檢查的Lean
4證明證書，發布在GitHub上，任何人用一台筆記本電腦就能獨立驗證。
這裡反覆出現的"Lean"，是一門大多數開發者和數學愛好者可能只在新聞里見過名字的編程語言。簡單說，Lean既是一門編程語言，也是一個證明助手。你可以在裡面寫代碼，也可以寫數學證明，而且Lean會替你檢查證明是否正確。它的獨特之處在於：你寫的證明不是給人看的文字論證，而是一段可以被電腦嚴格驗證的程序。如果Lean說你的證明通過了，那就意味著這個結論在數學上成立，沒有任何模糊地帶。
就在OpenAI發布這些成果後不到十天，播客The Peterman Pod的主持人Ryan Peterman對話了Lean的創造者Leonardo de Moura。de Moura目前在AWS擔任高級首席應用科學家，同時是Lean背後的非營利研究組織Lean FRO的首席架構師和聯合創始人。他也是另一個廣泛使用的工具Z3SMT求解器的創造者。在這次對話里，他說："我已經不再寫測試了。我寫性質，然後AI替我證明。"
de Moura用電腦科學家Dijkstra的一句話開場："程序測試可以用來表明存在bug，但永遠不能證明bug不存在。"
這句話是理解Lean存在意義的鑰匙。一個測試套件無論多全面，覆蓋的終究是你想到的場景。總有某個邊角情況不在其中。形式化證明做的事情不同：它覆蓋所有可能的場景，給出數學意義上的保證。
一個具體的例子：想像程序里有一排格子，一共10個，編號從0到9，這就是一個數組。程序需要從某個格子裡取數據，用一個叫i的變量記錄"取第幾個格子"。如果i跑到了10或者更大，程序就去取一個不存在的格子，這就是越界訪問，輕則數據出錯，重則系統崩潰。
在C語言裡，編譯器不會攔你，只有程序跑到那一行的時候才會出事。在Lean中，你可以寫一條數學語句，聲明在程序的某個位置，索引變量i的值大於等於0且小於10。Lean會要求你證明這條語句為真。證明不了，代碼就過不了檢查。問題在寫代碼的時候就必須解決，你得向Lean交代清楚"為什麼i不會越界"。
驗證過程會用到一種叫霍爾三元組的技術，它把每條語句拆成三部分來推理：執行前什麼條件應該為真、語句本身做了什麼、執行後什麼條件保證為真。自動化工具會處理大量這樣的推理步驟，讓證明可以模組化。de Moura把這個過程比作在源代碼上方疊加了一層"第二個軟體層"，專門用來描述和驗證程序的行為。
但Lean本身的程序怎麼辦？如果連Lean自己都可能有bug，憑什麼信任它的驗證結果？
de Moura的回答里有一個清晰的分層：你不需要信任整個Lean，只需要信任它的核心。
在Lean中，證明檢查本質上就是類型檢查。你寫了一個證明項，Lean的核心檢查這個項的類型是否匹配你聲稱要證明的命題。這個核心只有大約5000行代碼，目標是小到任何人都能自己從頭寫一個。
Lean本身是一個龐大的程序，功能在不斷增加，很難給出完整的規格說明。但核心可以有精確的規格說明，而且已經有人這麼做了。Mario Carneiro用Lean本身寫了一個叫Lean4Lean的核心，並證明了它相對於Lean語義的正確性。還有人用Rust和其他編程語言實現了獨立的核心。
擁有多個獨立核心是確保結果正確的最好方式。 一些外部核心還會列印出所有已證明命題的完整列表及其依賴鏈。這樣你可以確認自己看到的確實是你想證明的東西，而不是某個無關的恆真式（比如2+2=4）被冒充成了你的定理。
如果要驗證的是用C或Rust寫的軟體呢？有兩條路線。第一種叫淺嵌入（shallow embedding），把目標語言翻譯成Lean，然後驗證翻譯後的版本。現在已經有工具Aeneas可以把Rust代碼映射成Lean。第二種叫深嵌入（deep embedding），在Lean里寫出目標語言的語義，程序變成Lean里的數據結構，可以對這個數據結構聲明性質並證明。
de Moura的同事Kim Morrison最近做了一件他幾個月前還認為不可能的事。
她用AI把C語言的壓縮庫zlib翻譯成Lean，確保翻譯版通過了zlib的測試套件，然後證明了一條關鍵性質：壓縮數據再解壓，一定能恢復原始數據。 對一個壓縮引擎來說，這可能是最重要的性質了。
整個過程用了大約一周。Kim Morrison的GitHub倉庫lean-zip顯示，實現和驗證都由鬆散監督的AI完成，底層包含超過1100條定理、約32000行證明代碼，沒有任何未完成的占位符，每次提交都會從頭重新檢查所有證明。
現在他們在讓AI優化代碼，但有一條硬約束：優化不能破壞已有的證明。這正是de Moura反覆強調的一個核心觀點：有了證明，優化就是免費的。 你不需要人工檢查優化後的版本有沒有引入bug，因為證明會替你守住所有性質。
這件事之所以重要，是因為它改變了形式化驗證的成本結構。
de Moura給了一個直覺：如果寫程序花x時間，過去做形式化驗證要花10x。但真正的痛苦在於維護，而非初始投入。程序在不斷變化，每次改動都可能破壞證明，就像改了代碼後測試全紅一樣，只是修證明比修測試更難，因為你可能已經不記得某個證明背後的邏輯了。
AI在這個環節表現極好。de Moura舉了自己前一天的經歷：他想修改一些他本人沒寫的證明，甚至不知道那些證明是關於什麼的，他告訴AI"請在不使用某個特性的情況下重寫這些證明，因為我要改動它"，AI瞬間給出了新版本。
"I used to believe my superpower was that I could tolerate a lot of pain. That superpower is no longer relevant." 他在另一場演講中這樣總結。
作為對比，seL4是AI出現之前形式化驗證的標杆項目。這個經過完全驗證的微核心只有大約8700行C代碼，驗證總共花了約20人年的工作量，每行代碼的驗證成本約350美元。AWS過去十年一直在用形式化驗證，但只敢用在最關鍵的安全組件上，因為成本太高。
AI改變了這個等式。規格說明你仍然需要人來寫，但它從來不是最痛苦的部分。最痛苦的是手工開發證明和維護證明，AI在這兩件事上都極其擅長。
"那規格說明是不是比測試套件難寫得多？"主持人問。
de Moura給了一個否定的回答。很多時候，開發者心裡清楚程序應該滿足什麼性質，只是過去沒有工具讓他們表達並驗證。 現在流行的property-based testing就是在做這件事：開發者寫下期望成立的性質，用隨機輸入去檢驗。形式化驗證是這條路的終點：同樣的性質，不用測試，直接證明，覆蓋所有可能的輸入。
然後他提出了一個更關鍵的觀察：一個低效的程序本身就可以當規格說明。 你可以用最樸素、最慢、最容易理解的方式寫出"我想要什麼"，然後讓AI生成高效版本，並證明高效版本與樸素版本等價。
這消除了"規格說明太難寫"的顧慮。寫一個低效的正確程序通常遠比寫一個高效的程序容易，因為高效版本里充滿了你不敢隨便改的巧妙技巧。有了證明，你可以讓AI放手優化，因為任何優化都必須通過"和樸素版本等價"這道關卡。
Lean在數學領域的突破比軟體驗證更早引起公眾注意。
2024年，DeepMind的AlphaProof用Lean獲得國際數學奧林匹克（IMO）銀牌。當時整個社區覺得這已經是了不起的成就。到2025年，Harmonic的Aristotle系統、ByteDance的Seed-Prover都用Lean的形式化證明拿到了金牌水平。de Moura說他幾年前認為在IMO拿金牌不可能，"現在大家把它當作簡單問題的基準"。ByteDance參與這件事尤其讓他意外：他之前不知道TikTok背後的公司有一個形式化數學團隊。
AI把Lean當成一個遊戲來玩。Lean有一種叫tactic模式的證明書寫方式，輸入一個"by"關鍵字就進入這個模式。用戶在這種模式下逐步對證明狀態施加變換，比如"簡化當前目標""應用某條已知規則"，每一步操作後螢幕右側的info view會立刻刷新，告訴你還剩什麼需要證明。目標是讓"剩餘目標"歸零。AI通過強化學習不斷嘗試步驟，觀察狀態變化，就像下棋一樣。有用戶告訴de Moura："你給我造了我最喜歡的電腦遊戲。"
更早的一次標誌性事件發生在2020年。Fields獎得主Peter Scholze有一個他自己都不確定是否正確的結果，這是他認為自己職業生涯中最重要的成果之一，但他一直沒有發表，因為沒有十足把握。他把它交給Lean社區，由Johan Commelin領導的團隊完成了形式化驗證，還在不完全理解證明的情況下簡化了它。
de Moura把這比作代碼重構：你開始修改代碼，程序變快了，但你不完全理解為什麼。團隊有直覺，有info view的持續反饋，一步步推進。這個項目讓數學界意識到形式化是一種強大的協作工具：你不需要信任別人的證明，他們可以為你填補空白，Lean的核心會替你檢查一切。此後，Fields獎得主陶哲軒（Terence Tao）也開始使用Lean。他第一次用完說"我大概不會再用了"，一周後就開了第二個項目。
2026年5月，OpenAI宣布其模型反駁了Erdos的單位距離猜想。Kim Morrison隨即在Lean社區的挑戰平台上發布了形式化挑戰。OpenAI的Boris Alexeev用Sol模型完成了完整的形式化，整個證明（含所有依賴庫）約100萬行代碼，從挑戰發布到完成大約兩周。de Moura強調，這個底層需要的數學基礎設施（代數數論等內容）在過去需要專家花幾個月手動形式化。到8月1日，OpenAI的Astra模型又把這個範式推得更遠：10個橫跨8個領域的開放問題，每一個都帶Lean 4證明證書。
但de Moura對AI在數學中的能力邊界說得直接：AI可以找到已有問題的新證明路徑，可以反駁猜想，但還沒有證據表明它能提出新的數學概念。 Lean社區的挑戰平台上有一些要求AI自己構造數學對象的題目，這仍然處於能力邊界。他不願意打賭說AI永遠做不到，但截至目前，證據還沒有。
de Moura在創建Lean之前，花了近20年時間打造Z3 SMT求解器。Z3是一種可滿足性模理論求解器，可以理解為增強版的SAT求解器，在布爾邏輯之上加了對算術、數組等理論的支持。你可以把一個數獨問題編碼成一組約束扔給Z3，它會瞬間給出答案。
Z3和Lean都被歸類為定理證明器，但它們完全不同。Z3是全自動的、推按鈕式的：你給它一組約束，它要麼說"不可滿足"（意思是不可能），要麼給你一個反例。用戶無法控制Z3的推理過程。Lean是交互式的：用戶或AI可以逐步控制證明的每一步。
Z3在找bug方面非常成功。比如你知道程序里有一條路徑存在安全漏洞，但不知道什麼輸入能觸發它。把這條路徑轉化成約束集合扔給Z3，Z3會告訴你：要麼這條路徑不可達（你安全了），要麼給你一組具體輸入說"用這個就能觸發"。
但對於證明bug不存在，Z3不夠用。一旦性質涉及全稱量詞和複雜前後條件，Z3的啟發式規則就會失敗或超時。de Moura在這裡做了一個區分：程序和硬體之所以正確，原因通常很簡單，沒什麼深奧的，這就是為什麼自動化工具在實際的硬體驗證和有界檢查中效果很好。 但一旦要證明通用性質，問題變成不可判定的，自動化工具就力不從心了。
Lean誕生的直接原因就是這個局限。
另一個致命問題是"證明不穩定性"。de Moura提到一位Amazon同事的工作：用Z3類的自動化工具維護證明時，僅僅把公式A∧B改寫成B∧A就可能導致證明失敗。你什麼實質內容都沒改，只是調換了兩個條件的順序，證明就崩了。在Lean中，因為用戶（或AI）控制著證明的每一步，這個問題消失了。那位同事切換到Lean之後，維護體驗"super smooth"。
AI在這裡帶來的驚喜是：過去只有人類能分步驟解釋"為什麼某件事是對的"，現在AI也能做到。它可以一步步說服Lean某件事成立，提供完整的證明項。Z3隻能給你一個結論（行或不行），Lean可以給你整條推理鏈。
，我們不玩
Lean在設計之初面臨一個根本選擇：用高階邏輯（higher-order logic）還是依賴類型理論。高階邏輯實現起來簡單得多，de Moura最初傾向於這個方向。
Carnegie Mellon的哲學與數學科學教授、Lean早期核心貢獻者Jeremy Avigad說服了他。Avigad的論點是：如果想吸引Fields獎級別的數學家，高階邏輯行不通。高階邏輯適合具體數學，但處理抽象對象時必須用編碼技巧來模擬，結果一團糟。de Moura說他跟陶哲軒、Kevin Buzzard、Patrick Massot等數學家交流時，沒有一個人認為高階邏輯夠用，"None. I mean, you talk to Terence Tao, Jeremy, Kevin Buzzard, Patrick Massot, they would say, 'No, no, you have to do the dependent type theory.'"
依賴類型的核心思想可以用一個例子說清楚。假設你有一個結構體，裡面有欄位x和y都是整數。在依賴類型理論中，你可以加第三個欄位，它的類型是"x > y的證明"。這意味著你不可能構造這個結構體的實例，除非你同時提供x確實大於y的證據。不變量直接嵌入類型系統，不需要額外發明。
這在函數簽名里也一樣。一個除法函數可以要求調用者提供"除數不等於零"的證明。沒有這個證據，函數就無法被調用，不是運行時報錯，而是編譯時就過不了。
過去人們嫌提供這些證明太煩。但AI出現後，情況變了：AI可以自動合成這些類型層面的證明。 依賴類型理論從"理論上優美但實踐中煩人"變成了"理論上優美而且AI替你做煩人的部分"。
de Moura說，這是他從用戶那裡學到的最重要的教訓之一。聽用戶說什麼，比堅持自己的技術偏好重要得多。 如果你想吸引某個社區，你必須提供他們真正需要的東西。說"高階邏輯對數學也夠用"在技術上或許有道理，但數學家們不這麼認為，這就夠了。
Lean有一個特性，在編程語言中不多見：它的所有工具鏈都用Lean自身實現。編譯器、構建系統Lake、文檔系統Verso、LSP伺服器，全部是Lean代碼。這叫自舉（self-hosting），從C++切換到Lean自舉的過程是de Moura職業生涯中最痛苦的技術挑戰。
大約10萬行代碼需要用Lean自身的最基礎特性重寫。你從第一個文件開始編譯，失敗了，修bug，編譯通過，第二個文件又失敗了。整個過程就是不斷發現新舊實現之間的差異並逐個解決。Lean的依賴類型系統意味著某些基礎證明你必須手動構造，沒有任何交互工具幫忙，幾乎像是在寫匯編語言。
當他終於成功編譯了Lean的那一刻，他說自己差點想哭。 他打電話給聯合創始人Sebastian Ullrich說"Wow, man. This is insane."問Sebastian激不激動，Sebastian說"Yes, I am. I am." 很多人認為他們不可能完成這件事。
但自舉帶來的回報是極端的可擴展性。因為Lean的所有組件（解析器、宏系統、編譯器、策略框架）都是Lean代碼，用戶可以用同一門語言去操作和擴展這些組件。你可以在寫數學證明的過程中，在同一個文件里寫一段元程序來自動化某個步驟。AI也會利用這一點：如果你讓AI調試一個Lean文件，它會自己寫Lean元程序來驗證它關於問題原因的猜想。de Moura說看到這種行為時覺得"crazy"。
這種可擴展性產生了一些令人意外的項目。Patrick Massot是巴黎-薩克雷大學的數學家，不是電腦科學家。他用Lean的擴展機制創建了Verbose Lean，一種用受控自然語言（英文或法文）寫證明的教學系統，還加入了點擊式界面，學生可以點擊螢幕上的選項來推進證明，看上去完全像一本教科書。他完成整個項目沒有問過de Moura任何問題。
類似的例子還有協議驗證領域的Veil，它在Lean之上嵌入了一套協議驗證專用語言，打開後感覺像是一個完全不同的系統，但底層只是一個帶擴展的Lean文件。開發團隊唯一一次聯繫de Moura是說"能不能讓Lean的某個環節跑快一點"。
在工業端，Lean作為編程語言的最大規模實踐在AWS內部：一個用於AI加速器的編譯器，50萬行Lean代碼。這個項目主要把Lean當編程語言用，順帶證明一些程序性質。de Moura把這些證明叫做"bonus"：你不是為了證明而寫Lean，你是為了寫程序而寫Lean，但證明這件事自然而然就可以做了。
在數學一側，Lean的數學庫Mathlib是目前最大的形式化數學庫。要陳述一個開放猜想，你需要庫里有相應的概念定義。比如IMO的題目用到實數，Mathlib里有實數的完整定義。Mathlib目前距離覆蓋現代研究級數學的全部定義只差不到1000個。
社區也是競爭力的一部分。在AI普及之前，用戶在Lean的Zulip聊天頻道提問，通常五分鐘內就能得到答案。de Moura引用有人開玩笑說的"human-based AI"來形容這種響應速度。Lean的早期核心用戶Jeremy Avigad曾經跟de Moura說：任何他請求的新功能，當天就能拿到。 這種響應速度是社區增長的重要原因。
de Moura對Lean和形式化驗證的未來給了三個判斷。
第一，數學驗證和軟體驗證的技術挑戰方向相反。 在數學中，聲明通常簡短，但證明可能極長極深。Erdos單位距離猜想的反例就是這樣：問題本身一句話就能說清楚，但證明要100萬行代碼。在軟體驗證中，規格說明往往龐大（因為程序複雜），但每一條性質的證明通常淺，因為程序正確的原因大多不複雜。Lean需要在可擴展性上同時滿足這兩個方向。
第二，大型AI實驗室認真訓練Lean是最近的事。 在此之前，Lean只是"碰巧在數據集裡"，沒有針對性的強化學習管線。現在看到的成果已經令人驚嘆，但未來會好得多。de Moura預測，Lean和同類型的語言（比如Rocq）會因此變得更主流。很多人過去說"函數式編程我不喜歡"，但如果大部分代碼都不是你自己寫的，代碼長什麼樣其實不重要，重要的是規格說明層面的表達力。
第三，手寫數學不會消失，但混合工作流會成為常態。 de Moura用了一個比喻：就像有了機器製造家具之後仍然有人喜歡手工打磨，手寫證明作為溝通和教學工具會繼續存在。但完全不在工作流中使用AI的人會越來越少。
他自己已經不寫測試了。"I'm not writing tests anymore. I'm writing properties and proving them. The AI is proving most of them for me." 他覺得"寫代碼"這件事裡，有趣的部分是原型設計，嘗試新想法。把原型變成產品從來都不有趣。AI可以接管這些不有趣的部分，沒有人真正喜歡做那些事。
人類在這個未來中的角色是寫接口：告訴AI我們想要什麼（規格說明），理解AI生成的數學庫中的抽象，確保整個系統與現實世界的需求對齊。規格說明會一直存在，人類會一直在那個界面上。
他給想學Lean的人的建議是直接跟AI對話。很多人現在把螢幕分成三塊：Lean代碼、info view、底部的AI智能體。AI在寫代碼的同時用自然語言解釋發生了什麼。陶哲軒早期學Lean時還是手動在ChatGPT窗口和VS Code之間複製粘貼，現在有了AI智能體效率更高了。lean-lang.org上有多本入門書籍，包括函數式編程、定理證明和數學三個方向。
被問到如果能回到過去給自己一個建議會說什麼，de Moura笑著說他寧願保密。"Ignorance is a bliss." 不知道事情有多難，反而敢開始。不過他還是給出了一條：我是個極度內向的人，我會告訴年輕時的自己，練好跟人打交道的能力。 當你要跟一個社區互動的時候，這比你以為的重要得多。
Q1: Lean到底是什麼，跟普通編程語言有什麼區別？Lean是一門編程語言，同時也是一個證明助手。你可以用它寫程序，也可以用它寫數學證明，而且Lean會自動檢查你的證明是否正確。跟普通編程語言的關鍵區別是：Lean基於依賴類型理論，類型可以依賴於值，這意味著你可以在類型簽名里直接表達"這個函數的輸入必須滿足某種條件"這樣的約束，編譯器會在編譯時強制你提供證據。這讓"寫出有bug的程序"在某些情況下變得不可能，因為類型檢查通不過。
Q2: AI在形式化驗證中到底解決了什麼問題？解決的是證明的開發和維護。規格說明（你想要程序滿足什麼性質）仍然需要人來寫，但它從來不是最痛苦的部分。最痛苦的是手工構造證明和在代碼變動時修補證明。seL4微核心的驗證花了20人年，主要成本在這裡。AI可以在幾秒內完成同類任務，而且質量穩定。Kim Morrison用AI在一周內完成了zlib壓縮庫的翻譯和關鍵性質證明。這把形式化驗證的成本從"10倍於寫程序"降低到可能接近寫測試的水平。
Q3: de Moura同時創造了Z3和Lean，這兩個工具有什麼本質區別？Z3是全自動的約束求解器：你按一個按鈕，要麼得到答案，要麼超時，無法控制推理過程。它擅長找bug（給一個路徑，問能不能走到），但證明bug不存在時經常失敗或超時。Lean是交互式的：用戶或AI可以逐步控制證明的每一步。Z3還有一個"證明不穩定性"的問題：僅僅調換公式兩個子句的順序就可能導致證明失敗。Lean因為每一步都是顯式的，沒有這個問題。Lean誕生的直接原因就是Z3在證明軟體正確性方面的局限。
