ooo0ooo/lean-lsp-mcp

开发工具

本页由 AI 翻译，技术细节请以原文为准。查看原文

542 stars 84 forks 质量 88 趋势 42MIT

Repository Install

精益定理证明器 MCP

概览

MCP服务器允许通过语言服务器协议使用leanclient与精益定理证明器进行代理交互。该服务器为LLM代理提供了多种工具，帮助他们理解、分析和交互精益项目。 * ：访问诊断、目标状态、术语信息、悬停文档等。* ：使用 LeanSearch、Loogle、Lean Finder、Lean Hammer 和 Lean State Search 查找相关定理和定义。* ：为多种客户端（包括 VSCode、光标和 Claude 代码）提供简单配置。 1. 安装 uv，一个 Python 包管理器。2. 通过手动运行 lake build 确保你的精益项目快速构建。3. 配置你的 IDE/设置 4.（可选，强烈推荐）安装 ripgrep（rg），用于本地搜索和源扫描（lean_verify警告）。为你的系统安装 UV。在 Linux/MacOS 上：curl -lsSf https://astral.sh/uv/install.

概述（AI 翻译）

精益-LSP-MCP

精益定理证明器 MCP

MCP服务器允许通过语言服务器协议使用leanclient与精益定理证明器进行代理交互。该服务器为LLM代理提供了多种工具，帮助他们理解、分析和交互精益项目。

主要特色

丰富的精益交互：访问诊断、目标状态、术语信息、悬停文档等。
外部搜索工具：使用LeanSearch、Loogle、Lean Finder和Lean Hammer]查找相关定理和定义。
简单设置：适用于多种客户端的简单配置，包括VSCode、光标和Claude代码。

布置

概述

安装 uv，一个 Python 包管理器。
通过手动运行lake build，确保你的精益项目快速构建。
配置你的IDE/设置
（可选，强烈推荐）安装ripgrep （rg）用于本地搜索和源扫描（lean_verify 警告）。

1.安装UV

为你的系统安装UV。在Linux/MacOS上：curl -LsSf https://astral.sh/uv/install.sh | sh

1b. 替代方案：用Nix安装

如果你用 Nix，可以直接从 GitHub 安装这个包：

本页由 AI 翻译，技术细节请以原文为准。

README

以下为原文 README 节选，完整内容请查看原文。

lean-lsp-mcp

Lean Theorem Prover MCP

MCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient. This server provides a range of tools for LLM agents to understand, analyze and interact with Lean projects.

Key Features

Rich Lean Interaction: Access diagnostics, goal states, term information, hover documentation and more.
External Search Tools: Use LeanSearch, Loogle, Lean Finder and Lean Hammer to find relevant theorems and definitions.
Easy Setup: Simple configuration for various clients, including VSCode, Cursor and Claude Code.

Setup

Overview

Install uv, a Python package manager.
Make sure your Lean project builds quickly by running lake build manually.
Configure your IDE/Setup
(Optional, highly recommended) Install ripgrep (rg) for local search and source scanning (lean_verify warnings).

1. Install uv

Install uv for your system. On Linux/MacOS: curl -LsSf https://astral.sh/uv/install.sh | sh

1b. Alternative: Install with Nix

If you use Nix, you can install the package directly from GitHub:

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

Or run it without installing: nix run github:oOo0oOo/lean-lsp-mcp.

This provides the MCP server only. You still need a Lean toolchain (elan/lake) for your project, same as the uv setup below.

2. Run `lake build`

lean-lsp-mcp will run lake serve in the project root to use the language server (for most tools). Some clients (e.g. Cursor) might timeout during this process. Therefore, it is recommended to run lake build manually before starting the MCP. This ensures a faster build time and avoids timeouts.

3. Configure your IDE/Setup

One-click config setup:

在 GitHub 查看完整 README

安装

uvx lean-lsp-mcp

新手？先看 mcpskill.org 教程 →

配置

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