LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches — part 1/4

Cleaned-text code points [0, 15455). Bibliography omitted here; source.md includes it.

# LiveMathematicianBench : A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches

###### Abstract

Mathematical reasoning is widely regarded as a hallmark of human intelligence, and determining whether large language models (LLMs) can meaningfully perform it remains a central question in artificial intelligence and cognitive science. As LLMs are increasingly integrated into scientific workflows, rigorous evaluation of their mathematical capabilities becomes a practical necessity. Existing mathematical reasoning benchmarks, however, are often limited by synthetic problem settings and growing contamination from widely circulated datasets.

We present LiveMathematicianBench , a dynamic multiple-choice benchmark for evaluating research-level mathematical reasoning using recent arXiv papers published after model training cutoffs. By grounding evaluation in newly published theorem statements, the benchmark provides a more realistic testbed for assessing whether models can reason about natural mathematical claims beyond memorized benchmark patterns. LiveMathematicianBench introduces a taxonomy of thirteen problem categories based on the logical form of theorem statements, enabling fine-grained evaluation across reasoning types such as implication, equivalence, existence, and uniqueness. It further introduces a proof-sketch-guided distractor generation pipeline, in which proof sketches are used to construct plausible but invalid answer choices that reflect misleading proof directions. This design makes the benchmark more sensitive to genuine mathematical understanding rather than surface-level answer matching. We additionally introduce a substitution-resistant evaluation mechanism designed to distinguish answer recognition from substantive mathematical reasoning.

Evaluation of frontier models shows that the benchmark is far from saturated: the best-performing model, Gemini-3.1-pro-preview, achieves only 43.5% accuracy in the standard setting. Under substitution-resistant evaluation, accuracy drops sharply across all models: GPT-5.4 achieves the highest score at 30.6%, while Gemini-3.1-pro-preview falls to 17.6%, below the 20% random baseline. A dual-mode protocol comparing performance with and without proof-sketch access reveals that sketches yield consistent gains (e.g., +13.6 pp for Gemini-3.1-pro-preview), suggesting that models can leverage high-level proof strategies to improve reasoning.

Overall, LiveMathematicianBench offers a scalable and contamination-resistant testbed for studying research-level mathematical reasoning in large language models.

## 1 Introduction

As large language models (LLMs) become increasingly integrated into scientific workflows, evaluating their reasoning ability has become a central challenge. Mathematics is a natural domain for this evaluation because it combines precise logical structure with verifiable ground truth. Yet existing benchmarks, including GSM8K ( Cobbe et al., 2021 ) , MATH ( Hendrycks et al., 2021 ) , AIME, MathVista ( Lu et al., 2023 ) , Omni-Math ( Gao et al., 2024 ) , and OlympiadBench ( He et al., 2024 ) , are largely synthetic, competition-based, or historically sourced, and are increasingly susceptible to contamination. These limitations reduce their value for assessing research-level mathematical reasoning in frontier models.

The core limitation lies in the fundamental mismatch between “Olympiad-style” competition mathematics and authentic mathematical research. Existing benchmarks predominantly feature calculation-heavy problems that reward heuristic pattern matching and the use of specialized tricks to obtain a closed-form answer. Although challenging, such tasks do not reflect the true nature of mathematics research.

By research-level mathematics , we mean open-ended, non-routine mathematical reasoning that is characterized by abstraction, sensitivity to technical hypotheses, and the lack of a pre-specified solution strategy. Such work often requires one to reason through layers of definitions, infer subtle logical dependencies, and identify the right conceptual framework in which a problem can even be meaningfully posed. A central difficulty of research lies not only in proving statements, but also in determining what the right question is to ask and what potential statement might be true in the first place. Unlike competition problems, naturally arising research questions do not come with a contrived setup, an intended solution path, or even a clear indication of which tools are relevant. Progress therefore often requires exploration under substantial uncertainty, familiarity with prior literature, and occasional conceptual innovations, which are sometimes sparked by ideas from seemingly unrelated fields of mathematics.

