Auditing Reveals Flaws in AI Theorem Proving Benchmarks

Benchmarks used to evaluate Large Language Model (LLM)-assisted theorem proving in Lean are often considered highly reliable because every solved problem comes with a machine-verified proof. However, this research reveals a critical oversight: the Lean kernel only confirms the formal correctness of a statement, not whether that statement accurately represents the original informal problem or if the evaluation methods are resilient to trivial or adversarial solutions. A comprehensive audit of five prominent Lean theorem-proving benchmarks and their derivatives identified nearly 5,000 issues. Among these, 398 were mechanically certified defects, including instances of counterexamples, vacuous theorems, and unsound axioms. The audit also documented semantic flaws such as missing hypotheses, oversimplified problems, incorrect translations, and Lean-specific specification hazards. Beyond dataset construction, the study examined evaluation-time failures, demonstrating that these defects can both artificially inflate and deflate reported prover scores. To address these issues, the researchers propose a fault taxonomy, a suite of automated checkers, and recall-oriented semantic audit prompts, along with new standards for creating more trustworthy and reproducible formal math datasets and evaluations.