Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics

# Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics
Source: [https://arxiv.org/html/2607.06820](https://arxiv.org/html/2607.06820)
###### Abstract

Recent advances in AI for Mathematics have focused largely on autoformalization and theorem proving, leaving the role of Computer Algebra Systems \(CAS\) in agentic LLM workflows underexplored\. We propose a ReAct\-style agentic setup that combines LLM reasoning with verifiable feedback from SageMath, together with Context7 for the up\-to\-date documentation\. We evaluate this agentic setup across frontier models for solving research\-level mathematical problems from the RealMath benchmark in a setting that emulates a computational\-mathematics research loop\. We also propose a refinement to the RealMath benchmark by introducing a multi\-step post\-processing procedure and a multi\-stage validation pipeline, both of which improve the quality and reliability of the extracted problem set\. Our experiments reveal substantial performance gains from SageMath access across all evaluated models on \+9\.7 pp on average, the gains range from 1\.5 pp to 27\.8 pp and narrow the gap between open\-weight and closed models\. Qwen 3\.7\-Max benefits from SageMath the most, while GPT\-5\.5 achieves the highest solve rate of75\.2%75\.2\\%and the lowest token usage among tool\-enabled configurations\. Our findings suggest that CAS\-augmented agents represent a promising direction for assisting mathematicians in computational exploration, and we believe that this work is a step towards automated conjecture discovery\. The project repository is available online\.111[https://github\.com/Snopoff/Evaluating\-SageMath\-Augmented\-LLM\-Agents\-for\-Computational\-and\-Experimental\-Mathematics](https://github.com/Snopoff/Evaluating-SageMath-Augmented-LLM-Agents-for-Computational-and-Experimental-Mathematics)

## 1Introduction

Recent progress in LLMs and agentic systems that integrate LLM reasoning with deterministic, verifiable tool backends such as compilers, theorem provers, SAT/SMT solvers, type checkers, and physical simulators has established a new neuro\-symbolic paradigm in which generative reasoning is partially grounded in verifiable feedback\. By coupling LLM reasoning with components that provide ground\-truth signals, this paradigm enables a class of tools capable of automating tasks that previously required substantial expert effort and of producing answers with a level of reliability that purely generative approaches cannot achieve\.

A particularly active application of this paradigm is in mathematics\. Substantial progress has been made on autoformalization, the translation of mathematical statements into the formal programs written in proof\-assistant languages such as Lean, Coq, and Isabelle\(Wuet al\.,[2022](https://arxiv.org/html/2607.06820#bib.bib1)\), as well as on automated theorem proving, where LLM\-based systems guide the search for formal proofs\(Linet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib2)\), attain gold\-medal\-level performance on the 2025 International Mathematical Olympiad with formally verified solutions\(Achimet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib3)\), and and have recently autonomously resolved several open problems from the Erdős collection\(Sothanaphan,[2026](https://arxiv.org/html/2607.06820#bib.bib4); Tsoukalaset al\.,[2026](https://arxiv.org/html/2607.06820#bib.bib56)\)including the well\-known unit\-distance conjecture\(OpenAI,[2026b](https://arxiv.org/html/2607.06820#bib.bib57)\)\. These developments establish the integration of LLMs with formal proof assistants as a promising direction for mathematical reasoning, focused on proving and formalizing already specified statements\.

In many areas of mathematics, Computer Algebra Systems \(CAS\) and symbolic engines are routinely used for hypothesis exploration, candidate validation, and counterexample search\. A common workflow in modern mathematical research, particularly in computational areas such as combinatorial commutative algebra, algebraic combinatorics, graph theory, finite group theory, and related fields, relies heavily on CAS\. Prominent examples include SageMath\(The Sage Developers,[2022](https://arxiv.org/html/2607.06820#bib.bib5)\), Macaulay2\([Grayson and Stillman,](https://arxiv.org/html/2607.06820#bib.bib6)\), GAP\([17](https://arxiv.org/html/2607.06820#bib.bib7)\), Magma\(Bosmaet al\.,[1997](https://arxiv.org/html/2607.06820#bib.bib8)\), PARI/GP\(The PARI Group,[2023](https://arxiv.org/html/2607.06820#bib.bib10)\)and Singular\(Deckeret al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib9)\)which provide computational support for research\-level mathematical problem solving\. Researchers use such systems to discover and prune the conjecture space by iteratively computing examples, identifying patterns, formulating tentative conjectures, and testing them computationally222As famously remarked by V\. I\. Arnold, “mathematics is the part of physics where experiments are cheap\.”\. This workflow are common in computational and experimentally driven areas of mathematics\.

Despite the widespread use of CAS, their integration into LLM\-based systems for mathematical reasoning has received substantially less attention than the integration of formal proof assistants\. In particular, existing work has focused largely on formal proof construction, leaving computational workflows based on symbolic experimentation and executable verification comparatively underexplored\. This gap, together with the recent successes of LLMs in mathematical reasoning, motivates the present study\.

The central question of our work is the following: to what extent does verifiable symbolic feedback improve the performance of frontier LLMs on research\-level mathematics, and does it shape their behavior in agentic setup? To study this effect, we evaluate frontier LLMs within an agentic setup with an access to SageMath that closely emulates a mathematician’s computational workflow\. The proposed setup is particularly relevant for tasks where symbolic computation plays a central role and where core mathematical structures have already been algorithmically formalized within existing software systems\. Our contributions are threefold:

Tool\-use agentic evaluation:we present an empirical study of frontier LLMs in a ReAct\-style agentic setup with multi\-turn access to SageMath together with up\-to\-date documentation retrieval through Context7\. We evaluate how verifiable feedback from a CAS affects model performance on research\-level mathematical problems through a controlled tool\-access ablation\.

Benchmark refinement and evaluation protocol:building on the RealMath benchmark, we curate an evaluation set restricted to numerical and symbolic\-expression answers\. We additionally enrich problem statements with compressed contextual information and introduce an LLM\-assisted normalization pipeline for executable symbolic verification\. We further employ a hybrid validation protocol combining symbolic equivalence checking with LLM\-as\-a\-Judge re\-evaluation\.

Error and behavioral analysis:we complement the quantitative evaluation with an analysis of execution failures, recovery dynamics, and tool\-call traces, highlighting model\-specific patterns in how agents interact with symbolic computation tools\. We also present a case study with a description of the solution strategy used by agent to solve one of the problem\.

## 2Related Work

### 2\.1Autoformalization and Theorem Proving

This subsection situates our work within the broader recent progress in AI4Math, with a focus on autoformalization and automated theorem proving\. The dominant line couples LLMs with formal proof assistants\. Many works evaluate LLMs on competition mathematics and formal proof generation\.MathArena\(Balunović and others,[2025](https://arxiv.org/html/2607.06820#bib.bib20)\)evaluates LLMs on math competitions immediately after they occur to avoid contamination, and introduces a proof\-writing benchmark on which top models score below 25% on USAMO 2025\.PutnamBench\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib23)\)proposes 1,692 task formalizations across Lean 4, Isabelle, Coq\.

Herald\(Gaoet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib11)\)builds a large NL\-to\-Lean 4 corpus by back\-translating Mathlib and trains an autoformalizer reaching 96\.7% accuracy on miniF2F\-test\.AlphaProof\(Google DeepMind AlphaProof and AlphaGeometry teams,[2025](https://arxiv.org/html/2607.06820#bib.bib12)\)combines Lean with AlphaZero\-style RL, and together with the geometry\-specializedAlphaGeometry 2\(Chervonyiet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib13)\)reached silver\-medal performance at IMO 2024\. TheDeepSeek\-Proverline\(Xin and others,[2024](https://arxiv.org/html/2607.06820#bib.bib14); Ren and others,[2025](https://arxiv.org/html/2607.06820#bib.bib15)\)pursued open\-source provers through subgoal decomposition, with V2 reaching 88\.9% on MiniF2F\-test\.Kimina\-Prover\(Wanget al\.,[2025a](https://arxiv.org/html/2607.06820#bib.bib16)\)andSeed\-Prover\(Chenet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib17)\)pushed alternative recipes based on structured reasoning and lemma\-style proofs with iterative Lean feedback\. More recent work has moved beyond standard proof\-search training\.DeepSeekMath\-V2\(Shaoet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib18)\)trains a generator\-verifier pair that rewards reasoning steps, scoring 118/120 on Putnam 2024\. Agentic systems orchestrating LLMs around the Lean compiler have also emerged:AxiomProver\(Axiom Math Team,[2025](https://arxiv.org/html/2607.06820#bib.bib19)\)produced fully verified Lean proofs for all Putnam 2025 tasks\. We refer toWanget al\.\([2025b](https://arxiv.org/html/2607.06820#bib.bib36)\)for a broad survey of LLMs for mathematical reasoning, especially with tool usage\.

### 2\.2Benchmarking AI4Math

#### Research\-level benchmarks\.

A major line of benchmarks targets mathematics drawn from research\-level tasks and literature rather than competitions\.FrontierMath\(Glazer and others,[2024](https://arxiv.org/html/2607.06820#bib.bib25)\)pushes the difficulty ceiling with hundreds of unpublished problems crafted by leading mathematicians, including Terence Tao, spanning many research\-adjacent areas\. By mid\-2026, the best reasoning LLMs reach over 50% on Tiers 1–3 and 25\-40% on Tier 4\(Epoch AI,[2026](https://arxiv.org/html/2607.06820#bib.bib27)\)\.EternalMath\(Ma and others,[2026](https://arxiv.org/html/2607.06820#bib.bib21)\)pursues a fully automated theorem\-grounded pipeline that turns recent papers into executable, verifiable tasks, with the goal of producing a continuously refreshable benchmark\. An especially relevant work isRealMath\(Zhanget al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib26)\), which proposes an automated data\-collection pipeline that extracts research\-level problems from arXiv and Math Stack Exchange and presents them as \(context, question, answer\) triples, with a focus on constructive theorems\. Our work builds on it, we use the computable subset of the dataset extracted by their pipeline, and also propose refinements to the benchmark\.

#### Benchmarks involving symbolic computation\.

The benchmarks closest to our work involve symbolic or CAS\-augmented evaluation\.IMProofBench\(Schmittet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib28)\)evaluates LLMs in a multi\-turn agentic setup with tools \(Python, SageMath, Bash, web search\) on 39 research\-level proof\-generation problems, where the best model, GPT\-5, produces a fully correct proof for 22% of problems\. In contrast to our setup,IMProofBenchdoes not isolate the effect of tool access through a controlled tool\-free ablation, and its problem set remains private\.ASyMOB\(Shalytet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib29)\)comprises 17092 symbolic tasks spanning integration, simplification, limits, and differential equations, with the measuring performance degradation under symbolic perturbations and exposing drops of up to 70%, they used SymPy for answer validation\.IntegralBench\(Tanget al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib30)\)narrows the scope to 317 graduate\-level definite integral problems with symbolic and numerical ground truth, illustrating how tight, domain\-restricted benchmarks can isolate specific failure modes\.

### 2\.3Tool\-Augmented Agents for Mathematical Discovery and Reasoning

A complementary line of works combines agents with external symbolic and computational tools for the conjecture\-space discovery and pruning in mathematical reasoning\.FunSearch\(Romera\-Paredeset al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib31)\)and its successorAlphaEvolve\(Novikovet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib33)\)traverse the hypothesis space by evolving Python programs scored by a deterministic Python\-based evaluator:FunSearchproduced new lower bounds on the cap\-set problem, andAlphaEvolvegeneralizes the loop to whole\-codebase evolution and reports new SOTA constructions, including an improved scheme for4×44\\times 4complex matrix multiplication\. Early work in this direction includes\(Chuharskiet al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib32)\), who sample conjectures about the solubilizer in group theory from LLMs and prune the conjecture space via counterexamples generated by GAP\. TheToRA\(Gouet al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib34)\)trains open\-weight models to interleave reasoning with SymPy tool, substantially improving performance on competition\-level benchmarks\.MathSensei\(Daset al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib35)\)combines a knowledge retriever, a Python program generator and executor, and the Wolfram\-Alpha in a planner\-driven pipeline, and ablates these tools on the MATH benchmark to isolate their complementary effects\. We generalize this pattern to a general\-purpose CAS\-based tool and evaluate it on mathematical problem solving\.

## 3Experimental setup

We evaluate each model under two matched conditions: a tool\-free baseline, in which the model solves each problem using direct reasoning alone, and a tool\-augmented agentic setting, in which it can iteratively query SageMath and Context7\. Apart from tool access and the corresponding system prompt, the base model and problem set are held fixed\. This design isolates the effect of verifiable symbolic feedback on performance in research\-level mathematics\. We evaluate on a curated set of 133 problems from the RealMath benchmark and validate model outputs using a multi\-stage protocol that combines symbolic equivalence checking with an LLM\-as\-a\-judge stage\. The system prompts for both pipelines are provided in Appendices[F\.1](https://arxiv.org/html/2607.06820#A6.SS1)and[F\.2](https://arxiv.org/html/2607.06820#A6.SS2)\.

### 3\.1Evaluation Dataset

We extracted a curated subset of 133 problems by performing additional processing steps, multi\-stage filtering, and sampling from the RealMath benchmark\(Zhanget al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib26)\), a dataset of research\-level mathematical problems that is directly derived from the contemporary literature\. The additional steps are crucial, since we focus on executable mathematical reasoning and thus require problems to have algorithmically verifiable solutions\. However, RealMath was developed as a Q&A benchmark, in which theanswerfield is represented as plain LaTeX text, which prevents direct automatic comparison\. Moreover, it was collected without assessing the computational perspective of the problems, thus it might contain problems that are not directly suitable for symbolic computation within the SageMath framework\.

We therefore construct the final evaluation suite through the following multi\-stage pipeline \(see Appendix[A\.2](https://arxiv.org/html/2607.06820#A1.SS2)for the full details regarding the dataset construction, filtering criteria, and annotation prompts\):

1. 1\.We retain only those problems that can be normalized into SymPy objects that are suitable for automatic verification\.
2. 2\.We use LLM\-assisted filtering to identify problems for which the symbolic experimentation or computational verification is feasible within SageMath\.
3. 3\.We sample from the filtered pool and extend it with the problems from underrepresented arXiv categories\.

We also augment problem statements with the definitions and auxiliary statements that are crucial to interpret the question\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/x1.png)Figure 1:Overview of the proposed evaluation framework for executable mathematical reasoning\. A ReAct\-style LLM agent interacts with SageMath and Context7 through iterative tool use, receives verifiable feedback from symbolic computation, and produces a final answer validated through symbolic equivalence checking and an auxiliary LLM\-as\-a\-Judge stage\.
### 3\.2Agentic Setup

The agentic pipeline is organized to emulate the workflow of a working mathematician\. In the tool\-free setting, the model relies on its internal knowledge resources and reasoning capabilities\. However, the reasoning aimed to tackle a complicated mathematical problem might require intermediate computational steps with verifiable feedback\. It would allow the agent to refine its reasoning through iterative experimentation and explore the hypothesis space more efficiently\. We implement this pipeline by wrapping the models in a ReAct\-style multi\-turn loop, in which the agent repeatedly reasons about the current state, invokes an external tool, and incorporates the returned observation into the next turn\. The tool interface provides access to SageMath for symbolic and computational mathematics and to Context7 for retrieving relevant library documentation\.

#### SageMath\.

SageMath \(Sage\) is a widely used open\-source computer algebra system that provides a unified Python\-based interface to a broad collection of mathematical software systems, including GAP, Singular, and PARI/GP\. It supports symbolic computation, algebraic manipulation, and numerical experimentation, and provides extensive functionality for polynomial ideals, graph\-theoretic computations, number theory, and related areas\. In our pipeline, the agent can generate Sage code snippets, execute them in an isolated sandbox \(see Appendix[A\.1](https://arxiv.org/html/2607.06820#A1.SS1.SSS0.Px1)\), observe the returned output, and iterate on its hypotheses\.

#### Context7\.

Context7\(Upstash Team,[2026](https://arxiv.org/html/2607.06820#bib.bib38)\)is a project that provides access to up\-to\-date documentation and code examples from official sources\. The agent is given access to this tool to reduce hallucinations about modules, paths, and outdated API signatures, as the models may rely on outdated information about SageMath APIs acquired during pretraining\. Providing an access to that tool, we mitigate the possibility that models might not know how to write Sage code, focusing on the model’s capability for executable, verifiable thinking and its ability to refine candidate solutions\.

### 3\.3Experimental protocol

We evaluate the agentic setup by comparing it with a tool\-free baseline to measure the impact of tool integration on performance\. To ensure a controlled ablation, we keep the underlying model and problem instances fixed across conditions, only tool access and the associated system prompt differ\. In the agentic setting, we impose a hard cap of 15 tool calls per problem\. We also require the model to return SymPy\-parsable output, since the evaluation is based on symbolic verification\.

#### Tool\-free setting\.

The tool\-free pipeline consists of direct reasoning performed by a model without external feedback\. It allows us to ablate the model’s internal capabilities for solving research\-level mathematical problems\. This setting is similar to standard direct\-answer evaluation used in the original RealMath benchmark\.

#### Models and evaluation scope\.

For the base models, we evaluate Claude Opus 4\.7, Claude Opus 4\.8, Sonnet\-5\(Anthropic,[2026](https://arxiv.org/html/2607.06820#bib.bib40)\), DeepSeek\-V3\.2\(DeepSeek\-AI,[2025](https://arxiv.org/html/2607.06820#bib.bib41)\), DeepSeek\-V4\-Flash, DeepSeek\-V4\-Pro\(Xuet al\.,[2026](https://arxiv.org/html/2607.06820#bib.bib43)\), Qwen 3\.7\-Max\(Qwen,[2026](https://arxiv.org/html/2607.06820#bib.bib48)\), GLM 5\.2\(GLM\-5\-Team,[2026](https://arxiv.org/html/2607.06820#bib.bib49)\), Kimi 2\.7\(Moonshot AI,[2026](https://arxiv.org/html/2607.06820#bib.bib51)\), MiniMax\-M3\(MiniMax,[2026](https://arxiv.org/html/2607.06820#bib.bib52)\), GPT\-5\.5\(OpenAI,[2026a](https://arxiv.org/html/2607.06820#bib.bib44)\), Gemini\-3\.5\-Flash\(Google DeepMind,[2026b](https://arxiv.org/html/2607.06820#bib.bib45)\), Gemini\-3\.1\-Pro\-preview\(Google DeepMind,[2026a](https://arxiv.org/html/2607.06820#bib.bib46)\), Grok 4\.3\(xAI,[2026](https://arxiv.org/html/2607.06820#bib.bib47)\)accessed via APIs\. We also evaluate Fugu\-Ultra\(SakanaAI,[2026](https://arxiv.org/html/2607.06820#bib.bib55)\), noting that it is a multi\-agent orchestration system rather than a single LLM\. Each model was evaluated in both setups on 133 problems, yielding more than 3,990 independent runs \(15 models×\\times2 setups×\\times133 problems\)\.

### 3\.4Evaluation pipeline

Validating the equivalence of symbolic mathematical expressions is substantially more challenging than validating numerical answers, since structurally different expressions may still be mathematically equivalent\. Prior benchmarks address this issue either through symbolic equivalence procedures\(Shalytet al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib29)\)or through LLM\-based judging\(Tsoukalaset al\.,[2024](https://arxiv.org/html/2607.06820#bib.bib23); Zhanget al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib26)\)\. We combine both approaches in a multi\-stage evaluation pipeline, as symbolic simplification is not exhaustive and may incorrectly reject mathematically equivalent expressions\.

#### Symbolic validator\.

The first stage compares the SymPy\-parsable output produced by the model against the ground\-truth answer represented in the same format\. Expressions are parsed into SymPy objects and their difference is simplified symbolically\. If the resulting expression simplifies to zero, the prediction is considered correct\. For multi\-component answers, outputs are compared component\-wise\.

#### LLM\-as\-a\-Judge validator\.

Cases rejected by the symbolic validator are not necessarily incorrect\. For such cases, we employ a second\-stage evaluation procedure based on three frontier LLM judges: Claude Opus 4\.7, GPT\-5\.5, and Gemini 3\.5 Flash333The judge prompt is shared across models and provided in Appendix[F\.5](https://arxiv.org/html/2607.06820#A6.SS5)\.\. Each model independently produces a verdict together with a short justification, and the final decision is obtained through majority voting\. In addition, we manually inspect30%30\\%of the cases reaching this stage and treat the resulting human annotations as ground truth\.

#### Evaluation metric\.

We report solve rate: the fraction of problems whose final answer is accepted by the validation pipeline\. Predictions are accepted either by symbolic equivalence checking or, when this is inconclusive, by majority vote among three LLM judges\. Solve rate estimates are accompanied by 95% Wilson score confidence intervals\.

## 4Results and discussion

### 4\.1Main results

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/bars_main.png)Figure 2:Solve rate across models and evaluation setups\. Solve rates for each model without tools and with the tool\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/scatterplot_main.png)Figure 3:Solve rates against mean token usage per problem on a logarithmic axis, showing the accuracy\-cost trade\-off\.We evaluated fifteen models in both tool\-free and tool\-augmented settings; the main results are shown in Figure[2](https://arxiv.org/html/2607.06820#S4.F2), error bars show 95% Wilson confidence intervals\. Tool access improved the solve rate of every model, by\+9\.7\+9\.7pp on average, although the magnitude of the gains varied substantially across architectures\. The largest improvements were concentrated among open\-weight models: Qwen\-3\.7\-Max improved from42\.1%42\.1\\%to69\.9%69\.9\\%\(\+27\.8\+27\.8pp\), MiniMax from38\.3%38\.3\\%to55\.6%55\.6\\%\(\+17\.3\+17\.3pp\), and DeepSeek 3\.2 from33\.1%33\.1\\%to48\.9%48\.9\\%\(\+15\.8\+15\.8pp\)\. Closed frontier models gained more moderately from stronger baselines, and the two best results in the study belong to this group: GPT\-5\.5 improved from67\.7%67\.7\\%to75\.2%75\.2\\%and Opus 4\.8 from66\.2%66\.2\\%to73\.7%73\.7\\%\(\+7\.5\+7\.5pp each\)\. Fugu\-Ultra, a multi\-agent orchestration system rather than a single LLM, matches Opus 4\.7 at72\.9%72\.9\\%\(\+6\.0\+6\.0pp\)\. The leading open\-weight models with tool access reach the tool\-free performance of the strongest closed models\. This relationship between a low baseline and a large gain is not universal, however: Grok 4\.3, whose baseline is close to Qwen’s \(39\.1%39\.1\\%\), gained only\+3\.8\+3\.8pp, and Kimi\+1\.5\+1\.5pp despite issuing the second\-largest number of tool calls in the entire study \(1,4211\{,\}421\), in both cases because the potential benefit of the CAS was descried by incorrect tool interaction \(Section[4\.2](https://arxiv.org/html/2607.06820#S4.SS2)\)\.

Finding 1\.Tool access improves all models, but the gains are non\-uniform, ranging from\+1\.5\+1\.5pp \(Kimi\) to\+27\.8\+27\.8pp \(Qwen\)\. Open\-weight models gain\+15\.3\+15\.3pp on average, more than twice the\+6\.5\+6\.5pp of closed frontier models, a difference partly attributable to their weaker tool\-free baselines\. CAS access narrows the gap between open and closed models\.

#### Token usage efficiency\.

Figure[3](https://arxiv.org/html/2607.06820#S4.F3)shows a substantial efficiency gap between tool\-augmented configurations\. Tool access increases mean token consumption by factors ranging from4\.5×4\.5\\times\(Fugu\-Ultra\) to99×99\\times\(Qwen\), but the additional compute does not yield a proportional increase in accuracy: tool\-enabled configurations span roughly3434k–556556k tokens per problem at solve rates between42\.1%42\.1\\%and75\.2%75\.2\\%\.

Finding 2\.Higher token expenditure does not translate into higher accuracy\. GPT\-5\.5 is the most efficient configuration, achieving the highest solve rate \(75\.2%75\.2\\%\) at the lowest token usage, whereas MiniMax spends16×16\\timesmore tokens per problem for a19\.619\.6pp lower solve rate, meaning that token budget is not the bottleneck in mathematical problem solving

The largest multipliers \(5454–99×99\\times; Qwen, DeepSeek 3\.2, and DeepSeek V4\-flash\) belong to the models with the lowest tool\-free token usage \(2\.32\.3–2\.52\.5k tokens per problem\), so the multiplier largely reflects the terseness of the tool\-free model rather than the cost of the agentic loop itself\. GPT\-5\.5 attains the highest solve rate \(75\.2%75\.2\\%\) at the lowest token usage \(3434k tokens per problem\) among all tool\-enabled configurations, dominating every other model on both axes simultaneously; the nearest competitors are Fugu\-Ultra \(72\.9%72\.9\\%at7070k\), Opus 4\.7 \(72\.9%72\.9\\%at9797k\), and Opus 4\.8, which trades a higher solve rate \(73\.7%73\.7\\%\) for a larger budget \(119119k\)\. At the opposite end, MiniMax consumes556556k tokens per problem, a16×16\\timesoverhead relative to GPT\-5\.5, while solving19\.619\.6pp fewer problems\. Some models from the same provider tend to occupy nearby regions of the accuracy\-cost plane, apparently reflecting shared post\-training or tool\-use policies within a family\. Within the Gemini family, the Pro model is both more accurate and cheaper under tool access than Flash\. Low consumption is not by itself a sign of efficiency: Grok 4\.3 is the second\-cheapest agent \(3939k\), but only because its degenerate one\-liner code \(Section[4\.2](https://arxiv.org/html/2607.06820#S4.SS2)\) produces little output\. Kimi shows the worst trade\-off in the study, spending205205k tokens per problem for a gain of\+1\.5\+1\.5pp\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/token_usage.png)Figure 4:Mean tokens per problem on the common all\-solved set in both tool\-free and tool\-enabled setups\.
#### Model efficiency on commonly solved problems\.

In practice, one often faces the choice of which model to deploy when a problem is relatively easy and the goal is to solve it at minimal cost\. Here we therefore focus to the subset of problems solved by model within a given setup, accuracy is tied on this set by construction, so models are ranked purely by mean tokens per solved problem \(Figure[4](https://arxiv.org/html/2607.06820#S4.F4)\)\. Easiness is relative to the setup: the tool\-augmented common set is larger \(3030vs\.1515problems\) and includes problems that only become universally solvable with CAS access\. The two setups give opposite recommendations\. Without tools, the cheapest configurations are open\-weight: DeepSeek 3\.2 \(2\.22\.2k tokens\), Qwen \(2\.32\.3k\), and DeepSeek V4\-flash \(2\.62\.6k\)\. With tools, the top of the ranking is occupied entirely by closed models, GPT\-5\.5 \(2020k\), Opus 4\.7 \(2222k\), and Opus 4\.8 \(2929k\) while the tool\-free leaders drop to the bottom: DeepSeek\-V3\.2 falls to rank 11 \(9999k\) and Qwen to rank 14 \(131131k\)\. Therefore direct answering is thus not predictive of an efficient from the point of token usage agentic behavior\. However, for relatively easy problems, a better strategy would be to first try an open\-weight model such as DeepSeek before get expensive closed models\.

Finding 3\.On easy problems solved by every model in the tool\-free setup, the open\-weight DeepSeek and Qwen models are the most token\-efficient\. On problems solved by every model in the tool\-augmented setup, the ranking inverts: closed models are the most efficient, while open\-weight models fall to the bottom\.

#### Effect of answer type\.

The dataset contains7373expression\-typed and6060numerical\-typed answers\. In the tool\-free setting, thirteen of fifteen models perform substantially better on numerical problems than on expressions, with the largest gaps for the two light DeepSeek models, Qwen, MiniMax, and Grok 4\.3 \(2626–3333pp\); GPT\-5\.5 is the sole exception with a slightly higher expression score \(68%68\\%vs\.67%67\\%\)\. Tool access narrows this disparity where it is widest: Qwen gains\+36\+36pp on expressions \(27%→63%27\\%\\to 63\\%\) and DeepSeek 3\.2\+18\+18pp, whereas models already strong on expressions \(GPT\-5\.5, Fugu\-Ultra, Gemini 3\.1 Pro\) gain only11–55pp\. Overall, symbolic computation benefits most the models weakest at manipulating symbolic expressions\. Figure[11](https://arxiv.org/html/2607.06820#A2.F11)reports solve rates separately for expression\-type and numerical problems under both setups\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/solve_coverage.png)Figure 5:Problem\-level solve coverage across configurations\. Each bar shows number of problems solved byNNconfigurations\.
#### Problem solve coverage\.

Figure[5](https://arxiv.org/html/2607.06820#S4.F5)shows how many problems are solved by exactlyNNof the3030evaluated configurations\. We observed that118118problems were solved by at least one tool\-augmented agent,122122by at least one configuration overall, and1111problems \(8%8\\%\) were solved by no configuration\. Four problems were solved only in the tool\-free setting: for these items the agentic loop destroyed solutions that pure reasoning had produced\. Ten problems were solved by exactly one configuration, distributed across eight different models \(Fugu\-Ultra and GLM solved 2\)\. Universally unsolved problems require deep theoretical insight beyond CAS\-based feedback reasoning\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/math_category.png)Figure 6:Solve rate by arXiv category with and without tools\. Cells show solve rate and solved/total counts\.
#### Solve rate by mathematical category\.

We further examine the effect of the agentic setup on performance across arXiv categories \(Figure[6](https://arxiv.org/html/2607.06820#S4.F6)\)\. The largest mean gain is observed in combinatorics \(\+18\.7\+18\.7pp averaged over models,41%→60%41\\%\\to 60\\%\), followed by classical analysis \(\+12\.0\+12\.0pp\) and rings and algebras \(\+10\.7\+10\.7pp\), consistent with the mature SageMath support for these areas\. Number theory improves only moderately \(\+4\.5\+4\.5pp\) from an already strong baseline of70%70\\%, probability is nearly saturated, almost every model solves the same8/98/9problems in both setups, and analysis of PDEs benefits least \(\+2\.2\+2\.2pp\)\. Group theory remains the hardest large category: its\+10\.4\+10\.4pp gain comes from weaker models catching up rather than from the closed frontier models improving, no model exceeds44%44\\%, and GPT\-5\.5 is the only case where tool access lowers a category score\. Although group theory is well covered in SageMath, including the extensive functionality of the GAP, the experimental results show no substantial benefit for the agentic setup with SageMath tool\. Algebraic topology \(also computationally hard area\) exhibits the strongest divergence between models: the mean tool\-augmented solve rate is23%23\\%, yet Fugu\-Ultra, GPT\-5\.5, and Opus 4\.7 solve more than half of these problems while 7 LLMs remain at0%0\\%\.

Tool\-call intensity doesn’t track success \(Figure[9](https://arxiv.org/html/2607.06820#A2.F9)in Appendix\)\. The mean number of Sage calls per problem is weakly correlated with the solve rate\. For example, probability \(86%86\\%solve rate\), requires the fewest calls \(4\.44\.4\), but group theory \(9\.19\.1calls\) and algebraic topology \(8\.98\.9calls\) tend to provoke long tool call trace without effect\.

#### Cross\-model agreement\.

Mean pairwise per\-problem agreement rises from74\.5%74\.5\\%in the tool\-free setting to79\.1%79\.1\\%with tools: shared CAS access homogenizes the models by pulling them all toward the common subset of computationally reachable problems, and the family\-level agreement clusters \(DeepSeek, Gemini\) visible in the tool\-free matrix tighten further\. The highest pairwise agreements are observed between Opus 4\.7 and Opus 4\.8 \(88%88\\%tool\-free,93%93\\%with tools the largest value in the study\)\. The agreement between GPT\-5\.5 and Fugu\-Ultra \(90%90\\%in both settings\) may indicate that the orchestration system relies on a model whose behavior is close to GPT\-5\.5, although reliably establishing this would require a more extensive analysis\.

#### Sage usage statistics\.

Classification of the Sage function calls made by agents reveals consistent usage and is demonstrated at the Figure[16](https://arxiv.org/html/2607.06820#A3.F16)\(see also Appendix[C](https://arxiv.org/html/2607.06820#A3)for the detailed analysis\)\. This figure demonstrates that the most frequenst operation wasarith\.gcd, with 1274 traces, 1042 of them inmath\.NT\. Enumerative functions are also frequently used:itertools\.combinationsappears 1041 times, mainly inmath\.CO,math\.GR, andmath\.SG, whileitertools\.permutationsis highly concentrated inmath\.CO\. Linear algebra routines such asmatrix\.rank,matrix\.determinant,modules\.dimension, andmodules\.basisare more broadly distributed, with especially high usage inmath\.RA,math\.AG,math\.AT,math\.CA, andmath\.SG, suggesting that many algebraic and representation\-theoretic problems are reduced to rank, basis, dimension, or kernel computations\. Similarly, symbolic methods such assymbolic\.solve,symbolic\.expand,symbolic\.simplify, andsymbolic\.simplify\_fullare also broadly distributed, less domain\-specific, and often appear as intermediate steps for solving equations, expanding identities, comparing coefficients, or simplifying expressions before producing a final answer\.

#### Tool\-call volume\.

Overall tool\-call statistics \(see Figure[12](https://arxiv.org/html/2607.06820#A2.F12)in Appendix\) reports the total number of Sage and Context7 calls per model\. Sage usage spans a3\.6×3\.6\\timesrange, from435435calls \(Opus 4\.7\) to1,5491\{,\}549\(DeepSeek 3\.2\), and is inversely related to solve rate: the four heaviest users \(the DeepSeek family and Kimi,1,2851\{,\}285–1,5491\{,\}549calls\) all place in the lower half of the ranking, whereas the top\-scoring GPT\-5\.5 and both Opus models issue fewer than510510calls each\. Documentation retrieval Context7 tool have been used by only DeepSeek 3\.2 \(311311\) and DeepSeek V4\-flash \(446446\), while 11 models used at most ten each\.

Finding 4\.Only a few open\-weight models actively query the Context7 tool, but most models barely use it, indicating either sufficient knowledge of the SageMath or alternative verification strategies such as probing a function’s behavior via directly execution\.

#### Validation stage analysis\.

The hybrid validation pipeline behaved consistently across both evaluation settings\. The symbolic checker directly accepted39\.2%39\.2\\%of all3,9903\{,\}990predictions; the remaining60\.8%60\.8\\%were routed to the LLM\-judge panel, which overturned the rejection in30\.8%30\.8\\%of these cases \(747747answers\) and confirmed it in the rest\. These recoveries overwhelmingly correspond to mathematically equivalent answers expressed in different canonical forms, so the judge acts primarily as a recovery mechanism for symbolic\-verification failures rather than as an independent source of supervision\. The panel itself is highly consistent:97\.2%97\.2\\%of its verdicts are unanimous across the three judges\. Taking the final pipeline verdict as reference, the symbolic checker alone already produces the correct decision in81\.3%81\.3\\%of cases\. A more robust symbolic checker, one that handles a wider range of equivalent forms, could therefore close most of the remaining gap and enable fully deterministic validation of numerical and expression\-typed answers, removing the need for LLM judges\.

### 4\.2Error analysis and tool\-use traces

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/turn_distr_tools.png)Figure 7:Distribution of agentic trace lengths across models\. Each bar shows the number of problems for which the agent terminated after a given number of tool calls\.#### Sage execution failures\.

We define a tool\-execution error as an unsuccessful call of a Sage tool: generated code either raises an exception, exceeds the4545\-second wall\-clock limit, or crashes the SageMath process below the Python layer\. Here we analyze the types of errors raised during the execution of Sage snippets\. Table[1](https://arxiv.org/html/2607.06820#S4.T1)summarizes failed Sage calls by Python exception type, 4 dominant exception classes and the remaining classes \(ValueError,IndexError,RuntimeError,ImportError\) are grouped as Other\. Aditional visualizations are provided in Appendix \(Figure[13](https://arxiv.org/html/2607.06820#A2.F13)\)\. Exception volumes differ by more than an order of magnitude, from3131–3838\(Opus 4\.7, Opus 4\.8, GPT\-5\.5, Fugu\-Ultra\) to459459for DeepSeek 3\.2\. Four exception classes, namelyTypeError,NameError,AttributeError, andSyntaxError, account for87%87\\%of all exceptions\.NameErrors \(664664in total, of which151151from DeepSeek 3\.2 and122122from Kimi\) typically arise because each Sage call executes in a fresh interpreter and variables do not persist across calls\. Opus 4\.7 and Fugu\-Ultra produce0NameErrors and Opus 4\.8 a single one, i\.e\., these models essentially never lose interpreter state\.SyntaxErroris almost exclusively a Grok 4\.3 phenomenon \(248248of336336instances\): the model persistently emits semicolon\-joined one\-liners with inlineforstatements\. The dominant failure mode is insteadTypeError\(786786\), reflecting incorrect handling of Sage’s object system rather than of Python syntax\. The four best models show similar exception profiles: roughly half of their few failures areTypeErrors, mainly from Sage\-specific coercions\.

Table 1:Failed Sage calls by exception type across for 4 dominant exception classes\.
#### Recovery after failed calls\.

The ability to recover after a failed tool call varies more than any other agentic statistic, see Figure[14](https://arxiv.org/html/2607.06820#A2.F14)\. The probability that the next Sage call succeeds after a failure ranges from16%16\\%for Sonnet and26%26\\%for GLM, whose timeout failures recur because the models retry variants of the same infeasible computation, through32%32\\%for Grok 4\.3, whose repeated parse failures prevent it from converting feedback into working code, up to6969–77%77\\%for Opus 4\.7, Gemini 3\.5 Flash, DeepSeek V4\-Pro, Fugu\-Ultra, and GPT\-5\.5\. Opus 4\.8 is a notable outlier: it recovers in only38%38\\%of cases, yet fails so rarely \(157157post\-failure situations, the second\-fewest in the study\) that the weak recovery barely affects its overall performance\. This6161pp spread, contrasted with the far narrower spread in raw failure rates, indicates that the agents differ by the ability to revise their strategy after receiving tool feedback\.

#### Tool\-use depth\.

Figure[7](https://arxiv.org/html/2607.06820#S4.F7)shows the distribution of agentic turn counts across models, where a turn is one round of agent–tool interaction; the final bin extends to1616because a full run comprises up to1515tool calls plus one turn for submitting the final answer\. The distributions are strongly polarized rather than unimodal: most runs either terminate within the first33–44rounds or require the full budget of1515tool calls, while the intermediate55–1212region is sparsely populated for nearly all models\. The strongest models concentrate in the first mode: Opus 4\.7 \(median33, mean4\.84\.8, the shortest in the study\), GPT\-5\.5, Opus 4\.8, and Fugu\-Ultra \(medians33–44\) complete more than half of all problems within four rounds\. At the opposite pole, DeepSeek 3\.2 and DeepSeek V4\-flash reach the final bin on9090and8989of133133problems respectively, and Kimi on8686; their mean turn counts \(1313–1414\) approach the budget itself\. The remaining models fall between the two poles: Gemini 3\.5 Flash and GLM gravitate toward the final bin \(5151and6363problems\) without saturating it, Qwen and MiniMax show the flattest distributions \(medians88–1010\), and Gemini 3\.1 Pro combines a pronounced peak at33–44rounds with a heavy tail \(median99\)\. The two modes differ sharply in outcome: the short\-trace group contains the four highest solve rates in the study, whereas the budget\-saturating group occupies the lower half of the ranking\. This may indicate that strong LLMs arrive at the answer quickly and spend only a few tool calls verifying it, whereas weaker models rely on many tool turns to search for a solution, and a long computation is predominantly a symptom of failure rather than a path to one\.

Finding 5\.Agentic runs are bimodal: a model either solves the problem within the first33–44tool interactions or exhausts the entire tool budget, and intermediate trace lengths are rare\. The strongest models \(Opus 4\.7, GPT\-5\.5, Opus 4\.8, Fugu\-Ultra; median33–44turns\) in the first mode, using tools mainly to verify an answer reached by reasoning, whereas other agents \(DeepSeek, Kimi, exhausting the budget on8686–9090of133133problems\) search for a solution through computation, converting effort into marginal gains\.

#### Trace\-level behavior\.

To inspect agent\-tool interaction beyond aggregate error counts, we visualize tool\-call traces as tiled sequences, where each tile denotes a successful call, an execution error, a timeout, or another tool response, see Figure[15](https://arxiv.org/html/2607.06820#A2.F15)\. The tiled trace summaries show that models differ not only in final accuracy, but also in how efficiently they use the tools\. GPT\-5\.5 and Fugu\-Ultra have the cleanest trace profiles: most selected problems are resolved with a single successful Sage call, and failures, when they occur, are usually isolated rather than repeated\. Claude Opus 4\.8 is similarly concise on many problems, although a small number of timeout\-heavy traces create longer failure runs\. Gemini 3\.1 Pro and Qwen 3\.7 Max occupy a middle regime, often producing extended sequences of successful checks mixed with occasional code errors or timeouts, suggesting more iterative empirical probing\. DeepSeek v4\-Pro and Kimi K2\.7 use the largest tool budgets, with many traces stretching close to the plotted limit; DeepSeek’s long traces are often dominated by repeated successful calls, whereas Kimi’s contain dense mixtures of code errors and timeouts\. Grok 4\.3 exhibits a more polarized pattern, alternating between very short successful traces and long clusters of code errors\. Overall, the visualization suggests that strong tool use depends not just on avoiding errors, but on recovering from them quickly and pivoting away from unproductive computational strategies\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/execution_time.png)Figure 8:Mean SageMath sandbox runtime per problem in the tool\-augmented setting, with the sandbox share of total solve time\.
#### Sage execution time\.

Figure[8](https://arxiv.org/html/2607.06820#S4.F8)reports the mean pure SageMath sandbox runtime per problem, i\.e\., the cumulative execution time of Sage calls, excluding model inference\. The spread is more than fivefold, from2929s \(Opus 4\.7\) and3737s \(GPT\-5\.5\) to142142–161161s for Sonnet, GLM, and Kimi, the three models whose failure profiles are dominated by timeouts: their long sandbox times reflect computationally infeasible enumerations running until the wall\-clock limit rather than productive computation\. The share of total solve time spent inside the sandbox varies independently of the absolute runtime: for most models Sage accounts for1010–26%26\\%of the solve time, with reasoning dominating the rest, whereas for Grok 4\.3 the sandbox takes55%55\\%, a consequence of minimal reasoning around its short code snippets, and for Qwen only4%4\\%, as its very long reasoning traces dwarf the computation itself\. Open\-source models tend to write longer\-running code, whereas closed models produce fast\-executing code, with Sonnet and DeepSeek\-v4\-Pro as notable exceptions\. A possible explanation is that strong closed models use SageMath mainly to verify derived from reasoning solutions, while open\-source models try to solve the problem itself via tool calls\.

Finding 6\.Open\-source models mostly write code that runs substantially longer in the sandbox, often due to infeasible enumerations hitting the time limit, while closed frontier models tend to produce faster\-executing code\.

### 4\.3Limitations

The present study has several limitations\. First, the symbolic\-verification procedure may fail to recognize correct answers, since robust universal equivalence checking remains difficult in the general case; the judge stage recovers2323–44%44\\%of credited solutions, so small inter\-model gaps are methodologically fragile\. Second, both dataset post\-processing and secondary validation rely on LLM outputs, which are not fully reliable\. Third, the experimental dataset is limited in size and restricted to numerical or symbolic\-expression answers that can be normalized and automatically checked, introducing selection bias toward the computationally executable subset of research\-level mathematics\. Finally, the tool\-augmented setting combines SageMath, Context7, ReAct prompting, and a tool\-use budget; thus, gains cannot be attributed to CAS access alone\.

## 5Case Study: Conjecture Discovery via Tool\-Assisted Iterative Computation

In this section, we examine in detail a solution trajectory for a representative problem, illustrating how a CAS\-augmented GPT\-5\.5 can exhibit key elements of a computational mathematician’s workflow\. Rather than querying SageMath for the target invariants directly, the agent iteratively formulates and tests conjectures, diagnoses errors, and extracts patterns from computational results\. Neither invariant is directly implemented as a SageMath routine, requiring the agent to infer the target formulas indirectly based on iterative computation\.

The problem is drawn from\(Himeno and Teragaito,[2024](https://arxiv.org/html/2607.06820#bib.bib50)\)and focuses on the torsion orderOrd⁡\(K\)\\operatorname\{Ord\}\(K\)and the second torsion orderOrd′⁡\(K\)\\operatorname\{Ord\}^\{\\prime\}\(K\)of the twisted torus knotK=T​\(p,k​p\+1;2,1\)K=T\(p,kp\+1;2,1\)\. Specifically, the task asks for closed\-form expressions forOrd⁡\(K\)\\operatorname\{Ord\}\(K\)whenp≥2p\\geq 2and forOrd′⁡\(K\)\\operatorname\{Ord\}^\{\\prime\}\(K\)whenp≥4p\\geq 4\. The complete problem statement and background are provided in Appendix[E](https://arxiv.org/html/2607.06820#A5), which also contains concise case studies of other tasks\.

#### Stage 1\. Problem setup and capability discovery\.

Agent started with the exploration of its capabilities within SageMath\. It constructed aBraidGroupobject and inspected whether methods such asalexander\_polynomialandburau\_matrixare available\.

#### Stage 2\. From braid representatives to staircase complexes\.

The agent considered the positive braid representation of the knotKK

\(σ1​σ2​⋯​σp−1\)k​p\+1​σ12,\(\\sigma\_\{1\}\\sigma\_\{2\}\\cdots\\sigma\_\{p\-1\}\)^\{kp\+1\}\\sigma\_\{1\}^\{2\},and computed Alexander polynomials for several small values ofppwithk=1k=1\.

Listing 1:Sage computation of small\-case Alexander polynomials\.defalex\_twisted\(p,k\):

B=BraidGroup\(p\)

gens=B\.gens\(\)

beta=prod\(gens\)^\(k\*p\+1\)\*gens\[0\]^2

returnbeta\.alexander\_polynomial\(\)

RESULT=\[\(p,alex\_twisted\(p,1\)\)forpinrange\(2,7\)\]

Later the agent extracted the exponents of nonzero monomials of the Alexander polynomials and interpreted the gaps between successive exponents as staircase lengths for the associatedLL\-space knot complex\. The first implementation attempt failed with aTypeErrordue to inconsistent exponent representations in SageMath, but after adapting the implementation, the revised routine produced:

pstaircase lengthsmax2\[1,1,1,1\]13\[1,2,1,1,2,1\]24\[1,3,1,1,1,1,1,1,3,1\]35\[1,4,1,1,1,2,1,1,2,1,1,1,4,1\]46\[1,5,1,1,1,3,1,1,2,2,1,1,3,1,1,1,5,1\]5⋮⋮⋮\\begin\{array\}\[\]\{c\|c\|c\}p&\\text\{staircase lengths\}&\\max\\\\ \\hline\\cr 2&\[1,1,1,1\]&1\\\\ 3&\[1,2,1,1,2,1\]&2\\\\ 4&\[1,3,1,1,1,1,1,1,3,1\]&3\\\\ 5&\[1,4,1,1,1,2,1,1,2,1,1,1,4,1\]&4\\\\ 6&\[1,5,1,1,1,3,1,1,2,2,1,1,3,1,1,1,5,1\]&5\\\\ \\vdots&\\vdots&\\vdots\\end\{array\}In all computed examples, the largest staircase length was equal top−1p\-1\. Using the standard staircase description of knot Floer homology forLL\-space knots, the agent therefore formulated the conjecture

Ord​\(K\)=p−1\.\\mathrm\{Ord\}\(K\)=p\-1\.

#### Stage 3\. Computing Smith invariant factors\.

To study the second torsion order, the agent used the staircase lengths obtained from the Alexander polynomial to build an explicit presentation matrix over𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\. For the consecutive staircase lengthsℓ0,ℓ1,…,ℓ2​n−1,\\ell\_\{0\},\\ell\_\{1\},\\ldots,\\ell\_\{2n\-1\},the agent formed the\(n\+1\)×n\(n\+1\)\\times nmatrixMMwith nonzero entries

Mj,j=Uℓ2​j,Mj\+1,j=Uℓ2​j\+1,j=0,…,n−1\.M\_\{j,j\}=U^\{\\ell\_\{2j\}\},\\qquad M\_\{j\+1,j\}=U^\{\\ell\_\{2j\+1\}\},\\qquad j=0,\\ldots,n\-1\.It then computed the Smith normal form ofMMover𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\. The diagonal Smith entries are the invariant factors of this presentation; when such an entry has degreedd, it contributes aUU\-torsion factor with exponentdd\.

Fork=1k=1andp=2,…,8p=2,\\ldots,8, the largest degrees of the diagonal Smith factors were

1,1,1,1,2,2,3\.1,1,1,1,2,2,3\.Thus, in the rangep≥4p\\geq 4relevant toOrd′​\(K\)\\mathrm\{Ord\}^\{\\prime\}\(K\), the computed values agree with

Ord′​\(K\)=⌊p−22⌋\.\\mathrm\{Ord\}^\{\\prime\}\(K\)=\\left\\lfloor\\frac\{p\-2\}\{2\}\\right\\rfloor\.

#### Stage 4\. Testing stability across the parameterkk\.

The preceding computations were carried out withk=1k=1\. The agent repeated the extraction of staircase lengths and Smith invariant factors fork=2,3k=2,3andp=3,4,5,6p=3,4,5,6\. In these tests, the maximal staircase length remainedp−1p\-1, and the maximal Smith degree was unchanged askkvaried\. It supported the hypothesis that both torsion orders depend only onppbut not onkk\.

Attempts to push the computation to largerppeventually ran into SageMath timeouts and low\-level runtime failures\. At that point, however, the observed formulas had stabilized across the tested values:

Ord​\(K\)=p−1,Ord′​\(K\)=⌊p−22⌋\.\\mathrm\{Ord\}\(K\)=p\-1,\\qquad\\mathrm\{Ord\}^\{\\prime\}\(K\)=\\left\\lfloor\\frac\{p\-2\}\{2\}\\right\\rfloor\.

#### Summary\.

This example illustrates a successful form of tool\-augmented mathematical reasoning\. SageMath was not used as an oracle forOrd⁡\(K\)\\operatorname\{Ord\}\(K\)orOrd′⁡\(K\)\\operatorname\{Ord\}^\{\\prime\}\(K\), since neither invariant was directly implemented\. Instead, the agent used SageMath to compute accessible intermediate objects: braid Alexander polynomials, exponent gaps, and Smith normal forms over𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\. It recovered from an implementation error caused by Sage’s exponent representation, converted Alexander polynomial data into staircase lengths, and used Smith invariant factors to detectUU\-torsion exponents\.

The resulting formulas were not returned by a single Sage command, but were obtained through an iterative process in which the agent computed examples, identified patterns, formulated conjectures, and validated them across other parameters\. In this sense, the agent’s approach resembles a computational experiment: SageMath supplied evidences, while the agent used its mathematical knowledge to interpret it and infer the conjectural closed forms\.

## 6Conclusions

We evaluated 15 frontier LLMs on133133research\-level mathematical problems derived from the RealMath benchmark, comparing direct\-answer inference against a ReAct\-style agentic pipeline equipped with SageMath and Context7 documentation retrieval\. Tool access improved the solve rate of every evaluated model, by\+9\.7\+9\.7pp on average, with gains ranging from\+1\.5\+1\.5pp \(Kimi K2\.7\) to\+27\.8\+27\.8pp \(Qwen 3\.7\-Max, improving from42\.1%42\.1\\%to69\.9%69\.9\\%\)\. OpenAI’s flagship model, GPT\-5\.5, achieved the highest solve rate of75\.2%75\.2\\%at the lowest token usage among tool\-enabled configurations, dominating every other model on both axes; it is followed by Opus 4\.8 \(73\.7%73\.7\\%\) and the multi\-agent orchestration system Fugu\-Ultra, which matches Opus 4\.7 at72\.9%72\.9\\%while being the second most token\-efficient configuration\. The CAS access substantially narrowed the gap between open\-weight and closed frontier models\.

Beyond overall solve rates, our experiments reveal consistent behavioral patterns that separate effective and ineffective tool\-augmented agents\. Gains are non\-uniform: open\-weight models improve more than twice as much as closed models on average, largely due to weaker tool\-free baselines, yet higher token expenditure does not translate into higher accuracy, and the token\-efficiency ranking inverts between setups: open\-weight models consume the fewest tokens at direct answering but the most as agents\. Agentic runs are strongly bimodal: strong models solve a problem within the first33–44tool interactions, using SageMath mainly to verify solutions already derived through reasoning, whereas weaker agents exhaust the entire tool budget searching for a solution through computation, writing long\-running code\. Consistently, recovery dynamics after failed tool calls vary far more across models than raw failure rates, constituting a axis separating effective and ineffective agents\.

More broadly, our results support the view that computer algebra systems provide a promising substrate for computational and experimental mathematics with LLM agents\. Our case study shows that a CAS\-augmented agent can reproduce key elements of a working mathematician’s workflow: computing accessible intermediate objects, extracting patterns from examples, formulating conjectures, and validating them across parameters\. While current systems remain limited on problems requiring deep theoretical insight or specialized contemporary knowledge, the observed gains indicate that executable symbolic computation can substantially extend the practical reasoning capabilities of frontier models, and we view this direction as a step toward automated mathematical experimentation and computational conjecture discovery\. As future work, we propose a multi\-agent architecture that assigns distinct responsibilities to agents equipped with a diverse set of tools\.

## Impact Statement

This work studies CAS\-assisted LLM agents for research mathematics\. It advances verifiable AI\-assisted scientific reasoning; we foresee no specific societal risks beyond those already recognized and release our evaluation set and validation pipeline for reproducibility\.

## Acknowledgments

German Magai gratefully acknowledges Noeon Research for its support during the preparation of this work\. Both authors thank Anton Ayzenberg for insightful discussions and comments that helped shape the initial idea and narrative\. The authors also thank Darya Zvereva for valuable advice on the presentation of the results\.

## References

- T\. Achim, A\. Best, A\. Bietti, K\. Der, M\. Fédérico, S\. Gukov, D\. Halpern\-Leistner, K\. Henningsgard, Y\. Kudryashov, A\. Meiburg, M\. Michelsen, R\. Patterson, E\. Rodriguez, L\. Scharff, V\. Shanker, V\. Sicca, H\. Sowrirajan, A\. Swope, M\. Tamas, V\. Tenev, J\. Thomm, H\. Williams, and L\. Wu \(2025\)Aristotle: IMO\-level Automated Theorem Proving\.arXiv preprint arXiv:2510\.01346\.External Links:[Link](https://arxiv.org/abs/2510.01346)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- Anthropic \(2026\)Introducing claude sonnet 5\.Note:[https://www\.anthropic\.com/news/claude\-sonnet\-5](https://www.anthropic.com/news/claude-sonnet-5)Official model announcement\. Accessed: 2026\-07\-05Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Axiom Math Team \(2025\)AxiomProver: Solutions to Putnam 2025\.External Links:[Link](https://github.com/AxiomMath/Putnam2025)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- M\. Balunovićet al\.\(2025\)MathArena: Evaluating LLMs on Uncontaminated Math Competitions\.InAdvances in Neural Information Processing Systems \(NeurIPS\) Datasets and Benchmarks Track,External Links:[Link](https://arxiv.org/abs/2505.23281)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p1.1)\.
- M\. Barnabei, F\. Bonetti, N\. Castronuovo, and M\. Silimbani \(2022\)Pattern avoiding alternating involutions\.arXiv preprint arXiv:2206\.13877\.Cited by:[§E\.2](https://arxiv.org/html/2607.06820#A5.SS2.p1.1)\.
- W\. Bosma, J\. Cannon, and C\. Playoust \(1997\)The Magma algebra system\. I\. The user language\.J\. Symbolic Comput\.24\(3\-4\),pp\. 235–265\.Note:Computational algebra and number theory \(London, 1993\)External Links:ISSN 0747\-7171,[Document](https://dx.doi.org/10.1006/jsco.1996.0125),[Link](http://dx.doi.org/10.1006/jsco.1996.0125),[MathReview Entry](https://www.ams.org/mathscinet-getitem?mr=MR1484478)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- M\. J\. Capiński, S\. Kepley, and J\. M\. James \(2023\)Computer assisted proofs for transverse collision and near collision orbits in the restricted three body problem\.Journal of Differential Equations366,pp\. 132–191\.Cited by:[§E\.4](https://arxiv.org/html/2607.06820#A5.SS4.SSS0.Px4.p1.1),[§E\.4](https://arxiv.org/html/2607.06820#A5.SS4.p1.1)\.
- L\. Chen, J\. Gu, L\. Huang, W\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma, C\. Ren, J\. Shen, W\. Shi, T\. Sun, H\. Sun, J\. Wang, S\. Wang, Z\. Wang, C\. Wei, S\. Wei, Y\. Wu, Y\. Wu, Y\. Xia, H\. Xin, F\. Yang, H\. Ying, H\. Yuan, Z\. Yuan, T\. Zhan, C\. Zhang, Y\. Zhang, G\. Zhang, T\. Zhao, J\. Zhao, Y\. Zhou, and T\. H\. Zhu \(2025\)Seed\-prover: deep and broad reasoning for automated theorem proving\.arXiv preprint arXiv:2507\.23726\.External Links:2507\.23726,[Link](https://arxiv.org/abs/2507.23726)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- Y\. Chervonyi, T\. H\. Trinh, M\. Olšák, X\. Yang, H\. Nguyen, M\. Menegali, J\. Jung, V\. Verma, Q\. V\. Le, and T\. Luong \(2025\)Gold\-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2\.Journal of Machine Learning Research26,pp\. 1–39\.External Links:[Link](https://arxiv.org/abs/2502.03544)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- M\. Christianen, A\. Janssen, M\. Vlasiou, and B\. Zwart \(2023\)Asymptotic analysis of emden–fowler type equation with an application to power flow models\.Indagationes Mathematicae34\(5\),pp\. 1146–1180\.Cited by:[§E\.3](https://arxiv.org/html/2607.06820#A5.SS3.p1.1)\.
- J\. Chuharski, E\. R\. Collins, and M\. Meringolo \(2024\)Mining math conjectures from llms: a pruning approach\.External Links:2412\.16177,[Link](https://arxiv.org/abs/2412.16177)Cited by:[§2\.3](https://arxiv.org/html/2607.06820#S2.SS3.p1.1)\.
- D\. Das, D\. Banerjee, S\. Aditya, and A\. Kulkarni \(2024\)MathSensei: a tool\-augmented large language model for mathematical reasoning\.arXiv preprint arXiv:2402\.17231\.Note:Also in Proc\. NAACL 2024External Links:2402\.17231,[Link](https://arxiv.org/abs/2402.17231)Cited by:[§2\.3](https://arxiv.org/html/2607.06820#S2.SS3.p1.1)\.
- W\. Decker, G\. Greuel, G\. Pfister, and H\. Schönemann \(2024\)Singular4\-4\-0 — A computer algebra system for polynomial computations\.Note:[http://www\.singular\.uni\-kl\.de](http://www.singular.uni-kl.de/)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- DeepSeek\-AI \(2025\)DeepSeek\-v3\.2: pushing the frontier of open large language models\.External Links:2512\.02556,[Link](https://arxiv.org/abs/2512.02556)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Epoch AI \(2026\)FrontierMath Benchmark Leaderboard\.Note:[https://epoch\.ai/benchmarks/frontiermath\-tiers\-1\-3](https://epoch.ai/benchmarks/frontiermath-tiers-1-3)Accessed: 2026\-05\-24Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px1.p1.1)\.
- G\. Gao, Y\. Wang, J\. Jiang, Q\. Gao, Z\. Qin, T\. Xu, and B\. Dong \(2025\)Herald: A Natural Language Annotated Lean 4 Dataset\.InInternational Conference on Learning Representations \(ICLR\),External Links:[Link](https://arxiv.org/abs/2410.10878)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- \[17\]\(2026\)GAP – Groups, Algorithms, and Programming, Version 4\.16\.0\.The GAP Group\.External Links:[Link](https://www.gap-system.org/)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- E\. Glazeret al\.\(2024\)FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI\.arXiv preprint arXiv:2411\.04872\.External Links:[Link](https://arxiv.org/abs/2411.04872)Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px1.p1.1)\.
- GLM\-5\-Team \(2026\)GLM\-5: from vibe coding to agentic engineering\.External Links:2602\.15763,[Link](https://arxiv.org/abs/2602.15763)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Google DeepMind AlphaProof and AlphaGeometry teams \(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y),[Link](https://www.nature.com/articles/s41586-025-09833-y)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- Google DeepMind \(2026a\)Gemini 3\.1 pro model card\.External Links:[Link](https://deepmind.google/models/model-cards/gemini-3-1-pro/)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Google DeepMind \(2026b\)Gemini 3\.5 flash model card\.External Links:[Link](https://deepmind.google/models/model-cards/gemini-3-5-flash/)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Z\. Gou, Z\. Shao, Y\. Gong, Y\. Yang, M\. Huang, N\. Duan, W\. Chen,et al\.\(2024\)Tora: a tool\-integrated reasoning agent for mathematical problem solving\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 48362–48395\.Cited by:[§2\.3](https://arxiv.org/html/2607.06820#S2.SS3.p1.1)\.
- \[24\]D\. R\. Grayson and M\. E\. StillmanMacaulay2, a software system for research in algebraic geometry\.Note:Available at[http://www2\.macaulay2\.com](http://www2.macaulay2.com/)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- K\. Himeno and M\. Teragaito \(2024\)Hyperbolic knots with arbitrarily large torsion order in knot floer homology\.External Links:2412\.20652,[Link](https://arxiv.org/abs/2412.20652)Cited by:[§E\.1](https://arxiv.org/html/2607.06820#A5.SS1.p1.1),[§5](https://arxiv.org/html/2607.06820#S5.p2.7)\.
- Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. Jin \(2025\)Goedel\-Prover\-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self\-Correction\.arXiv preprint arXiv:2508\.03613\.External Links:[Link](https://arxiv.org/abs/2508.03613)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- J\. Maet al\.\(2026\)EternalMath: a living benchmark of frontier mathematics that evolves with human discovery\.arXiv preprint arXiv:2601\.01400\.Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px1.p1.1)\.
- G\. Martin, K\. Salehi, and Y\. Yamashita \(2022\)The\(4,p\)\(4,p\)\-arithmetic hyperbolic lattices,p≥2p\\geq 2, in three dimensions\.arXiv preprint arXiv:2206\.14174\.Cited by:[§E\.6](https://arxiv.org/html/2607.06820#A5.SS6.p1.2)\.
- A\. Meurer, C\. P\. Smith, M\. Paprocki, O\. Čertík, S\. B\. Kirpichev, M\. Rocklin, A\. Kumar, S\. Ivanov, J\. K\. Moore, S\. Singh, T\. Rathnayake, S\. Vig, B\. E\. Granger, R\. P\. Muller, F\. Bonazzi, H\. Gupta, S\. Vats, F\. Johansson, F\. Pedregosa, M\. J\. Curry, A\. R\. Terrel, Š\. Roučka, A\. Saboo, I\. Fernando, S\. Kulal, R\. Cimrman, and A\. Scopatz \(2017\)SymPy: symbolic computing in python\.PeerJ Computer Science3,pp\. e103\.External Links:ISSN 2376\-5992,[Link](https://doi.org/10.7717/peerj-cs.103),[Document](https://dx.doi.org/10.7717/peerj-cs.103)Cited by:[§A\.2](https://arxiv.org/html/2607.06820#A1.SS2.p2.5)\.
- MiniMax \(2026\)MiniMax m3: frontier coding, 1m context, native multimodality — all in one model\.Note:[https://www\.minimax\.io/blog/minimax\-m3](https://www.minimax.io/blog/minimax-m3)Accessed: 2026\-07\-05Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Moonshot AI \(2026\)Kimi k2\.7 code\.Note:[https://platform\.kimi\.ai/docs/guide/kimi\-k2\-7\-code\-quickstart](https://platform.kimi.ai/docs/guide/kimi-k2-7-code-quickstart)Accessed: 2026\-07\-05Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. R\. Ruiz, A\. Mehrabian, M\. P\. Kumar, A\. See, S\. Chaudhuri, G\. Holland, A\. Davies, S\. Nowozin, P\. Kohli, and M\. Balog \(2025\)AlphaEvolve: a coding agent for scientific and algorithmic discovery\.arXiv preprint arXiv:2506\.13131\.External Links:2506\.13131,[Link](https://arxiv.org/abs/2506.13131)Cited by:[§2\.3](https://arxiv.org/html/2607.06820#S2.SS3.p1.1)\.
- OpenAI \(2026a\)GPT\-5\.5 system card\.External Links:[Link](https://openai.com/index/gpt-5-5-system-card/)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- OpenAI \(2026b\)Planar point sets with many unit distances\.External Links:[Link](https://cdn.openai.com/pdf/74c24085-19b0-4534-9c90-465b8e29ad73/unit-distance-proof.pdf)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- D\. V\. Phuc \(2024\)On the hit problem for the polynomial algebra and the algebraic transfer\.arXiv preprint arXiv:2412\.02494\.Cited by:[§E\.5](https://arxiv.org/html/2607.06820#A5.SS5.p2.1)\.
- Qwen \(2026\)Qwen3\.7: the agent frontier\.Note:[https://qwen\.ai/blog?id=qwen3\.7](https://qwen.ai/blog?id=qwen3.7)Accessed: 2026\-07\-05Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- Z\. Z\. Renet al\.\(2025\)DeepSeek\-Prover\-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition\.arXiv preprint arXiv:2504\.21801\.External Links:[Link](https://arxiv.org/abs/2504.21801)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. R\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi, P\. Kohli, and A\. Fawzi \(2024\)Mathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.External Links:[Document](https://dx.doi.org/10.1038/s41586-023-06924-6)Cited by:[§2\.3](https://arxiv.org/html/2607.06820#S2.SS3.p1.1)\.
- SakanaAI \(2026\)Sakana fugu technical report\.arXiv preprint arXiv:2606\.21228\.Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- J\. Schmitt, G\. Bérczi, J\. Dekoninck, J\. Feusi, T\. Gehrunger,et al\.\(2025\)IMProofBench: benchmarking AI on research\-level mathematical proof generation\.arXiv preprint arXiv:2509\.26076\.Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px2.p1.1)\.
- M\. Shalyt, R\. Elimelech, and I\. Kaminer \(2025\)ASyMOB: algebraic symbolic mathematical operations benchmark\.arXiv preprint arXiv:2505\.23851\.Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px2.p1.1),[§3\.4](https://arxiv.org/html/2607.06820#S3.SS4.p1.1)\.
- Z\. Shao, Y\. Luo, C\. Lu, Z\. Z\. Ren,et al\.\(2025\)DeepSeekMath\-V2: Towards Self\-Verifiable Mathematical Reasoning\.arXiv preprint arXiv:2511\.22570\.External Links:[Link](https://arxiv.org/abs/2511.22570)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- N\. Sothanaphan \(2026\)Resolution of Erdős Problem \#728: A Writeup of Aristotle’s Lean Proof\.arXiv preprint arXiv:2601\.07421\.External Links:[Link](https://arxiv.org/abs/2601.07421)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- B\. Tang, X\. Yang, Y\. Wang, Z\. Qiu, Z\. Ji, and W\. Jiang \(2025\)IntegralBench: Benchmarking LLMs with Definite Integral Problems\.AI for Math Workshop at the 42nd International Conference on Machine Learning \(ICML\)\.External Links:[Link](https://arxiv.org/abs/2507.21130)Cited by:[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px2.p1.1)\.
- The PARI Group \(2023\)PARI/GP version2\.15\.4\.Univ\. Bordeaux\.Note:available from[http://pari\.math\.u\-bordeaux\.fr/](http://pari.math.u-bordeaux.fr/)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- The Sage Developers \(2022\)SageMath, the Sage Mathematics Software System\.Note:DOI 10\.5281/zenodo\.6259615External Links:[Link](https://www.sagemath.org/)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p3.1)\.
- G\. Tsoukalas, A\. Kovsharov, S\. Shirobokov, A\. Surina, M\. Firsching, G\. Bérczi, F\. J\. R\. Ruiz, A\. Suggala, A\. Z\. Wagner, E\. Wieser, L\. Yu, A\. Huang, M\. Z\. Horváth, A\. Ferrauiolo, H\. Michalewski, C\. Grosu, T\. Hubert, M\. Balog, P\. Kohli, and S\. Chaudhuri \(2026\)Advancing mathematics research with ai\-driven formal proof search\.External Links:2605\.22763,[Link](https://arxiv.org/abs/2605.22763)Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- G\. Tsoukalas, J\. Lee, J\. Jennings, J\. Xin, M\. Ding, M\. Jennings, A\. Thakur, and S\. Chaudhuri \(2024\)PutnamBench: evaluating neural theorem\-provers on the Putnam mathematical competition\.InAdvances in Neural Information Processing Systems \(NeurIPS\), Datasets and Benchmarks Track,Note:arXiv:2407\.11214Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p1.1),[§3\.4](https://arxiv.org/html/2607.06820#S3.SS4.p1.1)\.
- Upstash Team \(2026\)Context7: up\-to\-date documentation for llms and ai code editors\.Note:[https://context7\.com/](https://context7.com/)Context7 is an Upstash projectExternal Links:[Link](https://context7.com/)Cited by:[§3\.2](https://arxiv.org/html/2607.06820#S3.SS2.SSS0.Px2.p1.1)\.
- H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu,et al\.\(2025a\)Kimina\-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning\.arXiv preprint arXiv:2504\.11354\.External Links:[Link](https://arxiv.org/abs/2504.11354)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- P\. Wang, T\. Liu, C\. Wang, Y\. Wang, S\. Yan, C\. Jia, X\. Liu, X\. Chen, J\. Xu, Z\. Li, and Y\. Yu \(2025b\)A survey on large language models for mathematical reasoning\.ACM Computing Surveys\.Note:Just Accepted; also available as arXiv:2506\.08446External Links:[Document](https://dx.doi.org/10.1145/3786333)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. Szegedy \(2022\)Autoformalization with large language models\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§1](https://arxiv.org/html/2607.06820#S1.p2.1)\.
- xAI \(2026\)Grok 4\.3\.Note:Model documentationExternal Links:[Link](https://docs.x.ai/developers/models/grok-4.3)Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- H\. Xinet al\.\(2024\)DeepSeek\-Prover: Advancing Theorem Proving in LLMs through Large\-Scale Synthetic Data\.arXiv preprint arXiv:2405\.14333\.External Links:[Link](https://arxiv.org/abs/2405.14333)Cited by:[§2\.1](https://arxiv.org/html/2607.06820#S2.SS1.p2.1)\.
- A\. Xu, B\. Lin, B\. Xue, B\. Wang, B\. Xu, B\. Wu, B\. Zhang, C\. Lin, C\. Dong, C\. Ling,et al\.\(2026\)Deepseek\-v4: towards highly efficient million\-token context intelligence\.arXiv preprint arXiv:2606\.19348\.Cited by:[§3\.3](https://arxiv.org/html/2607.06820#S3.SS3.SSS0.Px2.p1.2)\.
- J\. Zhang, C\. Petrui, K\. Nikolić, and F\. Tramèr \(2025\)RealMath: A Continuous Benchmark for Evaluating Language Models on Research\-Level Mathematics\.InAdvances in Neural Information Processing Systems \(NeurIPS\) Datasets and Benchmarks Track,External Links:[Link](https://arxiv.org/abs/2505.12575)Cited by:[§A\.2](https://arxiv.org/html/2607.06820#A1.SS2.p1.1),[§2\.2](https://arxiv.org/html/2607.06820#S2.SS2.SSS0.Px1.p1.1),[§3\.1](https://arxiv.org/html/2607.06820#S3.SS1.p1.1),[§3\.4](https://arxiv.org/html/2607.06820#S3.SS4.p1.1)\.

## Appendix AExperimental Details

### A\.1Implementation Details

#### SageMath Sandbox\.

All SageMath execution is performed in an ephemeral Docker container\. For each tool call, a generated Sage program is launched through a small wrapper\. This wrapper importssage\.all, runs Sage’s preparser to standardize Sage syntax, executes the script and extracts the designated result variable\. It also captures standard output and returns a JSON\-friendly representation of the result to the host\.

For each tool call, the generated code snippet is executed in a fresh interpreter\. The execution is limited to 2 CPU cores, 4 GB of memory, a 45s wall\-clock timeout, and a 50s CPU\-time limit\. The executed code has no network access\. The host also rejects outputs larger than 262,144 bytes before parsing the returned result to prevent excessively large intermediate outputs\. Failure handling is normalized into a small number of categories\. User\-code exceptions are returned ascode\_errortogether with the captured traceback\. Docker startup failures, such as an unavailable daemon or missing image, are classified asdocker\_error\. Container crashes or abnormal exits are classified asruntime\_crash, and wall\-clock overruns are classified astimeout; in the timeout case the host forcibly removes the container\.

### A\.2Dataset Construction

We begin with the dataset of 633 problems obtained from the RealMath benchmark\(Zhanget al\.,[2025](https://arxiv.org/html/2607.06820#bib.bib26)\)\. We focus on this dataset because it is derived from the contemporary mathematical literature\. Each problem from this dataset contains the question, context and the answer, each of which is represented in a LaTeX format\. We also enrich the dataset enriching it with the arXiv categories that were associated with the papers from which the corresponding problems were scraped via the RealMath extraction pipeline\. If the paper had several categories, only the first one was used\.

We automatically retain only those tasks whose final answers can be normalized into executable SymPy\(Meureret al\.,[2017](https://arxiv.org/html/2607.06820#bib.bib53)\)objects suitable for automatic verification\. Specifically, we want the answers to be normalized into either a concrete numerical value, or a symbolic expression that might consist of several free variables or use the widely used mathematical notation \(such asπ\\pifor3\.14159​…3\.14159\.\.\.,eefor2\.71828​…2\.71828\.\.\.,Γ\\Gammafor the Gamma function, etc\)\. In order to do this, we employ LLM\-assisted normalization procedure, under which the original ground truth answer, given in the free LaTeX form, is transformed into SymPy\-parsable string\. Under this procedure we reduce the problem size in half, resulting in 300 problems\. Since the context field in RealMath often contains excessive or irrelevant information, we use an LLM to compress the context, retaining only the relevant definitions and incorporating them directly into the question\. We automatically annotate the answer type as one of the following: a number is a concrete numerical value, an expression is a symbolic expression in some free variables, a formula is an equality “named invariant = expression” in which the left\-hand side is a label rather than a checkable quantity\.

As a next step, we employ an LLM\-assisted annotation stage to estimate whether symbolic experimentation or computational verification is feasible within SageMath\. In order to do this, we define several criteria for a problem to be suitable for our study: a task is suitable if

1. 1\.Objects mentioned in the question can be represented by the means of SageMath,
2. 2\.Candidate answers can be explored with the help of computational experiment,
3. 3\.Intermediate computation steps can be executed in SageMath,

This stage reduces the problem set to 219\. From this, we sample 133 problems attempting to reduce the skewness of the distribution across arXiv categories\. Figure[6](https://arxiv.org/html/2607.06820#S4.F6)illustrates the distribution of the selected problems across arXiv categories\.

## Appendix BFigures for Empirical Analyses

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/bubbles.png)Figure 9:The relationship between the mean number of tool calls and the solve rate for various arXiv categories\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/pairwise-agreement.png)Figure 10:Pairwise per\-problem agreement matrices across all evaluated models\. Left: tool\-free setting\. Right: agentic setting with tools\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/answer_type.png)Figure 11:Solve rate by answer type for each model and setup\. Bars compare expression and numerical problems under no\-tool and tool\-augmented runs\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/tool_calls.png)Figure 12:Tool calls by model\. Bars show the total number of Sage execution calls and Context7 lookups across benchmark problems\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/error_types.png)Figure 13:Failed Sage calls broken down by Python exception type \(left\) and by model \(right\)\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/recovery_after_error.png)Figure 14:Recovery after an error per model\.![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/trace_tiles_2.png)Figure 15:Tool\-call traces for the selected 50 problems across models\. Each column is one problem and each vertical stack shows the sequence of tool calls made by a model in a single run\. Colors indicate successful Sage calls, code errors, timeouts, runtime crashes, documentation queries, missing tool calls\. The small bar below each stack marks the final answer as correct or incorrect\.
## Appendix CFunction usage by arXiv category

Figure[16](https://arxiv.org/html/2607.06820#A3.F16)reports the most frequent computational functions invoked by the tool\-augmented agents, grouped by arXiv primary category, focusing on the mathematical actions that were performed by the agents when dealing with the problems from these categories\. We exclude boilerplate calls such as object constructions, printing, iterations, and list manipulations\. Function names are reported as normalized display labels, such asmatrix\.rankorpolynomial\.factor\.

The most frequent operation overall isarith\.gcd, with 1274 traces, of which 1042 occur inmath\.NT\. Thus, the dominance of this row is largely a number\-theoretic effect rather than a uniform pattern across all areas\. Similarly,itertools\.combinationsappears 1041 times overall, with 601 occurrences inmath\.CO, 160 inmath\.GR, and 92 inmath\.SG\. This suggests that a substantial fraction of tool use in these areas consists of finite search over candidate subsets or configurations\. The related rowitertools\.permutationsis even more concentrated: 285 of its 360 occurrences are inmath\.CO\.

Linear algebra operations are more broadly distributed\. The rowmatrix\.rankappears 895 times overall and has substantial mass inmath\.RA,math\.AG,math\.AT,math\.CA, andmath\.SG\. Likewise,modules\.dimensionandmodules\.basisare especially prominent inmath\.RA, where they appear 302 and 179 times respectively, but also occur frequently inmath\.AG\. This indicates that agents often reduce problems in representation theory, algebraic geometry, and related algebraic categories to rank, dimension, basis, or kernel computations\. Polynomial operations form another distinct cluster\. The rowpolynomial\.factorappears 422 times, mainly inmath\.NTandmath\.AG\. The more specialized operationpolynomial\.groebner\_basisappears less frequently overall, but is concentrated in algebraic categories, especiallymath\.AGandmath\.AT\. This is consistent with the overall practice of Groebner basis computations being used for ideal membership, elimination, or solving polynomial systems\.

Analysis\-oriented categories show a different computational profile\. The rowsscipy\.integrate\.solve\_ivp,scipy\.integrate\.quad,mpmath\.quad,calculus\.derivativeandcalculus\.integrateare concentrated inmath\.AP,math\.PR,math\.CA, andmath\.DS\. For instance,scipy\.integrate\.solve\_ivpappears 92 times inmath\.DSand 72 times inmath\.CA, while quadrature routines are concentrated inmath\.APandmath\.CA\. This separates continuous\-analysis problems from the enumerative and algebraic patterns seen in the other categories\. Finally, methods for symbolic manipulations such assymbolic\.solve,symbolic\.expand,symbolic\.simplify, andsymbolic\.simplify\_fullare less tied to a particular mathematical domain, but often appear as intermediate steps used to solve equations, compare coefficients, expand polynomial identities, or simplify expressions before producing a final answer\. Notably,symbolic\.solveis especially frequent inmath\.CO, whilesymbolic\.expandis concentrated inmath\.AG; simplification routines are more broadly spread across algebraic, analytic, probabilistic, and geometric categories\.

![Refer to caption](https://arxiv.org/html/2607.06820v1/figures/function_usage_by_arxiv_category.png)Figure 16:Function\-level tool usage by arXiv primary category\. Rows show the top functions extracted from tool traces, after filtering constructors and generic programming utilities\. Columns show arXiv primary categories\. Each cell reports the number of Sage execution traces in which the function appears at least once\. These labels are normalized and indicate the mathematical subdomain and function or method name\.
## Appendix DModel\-specific observations

#### GPT\-5\.5\.

The dominant configuration: tools lift its solve rate from67\.7%67\.7\\%to75\.2%75\.2\\%, the best result overall, at the lowest cost \(3434k tokens and3\.83\.8Sage calls per problem, median trace of11\)\. It combines an85%85\\%call\-success rate with the best post\-failure recovery \(77%77\\%\), self\-finalizes91%91\\%of runs, and contributes the largest single\-model coverage \(100/133100/133\) to the ensemble analysis\.

#### Opus 4\.8\.

The second\-best solve rate overall \(73\.7%73\.7\\%, up from66\.2%66\.2\\%without tools\), reached with a compact agentic tool call traces \(3\.63\.6calls per problem, median trace of22,89%89\\%self\-finalization\)\. Its one weakness is timeouts:22\.6%22\.6\\%of its Sage calls exceed the wall\-clock limit, the highest share among the 4 leading models, which decreases its raw call\-success rate \(66%66\\%\) without noticeably hurting its accuracy\.

#### Opus 4\.7\.

Tool access improves solve rate from61\.7%61\.7\\%to72\.9%72\.9\\%, 16 problems gained\. It has the cleanest tool\-interaction profile in the study: the fewest Sage calls overall \(435435;3\.33\.3per problem\), an84%84\\%call\-success rate, zeroNameErrors,92%92\\%self\-finalization, and the shortest sandbox time per problem \(2929s\)\.

#### Fugu\-Ultra\.

Tied with Gemini 3\.1 Pro for the second\-strongest tool\-free baseline \(66\.9%66\.9\\%, behind GPT\-5\.5\)\. Fugu\-Ultra reaches72\.9%72\.9\\%with tools: short, clean code \(median662662characters\), an85%85\\%call\-success rate, and no interpreter\-state errors\. Its token multiplier under tool access is the smallest of any model \(4\.5×4\.5\\times,7070k tokens per problem\), placing it second on the accuracy\-cost plane among frontier models after GPT\-5\.5\.

#### Qwen 3\.7 Max\.

The largest gain from CAS access, jumping from42\.1%42\.1\\%to69\.9%69\.9\\%\(\+27\.8\+27\.8pp\)\. The cost is a≈99×\\approx 99\\timesincreased token usage \(230230k tokens per problem\), so dominated by reasoning that the sandbox accounts for only4%4\\%of its solve time\.

#### Gemini 3\.1 Pro\.

The most stable configuration \(66\.9%→69\.9%66\.9\\%\\to 69\.9\\%\): only77problems gained and33lost under tool access\. Its agentic statistics8\.18\.1calls per problem,78%78\\%call success,66%66\\%self\-finalization\. Gemini\-3\.1 also has the strongest symbolic\-checker accuracy among the models at 51\.1%, suggesting better answer normalization or cleaner exact outputs\.

#### Sonnet 5\.

Moves from59\.4%59\.4\\%to66\.9%66\.9\\%despite a problematic execution profile\. It writes the shortest code among non\-degenerate models \(median437437characters\) but launches honest, computationally infeasible enumerations:41%41\\%of its Sage calls time out \(the largest share of any model\), its mean sandbox time \(142142s\) is among the three highest, and its post\-failure recovery \(16%16\\%\) is the lowest, since it retries variants of the same infeasible computation\.

#### Gemini 3\.5 Flash\.

A solid mid\-tier agent \(61\.7%→66\.9%61\.7\\%\\to 66\.9\\%\) whose failure profile is dominated byNameErrors \(9999\), reflecting frequent loss of interpreter state across the stateless Sage calls; recovery is nonetheless strong \(71%71\\%\), and its overall call\-success rate \(74%74\\%\) remains respectable at9\.39\.3calls per problem\.

#### DeepSeek V4\-Pro\.

Improves its accuracy from52\.6%52\.6\\%to63\.2%63\.2\\%:1,2851\{,\}285Sage calls at an81%81\\%success rate \(the best among the heavy tool users\), combined with active documentation use \(3333Context7 lookups\)\. This throughput is not cheap:240240k tokens per problem, the second\-largest budget after MiniMax, and nearly half of its runs \(48%48\\%\) terminated by forced finalization\.

#### GLM 5\.2

Gains\+9\.0\+9\.0pp \(53\.4%→62\.4%53\.4\\%\\to 62\.4\\%\) but prefers heavy symbolic computations that frequently exceed the wall\-clock limit \(27%27\\%of calls; mean sandbox time147147s\), recovers poorly \(26%26\\%\), and self\-finalizes only53%53\\%of runs\.

#### Kimi K2\.7\.

This model is persistent but inefficient:1,4211\{,\}421Sage calls with a median trace of1414, a call\-success rate below50%50\\%split between code errors \(26%26\\%\) and timeouts \(25%25\\%\), the longest mean sandbox time \(161161s per problem\), and205205k tokens per problem \- all for a\+1\.5\+1\.5pp gain \(57\.1%→58\.6%57\.1\\%\\to 58\.6\\%\)\. It is also the only model whose traces contain a call to a nonexistent tool name, which the orchestrator rejected\.

#### MiniMax M3\.

A substantial tool gain \(38\.3%→55\.6%38\.3\\%\\to 55\.6\\%,\+17\.3\+17\.3pp\) achieved at extreme token usage:556556k tokens per problem, by far the largest budget we observed, driven by very long reasoning traces, with a third of runs terminated by forced finalization rather than by the model’s own decision\.

#### DeepSeek V3\.2\.

This model is highly tool\-persistent but inefficient \(1,5491\{,\}549Sage calls, median trace at the1515\-call cap\) and is the most frequent documentation reader \(143143Context7 lookups\); the brute force still helps, improving accuracy from33\.1%33\.1\\%to48\.9%48\.9\\%\. Only62%62\\%of its calls succeed \(third raise exceptions\) and it tends to revisit the same flawed approach across consecutive calls, self\-finalizing just35%35\\%of runs\.

#### Grok 4\.3\.

Barely improves with tools \(39\.1%→42\.9%39\.1\\%\\to 42\.9\\%\), yielding56%56\\%code errors \(mostlySyntaxErrors\), a42%42\\%call\-success rate \(the lowest\), and32%32\\%recovery\. The minimal reasoning around these snippets makes it the only model whose sandbox time exceeds half \(55%55\\%\) of its total solve time\.

#### DeepSeek V4\-Flash\.

Mirrors DeepSeek V3\.2’s budget\-saturating behavior \(median trace1515,168168Context7 lookups, the most of any model\) at the weakest absolute level \(30\.8%→42\.1%30\.8\\%\\to 42\.1\\%\); despite a decent77%77\\%call\-success rate, two\-thirds of its runs end in forced finalization, and its gains come almost entirely from numerical\-answer problems\.

## Appendix ECase Studies

This section presents case studies of six representative problems that were solved correctly by LLM agents with SageMath access\. Each problem is described in a separate subsection, which provides the problem statement and final answer\. Additionally we briefly summarize the agent’s solution strategy based on an analysis of the tool\-call traces logged during the experimental runs\. In the final we provide two examples of problems that required the highest number of tokens for a tool\-free zero\-shot run among problems solved by only one model\.

### E\.1Torsion Orders of Twisted Torus Knots

This problem was extracted from ”Hyperbolic knots with arbitrarily large torsion order in knot Floer homology”\(Himeno and Teragaito,[2024](https://arxiv.org/html/2607.06820#bib.bib50)\)posted on arXiv\.

#### Question\.

Consider a twisted torus knot

K=T​\(p,k​p\+1;2,1\),k≥1\.K=T\(p,kp\+1;2,1\),\\qquad k\\geq 1\.The torsion orderOrd​\(K\)\\mathrm\{Ord\}\(K\)is defined as

Ord​\(K\)=min⁡\{k≥0\|Uk⋅Tor​\(HFK−​\(K\)\)=0\}∈ℕ∪\{0\},\\mathrm\{Ord\}\(K\)=\\min\\left\\\{k\\geq 0\\;\\middle\|\\;U^\{k\}\\cdot\\mathrm\{Tor\}\\bigl\(\\mathrm\{HFK\}^\{\-\}\(K\)\\bigr\)=0\\right\\\}\\in\\mathbb\{N\}\\cup\\\{0\\\},whereHFK−​\(K\)\\mathrm\{HFK\}^\{\-\}\(K\)is the minus version of knot Floer homology \(a finitely generated module over𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\), andTor​\(HFK−​\(K\)\)\\mathrm\{Tor\}\\bigl\(\\mathrm\{HFK\}^\{\-\}\(K\)\\bigr\)denotes its𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\-torsion submodule\. The second torsion orderOrd′​\(K\)\\mathrm\{Ord\}^\{\\prime\}\(K\)is defined as

Ord′​\(K\)=min⁡\{k≥0\|Uk⋅Tor​\(HFK′​\(K\)\)=0\}∈ℕ∪\{0\},\\mathrm\{Ord\}^\{\\prime\}\(K\)=\\min\\left\\\{k\\geq 0\\;\\middle\|\\;U^\{k\}\\cdot\\mathrm\{Tor\}\\bigl\(\\mathrm\{HFK\}^\{\\prime\}\(K\)\\bigr\)=0\\right\\\}\\in\\mathbb\{N\}\\cup\\\{0\\\},whereHFK′​\(K\)\\mathrm\{HFK\}^\{\\prime\}\(K\)is Ozsváth, Stipsicz and Szabó’s unoriented knot Floer homology \(also a module over𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\), andTor​\(HFK′​\(K\)\)\\mathrm\{Tor\}\\bigl\(\\mathrm\{HFK\}^\{\\prime\}\(K\)\\bigr\)denotes its𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]\-torsion submodule\.

1. \(a\)Forp≥2p\\geq 2, what is the value ofOrd​\(K\)\\mathrm\{Ord\}\(K\)in terms ofpp?
2. \(b\)Forp≥4p\\geq 4, what is the value ofOrd′​\(K\)\\mathrm\{Ord\}^\{\\prime\}\(K\)in terms ofpp?

#### Answer\.

Ord⁡\(K\)=p−1\(p≥2\),\\operatorname\{Ord\}\(K\)=p\-1\\qquad\(p\\geq 2\),and

Ord′⁡\(K\)=⌊p−22⌋\(p≥4\)\.\\operatorname\{Ord\}^\{\\prime\}\(K\)=\\left\\lfloor\\frac\{p\-2\}\{2\}\\right\\rfloor\\qquad\(p\\geq 4\)\.

#### Solution’s strategy\.

GPT\-5\.5 represented the knots as closures of the braids

\(σ1​⋯​σp−1\)k​p\+1​σ12\(\\sigma\_\{1\}\\cdots\\sigma\_\{p\-1\}\)^\{kp\+1\}\\sigma\_\{1\}^\{2\}and computed Alexander polynomials for small values ofpp\.

It extracted the exponents of the nonzero Laurent\-polynomial terms, corrected an initial error caused by inconsistent exponent representations, and examined the resulting sequences of exponent gaps\. The agent then constructed small matrices over𝔽2​\[U\]\\mathbb\{F\}\_\{2\}\[U\]from the inferred staircase data and computed Smith normal forms for selected values ofppandkk\. These experiments consistently identified maximal relevant staircase gaps equal top−1p\-1and supported the stated formulas\. The final generalization relied on the known knot\-Floer\-theoretic structure of this family; the SageMath trace provides finite\-instance evidence rather than a proof of the general theorem\.

### E\.2Reverse Alternating Involutions

This problem was extracted from ”Pattern avoiding alternating involutions”\(Barnabeiet al\.,[2022](https://arxiv.org/html/2607.06820#bib.bib59)\)posted on arXiv\.

#### Question\.

A permutationπ=π1​…​πn\\pi=\\pi\_\{1\}\\ldots\\pi\_\{n\}is called reverse alternating if

πi\>πi\+1if and only ifi​is odd,\\pi\_\{i\}\>\\pi\_\{i\+1\}\\quad\\text\{if and only if\}\\quad i\\text\{ is odd\},i\.e\.,

Des⁡\(π\)=\{1,3,5,…\},\\operatorname\{Des\}\(\\pi\)=\\\{1,3,5,\\ldots\\\},whereDes⁡\(π\)\\operatorname\{Des\}\(\\pi\)denotes the set of descents \(indicesiisuch thatπi\>πi\+1\\pi\_\{i\}\>\\pi\_\{i\+1\}\)\. A permutation is an involution ifπ=π−1\\pi=\\pi^\{\-1\}\. LetR​A​I2​n​\(1234\)RAI\_\{2n\}\(1234\)denote the set of reverse alternating involutions of length2​n2nthat avoid the pattern12341234, i\.e\., no subsequence of four elements is order\-isomorphic to the increasing sequence12341234\. LetMnM\_\{n\}denote thenn\-th Motzkin number, which counts the number of Motzkin paths of lengthnn\. A Motzkin path of lengthnnis a lattice path from\(0,0\)\(0,0\)to\(n,0\)\(n,0\)using up stepsU=\(1,1\)U=\(1,1\), down stepsD=\(1,−1\)D=\(1,\-1\), and horizontal stepsH=\(1,0\)H=\(1,0\), never going below thexx\-axis\. The Motzkin numbers satisfy

M0=1,M1=1,M2=2,M\_\{0\}=1,\\qquad M\_\{1\}=1,\\qquad M\_\{2\}=2,and the recurrence or generating function as standard\. Express the cardinality\|R​A​I2​n​\(1234\)\|\|RAI\_\{2n\}\(1234\)\|in terms of Motzkin numbersMkM\_\{k\}for appropriatekk\.

#### Answer\.

Mn\+1−2​Mn−1\+Mn−3\.M\_\{n\+1\}\-2M\_\{n\-1\}\+M\_\{n\-3\}\.

#### Solution’s strategy\.

GPT\-5\.5 first directly enumerated involutions of length2​n2nfor smallnn, filtered them by the reverse\-alternating condition and by12341234\-avoidance, and obtained the sequence

1,2,6,14,35,89,…\.1,2,6,14,35,89,\\ldots\.It then inspected the corresponding Robinson–Schensted shapes and implemented a dynamic program over standard Young tableau growth states\. The dynamic program enforced the prescribed alternating descent pattern and restricted row lengths to at most three\. Finally, the agent generated a longer sequence, compared it against linear combinations of shifted Motzkin numbers, and verified agreement with

Mn\+1−2​Mn−1\+Mn−3M\_\{n\+1\}\-2M\_\{n\-1\}\+M\_\{n\-3\}on the computed range\.

### E\.3The Critical Emden–Fowler Parameter

This problem was extracted from ”Asymptotic analysis of Emden\-Fowler type equation with an application to power flow models”\(Christianenet al\.,[2023](https://arxiv.org/html/2607.06820#bib.bib61)\)published in*Indagationes Mathematicae*\.

#### Question\.

Consider the Emden–Fowler type differential equation

f′′​\(t\)=kf​\(t\),t≥0,f^\{\\prime\\prime\}\(t\)=\\frac\{k\}\{f\(t\)\},\\qquad t\\geq 0,with initial conditions

f​\(0\)=1andf′​\(0\)=w≥0,f\(0\)=1\\qquad\\text\{and\}\\qquad f^\{\\prime\}\(0\)=w\\geq 0,wherek\>0k\>0is a positive constant\. Define

g​\(t\):=t​2​k​ln⁡\(t\)g\(t\):=t\\sqrt\{2k\\ln\(t\)\}as the first\-order asymptotic approximation off​\(t\)f\(t\)ast→∞t\\to\\infty\. For eachk\>0k\>0, there exists a uniquew≥0w\\geq 0such that the solutionf​\(t\)f\(t\)satisfies the additional condition

Theorem states that there exists a unique critical valuekck\_\{c\}such that:

1. \(a\)Ifk≥kck\\geq k\_\{c\}, thenf​\(t\)≥g​\(t\)f\(t\)\\geq g\(t\)for allt≥1t\\geq 1\.
2. \(b\)If0<k<kc0<k<k\_\{c\}, then there existt1​\(k\),t2​\(k\)t\_\{1\}\(k\),t\_\{2\}\(k\)with 1<t1​\(k\)<t2​\(k\)<∞1<t\_\{1\}\(k\)<t\_\{2\}\(k\)<\\inftysuch thatf​\(t\)<g​\(t\)f\(t\)<g\(t\)whent1​\(k\)<t<t2​\(k\)t\_\{1\}\(k\)<t<t\_\{2\}\(k\)andf​\(t\)\>g​\(t\)f\(t\)\>g\(t\)when 1≤t<t1​\(k\)ort\>t2​\(k\)\.1\\leq t<t\_\{1\}\(k\)\\qquad\\text\{or\}\\qquad t\>t\_\{2\}\(k\)\.

What is the unique value ofkck\_\{c\}?

#### Answer\.

kc=1\.038408008803683392290341649198​…,k\_\{c\}=1\.038408008803683392290341649198\\ldots,

#### Solution’s strategy\.

GPT\-5\.5 first attempted a high\-precision numerical formulation, but the initial routine produced complex values\. It then reformulated the calculation using a real\-valued integral representation, numerically determined the auxiliary parameter associated with eachkk, and minimized the difference betweenffandgg\. The agent subsequently solved the two double\-contact equations with high\-precision root finding\. Its final SageMath computation returned

kc=1\.03840800880368339229034164919800701585437398409411391865025​…k\_\{c\}=1\.03840800880368339229034164919800701585437398409411391865025\\ldotsand a contact location parameter

L=2\.91125215132671158159663851200593904459028086983270951492491​…,L=2\.91125215132671158159663851200593904459028086983270951492491\\ldots,with the two reported numerical residuals of order10−8110^\{\-81\}and10−7910^\{\-79\}\.

### E\.4Ejection–Collision Orbits in the PCRTBP

This problem was extracted from ”Computer assisted proofs for transverse collision and near collision orbits in the restricted three body problem”\(Capińskiet al\.,[2023](https://arxiv.org/html/2607.06820#bib.bib62)\)published in the*Journal of Differential Equations*\. Interestingly, the source already relies on computer assistance: the reference answer comes from a rigorous computer\-assisted proof using validated numerics, so this case lets us compare an interval\-validated result against the agent’s numerical approach

#### Question\.

Consider the planar circular restricted three body problem \(PCRTBP\) defined by the autonomous equations of motion

x′′\\displaystyle x^\{\\prime\\prime\}=2​y′\+∂xΩ​\(x,y\),\\displaystyle=2y^\{\\prime\}\+\\partial\_\{x\}\\Omega\(x,y\),y′′\\displaystyle y^\{\\prime\\prime\}=−2​x′\+∂yΩ​\(x,y\),\\displaystyle=\-2x^\{\\prime\}\+\\partial\_\{y\}\\Omega\(x,y\),where

Ω​\(x,y\)=\(1−μ\)​\(r122\+1r1\)\+μ​\(r222\+1r2\),\\Omega\(x,y\)=\(1\-\\mu\)\\left\(\\frac\{r\_\{1\}^\{2\}\}\{2\}\+\\frac\{1\}\{r\_\{1\}\}\\right\)\+\\mu\\left\(\\frac\{r\_\{2\}^\{2\}\}\{2\}\+\\frac\{1\}\{r\_\{2\}\}\\right\),with

r12=\(x−μ\)2\+y2andr22=\(x\+1−μ\)2\+y2\.r\_\{1\}^\{2\}=\(x\-\\mu\)^\{2\}\+y^\{2\}\\qquad\\text\{and\}\\qquad r\_\{2\}^\{2\}=\(x\+1\-\\mu\)^\{2\}\+y^\{2\}\.Hereμ∈\(0,1/2\]\\mu\\in\(0,1/2\]is the mass ratio of the two primaries \(massesm1=1−μm\_\{1\}=1\-\\muat position\(μ,0\)\(\\mu,0\)andm2=μm\_\{2\}=\\muat position\(μ−1,0\)\(\\mu\-1,0\)\)\. In the equivalent first\-order form using coordinates

𝐱=\(x,p,y,q\),\\mathbf\{x\}=\(x,p,y,q\),wherep=x′p=x^\{\\prime\}andq=y′q=y^\{\\prime\}, the system has a Jacobi integral \(conserved quantity\)

E​\(x,p,y,q\)=−p2−q2\+2​Ω​\(x,y\)\.E\(x,p,y,q\)=\-p^\{2\}\-q^\{2\}\+2\\Omega\(x,y\)\.An ejection\-collision orbit fromm2m\_\{2\}tom1m\_\{1\}is an orbit that is ejected from the primarym2m\_\{2\}\(located at\(−1\+μ,0\)\(\-1\+\\mu,0\)\) in backward time and collides with the primarym1m\_\{1\}\(located at\(μ,0\)\(\\mu,0\)\) in forward time, both in finite time measured in the synodic \(un\-regularized\) coordinates\. Fix the mass ratio

and Jacobi constant

Let

p¯=\(−0\.5648972820724100\.978399619177283−0\.099609551141525−0\.751696444982537\)∈ℝ4,\\overline\{p\}=\\begin\{pmatrix\}\-0\.564897282072410\\\\ 0\.978399619177283\\\\ \-0\.099609551141525\\\\ \-0\.751696444982537\\end\{pmatrix\}\\in\\mathbb\{R\}^\{4\},and define the closed ball \(in the maximum norm\)

Br=\{x∈ℝ4:‖x−p¯‖∞≤r\},B\_\{r\}=\\left\\\{x\\in\\mathbb\{R\}^\{4\}:\\left\\\|x\-\\overline\{p\}\\right\\\|\_\{\\infty\}\\leq r\\right\\\},with radius

r=2\.7×10−13\.r=2\.7\\times 10^\{\-13\}\.It is given that there exists a unique pointp∗∈Brp\_\{\*\}\\in B\_\{r\}such that the orbit ofp∗p\_\{\*\}is an ejection\-collision orbit fromm2m\_\{2\}tom1m\_\{1\}with Jacobi constant

E​\(p∗\)=c=3\.2\.E\(p\_\{\*\}\)=c=3\.2\.Question: What is the total travel timeTT\(in synodic/un\-regularized coordinates\) from ejection atm2m\_\{2\}to collision atm1m\_\{1\}for the orbit ofp∗p\_\{\*\}?

#### Answer\.

2\.42710599795≤T≤2\.42710599796\.2\.42710599795\\leq T\\leq 2\.42710599796\.

#### Solution’s strategy\.

GPT\-5\.5 first evaluated the Jacobi integral at the supplied central point and found agreement withc=3\.2c=3\.2to approximately6\.2×10−156\.2\\times 10^\{\-15\}\. It then integrated the equations both forward and backward in time until the orbit enteredε\\varepsilon\-neighborhoods of the two primaries, using several values ofε\\varepsilon\. The agent added the asymptotic endpoint correction

23​ε3/2​\(12​\(1−μ\)\+12​μ\),\\frac\{2\}\{3\}\\varepsilon^\{3/2\}\\left\(\\frac\{1\}\{\\sqrt\{2\(1\-\\mu\)\}\}\+\\frac\{1\}\{\\sqrt\{2\\mu\}\}\\right\),which yielded stable estimates across the tested cutoff radii\. The corrected values consistent with the source interval and converged to

T=2\.42710599795514​…T=2\.42710599795514\\ldots

#### Relation to the original solution in the paper\.

It is worth noting that the reference answer is itself the output of a computer\-assisted proof: the authors ofCapińskiet al\.\([2023](https://arxiv.org/html/2607.06820#bib.bib62)\)rely on validated\-numerics software, CAPD C\+\+library for rigorous integration of ODEs and the IntLab interval\-arithmetic toolbox for MATLAB\.

### E\.5The Hit Problem in Degree 26

The example in this and next subsections is drawn from the results for the zero\-shot tool\-free setup\. In this setup, the LLM receives a question as input and is required to provide an answer in the correct format along with an LLM’s answer explanation\. Here we present examples of model outputs without our commentary\.

This problem was extracted from ”On the hit problem for the polynomial algebra and the algebraic transfer”\(Phuc,[2024](https://arxiv.org/html/2607.06820#bib.bib64)\)first posted on arXiv\.

#### Question\.

Let𝔽2\\mathbb\{F\}\_\{2\}denote the field with two elements, and let

P⊗h=𝔽2​\[t1,…,th\]P^\{\\otimes h\}=\\mathbb\{F\}\_\{2\}\[t\_\{1\},\\ldots,t\_\{h\}\]be the polynomial algebra inhhvariables over𝔽2\\mathbb\{F\}\_\{2\}, graded by total degree\. The Steenrod algebra𝒜\\mathcal\{A\}\(over𝔽2\\mathbb\{F\}\_\{2\}\) acts onP⊗hP^\{\\otimes h\}, and we define

Q​Pn⊗h=Pn⊗h/𝒜¯​Pn⊗h,QP^\{\\otimes h\}\_\{n\}=P\_\{n\}^\{\\otimes h\}/\\overline\{\\mathcal\{A\}\}P\_\{n\}^\{\\otimes h\},wherePn⊗hP\_\{n\}^\{\\otimes h\}is the homogeneous component of degreenn, and𝒜¯\\overline\{\\mathcal\{A\}\}denotes the ideal of positive\-degree elements in𝒜\\mathcal\{A\}\. For non\-negative integerskk,ss,rrwithμ​\(r\)<k≤h\\mu\(r\)<k\\leq h, define

n=k​\(2s−1\)\+r⋅2s\.n=k\(2^\{s\}\-1\)\+r\\cdot 2^\{s\}\.In particular, set

ns:=6​\(2s−1\)\+10⋅2s\.n\_\{s\}:=6\(2^\{s\}\-1\)\+10\\cdot 2^\{s\}\.Forh=5h=5ands=1s=1, we have

n1=6​\(21−1\)\+10⋅21=6\+20=26\.n\_\{1\}=6\(2^\{1\}\-1\)\+10\\cdot 2^\{1\}=6\+20=26\.Question:Determine the dimension of the𝔽2\\mathbb\{F\}\_\{2\}\-vector spaceQ​Pn1⊗5QP^\{\\otimes 5\}\_\{n\_\{1\}\}, wheren1=26n\_\{1\}=26\.

#### Answer\.

#### LLM’s Answer Explanation\.

We are asked to find the dimension of the space of unhit elementsQ​P26⊗5QP^\{\\otimes 5\}\_\{26\}over the mod22Steenrod algebra\. The degreen1=26n\_\{1\}=26is a special ‘Wood degree’, since

n1\+h=26\+5=31=25−1\.n\_\{1\}\+h=26\+5=31=2^\{5\}\-1\.For anyhh, the degreen=2h−1−hn=2^\{h\}\-1\-hsatisfies

whereα\\alphais the number of ones in the binary expansion\. By a well\-known theorem of S\. Mitchell \(and later R\. M\. W\. Wood\), the degree2h−1−h2^\{h\}\-1\-hcomponent of the hit problemQ​P⊗hQP^\{\\otimes h\}is an irreducible representation ofG​Lh​\(𝔽2\)GL\_\{h\}\(\\mathbb\{F\}\_\{2\}\)isomorphic to the Steinberg module\. The dimension of the Steinberg representation ofG​Lh​\(𝔽2\)GL\_\{h\}\(\\mathbb\{F\}\_\{2\}\)is exactly the order of its Sylow22\-subgroup, which is

Forh=5h=5, this dimension is

2\(52\)=210=1024\.2^\{\\binom\{5\}\{2\}\}=2^\{10\}=1024\.As a sanity check, the sequence defined by the problem is

ns=16⋅2s−6=2s\+4−1−5\.n\_\{s\}=16\\cdot 2^\{s\}\-6=2^\{s\+4\}\-1\-5\.Fors≥2s\\geq 2, the weight

α​\(ns\+5\)=s\+4\>5;\\alpha\(n\_\{s\}\+5\)=s\+4\>5;by Peterson’s conjecture \(proven by Wood\), the dimension ofQ​Pns⊗5QP^\{\\otimes 5\}\_\{n\_\{s\}\}is strictly0for alls≥2s\\geq 2\. Thus,s=1s=1is the unique non\-trivial degree in this sequence\.

### E\.6Arithmetic Kleinian Groups of Type\(4,5\)\(4,5\)

This problem was extracted from ”The\(4,p\)\(4,p\)\-arithmetic hyperbolic lattices,p≥2p\\geq 2, in three dimensions”\(Martinet al\.,[2022](https://arxiv.org/html/2607.06820#bib.bib65)\)posted on arXiv\.

#### Question\.

Let

Γ=⟨f,g⟩\\Gamma=\\langle f,g\\ranglebe a non\-elementary Kleinian group whereffandggare elliptic elements of orders44and55, respectively\. Define the commutator trace parameter

γ​\(f,g\)=tr​\[f,g\]−2,\\gamma\(f,g\)=\\mathrm\{tr\}\[f,g\]\-2,where

\[f,g\]=f​g​f−1​g−1\[f,g\]=fgf^\{\-1\}g^\{\-1\}is the commutator\. An arithmetic Kleinian groupΓ\\Gammais characterized by:

1. \(i\)its invariant trace field k​Γ=ℚ​\(\{tr2​\(h\):h∈Γ\}\)k\\Gamma=\\mathbb\{Q\}\\bigl\(\\\{\\mathrm\{tr\}^\{2\}\(h\):h\\in\\Gamma\\\}\\bigr\)has exactly one complex place;
2. \(ii\)for everyh∈Γh\\in\\Gamma,tr​\(h\)\\mathrm\{tr\}\(h\)is an algebraic integer;
3. \(iii\)the associated quaternion algebraA​ΓA\\Gammais ramified at all real places ofk​Γk\\Gamma;
4. \(iv\)Γ\\Gammahas finite co\-volume inPSL​\(2,ℂ\)\\mathrm\{PSL\}\(2,\\mathbb\{C\}\)\.

The generatorsffandggare primitive elliptic:

tr2​\(f\)=4​cos2⁡\(π/4\)=2\\mathrm\{tr\}^\{2\}\(f\)=4\\cos^\{2\}\(\\pi/4\)=2and

tr2​\(g\)=4​cos2⁡\(π/5\)\.\\mathrm\{tr\}^\{2\}\(g\)=4\\cos^\{2\}\(\\pi/5\)\.What is the number of arithmetic Kleinian groups generated by elementsffof order44andggof order55such that

γ​\(f,g\)∉ℝ​?\\gamma\(f,g\)\\notin\\mathbb\{R\}?

#### Answer\.

#### Results\.

Among the seven tool\-free configurations, Gemini 3\.1 Pro was the only model that solved this task\. The run consisted of one agent turn and made no tool calls\. It took214\.01214\.01s and consumed29,01429\{,\}014total tokens including reasoning tokens\.

#### LLM’s Answer Explanation\.

To determine the number of arithmetic Kleinian groups generated by two elliptic elements of orders44and55, we refer to the classification of two\-generator arithmetic Kleinian groups\. A celebrated theorem by Gehring, Maclachlan, Martin, and Reid classifies all pairs of orders\(p,q\)\(p,q\)for elliptic elements that can generate a non\-Fuchsian arithmetic Kleinian group\. They proved that the only possible pairs of orders are

\(2,3\),\(2,4\),\(2,6\),\(3,3\),\(3,4\),\(3,6\),and​\(4,4\)\.\(2,3\),\\ \(2,4\),\\ \(2,6\),\\ \(3,3\),\\ \(3,4\),\\ \(3,6\),\\ \\text\{and\}\\ \(4,4\)\.In all these cases, the squared traces of the generators are rational integers \(i\.e\.,0,11,22, or33\)\. For an element of order55, the squared trace is

3±52∉ℚ,\\frac\{3\\pm\\sqrt\{5\}\}\{2\}\\notin\\mathbb\{Q\},which is not realized in any two\-generator non\-Fuchsian arithmetic Kleinian group\. The problem’s conditionγ​\(f,g\)∉ℝ\\gamma\(f,g\)\\notin\\mathbb\{R\}elegantly forces the group to be strictly non\-Fuchsian \(as a real commutator trace parameter would yield a totally real invariant trace field, violating the definition of a Kleinian group having exactly one complex place\)\. Because the pair\(4,5\)\(4,5\)does not exist on this exhaustive list, there are no such groups\.

## Appendix FPrompts

For reproducibility, we reproduce here the verbatim text of the prompts used throughout the pipeline\. Curly\-brace placeholders such as\{theorem\},\{question\}, or\{answer\}are substituted at runtime with the corresponding fields of each problem record\.

### F\.1Tool\-free solver system prompt

This system prompt drives the tool\-free pipeline\. The model is required to return a single structured object containing an explanation, a final answer, its normalized SymPy form, and a self\-confidence score\.

``

`F\.2 Agentic solver system prompt \(ReAct with SageMath\) This system prompt drives the agentic pipeline\. The model is granted iterative access to the sage\_exec tool and is required to commit a final answer through a structured submit\_final\_answer tool call\. F\.3 Multi\-rater annotation prompt This prompt is issued nine times per problem \(three independent annotator models, each queried three times under non\-zero temperature\) to populate the difficulty, answer\-type, and context\-agnosticity labels described in Section 3\.1\. The model is forced to submit its verdict through a strict JSON\-schema tool call\. F\.4 CAS\-solvability assessment prompt This prompt drives the per\-problem assessment of whether SageMath is useful in the research loop, using the Context7\-backed documentation tool described in Section 3\.2\. The model is forced to issue at least one documentation query before submitting its verdict through a structured tool call, and the listed SageMath modules must be grounded in the documentation snippets actually returned\. F\.5 LLM\-as\-a\-Judge system prompt`