The logical skeleton of a paper as a graph of statements — theorems,
propositions, lemmas and definitions — joined by dependency edges (an arrow
A → B means A is used in the proof of B). Layout is automatic: prerequisites
sink to the bottom, results rise to the top, and node size + border thickness track weight (1–5).
Click a statement to read it.
The diagrams in the pre-installed library are LLM-generated editorial readings of each paper: the statements shown, their weights, and even some dependencies are simplified and subjective. Treat them as a visual aid for orientation, not an authoritative account of the paper. (The app renders any diagram in this format — including carefully hand-built ones; the library just doesn't have any yet.)
Uncheck a kind above to hide those statements (their dependencies re-link transitively). The thickness of a statement's border indicates its weight (1–5).
paper-diagram JSON format (for authoring new diagrams)Each paper in the library is one JSON object in the paper-diagram format (schemaVersion: 1): a directed acyclic graph of a paper's statements. Node positions are not stored — the viewer lays the graph out automatically from the dependency edges and per-node weights. To add a paper, write one such object; the fastest way to get a valid template is to open the currently-loaded paper with the JSON export button and mirror its shape.
Top level
format: "paper-diagram", schemaVersion: 1.meta: { title, paper: { arxiv, authors: […], year, companion? }, note?, date? }.layout: { engine: "layered", direction: "up" | "down" } — "up" puts results at the top.nodes: […], edges: […].Node
id (required): stable, unique, human-readable — e.g. "thm:1.2", "lem:5.7". Edges reference these.kind: theorem | proposition | lemma | corollary | definition | remark — colours the border.label: short tag shown on the node ("Thm 1.2"); name: a concise human name.weight: 1–5 editorial importance → node size + border thickness (never position).color (optional): box background fill — a hex colour like "#e7edfb" (or a CSS colour name); defaults to white. Set it with the Background picker in the edit panel. Rendered in the viewer and in the SVG, TikZ, DOT and Mermaid exports (quiver has no boxes, so it carries labels only).statement: the LaTeX source of the statement — shown in the selection panel (unless plain is given) and carried as a per-node comment in the TikZ export.plain (optional): a plain-text paraphrase shown in the viewer panel instead of the raw LaTeX.section (optional): paper section, e.g. "5.2". external: true + ref: for cited results not proved in the paper.Edge
from, to (required, node ids): from is a prerequisite used in the proof of to — the arrow points prerequisite → result.type: "uses" (solid) or "generalizes" (dashed; from ⇢ to reads "to generalizes from").The graph must be acyclic (no dependency loop) and every edge must reference existing node ids — the viewer rejects a diagram otherwise. Weights are purely editorial: they change size and emphasis, never layout position, which is always derived from the dependencies.
The exports
Six targets. SVG is a standalone image of the current layout. TikZ is a compilable LaTeX figure. quiver is an import link for q.uiver.app. DOT (Graphviz) and Mermaid are portable text graphs that are re-laid-out by their own tools — Graphviz/Gephi/yEd for DOT, GitHub/wikis/mermaid.live for Mermaid — so they carry the dependency structure, colours and styles but not the on-screen positions. All are self-contained text you can download and edit.
Only the JSON export is lossless — the others each drop something. Positions: SVG reproduces the exact layout, TikZ rounds coordinates, quiver snaps them to an integer grid, and DOT/Mermaid discard them entirely (re-laid-out by their tools). Node colour is kept by SVG, TikZ, DOT and Mermaid but dropped by quiver (it has no boxes). And the prose fields — the full statement, the plain paraphrase, section/ref — are not carried into any of the figure formats. Export JSON (and re-import it) whenever you need a faithful round-trip.
Write label and name as ordinary text. For the two LaTeX-bound targets the exporter escapes LaTeX-special characters (_ ^ & % # ~) and maps the common math Unicode (Greek, sub/superscripts, arrows, ≅, ×, …) to LaTeX, so TikZ compiles as-is; wrap anything in $…$ to pass it through verbatim (e.g. for a real subscript). quiver renders labels with a limited LaTeX subset (KaTeX-like) and does not share this toolchain: plain text, basic $…$ math and the mapped symbols are fine, but avoid exotic macros in fields destined for quiver. DOT and Mermaid are not LaTeX — their labels are emitted as plain Unicode text (so $…$ is shown literally there, not typeset).
A Lean blueprint already is a dependency DAG of a formalization's theorems, lemmas and definitions, so it maps directly onto this format. A small converter script turns a blueprint's dependency graph into paper-diagram JSON deterministically (no LLM): kinds come from the def:/thm:/lem: label prefixes, edges from \uses, and each node's Lean formalization status is carried into the color field. (The “Sphere packing in dimension 8 — Lean formalization” entry in the dropdown was built this way.)
The script makes no network calls of its own — it reads a local file or stdin, so you fetch the graph with a tool you trust (here curl):
curl -sL https://<project>.github.io/<repo>/blueprint/dep_graph_document.html | python3 leanblueprint_to_paperdiagram.py --title "My paper" > diagram.json
Then paste diagram.json into the edit JSON box above and press load into viewer. (Or point the script at a local dep_graph_document.html / dep_graph.dot from a local blueprint build — no web at all.)
Notes
plasTeX will add statements and sections).