leanforge-mcp

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 . Zustand . Biome . 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 claude_desktop_config.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

Tool	Description
submit_theorem	Submit a theorem statement → job ID (async)
submit_lean_file	Submit a full .lean file with sorry placeholders
get_proof_status	Poll job status; returns proof when complete
list_attempts	Inspect the attempt trajectory per agent/turn
list_jobs	List all jobs with status summary
validate_lean	Raw Lean 4 compile -- no job tracking
verify_proof	Re-check a proven file with verified kernels (con-leche, con-ron) -- needs workspace on Lean >= 4.35.0, see docs/VERIFIED_KERNELS.md
cancel_job	Cancel a running job
leanforge_shutdown	Gracefully shut down the server (cancels live jobs, exits)
get_mathlib_search	Natural language search over Mathlib theorems

---

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)

---

Ports & configuration

Piece	Value
MCP server	stdio (uv run python -m leanforge_mcp)
Web backend (FastAPI)	http://127.0.0.1:10867
Web frontend (Vite)	http://127.0.0.1:10868
Config file	config.toml (copy from config.example.toml; gitignored)
Environment	DEEPSEEK_API_KEY (tier 2), ANTHROPIC_API_KEY (tier 3) — see .env.example; keys stay in server env, never in the browser

---

Documentation

Doc	Contents
INSTALL.md	Prerequisites, Lean workspace setup, Claude Desktop config
docs/ONBOARDING.md	First-timer setup: costs, pitfalls, sanity check
docs/CONFIGURATION.md	All config options and environment variables
docs/TOOLS.md	Full tool reference with parameters and examples
docs/ARCHITECTURE.md	Proof loop, tier escalation, job lifecycle, SQLite schema
docs/LEAN.md	Lean 4 language reference, tactic guide, bibliography, link collection
docs/VERIFIED_KERNELS.md	Why verify_proof exists, what con-leche/con-ron are, workspace upgrade path
docs/LEAN_PRIMER.md	Quick Lean 4 intro for engineers (short version)
docs/ALPHAPROOF_NEXUS.md	The technique: AlphaProof Nexus paper explained
docs/COVERAGE_GAP.md	Why DeepMind got MSM coverage and a startup wouldn't
docs/BENCHMARK_RESULTS.md	MiniF2F, PutnamBench, Erdős results
docs/DEVELOPMENT.md	Contributing, dev setup, test commands
docs/TROUBLESHOOTING.md	Common errors and fixes
llms-full.txt	Full LLM context: tools, endpoints, config, ports

---

Roadmap

Phase	What	Status
A	Core loop: LLM proposes, Lean judges, error feeds back	Done
B	Correctness hardening, edge case handling, timeout tuning	Done (2026-07-09) -- tamper guard closed against default-arg truncation and a decoy-duplicate attack, cross-process job ownership/cancellation fixed, stateless-prompting mitigations added. 56/56 tests passing on real hardware. See docs/ASSESSMENT_2026-06-24.md
C	Performance and safety: REPL worker pool (compile-time is the real bottleneck), LLM timeout/retry, token/cost accounting (hard gate before any batch run)	In progress -- see TODO.md
D	Multi-agent parallel scheduling (Agent B from paper) -- run N loops in parallel, first to finish wins	Planned
E	Self-critique step -- LLM reviews its own proof before compile, catches obvious errors early	Planned
F	Webapp proof explorer -- interactive tree view of attempted proof paths, live tactic streaming	Planned
G	Premise selection -- before generating tactics, search Mathlib for relevant lemmas	Planned
H	Cumulative context windowing -- smart summarization of long error chains instead of blind concatenation	Planned
I	Benchmark dashboard -- webapp page tracking MiniF2F, PutnamBench, Erdős results per model/config	Stretch
J	Human-in-the-loop -- when the agent is stuck, pause and surface the current state for a human hint	Stretch
K	Proof caching -- deduplicate sub-proofs so repeated lemmas compile instantly	Stretch

What each phase enables

A + B let you submit a theorem and get a proof back on the other end. It works, it's useful, but it's single-threaded, pays a full compile per turn, and has no spend controls -- Phase C closes those gaps.

D changes the game: N parallel agents means wall-clock time drops from "however long one LLM takes" to "however long the fastest of N LLMs takes." For hard theorems where the LLM wanders into dead ends, this is the difference between 5 minutes and 30 seconds.

E prevents the LLM from wasting compiles on obviously wrong tactics. Cheap to add (one extra LLM call per attempt) and the paper shows it improves solve rate by ~15 percentage points on Agent A alone.

F is the user-facing payoff: instead of staring at "status: running" and polling, you watch the LLM try tactics in real time, see which paths it abandoned, and understand why it eventually succeeded or failed.

G addresses the most common failure mode: the LLM writes a correct tactic for a lemma that doesn't exist in the current context. Premise selection (a small retrieval step before tactic generation) cuts this dramatically.

H is invisible but critical: as the LLM accumulates 10+ failed attempts, the error context grows past the model's window. Smart summarization keeps relevant signal without drowning the LLM in noise.

Full gap analysis: docs/ASSESSMENT_2026-06-24.md

---

License

MIT