Ground False: Dissecting Errors in Formal Mathematics Benchmarks

The ground truths in formal mathematics benchmarks are taken on faith. For theorem proving, released formalizations come without formal proofs that certify their correctness. For autoformalization, faithfulness to the informal source is judged only by the benchmark authors, yet such judgments are inherently subjective and lack collective consensus. We show these assumptions fail at scale: our audit of 367 ProofNet formalizations shows that 104 (28\%) are mathematically false, and a further 100 (27\%) are not false yet still unfaithful, for a total of 204 (56\%) unfaithful items. We dissect these errors along three axes (provability, logical strength, root cause) and show they bias evaluation in predictable, asymmetric directions: false ground truths cap theorem-proving signal, while equivalence-based autoformalization metrics compress model gaps through capping and coincidental agreement. We release the corrected benchmark ProofNet-Verified, produced by a semi-automated pipeline combining Lean provability checks, an LLM faithfulness judge, and human review. Applying the same pipeline to six other benchmarks reveals that unfaithful-GT rates span more than an order of magnitude (4.8\% to 60.0\%), confirming that the failure modes generalize while absolute quality is dominated by curatorial process. Our data and code are available at https://github.com/marcusm117/ProofNet-Verified.