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

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

Stage 4a: Question Stem and Correct Choice. A key design principle is that every question should read as a genuine research-type question about a specific mathematical object or property, rather than a generic request such as “which is the correct result below.” To this end, the generator selects one of thirteen category-specific system prompts , one for each logical type in Table 1 , each prescribing a tailored stem formulation that exercises the distinguishing logical feature of the category. For example, an equivalence-type theorem is transformed into a question that presents one side of the biconditional and asks “which statement is equivalent to A A ?”; an implication-type theorem embeds all hypotheses in the stem and asks “which is the strongest conclusion about … that holds under these assumptions?”, etc. With the strongest quantifier, we ensure there is a unique answer for questions of all logical types.

Each prompt further instructs the model to (i) isolate a single decisive mathematical feature of the conclusion, such as quantifier scope, sharp bound, exact dependence, existence versus uniqueness, or asymptotic regime, rather than restating the theorem verbatim, and (ii) define any paper-specific objects or notation inline so that the question is self-contained. Red-flag checks automatically reject stems containing trivializing phrases (e.g., “which of the following is the strongest result”) or correct options that bundle multiple theorem clauses, triggering a regeneration pass. Finally, a repair pass re-examines the draft stem and, operating in theorem_only_repair mode, injects any missing definitions or notation from the recovered paper context (Stage 3, Step 5) to guarantee self-containedness without leaking answer-relevant information.

Stage 4b: Sketch-Adversarial Distractor Generation. The model receives the theorem, proof sketch, question stem, and correct choice, and generates four distractors (Options B–E). The proof sketch plays a critical role: by exposing the “load-bearing” logical steps of the argument (e.g., the dependence of constants on hidden parameters, a critical case split, or a uniformity condition that distinguishes effective from non-effective bounds), the generator is guided to engineer distractors that exploit specific mathematical constraints or misconceptions. Each distractor is constructed by one of four general perturbation strategies:

• Controlled perturbation. A small surface-level modification to the theorem’s conclusion, such as an altered constant, exponent, inequality direction, or parameter range.

• Semantic weakening. A statement that is plausible but strictly weaker than the theorem’s conclusion, e.g., dropping a uniformity requirement or restricting the domain.

• Semantic strengthening. A statement that overstates the conclusion beyond what is proven, e.g., adding uniqueness, higher regularity, or optimality not asserted by the theorem.

• Property confusion. A statement concerning a closely related but non-equivalent mathematical object or property, e.g., swapping an L 2 L^{2} norm for an L ∞ L^{\infty} norm, or confusing pointwise convergence with uniform convergence.

The concrete realization of each strategy is category-dependent : the distractor prompt is tailored to the theorem’s logical type (Table 1 ). For instance, for an equivalence-type theorem the controlled perturbation modifies a quantifier within one side of the biconditional, whereas for a bound-type theorem it alters the exponent or direction of the inequality; for an existence-type theorem the semantic strengthening adds uniqueness not stated in the theorem, whereas for a classification-type theorem it replaces the bijection with a mere surjection. This category-aware design ensures that distractors probe the decisive logical feature specific to each theorem type, rather than relying on generic, one-size-fits-all perturbations. An adversarial revision pass subsequently re-examines the generated distractors, auditing them for surface-level distinguishability from the correct option and rewriting any that can be rejected without genuine mathematical inspection.

Substitution-Resistant Option Design. A common shortcut exploited by strong models is option substitution : systematically plugging each candidate answer back into the question stem and verifying consistency, rather than deriving the answer through genuine mathematical reasoning. Process-of-elimination strategies similarly bypass comprehension by narrowing choices through superficial cues. To counteract both shortcuts, we introduce a substitution-resistant mechanism: for a configurable fraction of generated items, the correct option is replaced with the meta-option “One of the remaining options is correct, but a stronger result can be proven.” Answering correctly now requires the model to (i) identify the valid option among the distractors and (ii) independently determine whether a strictly stronger result holds, a task that demands substantive mathematical reasoning about the relative strength of claims and cannot be resolved by mechanical substitution or elimination alone.

