Metadata-Version: 2.4
Name: leanblueprint-mcp
Version: 0.1.2
Summary: MCP server for rendering Lean 4 blueprint dependency graphs from structured theorem data.
Author: Shuze Chen
License: MIT
Project-URL: Homepage, https://github.com/shuzechen/lean-blueprint-for-agent
Project-URL: Repository, https://github.com/shuzechen/lean-blueprint-for-agent
Keywords: lean4,blueprint,mcp,theorem,dependency-graph,formalization
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries :: Python Modules
Requires-Python: >=3.10
Description-Content-Type: text/markdown
Requires-Dist: mcp>=1.0.0
Requires-Dist: pydantic>=2.0
Requires-Dist: plastex>=3.1
Requires-Dist: plastexdepgraph>=0.0.4
Requires-Dist: leanblueprint>=0.0.20

# leanblueprint-mcp

MCP server for rendering Lean 4 blueprint dependency graphs from structured theorem data.

Works with any MCP-compatible client (Claude Desktop, Cursor, VS Code, Continue, etc.).

## Install

```bash
pip install leanblueprint-mcp
```

Or from source:

```bash
pip install -e .
```

## Prerequisites

```bash
pip install plastex plastexdepgraph leanblueprint
```

| Package | Purpose |
|---------|---------|
| Python 3.10+ | Runtime |
| `plastex` | LaTeX → HTML compiler |
| `plastexdepgraph` | Dependency graph generation (DOT → d3-graphviz) |
| `leanblueprint` | Blueprint LaTeX macros, CSS, Lean declaration tracking |

Optional:

| Dependency | Purpose | Install |
|-----------|---------|---------|
| Lean 4 (`elan`) | `.lean` code generation + `lake build` | https://lean-lang.org/lean4/doc/setup.html |

## MCP Client Configuration

### Claude Desktop

```json
{
  "mcpServers": {
    "leanblueprint": {
      "command": "python",
      "args": ["-m", "leanblueprint_mcp.server"]
    }
  }
}
```

### Codex / Cursor / Continue

```json
{
  "mcpServers": {
    "leanblueprint": {
      "command": "leanblueprint-mcp"
    }
  }
}
```

## Tools

### `leanblueprint_render`

Takes a JSON description of mathematical theorems, their proofs, and interdependencies, and compiles them into a color-coded interactive HTML dependency graph.

See `AGENTS.md` for the full input schema and usage examples for LLM agents.

## License

MIT
