/MCP [X 34.2, Y 40.8]

lean-mcp · same rules, prompt-menu injection.

A standalone MCP stdio server that serves the Lean ruleset for hosts whose only injection point is the prompt menu. Zero drift with the FastAPI adapters · both call get_lean_instructions().

[X 34.2, Y 40.8]

/M.01 Install

Two lines.

cd lean-mcp && pip install -e .
python server.py

/M.02 Client config

One JSON block.

{
  "mcpServers": {
    "lean": {
      "command": "python",
      "args": ["lean-mcp/server.py"]
    }
  }
}

/M.03 Surface

One prompt, one tool.

prompt

lean

Accepts mode (lite/full/ultra). Returns the persona for the requested intensity.

tool

lean_instructions

Callable from the model. Same mode parameter, same output.

← Lean layer Launch Studio