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 服務器庫提供了協議實現。