Lean LSP

lean-lsp-mcp

Servidor MCP para el Teorema de Lean

Servidor MCP que permite interacción agéntica con el demostrador de teoremas Lean mediante el Protocolo de Servidor de Lenguaje usando leanclient. Este servidor proporciona un conjunto de herramientas para que los agentes LLM comprendan, analicen e interactúen con proyectos Lean.

Características principales

• Interacción rica con Lean: Acceso a diagnósticos, estados de objetivos, información de términos, documentación flotante y más.
• Herramientas de búsqueda externa: Use LeanSearch, Loogle, Lean Finder y Lean Hammer para encontrar teoremas y definiciones relevantes.
• Configuración sencilla: Configuración simple para varios clientes, incluidos VSCode, Cursor y Claude Code.

Configuración

Resumen

1. Instale uv, un administrador de paquetes de Python.
2. Asegúrese de que su proyecto Lean compile rápidamente ejecutando lake build manualmente.
3. Configure su IDE/entorno.
4. (Opcional, muy recomendado) Instale ripgrep (rg) para búsqueda local y escaneo de código fuente (advertencias de lean_verify).

1. Instalar uv

Instale uv para su sistema. En Linux/MacOS: curl -LsSf https://astral.sh/uv/install.sh | sh

1b. Alternativa: Instalar con Nix

Si usa Nix, puede instalar el paquete directamente desde GitHub:

nix profile install github:oOo0oOo/lean-lsp-mcp

O ejecutarlo sin instalarlo: nix run github:oOo0oOo/lean-lsp-mcp.

Esto proporciona solo el servidor MCP. Aún necesita un toolchain de Lean (elan/lake) para su proyecto, igual que en la configuración de uv a continuación.

2. Ejecutar lake build

lean-lsp-mcp ejecutará lake serve en la raíz del proyecto para usar el servidor de lenguaje (para la mayoría de las herramientas). Algunos clientes (por ejemplo, Cursor) pueden agotar el tiempo de espera durante este proceso. Por lo tanto, se recomienda ejecutar lake build manualmente antes de iniciar el MCP. Esto garantiza un tiempo de compilación más rápido y evita tiempos de espera.

3. Configurar su IDE/entorno

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ]
        }
    }
}

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "wsl.exe",
            "args": [
                "uvx",
                "lean-lsp-mcp"
            ]
        }
    }
}

{
    "mcpServers": {
        "lean-lsp": {
            "command": "uvx",
            "args": ["lean-lsp-mcp"]
        }
    }
}

# Local-scoped MCP server
claude mcp add lean-lsp uvx lean-lsp-mcp

# OR project-scoped MCP server
# (creates or updates a .mcp.json file in the current directory)
claude mcp add lean-lsp -s project uvx lean-lsp-mcp

