╔════════════════════════════════════════════════════════════════════════════════════════════╗
║ ║
║ ██████╗ ██████╗ ███╗ ██╗███████╗ █████╗ ██╗ ██████╗ ██████╗ ║
║ ██╔════╝ ██╔═══██╗████╗ ██║╚══███╔╝██╔══██╗██║ ██╔════╝ ██╔═══██╗ ║
║ ██║ ███╗██║ ██║██╔██╗ ██║ ███╔╝ ███████║██║ ██║ ███╗██║ ██║ ║
║ ██║ ██║██║ ██║██║╚██╗██║ ███╔╝ ██╔══██║██║ ██║ ██║██║ ██║ ║
║ ╚██████╔╝╚██████╔╝██║ ╚████║███████╗██║ ██║███████╗╚██████╔╝╚██████╔╝ ║
║ ╚═════╝ ╚═════╝ ╚═╝ ╚═══╝╚══════╝╚═╝ ╚═╝╚══════╝ ╚═════╝ ╚═════╝ ║
║ ║
║ 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.
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
$ pip install "gonzalgo[mcp]"
Add to your MCP client's configuration:
{
"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.
name: kernel-clean
on: [push, pull_request]
jobs:
audit:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: vince-gonzalez/gonzalgo@v1
with:
module: MyProject
Then the badge, which is just the workflow's own status — no extra service:
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 collectAxioms, and Rewrite.lean submits the rewritten
proof term to addDecl. A name-based screen was tried first and measured 41.5%
precision, which is why none of this reads names.
Quickstart
Generate a dump from your own Lean project, then ask questions of it.
$ gonzalgo lean-files ./scripts
$ cd my-lean-project
$ lake env lean scripts/Split.lean
$ gonzalgo check mathlib_split.tsv
Why does this theorem need choice?
$ gonzalgo why mathlib_split.tsv Int.mem_box
Int.mem_box
Int.mem_box
--proof--> Int.mem_box._proof_1_5
--proof--> Classical.propDecidable
--proof--> Classical.choice
Every hop is labelled stmt or proof, and that label is the point: a proof
edge can often be rerouted by changing a tactic, a statement edge cannot be
touched without changing what the theorem says. A path made only of proof edges
is what makes a declaration worth patching at all.
If I change this, what breaks?
$ gonzalgo impact mathlib_split.tsv Nat.decLe
Nat.decLe
reached transitively 398,968 (295,411 of them theorems)
── direct ──
in a STATEMENT 626 API surface: changing the
type changes their meaning
in a PROOF only 4,225 insulated: a type-preserving
change costs a recompile
why run backwards. The statement/proof split is the value: a declaration whose
type mentions the target has the target in its API, so its meaning moves when
the target moves and its own users may need rewriting. One that merely calls it
inside a proof needs nothing but a rebuild. A plain "who uses this" cannot tell
them apart, which is why it can't tell you whether a change is safe.
How far does an axiom reach, and where is it spent?
$ gonzalgo amplify mathlib_split.tsv
axiom Classical.choice
theorems 532,605
dependents 324,808 reach 61.0%
entry points 144 2.704e-04 per theorem
amplification 2,256x
How much of that could even in principle be removed?
$ gonzalgo eligible mathlib_split.tsv
statement CHOICE-FREE, proof dep 69,571 13.1% <- eligible
...
ceiling on removable classical dependence: 13.1%
A theorem whose statement mentions something choice-dependent cannot be made
choice-free however it is proved. Only the rest are candidates, and that figure
is a ceiling, not an estimate.
Metamath, same measurements:
$ gonzalgo mm set.mm iset.mm nf.mm
set.mm
theorems 47,621
logical axioms (|-) 1,561 used 1447
median entries per axiom 2.0
overall amplification 292.1x
Kernel Trust Profile
gonzalgo profile writes what a library rests on as JSON, meant to be committed
and read by other programs:
$ lake exe gonzalgo MyProject myproject.tsv
$ gonzalgo profile myproject.tsv --name MyProject -o kernel-trust.json
{
"ktp_version": "0.1",
"subject": { "name": "Lean core + Std", "revision": "…", "system": "Lean 4" },
"counts": { "theorems": 88842 },
"unfinished": { "theorems_reaching": 0, "axioms": ["sorryAx"] },
"compiler_trusted": { "theorems_reaching": 0 },
"assumptions": [
{ "name": "Classical.choice", "kind": "optional",
"entry_points": 24, "reach": { "theorems": 31516, "fraction": 0.3548 },
"via": "both" }
]
}
Two rules do most of the work. An unmeasured field is null, never 0 —
Metamath has no native_decide, so its compiler_trusted count is
not-applicable rather than zero, and writing zero would be a claim nobody made.
And revision is refused on a dirty tree, because a profile whose commit
does not describe what was measured cannot be reproduced by anyone else.
There is no summary score, deliberately. A theorem either reaches an unfinished
proof or it does not; averaging that against anything else invents precision the
measurement does not have.
Full specification: Kernel Trust Profile 0.1 (Zenodo).
A sample is in examples/lean-core-kernel-trust.json.
Reach versus amplification
Under inlining and factoring — operations that change how a library is written,
not what it proves — the set of dependents is invariant while the set of
entry points is not. Rerouting every use of an axiom through one gateway
lemma, or inlining that lemma, moves amplification anywhere between 1 and the
number of dependents without changing a single theorem.
So reach bears comparison between libraries; amplification describes one
library's factorisation. The tool reports both and this README says which is
which, because the distinction is easy to lose and expensive to lose.
One hazard worth knowing about
In Lean 4.32, ConstantInfo.value? returns none for theorems unless
called as value? (allowOpaque := true), and this has changed across releases.
An extractor written the obvious way records no proof terms at all: every
theorem's value comes back empty, the analysis silently measures statements, and
reports them as proofs. Nothing about the output looks wrong — the library just
appears cleaner than it is.
gonzalgo check exists for this, and every subcommand runs it before trusting a
dump:
$ gonzalgo check bad_dump.tsv
ERROR: bad_dump.tsv: 532,605 theorems, none carrying a proof term.
The extractor called `ConstantInfo.value?` without `(allowOpaque := true)` ...
It raises rather than warns. A dump with no proof terms does not produce
slightly worse numbers; it produces confidently wrong ones.
Library use
from pathlib import Path
from gonzalgo import lean
dump = Path("mathlib_split.tsv")
lean.check_dump(dump)
g = lean.load(dump)
g.path_to("Int.mem_box", lean.AXIOM)
g.entry_points(lean.AXIOM, among="T")
g.dependents(lean.AXIOM)
lean.eligibility(dump, g).ceiling
As a Lake package
This repository is also a Lean library, so the extractor can be a dependency
rather than a file you copy and edit. Add to your lakefile.toml:
[[require]]
name = "gonzalgo"
git = "https://github.com/vince-gonzalez/gonzalgo"
Then no scratch file at all — it imports the target module at runtime:
$ lake exe gonzalgo MyProject myproject.tsv
importing MyProject ...
declarations written: 204543
now run: gonzalgo check myproject.tsv
Everything the module imports is included, and the fifth output column records
which module each declaration came from, which is what separates your project
from its dependencies afterwards.
If you would rather call it from inside a file, the library is two lines:
import Gonzalgo
#eval Gonzalgo.dumpSplit "myproject.tsv"
The library requires Lean only — no Mathlib dependency, deliberately, since
pinning a Mathlib revision here would force one on every project being measured.
Run against Lean core and Std alone, that gives:
axiom declared direct theorems
sorryAx yes 0 0
Lean.ofReduceBool yes 0 0
Classical.choice yes 32 31,516
propext yes 13,246 70,150
CLEAN: no theorem here rests on an unfinished proof or on the compiler.
88,842 theorems, and 32 declarations spend Classical.choice where 31,516
inherit it.
Shipped Lean sources
gonzalgo lean-files writes these into a directory of your choosing. Prefer the
Lake package above for Split.lean's job; these are for the analyses that go
beyond extraction, and for projects not using Lake.
| file | what it does |
|---|
Split.lean | declaration graph, statement and proof deps in separate columns |
Substitute.lean | re-synthesizes each classical-decidability site, classifies by collectAxioms |
Rewrite.lean | rewrites proof terms and kernel-checks the substitution |
OmegaFix.lean | a patched omega frontend — demonstration only, see below |
Extract.lean | earlier graph dump, superseded by Split.lean |
Substitute.lean decides substitutability with the kernel's own bookkeeping
rather than by name. A name-based screen measured 41.5% precision on set.mm;
its characteristic failure is a lemma that relocates choice into an antecedent
instead of discharging it, which looks like progress and is not.
Background
This package is the tooling behind Where Formal Libraries Spend Their Axioms:
A Cross-Foundation Measurement, and an Avoidable Classical Dependency in Lean's
omega — 10.5281/zenodo.21769846.
Applied to Lean 4.32.1 with Mathlib (790,171 declarations, 30M dependency
edges), it finds 280 declarations whose only route to Classical.choice runs
through a substitutable site, 276 of them attributable to a single cause in the
omega decision procedure. Rewriting all 280 proof terms and submitting them to
the kernel: 276 accepted, 4 rejected, 275 left free of Classical.choice.
Referenced by
- keithadler/tenet — an independent Lean 4
kernel checker in C#/.NET. Its
tenet why traces which step introduced an
axiom, the same question as gonzalgo's why for Lean.
Who wrote this, and how to cite it
Vince Gonzalez — ORCID 0009-0005-3640-014X
· f-keys.com/gonzalgo
@software{gonzalgo,
author = {Gonzalez, Vince},
title = {gonzalgo: axiom provenance for Lean 4 and Metamath},
year = {2026},
url = {https://github.com/vince-gonzalez/gonzalgo},
doi = {10.5281/zenodo.21769846},
license = {Apache-2.0}
}
Archived at Software Heritage as
swh:1:dir:871f62fca5b737da9b4f99516d3689d23ffbc60d, which resolves whether or
not this repository does. The qualified form, carrying the origin, visit and
anchor, is in codemeta.json.
Papers. Both CC-BY, both with archives that regenerate every figure from the
shipped data with one command.
Licence
Apache-2.0. See LICENSE and NOTICE.
OmegaFix.lean is a modified copy of Lean 4's
src/Lean/Elab/Tactic/Omega/Frontend.lean, Copyright (c) 2023 Lean FRO, LLC,
used under Apache-2.0. Its modifications are listed in a notice at the top of
that file. It exists to demonstrate that a proposed fix compiles and produces
choice-free proofs; it is not a replacement for omega and should not be used
as one.
Not affiliated with or endorsed by the Lean FRO or the Mathlib community.
╔════════════════════════════════════════════════════════════╗
║ ║
║ ███████╗ ██╗ ██╗███████╗██╗ ██╗███████╗ ║
║ ██╔════╝ ██║ ██╔╝██╔════╝╚██╗ ██╔╝██╔════╝ ║
║ █████╗ █████╗█████╔╝ █████╗ ╚████╔╝ ███████╗ ║
║ ██╔══╝ ╚════╝██╔═██╗ ██╔══╝ ╚██╔╝ ╚════██║ ║
║ ██║ ██║ ██╗███████╗ ██║ ███████║ ║
║ ╚═╝ ╚═╝ ╚═╝╚══════╝ ╚═╝ ╚══════╝ ║
║ ║
║ · C R E A T I V E · ║
║ ║
║ ──────────────────────────────────────── ║
║ ║
║ Vincent Gonzalez ║
║ f-keys.com ║
║ ORCID 0009-0005-3640-014X ║
║ ║
╚════════════════════════════════════════════════════════════╝
Part of F-Keys — independent hardware, software
and internet products. See the working log
and live status.