Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof. However, the kernel only checks that a proof establishes a \emph{formal} statement; it does not verify that the statement faithfully encodes the intended informal problem, nor that evaluation harnesses are robust to trivial or adversarial solutions. We audit five widely used Lean theorem-proving benchmarks and their forks, using corpus-scale static checkers to surface 4,833 findings, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms. We also document semantic defects such as missing hypotheses, problem simplification, incomplete or incorrect translations, and Lean-specific specification hazards. Beyond dataset construction, we survey evaluation-time failure modes and show, on corrected subsets, that defects can both inflate and deflate reported prover scores. We propose a fault taxonomy, a suite of automated checkers and recall-oriented semantic-audit prompts, and release standards to guide the creation of formal math datasets and make evaluation more reproducible and trustworthy. Our checkers, audit prompts, and corrected dataset snapshots are available at \url{https://github.com/Shashi456/atp-checkers}.

AI systems are increasingly judged on how much mathematics they can do, using benchmarks whose answers are verified by proof-checking software that guarantees each proof is logically airtight. The tests are widely trusted, but the software only checks that an answer proves the problem as written, not whether the problem was written correctly. It is like an exam grader who checks a student's working but never notices the question had a typo, was easier than intended, or could be answered on a technicality. We ran a large scale audit, using automated tools to scan about ten thousand problems across the five most widely used test sets. We found flawed questions are common: some omit a needed condition, some exploit quirks in the software's arithmetic (it treats 3 minus 5 as 0, and dividing by zero as 0), and some can be passed by loopholes. Our tools flagged thousands of suspicious cases and mechanically confirmed that nearly four hundred are genuinely broken. This matters because a flawed test misleads us about progress: correcting the bad questions can move reported AI scores both up and down. We release our checking tools and standards so future AI math tests are more trustworthy.