MMCPMarkets
OL

ooo0ooo/lean-lsp-mcp

Developer tools

Эта страница переведена автоматически. Технические детали смотрите в оригинале. Открыть оригинал

542 stars 84 forks Качество 88 Тренд 42MIT
Repository Install

MCP для подтверждения бережливой теоремы

Обзор

MCP-сервер, который позволяет агентно взаимодействовать с Lean-теоремным доказателем через протокол Language Server Protocol с использованием leanclient. Этот сервер предоставляет ряд инструментов для LLM-агентов для понимания, анализа и взаимодействия с Lean-проектами. * : Доступ к диагностике, целевых состояниям, информации о терминах, документации курсора и многое другое. * : Используйте LeanSearch, Loogle, Lean Finder, Lean Hammer и Lean State Search для поиска релевантных теорем и определений. * : Простая конфигурация для различных клиентов, включая VSCode, Cursor и Claude Code. 1. Установите uv, менеджер пакетов на Python. 2. Убедитесь, что ваш Lean-проект быстро собирается, вручную запуская lake build. 3. Настройте IDE/Setup 4. (По желанию, настоятельно рекомендую) Установите ripgrep (rg) для локального поиска и сканирования исходных кодов (lean_verify предупреждения). Установите UV для своей системы. На Linux/MacOS: curl -LsSf https://astral.sh/uv/install.

Обзор (машинный перевод)

LEAN-LSP-MCP

MCP для подтверждения бережливой теоремы

MCP-сервер, который позволяет агентно взаимодействовать с Lean-теоремным доказателем через протокол Language Server Protocol с использованием leanclient. Этот сервер предоставляет ряд инструментов для LLM-агентов для понимания, анализа и взаимодействия с Lean-проектами.

Ключевые особенности

  • Rich Lean Interaction: Диагностика доступа, состояния целей, информация о терминах, документация по наведению и многое другое.
  • Внешние инструменты поиска: используйте LeanSearch, Loogle, Lean Finder и Lean Hammer для поиска релевантных теорем и определений.
  • Easy Setup: Простая настройка для различных клиентов, включая VSCode, Cursor и Claude Code.

Подготовка

Обзор

  1. Установите uv — менеджер пакетов на Python.
  2. Убедитесь, что ваш Lean-проект строится быстро, вручную запуская lake build.
  3. Настройте свой IDE/Настройку
  4. (По желанию, настоятельно рекомендую) Установите ripgrep (rg) для локального поиска и сканирования источников (предупреждения [lean_verify).

1. Установка UV

Установите UV для вашей системы. На Linux/MacOS: curl -LsSf https://astral.sh/uv/install.sh | sh

1b. Альтернатива: установка с помощью Nix

Если вы используете Nix, вы можете установить пакет напрямую с GitHub:

Эта страница переведена автоматически. Технические детали смотрите в оригинале.

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:

Открыть полный README на GitHub

Установка

uvx lean-lsp-mcp
Новичок в MCP? Начните с руководства на mcpskill.org →

Конфигурация

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