Intro to the Lean Theorem Prover | Jakob von Raumer (Lindy Labs) - DSS 101 2024
三句話摘要
使用 Lean 定理證明系統進行形式化驗證：透過嵌入簡易編程語言演示如何驗證程式正確性。 Lean 透過依賴型別、語法可擴展性與大步語義的結合，成為構建形式驗證工具的理想框架，已被成功應用於智能合約驗證，能提供傳統方法無法達到的數學保證。 Lean 的核心優勢在語法可擴展性與工具整合：Lean 不僅是定理證明系統，更是構建形式驗證工具的框架。其解析器可在執行時擴展，允許無縫整合外部工具與自定義領域特定語言（DSL），這使其成為驗證不同編程語言的理想基礎。
重點整理
重點- 1
Lean 的核心優勢在語法可擴展性與工具整合：Lean 不僅是定理證明系統，更是構建形式驗證工具的框架。其解析器可在執行時擴展，允許無縫整合外部工具與自定義領域特定語言（DSL），這使其成為驗證不同編程語言的理想基礎。
- 2
透過歸納型別與宏規則實現語言嵌入：演講展示如何用 100 多行代碼定義一個 IMP 命令式語言的完整形式語義。透過定義表達式與語句的歸納型別，再用宏規則將表面語法映射至抽象語法樹，實現了高效的語言嵌入方法。
- 3
大步語義（Big-step Semantics）處理不終止程式：由於 Lean 是完全函數式語言，無法直接處理可能無限循環的程式。大步語義使用歸納謂詞定義程式執行關係，允許用結構化的證明技巧（如循環展開）驗證程式行為，即使在迴圈存在時也能證明性質。
- 4
形式驗證在實際 DeFi 合約中的應用：Egis 工具實現了 Cairo 合約的完整驗證流程，已驗證 Lindy Labs 白皮書中的控制論公式。在合理數值範圍內證明了複雜非線性運算的誤差有界，提供傳統測試無法達到的數學保證。
實用技巧與重點
乾貨- 工具與系統：
- Lean：由 Leonardo de Moura 創立（2012年），基於 Calculus of Constructions
- Egis：用於 Cairo/StarkNet 合約驗證的形式化工具
- Sierra：Cairo 的中間表示
- 標準庫：Mathlib（包含 Reservoir 套件）
- 開發環境：Zulip 伺服器（Lean 社群討論中心）
- 成功案例：
- Liquid Tensor Experiment：菲爾茲獎得主證明驗證與簡化
- Amazon AWS：採用 Lean 進行多項任務
- DeepMind Alpha Proof：在國際數學奧林匹克（IMO）上獲銀牌
- IMP 語言語法元素：
- 表達式：常數、變數、加法、小於比較（4 個構造函數）
- 語句：賦值、順序組合、if-then-else、while 迴圈（4 個構造函數）
- 值型別：32 位元位向量
- 上下文：字串到值的映射
- 優化實現：
- 常數折疊（Constant Folding）：預計算純常數表達式
- 驗證方法：證明 `eval σ e = eval σ (optimize e)`
- 大步語義規則：
- 空語句：`⟨σ, skip, σ⟩`
- 赋值：呼叫 `eval` 計算表達式值
- 順序：链接兩個程式的執行
- if-then-else：根據條件分支
- while：循環展開（條件真時遞迴，假時不執行）
- 驗證案例：變數交換
- 程式：`z := i; i := j; j := z`
- 性質：執行後 `σ'(i) = σ(j)` 且 `σ'(j) = σ(i)`
- DeFi 應用：
- 公式：控制理論中的全局利率修正因子（包含指數與平方根）
- 驗證內容：數值誤差在合理變數範圍內有界
結論
結論“Lean 透過依賴型別、語法可擴展性與大步語義的結合，成為構建形式驗證工具的理想框架，已被成功應用於智能合約驗證，能提供傳統方法無法達到的數學保證。”
完整解析
詳細Lean 是 Leonardo de Moura 於 2012 年創立的交互式定理證明系統，過去十多年間已發展成形式化驗證與數學證明的關鍵工具。與純自動證明不同，Lean 採用依賴型別系統，允許函數的返回型別依賴於輸入值，這使得型別系統本身可以表達複雜的數學性質。Lean 既是函數式編程語言，也是定理證明器，其核心用 Lisp 方言編寫並可自我編譯，這種自舉特性使其具備高度可信性與可擴展性。
演講的核心貢獻在於展示如何將任意編程語言嵌入 Lean 作為領域特定語言。講者首先定義了一個名為 IMP 的簡易命令式語言，包含變數賦值、條件語句與 while 迴圈。透過 Lean 的歸納型別系統，講者定義了表達式與語句的抽象語法樹，用構造函數精確描述每一種語言結構。隨後利用 Lean 強大的語法擴展機制，用巨集規則（macro rules）將日常編程語法（如 `x := y + 5`）自動轉譯為內部表示形式，實現了兼具可讀性與形式嚴謹性的編程體驗。
為了賦予程式實際意義，講者導入大步語義（big-step semantics），這是處理可能不終止程式的標準方法。由於 Lean 是完全函數式語言，無法直接定義可能無限循環的求值函數，大步語義改用歸納關係定義程式執行的充要條件：給定起始環境σ、程式 s 和終止環境σ'，歸納謂詞列舉所有可能使程式從σ執行至σ'的情況。對於 while 迴圈，這種方式巧妙地透過循環展開處理任意迭代次數的驗證，使得證明具有模組化與可組合性。
演講實時展示了驗證一個具體程式的過程：交換兩個變數 i 和 j 的程式。證明策略從展開程式定義開始，逐步應用 cases 策略拆解每一行賦值語句，最終呼叫 simplifier 自動驗證最終狀態確實交換了變數值。這個例子雖然簡單，卻完整展示了形式驗證的全貌：從語言定義、語義規則到程式驗證的整個流程。
最後，講者介紹了 Egis 工具的實際應用。Egis 將這套方法論應用於 StarkNet L2 的 Cairo 智能合約驗證。通過 Lean 的可擴展性，Egis 支援加載 Cairo 編譯器生成的中間表示（Sierra），允許合約開發者在 Lean 中為每個函數提供數學規範並自動驗證。Lindy Labs 已使用 Egis 驗證了白皮書中一個複雜的非線性控制公式，證明了在合理數值範圍內，浮點運算的累積誤差有界，這種保證遠超傳統測試與模擬分析。
關鍵時刻
Pipeline v2帶時間戳的重點，會在逐字稿層級分析上線後產生。目前請先透過原始影片觀看。
事實查核
Pipeline v2說法查證是下一次管線升級的一部分。KeyFrame 只會顯示它真正能驗證的內容。
