gonzalgo for Claude Code
io.github.vince-gonzalez/gonzalgo
Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
client:Claude Code
transport:stdio
runtime:pypi
Install gonzalgo in Claude Code
run in your project directory
claude mcp add gonzalgo -- uvx gonzalgoAdds it for this project only. Append --scope user to make it available everywhere. Claude Code docs