MCPLow riskUnclaimed
gonzalgo
Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
vince-gonzalezvince-gonzalez/gonzalgo
server.json
{
"$schema": "https://static.modelcontextprotocol.io/schemas/2025-12-11/server.schema.json",
"name": "io.github.vince-gonzalez/gonzalgo",
"description": "Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.",
"title": "gonzalgo",
"repository": {
"url": "https://github.com/vince-gonzalez/gonzalgo",
"source": "github"
},
"version": "0.5.6",
"websiteUrl": "https://f-keys.com/gonzalgo/",
"packages": [
{
"registryType": "pypi",
"registryBaseUrl": "https://pypi.org",
"identifier": "gonzalgo",
"version": "0.5.6",
"runtimeHint": "uvx",
"transport": {
"type": "stdio"
},
"runtimeArguments": [
{
"description": "The MCP server lives behind an optional dependency so the analysis tools stay dependency-light for CLI-only users.",
"isRequired": true,
"value": "gonzalgo[mcp]",
"type": "named",
"name": "--from"
}
],
"packageArguments": [
{
"description": "Starts the stdio server. Without it the binary runs the analysis CLI.",
"isRequired": true,
"value": "mcp",
"type": "positional"
}
]
}
]
}Permissions
DeclaredDetected
Runs code—
pythonInstalls—
pypi:gonzalgo@0.5.6Runs install scripts—None
NetworkNoneNone
Needs credentialsNoneNone
Outside the workspace—None
Agent tools—None
Checks
Low risk · Nothing worth a warning was found.
Not reviewed by a person · Checked by rules; the model review is not switched on yet.
Versions
- #10.5.6latestOct 7, 2026
gonzalgoOpen in Codeg