PaperlayerView exact revision on arXiv

Source-linked AI summary

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlasios Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Abdullahi Mohamed, Bilal Hamdi Aytekin, Jiewen Lang, Zezheng Song, Furong Huang

arXiv:2608.25449v1cs.CLcs.AIcs.LO

TL;DR

Existing formal mathematics benchmarks offer limited diagnostic resolution, narrow domain coverage, and limited testing of robustness to equivalent reformulations. MathAdv addresses these gaps with a 13-domain Lean 4 benchmark and auxiliary tasks, finding bottlenecks in formalization, uneven domain performance, guidance-dependent behavior, and brittleness to reformulation.

  • Problem

    Existing benchmarks often emphasize aggregate proof accuracy, cover a narrow range of mathematics, and provide limited evidence about robustness to equivalent reformulations.

  • Method

    MathAdv combines Lean 4 theorem proving with multiple-choice, fill-in-the-blank, and expert-crafted transformed tasks across 321 problems in 13 domains.

  • Results

    Evaluation finds formalization remains a major bottleneck, performance varies across domains, natural-language guidance affects model families differently, and equivalent reformulations expose substantial robustness limitations.

  • Takeaways & Limitations

    Component-wise evaluation reveals model capabilities and failure modes that aggregate theorem-proving accuracy obscures.

  • Takeaways & Limitations

    MathAdv remains modest in size and is constrained by current Mathlib coverage, leaving some advanced problems unformalized in Lean 4.

Abstract

from arXiv · show

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.

1 Introduction

MathAdv addresses limited diagnostic resolution, narrow mathematical coverage, and weak robustness testing in formal mathematics benchmarks. It combines component-wise tasks, broad domain coverage, and reformulated problems to characterize theorem-prover capabilities and failures.

  • Existing benchmarks often report aggregate proof accuracy, making knowledge, reasoning, and formalization failures difficult to distinguish.Successful theorem proving requires mathematical knowledge, logical deduction, and formal proof construction.
  • MathAdv contains 321 problems across 13 undergraduate- and graduate-level domains, including topology, Fourier analysis, and functional analysis.298 problems have formalized Lean 4 statements; 23 are deferred because required Mathlib support is unavailable.
  • Its original theorem-proving, multiple-choice, and fill-in-the-blank tasks help separate formal proof construction from mathematical knowledge and informal reasoning.The benchmark also includes transformed variants for robustness evaluation.
  • Expert-crafted reformulations preserve mathematical content while changing presentation, directly testing robustness beyond familiar wording or patterns.This design targets a limitation of benchmarks that provide limited evidence under equivalent reformulations.
  • Formalization remains a major bottleneck, with models often identifying promising proof directions but failing to produce valid Lean proofs.Performance also varies substantially across domains, and natural-language guidance affects general-purpose and proof-specialized models differently.
  • Most models solve original problems substantially more often than expert-crafted transformations, exposing brittleness to mathematically equivalent reformulations.The reported pattern suggests reliance on presentation-specific patterns rather than robust mathematical understanding.

2 Related work

Formal mathematics evaluates reasoning through machine-verifiable statements and proofs, while prior benchmarks span several settings but often provide narrower coverage and limited diagnostic depth. MathAdv extends this landscape with broader undergraduate- and graduate-level coverage and auxiliary tasks beyond theorem-proving accuracy.

  • Formal mathematics encodes statements and proofs in systems such as Lean, where logical steps can be checked and conclusions certified from assumptions.Models must translate mathematical ideas into precise definitions, statements, and valid proof steps.
  • Existing benchmarks cover competition mathematics, informal-to-formal translation, theorem collections, symbolic reasoning, and diagram-based geometry.The cited benchmark landscape spans multiple formal reasoning settings.
  • MathAdv spans 13 undergraduate- and graduate-level domains and includes fill-in-the-blank, multiple-choice, and transformed questions.These additions enable analysis beyond theorem-proving accuracy alone.

3 MathAdv: Advanced benchmarking of formal mathematical reasoning

