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

# paperproof-mcp

MCP server that exposes Lean proofs in the **Paperproof "boxes" format** (`NaturalProofTree`) - **without requiring Paperproof to be installed** in the user's project.

Given a Lean file, the `paperproof_proof_tree` tool returns each theorem's proof as a hierarchical tree of **boxes**, where each box is one proof goal with the tactics that transform or close it - exactly the structure Paperproof draws.

## How it works

The server runs **Paperproof's real parser** inside your Lean project, without you installing anything:

1. It injects `import Lean` + Paperproof's bundled parser + a `#ppjson in` command into your file **in-memory** (via the LSP, same trick `#info_trees in` uses).
2. Runs the parser on the target theorem and reads the resulting JSON off the diagnostics.

The bundled parser depends only on core `Lean` (no Mathlib), so it elaborates in any project. Because it's Paperproof's actual `BetterParser`, `have`/`calc`/case-splits are handled faithfully - including hypothesis-origin (`from`) links.

**No Paperproof dependency, no lakefile edit, no rebuild.** Only a working `lake serve` is needed (same requirement as `lean-lsp-mcp`).

## Setup

### Prerequisites

- [uv](https://docs.astral.sh/uv/getting-started/installation/)
- A Lean project that builds (`lake build`)

### Claude Code - add once, works in every project

```bash
claude mcp add -s user paperproof uvx paperproof-mcp
```

(`-s user` installs at user scope so you don't repeat it per-project; the server infers each project root from the file path you pass.)

### VS Code / Cursor - add to `mcp.json`

```jsonc
{
  "servers": {
    "paperproof": {
      "type": "stdio",
      "command": "uvx",
      "args": ["paperproof-mcp"]
    }
  }
}
```

## Tool

### `paperproof_proof_tree`

**Parameters:**
- `file_path` (required) - absolute path to a `.lean` file
- `theorem_name` (optional) - a specific theorem; omit to parse all theorems in the file
- `format` (optional, default `"paperproof"`) - `"paperproof"` returns the hierarchical box tree (`NaturalProofTree`); `"infoview"` returns a flat before/after list per tactic (see below)
- `include_theorems` (optional, default `false`) - also return the signatures of every theorem/def/axiom the proof references, in each tree's `used_theorems`

**Returns:** `{ lean_version, trees: [{ theorem_name, proof_tree, used_theorems }] }`, where each `proof_tree` is in the requested `format`.

### `format: "infoview"`

A flat, tactic-by-tactic before/after view, like Lean's infoview. Every goal shows its full hypothesis context (not a diff), and the theorem's initial hypotheses are listed once and never repeated:

```json
{
  "initialHypotheses": [{ "name": "a", "type": "Nat" }, { "name": "h", "type": "a = b" }],
  "tactics": [
    {
      "tactic": "cases n with",
      "beforeGoals": [{ "hypotheses": [], "goal": "n = n" }],
      "afterGoals": [
        { "hypotheses": [], "goal": "0 = 0" },
        { "hypotheses": [{ "name": "k", "type": "Nat" }], "goal": "k + 1 = k + 1" }
      ]
    }
  ]
}
```

A tactic that closes its goal has an empty `afterGoals`; a case split or `have` obligation produces multiple `afterGoals`.

### `used_theorems`

When `include_theorems=true`, each tree carries the lemmas it uses:

```json
"used_theorems": [
  { "kind": "def",     "name": "AddCircle.liftIco", "signature": "{𝕜 : Type u_1} → ..." },
  { "kind": "theorem", "name": "Function.comp_apply", "signature": "∀ {β δ α} {f : β → δ} {g : α → β} {x}, (f ∘ g) x = f (g x)" }
]
```

Referenced constants are collected by walking the proof's info tree and keeping every **identifier** the user wrote that resolves to a global constant - this targets exactly the lemmas named in the source and drops notation plumbing (`HAdd.hAdd`, `OfNat.ofNat`, ...) that `Expr.getUsedConstants` would include. `kind` is derived from the type (`Prop`-valued => `theorem`), so it stays correct even under Lean's module system where imported proofs are erased and constants otherwise appear as axioms.

Example for `have h2 : b = a := by rw [h]; exact h2`:

```json
{
  "tactic": "have h2 : b = a := by",
  "newHyps": [{ "name": "h2", "type": "b = a" }],
  "haveBoxes": [
    {
      "goal": "b = a",
      "newHyps": [],
      "tactics": [
        { "tactic": "rw [h]", "newGoal": "b = b" },
        { "tactic": "rw [rfl]", "closed": true }
      ]
    }
  ]
}
```

### NaturalProofTree shape

```
NaturalProofTree  (root box)
  goal      : string          - goal at the top of this box
  newHyps   : NaturalHyp[]    - hypotheses introduced on entry
  tactics   : NaturalStep[]   - proof steps
  format    : "unicode"

NaturalHyp
  name  : string
  type  : string
  from? : string              - name of the hyp this one derives from (drives the arrow)

NaturalStep
  tactic       : string
  dependsOn?   : string[]      - hyp names this step consumes
  newHyps?     : NaturalHyp[]  - hyps this step introduces
  newGoal?     : string        - new goal if the goal transformed
  closed?      : true          - this step closes the current goal
  newSubgoals? : NaturalBox[]  - sub-boxes, one per case after a split
  haveBoxes?   : NaturalBox[]  - sub-proof(s) of a `have`/anonymous `by`
```

## Lean version support

The parser must compile against your project's Lean version. Parsers are hand-maintained Lean files in `src/paperproof_mcp/lean_parsers/vX.Y.Z.lean`, each containing Paperproof's parser plus the `#ppjson` runner. The server picks the one matching your `lean-toolchain`; with no exact match it tries the nearest lower version, then the nearest higher.

To add a version, copy the closest existing parser to `vX.Y.Z.lean` and fix the Lean-API errors for that toolchain (they are usually small stdlib renames; e.g. for 4.25 vs 4.27: `Substring.Raw` -> `Substring`, `.trimAscii` -> `.trim`, `.dropEndWhile` -> `.dropRightWhile`).

Bundled versions: **v4.25.0**, **v4.27.0**. Module-system toolchains (Lean's `module` / `public import` / `public section`) are handled by the runner automatically: it marks the parser `meta` and `meta import`s the file's own imports.

## Development

```
src/paperproof_mcp/
  server.py        - MCP tool; orchestrates the pipeline
  lean_runner.py   - in-memory injection + revert, reads JSON off diagnostics
  converter.py     - port of Paperproof's converter.ts (LeanProofTree to ConvertedProofTree)
  natural.py       - port of copyAsNaturalProofTree.ts (ConvertedProofTree to NaturalProofTree)
  lean_parsers/    - hand-maintained Paperproof parser + runner, one per Lean version
```

## License

MIT (see [LICENSE](LICENSE)). This package bundles [Paperproof](https://github.com/Paper-Proof/paperproof)'s Lean parser, which is MIT licensed, Copyright (c) 2023 Anton Kovsharov.
