Measure the Library First: What a Formalization Pipeline's "Verified" Output Actually Asserts

Our formalization pipeline reported twenty theorems from arXiv papers as fully verified, each with a machine-checked Lean proof. Auditing them, one carries mathematical content. Twelve are closed by a single tactic in their own generated theory, because the pipeline emits each paper's objects as constant stubs and a theorem over constants is a claim about constants; one invokes an axiom whose statement is the theorem verbatim; one formalizes a remark absent from the cited paper. Every proof compiles. Almost no statement asserts anything. We report six distinct paths by which the system recorded "proved" without a proof, each with a fix, a regression test, and the artifact that exposed it. They share a shape: in every case a guard existed and was correct but sat one stage away from the decision it protected. The vacuity check ran before the definitions that make statements vacuous were generated; the sorry filter lived on the backend that was not in use; a promotion gate was keyed on the translator's opinion of itself. We then find the same pattern in how progress on this task is reported. On miniF2F, twenty library automation tactics with no model close 36.1% of elaborating statements against 26.0% $\pm$ 0.9% for our full retrieval-augmented search loop; any advantage of search is bounded above by 2.1 points at 95% confidence, and removing premise retrieval entirely does not hurt. That floor is not fixed: across five Mathlib releases from December 2023 to April 2026 it steps up 7.2 points in one six-month window ($p < 0.001$) and then holds for two years, while the number of benchmark statements that compile at all moves independently and in the opposite direction, from 194 to 222 and back to 194 of 244. Pass rates from different snapshots are therefore computed over different problem sets at different floors. Every accepted proof in this paper was recompiled from its released artifact with its kernel axioms audited. We release the checks as standalone tools, including a detector that asks whether a formalized statement is closed by a single tactic in its own theory.