MMCPMarkets
OL

ooo0ooo/lean-lsp-mcp

Developer tools

이 페이지는 AI로 자동 번역되었습니다. 기술적인 세부 사항은 원문을 확인하세요. 원문 보기

540 stars 84 forks 품질 88 트렌드 42MIT
Repository Install

린 정리 증명기 MCP

개요

Language Server 프로토콜을 통해 lean 정리 증명기와 Leanclient를 이용한 에이전트적 상호작용을 가능하게 하는 MCP 서버입니다. 이 서버는 LLM 에이전트가 Lean 프로젝트를 이해하고 분석하며 상호작용할 수 있는 다양한 도구를 제공합니다. * : 진단, 목표 상태, 용어 정보, 호버 문서 등 다양한 기능에 접근할 수 있습니다. * : LeanSearch, Loogle, Lean Finder, Lean Hammer, Lean State Search를 사용하여 관련 정리와 정의를 찾을 수 있습니다. * : VSCode, 커서, Claude 코드 등 다양한 클라이언트에 대한 간단한 구성. 1. 파이썬 패키지 매니저 uv 설치. 2. Lake 빌드를 수동으로 실행하여 Lean 프로젝트가 빠르게 빌드되도록 하세요. 3. IDE/설정 설정 4. (선택 사항이며 강력히 추천) 로컬 검색 및 소스 스캔을 위한 ripgrep(rg)을 설치하세요 (경고 lean_verify). 시스템에 UV를 설치하세요. Linux/MacOS에서: curl -lsSf https://astral.sh/uv/install.

개요(AI 번역)

lean-lsp-mcp

린 정리 증명기 MCP

Language Server 프로토콜을 통해 lean 정리 증명기와 Leanclient를 이용한 에이전트적 상호작용을 가능하게 하는 MCP 서버입니다. 이 서버는 LLM 에이전트가 Lean 프로젝트를 이해하고 분석하며 상호작용할 수 있는 다양한 도구를 제공합니다.

주요 특징

  • 풍부한 린 상호작용: 진단, 목표 상태, 용어 정보, 호버 문서 등 다양한 기능에 접근할 수 있습니다.
  • 외부 검색 도구: LeanSearch, Loogle, Lean Finder 및 Lean Hammer를 사용하여 관련 정리와 정의를 찾으세요.
  • 쉬운 설정: VSCode, 커서, Claude 코드 등 다양한 클라이언트에 대한 간단한 구성.

준비

개요

  1. uv, Python 패키지 관리자 설치.
  2. 린 프로젝트가 lake build를 수동으로 실행하여 빠르게 구축되도록 하세요.
  3. IDE/설정 설정
  4. (선택적이고 강력히 권장) 로컬 검색 및 소스 스캔(lean_verify 경고)을 위한 ripgrep (rg]) 설치.

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

  1. Install uv, a Python package manager.
  2. Make sure your Lean project builds quickly by running lake build manually.
  3. Configure your IDE/Setup
  4. (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
MCP 초보자라면? mcpskill.org 가이드부터 시작하세요 →

설정

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