This gap is visible even at the level of theorem comprehension. A model that can solve routine calculus or algebra problems may still fail to track the precise hypotheses of a modularity lifting theorem, a stability result in geometric invariant theory, or a compactness theorem in nonlinear PDE, where small changes in local conditions, regularity assumptions, or finiteness hypotheses can fundamentally alter the statement. Therefore, to truly assess an LLM’s potential as a scientific research assistant, evaluation must shift from measuring the ability to ”solve exams” toward measuring the ability to comprehend, interpret, and reason about mathematical hypotheses and statements.

This conceptual mismatch is compounded by a second problem: data contamination. State-of-the-Art (SOTA) models have reached saturation on standard benchmarks, often exceeding 90% accuracy, yet this performance is brittle. Studies suggest that many problems have leaked into pre-training corpora, allowing models to memorize solution templates rather than derive answers from first principles ( Glazer et al., 2024 ) . Consequently, performance drops precipitously when questions are rephrased or numerical values altered. This reliance on static, potentially contaminated datasets necessitates a shift toward continuous and refreshable evaluations grounded in authentic research artifacts.

Notably, Zhang et al. (2025) introduced RealMath, a benchmark derived directly from arXiv papers to reduce contamination risk. While RealMath reduces contamination risk and demonstrates that LLMs can engage with research-derived material, its construction prioritizes theorem types that admit straightforward automated verification. As a result, it covers only a limited subset of research-level mathematical reasoning, with less support for tasks involving inequalities, asymptotic relations, or non-constructive arguments, excluding common research tasks such as establishing asymptotic bounds in analysis, deriving classification results in algebraic geometry, or determining modes of convergence in probability. These limitations suggest that the central challenge is not only to control contamination risk in benchmarks, but to do so without collapsing research mathematics into a narrowly verifiable subset of problems of limited width and depth.

To address these limitations, we introduce LiveMathematicianBench , a benchmark framework that expands evaluation along two dimensions: the diversity of mathematical reasoning it captures and the use of high-level proof strategies, enabling evaluation beyond statement-level recognition to strategy-level mathematical reasoning.

For the first dimension, we introduce a taxonomy of thirteen distinct problem types defined by the underlying logical forms and tailor question design to each type. Unlike RealMath, whose questions are restricted to settings with a single uniquely verifiable answer, this framework enables evaluation of mathematical skills that are central to research practice but often considered too ambiguous for automated metrics. These include Logical Structure (distinguishing necessary vs. sufficient conditions via Equivalence and Implication), Qualitative Analysis (establishing Inequalities and Asymptotic bounds), and Generalization (validating Universal quantifiers and structural Bijections).

For the second dimension, we incorporate proof sketches into the benchmark. A proof sketch is a high-level outline of the main ideas and strategic steps of a proof, omitting most technical details. Access to this proof structure makes question construction more targeted and more diagnostic: instead of merely testing whether a model can retrieve a theorem statement, it allows us to design questions about the same result that probe deeper structural understanding. Without such proof-aware design, questions are more likely to be too easy or to reward memorization and surface-level pattern matching. Proof sketches also enable a dual-mode evaluation protocol, where models are assessed both with and without access to high-level proof guidance. This makes it possible to measure whether strategic hints improve mathematical reasoning, and how effectively current models can use them.

Building on these two design principles, we introduce the LiveMathematicianBench , a dynamic benchmark designed to assess LLMs on research-level mathematical reasoning. Each item is presented as a multiple-choice question ( MCQ ) with five answer options, exactly one of which is correct. Our contributions fall into three categories: benchmark construction, methodological novelty, and scientific questions enabled by the benchmark.

Our contributions are threefold. 1) We present a contamination-resistant benchmark for research-level mathematical reasoning, built from dynamically sourced post-cutoff arXiv theorems, organized by a logic-based taxonomy, and augmented with curated proof sketches. 2) We introduce a proof-aware benchmark construction methodology, including category-specific question design, sketch-adversarial distractor generation, and dual-mode evaluation with and without sketch access. 3) We establish a new testbed for studying higher-level mathematical reasoning in LLMs, including logical-form-specific failure modes, the use of proof-level guidance, and progress beyond theorem recognition toward proof planning.

## 2 Methods

