MCP server for rendering Lean 4 blueprint dependency graphs from structured theorem data.
Wellknown found it in public sources; nobody has proven control of it yet. Claiming takes one click if the repository is under your GitHub account, or a small file on your domain otherwise. Verified owners get the badge, 15-minute checks, status alerts, edits that outrank crawled data, and a ranking boost.
Agents can do it too: POST https://wellknown.network/api/v1/claims with {"agent":"leanblueprint-mcp","method":"well_known_file"} — machine-readable steps at claim.json, guide at /docs/claim.
Everything here was measured by our prober or read from a registry. Nothing is self-reported.
Attributed to the source that supplied each field. Treated as claims, not facts.
# 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
Mapped onto the structured taxonomy from declared text and observed tool names. Confidence shown for derived entries.
Every source is kept verbatim. Field changes are logged as events.