[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

4. Instalar ripgrep (opcional pero recomendado)

Para la herramienta de búsqueda local lean_local_search, instale ripgrep (rg) y asegúrese de que esté disponible en su PATH.

5. Instalar la habilidad de Lean 4 (opcional pero recomendado)

Con cualquier plataforma de codificación agéntica como Claude Code o Codex, puede instalar la Habilidad de Codificación Agéntica: Demostración de Teoremas de Lean 4. Esta habilidad proporciona indicaciones y plantillas adicionales para interactuar con proyectos de Lean 4, incluida orientación sobre el uso de lean-lsp-mcp.

Herramientas MCP

Lista de herramientas disponibles

Consulte la Documentación de herramientas para obtener la lista completa de herramientas disponibles.

Deshabilitar herramientas

Muchos clientes permiten al usuario deshabilitar herramientas específicas manualmente (por ejemplo, lean_build).

VSCode: Haga clic en el ícono de Llave/Desarmador en el chat.

Cursor: En "Configuración de Cursor" > "MCP", haga clic en el nombre de una herramienta para deshabilitarla (tachada).

También puede deshabilitar herramientas al iniciar el servidor:

• LEAN_MCP_DISABLED_TOOLS: Nombres de herramientas separados por comas (por ejemplo, lean_run_code,lean_build).
• LEAN_MCP_INSTRUCTIONS: Cadena de instrucciones de servidor de reemplazo.
• LEAN_MCP_TOOL_DESCRIPTIONS: Objeto JSON para sobrescribir descripciones de herramientas.

Ejemplo:

export LEAN_MCP_DISABLED_TOOLS="lean_run_code,lean_build"
export LEAN_MCP_INSTRUCTIONS="Prefer lean_local_search before remote search tools."
export LEAN_MCP_TOOL_DESCRIPTIONS='{"lean_goal":"Primary proof-state inspection tool."}'

Configuración de MCP

Este servidor MCP funciona de inmediato sin ninguna configuración. Sin embargo, hay algunas configuraciones opcionales disponibles.

Variables de entorno

• LEAN_LOG_LEVEL: Nivel de registro para el servidor. Las opciones son "INFO", "WARNING", "ERROR", "NONE". El valor predeterminado es "INFO".
• LEAN_LOG_FILE_CONFIG: Ruta del archivo de configuración para el registro, con prioridad sobre LEAN_LOG_LEVEL. Si no se establece, los registros se imprimen en stdout.
• LEAN_PROJECT_PATH: Ruta a la raíz de su proyecto Lean. Una raíz de proyecto Lean válida debe contener lean-toolchain y ya sea lakefile.lean o lakefile.toml. Los argumentos relativos de file_path se resuelven contra esta raíz. Esta variable es necesaria para streamable-http y sse.
• LEAN_MCP_DISABLED_TOOLS: Lista separada por comas de nombres de herramientas para eliminar del listado de herramientas MCP.
• LEAN_MCP_INSTRUCTIONS: Cadena de instrucciones de servidor de reemplazo.
• LEAN_MCP_TOOL_DESCRIPTIONS: Objeto JSON que asigna nombres de herramientas a descripciones de reemplazo.
• LEAN_MCP_SCRATCH_SLOTS: Número de documentos de borrador paralelos utilizados para pruebas de fragmentos. El valor predeterminado es 1; auméntelo solo cuando los intentos paralelos valgan la memoria adicional del proceso de Lean.
• LEAN_MCP_MAX_OUTPUT_CHARS: Presupuesto de caracteres por campo para estados de objetivos y mensajes de diagnóstico. El valor predeterminado es 6000; el texto demasiado grande se elide del medio para que tanto el contexto local como el objetivo sobrevivan. Establezca en 0 para devolver todo sin truncar.
• LEAN_REPL: Establezca en true, 1 o yes para habilitar lean_run_code rápido basado en REPL y lean_multi_attempt basado en líneas (consulte Configuración de REPL).
• LEAN_REPL_PATH: Ruta al binario de repl. Se detecta automáticamente desde .lake/packages/repl/ o .lake/packages/REPL/ si no se establece.
• LEAN_REPL_TIMEOUT: Tiempo de espera por comando en segundos (predeterminado: 60).
• LEAN_REPL_MEM_MB: Memoria máxima por REPL en MB (predeterminado: 16384). Solo se aplica en Linux/macOS.
• LEAN_LSP_MCP_TOKEN: Token secreto para autenticación de portador cuando se usa transporte streamable-http o sse. Si se establece, se requiere autenticación de portador para cada solicitud.
• LEAN_BUILD_CONCURRENCY: Modo de concurrencia de compilación para lean_build. Opciones: allow (predeterminado), cancel, share.
• LEAN_HAMMER_URL: URL para una instancia autohospedada de Búsqueda de Premisas de Lean Hammer. Los límites de velocidad se omiten cuando se establece un backend personalizado.
• LEAN_LOOGLE_LOCAL: Establezca en true, 1 o yes para habilitar loogle local (consulte la sección Loogle Local).
• LEAN_LOOGLE_CACHE_DIR: Sobrescriba el directorio de caché para loogle local (predeterminado: ~/.cache/lean-lsp-mcp/loogle).
• LOOGLE_URL: URL para una instancia de Loogle autohospedada (predeterminado: https://loogle.lean-lang.org). Los límites de velocidad se omiten cuando se establece un backend personalizado.
• LOOGLE_HEADERS: Objeto JSON de encabezados HTTP adicionales para solicitudes de Loogle (por ejemplo, '{"X-API-Key": "..."}').

También puede establecer estas variables de entorno en la configuración de su cliente MCP:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ],
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/your/lean/project",
                "LEAN_LOG_LEVEL": "NONE"
            }
        }
    }
}

Métodos de transporte

El servidor MCP de Lean LSP admite los siguientes métodos de transporte:

• stdio: Entrada/salida estándar (predeterminado)
• streamable-http: Transmisión HTTP
• sse: Eventos enviados por el servidor (MCP heredado, use streamable-http si es posible)

stdio admite la inferencia y el cambio de proyecto a medida que se mueve entre proyectos Lean. streamable-http y sse son implementaciones de un solo proyecto: requieren LEAN_PROJECT_PATH al inicio y rechazan el cambio de proyecto impulsado por herramientas.

