Leanforge MCP server

leanforge-mcp

MCP server for AI-driven formal proof search in Lean 4. Submit a theorem with sorry; get back a machine-verified proof. Implements Agent A from AlphaProof Nexus (DeepMind, May 2026).

Stack: Python 3.12+ . FastMCP 3.4+ . FastAPI . React/Vite . Tailwind . Lean 4 / Mathlib

Table of Contents

• What it does
• Quick Install
• What You Can Do
• Tools
• Requirements
• Documentation
• Status
• License

What it does

Feed it a Lean 4 theorem with a sorry placeholder. It runs N parallel agents in a loop: the LLM proposes a proof edit, the Lean compiler judges it, errors feed back to the LLM. First agent to produce a sorry-free compile wins.

-- Input
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  sorry

-- Output (machine-verified)
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih => rw [Finset.sum_range_succ]; ring_nf; linarith

The compiler is the only oracle -- if it compiles without sorry, the proof is correct.

Quick Install

git clone https://github.com/sandraschi/leanforge-mcp
cd leanforge-mcp
uv sync
Copy-Item config.example.toml config.toml

Then add to claudedesktopconfig.json:

{
  "mcpServers": {
    "leanforge": {
      "command": "uv",
      "args": ["--directory", "C:\\path\\to\\leanforge-mcp", "run", "python", "-m", "leanforge_mcp"],
      "env": { "DEEPSEEK_API_KEY": "...", "ANTHROPIC_API_KEY": "..." }
    }
  }
}

See INSTALL.md for the Lean + Mathlib workspace setup (~4GB, one-time -- already provisioned and verified on Goliath as of 2026-07-09).

What You Can Do

"Prove that the sum of the first n natural numbers is n*(n+1)/2"

"Submit this MiniF2F problem and check back in 10 minutes"

"Show me all the proof attempts for job abc-123 -- why is it stuck?"

"Run validate_lean on this tactic proof to see if it compiles"

Tools

Requirements

• Python 3.11+
• Lean 4 via elan (winget install leanprover.elan)
• Mathlib workspace with cached oleans (~4GB, one-time setup -- see INSTALL.md)
• Ollama with deepseek-prover-v2:7b for tier-1 (local, free)
• DeepSeek or Anthropic API key for tier-2/3 (optional)

Documentation

Shortened. The full README is on GitHub.