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

An autoformalization pipeline that ingests arXiv papers, translates theirtheorem statements into Lean 4 and searches for proofs reported twenty theoremsas fully verified, each with a machine-checked proof. On audit, one carriesmathematical content. Twelve are closed by a single tactic in their own generatedtheory, because the pipeline emits each paper's objects as constant stubs and atheorem over constants is a claim about constants. One invokes an axiom whosestatement is the theorem verbatim. One formalizes a remark absent from the citedpaper. Every proof compiles. This deposit contains the paper and everything needed to check it. The paperreports 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 ashape: in every case a guard existed and was correct but sat one stage away fromthe decision it protected. It then reports the same pattern in how progress on this task is measured. OnminiF2F, twenty Mathlib automation tactics with no model close 36.1 percent ofelaborating statements, against 26.0 plus or minus 0.9 percent for a fullretrieval-augmented search loop; any advantage of search is bounded above by 2.1percentage points at 95 percent confidence. That floor is not fixed. Across fiveMathlib releases from December 2023 to April 2026 it steps up 7.2 points in onesix-month window (McNemar p less than 0.001) and then holds for two years, whilethe number of benchmark statements that compile at all moves independently and inthe opposite direction, from 194 to 222 and back to 194 of 244. Pass rates fromdifferent snapshots are therefore computed over different problem sets atdifferent floors. Contents: the paper in named and anonymous builds with LaTeX sources; fifteenbenchmark artifacts with full per-problem records, each carrying its Leantoolchain, git commit and seed; four standalone verification tools, including adetector that asks whether a formalized statement is closed by a single tactic inits own theory; the shell drivers that produced the artifacts; and a plan mappingevery number in the paper to the command that produced it. Code is released under the MIT licence.