Quality Rubric. Each generated MCQ undergoes a quality evaluation scored on a 0 0 – 8 8 rubric comprising four dimensions: • Answer Leakage Score (ALS, 0–2): Measures whether the correct answer is inadvertently revealed by the question stem or distractor phrasing.

• Tautology Avoidance Score (TAS, 0–2): Assesses whether the correct option is trivially true or self-evident without mathematical knowledge.

• Generative Pressure Score (GPS, 0–2): Evaluates whether distractors exert sufficient “pressure” to discriminate genuine understanding from guessing.

• Distractor Quality Score (DQS, 0–2): Rates the mathematical plausibility, precision, and diversity of the distractors.

MCQs that do not meet a minimum aggregate threshold (5) are discarded.

Stage 5: Rote-Recall Prevented Triviality Filter. Stage 5 ensures that the remaining questions are not trivially solvable from the question stem alone, without reference to the answer choices. A judge model receives only the question stem (with all options withheld) and generates a free-form response. A second judge then determines whether this response matches the correct answer (Option A). Questions for which the stem alone reveals the answer are classified as stem-trivial and excluded from the final candidate pool. This filter prevents the benchmark from rewarding rote recall and ensures that genuine option-level reasoning is required.

Stage 6: Hardness Calibration. Stage 6 ensures that the final benchmark is genuinely difficult for state-of-the-art models through a three-step calibration pipeline:

Step 1: Overgenerate Hard Pool. For each stem-nontrivial item, we retain both the original distractor set and one regenerated alternative set, thereby doubling the candidate pool per source theorem. This overgeneration increases the likelihood of retaining at least one maximally challenging variant.

Step 2: First-Pass Accuracy Test. A frontier model is evaluated on the entire candidate pool at moderate reasoning effort. Items that the model answers correctly are flagged as potentially too easy.

Step 3: Source-Level Hardest Selection. For each source theorem, the pipeline compares all surviving candidate variants and selects the hardest , defined as the variant the calibration model answered incorrectly while achieving the highest quality rubric score. Source groups in which all candidates were solved are dropped entirely. This procedure yields the final benchmark subset.

Stage 7: Evaluation Protocol. We propose a dual-mode evaluation protocol: Mode 1: Selection. The model receives the question stem and all five options, then selects the answer that it judges to be the correct theorem statement. This mode evaluates the model’s baseline mathematical comprehension. Mode 2: Sketch-Aware Selection. The model additionally receives the proof sketch as a hint alongside the stem and options. By comparing performance across modes, we isolate the model’s ability to synthesize and apply high-level proof strategies, a proxy for mathematical intuition .

To ensure a fair rendering of notations, all questions undergo L a T e X validation via compilation and, when necessary, automated L a T e X repair before presentation to the model.

## 3 Benchmark

We summarize the logical-form composition of the hard benchmark split in Figure 3 . The hard split contains 177 theorems in total, and a single theorem may belong to multiple logical categories. The benchmark therefore covers a broad range of theorem structures rather than concentrating on a single template: implication and universal statements are the most common categories, followed by existence and inequality/bound problems. The month-level breakdown further shows that benchmark composition changes over time while preserving category diversity, with all slices drawn from papers released after the evaluated models’ knowledge cutoffs. Examples can be found in the Appendix C .

## 4 Evaluation Results

#### Even frontier models suffer.

Figure 1 shows overall accuracy on LiveMathematicianBench . The strongest performance is achieved by Gemini-3.1-pro-preview at 43.5% overall, followed by GPT-5.4 (high) at 41.8%. Even the strongest systems remain far from saturation.

#### Category-wise pattern and monthly trajectories.

Figure 4 -(a) shows that no single model dominates every reasoning type. Gemini-3.1-pro-preview achieves the strongest overall profile and is particularly competitive on biconditional/equivalence and classification/bijection problems, whereas GPT-5.4 variants are stronger on implication, universal, and inequality/bound items. These categories combined constitute a substantial portion of the benchmark (Figure 3 ). This heterogeneity suggests that research-level mathematical reasoning is not a one-dimensional capability: models with similar aggregate performance can still exhibit sharp weaknesses on particular logical forms. The monthly trajectories in Figure 4 -(b) further show that performance is unstable across benchmark slices. Several models do best on the 2026/01 subset but perform worse again on the 2026/02 subset.

