io.github.zengineco/gonzalgo
gonzalgo
Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
needs args probed 2026-10-15
MCP error -32000: Connection closed
usage: gonzalgo [-h]
{lean-files,check,amplify,eligible,why,index,mcp,trust,impact,audit,mm}
- Run it
- uvx gonzalgo==0.5.2 (stdio, probed in a container with the network off)
- Host
- pypi.org
- Repository
- https://github.com/zengineco/gonzalgo
- Website
- https://f-keys.com/gonzalgo/
- Registry
- deprecated, updated 2026-09-11 · registry entry
- Reachable
- 0 of the last 1 probe
Badge and feed
[](https://mcpcost.ulehla.dev/s/io.github.zengineco/gonzalgo)
An entry for every probe that changed the result, the tool count or the token cost: Atom feed. Add it to a feed reader or a Slack RSS app to hear when the server stops answering or its tool set grows.