gonzalgo

Measure where a formal library spends 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

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

Quickstart

Generate a dump from your own Lean project, then ask questions of it.

$ gonzalgo lean-files ./scripts        # writes the Lean extractors
$ cd my-lean-project
$ lake env lean scripts/Split.lean     # -> mathlib_split.tsv
$ gonzalgo check mathlib_split.tsv     # verify it actually contains proofs

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.

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

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)      # why
g.entry_points(lean.AXIOM, among="T")     # where it is spent
g.dependents(lean.AXIOM)                  # boolean mask over all nodes
lean.eligibility(dump, g).ceiling         # what fraction could be removed

Shipped Lean sources

gonzalgo lean-files writes these into a directory of your choosing:

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.21769847.

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.

Attribution and 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.