Metadata-Version: 2.4
Name: paperproof-mcp
Version: 0.2.1
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

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