gonzalgo MCP server

by vince-gonzalez·io.github.vince-gonzalez/gonzalgo·v0.5.6·2 stars

No reviews yet

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

A89/100grade A

Write a review Install

What users say

No reviews yet

Be the first

Safety scan

A89/100

full report

Adoption

Growing

2 stars130 downloads/wk

Reviews

Write one

Nobody has reviewed gonzalgo yet.

If you have run it, two minutes of your experience saves the next person an afternoon.

gonzalgo tools (10, 1 write)

write = sends, deletes, buys or posts

Read from the package source without running it. The installed server may list more.

audit_trust
axiom_reach
check_dump
how_to_extract
impact
kernel_index
metamath_audit
scope
why
write_lean_extractorswrite action

Public scan report

scanner v0.1.10 · 2026-10-14 · same rubric, same numbers if you re-run it

no findings

Code scan10 source files scanned25/25
–Live reliabilityno gateway calls yet and no remote to proben/a
–Tool poisoningtools not inspected (local package is not executed); not countedn/a
Auth qualitylocal package, no credentials required12/15
Maintenancelast push 11 days ago15/15
Maintainer identityregistry namespace matches repository owner6/10

Overall 89/100. Components that don't apply are left out of the denominator. Any critical finding is an F.Rubric Appeal a finding JSON

How gonzalgo compares

Against every graded MCP server, from our own scans and uptime checks. Updated after each scan run.

Safety score: 89/100; higher than 80% of 48,243 servers
Tools: 10; the typical server has 7
Tools that change things: 10%; typical: 0%. Fewer write tools means less an agent can break
GitHub stars: 2; more than 75% of 28,706 servers
Downloads a week: 130; more than 68% of 12,306 servers with a package

What its tools let an agent do: 9 read · 1 create

Install gonzalgo in Claude Code, Cursor or VS Code

claude mcp add gonzalgo -- uvx gonzalgo

Add to Cursor

What the publisher says

From the gonzalgo repository's README, as published. We do not edit it. Read it on GitHub

╔════════════════════════════════════════════════════════════════════════════════════════════╗
║                                                                                            ║
║            ██████╗  ██████╗ ███╗   ██╗███████╗ █████╗ ██╗      ██████╗  ██████╗            ║
║           ██╔════╝ ██╔═══██╗████╗  ██║╚══███╔╝██╔══██╗██║     ██╔════╝ ██╔═══██╗           ║
║           ██║  ███╗██║   ██║██╔██╗ ██║  ███╔╝ ███████║██║     ██║  ███╗██║   ██║           ║
║           ██║   ██║██║   ██║██║╚██╗██║ ███╔╝  ██╔══██║██║     ██║   ██║██║   ██║           ║
║           ╚██████╔╝╚██████╔╝██║ ╚████║███████╗██║  ██║███████╗╚██████╔╝╚██████╔╝           ║
║            ╚═════╝  ╚═════╝ ╚═╝  ╚═══╝╚══════╝╚═╝  ╚═╝╚══════╝ ╚═════╝  ╚═════╝            ║
║                                                                                            ║
║                       where does a formal library spend its axioms?                        ║
║                                                                                            ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝

#print axioms tells you whether one theorem depends on an axiom. It cannot tell you where an axiom is spent rather than inherited, how far that spending reaches, how much of it could be avoided, or — for a given theorem — which step introduced it. This does.

Works on Lean 4 / Mathlib and on Metamath databases (set.mm, iset.mm, nf.mm), by one program, so two foundations are compared under identical definitions rather than by analogy.

$ pip install gonzalgo
$ gonzalgo index

  THE KERNEL INDEX  (2026-08-05)   what formal libraries rest on
  library             system      theorems  unfinished  compiler   choice
  -----------------------------------------------------------------------
  Mathlib             Lean 4       437,429           0         0   66.62%
  Lean core (Init)    Lean 4        45,051           0         0   23.91%
  Std                 Lean 4        34,510           0         0   56.66%
  Batteries           Lean 4         5,249           0         0   32.63%
  set.mm              Metamath      47,621           0         -    1.22%
  ...
  14 libraries, 603,703 theorems, 0 resting on an unfinished proof.

That runs the moment it's installed — no Lean, no build, no files. Everything below needs a Lean project.

Pure Python. macOS, Windows, Linux. numpy is the only dependency.

Questions this answers

How do I know if my Lean proof depends on a sorry? Lean warns once, on the line you typed it. It does not warn you about the theorem three files later that uses that lemma and is therefore not proved either. Run gonzalgo trust and it reports every theorem that reaches a sorry anywhere upstream, however far.

How do I find a sorry I inherited from a dependency? Same command. The audit is over the whole environment, so a sorry in a library you import is reported exactly like one in your own file.

Shortened. The full README is on GitHub.

Nothing above is checked by us. What we check is on the safety report.

gonzalgo: common questions

Is gonzalgo MCP server safe?: Yes, by our scan: it is graded A (89/100). Read the gonzalgo safety report
How do I install gonzalgo?: It runs on your machine. Copy the Claude Code, Cursor, VS Code or Claude Desktop config from the install section.
Does gonzalgo need an API key?: Not as far as the registry entry and our scan can tell: no credentials are declared or required.
Is gonzalgo maintained?: The last commit was 33 days ago (2026-10-03). The latest release is v0.5.6.
How does gonzalgo compare with other MCP servers?: safety score 89/100 (higher than 80% of 48,243 servers); tools 10 (the typical server has 7); tools that change things 10% (typical: 0%. Fewer write tools means less an agent can break). Full comparison.