vince-gonzalez/generated-proofs-axioms

What machine-generated Lean proofs rest on

Per-theorem axiom dependencies for 9,729 machine-generated Lean 4 proofs.

A model writing Lean gets one bit of feedback: the proof compiles, or it does not. What the proof ends up standing on is not part of that signal. This is that measurement, over the Goedel-Prover output for the Lean Workbook problems.

Headline

Of the 9,169 proofs that still compile under Lean 4.32:

Every proof that compiles proves its theorem.

92.7% depending on the axiom of choice reads alarmingly and means almost nothing on its own. 86.1% of those depend on it because of what they say — the theorem is about the real numbers, which Mathlib constructs with choice, and no proof of such a statement can avoid it. Only 6.5% depend on it because of how they were proved. Separating the statement from the proof is what turns one number into two that mean different things.

Fields

Read this before computing anything

Filter `compile_error == False`. The corpus targets Lean 4.27; this was measured under 4.32. 560 proofs fail on the version gap, and Lean admits a declaration whose proof failed to elaborate carrying `sorryAx`. Those rows are present so the drift is auditable, but including them silently reports version skew as a property of the proofs.

All 520 reaches_sorry rows lie inside those 560. Among the 9,169 that compile, none reaches sorryAx.

import pandas as pd
df = pd.read_csv("data/axioms.csv")
ok = df[~df.compile_error]           # 9,169 rows
ok.choice_eligible.mean()            # 0.065
ok.reaches_sorry.sum()               # 0

Method

Axioms come from Lean.collectAxioms, the call behind #print axioms, run per theorem inside the environment. Statement axioms are the union over constants appearing in the theorem's type.

Controls fixed before measuring: a Nat goal closed by omega must show choice in the proof and not the statement; a structural proof must show nothing; a goal over the reals must show choice in both. All three behave as required.

Cross-checked against an independent route — serialising the whole 790,000-declaration environment and recomputing reachability outside Lean gives the same answer on the same subset, and that graph was traversed in both directions returning identical sets.

Why the whole corpus and not a sample

Measuring only the proofs that invoke omega returns 6.5% → 46.6% avoidable. That is wrong by a factor of seven: omega operates on Nat and Int, exactly the population whose statements are choice-free and whose dependence is therefore removable. Any sample drawn on tactic use selects on the outcome.

Where the avoidable dependence comes from

Largely one tactic. omega supplies the Decidable argument of six helper lemmas as a literal Classical.propDecidable and never attempts instance synthesis. On Nat and Int the constructive instance exists and is axiom-free, so an otherwise constructive proof comes out classical. Reported upstream and closed as completed, with the reply that avoiding choice is a deliberate non-goal of Lean core.

Reproducing

pip install gonzalgo

Compile the corpus in batches against Mathlib and run the axiom report. Full method and definitions: <https://doi.org/10.5281/zenodo.21769846>

Citation

@dataset{gonzalez2026genproofs,
  author = {Gonzalez, Vince},
  title  = {What machine-generated Lean proofs rest on},
  year   = {2026},
  url    = {https://f-keys.com/gonzalgo/generated-proofs/},
  note   = {Measured with gonzalgo; method at doi:10.5281/zenodo.21769846}
}

Source corpus: `banach1729/goedel-workbook-lean427`, Apache-2.0. This dataset is Apache-2.0.