What 9,169 machine-generated Lean proofs rest on

none of them rests on an unfinished proof

corpus                        10,000
compiled under Lean 4.32       9,169
held out, failed to compile      560

reach Classical.choice         8,496    92.7%
  statement-bound              7,899    86.1%   unavoidable
  avoidable, proof only          597     6.5%
choice-free entirely             673     7.3%

rests on an unfinished proof       0
native_decide / compiler trust     0
axioms beyond the standard three   0

A language model that writes a Lean proof 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 and nobody has measured it.

This is that measurement, over the Goedel-Prover output for the Lean Workbook problems — 10,000 proofs, of which 9,169 still compile under Lean 4.32. The other 560 fail on the version gap and are held out of every figure below.

Lean 4.32.

The result

Every proof that compiles proves its theorem. None rests on an unfinished proof, none was obtained by trusting the compiler instead of the kernel, and none cites an axiom outside the three that all of Mathlib rests on.

That has not previously been checkable about a generated corpus. It could be asserted; it could not be shown.

Classical dependence, and what it means

8,496 of the 9,169 — 92.7% — depend on the axiom of choice. Read alone that number is alarming and it is also nearly meaningless.

7,899 of them depend on it because of what they SAY. The theorem is about the real numbers, the reals are constructed with choice in Mathlib, and no proof of such a statement can avoid it. The dependence is a property of the claim.

597 depend on it only because of HOW they were proved. Nothing in those statements needs choice; a different proof would not carry it. That is 6.5% of the corpus, and it is the only part anyone could act on.

Separating the statement from the proof is what turns 92.7% into two numbers that mean different things. Without it the honest report and the misleading one are the same figure.

Where the avoidable dependence comes from

A tactic, mostly. 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. It reproduces in one line with no imports.

This was reported upstream and closed as completed, with the reply that avoiding choice is a deliberate non-goal of Lean core. The behaviour is within Lean's stated design. It still propagates into every proof a model generates with that tactic.

Why the whole corpus, and not a sample

Measuring only the proofs that invoke omega returns 46.6% avoidable. That figure is wrong by a factor of seven, and wrong for a reason worth stating: omega operates on Nat and Int, which is exactly the population whose statements are choice-free and whose dependence is therefore removable.

Any sample drawn on tactic use selects on the outcome. The denominator has to be the corpus.

Separating drift from finding

Lean admits a declaration whose proof failed to elaborate, carrying sorryAx. In a report that is indistinguishable from a proof that was genuinely never finished, so the two have to be told apart by the compiler's error output rather than by the axiom set.

520 theorems reach sorryAx and every one of them is among the 560 that failed to compile. Of the 9,169 that compiled, none does. Compile failures are held out of every figure here; a corpus targeting Lean 4.27 measured under 4.32 would otherwise report version drift as a property of the proofs.

Method

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

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 itself traversed in both directions returning identical sets. The kernel's own bookkeeping is what is reported here.

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, and a goal over the reals must show choice in both. All three behave as required.

Reproducing it

The corpus is banach1729/goedel-workbook-lean427 on Hugging Face, Apache-2.0. The tool is pip install gonzalgo. Compile the proofs in batches against Mathlib and run the axiom report; the whole thing takes a few hours on a laptop and needs no Lean expertise.