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

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

Finally, we have observed earlier that providing proof sketches at inference time induces significant performance improvements in the two highest-scoring models (Fig. 5 (b)). Since proof sketches are extracted from the source papers and typically summarize the central ideas of the proof at a high level, this result suggests that models can often use strategic mathematical guidance without full derivational detail, demonstrating some similarities to how expert researchers work. These findings further support the second design philosophy of LiveMathematicianBench : incorporating proof strategy into evaluation rather than restricting assessment to statement-level recognition alone. More broadly, they indicate that the benchmark can distinguish not only whether a model reaches the correct answer, but also how its performance changes when supplied with information closer to the level of mathematical strategy used by human researchers. Collectively, these features make LiveMathematicianBench useful not only for comparing current models, but also for future work on proof-guided reasoning, tool use, and interactive mathematical exploration.

## Appendix A Related Work

#### Standard and Advanced Mathematical Benchmarks

The evaluation of mathematical reasoning in large language models has traditionally relied on static datasets spanning elementary to undergraduate-level problems. Early benchmarks such as GSM8K ( Cobbe et al., 2021 ) and MATH ( Hendrycks et al., 2021 ) helped establish common evaluation standards for quantitative and symbolic reasoning. As model performance has improved, however, these benchmarks have become less discriminative for frontier systems.

Subsequent work has therefore shifted toward more challenging settings. The Advanced Reasoning Benchmark (ARB) ( Sawada et al., 2023 ) and GHOSTS ( Frieder, 2023 ) extend evaluation toward graduate-level mathematics, with GHOSTS further emphasizing natural language interaction and expert assessment. Other efforts focus on competition-level mathematics, including OlympiadBench ( He et al., 2024 ) , PutnamBench ( Tsoukalas et al., 2024 ) , and Omni-Math ( Gao et al., 2024 ) . These benchmarks substantially increase difficulty, but because they are derived from historical competition archives, they may be more susceptible to contamination from pretraining data and benchmark-specific memorization.

#### Contamination Mitigation, Formal Mathematics, and Frontier-Level Evaluation

Several recent benchmarks attempt to mitigate contamination more directly. Putnam-AXIOM ( Gulati et al., 2025 ) perturbs existing problems through programmatic modifications such as renaming variables or altering constants. While this strategy can reduce exact overlap with known solutions, it preserves much of the original problem structure. The AI Mathematical Olympiad (AIMO) ( XTX Markets, 2024 ) instead introduces newly created olympiad-style problems, and MiniF2F ( Zheng et al., 2021 ) focuses on formally verified mathematics across theorem proving systems such as Lean and Isabelle. These directions address important aspects of evaluation reliability, but they remain centered on competition-style or formalized problem settings.

Moving beyond competition settings, First Proof ( Abouzaid et al. (2026) ) curates a collection of ten original, research-level problems drawn directly from the authors’ active work. While this approach effectively guarantees the absence of data contamination, the extremely small sample size limits its utility as a comprehensive evaluation benchmark.

FrontierMath ( Glazer et al., 2024 ) is more closely related to our setting in that it targets highly difficult mathematics under reduced contamination risk through a larger set of expert-authored problems. However, similar to First Proof, tailored problem authoring requires substantial dedicated human effort, which inherently limits scalability.

LiveMathematicianBench differs in both construction and evaluation emphasis. Rather than relying on manually authored problems, it draws from a continuously growing stream of recent arXiv papers, enabling a scalable and refreshable benchmark construction pipeline. In addition, whereas prior benchmarks largely emphasize answer derivation, our framework explicitly evaluates structural comprehension through theorem-level logical categories and proof-sketch-guided distractors that probe sensitivity to plausible but invalid reasoning directions.

## Appendix B Human Validation Protocol

