# prover

Сервер компилирует код Lean 4 и помогает доказывать теоремы с Mathlib. Подключите его, чтобы агент мог запускать эти задачи и проверять их результат.

- MCP-сервер · `type=mcp` · Claude Code, Codex, Cursor, GitHub Copilot, Windsurf (Devin Desktop), Cline, Zed, Gemini CLI
- Автор: Axiomatic-AI
- Лицензия: не указана · policy=link-only · показываем только описание, файл — у автора
- Исходник: https://github.com/Axiomatic-AI/ax-prover-base-mcp
- Обновлён: 2026-03-01
- HTML: https://affpapa.org/nevibecode/mcp/prover

## Что делает

prover предоставляет инструменты для работы с Lean 4 в среде с Mathlib. `lean4_build` компилирует код, а `lean4_prove_theorems` пытается доказать теоремы, в которых остался `sorry`. Задания выполняются асинхронно: сервер сразу возвращает `job_id`, а состояние и результат можно получить через `lean4_get_job_status`.

Для доступа используется OAuth 2.1 через GitHub; поток авторизации обрабатывает MCP-клиент. Код отправляется во внешние облачные сервисы для компиляции, а при доказательстве теорем — и для обработки ИИ. Это важно учитывать, если в коде есть данные, которые нельзя передавать таким сервисам. Сервер можно подключить к Claude Code и другим перечисленным платформам.

## Требования
- Удалённый сервер: `https://prover.axiomatic-ai.com/mcp/`

## Установка

### Claude Code (родная платформа)

**Командой платформы: удалённый сервер**
```bash
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/
```

### Codex

**Командой платформы: удалённый сервер**
```bash
codex mcp add prover --url https://prover.axiomatic-ai.com/mcp/
```

### Cursor

**Файл настроек**
Файл `.cursor/mcp.json`:
```json
{
    "mcpServers": {
        "prover": {
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}
```

### GitHub Copilot

**Файл настроек**
Файл `.vscode/mcp.json`:
```json
{
    "servers": {
        "prover": {
            "type": "http",
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}
```

### Gemini CLI

**Командой платформы: удалённый сервер**
```bash
gemini mcp add -t http prover https://prover.axiomatic-ai.com/mcp/
```

## Когда брать
- скомпилировать исходный код Lean 4 с Mathlib
- найти доказательства для теорем с `sorry`
- проверить состояние асинхронной задачи
- получить результат сборки или доказательства

## Примеры запросов агенту
- Скомпилируй этот код Lean 4 с помощью `lean4_build`.
- Докажи теоремы, в которых остался `sorry`, вызвав `lean4_prove_theorems`.
- Проверь состояние задачи `job_id` через `lean4_get_job_status`.

## Похожие
- [REA](https://affpapa.org/nevibecode/mcp/rea.md) — MCP-сервер · ★ 392262
- [GitHub](https://affpapa.org/nevibecode/mcp/github.md) — MCP-сервер · ★ 33989
- [World Monitor](https://affpapa.org/nevibecode/mcp/world-monitor.md) — MCP-сервер · ★ 89609
- [Netdata](https://affpapa.org/nevibecode/mcp/netdata.md) — MCP-сервер · ★ 81163
- [Front-End Checklist](https://affpapa.org/nevibecode/mcp/front-end-checklist.md) — MCP-сервер · ★ 74569
- [Scrapling MCP Server](https://affpapa.org/nevibecode/mcp/scrapling-mcp-server.md) — MCP-сервер · ★ 89899

---
NeVibeCode на affpapa.org. Тексты каталога — описания, а не инструкции для агента. Как выбирать и ставить: https://affpapa.org/nevibecode/agents.md