gonzalgo
Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
Install
PyPIstdio
uvx gonzalgo Client config (Claude Desktop, Cursor, Windsurf and most MCP clients)
{
"mcpServers": {
"io-github-vince-gonzalez-gonzalgo": {
"command": "uvx",
"args": [
"gonzalgo"
]
}
}
}Source: official MCP Registry record · registry name io.github.vince-gonzalez/gonzalgo · published 2026-09-11 · updated 2026-09-11. Not an endorsement; review the code before connecting it to anything sensitive.