MathAdv is a broad, component-wise benchmark that pairs Lean formalization with auxiliary tasks probing natural-language solving, theorem knowledge, and robustness to reformulation. Its problems cover 13 domains and use expert-selected transformations to preserve reasoning while changing presentation.

  • 3.1 MathAdv: MathAdv contains 321 textbook- or expert-contributed problems spanning 13 undergraduate- and graduate-level mathematical domains.The domains include number theory, algebra, analysis, probability, topology, geometry, combinatorics, and logic.
  • 3.1 MathAdv: 298 problems are formalized in Lean 4, while 23 remain auxiliary-only because current Mathlib gaps prevent immediate formalization.The deferred problems are retained for future formalization.
  • 3.1 MathAdv: Each suitable problem can receive up to three auxiliary tasks: fill-in-the-blank, multiple-choice reasoning, and an expert-crafted transformed problem.These tasks complement the original formal proof problem.
  • 3.1 MathAdv: Direct-answer questions ask models to compute a target quantity or expression without writing a Lean proof.They help separate informal problem solving from formal proof construction.
  • 3.1 MathAdv: Multiple-choice questions test whether models know the theorem, concept, or proof strategy most relevant to the original problem.They were constructed for 293 problems, excluding primarily computational or basic-fact cases.
  • 3.1 MathAdv: Transformed problems substantially change presentation while preserving the underlying mathematical reasoning.Comparing original and transformed performance tests consistency rather than reliance on familiar wording or memorized patterns.
  • 3.1 MathAdv: Expert-crafted transformed versions were constructed for 30 problems across the benchmark’s domains.The transformations are designed to appear distinct while relying on the same mathematical ideas.

D E F

The benchmark combines diagnostic question formats with an expert-reviewed, verifier-in-the-loop formalization process. Its scope is constrained by Mathlib coverage, while evaluation separates semantic understanding from reliable compilation judgments.

  • The benchmark’s domain distribution includes probability, real analysis, calculus, combinatorics, complex analysis, Fourier analysis, functional analysis, geometry, linear algebra, logic, and number theory.Figure 2 presents the distribution across the 321 problems.
  • The probability example pairs an original random-walk stopping-time problem with a direct-answer task and a multiple-choice reasoning question.The multiple-choice format asks which result or concept is most useful for solving the problem.
  • The diagnostic framework uses direct-answer, multiple-choice, and transformed questions alongside formal proof construction.These tasks test natural-language solving, theorem knowledge, proof strategies, and robustness to equivalent reformulations.
  • The formalization workflow has four stages: initial autoformalization, syntax correction, dual semantic verification, and final expert review.Compiler feedback guides iterative correction before independent LLM and expert semantic checks.
  • General-purpose LLMs can explain formal meaning yet incorrectly predict compilation, motivating verifier feedback in the pipeline.The paper distinguishes semantic interpretation from judging whether Lean accepts the code.
  • Lean provides direct compiler feedback, while LLMs interpret and revise formalizations at the semantic level.The pipeline avoids relying on LLMs alone as syntax or type-checking judges.
  • Mathlib lacks prerequisite definitions and lemmas for some advanced areas, including examples from Riemannian geometry involving the Bishop–Gromov inequality.Problems requiring prohibitive library development are deferred to future benchmark iterations.

4 Diagnostic evaluation of theorem provers