#### Substitution-resistant options sharply reduce accuracy.

Figure 5 -(a) compares model accuracy on the original-choice subset and the substitution-resistant subset, where the correct answer is replaced by a stronger meta-option intended to frustrate shortcut strategies such as direct substitution and surface-level elimination. Across all evaluated systems, the substitution-resistant setting is substantially harder than the original-choice setting. The strongest original-choice performance is achieved by Gemini-3.1-pro-preview at 67.4%, but its accuracy drops to only 17.6% on substitution-resistant items, below the 20% random-guess baseline. GPT-5.4 provides a useful contrast: although it ranks second overall, it reaches 52.2% on original items under both medium and high reasoning effort and still retains 29.4%–30.6% on the substitution-resistant subset. GPT-5.4 is therefore more stable under the harder choice design, remaining above the random-guess baseline even when the benchmark removes the direct theorem statement as an option, whereas most other evaluated models fall to chance level or below. More broadly, the remaining difficulty in LiveMathematicianBench lies not only in understanding the theorem itself, but also in reasoning among nearby mathematical claims once surface matching and answer substitution become ineffective.

#### Proof sketches yields a consistent improvement.

As shown in Figure 5 -(b), GPT-5.4 (high) improves from 41.8% to 53.7% overall, a gain of 11.9% points, while Gemini-3.1-pro-preview (high) rises from 43.5% to 57.1%, a gain of 13.6% points. This pattern suggests that proof sketches are not merely redundant restatements of the theorem. Instead, they provide useful strategic information that helps models disambiguate closely related answer choices and identify the load-bearing structure of the argument.

## 5 Endnote and Discussion

From aggregate accuracy alone, Gemini-3.1-pro-preview (high) achieves the highest score, with GPT-5.4 variants close behind by less than 3%. However, a category-level analysis in Section 4 (Fig. 4 (a)) reveals additional structure that supports the first central design choice of LiveMathematicianBench : organizing problems by logical type. Performance varies meaningfully across logical forms in ways that are not visible from aggregate scores alone. This suggests that logical structure may be an important axis along which current models differ, and it raises a broader interpretability question: why are some models systematically stronger on certain forms of reasoning than others? If such patterns persist at scale, they may also have practical implications for mathematical workflows, since different models may prove more useful for different kinds of reasoning tasks. In this sense, a logic-based taxonomy complements traditional field-based categorization by capturing structural similarities that cut across mathematical areas. More broadly, this suggests that LiveMathematicianBench can serve not only as a leaderboard benchmark, but also as a diagnostic testbed for studying structure-specific strengths and weaknesses in mathematical reasoning. This diagnostic value is especially relevant because the benchmark is constructed from recent post-cutoff arXiv papers, making it less vulnerable to rapid saturation and contamination than static mathematics benchmarks. In this sense, LiveMathematicianBench contributes not only a new dataset, but also a more durable evaluation setting for tracking progress in research-level mathematical reasoning.

Substitution-resistant options (Stage 4b) are designed to test whether a model can recognize that the semantically weakened option is true while also inferring that a strictly stronger statement follows from the hypotheses. Success on such questions therefore requires an additional deductive step. In this sense, substitution-resistant questions provide a useful probe of whether a model can move beyond recognition toward a limited form of mathematical conjecturing. This is precisely the kind of ability mathematicians hope AI systems may leverage on when facilitating research, as illustrated by the work of Georgiev et al. (2025) using AlphaEvolve for mathematical exploration and discovery. As highlighted in Section 4 , all tested models perform substantially worse with substitution-resistant options (Fig. 5 (a)). This gap suggests that current models rely heavily on option substitution in standard multiple-choice settings. More importantly, it underscores the importance of adversarial option design for isolating genuine reasoning ability. At its core, it shows that benchmark design can materially affect the capabilities we appear to measure. From considerations of both overall benchmark performance and performance under substitution-resistant evaluation, GPT-5.4 (high) and Gemini-3.1-pro-preview (high) emerge as the two strongest models on LiveMathematicianBench .