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).
Run
uvx gonzalgo
MCP client config
{
"mcpServers": {
"gonzalgo": {
"command": "uvx",
"args": [
"gonzalgo"
]
}
}
}