gonzalgo

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

[![PyPI](https://img.shields.io/pypi/v/gonzalgo)](https://pypi.org/project/gonzalgo/)
[![Python](https://img.shields.io/pypi/pyversions/gonzalgo)](https://pypi.org/project/gonzalgo/)
[![License](https://img.shields.io/pypi/l/gonzalgo)](LICENSE)
[![DOI](https://img.shields.io/badge/DOI-10.5281%2Fzenodo.21769846-blue)](https://doi.org/10.5281/zenodo.21769846)

<!-- mcp-name: io.github.zengineco/gonzalgo -->
<!-- ^ how the MCP Registry verifies this PyPI package belongs to that server
     name. It reads the package description, which is this README. Removing the
     line makes the next `mcp-publisher publish` fail package validation. -->


`#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.

```console
$ 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.

**Does my project use `native_decide` anywhere?**
`native_decide` results are obtained by compiling and running code and believing
the answer — the compiler and runtime are trusted, not the kernel, and soundness
bugs have been found there. `gonzalgo trust` reports `Lean.ofReduceBool` and
`Lean.ofReduceNat`, the axioms it emits, and how many theorems inherit them.

**What axioms does this Lean theorem actually depend on, and why?**
`#print axioms` tells you *whether*. `gonzalgo why <decl> -a <axiom>` gives the
shortest path from the theorem to the axiom, labelling each step as a statement
dependency or a proof dependency — so you can see which step introduced it and
whether it is reroutable.

**Can I fail CI when a proof rests on something unfinished?**
Yes. `--fail-on-trust`, or the GitHub Action below.

**If I change this definition, what breaks?**
`gonzalgo impact` splits dependents into those that name it in a *statement* —
whose meaning changes with it — and those that only use it in a *proof*, which
merely rebuild.

**kernel > sorry**

## What it found

Pointed at Lean 4.32.1 with Mathlib — 790,171 declarations, 30 million
dependency edges — the funnel from "the whole library" down to "provably
removable" runs like this:

```
   532,605   theorems in Mathlib
  ─────────────────────────────────────────────────────────────────────
   324,808   ██████████████████████████████░░░░░░░░░░  depend on Classical.choice   61.0%
       144   ▏                                         actually SPEND it (entry points)
  ─────────────────────────────────────────────────────────────────────
    69,571   ██████░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░░  could be stated without it   13.1%
                                                       └─ a ceiling, not an estimate
  ─────────────────────────────────────────────────────────────────────
       805   substitutable sites — a choice-free instance existed, unused
       280   declarations whose ONLY route to the axiom runs through one
       276   ▏ attributable to a single tactic  ────────────────────┐
       275   ▏ kernel-verified choice-free after substitution       │
         4   ▏ kernel REJECTED — and they are exactly the 4 NOT ────┘
             ▏ attributable to that tactic. The partition was not designed.
```

That single tactic is **`omega`**, which supplies the `Decidable` arguments of
six helper lemmas as a hardcoded `Classical.propDecidable` and never attempts
instance synthesis — so proofs as elementary as `a - b = 0 ↔ a ≤ b` over `Nat`
rest on the axiom of choice with no need. Filed upstream; the fix is one file.

---

## Let a language model call it

```console
$ pip install "gonzalgo[mcp]"
```

Add to your MCP client's configuration:

```json
{
  "mcpServers": {
    "gonzalgo": { "command": "gonzalgo-mcp" }
  }
}
```

Ten tools: `audit_trust`, `why`, `impact`, `axiom_reach`, `metamath_audit`,
`kernel_index`, plus the plumbing to produce a dump from a project.

There's also a `scope` tool that reports what gonzalgo can't do — read a paper,
mark homework, judge whether text is any good. It's there so a model asked "is
this proof correct?" about a page of prose doesn't grab the nearest proof-shaped
tool and return something meaningless. Every other tool restates the
precondition in its description.

The case it's built for: a generated Lean proof that fails to compile is easy to
spot. One that compiles while resting on a `sorry` three lemmas upstream isn't,
and Lean only mentions it once, in a warning, at the site.

`kernel_index` runs with no files and no network, so a model can call it cold for
figures on known libraries.

## Put it in CI, get a badge

Three lines in any Lean 4 project. Every commit is checked for theorems resting
on an unfinished proof or on trusting the compiler rather than the kernel.

```yaml
# .github/workflows/kernel-clean.yml
name: kernel-clean
on: [push, pull_request]
jobs:
  audit:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: zengineco/gonzalgo@v1
        with:
          module: MyProject
```

Then the badge, which is just the workflow's own status — no extra service:

```markdown
![kernel-clean](https://github.com/YOU/REPO/actions/workflows/kernel-clean.yml/badge.svg)
```

**What the badge actually certifies.** Not that the proofs are correct — Lean
already checks that. That no theorem in the project is standing on a `sorry`
somewhere upstream, and that none of them were decided by compiling and running
code instead of by the kernel.

Lean warns about the `sorry` you just typed. It says nothing about the theorem
three files later that quietly inherits it. In the worked example under
`examples/dirty`, Lean reports **one** warning and the audit finds **two**
contaminated theorems.

## How it fits together

```
        your Lean project
               │
               │  gonzalgo lean-files ./scripts
               │  lake env lean scripts/Split.lean
               ▼
     ┌───────────────────────┐
     │   dependency graph    │   one row per declaration:
     │  statement │ proof    │   KIND · NAME · stmt-deps · proof-deps
     └───────────┬───────────┘
                 │
                 │  gonzalgo check      ← refuses a dump with no proof terms
                 ▼
     ┌───────────────────────────────────────────────────┐
     │                                                   │
     ▼                  ▼                ▼               ▼
  amplify           eligible            why            audit
  ───────           ────────            ───            ─────
  where is the      how much is         which step     which sites are
  axiom spent,      even eligible       introduced     substitutable, and
  and how far       for removal?        it?            which declarations
  does it reach?    (the ceiling)                      go clean if you fix
                                                       every one
                                                            │
                                                            ▼
                                                   lake env lean Rewrite.lean
                                                   ───────────────────────────
                                                   swap the instance in and ask
                                                   the KERNEL if the proof holds
```

Nothing above the kernel step is trusted on my say-so: `Substitute.lean` decides
substitutability with `colle