paperproof-mcp 0.1.2

MCP server that exposes Lean proofs in the Paperproof boxes format, without installing Paperproof

paperproof-mcp

MCP server for inspecting the full structure of a Lean proof.

MCP server that compactly shows how hypotheses and goals change throughout your Lean proof. Meant as a companion for lean-lsp-mcp.

Works immediately - no Paperproof dependency, no lakefile edit, no rebuild (so, same requirements as lean-lsp-mcp).

Setup

Claude Code

claude mcp add -s user paperproof uvx paperproof-mcp

VSCode

Add to mcp.json:

{
  "servers": {
    "paperproof": {
      "type": "stdio",
      "command": "uvx",
      "args": ["paperproof-mcp"]
    }
  }
}

Tools

Both tools parse the proof the same way and differ only in the shape of the output. Each returns { lean_version, trees: [{ theorem_name, proof_tree, used_theorems }] }, and both take the same options:

option	default	meaning
file_path	(required)	absolute path to a .lean file
theorem_name	(required)	name of the theorem to parse
include_theorems	false	also return signatures of every theorem/def/axiom the proof references, in each tree's used_theorems

Tool: lean_proof_structure

The full nested structure as a tree of boxes. Each box is one goal with its tactics. The root box lists the theorem's initialHyps; nested boxes and tactics carry the newHyps they introduce. A tactic may close the goal (closed), transform it (newGoal), split it into branches (newSubgoals), or open a sub-proof (haveBoxes).

{
  "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": [
            {"tactic": "intro h2", "newHyps": ["h2: x ∈ t ∩ s"], "newGoal": "x ∈ s ∩ t"},
            {"tactic": "rw [Set.mem_inter_iff]", "newHyps": ["h2: x ∈ t ∧ x ∈ s"]},
            {"tactic": "rw [and_comm]", "newHyps": ["h2: x ∈ s ∧ x ∈ t"]},
            {"tactic": "exact h2", "closed": true}
          ]
        }
      ]
    }
  ]
}

Tool: lean_proof_steps

Before&after goal states per tactic, like Lean's infoview. Every goal shows its full hypothesis context (not a diff); the proof's initial hypotheses are listed once under initialHyps and never repeated. A tactic that closes its goal has an empty afterGoals; a case split or have obligation yields several.

{
  "initialHyps": ["s: Set ℕ", "t: Set ℕ"],
  "tactics": [
    {
      "tactic": "ext x",
      "beforeGoals": [{"goal": "s ∩ t = t ∩ s", "hyps": []}],
      "afterGoals": [{"goal": "x ∈ s ∩ t ↔ x ∈ t ∩ s", "hyps": ["x: ℕ"]}]
    },
    {
      "tactic": "apply Iff.intro",
      "beforeGoals": [{"goal": "x ∈ s ∩ t ↔ x ∈ t ∩ s", "hyps": ["x: ℕ"]}],
      "afterGoals": [
        {"goal": "x ∈ s ∩ t → x ∈ t ∩ s", "hyps": ["x: ℕ"]},
        {"goal": "x ∈ t ∩ s → x ∈ s ∩ t", "hyps": ["x: ℕ"]}
      ]
    },
    {
      "tactic": "intro h1",
      "beforeGoals": [{"goal": "x ∈ s ∩ t → x ∈ t ∩ s", "hyps": ["x: ℕ"]}],
      "afterGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ s ∩ t"]}]
    },
    {
      "tactic": "rw [Set.mem_inter_iff]",
      "beforeGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ s ∩ t"]}],
      "afterGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ s ∧ x ∈ t"]}]
    },
    {
      "tactic": "rw [and_comm]",
      "beforeGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ s ∧ x ∈ t"]}],
      "afterGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ t ∧ x ∈ s"]}]
    },
    {
      "tactic": "exact h1",
      "beforeGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ t ∧ x ∈ s"]}],
      "afterGoals": []
    },
    {
      "tactic": "intro h2",
      "beforeGoals": [{"goal": "x ∈ t ∩ s → x ∈ s ∩ t", "hyps": ["x: ℕ"]}],
      "afterGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ t ∩ s"]}]
    },
    {
      "tactic": "rw [Set.mem_inter_iff]",
      "beforeGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ t ∩ s"]}],
      "afterGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ t ∧ x ∈ s"]}]
    },
    {
      "tactic": "rw [and_comm]",
      "beforeGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ t ∧ x ∈ s"]}],
      "afterGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ s ∧ x ∈ t"]}]
    },
    {
      "tactic": "exact h2",
      "beforeGoals": [{"goal": "x ∈ s ∩ t", "hyps": ["x: ℕ", "h2: x ∈ s ∧ x ∈ t"]}],
      "afterGoals": []
    }
  ]
}

Option: include_theorems

With include_theorems: true, each tree also carries the lemmas the proof uses:

"used_theorems": [
  "theorem Set.mem_inter_iff: ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b",
  "theorem and_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ a",
  "theorem Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)"
]