Puede especificar el método de transporte usando el argumento --transport al ejecutar el servidor. Para sse y streamable-http, también puede especificar opcionalmente el host y el puerto:

uvx lean-lsp-mcp --transport stdio # Default transport
uvx lean-lsp-mcp --transport streamable-http # Available at http://127.0.0.1:8000/mcp
uvx lean-lsp-mcp --transport sse --host localhost --port 12345 # Available at http://localhost:12345/sse
uvx lean-lsp-mcp --version # Print the installed version

Túnel MCP Seguro de OpenAI

Para ChatGPT, Codex, API de Respuestas u otras superficies de OpenAI, use Túnel MCP Seguro de OpenAI en lugar de exponer lean-lsp-mcp a Internet público. Cree un túnel en Configuración de túneles de la plataforma, luego ejecute tunnel-client en un host que pueda alcanzar su proyecto Lean:

export CONTROL_PLANE_API_KEY="sk-..."

tunnel-client init \
  --sample sample_mcp_stdio_local \
  --profile lean-lsp-local \
  --tunnel-id tunnel_0123456789abcdef0123456789abcdef \
  --mcp-command "uvx lean-lsp-mcp --transport stdio --lean-project-path /path/to/lean/project"

tunnel-client doctor --profile lean-lsp-local --explain
tunnel-client run --profile lean-lsp-local

Use --lean-project-path para que los argumentos relativos de file_path se resuelvan dentro del proyecto Lean previsto. Para HTTP, enlace lean-lsp-mcp a loopback y use --mcp-server-url http://127.0.0.1:8000/mcp en el perfil del túnel:

export LEAN_PROJECT_PATH="/path/to/lean/project"
uvx lean-lsp-mcp --transport streamable-http --host 127.0.0.1 --port 8000

Mantenga tunnel-client run saludable mientras prueba el descubrimiento de conectores o las llamadas a herramientas. En la configuración del conector de ChatGPT, elija Túnel como tipo de conexión.

Autenticación de token de portador

El transporte a través de streamable-http y sse admite autenticación de token de portador. Para acceso privado de OpenAI, prefiera el Túnel MCP Seguro de OpenAI; la autenticación de portador sigue disponible para implementaciones HTTP/SSE a las que los clientes acceden directamente.

Establezca la variable de entorno LEAN_LSP_MCP_TOKEN (o consulte la sección 3 para establecer variables de entorno en la configuración de MCP) a un token secreto antes de iniciar el servidor. Si esta variable está establecida, las solicitudes sin un encabezado Authorization: Bearer ... coincidente se rechazan antes del despacho de herramientas.

Ejemplo de configuración en Linux/MacOS:

export LEAN_LSP_MCP_TOKEN="your_secret_token"
uvx lean-lsp-mcp --transport streamable-http

Los clientes deben incluir el token en el encabezado Authorization.

Configuración de REPL

Habilite lean_run_code rápido basado en REPL y lean_multi_attempt basado en líneas. Usa el modo de táctica de leanprover-community/repl. Los intentos exactos basados en column aún usan la ruta LSP.

1. Agregue REPL al lakefile.toml de su proyecto Lean:

[[require]]
name = "repl"
git = "https://github.com/leanprover-community/repl"
rev = "v4.34.0"  # Use a REPL tag compatible with your Lean toolchain

2. Compílelo:

lake build repl

3. Habilítelo mediante CLI o variable de entorno:

uvx lean-lsp-mcp --repl

# Or via environment variable
export LEAN_REPL=true

El binario de REPL se detecta automáticamente desde .lake/packages/repl/ o .lake/packages/REPL/. Si no se encuentra, se usa LSP como respaldo.

Política de rutas

