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.

† 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:

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:

Semantic Audit Results

Both models achieve high recall but low precision overall:

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

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.