Summary (Overview)

• ProofGap is a new fine-grained benchmark for step-level formal reasoning, derived from 3,015 exercises in Demidovich's Problems in Mathematical Analysis, yielding 26,116 proof gaps.
• The benchmark decomposes natural-language solutions into individual local proof obligations ($\Gamma \vdash g$), enabling evaluation of local formal proof construction independent of end-to-end proof composition.
• A semantics-aware pipeline translates natural-language solutions into a formal intermediate representation (Relaxed NFL → Core NFL), from which proof-gap generators derive verification conditions.
• Experiments show step-level gaps are substantially more tractable than complete theorems (Pass@8: 31.99–35.39% vs. 2.92–4.28%), and general-purpose models outperform specialized provers on the balanced ProofGap-280 subset.
• The benchmark provides both an original DSL-based version with a lightweight checker and a Lean version with verified ground-truth proofs.

---

Introduction and Theoretical Foundation

The paper addresses a critical gap in formal mathematics evaluation: existing benchmarks (miniF2F, ProofNet, PutnamBench) evaluate models at the theorem level, providing only a coarse success/failure signal. This is insufficient for:

• Fine-grained diagnosis: Theorem-level failure cannot distinguish between errors in local inference, autoformalization mistakes, or failures in global proof planning.
• Process supervision: Prior work (Lightman et al., 2024) shows step-level feedback provides more effective training signals than outcome-only supervision.
• Localized verification: Applications like SAFE (Liu et al., 2025) formalize individual reasoning steps for Best-of-N trajectory selection, requiring trustworthy, localized formal feedback.

Key motivation: Mathematical analysis is particularly challenging because local inferences often depend on implicit conditions — domain restrictions, nonzero conditions, sign conditions, and convergence assumptions. MA-ProofBench (Pu et al., 2026) found models achieving near-zero formal proof success despite producing correct natural-language proofs, highlighting the need for finer-grained evaluation.

Theoretical foundation: A ProofGap instance is formally defined as a triple:

$$(\Gamma, g, m) \tag{1}$$

where $\Gamma$ is the well-scoped local context, $g$ is the target proposition, and $m$ is an optional strategy annotation. The task requires establishing:

$$\Gamma \vdash g \tag{2}$$

---

Methodology

Benchmark Construction Pipeline

The construction proceeds in three stages:

Stage 1: Relaxed NFL Translation

• A prompt-based translator converts each problem/solution into Relaxed Natural Formal Language (Relaxed NFL), a parser-readable intermediate representation preserving conditions, goals, proof structure, and method annotations.
• Output undergoes parser validation and representation-consistency screening (checking preservation of assumptions, goals, and proof steps).

Stage 2: Core NFL Elaboration

• Relaxed NFL AST is elaborated into Core NFL, a normalized representation with explicit proof contexts and variable bindings.
• Transformations decompose compound propositions, disambiguate notation, canonicalize operations, and make free variables explicit.
• Notation normalization includes: $f'$ → $\text{FunDeri}(f, 1, 1)$ (first-order derivative w.r.t. first formal argument).

Stage 3: Proof-Gap Generation

• The generator traverses the Core NFL AST, maintaining current proof state $\Gamma \vdash g$.
• Each intermediate proposition $P$ emits obligation $\Gamma \vdash P$ and adds $P$ to the context.
• Each gap is translated to Lean using GPT-5.6-sol, with human-in-the-loop cross-review auditing.

Lightweight Proof-Checking Framework

• An 18-command domain-specific language (DSL) with a deterministic checker.
• Features include autosolve for deterministic solving and a 514-entry theorem library.
• A verifier-guided agent workflow uses checker feedback to revise candidate programs.

---

Empirical Validation / Results

Full-Set Solvability (RQ1)

Table 3: Pass@8 (%) on all 26,116 gaps and 3,015 exercise theorems

• Even the strongest prover leaves 64.61% of local obligations unsolved.
• The strongest standard tactic (aesop) solves only 9.67% of gaps; the tactic union solves 11.20%.
• Topic-level patterns (Table 4): Best performance on functions/limits (39.10–44.41%), worst on parameter integrals (18.21–20.43%) — consistent ordering across all three provers.

Effect of Proof Granularity (RQ2)

• Per-gap Pass@8: 31.99–35.39% vs. complete-theorem Pass@8: 2.92–4.28%.
• Mean exercise-level gap coverage: 27.63–31.15% (Table 5).
• Parameter integrals: models solve 18.21–20.43% of gaps but ≤1.00% of complete theorems.

Cross-Model Comparison (RQ3)

Table 7: Pass@k on ProofGap-280 (gap / parent exercise)

• Every general-purpose model outperforms every specialized prover at gap level (GLM-5.2 at 65.00% exceeds best specialized at 39.64%).
• GPT-5.6-sol and Claude-Opus-4.8 tie at 87.86% on gaps but differ markedly on parent exercises (21.43% vs. 13.93%).

Diagnostic Resolution (RQ4)

Table 6: Local progress among theorem-failed exercises (%)

• Theorem-solved exercises have mean gap coverage of 75.07–79.12% vs. 26.08–29.19% for theorem-failed exercises.
• 72.39–78.03% of theorem-failed exercises contain at least one solved gap — refining binary failure into graded local progress.

---

Theoretical and Practical Implications

Theoretical significance:

• Establishes local formal proof completion as a distinct evaluation dimension, separable from end-to-end proof composition.
• Demonstrates that theorem-level failure masks substantial local reasoning capability — models can discharge individual inferences while failing to compose complete proofs.
• The benchmark's structure (with 8.66 gaps per exercise on average and 8.33 assumptions per gap) enables fine-grained analysis of which mathematical topics and reasoning patterns pose the greatest challenges.

Practical applications:

• Process supervision: ProofGap-style obligations can provide machine-checkable training signals for process reward models, extending work like FoVer (Kamoi et al., 2026).
• Proof verification systems: The pipeline may support future natural-language proof verification, provided semantic translation and sequential proof composition are handled reliably.
• Model diagnosis: The benchmark identifies parameter integrals as a particularly challenging topic (18.21–20.43% gap Pass@8), suggesting specific areas for improvement.

---

Conclusion

Main takeaways:

1. ProofGap provides a fine-grained, scalable benchmark for step-level formal reasoning with 26,116 gaps from 3,015 mathematical analysis exercises.
2. Step-level evaluation reveals substantial local reasoning capability hidden by theorem-level failure (31.99–35.39% vs. 2.92–4.28% Pass@8).
3. General-purpose models now outperform specialized provers on local obligations, though end-to-end proof composition remains challenging for all models.
4. The benchmark enables graded diagnosis of model failures, distinguishing between local inference errors and global proof-planning failures.

Limitations:

• Covers only one textbook (Demidovich) in mathematical analysis.
• Evaluation limited to Lean proof assistant.
• Does not directly measure natural-language autoformalization or invalid-step detection.

Future directions:

• Extend coverage across mathematical domains and proof assistants.
• Evaluate complete pipelines jointly addressing semantic translation, local proof discharge, and sequential proof composition.
• Use ProofGap-style obligations for training process reward models and improving end-to-end formal reasoning.