proofpatch

arclabs561/proofpatch

★ 0 stars Rust 💻 Code/Dev Tools Updated today

CLI and MCP server for debuggable Lean 4 proof workflows

View on GitHub →

Quick Install

Copy the config for your editor. Some servers may need additional setup — check the README.

Add to claude_desktop_config.json:

{
  "mcpServers": {
    "proofpatch": {
      "command": "cargo",
      "args": [
        "run",
        "--",
        "proofpatch"
      ]
    }
  }
}

README Excerpt

`proofpatch` is a CLI + MCP server for **debuggable Lean 4 workflows**: verify, locate `sorry`s, extract bounded context packs, and (optionally) call an OpenAI-compatible LLM. - **Target-agnostic**: point at a Lean repo with `--repo`, then target a file/decl/region inside it. - **Evidence-first**: commands return structured JSON and can emit on-disk artifacts under `.generated/`.

Topics

formal-verificationlean4mcpproof-assistant

proofpatch

Quick Install

README Excerpt

Topics

Related Code/Dev Tools Servers