Skip to content
mcp/harbor
Verified official

gonzalgo MCP

v0.5.6

io.github.vince-gonzalez/gonzalgo

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

transport:stdio runtime:pypi
View source Website

Target client

run in your project directory 

claude mcp add gonzalgo -- uvx gonzalgo

Adds it for this project only. Append --scope user to make it available everywhere. Claude Code docs

This listing does not declare its tools. Connect the server and your client will discover them on the handshake.