精益Mathlib 4文档搜索MCP服务器
该项目提供了一个用于搜索Lean Mathlib 4文档的最小MCP（模型上下文协议）服务器。它允许LLM查询Lean Mathlib 4声明并检索相关文档链接和详细信息。MCP服务器目前仅适用于VSCode。
特性
- 搜索精益Mathlib 4文档：查询文档中的声明、模块和实例。
- MCP服务器集成：实现MCP协议，与工具无缝集成。
- 本地数据处理：首次运行后，在本地下载和处理Lean Mathlib 4文档数据。
先决条件
- Python 3.11或更高版本
requests图书馆mcpMCP服务器库
安装
- 克隆存储库：
git clone https://github.com/CriticalLine/lean-mathlib-docs-mcp.git
cd lean-mathlib-docs-mcp- 安装所需的Python依赖项：
conda env create -f environment.yml
conda activate lean-mathlib-docs-env- 确保
mcp.json文件在中配置正确.vscode文件夹或项目根目录。
用法
- 当您使用适当的配置启动MCP服务器时，VSCode将自动启动它。
- 通过显式使用查询服务器
#search_lean_doc或者告诉LLM使用搜索功能。
项目结构
lean-mathlib-docs-mcp/
├── LICENSE
├── README.md
├── src/
│ ├── lean_docs_server.py
│ └── mcp.json发展
- 测试mcp服务器
- 添加检查原始代码
许可证
该项目根据GPLv3许可证获得许可。请参阅 LICENSE 文件以获取详细信息。 禁止一切商业用途。
致谢
- 精益数学库4 对于文档数据。
- 用于提供协议实现的MCP服务器库。