Lean LSP

lean-lsp-mcp

Lean Theorem Prover MCP

Servidor MCP que permite interação agêntica com o Lean theorem prover via Language Server Protocol usando leanclient. Este servidor fornece uma variedade de ferramentas para agentes de LLM entenderem, analisarem e interagirem com projetos Lean.

Principais Recursos

• Interação Rica com Lean: Acesse diagnósticos, estados de objetivos, informações de termos, documentação de hover e muito mais.
• Ferramentas de Busca Externa: Use LeanSearch, Loogle, Lean Finder e Lean Hammer para encontrar teoremas e definições relevantes.
• Configuração Fácil: Configuração simples para vários clientes, incluindo VSCode, Cursor e Claude Code.

Configuração

Visão Geral

1. Instale uv, um gerenciador de pacotes Python.
2. Certifique-se de que seu projeto Lean compila rapidamente executando lake build manualmente.
3. Configure seu IDE/Setup
4. (Opcional, altamente recomendado) Instale ripgrep (rg) para busca local e varredura de código-fonte (avisos de lean_verify).

1. Instale uv

Instale uv para o seu sistema. No Linux/MacOS: curl -LsSf https://astral.sh/uv/install.sh | sh

1b. Alternativa: Instale com Nix

Se você usa Nix, pode instalar o pacote diretamente do GitHub:

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

Ou execute sem instalar: nix run github:oOo0oOo/lean-lsp-mcp.

Isso fornece apenas o servidor MCP. Você ainda precisa de uma toolchain Lean (elan/lake) para o seu projeto, igual à configuração uv abaixo.

2. Execute lake build

lean-lsp-mcp executará lake serve na raiz do projeto para usar o servidor de linguagem (para a maioria das ferramentas). Alguns clientes (ex.: Cursor) podem expirar durante esse processo. Portanto, é recomendado executar lake build manualmente antes de iniciar o MCP. Isso garante um tempo de compilação mais rápido e evita timeouts.

3. Configure seu IDE/Setup

