lean-mathlib-docs-mcp

🚀 Lean Mathlib 4 文档搜索 MCP 服务器

本项目提供了一个用于搜索 Lean Mathlib 4 文档的最小 MCP（模型上下文协议）服务器。它允许大语言模型（LLMs）查询 Lean Mathlib 4 的声明，并获取相关的文档链接和详细信息。目前，该 MCP 服务器仅支持 VSCode。

🚀 快速开始

本项目提供的 MCP 服务器可让你轻松搜索 Lean Mathlib 4 文档。按以下步骤操作，即可开启搜索之旅。

✨ 主要特性

• 搜索 Lean Mathlib 4 文档：可查询声明、模块和实例的文档。
• MCP 服务器集成：实现了 MCP 协议，可与工具无缝集成。
• 本地数据处理：首次运行后，会在本地下载并处理 Lean Mathlib 4 文档数据。

📦 安装指南

环境要求

• Python 3.11 或更高版本
• requests 库
• mcp MCP 服务器库

安装步骤

1. 克隆仓库：

git clone https://github.com/CriticalLine/lean-mathlib-docs-mcp.git
cd lean-mathlib-docs-mcp

2. 安装所需的 Python 依赖项：

conda env create -f environment.yml
conda activate lean-mathlib-docs-env

3. 确保 .vscode 文件夹或项目根目录中的 mcp.json 文件配置正确。

💻 使用示例

基础用法

1. 使用适当的配置启动 VSCode 后，它将自动启动 MCP 服务器。
2. 你可以通过显式使用 #search_lean_doc <查询内容> 来查询服务器，或者告知大语言模型使用搜索功能。

📚 详细文档

项目结构

lean-mathlib-docs-mcp/
├── LICENSE
├── README.md
├── src/
│   ├── lean_docs_server.py
│   └── mcp.json

开发相关

• 测试 MCP 服务器
• 检查原始代码

📄 许可证

本项目采用 GPLv3 许可证。详情请参阅 LICENSE 文件。本项目禁止一切商业用途。

🙏 致谢

• Lean Mathlib 4 提供了文档数据。
• MCP 服务器库提供了协议实现。