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.
Figures & tables
Figure 1: MathAdv at a glance.
Figure 2: Left: Distribution of the 321 problems across mathematical domains. Right: An original probability problem with its direct-answer and multiple-choice diagnostic tasks.
Figure 3: Human-in-the-loop autoformalization process for MathAdv.
Figure 4Table 5Figure 6
Appendix figures & tables20 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 6: Multiple-choice Reasoning Problems by Category (Total = 293).
Figure 7: Transformed Problems by Category (Total = 30).
Figure 8: Fill-in-the-blank Problems by Category (Total = 81).
Model
Compilation Accuracy (%)
Semantic Understanding (0–2)
gpt-5.5
58%
2.00
deepseek-v4-pro
4%
1.91
deepseek-chat
4%
1.51
gpt-4o
18%
0.89
Appendix
Table 5: Model performance on the Lean 4 Junk Theorems testbed.
Domain
N
DS Non-Int.
DS Int.
DS Δ
GPT Non-Int.
GPT Int.
GPT Δ
Abstract Algebra
30
10.0%
10.0%
+0.0%
16.7%
23.3%
+6.7%
Calculus
26
3.9%
3.9%
+0.0%
7.7%
7.7%
+0.0%
Combinatorial
23
4.3%
4.3%
+0.0%
8.7%
8.7%
+0.0%
Complex Analysis
15
0.0%
0.0%
+0.0%
0.0%
0.0%
+0.0%
Fourier Analysis
31
9.7%
9.7%
+0.0%
9.7%
12.9%
+3.2%
Functional Analysis
25
4.0%
4.0%
+0.0%
4.0%
4.0%
+0.0%
Appendix
Table 6: Lean 4 accuracy by domain with and without interaction.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
0.0
58.3
Calculus
0.0
48.1
Combinatorial
0.0
65.2
Complex Analysis
0.0
43.8
Fourier Analysis
3.2
54.8
Functional Analysis
0.0
48.0
Appendix
Table 7: Accuracy by domain for DeepSeek V1.5 Base.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
16.7
16.7
Calculus
0.0
37.0
Combinatorial
4.3
43.5
Complex Analysis
0.0
37.5
Fourier Analysis
9.7
29.0
Functional Analysis
4.0
32.0
Appendix
Table 8: Accuracy by domain for DeepSeek V1.5 SFT.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
16.7
41.7
Calculus
7.7
18.5
Combinatorial
4.3
52.2
Complex Analysis
0.0
25.0
Fourier Analysis
9.7
22.6
Functional Analysis
4.0
44.0
Appendix
Table 9: Accuracy by domain for DeepSeek V1.5 RL.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
20.0
41.7
Calculus
15.4
29.6
Combinatorial
4.3
30.4
Complex Analysis
0.0
37.5
Fourier Analysis
12.9
48.4
Functional Analysis
4.0
44.0
Appendix
Table 10: Accuracy by domain for RMaxTS.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
23.3
75.0
Calculus
19.2
70.4
Combinatorial
4.3
73.9
Complex Analysis
0.0
68.8
Fourier Analysis
9.7
54.8
Functional Analysis
4.0
60.0
Appendix
Table 11: Accuracy by domain for InternLM2-Math.
Domain
Solved
Total
Lean 4 Acc. (%)
Abstract Algebra
5
30
16.7
Calculus
4
26
15.4
Combinatorial
0
23
0.0
Complex Analysis
0
15
0.0
Fourier Analysis
3
31
9.7
Functional Analysis
1
25
4.0
Appendix
Table 12: Accuracy by domain for InternLM2.5 Step Prover.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
16.7
16.7
Calculus
11.5
22.2
Combinatorial
4.3
26.1
Complex Analysis
0.0
18.8
Fourier Analysis
9.7
12.9
Functional Analysis
4.0
28.0
Appendix
Table 13: Accuracy by domain for Goedel SFT.
Domain
Lean 4 Acc. (%)
MC Acc. (%)
Abstract Algebra
10.0
16.7
Calculus
15.4
22.2
Combinatorial
4.3
26.1
Complex Analysis
0.0
12.5
Fourier Analysis
9.7
16.1
Functional Analysis
8.0
28.0
Appendix
Table 14: Accuracy by domain for Goedel DPO.
Domain
Solved
Total
Lean 4 Acc. (%)
Abstract Algebra
7
30
23.3
Calculus
5
26
19.2
Combinatorial
2
23
8.7
Complex Analysis
1
15
6.7
Fourier Analysis
4
31
12.9
Functional Analysis
1
25
4.0
Appendix
Table 15: Goedel v2 union outcomes aggregated by domain.
Domain
Solved
Total
Lean 4 Acc. (%)
Abstract Algebra
4
30
13.3
Calculus
3
26
11.5
Combinatorial
1
23
4.3
Complex Analysis
3
15
20.0
Fourier Analysis
3
31
9.7
Functional Analysis
1
25
4.0
Appendix
Table 16: Accuracy by domain for MA-LoT + DeepSeek V1.5.