Our benchmark construction pipeline transforms raw arXiv papers into calibrated research-level multiple-choice questions (MCQs). The pipeline contains seven stages: (1) paper retrieval, (2) L a T e X source extraction, (3) theorem extraction and classification, (4) MCQ generation, (5) stem-only triviality filtering, (6) hardness calibration, and (7) model evaluation. Each stage is designed to preserve mathematical fidelity while increasing question discriminativeness and benchmark difficulty. Human validation is performed at every stage to ensure quality control (see Appendix B for details).

Stage 1: Paper Retrieval. We query the arXiv API for papers submitted within a target month under the math.* category. The retrieval window is incrementally widened until a configurable maximum number of papers is collected. For each paper, we record its arXiv identifier, submission link, source link, and title. By restricting retrieval to papers published strictly after a model’s training cutoff, we ensure that the resulting benchmark is contamination-free by construction.

Stage 2: L a T e X Source Extraction. For each retrieved paper, we download its e-print source archive and extract the constituent .tex files. The extractor resolves \input and \include directives to reconstruct the complete document in its logical order, strips L a T e X comments and comment environments, and concatenates the result into a single full-text representation. This produces a clean, self-contained L a T e X corpus suitable for downstream parsing.

Stage 3: Theorem Extraction and Classification.

Stage 3a: Hybrid Agentic Extraction. Extracting well-formed theorem statements from raw L a T e X is nontrivial due to the heterogeneity of document styles, custom macros, and cross-referencing conventions. We adopt a hybrid agentic extraction architecture that balances throughput with robustness:

1. Rule-based fast path. A rule-based extractor restricts its search to the Introduction section, exploiting the convention that a paper’s main theorem is formally stated there. Within the introduction, it identifies all theorem-like environments declared via \newtheorem in the preamble (excluding remark -type environments) and applies a priority ranking : the standard theorem environment is selected first; only if no theorem block is found does the extractor fall back to custom environments. This design ensures that auxiliary results such as lemmas, propositions, or corollaries, which may appear elsewhere in the introduction, are not mistakenly extracted in place of the main theorem.

2. Agentic fallback. When the rule-based path fails (e.g., due to an absent Introduction heading or unconventional formatting), an LLM-based agentic extractor is invoked over a larger document window. The extraction prompt explicitly instructs the model to return at most one primary theorem-level claim and to prefer theorem environments over lemma , proposition , or corollary when multiple candidates appear, maintaining the same main-theorem priority as the rule-based path.

3. L a T e X normalization. Custom commands ( \newcommand , \def ) are expanded in-line so that downstream modules receive standard mathematical notation.

4. Reference resolution. Internal cross-references ( \ref , \eqref ) are resolved by collecting all labeled environments and substituting their content, producing an Expanded Theorem that is semantically self-contained.

5. Context recovery. A two-layer retrieval mechanism assembles the notational and definitional context needed to make the theorem self-contained. First , within the Introduction, paragraph blocks preceding the theorem are scored by (i) token overlap with the theorem statement, (ii) the presence of definitional cues (e.g., “let,” “denote,” “suppose”), (iii) mathematical content density, and (iv) positional proximity, with the two blocks immediately before the theorem always retained. The top-scoring blocks are selected and concatenated in their original order. Second , a full-paper pass extracts high-value anchor terms from the theorem and scans the entire document for blocks containing definitions, setup, or preliminaries, scoring them by anchor-term hits, section-heading relevance (e.g., Setup , Preliminary ), and distance to the theorem. Finally, any content referenced via \ref or \eqref within the selected blocks is resolved and appended, and the combined context is trimmed to a character budget.

Stage 3b: Proof-sketch summarization. A large language model extracts a concise proof sketch for each theorem, capturing the high-level strategy without full formal detail. These sketches serve a dual purpose: they inform adversarial distractor generation (Stage 4) and enable sketch-aware evaluation (Stage 7).

Stage 3c: Logical Taxonomy of Theorems. Each extracted theorem is classified into one of thirteen logical categories, listed in Table 1 . Classification is performed by a specialized LLM-based classifier. This taxonomy enables fine-grained diagnosis of model reasoning failures across distinct logical forms.

Stage 4: Question–Answer Pair Generation. Stage 4 synthesizes adversarial MCQs via a two-stage generative protocol , each informed by the theorem’s logical category and the proof sketch.