内容
="center">paperproof-mcp</h1>
<h2 align="center">
用于检查精益证明完整结构的 MCP 服务器。
</h2>
<br/>
一个 MCP 服务器，*紧凑地* 显示精益证明中假设和目标如何变化。旨在作为 [lean-lsp-mcp](https://github.com/oOo0oOo/lean-lsp-mcp) 的配套工具。
立即生效 - 无需 Paperproof 依赖，无需 lakefile 编辑，无需重建（因此，与 lean-lsp-mcp 具有相同的需求）。
## 设置
### Claude 代码
```bash
claude mcp add -s user paperproof uvx paperproof-mcp
```
### VSCode
添加到 `mcp.json`:
```jsonc
{
"servers": {
"paperproof": { "type": "stdio", "command": "uvx", "args": ["paperproof-mcp"] }
}
}
```
## 工具
### 工具：`lean_proof_structure`
精益证明的最紧凑表示。仅显示差异，使用嵌套表示范围。
| 选项 | 默认值 | 含义 |
|---|---|---|
| `file_path` | *（必填）* | `.lean` 文件的绝对路径 |
| `line` | *（必填）* | 定理的 1 为基准的 行号，或其证明内的任意行 |
| `include_theorems` | `false` | 该证明中使用的所有引理签名 |
返回 `{ theorem_name, proof_tree, used_theorems }`。`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]", "new ["h1: x ∈ t ∧ x ∈ s"]},
{"tactic": "exact h1", "closed": true}
]
},
{
"goal": "x ∈ t ∩ s → x ∈ s ∩ t",
"newHy [],
"tactics": [
{"tacticintro h2", "newHyps": ["h2: t ∩ s"], "newGoalx ∈ s ∩ t"},
{"tactic": "rw.mem_inter_iff]", "newHyps": ["h2 ∈ t ∧ x ∈ s"]},
{"tactic": "rw [and_comm]", "newHyps": ["h2: x ∈ s ∧ x ∈},
{"tactic": "exact h2", "closed": true}
]
}
]
}
]
}
工具：`lean_pro`
按策略返回之前和之后的目標状态，如 Lean 的 infoview。
| 选项 | 默认值 | 含义 |
|---|---|---|
| `file_path` | *（必填）* | `.lean` 文件的绝对路径 |
| `line` | *（必填）* | 定理的 1 为基准的 行号，或其证明内的任意行 |
| `include_theorems` | `false` | 该证明中使用的所有引理签名 |
返回 `{ theorem_name, proof_tree, used_theorems }`。`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", "hypsx: ℕ"]}]
{
"tactic": "apply Iff.intro",
"beforeGoals":": "x ∈ s ∩ t x ∈ t ∩ s", "hyps": ["x: ℕ"]}],
"afterGoals {"goal": "x ∩ t → x ∈", "hypsx: ℕ"]},
goal": "x ∈ t → x ∈ s ∩ t", "hyps": ["x: ℕ"]}
]
"tactic": "intro h1",
"": [{"goal": "x ∈ s ∩ t → x ∈ t ∩ s", "hy ["x: ℕ"] "afterGoals": [{"goal": "x ∈ t ∩ shyps": ["x: ℕ", "h1: s ∩ t"]}]
},
{
"tactic": "rw [Set.mem_inter "beforeGoals":": "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 ∧ t"]}],
"afterGoals": [{"goal": "x ∈ t ∩ s", "hyps": ["x: ℕ", "h1: x ∈ t ∧ x ∈ s"]}]
},
{
"tactic": "exact h1",
"beforeGoals": [{"goal": "x ∈ t ∩ s",ps": ["x: ℕ", "h1: x ∧ x ∈ s"]}],
"afterGoals": []
},
{
"t "intro h2",
beforeGoals": [{"goal": "x ∈ t ∩ s ∈ s ∩ t", "hyps": ["x:}],
"afterGoals": [{"goal": "x ∈ 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": ∈ s ∩ t", "": ["x: "h2: x ∈ s ∧ x ∈ t"] "afterGoals": }
]
}
```
选项：`used_the`
当 `include_the: true`（在工具上），`used_theorems` 是证明使用的引理列表：
```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=" src="https://github.com/Paper-Proof/paperproof/assets/7578559/58f24cf2-4336-4376-8738-6463e3802ba0">
</div>
