LeanSearch是一個語義搜尋引擎，由北京大學AI4Math團隊構建，於2026年4月6日提出。該引擎允許用戶使用自然語言描述需求，語義檢索出相關的定理。現已被Lean官方社區廣泛使用，API日均調用超過8000次。
研發背景,發展歷程,核心技術,運營模式,核心團隊,重要事件,
研發背景
LeanSearch的研發旨在探索人工智慧（AI）在數學形式化證明中的套用，將AI的理解能力延伸至數學領域。
其初衷是為了解決在Lean定理證明環境中，使用自然語言高效檢索相關定理和策略的難題。
發展歷程
2025年8月，相關工具LeanSearchClient發布，它提供了從Lean內部使用自然語言搜尋定理和策略的語法，支持leansearch等多個後端API。
2025年12月，獨立的LeanSearch語義搜尋引擎項目出現，這是一個專為Lean 4項目設計的語義搜尋引擎，通過將形式化陳述轉化為自然語言描述並生成嵌入向量來實現搜尋功能。
2026年4月6日，北京大學AI4Math團隊正式打造了由LeanSearch與Matlas構成的雙引擎檢索架構。其中，LeanSearch專注於形式化數學世界的語義檢索。
核心技術
LeanSearch的核心技術創新在於採用了“形式化（LeanSearch）+非形式化（Matlas）”雙引擎檢索架構。這種雙引擎架構是該框架區別於其他AI數學系統的核心特色。
其實現語義搜尋的關鍵技術環節包括利用大語言模型將形式化語句翻譯為自然語言描述，以及使用嵌入模型生成查詢和知識庫內容的文本向量，並通過相似度計算實現語義匹配。LeanSearch允許用戶使用自然語言搜尋Lean策略和定理，現已被Lean官方社區廣泛使用。
運營模式
LeanSearch現已被Lean官方社區廣泛使用，其API日均調用超過8000次。
在技術運營上，LeanSearch支持配置不同的後端搜尋服務，例如leansearch API、Moogle API以及LeanStateSearch API，具體使用哪個後端由leansearchclient.backend選項決定。
核心團隊
該團隊致力於將人工智慧的理解能力延伸至數學這一科學的核心語言，構建了LeanSearch和Matlas兩套檢索系統。
重要事件
2026年4月6日，北京大學AI4Math團隊打造了雙引擎檢索架構——LeanSearch和Matlas。LeanSearch作為該架構的關鍵組件，助力實現了“國內首次由AI自主解決數學開放問題並完成大規模形式化驗證”。
LeanSearch用自然語言描述需求即可語義檢索出相關定理，現已被Lean官方社區廣泛使用，API日均調用超過8000次。其與Matlas構成的雙引擎架構也成為相關AI數學系統的核心特色。
