lake check 是什麼
Lean 是一套證明輔助工具，「核心」（kernel）負責最後檢查每一個證明是否正確。Lean FRO 共同創辦人 Leonardo de Moura 在 2026 年 10 月 15 日的文章指出，AI 代理很擅長找出軟體漏洞，也包括 Lean 的核心，因此團隊正在強化官方核心、加入新核心，並讓使用者更容易用外部核心重新檢查自己的專案。
依 2026 年 10 月 12 日的 Lean 4.35.0 版本說明，新指令 lake check 會建置專案、匯出後交給核心重新檢查，並在用到標準公理以外的公理時失敗。整個過程在 bubblewrap 沙盒中執行（目前只支援 Linux）。
| 指令 | 作用 |
|---|---|
| lake check | 用 Lean 官方核心檢查，只允許標準公理 |
| lake check --paranoid | 再加上所有內建的外部檢查器，全部通過才算通過 |
工具鏈現在內建 lean4lean、nanoda、con-leche、con-ron 四個外部核心，以及用強化記憶體配置器建置、把記憶體損壞轉成明確中止的 leanchecker-paranoid。
Claude 寫的核心
con-leche 是第一個用 Lean 撰寫、並證明具一致性的 Lean 核心。GitHub 專案說明寫道，它由 Claude（Fable 與 Opus）實作並完成一致性證明，過程在 Lean FRO 的 Joachim Breitner 嚴密監督下進行，git 歷史保留了所有繞路與死胡同。
這裡的「一致性」是指 con-leche 接受的每個環境，在集合論中都有對應的模型，沿用 Mario Carneiro 對 Lean 型別理論的模型。證明本身由官方核心檢查。de Moura 表示，這種做法排除了一整類錯誤，也就是核心實作上的程式錯誤，而且沒有效能代價：在完整 Mathlib 匯出上，con-leche 執行的指令數是官方核心的 0.69 倍，用 8 個執行緒約 100 秒就能檢查完整個函式庫。
仍非萬無一失
官方文章直接寫明 con-leche 並非萬無一失，限制有兩層：
- 一致性證明有前提：它假設模型所用的集合論本身是一致的。
- 編譯器與執行環境可能有錯：建置 con-leche 用的 Lean 編譯器與執行環境（包括大數函式庫）仍可能有漏洞。
為降低第二種風險，Joachim 用 AI 把 con-leche 翻譯成 Rust，再用 Aeneas 證明 Rust 版本精化了 con-leche 的檢查演算法，這個版本稱為 con-ron。de Moura 的說法是，同一個漏洞同時出現在 Lean 與 Rust 的編譯器或執行環境的可能性很低，兩者都檢查一次能提供高度保護。團隊預計未來幾個月完成 lean4lean 的驗證，屆時發行版將有三個驗證過的核心。
我們的解讀：這是 AI 寫程式、人類監督、再用形式化證明把關的實例。如果你在做 Lean 專案，可以先在 Linux 上跑一次 lake check --paranoid；官方也請使用者在核心結果不一致時回報。
