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

> Auditing 10,000 Lean theorem-proving benchmark problems reveals 398 mechanically certified defects that both inflate and deflate prover scores, invalidating benchmarks as self-verifying.

- **Source:** [arXiv](https://arxiv.org/abs/2606.29493)
- **Published:** 2026-08-17
- **Permalink:** https://picx.dev/p/jG3uEe
- **Whiteboard:** https://picx.dev/p/jG3uEe/image

## Summary

## Summary (Overview)

- This paper presents the first large-scale audit of five widely used Lean theorem-proving benchmarks (miniF2F, ProofNet, FormalMath, CombiBench, ProverBench) and their 13 variants (~10,000 problems), surfacing **4,833 findings** including **398 mechanically certified issues** (counterexamples, vacuous theorems, unsound axioms).
- The authors argue that Lean benchmarks are **not self-verifying**: the kernel only certifies that a proof establishes a formal statement, not that the statement faithfully encodes the intended informal problem or that evaluation harnesses are robust to trivial/adversarial solutions.
- They propose a **fault taxonomy** with three categories—Fidelity Issues (formalization-time), Evaluation Loopholes (harness robustness), and Maintenance Issues (version drift and source defects)—each requiring different remediation.
- They develop **automated static checkers** as Lean 4 metaprograms (counterexample finding, vacuity detection, axiom auditing, arithmetic hazard detection) plus **LLM-assisted semantic audit prompts**, demonstrating that defects can both **inflate and deflate** reported prover scores.
- They release **release standards** for trustworthy benchmark creation, including using `proof_wanted` instead of `sorry`, disabling auto-implicit, avoiding axioms, and pinning Lean/mathlib versions.

## Introduction and Theoretical Foundation

The paper addresses a critical gap in LLM-assisted theorem proving evaluation. Recent systems (DeepSeek-Prover V2, Goedel Prover 2, Kimina Prover) report progress on benchmarks like miniF2F and ProofNet, but benchmark scores can be misleading when problem statements are mis-specified or evaluation protocols contain loopholes.

**The core theoretical insight**: The Lean kernel provides certainty about a narrow claim—that a proof artifact establishes a given formal statement. This provides mathematical certainty about the *formal claim*, but overall benchmark reliability is limited by:

1. **Specification accuracy**: Does the formal statement match the intended informal problem?
2. **NL-to-Lean translation correctness**: Was the natural language problem faithfully encoded?
3. **Lean-specific semantic pitfalls**: Does the encoding avoid issues like Nat subtraction truncation?
4. **Evaluation protocol robustness**: Can the harness be exploited?

The paper walks through a five-step pipeline where errors can enter:

- **Step 1 (Informal Problem)**: Source errors, ambiguity, ill-posedness → *validity issues*
- **Step 2 (Formalization)**: Translation defects → *fidelity issues* (most defects arise here)
- **Step 3 (Model/Prover)**: Model attempts to produce a proof artifact
- **Step 4 (Lean Kernel)**: The trust boundary—certifies proof establishes formal statement
- **Step 5 (Reported Metric)**: Evaluation harness aggregates results → *robustness issues*

## Methodology

### Static Checkers (Lean 4 Metaprograms)

The authors implement static analyzers as Lean 4 metaprograms that combine syntactic pattern matching with semantic guard proving. When a potentially problematic pattern is detected, they attempt to discharge necessary guard conditions using tactics like `omega`, `assumption`, and `simp`. A finding is reported only when the guard cannot be automatically proven.

| Checker | Description |
|---|---|
| **Counterexample** | Finds concrete values that disprove the theorem |
| **Vacuous Theorem** | Detects unsatisfiable hypotheses (trivially true) |
| **Unsound Axiom** | Use of axiom or `sorry` in proofs |
| **Division by Zero** † | Division, modulo, or inverse without non-zero guard |
| **Nat Subtraction** † | Natural subtraction that may truncate to zero |
| **Analytic Domain** † | Functions like sqrt, log outside valid domain |
| **Unused Binder** | Quantified variable not used in formula body |

† indicates LLM-assisted false positive filtering support.

### LLM-Assisted Semantic Audit

For semantic mismatches that static analysis cannot decide, the authors evaluate LLM-based detection. For each benchmark problem, the LLM is presented with:
- The informal problem statement
- The formal Lean statement
- A description of one error category
- Few-shot examples

Six error categories are evaluated: problem statement errors, specification errors, formalization errors, domain mismatches, definition mismatches, and quantifier/indexing mismatches.

### Evaluation Setup

- **Corpus audit**: All 13 benchmark variants (~10,000 problems)
- **Semantic audit challenge set**: 92 problems across FormalMath (22), ProofNet (13), ProverBench (23), CombiBench (34), with each assessed across all six categories (552 total classifications)
- **Score impact study**: 20 problems with mechanically proven issues, manually corrected, evaluated with DeepSeek-Prover-V2-7B and Kimina-Prover-8B

## Empirical Validation / Results

### Corpus-Scale Static Audit Results

Running static checkers over all released variants surfaces **4,833 findings and 398 proven issues**:

| Benchmark | Variant | Prob. | Find. | Proven | Div/0 | Nat Sub | Int Div | Analytic | Axiom | CEx |
|---|---|---|---|---|---|---|---|---|---|---|
| FormalMath | all | 5,560 | 3,250 | 141 | 1,127 | 582 | 423 | 351 | 0 | 55 |
| FormalMath | lite | 425 | 213 | 6 | 80 | 34 | 25 | 33 | 0 | 1 |
| ProverBench | deepseek | 325 | 370 | 208 | 81 | 7 | 6 | 19 | 199 | 5 |
| ProofNet | original | 371 | 82 | 5 | 13 | 8 | 3 | 8 | 0 | 5 |
| ProofNet | sharp (#) | 371 | 67 | 1 | 11 | 6 | 4 | 8 | 0 | 1 |
| miniF2F | v2c | 488 | 193 | 8 | 45 | 28 | 20 | 31 | 0 | 3 |
| miniF2F | v2s | 488 | 181 | 8 | 45 | 29 | 15 | 28 | 0 | 3 |
| miniF2F | yangkyll | 488 | 135 | 6 | 34 | 24 | 12 | 16 | 0 | 0 |
| miniF2F | yangkyll-early | 488 | 79 | 13 | 14 | 19 | 15 | 9 | 0 | 5 |
| miniF2F | justincasher | 485 | 74 | 0 | 25 | 13 | 5 | 16 | 0 | 0 |
| miniF2F | harmonic | 485 | 74 | 0 | 25 | 13 | 5 | 16 | 0 | 0 |
| miniF2F | ai-mo | 244 | 37 | 1 | 17 | 6 | 3 | 5 | 0 | 0 |
| CombiBench | hf | 100 | 78 | 1 | 1 | 27 | 2 | 0 | 0 | 1 |
| **Total** | | **10,318** | **4,833** | **398** | **1,518** | **796** | **538** | **540** | **199** | **79** |

### LLM-Assisted False Positive Filtering

On a 55-example ProverBench warning verification set, LLM filtering reduces findings from 427 to 277 (35% reduction) while preserving all confirmed true positives:

| Model | Accuracy | Precision | Recall | Cost |
|---|---|---|---|---|
| Gemini 3.0 Flash | 83.3% | 0.89 | 0.86 | $0.09 |
| GPT-5.2 | 81.8% | 0.92 | 0.83 | $0.18 |
| Claude Sonnet 4.5 | 81.5% | 0.89 | 0.81 | $0.42 |
| DeepSeek-V3 | 68.5% | 0.68 | 1.00 | $0.12 |

### Semantic Audit Results

Both models achieve high recall but low precision overall:

| Model | Prec. | Rec. | F1 | Acc. | Cost |
|---|---|---|---|---|---|
| Sonnet 4.5 + Thinking | 0.30 | 0.82 | 0.42 | 68.1% | $13.71 |
| GPT-5.2 + Thinking | 0.24 | 0.91 | 0.37 | 54.6% | $6.86 |

Per-type F1 scores reveal that specification errors and definition mismatches are detected far more reliably than formalization errors:

| Error Type | Sonnet 4.5 | GPT-5.2 |
|---|---|---|
| Problem Statement Error | 0.29 | 0.10 |
| Specification Error | 0.51 | 0.48 |
| Formalization Error | 0.18 | 0.15 |
| Domain Mismatch | 0.33 | 0.27 |
| Definition Mismatch | 0.57 | 0.54 |
| Quantifier/Indexing | 0.39 | 0.33 |

### Effect on Reported Prover Scores

Defects affect reported scores in **opposing directions**:

**Score deflation** (unprovable statements): On 20 problems with mechanically proven issues, both models solved 0/20 on the original flawed statements. After correction: DeepSeek-Prover-V2-7B solved 3/20 and Kimina-Prover-8B solved 2/20.

**Score inflation** (weakened statements): Repairing weakened statements that distinguish ProofNet from its human-corrected counterpart ProofNet# lowers measured pass rates for tested provers.

These opposing effects can coexist within a single benchmark and partially cancel, leaving headline pass rates unreliable.

### Representative Fault Examples

**Missing hypothesis** (ProofNet – Axler Exercise 3.8): The formalization omits the requirement that V be finite-dimensional, essential for the theorem to hold.

**Incomplete translation** (miniF2F – IMO 1983 Problem 6): The Lean statement captures the inequality but omits the "determine when equality occurs" requirement.

**Vacuous hypotheses** (CombiBench): An earlier formalization encoded a minimality condition as $\forall N' < N, \neg \text{Periodic}(W, N')$, but Periodic W 0 is trivially provable with `simp`, making hypotheses unsatisfiable and allowing a trivial `exfalso` proof.

**NL statement defect** (ProverBench): A problem states the general solution to $x^2 + y^2 - 1 = 4xy$ is $x + u\sqrt{3} = (2 + \sqrt{3})^n$, whereas the correct Pell reduction gives $u + x\sqrt{3} = (2 + \sqrt{3})^n$, with variables swapped.

**The apply? frontend bug**: A bug in Lean versions prior to 4.20.0 allowed the `apply?` tactic to report success without producing a theorem declaration that passed ordinary kernel verification. This appeared in at least three proofs claimed by DeepSeek-Prover-V2.

## Theoretical and Practical Implications

### Trust Boundary Analysis

The paper's central theoretical contribution is clarifying **what Lean's kernel certifies and what it does not**. The trust boundary marks the limit of mathematical certainty: everything to the left (informal problem, formalization) and right (evaluation protocol, metric reporting) must be validated by other means. This reframes the common intuition that Lean benchmarks are "self-verifying."

### Taxonomy-Driven Remediation

The fault taxonomy makes remediation actionable by matching faults to appropriate interventions:

- **Fidelity issues** → require careful review at creation time; Lean encoding hazards detectable by static analysis
- **Evaluation loopholes** → require stricter harnesses and patched Lean versions
- **Maintenance decay** → requires version pinning and active stewardship

One cannot "fix" a kernel bug/bypass by adding dataset review, nor prevent missing hypotheses by restricting tactics.

### Release Standards

The authors propose concrete standards for trustworthy benchmark creation:

1. **Use `proof_wanted` instead of `sorry`** for problem statements—this declares the theorem signature without adding it to the environment as an axiom, closing the sorry-exploitation loophole and preventing `native decide` and other kernel-bypassing tactics.

2. **Turn off auto-implicit** (`set_option autoImplicit false`)—forces errors at formalization time instead of silently "fixing" mistyped variable names with implicit parameters.

3. **Basic checkers**—flag known Lean pitfalls: division by zero, Nat subtraction truncation, analytic domain issues.

4. **Avoid using axioms**—problem statements should be encoded as definitions of propositions, never as axioms, since any solver can "solve" an item by citing the axiom.

5. **Dataset maintenance and pinning**—clearly specify the Lean/mathlib version a dataset targets.

6. **Capture all requirements**—use LLM-as-judge as a triage tool to identify whether a formalization captures all requirements, not just the main claim.

## Conclusion

The paper demonstrates that Lean proof checking removes many sources of error but does not guarantee benchmark validity. Specification fidelity is a known challenge across formal methods and ML evaluation, yet systematic audits of Lean theorem-proving benchmarks have been lacking—a gap this work fills with a taxonomy, checkers, and case studies.

**Key findings**:
- Benchmark defects are common enough to matter (398 mechanically certified issues across ~10,000 problems)
- Defects can both inflate and deflate reported prover scores
- Static checkers + LLM-assisted filtering effectively surface statements worth human review
- The taxonomy transfers to other proof assistants, though specific checks would differ

**Future work**:
- Extending the audit to more benchmarks
- Generating better high-quality synthetic data
- Filtering existing Lean datasets
- Developing an effective theorem proving harness

**Software and data**: Static checkers (Lean 4 metaprograms), evaluation harness, semantic-audit prompts, and snapshot of audited benchmark variants are available at https://github.com/Shashi456/atp-checkers.

---

_Markdown view of https://picx.dev/p/jG3uEe, served by PicX — AI-generated visual whiteboard summaries of research papers._