A lightweight MCP (Model Context Protocol) server that proxies between AI agents and the Lean 4 language server.
Quick Install
Copy the config for your editor. Some servers may need additional setup — check the README.
Add to claude_desktop_config.json:
{
"mcpServers": {
"lean4-mcp": {
"command": "cargo",
"args": [
"run",
"--",
"lean4-mcp"
]
}
}
}
Run in terminal:
claude mcp add lean4-mcp cargo run -- lean4-mcp
Add to .cursor/mcp.json:
{
"mcpServers": {
"lean4-mcp": {
"command": "cargo",
"args": [
"run",
"--",
"lean4-mcp"
]
}
}
}