Technical Summary: MathAdv

Problem Statement

Formal theorem proving offers a rigorous, machine-verifiable framework for evaluating mathematical reasoning, yet existing benchmarks suffer from three critical limitations that obscure a nuanced understanding of model capabilities:

1. Limited Diagnostic Resolution: Current benchmarks typically report only aggregate proof accuracy. This fails to distinguish whether a failure stems from a lack of mathematical background knowledge, an error in informal reasoning, or an inability to translate a valid argument into a formal proof.
2. Narrow Domain Coverage: Existing datasets largely focus on competition-level problems from high school and undergraduate mathematics, with a heavy emphasis on algebra and number theory. Advanced domains such as topology, Fourier analysis, and functional analysis remain underrepresented.
3. Lack of Robustness Evaluation: Evaluations generally rely on a single, fixed problem formulation. This ignores the sensitivity of language models to minor changes in problem presentation, making it difficult to determine if success reflects robust reasoning or reliance on memorized patterns and superficial cues.

Methodology

The authors introduce MathAdv, a diagnostic benchmark designed to address these limitations through a component-wise evaluation framework.

Dataset Construction

• Scope: MathAdv comprises 321 problems spanning 13 mathematical domains, ranging from undergraduate to graduate levels (e.g., Abstract Algebra, Calculus, Topology, Functional Analysis, Logic).
• Formalization: 298 problems were formalized in Lean 4. The remaining 23 were retained for auxiliary tasks but deferred for formalization due to gaps in the Mathlib library (e.g., lack of definitions for Riemannian geometry concepts like the Bishop–Gromov inequality).
• Human-in-the-Loop Pipeline: To ensure semantic fidelity and compilability, the authors employed an LLM-assisted pipeline with human expert review. This process included:
  1. Initial Autoformalization: An LLM drafts the Lean 4 statement.
  2. Syntax Correction: The Lean compiler provides feedback for iterative correction until the code type-checks.
  3. Dual Semantic Verification: An independent LLM and a domain expert verify that the formal statement matches the original mathematical intent.
  4. Final Expert Review: A second expert conducts a final validation.

Diagnostic Task Design

For each problem, MathAdv constructs up to three auxiliary tasks to isolate specific capabilities:

1. Formal Proof (Core): The standard task of constructing a machine-verifiable Lean 4 proof.
2. Knowledge (Multiple Choice): Questions asking the model to identify the relevant theorem, concept, or strategy from plausible options. This probes background knowledge without requiring proof construction.
3. Informal Reasoning (Fill-in-the-Blank): Direct-answer problems requiring the model to compute a target quantity or expression in natural language, isolating mathematical reasoning from formalization constraints.
4. Robustness (Expert-Crafted Variants): Domain experts manually reformulate problems to preserve the underlying mathematics while substantially altering the presentation (e.g., changing wording or structure). This tests whether models rely on specific formulations or possess generalizable reasoning.

Key Contributions

1. A Broad, Expert-Reviewed Benchmark: MathAdv is a comprehensive benchmark that spans 13 advanced mathematical domains with a mix of formal and auxiliary tasks, including underrepresented areas like topology and functional analysis.
2. A Component-Wise Diagnostic Framework: By decoupling formal proof construction from knowledge retrieval and informal reasoning, the framework allows researchers to pinpoint specific failure modes (e.g., knowledge gaps vs. formalization bottlenecks).
3. Systematic Characterization of Theorem Provers: The authors provide a comprehensive evaluation of contemporary models, revealing disparities in performance across domains and the varying effects of natural-language guidance.

Results

The evaluation of various theorem provers (including DeepSeek-Prover, Goedel-Prover, InternLM, and general-purpose LLMs like GPT-5.4 and DeepSeek-R1) yielded four primary findings:

1. Formalization is a Major Bottleneck: Models often identify promising proof directions and solve the underlying mathematics (high accuracy on Fill-in-the-Blank and Multiple Choice tasks) but fail to translate these insights into valid Lean 4 proofs. For instance, DeepSeek-Prover-V1.5 RL achieved 11.25% accuracy on formal proofs but 37.0% on direct-answer problems.
2. Domain-Specific Performance Variance: Performance varies significantly across mathematical domains. Models trained heavily on competition math (e.g., Goedel-Prover-V2) excel in Number Theory and Linear Algebra but achieve 0% accuracy in Topology. This suggests training data bias and the difficulty of formalizing advanced concepts in current libraries.
3. Context-Dependent Utility of Natural Language Hints: Providing natural-language reasoning hints (derived from the Multiple Choice answers) improved performance for general-purpose LLMs (DeepSeek-V3.2, DeepSeek-R1) but degraded performance for proof-specialized models (Goedel-Prover variants). This indicates that specialized models may rely on learned formal patterns that are disrupted by informal guidance.
4. Fragility to Reformulation: Models exhibit a "robustness gap." Most models solved the original problem significantly more often than the expert-crafted transformed variants (e.g., Goedel-Prover-V2 solved 6 original problems but 0 transformed ones). This suggests a reliance on surface-level patterns and specific problem formulations rather than robust mathematical understanding.

Significance

The paper argues that aggregate theorem-proving accuracy is insufficient for diagnosing the capabilities of modern AI systems. By introducing MathAdv, the authors demonstrate that component-wise evaluation reveals distinct failure modes:

• Knowledge Gaps: Models may lack the specific theorems required for a domain.
• Reasoning Errors: Models may fail to solve the problem even in natural language.
• Formalization Difficulties: Models may understand the math but cannot express it in the strict syntax of a proof assistant.
• Presentation Sensitivity: Models may fail when the problem is rephrased, indicating a lack of true generalization.

The authors conclude that future progress in formal theorem proving requires not only better mathematical reasoning but also improved interaction with proof assistants, better coverage of advanced mathematical libraries (Mathlib), and training strategies that prioritize robustness to problem reformulation over memorization of specific formulations. The dataset and evaluation scripts are publicly available to facilitate further research in this direction.