Search / io.github.vince-gonzalez/gonzalgo
gonzalgo
L0· runs locallyReports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
v0.5.6 · active · repository · website · descriptor JSON · versions
Search / io.github.vince-gonzalez/gonzalgo
L0· runs locallyReports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms.
v0.5.6 · active · repository · website · descriptor JSON · versions
{
"mcpServers": {
"gonzalgo": {
"command": "uvx",
"args": [
"--from",
"gonzalgo[mcp]",
"gonzalgo==0.5.6",
"mcp"
]
}
}
}claude mcp add gonzalgo -- uvx --from gonzalgo[mcp] gonzalgo==0.5.6 mcp[mcp_servers.gonzalgo]
command = "uvx"
args = ["--from", "gonzalgo[mcp]", "gonzalgo==0.5.6", "mcp"]
{
"$schema": "https://opencode.ai/config.json",
"mcp": {
"gonzalgo": {
"type": "local",
"command": [
"uvx",
"--from",
"gonzalgo[mcp]",
"gonzalgo==0.5.6",
"mcp"
],
"enabled": true
}
}
}{
"mcpServers": {
"gonzalgo": {
"command": "uvx",
"args": [
"--from",
"gonzalgo[mcp]",
"gonzalgo==0.5.6",
"mcp"
]
}
},
"deeplink": "cursor://anysphere.cursor-deeplink/mcp/install?name=gonzalgo&config=eyJjb21tYW5kIjoidXZ4IiwiYXJncyI6WyItLWZyb20iLCJnb256YWxnb1ttY3BdIiwiZ29uemFsZ289PTAuNS42IiwibWNwIl19"
}{
"servers": {
"gonzalgo": {
"type": "stdio",
"command": "uvx",
"args": [
"--from",
"gonzalgo[mcp]",
"gonzalgo==0.5.6",
"mcp"
]
}
}
}{
"mcpServers": {
"gonzalgo": {
"command": "uvx",
"args": [
"--from",
"gonzalgo[mcp]",
"gonzalgo==0.5.6",
"mcp"
]
}
}
}extensions:
"gonzalgo":
enabled: true
name: "gonzalgo"
type: stdio
cmd: "uvx"
args:
- "--from"
- "gonzalgo[mcp]"
- "gonzalgo==0.5.6"
- "mcp"
timeout: 300
This is a local package: the command runs on your machine.
Not scored: fewer than three checks apply, usually because no remote answered a credential-free probe or the server is a local package.
protocol.modern, protocol.stateless, protocol.transport, protocol.list_ttlno remote answered a protocol handshake (not probed yet, unreachable, or local-only)auth.prm, auth.as_metadata, auth.cimdno remote uses OAuthauth.secret_in_urlno templated URLtools.descriptions, tools.description_length, tools.schemas, tools.annotations, tools.directory_hints, tools.token_cost, tools.api_dumptool list unknown (behind auth, not probed, or empty)stability.changes, stability.rug_pulltool list unknowndeps.known_vulnsno known advisory in 2 resolved packagesdeps.mcp_sdk_versionthe official MCP SDK is not in the dependency graphdeps.resolvable[email protected] resolved: 2 packagesNo tool definition changes recorded. A server's first observation is its baseline; later probes record what changes.
Checks run on what our credential-free, read-only probes observe; tools are never called and no code audit is performed. How it is computed.
+repository +namespace-matches-repo +website ~liveness-unmeasured ~updated-39d-ago
Derived from observable signals (official registry feed and our own credential-free probes); no code audit performed. How it is computed.
[email protected] PyPI1 dependencies, resolved · advisories checked 2026-10-19
No known advisory affects this dependency graph.
Dependency graphs from deps.dev; advisories from OSV.dev, including the GitHub Advisory Database and the PyPI Advisory Database; all CC BY 4.0. The graph is what a clean install of this version resolves today; nothing was installed or run. How it is checked.
| package | registry | version | runtime | secrets |
|---|---|---|---|---|
gonzalgo | pypi | 0.5.6 | uvx |
No tools observed. Local packages are never executed by the registry.
Schemas: list_tools.
{
"name": "io.github.vince-gonzalez/gonzalgo",
"title": "gonzalgo",
"$schema": "https://static.modelcontextprotocol.io/schemas/2025-12-11/server.schema.json",
"version": "0.5.6",
"packages": [
{
"version": "0.5.6",
"transport": {
"type": "stdio"
},
"identifier": "gonzalgo",
"runtimeHint": "uvx",
"registryType": "pypi",
"registryBaseUrl": "https://pypi.org",
"packageArguments": [
{
"type": "positional",
"value": "mcp",
"isRequired": true,
"description": "Starts the stdio server. Without it the binary runs the analysis CLI."
}
],
"runtimeArguments": [
{
"name": "--from",
"type": "named",
"value": "gonzalgo[mcp]",
"isRequired": true,
"description": "The MCP server lives behind an optional dependency so the analysis tools stay dependency-light for CLI-only users."
}
]
}
],
"repository": {
"url": "https://github.com/vince-gonzalez/gonzalgo",
"source": "github"
},
"websiteUrl": "https://f-keys.com/gonzalgo/",
"description": "Reports what a checked Lean 4 or Metamath proof rests on: inherited sorry, compiler trust, axioms."
}