Pith. sign in

REVIEW 3 minor 1 cited by

Defects in five widely used Lean theorem-proving benchmarks can both inflate and deflate reported prover scores.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-30 06:54 UTC pith:2FUKPHJK

load-bearing objection The paper finds 398 mechanically certified defects across five Lean benchmarks and shows they distort prover scores on corrected subsets, with released checkers and snapshots.

arxiv 2606.29493 v1 pith:2FUKPHJK submitted 2026-06-28 cs.AI

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

Pawan Sasanka Ammanamanchi , Siddharth Bhat , Stella Biderman This is my paper
classification cs.AI
keywords Lean theorem provingbenchmark defectsformal verificationLLM-assisted provingevaluation failuresdataset qualitystatic checkersfault taxonomy
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper audits five popular Lean benchmarks for theorem proving and finds 4,833 findings from static checkers, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms. These defects exist because the Lean kernel verifies only that a proof matches its formal statement, not that the statement matches the intended informal problem or that evaluation harnesses resist trivial solutions. On corrected subsets of the datasets, prover performance scores change in both directions. The authors supply a fault taxonomy, automated checkers, and recall-oriented semantic audit prompts to support more reliable benchmark construction.

Core claim

Five widely used Lean theorem-proving benchmarks and their forks contain 4,833 findings surfaced by corpus-scale static checkers, of which 398 are mechanically certified issues including counterexamples, vacuous theorems, and unsound axioms, plus semantic defects such as missing hypotheses, problem simplification, incomplete translations, and Lean-specific hazards; these defects cause reported prover scores both to increase and to decrease when measured on corrected subsets, showing that evaluation harnesses are not robust to trivial or adversarial solutions.

What carries the argument

Corpus-scale static checkers that detect counterexamples, vacuous theorems, and unsound axioms, together with a proposed fault taxonomy for formal mathematics datasets.

Load-bearing premise

The five audited benchmarks and the static checkers together capture the main sources of evaluation failure without missing important semantic mismatches that only human review would detect.

What would settle it

If prover success rates on the corrected dataset snapshots remain statistically indistinguishable from rates on the original benchmarks, that would show the identified defects do not affect reported scores.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Corrected benchmark subsets produce different prover performance scores than the original versions.
  • Evaluation harnesses require design changes to resist trivial and adversarial solutions.
  • Future formal math datasets can use the released checkers and standards to reduce similar defects.
  • Semantic audit prompts can surface additional issues beyond those found by static analysis.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Analogous defects are likely present in theorem-proving benchmarks for formal systems other than Lean.
  • Human review will probably remain necessary to catch semantic mismatches the checkers do not surface.
  • Widespread use of the checkers could make cross-paper comparisons of prover performance more reliable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 3 minor

Summary. The paper audits five widely used Lean theorem-proving benchmarks and their forks using corpus-scale static checkers, surfacing 4,833 findings including 398 mechanically certified issues (counterexamples, vacuous theorems, unsound axioms). It documents additional semantic defects (missing hypotheses, incomplete translations, Lean-specific hazards) and shows via re-evaluation on corrected subsets that defects can both inflate and deflate reported prover scores. The authors propose a fault taxonomy, automated checkers, and recall-oriented semantic audit prompts, releasing all artifacts at the linked GitHub repository.

Significance. If the results hold, the work is significant for LLM-assisted theorem proving because it supplies mechanically verified evidence of benchmark defects together with explicit demonstrations of score impact on corrected data. The open release of checkers, audit prompts, and corrected dataset snapshots directly supports reproducibility and better dataset construction practices in the field.

minor comments (3)
  1. The abstract states 4,833 findings with 398 mechanically certified issues, but the main text would benefit from an explicit table or section breaking down the 398 issues by type and by benchmark to improve traceability.
  2. In the evaluation on corrected subsets, the demonstration of both inflation and deflation is clear, but adding statistical measures (e.g., confidence intervals on score deltas) would strengthen the quantitative claims without altering the central argument.
  3. The fault taxonomy is introduced as a contribution; a short comparison table relating it to prior informal-benchmark taxonomies would help readers situate the new categories.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation of minor revision. We will incorporate any minor improvements in the revised version.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper's central claims rest on corpus-scale application of independent static checkers and Lean kernel verification to five external benchmarks, mechanically certifying 398 defects (counterexamples, vacuous theorems, unsound axioms), documenting semantic issues, and re-running provers on corrected subsets to measure score inflation/deflation. No derivation step reduces by construction to a fitted parameter, self-definition, or self-citation chain; the argument is externally falsifiable via released artifacts and does not invoke uniqueness theorems or ansatzes from prior author work.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claims rest on the soundness of the Lean kernel for certifying defects and on the assumption that the chosen static checkers are sufficiently complete; no free parameters are fitted and no new physical or mathematical entities are postulated.

