MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlassis Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Mohamed, Bilal Aytekin, Jiewen Lang, Zezheng Song, Furong Huang
cs.CL, cs.AI, cs.LO
2026-08-26
MathAdv's 321 advanced problems: Goedel-Prover-V2 hits 21.88% on Lean. GPT-5.4 scores 82.88% on strategy MCQs, 10.62% on Lean, and often fails equivalent rewrites.
Most formal-math benchmarks publish one number: did the model close a Lean proof. A miss does not say whether the model lacked the fact, broke the argument, or simply could not write something the kernel accepts. Coverage is thin as well. MiniF2F and PutnamBench sit on contest algebra and number theory. Topology, Fourier analysis, and functional analysis barely show up. Each item is frozen in one wording, so a pass can be familiarity with the surface form.
MathAdv is a diagnostic set led by the University of Maryland, College Park, with Georgia Tech and Cornell. It has 321 undergraduate-to-graduate problems across 13 areas: number theory, linear algebra, abstract algebra, calculus, real analysis, complex analysis, Fourier analysis, functional analysis, probability, topology, geometry, combinatorics, and logic. 298 items have Lean 4 statements; 23 wait because Mathlib still lacks the definitions. Each item can carry up to three extra tests: 81 fill-in-the-blank (direct-answer) questions for informal solving, 293 multiple-choice items for which theorem or strategy to use, and 30 expert rewrites that keep the math and change the presentation.
Problems come from textbooks and domain experts. Contributors are PhD students in the relevant area; a second expert reviews every statement and its auxiliaries. One probability multiple-choice item asks whether optional stopping or a Doob decomposition is the right tool. A real-analysis original writes an explicit convex combination; the rewrite asks for the smallest convex set containing the same points. Recognizing they are the same problem is the point.
Formalization is a human-in-the-loop pipeline. An LLM drafts a Lean statement, compiler errors go back until the file type-checks, a second model plus one expert check semantic fidelity, and a second expert signs off. Models are not used as compile oracles. On James Hanson's Lean 4 junk theorems (snippets that type-check but read like nonsense), gpt-5.5 predicted compilation 58% of the time and two DeepSeek variants 4%, while deepseek-v4-pro scored 1.91/2 on meaning. Lean judges syntax. Models and people judge meaning.
Mathlib gaps are a hard stop. An appendix example from Petersen needs sectional curvature, geodesic balls, and the Bishop-Gromov inequality, none of which were in the library. A faithful encoding would mean building that library first, so those items were deferred.
The evaluation splits proof systems in two. Step-level search includes InternLM2-Math-Plus-7B, InternLM2.5-StepProver, DeepSeek-Prover-V1.5-RL + RMaxTS, MA-LoT on DeepSeek or Goedel, and Goedel-Prover-V2-32B. Whole-proof generators include Goedel-Prover-SFT/DPO and DeepSeek-Prover-V1.5 Base/SFT/RL. General models tested: GPT-5.4, DeepSeek-V3.2, DeepSeek-R1. Compute is not matched. DeepSeek-Prover-V1.5 variants use pass@128, Goedel-Prover-V2 uses pass@32 plus two self-correction rounds, GPT-5.4 uses pass@32, DeepSeek-R1 uses pass@16. Table 1 is not a fair FLOPs contest.
On Lean 4 proving, Goedel-Prover-V2 leads at 21.88%, then DeepSeek-Prover-V1.5 RL + RMaxTS at 16.56%. Specialized training and search help; the ceiling stays low. Along the DeepSeek-Prover-V1.5 line, Base is 1.25%, RL is 11.25%, and RMaxTS reaches 16.56%. GPT-5.4 scores 10.62%, DeepSeek-R1 10.94%, DeepSeek-V3.2 5.31%. In the appendix, Goedel-Prover-V2 hits 70.0% on number theory (7/10) and 65.0% on linear algebra (13/20), and 0% on topology. The paper says every model scores 0% on topology.
| Model | Lean proof | Fill-in DA | MC |
| Goedel-Prover-V2 | 21.88% | not reported | not reported |
| DeepSeek-Prover-V1.5 RL+RMaxTS | 16.56% | 42.0% | 38.70% |
| InternLM2-Math-Plus-7B | 13.12% | 39.5% | 64.04% |
| GPT-5.4 | 10.62% | 64.2% | 82.88% |
| DeepSeek-V3.2 | 5.31% | 66.7% | 75.00% |
| Goedel-Prover-SFT | 10.62% | 4.9% | 21.23% |
General models can solve and pick a strategy; they cannot write Lean. Goedel-Prover flips the pattern. SFT and DPO score 4.9% on fill-in but 10.62% and 11.25% on proofs. Their strength is tactic search, not natural-language answers.
The 30 rewrites are reported as counts. Goedel-Prover-V2 solves 6 originals it then misses after rewriting, and 0 the other way. DeepSeek-R1 is 4 to 0. Across families, original-only wins outnumber rewrite-only wins. The n is small. The direction is stable.
Feeding Lean errors back, same budget K=16×3, lifts DeepSeek-V3.2 from 5.00% to 7.50% and GPT-5.4 from 9.06% to 13.75%. Interaction clears many syntax misses; remaining errors are about building the argument. GPT-5.4 piles unused intermediate claims and replaces a rejected short proof with a long one. Natural-language hints taken from the multiple-choice key help the two general DeepSeek models and hurt Goedel-Prover-SFT/DPO. Figure 5 is not tabulated, so the paper gives the split without exact percentage points.
Failures cluster four ways: a half-finished argument treated as done, a legal tactic aimed at the wrong goal (linear arithmetic on a divisibility claim), invented Mathlib names, and a tactic loop that does not move the goal. Wins are a close library lemma, an explicit have-chain, or a definition that collapses once unfolded.
For people training provers, MathAdv splits a low score into parts. Most general models stall at formalization, not at "which theorem applies." Informal hints may help a general LLM and get in the way of a Lean-specialized searcher. Verifier feedback is worth the extra turns. It does not, by itself, produce tidy proofs.
For people who only watch contest leaderboards, domain skew and wording overfitting stay hidden. Topology at 0% and number theory / linear algebra at the top line up with contest pretraining and with Mathlib coverage. Thirty rewrites are too few for a headline ranking. They are already enough as a familiarity check.
This is a diagnostic benchmark, not a new proving algorithm. The increment is four tests on the same items: knowledge, informal solving, formal construction, and robustness to presentation.
The authors list two limits: the set is modest because expert work is expensive, and Mathlib coverage blocks 23 items.
Several more sit in the tables. Sampling budgets differ, so 21.88% for Goedel-Prover-V2 and 10.62% for GPT-5.4 are not a matched comparison. Appendix denominators disagree: some tables use 320 overall against 298 formalized statements in the main text, and topology is 28 in some tables and 8 in others. The rewrite study is 30 items and Table 3 is single-digit counts. Figure 5 never prints the hint deltas. The multiple-choice task asks which theorem is useful, not whether the model can prove it, so GPT-5.4's 82.88% is strategy retrieval. Source textbooks are public, so contamination is live; the rewrite set is the intended control, and 30 items cannot cover 321.