Summary (Overview)

• MathAdv is a new diagnostic benchmark for formal mathematical reasoning in Lean 4, spanning 321 problems across 13 undergraduate- and graduate-level domains, including underrepresented areas like topology, Fourier analysis, and functional analysis.
• The benchmark provides up to three auxiliary tasks beyond theorem proving: multiple-choice questions (probing mathematical knowledge), direct-answer/fill-in-the-blank problems (isolating informal reasoning), and expert-crafted transformed variants (testing robustness to problem reformulation).
• Four key findings emerge from evaluating contemporary theorem provers: (1) formalization remains a major bottleneck, (2) performance varies substantially across domains, (3) natural-language hints help general-purpose LLMs but hurt proof-specialized models, and (4) models are brittle to mathematically equivalent reformulations.
• Goedel-Prover-V2 achieves the best Lean 4 performance at 21.88%, followed by DeepSeek-Prover-V1.5 RL + RMaxTS at 16.56%, while general-purpose models like GPT-5.4 reach only 10.62%.
• The dataset and evaluation scripts are publicly available at https://github.com/margotyjx/MathAdv.git.

---

Introduction and Theoretical Foundation

Background and Motivation

Mathematical reasoning is a fundamental benchmark for AI because it requires abstract understanding, logical deduction, and multi-step reasoning beyond memorization. Formal theorem proving offers a rigorous alternative to informal natural-language evaluation: models construct machine-verifiable proofs in proof assistants such as Lean, Coq, and Isabelle, enabling automatic verification.

Three Critical Limitations of Existing Benchmarks

1. Limited diagnostic resolution: Benchmarks report only aggregate proof accuracy, making it impossible to distinguish failures from knowledge gaps, reasoning errors, or formalization difficulties.

2. Narrow domain coverage: Existing benchmarks focus on competition-level problems (high-school and undergraduate), with an emphasis on algebra and number theory. Advanced areas like topology, Fourier analysis, and functional analysis are poorly represented.

3. Limited robustness evidence: Models are evaluated on a single, fixed formulation of each problem, even though language-model reasoning is sensitive to minor changes in problem formulation. This also raises concerns about data contamination and memorization.

Theoretical Foundation

Formal mathematics encodes statements and proofs within a logical system implemented by a proof assistant. Mathematical objects must be built from concepts recognized by the system, and every derivation must follow its logical rules. This requires models to translate mathematical ideas into precise definitions, statements, and logically valid proof steps.

---

Methodology

Benchmark Design

MathAdv contains 321 problems across 13 domains: number theory, linear algebra, abstract algebra, calculus, real analysis, complex analysis, Fourier analysis, functional analysis, probability, topology, geometry, combinatorics, and logic. 298 problems are formalized in Lean 4; the remaining 23 are deferred due to gaps in Mathlib coverage.

Auxiliary Task Types

Direct-answer problems: Recast proof problems as questions asking models to compute a target quantity without writing a Lean proof, separating informal problem solving from formal proof construction.

Multiple-choice problems: Ask models to identify the theorem, concept, or reasoning strategy most relevant to the original problem from several plausible options. Constructed for 293 problems.

Transformed problems: Expert-crafted reformulations that preserve underlying mathematical reasoning while substantially altering problem presentation. Constructed for 30 problems.

Example Transformation (Real Analysis)

Original: Let $S = \{(0, 0), (2, 0), (0, 1)\}$. Prove that

$$\{\lambda_1(0,0)+\lambda_2(2,0)+\lambda_3(0,1):\lambda_1,\lambda_2,\lambda_3\geq0,\lambda_1+\lambda_2+\lambda_3=1\}=\{(x,y)\in\mathbb{R}^2:x\geq0,y\geq0,\frac{x}{2}+y\leq1\}$$

Transformed: Let $S = \{(0, 0), (2, 0), (0, 1)\}$. Prove that the smallest convex set containing $S$ is

$$\{(x,y)\in\mathbb{R}^2:x\geq0,y\geq0,x/2+y\leq1\}$$

Human-in-the-Loop Autoformalization Pipeline

The pipeline comprises four stages:

1. Initial Autoformalization: An LLM generates a Lean 4 statement.
2. Syntax Correction: Compiler errors are returned to the model for iterative correction until the statement type-checks.
3. Dual Semantic Verification: An independent LLM and a human expert check semantic fidelity.
4. Final Expert Review: A second expert performs final review.

