Lean是一種由Leonardo de Moura主導開發的開源函式式程式語言和互動式定理證明器（即證明輔助工具）。它是一款免費、開源的軟體，支持Linux、Windows和MacOS系統。2021年1月發布的Lean 4版本進行了編譯器、錯誤處理等方面的最佳化。
其核心社區項目是數學庫mathlib，這是一個社區驅動的、旨在構建統一形式化數學知識庫的努力。該項目已包含超過12萬個定義和25萬個定理，並已獲得超過1000萬美元的資金支持。Lean及其mathlib已被用於形式化多個數學猜想和定理，如多項式Freiman-Ruzsa猜想於2023年11月宣布解決並在三周內完成形式化。陶哲軒等人還於2024年啟動了使用Lean對素數定理進行形式化證明的項目。基於Lean 4構建的形式驗證最佳化器AMO-Lean等項目展示了其在計算機科學領域的套用，AMO-Lean於2026年被發布。AI輔助工具如Lean Copilot能幫助自動化部分證明步驟，提升了形式化研究的效率。在商業套用與初創生態方面，基於Lean語言的形式化驗證技術開始套用於AI系統和金融領域，推動了相關初創公司的發展。
基本介紹
- 中文名：Lean語言
- 外文名：Lean
- 產品類型：函式式程式語言、互動式定理證明器
- 上市時間：2021年1月
研發背景,發展歷程,運營模式,核心團隊,重要事件,
研發背景
Lean是一種由Leonardo de Moura主導開發的開源定理證明器（證明助手）和函式式程式語言，旨在為數學陳述和證明提供形式化語言並進行自動驗證。其開發思想源於20世紀初以來對數學基礎的形式化追求，即認識到數學陳述可以用形式語言表達，數學證明可以用具有精確規則和語義的形式演繹系統來表示。
Leonardo de Moura是Lean的主要創始人和開發者。其重要版本Lean 4於2021年1月發布。
發展歷程
Lean定理證明器（Lean theorem prover）由Leonardo de Moura主導開發，是一款免費、開源、支持多平台（Linux, Windows, MacOS）的證明輔助工具和函式式程式語言。
Lean 4於2021年1月發布，相比初代版本進行了多項最佳化，包括更快的編譯器、改進的錯誤處理和更好的與外部工具集成的能力。
其核心數學庫mathlib是一個由用戶維護的庫，社區使用mathport工具將整個mathlib從Lean 3遷移到了Lean 4，當前教程和庫已基於Lean 4和Mathlib4。
使用Lean和mathlib完成的重要形式化成果包括多項式Freiman-Ruzsa猜想，該猜想於2023年11月宣布解決並在三周內完成形式化；以及完美胚空間的定義和定理形式化。
基於Lean 4構建的形式驗證最佳化器AMO-Lean，能夠將用Lean 4編寫的數學規範轉換為最佳化後的C和Rust代碼。
運營模式
Lean是一款免費、開源軟體，其開發與維護採用社區驅動的模式。其核心社區主要聚集在Zulip聊天平台和GitHub上進行協作、討論與技術支持。
社區的核心項目是數學庫mathlib，這是一個由全球用戶共同維護的、旨在構建統一形式化數學知識庫的社區驅動項目。mathlib有詳細的貢獻指南、代碼風格規範和命名約定，社區成員可以通過提交Pull Request的方式參與貢獻，並在Zulip頻道進行項目規劃與討論。
項目的治理模式傾向於民主協商，類似維基百科，由一個專注的維護者團隊引導，負責確定庫的定義納入與編碼方式，決策過程基本保持民主。該項目已獲得超過1000萬美元的資金支持，大部分來自億萬富翁金融家阿列克謝·格爾科（Alex Gerko），部分核心維護者因此得以全職投入工作。
核心團隊
Lean 證明助手由 Leonardo de Moura 主導開發並創立。
圍繞 Lean 和其數學庫 mathlib 形成了一個活躍、多元的社區，由眾多數學家、計算機科學家和愛好者共同維護與推動，有多位數學家負責維護這一資料庫並審核新的研究成果。社區成員主要聚集在 Zulip 聊天平台和 GitHub 上進行協作與討論。
社區中湧現了許多對重要形式化項目做出關鍵貢獻的數學家，例如倫敦帝國理工學院的凱文·巴扎德長期致力於用 Lean 對費馬大定理的證明進行形式化處理；約翰·科梅林和派屈克·馬索等人領導了“完美胚空間”理論的形式化驗證工作。
重要事件
Lean社區在形式化數學、工具生態建設及教育推廣等多個方面取得了重要進展。
在數學成果形式化方面，Lean社區完成了一系列代表性工作。這些成果包括多項式Freiman-Ruzsa猜想，該猜想於2023年由陶哲軒等人解決並迅速完成了形式化驗證。其他形式化成果還包括連續統假設獨立性、完美胚空間定義、球面外翻定理以及帽子集問題，涵蓋了組合數學、集合論、算術幾何和微分拓撲等多個數學分支。2020年末至2021年，數學家彼得·舒爾茨的一個複雜定理證明也通過Lean完成了形式化驗證，增強了數學界對該理論的信心，並在此過程中最佳化了原證明。陶哲軒等人還於2024年啟動了使用Lean對素數定理進行形式化證明的項目。
在教育套用與推廣方面，出現了《Mathematics in Lean》等教程，推動了Lean在數學教育特別是本科教學中的套用。
在工具生態與發展方面，社區驅動的核心數學庫mathlib完成了從Lean 3到Lean 4的遷移和持續開發。2026年，基於Lean 4構建的、經過形式驗證的最佳化器AMO-Lean被發布。此外，諸如Lean Copilot等AI輔助工具能夠自動化部分證明步驟，提升了形式化研究的效率。
在社區與資金支持方面，旨在將所有數學內容形式化的項目獲得了超過1000萬美元的資金支持。
在商業套用與初創生態方面，基於Lean語言的形式化驗證技術開始套用於AI系統和金融領域，推動了相關初創公司的發展。例如，初創公司Axiom利用Lean開發AI數學家系統，其技術可服務於對沖基金和量化交易公司，並獲得了投資。2025年12月，Axiom核心繫統AxiomProver在普特南數學競賽中完成全部12道試題並取得滿分。2026年3月，Axiom完成2億美元A輪融資，估值達110億元（約16億美元），躋身獨角獸行列。Axiom由洪樂潼創立，在2024年至2026年間獲得了多輪融資，並吸引了包括數學家小野健在內的核心團隊加入。同月（2025年12月），公司創始人洪樂潼入選“福布斯30歲以下30人”榜單。
