Skip to main content

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

pip install leanblueprint-mcp

Or from source:

pip install -e .

Prerequisites

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

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

Codex / Cursor / Continue

{
  "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

Metadata

Release files for leanblueprint-mcp 0.1.3

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for leanblueprint-mcp 0.1.3
File Size Uploaded Provenance Actions
leanblueprint_mcp-0.1.3.tar.gz 14.5 kB Without provenance Details for leanblueprint_mcp-0.1.3.tar.gz

Built distribution (wheel)

Table of built distributions (wheels) for leanblueprint-mcp 0.1.3
File Interpreter ABI Platform Actions
leanblueprint_mcp-0.1.3-py3-none-any.whl Python 3 none any Details for leanblueprint_mcp-0.1.3-py3-none-any.whl

Total release size: 30.6 kB

Release files / leanblueprint_mcp-0.1.3.tar.gz

Download URL leanblueprint_mcp-0.1.3.tar.gz
Size 14.5 kB
Tags Source
SHA-256 checksum
How to use checksums
4335bc38bd95cb340743661d07532de8f21ac2bfbf1af1a34b3f3b7cf39613da
BLAKE2b-256 checksum
How to use checksums
be15f9fddee0a6a807a815a621c83b549758cefd3dfe64c1d1996e3ea080362e
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/6.2.0 CPython/3.12.9

Release files / leanblueprint_mcp-0.1.3-py3-none-any.whl

Download URL leanblueprint_mcp-0.1.3-py3-none-any.whl
Size 16.1 kB
Tags Python 3
SHA-256 checksum
How to use checksums
46987e5d11ebcee4558a2fcb58751dd88fd1b7b1c45c4aae432024ddfb84abdd
BLAKE2b-256 checksum
How to use checksums
1663fa257f048c16e59ff5601d6549656353870140c155092540104af27363ef
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/6.2.0 CPython/3.12.9

Security for leanblueprint-mcp 0.1.3

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.

To learn more about protecting yourself from malicious actors, visit our package security documentation.

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page