MathAdv evaluates theorem provers across formal proof construction, natural-language reasoning, mathematical knowledge, domains, and equivalent reformulations. The results show limited Lean success, uneven domain performance, a gap between answering and formalizing, and substantial sensitivity to presentation.

  • Evaluation setup: The evaluation covers proof-step and whole-proof generation models, alongside general-purpose LLMs, using Lean 4, direct-answer, multiple-choice, and reformulation tasks.These protocols separate formal proof construction from natural-language problem solving, theorem knowledge, and robustness to equivalent formulations.
  • Formal theorem proving: 1.25% to 11.25% to 16.56%: DeepSeek-Prover-V1.5 accuracy rises from the base model to reinforcement learning and then RMaxTS.The progression suggests a benefit from search-based inference in formal theorem proving.
  • Formal theorem proving: 21.88%: Goedel-Prover-V2 achieves the best Lean 4 performance on MathAdv, followed by DeepSeek-Prover-V1.5 RL + RMaxTS.Both systems employ verifier-guided search rather than one-shot generation.
  • Domain performance: Performance varies substantially by domain: Goedel-Prover-V2 performs best in number theory and linear algebra, while all models score 0% on topology.The reported imbalance is associated with uneven training coverage and the difficulty of formalizing some areas.
  • Natural-language reasoning and knowledge: Most models score higher on direct-answer and multiple-choice problems than on corresponding Lean tasks, indicating that formalization remains an additional challenge beyond solving or recognizing the mathematics.Goedel-Prover is an exception, performing comparatively worse on direct-answer and multiple-choice tasks despite strong theorem-proving performance.
  • Robustness to reformulation: Most models more often solve an original problem but fail its equivalent transformed version than the reverse, exposing sensitivity to wording or structure.The asymmetry is especially pronounced for Goedel-Prover-V2 and DeepSeek-R1, although the absolute counts are small.
  • Overall findings: Current models remain limited by mathematical knowledge, formal proof construction, uneven domain coverage, and sensitivity to equivalent formulations.The component-wise evaluation makes these distinct capability limitations visible beyond aggregate theorem-proving accuracy.

5 Failure Analysis and Improvement Strategies

The failure analysis distinguishes plausible mathematical ideas from valid Lean proofs and examines verifier interaction and natural-language hints as improvement strategies. Feedback improves performance and changes the error profile, while hints help general-purpose models but substantially reduce proof-specialized performance.

  • Failure modes and successful patterns: Many failed proofs begin with reasonable ideas but omit necessary steps, use unsuitable tactics or nonexistent lemmas, or repeat without progress.Successful proofs instead retrieve an appropriate Mathlib result or construct the argument step by step while tracking remaining goals.
  • Failure modes and successful patterns: Four recurring failure modes are incomplete proofs, unsuitable proof commands, invented library results, and repeated commands that do not change the remaining goal.A plausible overall idea is insufficient unless each step is checked for what it proves and whether it advances the proof.
  • Interactive Lean feedback: Interactive Lean feedback is evaluated under the same total budget, K = 16 × 3, for interactive and non-interactive settings.The protocol appends Lean error messages for up to T turns across N independent attempts, with K = N × T.
  • Interactive Lean feedback: Interactive feedback improves both DeepSeek-V3.2 and GPT-5.4, but shifts remaining failures toward constructing and applying the formal argument after surface syntax errors are corrected.GPT-5.4 often introduces unnecessary intermediate claims and replaces rejected short proofs with longer attempts.
  • Natural-language hints: Hints derived from corresponding multiple-choice questions are added to the standard Lean theorem-proving prompt.The experiment tests whether supplying relevant mathematical knowledge and proof strategies helps end-to-end formal proof construction.
  • Natural-language hints: Hints improve the two DeepSeek models but substantially reduce Goedel-Prover-SFT and Goedel-Prover-DPO performance.The results support model-dependent guidance: general-purpose models may benefit from informal reasoning hints, whereas proof-specialized systems may need Lean-aligned guidance.

6 Conclusion and Limitations

MathAdv provides a broad, component-wise diagnostic benchmark for formal mathematical reasoning, while remaining limited by expert-scaling demands and current Mathlib coverage.

  • MathAdv spans 13 mathematical domains and evaluates background knowledge, problem solving, formal proof construction, and robustness to equivalent reformulations.
  • Its auxiliary tasks complement Lean 4 theorem proving by providing a finer-grained view of why models succeed or fail.
  • MathAdv remains modest in size because creating and validating high-quality problems across many domains requires substantial expert effort.
  • Current Mathlib coverage constrains formalization, leaving some advanced problems deferred until the library expands.

C Data sources

The data sources combine domain-specific mathematical references with an expert-reviewed, verifier-in-the-loop process for producing Lean 4 statements and evaluating model judgments.

  • Data sources: MathAdv draws from mathematical sources spanning Fourier and functional analysis, combinatorics, calculus, probability, geometry, topology, algebra, logic, and related domains.
  • Autoformalization: An LLM-based autoformalizer translates each natural-language problem statement into Lean 4.
  • Autoformalization: Compiler feedback drives iterative syntax correction until the Lean code compiles without syntax errors.
  • Autoformalization: Independent LLM and human checks assess semantic fidelity, followed by final review from another human expert.
  • Evaluation: Models are separately queried about Lean 4 compilation and theorem semantics in 360 calls across four models.

