LeanBack

Lean back and let the AI agent write the proof.

Lightweight MCP server for Lean 4 theorem proving. Exposes six tools — project_info, check, prove, goals, eval, search — via the Model Context Protocol, enabling AI assistants to verify proofs, inspect goal states, evaluate expressions, and search Mathlib.

Prerequisites

• Lean 4 with elan (the Lean version manager)
• At least one Lean project (see Project Setup)

Installation

Claude Code

Simply run:

claude mcp add leanback -- uvx leanback

No installation required — uvx automatically downloads and runs LeanBack in an isolated environment.

Other MCP Clients

Any MCP-compatible client can connect. Run uvx leanback as a stdio MCP server, or use --transport sse --port 3000 for HTTP.

Manual Install (optional)

If you prefer a permanent installation:

uv tool install leanback

Project Setup

LeanBack works with any Lean project on disk — just pass its absolute path. To create a new project with Mathlib:

cd /path/to/parent/directory
lake +leanprover-community/mathlib4:lean-toolchain new myproject math
cd myproject
lake exe cache get

This takes a few minutes (downloading precompiled Mathlib). Once done, the project is ready to use.

You can also call project_info(project="/path/to/myproject") to check if a project is properly set up, or to get the exact shell commands to create one.

Tools

All tools require project as an absolute path (e.g., "/home/user/lean/myproject").

project_info

Check project status and get setup instructions. Call this first.

project_info(project="/home/user/lean/myproject")
→ { "valid": true, "lean_version": "...", "has_mathlib": true, "built": true }

If the path doesn't exist, returns setup commands to create the project.

check

Verify Lean code correctness — entire projects, specific files, or expressions.

check(project="/home/user/lean/myproject")
check(project="/home/user/lean/myproject", file="MyProof.lean")
check(project="/home/user/lean/myproject", expr="#check Nat.add", imports=["Mathlib.Tactic"])

Repeated check(file=...) calls on the same file reuse a warm Lean server: the first check pays the import cost, subsequent checks after edits take seconds (as long as the file's import lines are unchanged). Idle servers shut down automatically after 10 minutes; set LEANBACK_NO_WARM=1 to disable warm sessions entirely.

prove

Verify theorem proofs with tactics, or check proof files.

prove(project="/home/user/lean/myproject", theorem="2 + 2 = 4", tactics=["rfl"])
prove(project="/home/user/lean/myproject", theorem="∀ n : Nat, n + 0 = n", tactics=["intro n", "rfl"])
prove(project="/home/user/lean/myproject", theorem="∃ x : Nat, x > 0", tactics=["use 1", "simp"], mathlib=True)
prove(project="/home/user/lean/myproject", file="MyTheorems.lean")

goals

Inspect the proof state during proof construction. See what goals remain after applying tactics.

goals(project="/home/user/lean/myproject", theorem="∀ n : Nat, n + 0 = n")
goals(project="/home/user/lean/myproject", theorem="∀ n : Nat, n + 0 = n", tactics=["intro n"])
goals(project="/home/user/lean/myproject", theorem="True ∧ True", tactics=["constructor"])

eval

Execute Lean expressions and see results.

eval(project="/home/user/lean/myproject", code="#eval 2 + 2")
eval(project="/home/user/lean/myproject", code="#check List.map")
eval(project="/home/user/lean/myproject", code="#eval Nat.gcd 12 18", mathlib=True)
eval(project="/home/user/lean/myproject", code="#eval myFunc 3", imports=["MyProject.Definitions"], build=True)

With build=True, imported modules of the project itself are compiled first (lake build), so they don't need to be built manually before use.

search

Find declarations in Mathlib by pattern.

search(project="/home/user/lean/myproject", pattern="add_comm")
search(project="/home/user/lean/myproject", pattern="reverse", filter_namespace="List")
search(project="/home/user/lean/myproject", batch="add_assoc,mul_assoc,add_comm")

All Tools Are Read-Only

LeanBack never modifies your source files. It only reads project structure and runs Lean to check/evaluate code. File creation and editing is left to your agent's own tools. The one exception: eval with build=True runs lake build, which writes build artifacts to the project's .lake directory.

Response Format

All tools return JSON with a success (or valid) boolean. On failure, an error_code and message explain what went wrong. Detailed response schemas are documented in each tool's description (visible to your AI assistant via MCP).

Testing

leanback-test --tool-descriptions
leanback-test --project /path/to/myproject
leanback-test --project /path/to/myproject --tool check

License

Apache 2.0 — see LICENSE.