AXIOM PROVENANCE
FOR LEAN 4

gonzalgo  ·  which step introduced it, and could it not have

#print axioms tells you a theorem depends on Classical.choice. It does not tell you which of the eight tactics in the proof put it there, whether the theorem's own statement required it, or whether a constructive route exists.

Those are the questions gonzalgo answers.

Lean 4Metamath Apache-2.0macOS · Windows · Linux

pip install gonzalgo

PyPI · Source · FAQ · Indexes · Kernel Index · Dominator Table · Controlled Tactics · Spend Points · Substitution Ledger · Entry Points · Tactic Bands · Cleanable · set.mm Axioms · Site Diagnosis · Choice Strength · Version Delta · Module Spend · Metamath Axioms · Kernel Trust Profile · Generated proofs

Papers: where axioms are spent · why tactic rates cannot attribute them

The distinction the tool is built on

A theorem about the real numbers depends on the axiom of choice because ℝ is constructed with it. No proof of that theorem avoids it. A theorem about the integers that comes out classical because a tactic reached for Classical.propDecidable is a different situation entirely, and a fixable one.

gonzalgo separates a theorem's statement dependencies from its proof dependencies, so those two cases stop looking identical. Across 9,169 machine-generated Lean proofs, 92.7% depend on choice — but 86.1% of them are fixed by what the theorems say, and only 6.5% are avoidable. Without the split you would report the first number and mean nothing by it.

Questions it answers

Which step introduced this axiom?

gonzalgo why gives the shortest path from a declaration to an axiom, labelling every step a statement dependency or a proof dependency — so you can see where it entered and whether it can be rerouted. This is how the omega and norm_num defects in the papers were found.

Could this theorem be stated without the axiom of choice?

gonzalgo eligible computes the band whose statements are choice-free while their proofs are not — an upper bound on what could be removed. For Mathlib that is 13.1% of theorems, against a figure of 55% that circulates without a measurement behind it.

If I change this definition, what breaks?

gonzalgo impact splits dependents into those naming it in a statement, whose meaning changes with it, and those using it only in a proof, which simply rebuild.

How do I know if my proof depends on a sorry?

Lean warns once, on the line you typed. It says nothing about the theorem three files later that uses that lemma and is therefore also not proved. gonzalgo trust reports every theorem reaching a sorry anywhere upstream, however far, and fails CI when one does.

For that job alone — an allowlist gate in CI, nothing else — the Lean community maintains axiom-audit, which is Lean-native and needs no Python. Use it if a pass/fail gate is all you want. gonzalgo is for the questions above it.

Does my project use native_decide anywhere?

A native_decide result is 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 reports the axioms it emits and how many theorems inherit them.

What axioms does this theorem depend on, and why?

#print axioms answers whether. gonzalgo why gives the shortest path from a declaration to an axiom and labels every step as a statement dependency or a proof dependency — so you can see which step introduced it, and whether it can be rerouted.

Int.mem_box
  --proof--> Int.mem_box._proof_1_5
    --proof--> Classical.propDecidable
      --proof--> Classical.choice

Can I fail a build when a proof rests on something unfinished?

Yes. Three lines:

- uses: vince-gonzalez/gonzalgo@v1
  with:
    module: MyProject

Name the workflow kernel-clean and GitHub's ordinary status badge reads kernel-clean ✓. It certifies that no theorem in the project is standing on an unfinished proof, and that none were decided by running compiled code instead of by the kernel.

Measured

Applied to Lean 4.32.1 with Mathlib — 790,171 declarations, 30 million dependency edges — reported in the accompanying paper:

Mathlib's compiler-trust surface comes to two opaque primitives that no mathematical result reaches, and nothing anywhere rests on a sorry. Both checked rather than assumed — at this scale there was previously no way to check them.

The Kernel Index

Fourteen formal libraries, measured and published: what each one rests on, as a table and as JSON and CSV. Across 532,579 Lean theorems in nine libraries and 71,124 Metamath theorems in five databases, none rest on an unfinished proof and none rest on the compiler.

Read the Kernel Index →

Also

Reads the Metamath databases set.mm, iset.mm, nf.mm, ql.mm and hol.mm with the same measurements and the same code, so foundations as different as ZFC, intuitionistic logic, New Foundations, quantum logic and higher-order logic are compared under identical definitions rather than by analogy.