prover — MCP-сервер для Claude Code: доказательства Lean 4
Сервер компилирует код Lean 4 и помогает доказывать теоремы с Mathlib. Подключите его, чтобы агент мог запускать эти задачи и проверять их результат.
claude mcp add --transport http prover https://prover.axiomatic-ai.com/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 и другим перечисленным платформам.
Какие задачи решает
- скомпилировать исходный код Lean 4 с Mathlib
- найти доказательства для теорем с
sorry - проверить состояние асинхронной задачи
- получить результат сборки или доказательства
Примеры запросов агенту
- Скомпилируй этот код Lean 4 с помощью
lean4_build. - Докажи теоремы, в которых остался
sorry, вызвавlean4_prove_theorems. - Проверь состояние задачи
job_idчерезlean4_get_job_status.
Как установить prover
Командой платформы: удалённый сервер
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/Командой платформы: удалённый сервер
codex mcp add prover --url https://prover.axiomatic-ai.com/mcp/Файл настроек
{
"mcpServers": {
"prover": {
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}Файл настроек
{
"servers": {
"prover": {
"type": "http",
"url": "https://prover.axiomatic-ai.com/mcp/"
}
}
}Командой платформы: удалённый сервер
gemini mcp add -t http prover https://prover.axiomatic-ai.com/mcp/По шагам, с командами для каждой платформы: Как подключить MCP-сервер: Claude Code, Codex, Cursor, VS Code, Gemini CLI и другие
Вопросы о prover
Как установить prover в Claude Code?
Выполните claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/. При подключении авторизация проходит через OAuth 2.1 с GitHub.
Что делает prover?
Он компилирует код Lean 4 с Mathlib и пытается автоматически доказать теоремы, помеченные sorry. Задания выполняются асинхронно, а результат возвращает lean4_get_job_status.
Куда отправляется код при работе с prover?
Код передаётся внешним облачным сервисам для компиляции, а при доказательстве теорем — также для обработки ИИ.
