LeanProbe

Lemmy00/LeanProbe

★ 0 stars Python 💻 Code/Dev Tools Updated 7d ago

Fast Lean 4 proof feedback for coding agents. CLI, Python library, and MCP server with warm LeanInteract sessions and cached env reuse.

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": {
    "leanprobe": {
      "command": "uvx",
      "args": [
        "leanprobe"
      ]
    }
  }
}

Or install with pip: pip install leanprobe

README Excerpt

LeanProbe is a standalone Python package, CLI, and MCP server for fast Lean 4 feedback when a tool repeatedly checks declarations in the same Lean project. It uses [LeanInteract](https://github.com/augustepoiroux/LeanInteract) as its execution backend, keeps a Lean REPL warm, reuses elaborated imports and prior

Tools (8)

cacheelapsed_serror_codefeedback_leanmessagessuccesstacticstimed_out

Topics

clicoding-agentsleanlean-proverlean4leaninteractmathlibmcpmcp-servermodel-context-protocolproof-assistantpythontheorem-proving

LeanProbe

Quick Install

README Excerpt

Tools (8)

Topics

Related Code/Dev Tools Servers