Las herramientas basadas en archivos solo operan en archivos dentro del proyecto Lean activo, dependencias resueltas de .lake/packages/* y el árbol de código fuente de la biblioteca estándar de Lean. Las rutas de archivo devueltas se sanean para evitar filtrar rutas absolutas del host:

• Los archivos del proyecto se devuelven relativos a la raíz del proyecto, por ejemplo, src/MyFile.lean.
• Los archivos de dependencia se devuelven bajo .lake/packages/<package>/....
• Los archivos de la biblioteca estándar se devuelven bajo .lean-stdlib/....

Se rechazan los escapes de enlaces simbólicos fuera de esas raíces.

Loogle Local

Ejecute Loogle localmente para evitar el límite de velocidad de la API remota (3 solicitudes/30 s). El binario se compila una vez para el toolchain de Lean del proyecto. El primer índice de Mathlib tarda unos minutos; los inicios posteriores lo cargan en segundos.

# Enable via CLI
uvx lean-lsp-mcp --loogle-local

# Or via environment variable
export LEAN_LOOGLE_LOCAL=true

Requisitos: git, lake (elan), un proyecto Mathlib compilado y memoria sustancial para la indexación. En mediciones con Mathlib actual, el índice inicial usó ~13 GiB de RSS máximo y una carga en caliente usó ~7 GiB. Nota: Loogle local actualmente solo es compatible con sistemas Unix (Linux/macOS). Los usuarios de Windows deben usar WSL o la API remota.

Mathlib proviene de tu proyecto: --lean-project-path debe apuntar a un proyecto compilado que dependa de Mathlib. El binario local está compilado para la cadena de herramientas Lean de ese proyecto y se ejecuta a través de lake env, por lo que Lake proporciona el entorno de dependencias propio del proyecto. El hash de dependencias nativo de Loogle detecta cambios en los archivos .olean y reconstruye automáticamente un índice desactualizado.

Si loogle local falla, se recurre a la API remota.

Notas sobre la seguridad de MCP

¡Existen muchas preocupaciones de seguridad válidas con el Protocolo de Contexto de Modelos (MCP) en general!

Este servidor MCP está pensado como una herramienta de investigación y actualmente se encuentra en beta. Aunque no maneja datos sensibles como contraseñas o claves API, aún incluye varios riesgos de seguridad:

• Acceso a tu sistema de archivos local.
• Potentes capacidades locales de compilación y análisis.
• Acceso a redes externas para herramientas de búsqueda remota, a menos que el operador lo desactive.

Ten en cuenta estos riesgos. ¡Siéntete libre de auditar el código e informar problemas de seguridad!

Configuración con contenedores (recomendada para un aislamiento más estricto)

Construir la imagen:

docker build -t lean-lsp-mcp:containerized .

Ejecutar con una raíz de proyecto montada (fuente de solo lectura + caché de Lake escribible):

docker run --rm -i \
  -v "$PWD":/workspace:ro \
  -v lean-lsp-mcp-lake-cache:/workspace/.lake \
  lean-lsp-mcp:containerized

La imagen Docker incluida tiene por defecto:

• LEAN_PROJECT_PATH=/workspace
• LEAN_MCP_DISABLED_TOOLS=lean_run_code

Notas:

• LEAN_MCP_DISABLED_TOOLS es un valor predeterminado de inicio y puede sobrescribirse con docker run -e.
• Usar --network none puede romper herramientas que requieren acceso a la red (leansearch, loogle, leanfinder, hammer_premise) y descargas de dependencias.
• El punto de entrada se cierra inmediatamente si LEAN_PROJECT_PATH no existe.

Para más información, puedes usar Awesome MCP Security como punto de partida.

Desarrollo

Consulta Adding a new tool para una guía paso a paso sobre cómo implementar una nueva herramienta MCP (modelos de retorno, módulos auxiliares, registro, pruebas y documentación).

Inspector MCP

npx @modelcontextprotocol/inspector uvx --with-editable path/to/lean-lsp-mcp python -m lean_lsp_mcp.server

Ejecutar pruebas

uv sync --all-extras
uv run pytest tests

Publicaciones y proyectos de formalización que usan lean-lsp-mcp

• Ax-Prover: Un marco agéntico de razonamiento profundo para la demostración de teoremas en matemáticas y física cuántica arxiv
• Numina-Lean-Agent: Un sistema de razonamiento agéntico abierto y general para matemáticas formales arxiv github
• MerLean: Un marco agéntico para la autoformalización en computación cuántica arxiv
• M2F: Formalización automatizada de literatura matemática a escala arxiv
• Un enfoque teórico de grupos para la capacidad de Shannon de grafos y un teorema de límite a partir de empaquetamientos reticulares github

Charlas

lean-lsp-mcp: Herramientas para la interacción agéntica con Lean (Lean Together 2026) youtube

Proyectos relacionados

• LeanTool
• LeanExplore MCP

Licencia y citación

Con licencia MIT. Consulta LICENSE para más información.

Se agradece enormemente citar este repositorio, aunque la licencia no lo exige.

@software{lean-lsp-mcp,
  author = {Oliver Dressler},
  title = {{Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover}},
  url = {https://github.com/oOo0oOo/lean-lsp-mcp},
  month = {3},
  year = {2025}
}