MCP server that exposes Lean proofs in the Paperproof boxes format, without installing Paperproof
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":"paperproof-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.
<h1 align="center">paperproof-mcp</h1> <h2 align="center"> MCP server for inspecting the full structure of a Lean proof. </h2> <br/> MCP server that *compactly* shows how hypotheses and goals change throughout your Lean proof. Meant as a companion for [lean-lsp-mcp](https://github.com/oOo0oOo/lean-lsp-mcp). Works immediately - no Paperproof dependency, no lakefile edit, no rebuild (so, same requirements as lean-lsp-mcp). ## Setup ### Claude Code ```bash claude mcp add -s user paperproof uvx paperproof-mcp ``` ### VSCode Add to `mcp.json`: ```jsonc { "servers": { "paperproof": { "type": "stdio", "command": "uvx", "args": ["paperproof-mcp"] } } } ``` ## Tools ### Tool: `lean_proof_structure` The most compact representation of a full Lean proof. Only shows the diffs, uses nesting to denote scope. | option | default | meaning | |---|---|---| | `file_path` | *(required)* | absolute path to a `.lean` file | | `line` | *(required)* | 1-based line of the theorem, or any line inside its proof | | `include_theorems` | `false` | all lemma signatures for the lemmas used in this proof | Returns `{ theorem_name, proof_tree, used_theorems }`. The `proof_tree`: ```json { "goal": "s ∩ t = t ∩ s", "initialHyps": ["s: Set ℕ", "t: Set ℕ"], "tactics": [ { "tactic": "ext x", "newHyps": ["x: ℕ"], "newGoal": "x ∈ s ∩ t ↔ x ∈ t ∩ s" }, { "tactic": "apply Iff.intro", "newSubgoals": [ { "goal": "x ∈ s ∩ t → x ∈ t ∩ s", "newHyps": [], "tactics": [ {"tactic": "intro h1", "newHyps": ["h1: x ∈ s ∩ t"], "newGoal": "x ∈ t ∩ s"}, {"tactic": "rw [Set.mem_inter_iff]", "newHyps": ["h1: x ∈ s ∧ x ∈ t"]}, {"tactic": "rw [and_comm]", "newHyps": ["h1: x ∈ t ∧ x ∈ s"]}, {"tactic": "exact h1", "closed": true} ] }, { "goal": "x ∈ t ∩ s → x ∈ s ∩ t", "newHyps": [], "tactics": [ {"tacti…
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.