axioms (2)
  • standard math The Lean kernel correctly identifies counterexamples, vacuous theorems, and unsound axioms when they exist in the formal statements.
    Invoked when the paper treats 398 findings as mechanically certified.
  • domain assumption The five selected benchmarks are representative of current practice in Lean theorem-proving evaluation.
    The audit scope is limited to these benchmarks and their forks.
invented entities (1)
  • Fault taxonomy no independent evidence
    purpose: Categorize dataset construction and evaluation defects
    New classification introduced to organize the 4,833 findings.

pith-pipeline@v0.9.1-grok · 5751 in / 1345 out tokens · 25713 ms · 2026-06-30T06:54:23.070139+00:00 · methodology

0 comments
read the original abstract

Benchmarks for LLM-assisted theorem proving in Lean are often treated as intrinsically reliable because every solved instance comes with a machine-checked proof. However, the kernel only checks that a proof establishes a \emph{formal} statement; it does not verify that the statement faithfully encodes the intended informal problem, nor that evaluation harnesses are robust to trivial or adversarial solutions. We audit five widely used Lean theorem-proving benchmarks and their forks, using corpus-scale static checkers to surface 4,833 findings, including 398 mechanically certified issues such as counterexamples, vacuous theorems, and unsound axioms. We also document semantic defects such as missing hypotheses, problem simplification, incomplete or incorrect translations, and Lean-specific specification hazards. Beyond dataset construction, we survey evaluation-time failure modes and show, on corrected subsets, that defects can both inflate and deflate reported prover scores. We propose a fault taxonomy, a suite of automated checkers and recall-oriented semantic audit prompts, and release standards to guide the creation of formal math datasets and to make evaluation more reproducible and trustworthy. Our checkers, audit prompts, and corrected dataset snapshots are available at https://github.com/Shashi456/atp-checkers.

Figures

Figures reproduced from arXiv: 2606.29493 by Pawan Sasanka Ammanamanchi, Siddharth Bhat, Stella Biderman.

