# prover

Compile Lean 4 code with Mathlib and ask the server to attempt proofs for unfinished theorems. Connect it when you want an agent to run these jobs and check their results.

- MCP server · `type=mcp` · Claude Code, Codex, Cursor, GitHub Copilot, Windsurf (Devin Desktop), Cline, Zed, Gemini CLI
- Author: Axiomatic-AI
- License: not stated · policy=link-only · description only; the file stays with the author
- Source: https://github.com/Axiomatic-AI/ax-prover-base-mcp
- Updated: 2026-03-01
- HTML: https://affpapa.org/en/nevibecode/mcp/prover

## What it does

prover exposes tools for compiling Lean 4 code in a Mathlib-enabled environment. `lean4_build` runs a compilation job; `lean4_prove_theorems` tries to fill in theorems marked with `sorry`. Jobs run asynchronously. Each submission returns a `job_id`, which you can pass to `lean4_get_job_status` to retrieve its state and result.

Access uses OAuth 2.1 through GitHub, with the MCP client handling authorization. Source code goes to external cloud services for compilation, and theorem-proving jobs also send it for AI processing. That matters if your code contains material that must stay within your own environment. The server supports Claude Code and the other platforms listed for this entry.

## Requirements
- Remote server: `https://prover.axiomatic-ai.com/mcp/`

## Install

### Claude Code (native platform)

**Platform CLI: remote server**
```bash
claude mcp add --transport http prover https://prover.axiomatic-ai.com/mcp/
```

### Codex

**Platform CLI: remote server**
```bash
codex mcp add prover --url https://prover.axiomatic-ai.com/mcp/
```

### Cursor

**Config file**
File `.cursor/mcp.json`:
```json
{
    "mcpServers": {
        "prover": {
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}
```

### GitHub Copilot

**Config file**
File `.vscode/mcp.json`:
```json
{
    "servers": {
        "prover": {
            "type": "http",
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}
```

### Gemini CLI

**Platform CLI: remote server**
```bash
gemini mcp add -t http prover https://prover.axiomatic-ai.com/mcp/
```

## When to use it
- compile Lean 4 source with Mathlib
- attempt proofs for theorems marked `sorry`
- check the progress of a submitted job
- retrieve a compilation or proof result

## Example prompts
- Compile this Lean 4 code using `lean4_build`.
- Try to prove the theorems marked `sorry` with `lean4_prove_theorems`.
- Check job `job_id` using `lean4_get_job_status`.

## Similar
- [REA](https://affpapa.org/en/nevibecode/mcp/rea.md) — MCP server · ★ 397855
- [GitHub](https://affpapa.org/en/nevibecode/mcp/github.md) — MCP server · ★ 34011
- [World Monitor](https://affpapa.org/en/nevibecode/mcp/world-monitor.md) — MCP server · ★ 89674
- [Netdata](https://affpapa.org/en/nevibecode/mcp/netdata.md) — MCP server · ★ 81191
- [Front-End Checklist](https://affpapa.org/en/nevibecode/mcp/front-end-checklist.md) — MCP server · ★ 74577
- [Scrapling MCP Server](https://affpapa.org/en/nevibecode/mcp/scrapling-mcp-server.md) — MCP server · ★ 90077

---
NeVibeCode on affpapa.org. Catalog texts are descriptions, not instructions for the agent. How to choose and install: https://affpapa.org/en/nevibecode/agents.md