{
    "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. Instale ripgrep (opcional, mas recomendado)

Para a ferramenta de busca local lean_local_search, instale ripgrep (rg) e certifique-se de que esteja disponível no seu PATH.

5. Instale a habilidade Lean 4 (opcional, mas recomendado)

Com qualquer plataforma de codificação agêntica, como Claude Code ou Codex, você pode instalar a Agentic Coding Skill: Lean 4 Theorem Proving. Essa habilidade fornece prompts e modelos adicionais para interagir com projetos Lean 4, incluindo orientação sobre o uso de lean-lsp-mcp.

Ferramentas MCP

Lista de ferramentas disponíveis

Consulte a Documentação de Ferramentas para a lista completa de ferramentas disponíveis.

Desabilitando Ferramentas

Muitos clientes permitem que o usuário desabilite ferramentas específicas manualmente (ex.: lean_build).

VSCode: Clique no ícone de Chave Inglesa/Chave de Fenda no chat.

Cursor: Em "Cursor Settings" > "MCP", clique no nome de uma ferramenta para desabilitá-la (riscado).

Você também pode desabilitar ferramentas na inicialização do servidor:

• LEAN_MCP_DISABLED_TOOLS: Nomes de ferramentas separados por vírgula (por exemplo, lean_run_code,lean_build).
• LEAN_MCP_INSTRUCTIONS: String de instruções do servidor de substituição.
• LEAN_MCP_TOOL_DESCRIPTIONS: Objeto JSON para substituir descrições de ferramentas.

Exemplo:

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."}'

Configuração MCP

Este servidor MCP funciona pronto para uso sem qualquer configuração. No entanto, algumas configurações opcionais estão disponíveis.

Variáveis de Ambiente

• LEAN_LOG_LEVEL: Nível de log do servidor. Opções: "INFO", "WARNING", "ERROR", "NONE". Padrão: "INFO".
• LEAN_LOG_FILE_CONFIG: Caminho do arquivo de configuração para logging, com prioridade sobre LEAN_LOG_LEVEL. Se não definido, os logs são impressos no stdout.
• LEAN_PROJECT_PATH: Caminho para a raiz do seu projeto Lean. Uma raiz de projeto Lean válida deve conter lean-toolchain e lakefile.lean ou lakefile.toml. Argumentos file_path relativos são resolvidos em relação a esta raiz. Esta variável é necessária para streamable-http e sse.
• LEAN_MCP_DISABLED_TOOLS: Lista separada por vírgulas de nomes de ferramentas a serem removidas da listagem de ferramentas MCP.
• LEAN_MCP_INSTRUCTIONS: String de instruções do servidor de substituição.
• LEAN_MCP_TOOL_DESCRIPTIONS: Objeto JSON mapeando nomes de ferramentas para descrições de substituição.
• LEAN_MCP_SCRATCH_SLOTS: Número de documentos de rascunho paralelos usados para tentativas de snippets. Padrão: 1; aumente apenas quando tentativas paralelas valerem a memória adicional do processo Lean.
• LEAN_MCP_MAX_OUTPUT_CHARS: Orçamento de caracteres por campo para estados de objetivos e mensagens de diagnóstico. Padrão: 6000; texto excessivo é elidido do meio para que tanto o contexto local quanto o alvo do objetivo sobrevivam. Defina como 0 para retornar tudo sem truncamento.
• LEAN_REPL: Defina como true, 1 ou yes para habilitar lean_run_code rápido baseado em REPL e lean_multi_attempt baseado em linha (veja Configuração REPL).
• LEAN_REPL_PATH: Caminho para o binário repl. Detectado automaticamente de .lake/packages/repl/ ou .lake/packages/REPL/ se não definido.
• LEAN_REPL_TIMEOUT: Timeout por comando em segundos (padrão: 60).
• LEAN_REPL_MEM_MB: Memória máxima por REPL em MB (padrão: 16384). Aplicado apenas no Linux/macOS.
• LEAN_LSP_MCP_TOKEN: Token secreto para autenticação bearer ao usar transporte streamable-http ou sse. Se definido, a autenticação bearer é necessária para cada requisição.
• LEAN_BUILD_CONCURRENCY: Modo de concorrência de build para lean_build. Opções: allow (padrão), cancel, share.
• LEAN_HAMMER_URL: URL para uma instância auto-hospedada de Lean Hammer Premise Search. Limites de taxa são ignorados quando definido para um backend personalizado.
• LEAN_LOOGLE_LOCAL: Defina como true, 1 ou yes para habilitar loogle local (veja a seção Loogle Local).
• LEAN_LOOGLE_CACHE_DIR: Substitua o diretório de cache para loogle local (padrão: ~/.cache/lean-lsp-mcp/loogle).
• LOOGLE_URL: URL para uma instância Loogle auto-hospedada (padrão: https://loogle.lean-lang.org). Limites de taxa são ignorados quando definido para um backend personalizado.
• LOOGLE_HEADERS: Objeto JSON de cabeçalhos HTTP extras para requisições Loogle (ex.: '{"X-API-Key": "..."}').

Você também pode frequentemente definir essas variáveis de ambiente na configuração do seu 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

O servidor MCP Lean LSP suporta os seguintes métodos de transporte:

• stdio: Entrada/saída padrão (padrão)
• streamable-http: Streaming HTTP
• sse: Eventos enviados pelo servidor (MCP legado, use streamable-http se possível)

stdio suporta inferência e troca de projeto conforme você se move entre projetos Lean. streamable-http e sse são implantações de projeto único: exigem LEAN_PROJECT_PATH na inicialização e rejeitam troca de projeto orientada por ferramentas.

Você pode especificar o método de transporte usando o argumento --transport ao executar o servidor. Para sse e streamable-http, você também pode opcionalmente especificar o host e a porta:

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 OpenAI

Para ChatGPT, Codex, Responses API ou outras superfícies OpenAI, use OpenAI Secure MCP Tunnel em vez de expor lean-lsp-mcp à internet pública. Crie um túnel em Platform tunnel settings e então execute tunnel-client em um host que possa alcançar seu projeto 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 argumentos file_path relativos sejam resolvidos dentro do projeto Lean pretendido. Para HTTP, vincule lean-lsp-mcp ao loopback e use --mcp-server-url http://127.0.0.1:8000/mcp no perfil do túnel:

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

Mantenha tunnel-client run saudável ao testar descoberta de conectores ou chamadas de ferramentas. Nas configurações do conector ChatGPT, escolha Tunnel como o tipo de conexão.

Autenticação com Token Bearer

O transporte via streamable-http e sse suporta autenticação com token bearer. Para acesso privado OpenAI, prefira OpenAI Secure MCP Tunnel; a autenticação bearer permanece disponível para implantações HTTP/SSE que os clientes alcançam diretamente.

Defina a variável de ambiente LEAN_LSP_MCP_TOKEN (ou veja a seção 3 para definir variáveis de ambiente na configuração MCP) para um token secreto antes de iniciar o servidor. Se esta variável estiver definida, requisições sem um cabeçalho Authorization: Bearer ... correspondente são rejeitadas antes do despacho de ferramentas.

Exemplo de configuração Linux/MacOS:

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

Os clientes devem então incluir o token no cabeçalho Authorization.

Configuração REPL

Habilite lean_run_code rápido baseado em REPL e lean_multi_attempt baseado em linha. Usa o modo de táticas leanprover-community/repl. Tentativas exatas baseadas em column ainda usam o caminho LSP.

1. Adicione REPL ao lakefile.toml do seu projeto 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. Compile-o:

lake build repl

3. Habilite via CLI ou variável de ambiente:

uvx lean-lsp-mcp --repl

# Or via environment variable
export LEAN_REPL=true

O binário REPL é detectado automaticamente de .lake/packages/repl/ ou .lake/packages/REPL/. Retorna ao LSP se não for encontrado.

Política de Caminhos

Ferramentas baseadas em arquivos operam apenas em arquivos dentro do projeto Lean ativo, dependências .lake/packages/* resolvidas e a árvore de código-fonte stdlib Lean. Os caminhos de arquivo retornados são sanitizados para evitar vazamento de caminhos absolutos do host:

• Arquivos do projeto são retornados relativos à raiz do projeto, por exemplo, src/MyFile.lean.
• Arquivos de dependência são retornados sob .lake/packages/<package>/....
• Arquivos stdlib são retornados sob .lean-stdlib/....

Escapamentos de symlink fora dessas raízes são rejeitados.

Loogle Local

Execute Loogle localmente para evitar o limite de taxa da API remota (3 req/30s). O binário é compilado uma vez para a toolchain Lean do projeto. O primeiro índice Mathlib leva alguns minutos; inicializações subsequentes o carregam em segundos.

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

# Or via environment variable
export LEAN_LOOGLE_LOCAL=true

Requisitos: git, lake (elan), um projeto Mathlib compilado e memória substancial para indexação. Em medições no Mathlib atual, o índice inicial usou ~13 GiB de RSS de pico e um carregamento quente usou ~7 GiB. Nota: O loogle local atualmente é suportado apenas em sistemas Unix (Linux/macOS). Usuários de Windows devem usar WSL ou a API remota.

Mathlib vem do seu projeto: --lean-project-path deve apontar para um projeto compilado que depende de Mathlib. O binário local é compilado para a toolchain Lean desse projeto e é executado através de lake env, então o Lake fornece o ambiente de dependências do próprio projeto. O hash de dependências nativo do Loogle detecta arquivos .olean alterados e reconstrói um índice desatualizado automaticamente.

Faz fallback para a API remota se o loogle local falhar.

Notas sobre Segurança do MCP

Existem muitas preocupações de segurança válidas com o Model Context Protocol (MCP) em geral!

Este servidor MCP é destinado como uma ferramenta de pesquisa e está atualmente em beta. Embora não lide com dados sensíveis, como senhas ou chaves de API, ele ainda inclui vários riscos de segurança:

• Acesso ao seu sistema de arquivos local.
• Capacidades poderosas de compilação e análise local.
• Acesso à rede externa para ferramentas de busca remota, a menos que seja desabilitado pelo operador.

Esteja ciente desses riscos. Sinta-se à vontade para auditar o código e relatar problemas de segurança!

Configuração em contêiner (recomendada para isolamento mais rigoroso)

Construir imagem:

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

Executar com uma raiz de projeto montada (fonte somente leitura + cache Lake gravável):

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

A imagem Docker incluída tem como padrão:

• LEAN_PROJECT_PATH=/workspace
• LEAN_MCP_DISABLED_TOOLS=lean_run_code

Notas:

• LEAN_MCP_DISABLED_TOOLS é um padrão de inicialização e pode ser substituído por docker run -e.
• Usar --network none pode quebrar ferramentas que exigem acesso à rede (leansearch, loogle, leanfinder, hammer_premise) e downloads de dependências.
• O entrypoint sai imediatamente se LEAN_PROJECT_PATH não existir.

Para mais informações, você pode usar Awesome MCP Security como ponto de partida.

Desenvolvimento

Consulte Adding a new tool para um guia passo a passo sobre como implementar uma nova ferramenta MCP (modelos de retorno, módulos auxiliares, registro, testes e documentação).

MCP Inspector

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

Executar Testes

uv sync --all-extras
uv run pytest tests

Publicações e Projetos de Formalização usando lean-lsp-mcp

• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics arxiv
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics arxiv github
• MerLean: An Agentic Framework for Autoformalization in Quantum Computation arxiv
• M2F: Automated Formalization of Mathematical Literature at Scale arxiv
• A Group-Theoretic Approach to Shannon Capacity of Graphs and a Limit Theorem from Lattice Packings github

Palestras

lean-lsp-mcp: Tools for agentic interaction with Lean (Lean Together 2026) youtube

Projetos Relacionados

• LeanTool
• LeanExplore MCP

Licença e Citação

MIT licenciado. Consulte LICENSE para mais informações.

Citar este repositório é altamente apreciado, mas não é exigido pela licença.

@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}
}