Odel
gonzalgo

gonzalgo

Local
@zengineco2PythonApache-2.0Updated 3w ago

Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.

Runs locally over stdio

This server isn't hosted — your MCP client launches it from a package registry. Use one of the commands below, or drop the config into your client (e.g. Claude Desktop).

PyPIgonzalgov0.5.2

Run

uvx gonzalgo

MCP client config

{
  "mcpServers": {
    "gonzalgo": {
      "command": "uvx",
      "args": [
        "gonzalgo"
      ]
    }
  }
}