Introduces MathAdv, a Lean 4 diagnostic benchmark of 298 formalized problems across 13 math domains, evaluating theorem provers and auxiliary reasoning tasks.
Abstract
Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.
Problem
Existing formal mathematics benchmarks emphasize aggregate proof accuracy, cover a narrow range of domains, and rarely test robustness to equivalent reformulations, making it hard to localize model failures.
Approach
MathAdv comprises 321 undergraduate- and graduate-level problems across 13 domains, with 298 formalized in Lean 4 via a human-in-the-loop pipeline. Alongside Lean 4 proving, it adds three auxiliary tasks: multiple-choice knowledge probes, fill-in-the-blank informal reasoning, and expert-crafted equivalent transformations. Proof-step and whole-proof provers plus general-purpose LLMs are evaluated component-wise. Interactive feedback and natural-language hints are also assessed.
Figure 3: Human-in-the-loop autoformalization process for MathAdv.
Results
Formalization is a major bottleneck with low overall Lean 4 accuracy (best around 21.9%); performance varies substantially across domains; natural-language hints help general LLMs but can hurt proof-specialized models; equivalent reformulations expose robustness limitations.
Figure 5: Performance on Lean 4 formal proving with and without hints from MC questions.
