This MCP server provides a local, searchable interface to Lean Mathlib 4 documentation. It downloads and processes the documentation data once and serves search results that include declarations, modules, and instances with links and concise explanations. You can invoke it from an IDE like VSCode via the MCP integration, and use the provided search command to query the documentation. To use it, start your environment with the server script; once the server is running, you can issue queries through the MCP protocol, for example by asking the LLM to call the #search_Lean_doc function with a query related to a Lean declaration or module. The server will return relevant documentation entries and URLs, enabling quick access to the Mathlib docs while composing or validating Lean code.

Available tools and capabilities include: - Full-text search over Lean Mathlib 4 declarations, modules, and instances. - Retrieval of documentation links and brief summaries suitable for embedding in responses. - Local data handling to avoid repeated downloads after the first run. - Seamless MCP protocol integration for tooling and LLMs that support MCP commands.

Prerequisites:

• Python 3.11 or higher
• pip or conda for dependency management
• Basic Git and shell access

Installation steps:

1. Clone the repository: git clone https://github.com/CriticalLine/lean-mathlib-docs-mcp.git cd lean-mathlib-docs-mcp

2. Create and activate a Python environment (recommended): python -m venv venv source venv/bin/activate # Linux/macOS

   Windows: venv\Scripts\activate

3. Install required dependencies (the project uses a requirements file or setup in environment.yml):

   If a requirements.txt exists:

   pip install -r requirements.txt

   If the project provides environment.yml (conda):

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

4. Ensure the MCP server script is ready:

   • Confirm the file src/lean_docs_server.py exists and is configured to run as an MCP server.
   • Ensure a valid mcp.json is present in the .vscode folder or project root as documented by the project.

5. Prepare for running:

   • If needed, install additional dependencies via pip (e.g., requests, mcp) inside your environment.

6. Start the server (as described in the README):

   • Use your IDE to launch the MCP server, or run the Python script directly: python src/lean_docs_server.py

Tips and common issues:

• The server downloads Lean Mathlib 4 documentation data on first run; ensure you have a stable internet connection during the initial setup.
• If the server fails to start, check that Python 3.11+ is being used and that the required libraries (requests, mcp) are installed in the active environment.
• The mcp.json file should be correctly configured either in the project root or under the .vscode folder to enable VSCode integration.
• The MCP command name used by your LLM should align with the server's exposed commands, such as #search_Lean_doc, as documented by the project.
• Since this server is currently VSCode-focused, ensure your tooling environment is configured to use the MCP server protocol within VSCode extensions or other MCP-enabled clients.
• Data handling: after the first run, the server uses locally stored documentation data. If you need to refresh the data, delete the local storage (as documented by the project) and restart the server.