MCPLow riskUnclaimed

gonzalgo

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

vince-gonzalezvince-gonzalez/gonzalgo★ 2Updated Sep 11, 2026

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—python
Installs—pypi:gonzalgo@0.5.6
Runs 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

  1. #10.5.6latestOct 7, 2026