Metadata-Version: 2.4
Name: leanback
Version: 0.1.1
Summary: MCP server for Lean 4 theorem proving — check, prove, goals, eval, search
Author: Stefan Szeider
License: Apache-2.0
License-File: LICENSE
Classifier: Development Status :: 4 - Beta
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.11
Requires-Dist: mcp>=1.9.4
Requires-Dist: rich>=14.0.0
Description-Content-Type: text/markdown

# 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](https://modelcontextprotocol.io), enabling AI assistants to verify proofs, inspect goal states, evaluate expressions, and search Mathlib.

## Prerequisites

- **Lean 4** with [elan](https://github.com/leanprover/elan) (the Lean version manager)
- At least one Lean project (see [Project Setup](#project-setup))

## Installation

### Claude Code

Simply run:

```bash
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:

```bash
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:

```bash
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"])
```

### 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)
```

### 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 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.

## 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

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

## License

Apache 2.0 — see [LICENSE](LICENSE).
