A Prover's Share of Mathlib: Measuring Premise Coverage Without Running Lean

A Lean proof the kernel accepts is correct; it is also a selection of premises from a library, and pass@k is blind to that selection. We ask what can be measured about it from released artifacts alone (a published mathlib dependency graph and pre- verified proof corpora, with no Lean invocation), and how reliably. The instrument needs characterizing first. The release’s explicit-edge flag does not mean “written in source”, so no source-level extractor, however good, reaches unit retention against it. We therefore report retention as a scope decomposition, at 0.6124, of which 0.8815 is what a per-declaration instrument can reach and the rest is not addressable by reading source. That efficiency is flat across tactic classes, so the instrument does not fail preferentially on the proof styles that separate the corpora. We quantify the displacement our own extractor induces, and show that proof length must be measured on a wrap-invariant axis, because character counts measure source formatting rather than proof size. Measured with that instrument, mathlib’s proofs draw on 78,642 distinct premises against 1,127 for a released machine corpus: 69.8×on the full corpora, 28.5×restricted to the library regions the machine vocabulary occupies, and 18.8×matched on proof count, tactic class and proof length, with the human-only fraction falling from 98.7% to 96.3% across those designs. Only 113 premises are machine-only, and 25.6% of the machine vocabulary is language infrastructure rather than mathematics. A depth finding we built on a released per-declaration attribute is withdrawn, because the attribute is a centrality proxy. The one-line check that would have caught it is to correlate a derived attribute against in-degree and inspect its extremes.