OpenProver

What it does

OpenProver is an automated theorem prover that leverages large language models to discover and verify mathematical proofs. It employs a sophisticated planner-worker architecture where a central planner manages a whiteboard and repository of lemmas, delegating specific exploration tasks to parallel workers. This allows it to tackle complex mathematical statements by breaking them down into manageable pieces.

Tools

• lean_verify: Compiles Lean 4 code to verify correctness.
• lean_store: Persists verified mathematical snippets for reuse.
• lean_search: Searches Mathlib and Lean declarations for relevant theorems.
• literature_search: Performs web searches for existing mathematical papers and results.

Installation

To use OpenProver via Claude Desktop, add the following to your claude_desktop_config.json:

{
  "mcpServers": {
    "openprover": {
      "command": "openprover",
      "args": []
    }
  }
}

Note: Requires Python 3.10+ and pip install openprover.

Supported hosts

• Claude
• vLLM
• OpenRouter