The benchmarks used to measure AI progress on formal math are riddled with defects — and the machine-checker everyone trusts isn't catching them.
Researchers audited five widely used Lean theorem-proving benchmarks and their forks, running corpus-scale static analysis across the datasets. They surfaced 4,833 findings in total. Of those, 398 were mechanically certified problems: counterexamples that disprove stated theorems, vacuous theorems that are trivially true, and unsound axioms that corrupt any proof built on them. The rest were semantic defects — missing hypotheses, sloppy translations from informal math to formal statements, and specification traps specific to Lean's proof language. The researchers also documented how these flaws affect scores, showing that defects can push reported prover performance both up and down depending on which direction the error cuts.
This matters because the entire field treats Lean's kernel as a quality floor. The kernel confirms that a proof is formally valid — but it has no opinion on whether the formal statement actually encodes the problem anyone intended to solve. A model can "prove" a theorem that is a weaker or different claim than the benchmark intended, score the point, and no alarm sounds. If the leaderboards driving AI math research are measuring the wrong things, the field's sense of progress is unreliable.
The team released automated checkers, audit prompts, and corrected dataset snapshots at a public GitHub repository, and proposed a fault taxonomy to standardize how future datasets get built and reviewed. The timing is pointed: AI labs have leaned heavily on formal math benchmarks as prestige metrics precisely because machine-checked proofs seemed immune to the fuzziness that plagues natural-language evals. Turns out the fuzziness just moved upstream.