Metadata-Version: 2.4
Name: paperproof-mcp
Version: 0.1.2
Summary: MCP server that exposes Lean proofs in the Paperproof boxes format, without installing Paperproof
Project-URL: Homepage, https://github.com/Paper-Proof/paperproof-mcp
Project-URL: Repository, https://github.com/Paper-Proof/paperproof-mcp
Project-URL: Issues, https://github.com/Paper-Proof/paperproof-mcp/issues
Author-email: Evgenia Karunus <lakesare@gmail.com>
License-Expression: MIT
License-File: LICENSE
Keywords: lean,lean4,mcp,paperproof,proof-visualization,theorem-proving
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries
Requires-Python: >=3.10
Requires-Dist: leanclient>=0.3.0
Requires-Dist: mcp[cli]>=1.0.0
Description-Content-Type: text/markdown

<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

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`).

```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`

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.

```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: `include_theorems`

With `include_theorems: true`, each tree also carries 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>
