lean-lsp-mcp
MCP-сервер к языковому серверу Lean 4: агент читает цели доказательства, ошибки и ищет теоремы прямо в проекте
- 550 ★ репозитория
- Последний коммит
- MIT
Расширенный доступ
Почему такой уровень
- Сервер запускает `lake serve` и компилирует код проекта на вашей машине.
- Запросы поиска теорем уходят во внешние сервисы LeanSearch, Loogle и Lean Finder.
Установка
- Работает в
В терминале, через SkillFoxx CLI
npx skillfoxx add mcp/lean-lsp-mcpОпределит агенты на машине, покажет уровень доступа и зафиксирует версию.
Другие способы установки
Доступ и проверки
Как мы проверяемРасширенный доступИнструмент запускает код или ходит в сеть, а внешние данные только читает.
- Сервер запускает `lake serve` и компилирует код проекта на вашей машине.
- Запросы поиска теорем уходят во внешние сервисы LeanSearch, Loogle и Lean Finder.
Это чужой код. Посмотрите файлы в репозитории перед установкой.
Что делает
lean-lsp-mcp соединяет агента с проектом на Lean 4 через языковой сервер `lake serve`. Агент запрашивает цель доказательства в нужной строке, диагностику файла, подсказки при наведении, места объявления и ссылки на символ, автодополнение и структуру файла с сигнатурами. Отдельные инструменты пробуют код: `lean_run_code` компилирует фрагмент, `lean_multi_attempt` проверяет несколько тактик в одной точке и возвращает цель и ошибки по каждой. Для поиска теорем сервер обращается к LeanSearch, Loogle, Lean Finder и Lean Hammer, есть и локальный поиск через `ripgrep`. Сервер работает по `stdio` и не требует настройки. Режим REPL включается переменной `LEAN_REPL=true` и ускоряет запуск кода и перебор тактик. Лишние инструменты отключает `LEAN_MCP_DISABLED_TOOLS`.
Для кого. Математикам и разработчикам, которые доказывают теоремы в Lean 4 с Claude Code, Cursor или Codex и хотят, чтобы агент видел состояние доказательства.
Подходит, если
- Доказательство застряло на строке, и агенту нужна цель с гипотезами в этой точке
- Файл не собирается, и надо быстро получить все ошибки и предупреждения с позициями
- Несколько вариантов тактики хочется проверить разом, не правя файл по одному
- Нужна подходящая лемма из Mathlib, а название неизвестно: поиск идет по смыслу через LeanSearch или Loogle
- Модуль большой, и перед правкой нужен обзор объявлений файла с типами
Не подходит, если
- Код написан на другом языке: сервер работает только с Lean
- На машине нет `lake` и тулчейна Lean, а ставить их нельзя
- Сборка идет долго, а клиент обрывает долгие запуски: сначала выполните `lake build` вручную
- Сетевые запросы к внешним поисковикам теорем недопустимы: их можно отключить, но тогда останется локальный поиск
Пример запроса к агенту
В файле Basic.lean доказательство теоремы застряло на строке 42. Покажи цель в этой точке и попробуй `simp`, `omega` и `linarith`.MCP
- Транспорт
- stdio, http, sse
- Авторизация
- не нужна
Переменные окружения
`LEAN_PROJECT_PATH`- Путь к корню проекта Lean. Обязателен для режимов `streamable-http` и `sse`.
`LEAN_REPL`- Значение `true` включает быстрый запуск кода и перебор тактик через REPL.
Ограничения
- Для запуска нужны `uv` и проект, который собирается командой `lake build`. Некоторые клиенты, например Cursor, обрывают запуск по таймауту, поэтому проект лучше собрать заранее.
- Поиск по LeanSearch, Loogle и Lean Finder идет во внешние сервисы, а не на вашей машине.
- `ripgrep` не обязателен, но без него не работает `lean_local_search` и предупреждения `lean_verify`.
- Для режимов `streamable-http` и `sse` обязательна переменная `LEAN_PROJECT_PATH` с путем к корню проекта.
Как отключить. Выполните `claude mcp remove lean-lsp` или удалите запись `lean-lsp` из `mcp.json` клиента. Отдельные инструменты отключает переменная `LEAN_MCP_DISABLED_TOOLS`.
Частые вопросы
Как подключить lean-lsp-mcp к Claude Code?
Выполните в корне проекта, где лежит `lakefile.toml`, команду `claude mcp add lean-lsp uvx lean-lsp-mcp`. Для общей конфигурации проекта добавьте ключ `-s project`: запись попадет в файл `.mcp.json`.
Зачем собирать проект до запуска сервера?
Сервер запускает `lake serve`, а первая сборка занимает много времени. Клиент может оборвать запуск по таймауту, поэтому проект собирают заранее командой `lake build`.
Что дает режим REPL?
При `LEAN_REPL=true` инструмент `lean_run_code` переиспользует кэш импортов, а `lean_multi_attempt` перебирает тактики по строке до пяти раз быстрее. Путь к бинарнику задает `LEAN_REPL_PATH`, иначе сервер ищет его в `.lake/packages/`.
Нужен ли `ripgrep`?
Нет, сервер стартует без него. Но `lean_local_search` и предупреждения `lean_verify` работают только при установленном `rg` в PATH.
Как убрать лишние инструменты?
Перечислите их в переменной `LEAN_MCP_DISABLED_TOOLS` через запятую, например `lean_run_code,lean_build`. В VS Code и Cursor инструмент можно отключить и в настройках клиента.
Обсуждение
Вопросов и отзывов пока нет.
Похожие
MCP-серверыМост между языковым сервером LSP и агентом: определения, ссылки, диагностика, подсказки и переименование символов
Мост MCP и LSP: агент получает типы, ссылки, диагностику и рефакторинг от языковых серверов, например Pyright.
Плагин для доказательства теорем в Lean 4: поиск по mathlib, циклы заполнения sorry, проверка аксиом и страховочные хуки
MCP-сервер agent-lsp собирает языковые серверы в связки для агента: вызовы, безопасная правка, переименование, диагностика.
Граф знаний по коду проекта для агента: вызывающие, зависимости и радиус правки через MCP вместо чтения файлов
cclsp подключает языковые серверы LSP к Claude Code через MCP: переход к определению, поиск ссылок, переименование символов и диагностика без редактора
Коротко о README
Установка идет через `uv` и `uvx`, конфигурации даны для VS Code, Cursor, Claude Code, Mistral Vibe и Codex. Дальше перечислены переменные окружения, режим REPL и ссылка на отдельный файл со списком инструментов.