Skip to content
Agentmart
Submit a tool

Leanforge MCP

Lean 4 theorem prover MCP: automated proof search, mathlib integration, job management

Connector by sandraschi · GitHub account verified by the MCP Registry

IndexedMITLocal (stdio)★ 3
Write a review

Install

Works with Claude Desktop. Read the repository before you give any tool access to your data.

Download the bundle

MCP bundle (.mcpb): open it with Claude Desktop.

Get the weekly diff

The weekly diff: one email a week with new agent tools, notable updates and grade changes, plus security alerts for tools you follow. Double opt-in, one-click unsubscribe.

We use your email only for this newsletter. Privacy

About

Lean 4 theorem prover MCP: automated proof search, mathlib integration, job management

Reviews

Write a review

No reviews yet. Installed it? Reviews come from verified installers only. How reviews work

Permissions

What this server can do and what it asks for, from its tool list, install config and code. Checked Oct 25, 2026.

Tools
6 read · 2 write · 2 delete
Secrets
None asked for
Install scripts
None found
Runs as
Downloaded binary

Tools by what they do 10

Read from the source code; the running server may list different tools.

Read 6 · Look things up without changing anything.

  • get_mathlib_search
  • get_proof_status
  • list_attempts
  • list_jobs
  • validate_lean
  • verify_proof

Write 2 · Create, change, send or run things.

  • submit_lean_file
  • submit_theorem

Delete 2 · Delete, drop, revoke or wipe things.

  • cancel_job
  • leanforge_shutdown

Network hosts it talks to 8

  • api.deepseek.com · found in code
  • arxiv.org · found in code
  • biomejs.dev · found in code
  • bun.sh · found in code
  • elan.lean-lang.org · found in code
  • github.com · found in install command, code
  • leansearch.net · found in code
  • schema.tauri.app · found in code

Files it touches

  • %APPDATA%\com.sandraschi.pywinauto-mcp\logs\backend-spawn.log
  • Your home directory (~)

Tools (10)

Read from the source code; the running server may differ. Descriptions are the server’s own words; hidden characters are shown as [U+…].

  • cancel_jobcan change or delete data

    Cancel a running proof search job.

  • get_mathlib_searchread-only

    Search Mathlib4 for theorems matching a natural language query. Returns theorem names and type signatures useful for building proofs. Use this when stuck -- find the right Mathlib lemma name and pass it as a hint to submit_theorem.

  • get_proof_statusread-only

    Get the status of a proof search job. If complete, returns the proven Lean 4 file. If running, returns turn count and latest attempt. Poll every 10-30s.

  • leanforge_shutdowncan change or delete data

    Shut down the leanforge-mcp server gracefully. Cancels live proof jobs, then exits the process. Use before upgrades or restarts.

  • list_attemptsread-only

    List proof attempts for a job, with Lean source and compiler feedback per turn. Useful for understanding why a search is stuck or inspecting the trajectory.

  • list_jobsread-only

    List all jobs with status and summary.

  • submit_lean_file

    Submit a complete Lean 4 file with sorry placeholders directly. Ideal for MiniF2F or AlphaProof Nexus problem stubs that are already formalized.

  • submit_theorem

    Submit a theorem for formal proof search. Returns a job_id immediately -- use get_proof_status to poll. The server runs parallel agents looping LLM-propose -> Lean-compile -> error-feedback until proven or budget exhausted.

  • validate_leanread-only

    Run the Lean 4 compiler on arbitrary source and return output. No job tracking, no LLM -- raw compile. Use to test a proof or debug Lean syntax before submitting.

  • verify_proofread-only

    Re-verify Lean 4 source with independent verified kernels (con-leche, con-ron). Compiles first: unproven input is rejected without touching the kernels. Proven input is exported via leanexport and replayed through each kernel; all must accept. Needs a workspace on Lean >= 4.35.0, otherwise returns supported=false with the upgrade path. Slow (minutes for Mathlib proofs) -- use for results that matter, not per-turn checking.

Signals

Stars
3
Forks
0
Open issues
0
Last commit
Oct 24, 2026 (5 days ago)
Last release
Oct 19, 2026 (10 days ago)

From GitHub (fetched Oct 24, 2026).

Details

Registry name
io.github.sandraschi/leanforge-mcp
Version
0.1.1
Auth
No auth
Packages
mcpb https://github.com/sandraschi/leanforge-mcp/releases/download/v0.1.1/leanforge-mcp-v0.1.1.mcpb
License
MIT
Repository
github.com/sandraschi/leanforge-mcp
First seen
Oct 24, 2026
Last checked
Oct 24, 2026
Source
Official MCP Registrygithub-graphql

More from sandraschi

Cite this page

Leanforge MCP. Agent Mart. https://agentmart.dev/connectors/sandraschi-leanforge-mcp (last updated 2026-10-24)