All prompts used in theorem extraction, classification, question generation, and filtering were authored by a research-level mathematician. For quality control, the final released set of 177 benchmark items was reviewed for theorem fidelity, self-containedness, answer uniqueness, and distractor quality. To audit upstream pipeline quality, we additionally performed stratified reviews of intermediate outputs, sampling approximately 10 cases per logical category for theorem extraction, category assignment, proof-sketch quality, and MCQ generation. Given the unusual breadth and depth of the mathematical content covered by the pipeline, these reviews were intended as benchmark quality control, assessing whether outputs were mathematically sound, internally consistent, and benchmark-ready, rather than as full peer-review-level sense of independent verification of every source-paper claim.

We now provide an example demonstrating how the combination of prompt design and human validation ensures that all distractors are demonstrably false, thereby guaranteeing the overall validity of the MCQs.

In Appendix C , Example C is generated from an Existential-Universal type theorem, and the correct option generated from the theorem is replaced by the correct substitution-resistant option. When generating distractors, the system prompt (see Appendix G , Stage 4b) forces the LLM to include a meta description for each distractor indicating the type of perturbation strategies used in its construction. For Example C , the meta description reads:

"meta": { "weaker_true_label": "C", "false_labels": [ "B", "D", "E" ], "wildcard_false_label": "B" }, "sketch_usage_meta": [ { "label": "B", "sketch_hook_type": "counting_estimate", "tampered_component": "counts signed cubic discriminants instead of cubic fields", "template_used": "wildcard" }, { "label": "C", "sketch_hook_type": "finiteness", "tampered_component": "dropped the lower bound guaranteeing at least k/2 cubic fields in the interval", "template_used": "weaker_true" }, { "label": "D", "sketch_hook_type": "counting_estimate", "tampered_component": "threshold k/2 replaced by (k+1)/2", "template_used": "stronger_trap" }, { "label": "E", "sketch_hook_type": "regularity", "tampered_component": "removed the epsilon-loss in the exponent", "template_used": "stronger_trap" } ]

We first notice that option C is the ”weaker_true_label”, meaning that it is strictly weaker than the theorem’s assertion (which is always true if we assume the theorem itself is true). However, since the question asks for the ’strongest’ true statement, option C is not correct.

Option B is the ”wildcard_false_label”, meaning that it is designed to be false but with a question specific tempering. It counts the number of integers within that range that are determinants of cubic fields. This is clearly not the same as counting the number of cubic fields, as multiple non-isomorphic fields can share the same discriminant. Therefore, it is not realistic for a smaller set to have the same lower bound. This reasoning aligns with the ”tempered_component” field provided in the meta description. Moreover, this option critically uses the proof sketch.

Option D and E are false labels tempered with ”stronger_trap”, meaning that they are strengthened versions of the theorem statement in different ways. Option D increases the lower bound of the set being counted, making the statement stronger. However, the lower bound is obtained by explicit construction and a bigger lower bound cannot be achieved. Option E modifies the count for the specific integers d d by removing the epsilon factor in the exponent. The epsilon-dependence in the original theorem comes from deep conjectures in the subject of counting number fields, which cannot be removed.

To conclude, taking the original theorem as the ground truth, we can see from a combination of meta description and human expertise that the distractors are false and the MCQ is valid. In particular, this example demonstrates that our prompt design alone has guaranteed the mathematical falsity of the distractors to a great extent.

## Appendix C Detailed Logical Taxonomy of Theorem Categories

This appendix provides extended descriptions of the thirteen logical theorem categories listed in Table 1 . The taxonomy focuses exclusively on the logical form of a theorem statement, independent of its mathematical topic or context. Each category is accompanied by its canonical logical form and a representative example.

#### 1. Algorithmic / Constructive.

Canonical form: There exists an algorithm A A that computes f ⁡ ( x ) f(x) , or “object X X can be explicitly constructed.” This category covers theorems providing an explicit or computable method to obtain an object. Example: “There exists a polynomial-time algorithm that computes a maximum matching in any bipartite graph.”

