paperproof-mcp 0.1.0

MCP server that exposes Lean proofs in the Paperproof boxes format, without installing Paperproof

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
• A Lean project that builds (lake build)

Claude Code - add once, works in every project

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

{
  "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
• 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 a NaturalProofTree.

used_theorems

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

"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:

{
  "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 imports 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). This package bundles Paperproof's Lean parser, which is MIT licensed, Copyright (c) 2023 Anton Kovsharov.