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

A formal statement can typecheck, be provable, and still fail to express the intended informal mathematics. We study such statement-level errors in the review history of a Lean 4 library of formalized open problems. From squash-merged pull requests, we recover 74 natural negatives among 360 changed statements: semantic errors whose first pushed version differs from the reviewer-approved version. All 360 are labeled by one annotator against a 14-class error taxonomy, with the reviewers' corrections and comments available. We evaluate twelve frontier models (eleven with scoreable output) with and without those corrections. The highest agreement with the reference labels is F1=0.79 (κ=0.73) when corrections and comments are supplied, versus 0.56 (κ=0.46) for detection from the informal statement and candidate formalization alone. Wrong carriers and definitional mismatches are particularly difficult. Additional file context helps some models but does not close the gap. Among complete-coverage models, the same detection prompt yields F1=0.74–1.00 on rule-written synthetic errors versus 0.29–0.52 on natural errors restricted to rule-supported classes. The corpus of 5,726 documented statement pairs, the labeled negatives, model predictions, and evaluation code are publicly released.