Lean 4

Lean 4是微軟研究院在2013年推出的Lean定理證明器於2021年發布的新版本，是該定理證明器的重新實現，它是一種兼具通用函式式程式語言和互動式定理證明器特性的形式化驗證工具。其核心團隊由創始人Leonardo de Moura領導，他是Z3 SMT求解器和Lean定理證明器的締造者。

在數學研究領域，Lean 4被用於對數學定理進行嚴格的形式化驗證，例如2026年北京大學AI4Math團隊利用其完成了交換代數中Anderson猜想約19000行的形式化驗證，並開發了LeanSearch等輔助工具。圍繞Lean形成了活躍的開源社區，其核心基礎設施Mathlib數學庫包含了數十萬條定理和定義。在軟體工程領域，Lean 4被套用於驗證軟體的正確性與安全屬性，如2024年AWS團隊驗證其開源授權策略語言Cedar。2026年，首個面向Lean 4的開原始碼智慧型體出現，用於輔助自動化代碼生成與證明補全。Lean 4擁有線上版本和計算機版本，可通過Visual Studio及其Lean 4擴展設定使用，社區在Zulip上組織交流。

基本介紹

• 外文名：Lean 4

研發背景

Lean是微軟研究院在2013年推出的計算機定理證明器。Lean 4於2021年發布（具體為2021年1月），它既是函式式程式語言，也是互動式定理證明器，能夠生成C代碼後進行編譯，以便開發高效的特定領域自動化。Leonardo de Moura是Z3 SMT求解器和Lean定理證明器的締造者。

發展歷程

Lean是微軟研究院在2013年推出的計算機定理證明器。Lean 4於2021年發布，是Lean定理證明器的重新實現，能夠生成C代碼後進行編譯，以便開發高效的特定領域自動化。圍繞Lean形成了活躍的開源社區，其核心基礎設施Mathlib數學庫包含了數十萬條定理和定義，支撐著大規模的形式化驗證工作。2024年，AWS團隊在開發Cedar授權策略語言時，採用Lean驗證其正確性和安全屬性。同年，一篇關於在Lean 4中形式化集合論與初等代數的論文在IEEE會議上發表，展示了Lean 4在數學基礎形式化方面的套用。2026年，北京大學AI4Math團隊利用自主構建的自動化AI框架Archon解決了交換代數中的Anderson猜想，並在Lean 4中完成了約19,000行的形式化驗證。團隊開發的LeanSearch工具被Lean官方社區廣泛使用。Lean的締造者Leonardo de Moura構想了構建一整套經過數學證明的開源軟體棧的願景。

核心團隊

Lean 4的核心團隊由創始人Leonardo de Moura領導，他是Z3 SMT求解器和Lean定理證明器的締造者，現任AWS高級首席套用科學家、Lean FRO首席架構師。其他關鍵成員包括微軟研究院的研究軟體工程師Gabriel Ebner以及Lean FRO的高級研究軟體工程師Kim Morrison。該團隊最初依託於微軟研究院。

重要事件

2026年，北京大學AI4Math團隊使用Lean 4完成了交換代數中Anderson猜想的形式化驗證，共編寫約19,000行Lean 4代碼，並開發了LeanSearch等輔助工具。

該團隊使用其構建的自動化AI框架Archon將證明轉化為代碼，並在過程中發現了初始方案中的邏輯漏洞，重新設計了形式化證明的技術路線。當所需數學概念在Lean形式化數學庫中未被收錄時，團隊找到了替代路徑。最終完成的代碼覆蓋了6篇外部論文的關鍵結果，其工作效率相較於經驗豐富的Lean專家有所提升。團隊開發的輔助工具LeanSearch能夠根據自然語言描述進行語義檢索，該工具在Lean社區中得到套用。

2026年，出現了首個面向Lean 4的開原始碼智慧型體，旨在自動化代碼生成、證明補全等任務。

2024年，AWS團隊使用Lean證明助手驗證其開源授權策略語言Cedar的正確性與安全屬性。