D.2 Results and Analysis

The appendix reports model evaluations, formalization examples, computational budgets, and diagnostic procedures across Lean 4 tasks and mathematical domains.

  • Junk Theorems: Table 5 summarizes model performance on the Lean 4 Junk Theorems testbed.
  • Junk Theorems: 58% was the highest compilation-prediction accuracy for gpt-5.5, compared with 4% for the DeepSeek models.
  • Junk Theorems: DeepSeek-v4-pro scored 1.91/2.00 on semantic meaning while predicting compilation failures 96% of the time.
  • Mathlib coverage: The Riemannian-geometry example requires formalizing specialized curvature, volume, geodesic-ball, and model-space concepts unavailable or incomplete in Mathlib.
  • Computational budgets: Proof-step generation budgets use K = N × S × T, while whole-proof generation is measured with pass@K.
  • Additional analyses: The appendix also reports accuracy by domain, interaction condition, model, and representative error category.

H.1 Incorrect Theorem Application

The examples show theorem-proving failures caused by incorrect theorem application, malformed proof construction, and tactics that do not match the remaining goal.

  • Incorrect theorem application: The proof contains syntax and elaboration errors, including an unexpected have token and a function-application error involving pow_card_eq_one.A later state remains unsolved with goal orderOf (x ^ 13) = 3.
  • Incorrect theorem application: GPT-5.4 identifies the intended strategy but incorrectly derives x^2 = 1 instead of x^3 = 1, leaving the final goal unsolved.The resulting proof state no longer matches the intended argument.
  • Incorrect tactic selection: Using omega for the final divisibility goal fails because the remaining obligation is not linear arithmetic.The overall proof direction is described as reasonable, but the selected tactic cannot establish the required divisibility property.
  • Incorrect tactic selection: DeepSeek-Prover-V1.5-RL repeatedly applies the same tactic without progressing toward the goal, potentially consuming the token budget.The proof state remains essentially unchanged during the loop.

I.1 Exact-lemma proofs

The exact-lemma examples show models succeeding when existing lemmas or direct case analyses closely match the target, while interaction changes proof construction and exposes inefficiencies.

  • Exact-lemma proofs: DeepSeek-R1 discharges the Dedekind-algebra induction goal by applying Set.mem_sInter.mp to the closure axiom.It constructs the predicate set as closed under the successor function before invoking the closure property.
  • Exact-lemma proofs: DeepSeek-R1 reduces ordinal trichotomy to lt trichotomy followed by a case split.The resulting proof separates the less-than and greater-than cases.
  • Exact-lemma proofs: The power-set non-enumerability proof uses a diagonal-style contradiction by comparing Part.some and Part.none outputs.The construction derives an index whose function must both return a value and remain undefined.
  • Exact-lemma proofs: In the exam-score problem, the interactive proof derives the total score 10800 and bounds the selected scores by their cardinality times 180.The proof then uses nonnegativity to relate the selected-score sum to the total sum.
  • Exact-lemma proofs: The non-interactive proof introduces intermediate have statements that are never used in the final proof.This pattern occurs less frequently in the interactive setting.

J.2 Manual longer proofs

The manual longer-proof examples show interactive models replacing overly compressed proof attempts with explicit constructions and case analyses that align more closely with the target.

  • Manual longer proofs: For the factorial cardinality theorem, interaction replaces a direct lemma application with an explicit Equiv.Perm construction and a calc chain.The construction establishes an equivalence between bijections on Fin n and permutations before applying cardinality lemmas.
  • Manual longer proofs: The examples contrast successful interactive proof snippets with failed non-interactive snippets.The contrast is shown for both the factorial-cardinality and ordinal-trichotomy problems.
  • Manual longer proofs: For ordinal trichotomy, the interactive proof uses by_cases on α = β and then applies lt_or_gt_of_ne to the unequal case.This replaces the shorter simpa-with-lt-trichotomy strategy.
Loading 2608.25449v1…