Figure 1
Figure 1. Figure 1: The formal benchmarking pipeline and where errors can enter. The kernel (trust boundary) certifies only that a proof artifact establishes the formal Lean statement. Three categories of issues arise: Fidelity Issues in the translation step, Evaluation Loopholes (robustness) in the proof-checking and reporting steps, and Maintenance Issues (validity + drift) spanning the entire pipeline [PITH_FULL_IMAGE:fig… view at source ↗
Figure 2
Figure 2. Figure 2: Missing hypothesis: the Lean statement omits finite￾dimensionality, which is required for the theorem to hold. Incomplete translation. (Formalization) Problems often have several parts, and a formalization can silently drop one. In [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Incomplete specification: the equality-case determination is missing from the formalization. Wrong domain or type. (Domain & Definition mismatch) Translating variable domains inaccurately changes problem semantics. If a problem states “for all positive integers n,” using (n : N) without a guard (hn : 0 < n) includes n = 0. Conversely, using N when Z is intended can intro￾duce truncation errors. 3 [PITH_FU… view at source ↗
Figure 5
Figure 5. Figure 5: Incorrect source statement: the correct Pell reduction gives u + x √ 3 = (2 + √ 3)n . tion, since filters unify the disparate conditions needed to define two-sided limits, one-sided limits, and limits to ±∞. Another example is that of a semilinear map (Dupuis et al., 2024), which is a generalization of linear maps, created to unify linear algebra over R and C, where C has an extra complex-conjugate structu… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

    cs.AI 2026-07 conditional novelty 6.0

    Typed local edits on Lean proof blueprints match free-form repair coverage on localized defects while using far fewer tokens and lower cost.

Reference graph

Works this paper leans on

21 extracted references · 1 canonical work pages · cited by 1 Pith paper

  1. [1]

    CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

    URL https://openreview.net/forum? id=s9t2FJVsBH. de Moura, L. M., Kong, S., Avigad, J., van Doorn, F., and von Raumer, J. The lean theorem prover (system description). InCADE, 2015. URL https://api. semanticscholar.org/CorpusID:232990. Dupuis, F., Lewis, R. Y ., and Macbeth, H. Formalized functional analysis with semilinear maps.Journal of Automated Reaso...

    work page Pith review arXiv 2015

  2. [2]

    11 Faults in Our Formal Benchmarking A

    URL https://openreview.net/forum? id=9ZPegFuFTFv. 11 Faults in Our Formal Benchmarking A. Dataset Details Our goal is to demonstrate that defects are systematic, not anecdotal, and to identify checks that catch them early. A.1. Popular Formal Math Datasets We focus on widely used Lean datasets that collectively represent the standard evaluation suite for ...

    2022

  3. [3]

    ProofNet(Azerbayev et al., 2023): 371 undergraduate-level problems from textbooks (analysis, algebra, topology), released in Lean 3 with paired natural-language statements and proofs

    2023

  4. [4]

    They also release FormalMath Lite, a carefully selected subset of 425 problems (comprising 359 high school-level and 66 undergraduate- level problems)

    FormalMath(Yu et al., 2025): 5,560 Lean 4 problems spanning from Olympiad challenges to undergraduate-level theorems across algebra, applied mathematics, calculus, number theory, and discrete mathematics. They also release FormalMath Lite, a carefully selected subset of 425 problems (comprising 359 high school-level and 66 undergraduate- level problems)

    2025

  5. [5]

    CombiBench(Liu et al., 2025a): A benchmark comprising 100 combinatorial problems, each formalized in Lean 4 and paired with its corresponding informal statement

  6. [6]

    complete

    ProverBench(Ren et al., 2025): A benchmark dataset comprising 325 problems. 15 are formalized from AIME 24 and 25. The remaining 310 problems are drawn from curated textbook examples and educational tutorials. A.2. Provenance of Audited Variants Because ports, forks, and corrected re-releases of these benchmarks proliferate (Section 3), and because papers...

    2025

  7. [7]

    Parse Lean source and elaborate toExpr

  8. [8]

    Traverse subexpressions, matching patterns for each checker category

  9. [9]

    For guard-based checkers, construct the guard as a goal and run tactic proof 24 Faults in Our Formal Benchmarking

  10. [10]

    This discharges approximately 60% of valid guards automatically

    Collect findings where pattern matches but guard proof fails Guard proving uses a tactic sequence: omega (linear arithmetic over Z and N), assumption (direct hypothesis match), simp [ *](simplification with local lemmas). This discharges approximately 60% of valid guards automatically. G. LLM Verification Details G.1. Motivation Static guard proving fails...

  11. [11]

    System instruction defining the classification task

  12. [12]

    Error category definition and detection criteria from our taxonomy

  13. [13]

    Three few-shot examples (both positive and negative cases)

  14. [14]

    The problem to evaluate (NL statement + Lean formalization)

  15. [15]

    Output format specification (structured JSON with classification and explanation) Few-shot examples were drawn from problems not in the evaluation set and manually verified for correctness. H.4.1. SHAREDPREAMBLE(SYSTEMPROMPT) All six category prompts share a common preamble: Shared Preamble (System Prompt) Role:You are an expert auditor for NL→Lean 4 form...

  16. [16]

    Output MUST be valid JSON (no markdown, no extra keys)

  17. [17]

    Say NO if the formalization is correct for this category, even if other categories might have issues

  18. [18]

    Say NO if there is no semantic error at all

  19. [19]

    Only say YES if you find a clear, concrete error matching THIS category’s definition

  20. [20]

    YES". 6.DetailTagsmust be chosen ONLY from the allowed list. Output format (JSON): Verdict:

    If not confident, setNeedsReview = "YES". 6.DetailTagsmust be chosen ONLY from the allowed list. Output format (JSON): Verdict: "YES" or "NO" Explanation : 1–3 sentences DetailTags: array of strings NeedsReview:"YES"or"NO" H.4.2. CATEGORYPROMPTS Each category prompt appends a definition, boundary rules, allowed detail tags, and three few-shot examples (on...

  21. [21]

    prime p dividing its order

    :∃(p : Nat) (P : Sylow p G), P.Normal := sorry Verdict:YES. NL requires “prime p dividing its order” but Lean only has ∃p without p.Prime or p|card G . Trivialp= 1satisfies the Lean statement. Tag:incomplete spec. Example 2(Verdict: NO — error isdefinition mismatch) NL:What is the smallest integernsuch that1/2< n/9? Answer: 5. Lean:theorem omni theorem 29...