Description

Enables searching through Lean Mathlib 4 documentation by downloading and parsing declaration data from the official Lean community documentation site. Provides regex-based search functionality to find theorems, definitions, and other mathematical constructs by name, returning formatted results with documentation links and type information. Designed for mathematicians and formal verification practitioners working with Lean who need quick access to Mathlib's extensive library of mathematical formalization.

Installation

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

Claude Desktop Configuration

Add this configuration to your Claude Desktop config file to enable this MCP server:

Config file location: ~/Library/Application Support/Claude/claude_desktop_config.json

Config file location: %APPDATA%\Claude\claude_desktop_config.json

Config file location: ~/.config/Claude/claude_desktop_config.json

claude_desktop_config.json

{
  "mcpServers": {
    "lean-mathlib-4-documentation": {
      "command": "node",
      "args": [
        "path/to/server.js"
      ]
    }
  }
}