MCPLow riskUnclaimed

leanforge-mcp

MCP server for AI-driven formal proof search in Lean 4

sandraschisandraschi/leanforge-mcp★ 1Updated Aug 28, 2026

server.json

{
  "$schema": "https://static.modelcontextprotocol.io/schemas/2025-12-11/server.schema.json",
  "name": "io.github.sandraschi/leanforge-mcp",
  "description": "MCP server for AI-driven formal proof search in Lean 4",
  "repository": {
    "url": "https://github.com/sandraschi/leanforge-mcp",
    "source": "github"
  },
  "version": "0.1.0",
  "packages": [
    {
      "registryType": "mcpb",
      "identifier": "https://github.com/sandraschi/leanforge-mcp/releases/download/v0.1.0/leanforge-mcp-v0.1.0.mcpb",
      "fileSha256": "267c7214023a51328495d0dbd0354364dab7d91abb7b50595d0fb889ac78f00f",
      "transport": {
        "type": "stdio"
      }
    }
  ]
}

Permissions

DeclaredDetected
Runs code—bundle
Installs—mcpb:https://github.com/sandraschi/leanforge-mcp/releases/download/v0.1.0/leanforge-mcp-v0.1.0.mcpb
Runs install scripts—None
NetworkNoneNone
Needs credentialsNoneNone
Outside the workspace—None
Agent tools—None

Checks

Low risk · Nothing worth a warning was found.

Not reviewed by a person · Checked by rules; the model review is not switched on yet.

Versions

  1. #10.1.0latestOct 7, 2026