Structural Coverage: Do AI Provers Use Mathlib the Way Mathematicians Do?

A Lean proof is not only a binary success. It is a selection of premises from a library, and that selection induces a subgraph of mathlib4's dependency graph. Two proofs can both be correct and induce structurally different subgraphs; pass@k is blind to the difference. We define structural coverage over these subgraphs and compare 29,750 released machine Lean proofs against 70,086 human mathlib declarations. Three findings. (i) Machine proofs draw on a small subset of the human premise vocabulary, one to two orders of magnitude smaller: 78,642 against 1,127 premises, Jaccard 0.0129, leaving 98.7% of the human vocabulary untouched. The gap survives every control we build, narrowing to 19x-28x when the human corpus is restricted to the regions the machine corpus occupies and to 5.7x under an exploratory genre-matched comparison against mathlib's own competition archive. (ii) The machine corpus concentrates on a stratum that is essentially absent from mathlib: arithmetic-tactic proofs of at most two tactic steps are 23.1% of the machine corpus and 0.02% of mathlib, and a single premise, sq_nonneg, accounts for 27.0% of all machine premise occurrences. (iii) A cautionary negative result: the graph's published depth attribute proved to be a centrality proxy, not a derivation-length measure, and we withdraw a finding built on it. Structural coverage is a non-redundant evaluation axis, cheap to compute from released corpora.