Metadata-Version: 2.4
Name: gonzalgo
Version: 0.1.0
Summary: Measure where a formal library spends its axioms — Lean 4 and Metamath.
Project-URL: Paper, https://doi.org/10.5281/zenodo.21769847
Project-URL: Source, https://github.com/zengineco/gonzalgo
Project-URL: Issues, https://github.com/zengineco/gonzalgo/issues
Author: Vince Gonzalez
License-Expression: Apache-2.0
License-File: LICENSE
License-File: NOTICE
Keywords: axiom-of-choice,constructive-mathematics,dependency-analysis,formal-verification,lean4,mathlib,metamath,proof-assistant
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Operating System :: OS Independent
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Requires-Dist: numpy>=1.23
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == 'dev'
Description-Content-Type: text/markdown

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

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

```console
$ 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?**

```console
$ 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?**

```console
$ 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?**

```console
$ 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:**

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

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

```python
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:

| 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.21769847](https://doi.org/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.
