Content
<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": [
{"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.
| 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
{
"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:
```json
"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)"
]
```
<div align="center">
<img width="60px" src="https://github.com/Paper-Proof/paperproof/assets/7578559/58f24cf2-4336-4376-8738-6463e3802ba0">
</div>
