Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving
For researchers evaluating LLM-assisted theorem provers, this work reveals that existing benchmarks contain systematic defects that compromise reliability, and provides tools to mitigate these issues.
The paper audits five widely used Lean theorem-proving benchmarks, uncovering 4,833 findings including 398 mechanically certified issues such as counterexamples and vacuous theorems. It shows that dataset defects can both inflate and deflate reported prover scores, and proposes a fault taxonomy, automated checkers, and release standards to improve evaluation trustworthiness.
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 to make evaluation more reproducible and trustworthy. Our checkers, audit prompts, and corrected dataset snapshots are available at https://github.com/Shashi456/atp-checkers.