This design is motivated by the observation that LLMs can explain mathematical meaning and identify semantic issues but are unreliable at predicting whether code will be accepted by the Lean type checker. The Lean compiler provides direct feedback, while LLMs help interpret and revise at the semantic level.

Evaluated Models

• Proof-step generation models: InternLM2-Math-Plus-7B, InternLM2-Step-Prover, DeepSeek-Prover-V1.5-RL + RMaxTS, DeepSeek-Prover + MA-LoT, Goedel-Prover + MA-LoT, Goedel-Prover-V2-32B
• Whole-proof generation models: Goedel-Prover-SFT, Goedel-Prover-DPO, DeepSeek-Prover-V1.5 variants
• General-purpose LLMs: GPT-5.4, DeepSeek-V3.2, DeepSeek-R1

---

Empirical Validation / Results

Formal Theorem-Proving Performance

Table 1: Performance comparison of theorem prover LLMs on MathAdv in Lean 4.

Key observations:

• Verifier-guided search (Goedel-Prover-V2, DeepSeek-Prover-V1.5 RL + RMaxTS) significantly outperforms one-shot generation.
• General-purpose LLMs achieve only modest accuracy despite larger scale.
• All models score 0% on topology, while performance is best in number theory and linear algebra.

Direct-Answer and Multiple-Choice Performance

Table 2: Overall accuracy on direct-answer and multiple-choice reasoning questions.

Most models achieve higher accuracy on DA and MC tasks than on Lean 4 theorem proving, indicating that formal proof construction is a distinct bottleneck. Goedel-Prover is the exception, performing better on Lean proofs than on natural-language tasks.

Robustness to Transformations

Table 3: Original vs. transformed comparison on theorem proving questions in Lean.

For most models, solving the original but failing the transformed version (O✓/T×) is more common than the reverse, revealing significant brittleness to equivalent reformulations.

Interactive Feedback Experiment

Table 4: Overall Lean 4 accuracy with and without interaction (budget $K = 16 \times 3$).

Interactive feedback improves both models, confirming the value of direct compiler feedback.

Natural-Language Hints

Hints improve DeepSeek-V3.2 and DeepSeek-R1 but substantially reduce performance of Goedel-Prover-SFT and Goedel-Prover-DPO, showing a clear split between general-purpose and proof-specialized models.

---

Theoretical and Practical Implications

Failure Patterns Identified

1. Incomplete proofs: Reasonable approach but proves only a weaker statement or skips required cases.
2. Inappropriate tactics: Valid Lean code that cannot establish the current claim (e.g., linear arithmetic for divisibility proofs).
3. Hallucinated library names: Models invent results that sound plausible but do not exist in Mathlib.
4. Non-progressing repetition: Proofs repeat the same rewriting without advancing toward the goal.

Successful Proof Patterns

1. Library retrieval: Finding an existing Mathlib result that closely matches the statement.
2. Step-by-step translation: Introducing intermediate claims, separating cases, and providing required objects.
3. Definition unfolding: Problems that appear difficult become simple after formal definitions are expanded.

Implications

• Formalization is a distinct capability: Models can solve problems in natural language yet fail to produce valid Lean proofs, suggesting the need for specialized training on formal proof construction.
• Domain imbalance matters: Training corpora concentrated in competition mathematics leave advanced domains (topology, functional analysis) underserved, both in model training and library infrastructure.
• Model-dependent prompting: Natural-language hints should be tailored to model type—helpful for general-purpose LLMs, harmful for proof-specialized systems.
• Robustness requires explicit attention: Training should reward consistency across equivalent formulations rather than reliance on surface cues.

---

Conclusion

MathAdv provides a comprehensive diagnostic framework for formal mathematical reasoning that moves beyond aggregate theorem-proving accuracy. By decomposing theorem proving into component capabilities—mathematical knowledge, informal reasoning, formal proof construction, and robustness to reformulation—it reveals that current models are limited not only by mathematical knowledge, but also by formal proof construction, uneven domain coverage, and sensitivity to equivalent problem formulations.

Future directions include:

1. Expanding the benchmark size as expert effort permits.
2. Formalizing the 23 deferred problems as Mathlib coverage grows (e.g., Riemannian geometry requiring Bishop–Gromov inequality).
3. Developing training strategies that reward consistency across equivalent formulations.
4. Designing model-specific prompting strategies that account for specialization.

Limitations: MathAdv remains modest in size due to the substantial expert effort required for high-quality problem creation and validation, and it is constrained by the current coverage of Mathlib for advanced mathematical concepts.