gonzalgo

Install

Works with Claude Code, Codex, VS Code, Cursor, Windsurf, Claude Desktop. Read the repository before you give any tool access to your data.

npx agentmarket install connector/vince-gonzalez-gonzalgo

About

No reviews yet. Installed it? Reviews come from verified installers only. How reviews work

Permissions

What this server can do and what it asks for, from its tool list, install config and code. Checked Oct 25, 2026.

Tools

5 read · 1 write · 0 delete · 4 not yet classified

Secrets

None asked for

Install scripts

None found

Runs as

Python package

Tools (10)

Read from the source code; the running server may differ. Descriptions are the server’s own words; hidden characters are shown as [U+…].

• audit_trust

  THE SAFETY CHECK. Given a Lean dependency dump, report whether any theorem rests on an unfinished proof (`sorry`) or on trusting the compiler (`native_decide`), and how far an optional axiom reaches. This is the tool to reach for when asked whether a formalisation is sound, complete, or trustworthy. Requires a dump — see how_to_extract.

• axiom_reach

  How far an axiom reaches through a library, and where it is actually spent rather than inherited. Reports dependents, entry points (the declarations citing it directly — the positions someone would have to edit to remove it) and amplification.

• check_dump

  Verify a dependency dump is usable before drawing conclusions from it. Raises if the dump contains no proof terms, which silently inverts every downstream number. Cheap; call it when a dump's provenance is unknown.

• how_to_extract

  Return the exact commands that produce the dependency dump every other tool needs, for a given Lean 4 project directory. Use when the user has a Lean project but no dump yet.

• impact

  What breaks if this declaration changes. Splits dependents into those naming it in a STATEMENT — whose meaning changes with it, so their own users may need rewriting — and those using it only in a PROOF, which merely rebuild. Use before a refactor, or to judge how risky a change is.

• kernel_index

  The Kernel Index: published measurements of what well-known formal libraries rest on — Mathlib, Lean core, Std, Batteries and others, plus five Metamath databases. Needs no files and no dump. Use it to answer questions about known libraries, or to give a user a reference point for their own numbers.

• metamath_audit

  Audit Metamath databases (set.mm, iset.mm, nf.mm, ql.mm, hol.mm). Reports theorems, logical axioms identified by typecode rather than naming convention, entry points and amplification. Give filesystem paths to the .mm files.

• scope

  Report what gonzalgo can and cannot answer. CALL THIS FIRST when a user asks anything resembling 'is this proof correct', 'does this paper check out', 'check my homework', or 'is this AI slop'. It will tell you whether the question is answerable with these tools, and what to say if it is not. Takes no arguments and needs no files.

• why

  Explain WHY a declaration depends on an axiom: the shortest dependency path, with each step labelled a statement dependency or a proof dependency. `#print axioms` answers whether; this answers why. A path made only of proof edges can often be rerouted; a statement edge cannot be touched without changing what the theorem says.

• write_lean_extractors

  Write the Lean extractor files into a directory, so the user can run them against their own project. Returns the paths written.

Signals

Stars

2

Forks

0

Open issues

0

Weekly downloads

89

Last commit

Oct 3, 2026 (25 days ago)

Last release

Sep 11, 2026 (1 month ago)

Last package publish

Sep 11, 2026 (1 month ago)

From GitHub (fetched Oct 24, 2026) and the package registry.

Details

Registry name

io.github.vince-gonzalez/gonzalgo

Version

0.5.6

Auth

No auth

Packages

pypi gonzalgo

License

Apache-2.0

Repository

github.com/vince-gonzalez/gonzalgo

Website

f-keys.com/gonzalgo/

First seen

Oct 24, 2026

Last checked

Oct 24, 2026

Source

Official MCP Registrygithub-graphql