What Reviewers Catch and Frontier Models Miss: Statement-Level Errors in Autoformalization

A formal statement can typecheck and admit a proof while failing to express the intended mathematics. We study such statement-level errors where they naturally occur: in the human review process of a Lean 4 library of formalized open problems. From squash-merged pull-request history we recover 74 natural negatives, erroneous statements corrected during human review. Each is hand-labeled against a 14-class error taxonomy, using the reviewer's fix and comments as the reference. We then evaluate twelve frontier models. When shown the reviewer's correction and comments, the best model distinguishes semantic errors from non-semantic changes at $F_1=0.79$ ($\kappa =0.73$); without the correction, no model exceeds $F_1=0.56$. In detection, misses concentrate in the classes that depend on Lean semantics: wrong carriers, definitional mismatches, junk-value traps. Under the same detection prompt, the strongest models achieve drastically higher scores on evaluator-injected errors from the same error classes, with $F_1$ reaching $1.00$. Supplying the file's definitions, forcing a pass through the class list, or saying only that an error is present helps at most modestly; naming the reviewer-assigned error class dramatically improves class-level recall, but wrong hints also elicit substantial label compliance. The corpus of 5,726 reviewed (informal, formal) pairs, the labeled negatives, and the evaluation harness will be released.