none of them rests on an unfinished proof
corpus 10,000 compiled under Lean 4.32 9,169 100.0% excluded: no parsable theorem header 1 excluded: never entered the environment 270 excluded: admitted carrying sorryAx 560 held out, failed to compile 831 depends on Classical.choice 8,496 92.7% choice dependence bound by the statement 7,899 86.1% choice dependence avoidable, proof only 597 6.5% choice-free entirely 673 7.3% rests on an unfinished proof 0 0.0% native_decide / compiler-trusted 0 0.0% axioms beyond propext, Quot.sound, Classical.choice 0 0.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 while the field agrees the check matters, no one had reported what it returns over a corpus.
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 831 fail on the version gap and are held out of every figure below.
Lean 4.32.
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.
Tools to check that exist — SorryDB strips sorryAx from agent output, AXLE's verify_proof rejects non-whitelisted axioms. What had not been done was running the check across a whole corpus and reporting what it costs.
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.
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 behavior is within Lean's stated design. It still propagates into every proof a model generates with that tactic.
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.
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 831 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.
That compilation is not verification is established. SorryDB (arXiv:2603.02668) removes <code>sorryAx</code> from agent output and calls it an exploit agents used to get around sorry verification. AXLE (arXiv:2606.26442) states it plainly: a passing compile accepts proofs containing sorry, unsound axioms, or incorrectly restated theorems. And Ammanamanchi, Bhat and Biderman (arXiv:2606.29493) audit five Lean benchmarks, surface 4,833 findings including 398 mechanically certified issues, and recommend that evaluation harnesses verify <code>#print axioms</code> output.
This note is the measurement that recommendation implies and nobody had taken: what the check costs on a real corpus. The mechanism was already known; the rate was not.
The two sides are complementary rather than competing. Those audits examine the benchmark STATEMENTS — whether a formalisation says what it should. This examines the prover OUTPUT — what a proof of it rests on. A harness can be right about one and blind to the other.
One distinction is worth keeping sharp. Lean issue #8212 documents <code>apply?</code> emitting a synthetic <code>sorry</code> without logging an error, so <code>lake build --wfail</code> exited 0 while the theorem was never added to the environment — the case DeepSeek-Prover-V2 output hit. That is a different failure from the 560 counted here, which ARE in the environment. A harness verifying the declaration exists catches the first and misses the second.
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,171-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.
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.
The table above, machine-readable: generated-proofs.json · generated-proofs.csv · CC-BY-4.0 · version 2026-08-13
One of the gonzalgo indexes — standing measurements of what formal libraries rest on. The per-proof results behind these totals are not published yet; releasing them means re-running the audit, and a summary is not a substitute for the rows.