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

Tool: lean_proof_structure

The most compact representation of a full Lean proof. Only shows the diffs, uses nesting to denote scope.

Returns { theorem_name, proof_tree, used_theorems }. The proof_tree:

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

Returns before&after goal state per tactic, like Lean's infoview.

Returns { theorem_name, proof_tree, used_theorems }. The proof_tree:

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

With include_theorems: true (on either tool), used_theorems is a list of 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)"
]