#### 2. Asymptotic / Limit.

Canonical form: As n → ∞ n\to\infty (or another limiting regime), a quantity behaves as described. This category covers theorems describing limiting or asymptotic behavior, including exact limits, asymptotic equivalences ( ∼ \sim ), and big- O O /little- o o estimates. Example: “The number of primes less than x x satisfies π ⁡ ( x ) ∼ x / ln ⁡ x \pi(x)\sim x/\ln x as x → ∞ x\to\infty .”

#### 3. Biconditional / Equivalence.

Canonical form: A ⇔ B A\iff B , or “the following are equivalent.” This category covers theorems asserting that two (or more) conditions are logically equivalent. The theorem may present the equivalence as a single biconditional or as a list of mutually equivalent statements. Example: “A ring R R is Noetherian if and only if every ideal of R R is finitely generated.”

#### 4. Classification / Bijection.

Canonical form: There is a bijection between X X and Y Y , or “objects of type A A are completely classified by objects of type B B .” This category covers theorems establishing a one-to-one correspondence or a complete classification between two classes of mathematical objects. Example: “Finite simple groups are classified into cyclic groups of prime order, alternating groups, groups of Lie type, and 26 26 sporadic groups.”

“yields a both computational and much explicit perspective.” Under the assumptions of the main theorem, one “easily deduce[s] ker ⁡ ( d ​ 𝒫 B , f k ) = ker ⁡ ( d ​ 𝒫 B , f 1 ) , k ≥ 1 \ker(d\mathcal{P}_{B,f}^{k})=\ker(d\mathcal{P}_{B,f}^{1}),\quad k\geq 1 We record the precise statement as follows. Corollary . Under the assumption of theorem we have ker ⁡ ( d ​ ϕ f ) = ker ⁡ ( d ​ ϕ f 1 ) . \ker(d\phi_{f})=\ker(d\phi_{f}^{1}). For an element g = g Γ ​ ( f ) ⋅ x w ∈ ker ⁡ ( d ​ 𝒫 f 1 ) g=g_{\Gamma}(f)\cdot x^{w}\in\ker(d\mathcal{P}_{f}^{1}) one obtains the distinction ⟨ w , n Γ ⟩ = { 0 ⇔ g ≡ 0 , − 1 ⇔ g ∈ ker ⁡ ( κ f ) , ≤ − 2 exceptional cases, \langle w,n_{\Gamma}\rangle=\begin{cases}0&\Leftrightarrow\ g\equiv 0,\\ -1&\Leftrightarrow\ g\in\ker(\kappa_{f}),\\ \leq-2&\text{exceptional cases,}\end{cases} and also “ ⟨ w , n Γ ′ ⟩ ≥ 0 \langle w,n_{\Gamma^{\prime}}\rangle\geq 0 for Γ ′ ≠ Γ \Gamma^{\prime}\neq\Gamma by the main theorem.” The “last case” ⟨ w , n Γ ⟩ ≤ − 2 \langle w,n_{\Gamma}\rangle\leq-2 “causes Φ f | Im ⁡ κ f \Phi_{f|{\operatorname{Im}\,\kappa_{f}}} to be not injective, which implies in particular that the infinitesimal Torelli theorem (ITT) fails.” For n = 3 n=3 , to rule out the exceptional case and conclude injectivity, the text sketches: “we construct a 3 3 -dimensional empty polytope Q Q with 6 6 vertices,” namely “the convex span of an empty triangle with vertex ( 0 , 0 , 0 ) (0,0,0) and this triangle dilated by w w ,” and then “use a theorem of White on empty 3 3 -simplices to deduce | Q ∩ M | ≥ 7 |Q\cap M|\geq 7 under the assumption ⟨ w , n Γ ⟩ ≤ − 2 \langle w,n_{\Gamma}\rangle\leq-2 , contradiction.”

#### 5. Existence.

Canonical form: ∃ x \exists\,x such that P ⁡ ( x ) P(x) . This category covers theorems guaranteeing that at least one object with a given property exists, without claiming uniqueness. Example: “There exists a continuous, nowhere-differentiable function on [ 0 , 1 ] [0,1] .”

#### 6. Existential–Universal.

Canonical form: ∃ x ​ ∀ y , P ⁡ ( x , y ) \exists\,x\;\forall\,y,\;P(x,y) . This category covers theorems asserting the existence of an object (often a constant, function, or parameter) that “works” uniformly for all elements of a given class. The existential quantifier precedes the universal one. Example: “There exists a constant C > 0 C>0 such that for all f ∈ L 2 ​ ( ℝ ) f\in L^{2}(\mathbb{R}) , ‖ f ‖ ∞ ≤ C ​ ‖ f ‖ H 1 \|f\|_{\infty}\leq C\,\|f\|_{H^{1}} .”

#### 7. Implication.

Canonical form: A ⟹ B A\implies B , or “if P P holds, then Q Q holds.” This category covers theorems in which a set of hypotheses implies a specific conclusion, without asserting the converse. Example: “If f f is a continuous function on a closed interval [ a , b ] [a,b] , then f f is uniformly continuous on [ a , b ] [a,b] .”

#### 8. Independence / Consistency.

Canonical form: T ⊬ P T\not\vdash P and T ⊬ ¬ P T\not\vdash\neg P , or “statement P P is independent of axiom system T T .” This category covers theorems expressing a meta-mathematical statement that a proposition cannot be proved or refuted from given axioms. Example: “The Continuum Hypothesis is independent of ZFC.”

#### 9. Inequality / Bound.

Canonical form: f ⁡ ( x ) ≤ g ⁡ ( x ) f(x)\leq g(x) (or ≥ \geq , < < , > > ), holding universally. This category covers theorems providing a quantitative estimate, such as a uniform bound, norm inequality, or comparison between quantities. Example: “For all f ∈ L 1 ​ ( ℝ ) ∩ L 2 ​ ( ℝ ) f\in L^{1}(\mathbb{R})\cap L^{2}(\mathbb{R}) , ‖ f ^ ‖ 2 = ‖ f ‖ 2 \|\hat{f}\|_{2}=\|f\|_{2} .”

#### 10. Nonexistence.

Canonical form: ∄ x \not\exists\,x such that P ⁡ ( x ) P(x) (or equivalently, ∀ x , ¬ P ⁡ ( x ) \forall\,x,\;\neg P(x) ). This category covers theorems asserting that no object satisfies a given property. Example: “There does not exist a rational number whose square is 2 2 .”

#### 11. Uniqueness.

Canonical form: ∃ ! x \exists!\,x such that P ⁡ ( x ) P(x) . This category covers theorems asserting both existence and uniqueness of an object satisfying a given property. Example: “For every positive definite matrix A A , there exists a unique positive definite matrix B B such that B 2 = A B^{2}=A .”

#### 12. Universal.

Canonical form: ∀ x , P ⁡ ( x ) \forall\,x,\;P(x) . This category covers theorems asserting that a property holds for every object in a specified class. Example: “Every finite-dimensional real vector space admits an inner product.”

#### 13. Universal–Existential.

Canonical form: ∀ x ​ ∃ y , P ⁡ ( x , y ) \forall\,x\;\exists\,y,\;P(x,y) . This category covers theorems asserting that for every object in a class, there exists an associated object satisfying a property. The existential witness may depend on the universally quantified variable. Example: “For every ε > 0 \varepsilon>0 , there exists δ > 0 \delta>0 such that | f ⁡ ( x ) − f ⁡ ( a ) | < ε |f(x)-f(a)|<\varepsilon whenever | x − a | < δ |x-a|<\delta .”

## Appendix D Benchmark Composition Across Construction Stages