让数学家轻松搜索Lean 4代码声明，支持语义与关键词混合检索。
LeanExplore: A search engine for Lean 4 declarations
- 融合形式化代码、文档、AI翻译等多源语义嵌入，实现精准语义搜索
- 采用混合排序策略，结合语义得分、关键词匹配和声明重要性评分
- 支持网页端、Python API及本地部署，可与大模型无缝集成
随着Lean 4生态持续扩展，其庞大库的导航变得愈发困难。本文提出LeanExplore，一个针对Lean 4声明的搜索引擎。该系统支持在多个核心包（包括Batteries、Init、Lean、Mathlib、PhysLean和Std）中进行形式化与非形式化的语义搜索。搜索能力基于混合排名策略：整合多源语义嵌入模型（捕捉形式代码、文档字符串、AI生成的自然语言翻译及声明标题的语义）、BM25+关键词匹配，以及基于PageRank的声明重要性与关联度评分。用户可通过官网（https://www.leanexplore.com/）或Python API（https://github.com/justincasher/lean-explore）访问服务，亦可下载数据库自行部署。系统支持通过模型上下文协议（MCP）与大模型集成，可用于与AI助手对话或构建自动定理证明代理。本文详述了其架构、数据处理流程、功能特性及其对提升Lean 4工作流与人工智能驱动数学研究的潜力。
原文摘要 · Abstract (English)
The expanding Lean 4 ecosystem poses challenges for navigating its vast libraries. This paper introduces LeanExplore, a search engine for Lean 4 declarations. LeanExplore enables users to semantically search for statements, both formally and informally, across select Lean 4 packages (including Batteries, Init, Lean, Mathlib, PhysLean, and Std). This search capability is powered by a hybrid ranking strategy, integrating scores from a multi-source semantic embedding model (capturing conceptual meaning from formal Lean code, docstrings, AI-generated informal translations, and declaration titles), BM25+ for keyword-based lexical relevance, and a PageRank-based score reflecting declaration importance and interconnectedness. The search engine is accessible via a dedicated website (https://www.leanexplore.com/) and a Python API (https://github.com/justincasher/lean-explore). Furthermore, the database can be downloaded, allowing users to self-host the service. LeanExplore integrates easily with LLMs via the model context protocol (MCP), enabling users to chat with an AI assistant about Lean declarations or utilize the search engine for building theorem-proving agents. This work details LeanExplore's architecture, data processing, functionalities, and its potential to enhance Lean 4 workflows and AI-driven mathematical research
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。