Paper deep dive
The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning
Max Zimmer, Nico Pelleriti, Christophe Roux, Sebastian Pokutta
Intelligence
Status: succeeded | Model: google/gemini-3.1-flash-lite-preview | Prompt: intel-v1 | Confidence: 96%
Last extracted: 3/22/2026, 5:26:54 AM
Summary
This paper presents a practical guide and an open-source framework for AI-assisted research in mathematics and machine learning. It introduces a five-level taxonomy of AI integration, ranging from classical research to autonomous research associates, and provides a methodology using CLI coding agents within sandboxed containers to automate research workflows while keeping the human in the loop.
Entities (5)
Relation Signals (3)
Max Zimmer ā authored ā The Agentic Researcher Framework
confidence 98% Ā· The four authors approached AI-assisted research... The insights gained from these diverse experiences form the basis of the unified framework we present here.
Aletheia ā solved ā Mathematical Problems
confidence 95% Ā· Aletheia also solved several open problems from First Proof
The Agentic Researcher Framework ā utilizes ā CLI Coding Agent
confidence 95% Ā· turns CLI coding agents (e.g., Claude Code, Codex CLI, OpenCode) into autonomous research assistants
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:AI tools and agents are reshaping how researchers work, from proving theorems to training neural networks. Yet for many, it remains unclear how these tools fit into everyday research practice. This paper is a practical guide to AI-assisted research in mathematics and machine learning: We discuss how researchers can use modern AI systems productively, where these systems help most, and what kinds of guardrails are needed to use them responsibly. It is organized into three parts: (I) a five-level taxonomy of AI integration, (II) an open-source framework that, through a set of methodological rules formulated as agent prompts, turns CLI coding agents (e.g., Claude Code, Codex CLI, OpenCode) into autonomous research assistants, and (III) case studies from deep learning and mathematics. The framework runs inside a sandboxed container, works with any frontier LLM through existing CLI agents, is simple enough to install and use within minutes, and scales from personal-laptop prototyping to multi-node, multi-GPU experimentation across compute clusters. In practice, our longest autonomous session ran for over 20 hours, dispatching independent experiments across multiple nodes without human intervention. We stress that our framework is not intended to replace the researcher in the loop, but to augment them. Our code is publicly available at this https URL.
Tags
Links
- Source: https://arxiv.org/abs/2603.15914v1
- Canonical: https://arxiv.org/abs/2603.15914v1
Trouble viewing inline? Open PDF directly ā
Full Text
120,718 characters extracted from source content.
Expand or collapse full text
THE AGENTIC RESEARCHER: A PRACTICAL GUIDE TO AI-ASSISTED RESEARCH IN MATHEMATICS AND MACHINE LEARNING Max Zimmer ā Nico PelleritiChristophe RouxSebastian Pokutta Department for AI in Society, Science, and Technology, Zuse Institute Berlin, Germany Institute of Mathematics, Technische Universit Ģ at Berlin, Germany zimmer, pelleriti, roux, pokutta@zib.de Let me now wait for the final check: ā Task Output bwzs8ty88 1-hour mid-training status check Waiting for task (esc to give additional instructions) ā³ Gitifying... (8h 39m 19s Ā· ā 39.3k tokens Ā· thought for 20s) ā Tip: Run /install-github-app to tag @claude right from your Github issues and PRs Background tasks 10 active shells āÆ sleep 2700 && echo "ā” Final completion check ā”" && python3 &< 'PYEOF'... (running) sleep 3600 && echo "ā” 1h mid-training ā”" && python3 -c "... (running) sleep 5400 && echo "ā” Final completion check ā”" && for exp in E023_no_nor... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=6 uv run torchrun &-standalone &-npr... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=5 uv run torchrun &-standalone &-npr... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=4 uv run torchrun &-standalone &-npr... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=3 uv run torchrun &-standalone &-npr... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=2 uv run torchrun &-standalone &-npr... (running) source ~/.bashrc && CUDA_VISIBLE_DEVICES=1 uv run torchrun &-standalone &-npr... (running) Figure 1: A command-line interface (CLI) agent during an autonomous research session: over 8 hours in, managing six parallel GPU training runs and three scheduled monitoring tasks. The same framework supports mathematical derivations, proofs, and verification alongside computational ex- periments. The agent is idle, consuming no tokens while waiting for a status check to complete. ABSTRACT AI tools and agents are reshaping how researchers work, from proving theorems to training neural networks. Yet for many, it remains unclear how these tools fit into everyday research practice. This paper is a practical guide to AI-assisted re- search in mathematics and machine learning: We discuss how researchers can use modern AI systems productively, where these systems help most, and what kinds of guardrails are needed to use them responsibly. It is organized into three parts: (I) a five-level taxonomy of AI integration, (I) an open-source framework that, through a set of methodological rules formulated as agent prompts, turns CLI coding agents (e.g., Claude Code, Codex CLI, OpenCode) into autonomous research assistants, and (I) case studies from deep learning and mathematics. The framework runs inside a sandboxed container, works with any frontier LLM through existing CLI agents, is simple enough to install and use within minutes, and scales from personal-laptop prototyping to multi-node, multi-GPU experi- mentation across compute clusters. In practice, our longest autonomous session ran for over 20 hours, dispatching independent experiments across multiple nodes without human intervention. We stress that our framework is not intended to re- place the researcher in the loop, but to augment them. Our code is publicly avail- able at github.com/ZIB-IOL/The-Agentic-Researcher. ā We welcome contributions, issue reports, improvement suggestions, additional case studies via issues, PR, github.com/ZIB-IOL/The-Agentic-Researcher, to keep this up-to-date and useful. 1 arXiv:2603.15914v1 [cs.LG] 16 Mar 2026 1INTRODUCTION In 2024, DeepMindās AlphaProof (Hubert et al., 2025) combined with AlphaGeometry (Trinh et al., 2024) became the first AI system to achieve medal-level performance at the International Mathemat- ical Olympiad (IMO), reaching silver-medal standard by solving four of the six competition prob- lems through reinforcement learning and formal verification. AlphaEvolve (Novikov et al., 2025) demonstrated that LLM-guided evolutionary search can discover new mathematical constructions, rediscovering best-known solutions across a broad collection of problems and improving on them in several cases (Georgiev et al., 2025). Most recently, Aletheia (Feng et al., 2026b), an autonomous mathematical research agent, resolved several open problems originally posed by Erd Ģ os while op- erating with minimal human intervention. Aletheia also solved several open problems from First Proof (Abouzaid et al., 2026), a benchmark of previously unpublished research-level mathematics questions drawn from the authorsā own research process, within weeks of its release. These results are remarkable, and recent systems now address not only well-defined benchmarks but also genuine open mathematical problems. In parallel, the Machine Learning (ML) community has seen a surge in agentic experimentation: for instance, Karpathyās autoresearch (Karpathy, 2026) demonstrated how agents can run automated ML experiment pipelines through iterative code modification, and such pipelines are becoming increasingly common. Most of the current literature, including the works discussed above, focuses on what AI systems can achieve. Much less attention has been given to the complementary practical question of how researchers should integrate such systems into everyday research. In practice, research rarely pro- ceeds by pursuing a fixed objective from the outset: researchers must decide which questions to ask, which experiments to run, when to reformulate a conjecture, and how to respond to unexpected results. Supporting this kind of work requires workflows that accommodate shifting objectives, it- erative experimentation, and sustained human guidance, yet how to build and use such workflows remains an open question. For most researchers, the challenge is not building a discovery pipeline from scratch but understanding which tools are available and how to use them effectively. A growing body of work has begun to map this landscape, including conceptual frameworks for human-AI co-creativity (Haase & Pokutta, 2026), visions of the āaugmented mathemati- cianā (Henkel, 2025), formal-proof assistants (Yang et al., 2023; Song et al., 2025), and numerous first-hand accounts of AI-assisted research (Bubeck et al., 2025; Diez et al., 2025; Alexeev & Mixon, 2026; Ivanisvili & Xie, 2025; Feldman & Karbasi, 2025; Salim, 2025; Dobriban, 2025; Schmitt, 2025). Avigad (2026) make this point especially clearly: mathematicians should not merely react to AI but should take an active role in deploying and shaping it for their own purposes. Yet none of these works provides actionable, end-to-end guidance that a researcher could follow today. We hope to make some progress on these questions and aim to fill parts of that gap. The frameworks, approaches, and insights presented here have been developed over roughly the last one and a half years in the context of the MATH+ project Agentic AI in Mathematics 1 but apply beyond mathemat- ics and have proven to be very powerful, e.g., in ML research. This also explains our choice of use cases in machine learning and mathematics. The four authors approached AI-assisted research from complementary directions: some built on existing CLI coding agents with either an experimental or a theoretical and proof-oriented focus, while others developed a custom multi-agent system from scratch. The insights gained from these diverse experiences form the basis of the unified framework we present here. Contributions. Our contributions are as follows. 1. A practical taxonomy (Section 2). We identify five levels of AI integration into mathematical and ML research, ranging from full human control to high agent autonomy. 2. An open-source, sandboxed agentic research framework (Section 3). We present a set of methodological rules, formulated as agent prompts, which we call commandments, together with a sandboxed container environment and reporting conventions that turn general-purpose CLI cod- ing agents into autonomous research assistants. The commandments encode the norms of scien- tific practice and guide the agent throughout the research workflow. The framework is model- and harness-agnostic, supports any frontier LLM through existing CLI agents (such as Claude 1 https://iol.zib.de/project/agentmath.html 2 Code (Anthropic), Codex CLI (OpenAI), or OpenCode (Anomaly)), and can be set up within minutes. 3. Case studies (Section 4). We demonstrate the framework in action across diverse domains, including deep learning as well as pure and applied mathematics, illustrating both successes and failure modes. We provide screenshots of the agentās reports as they were produced. We want to emphasize what this paper is not: we do not claim that AI replaces research creativity, insight, or the researcher. Rather, we demonstrate that specific parts of the research workflow can be significantly accelerated when a researcher directs an AI agent in a structured way. Unlike ap- proaches that seemingly remove the human from the research process entirely (cf., e.g., Lu et al., 2024), our framework keeps the researcher as the principal investigator, who can now operate at greater scale and speed. We believe that mathematical research is not a fully automatable task, and we will not speculate on whether this will change in the future. What we do claim is that mathe- maticians and researchers in general should take an active role in this partial transformation of the field and, echoing Avigad (2026), should own the technology. The rest of this paper is organized as follows. Section 2 presents our taxonomy of integration levels. Section 3 describes the agentic research framework in detail, the core contribution of this paper. Section 4 presents case studies, and Section 5 concludes with lessons learned, limitations, and future directions. We defer the survey of related work to Section 6 at the end of the paper. 2LEVELS OF AI INTEGRATION IN MATHEMATICAL AND ML RESEARCH Inspired by Haase & Pokutta (2026), we propose a taxonomy of five levels that characterize how deeply AI is integrated into the research process, ranging from no AI involvement to fully au- tonomous research loops. These levels are not mutually exclusive, and a researcher might use dif- ferent levels for different tasks, all within the same project. In particular, even (fully) autonomous systems can delegate subtasks to less autonomous components. This regularly happens also in our setup when subagents are spawned to accomplish subtasks. In general, the key lies in recognizing which level is appropriate for which task. Table 1 summarizes the taxonomy, and we describe each level in detail below. Level 0: Classical. The classical level is the baseline of our taxonomy and the traditional mode of mathematical and ML research. The researcher uses all traditional computational tools, includ- ing typesetting software (e.g., L A T E X), mathematical software (e.g., Mathematica, MATLAB), and programming languages for custom implementations (e.g., Python, Julia, PyTorch), but no AI as- sistance. This remains the predominant mode of research and is perfectly appropriate. The goal of this paper is not to argue that AI should render it obsolete, but to show when and how AI can complement it. Table 1: Five levels of AI integration in mathematical research. Each (not necessarily mutually exclusive) level represents a qualitatively different trade-off between agent autonomy and human involvement. Level NameToolsAI TasksHuman Role 0ClassicalL A T E X, math. software No AI integrationEverything 1ConsultantLLM chatbotsTargeted queries for explanation, lit- erature, brainstorming Asks, evaluates 2TypistEditor plugins (Copilot, Cursor) Code and text generation without execution Thinks, reviews, decides 3CollaboratorCLI coding agentsHuman describes task, AI imple- ments and iterates Reviews each output, assigns next task 4Research Assoc. Our frameworkAutonomous experiment loop fol- lowing structured research plan Steers, audits 3 Level 1: AI as Consultant. The researcher uses LLM-based chatbots (e.g., ChatGPT, Claude, Gemini) for specific queries and assistance. Typical cases include concept explanation (Explain the difference between strong and weak duality in linear programming), literature search (What are the current best convergence rates for SGD with heavy-tailed noise?), brainstorming (What techniques exist for proving convergence of iterative algorithms when the operator is only approximately con- tractive?), and debugging ideas (Here is my proof attempt. Where does the argument break down?). The core intellectual work remains with the researcher; the AI provides targeted assistance. The key skill is asking the right questions and crafting sufficiently detailed prompts to guide the AI toward a useful answer. A clear limitation is that the interaction is stateless across sessions unless the user manually provides context. Getting started: A web browser and access to an LLM chatbot (free tiers available from most providers). No setup required. Level 2: AI as Typist. The researcher uses AI for code and text generation, ranging from tab completion (e.g., GitHub Copilot predicting the next line) to more complex prompt-based generation that produces entire functions or L A T E X paragraphs from a natural-language description. Every output is reviewed by the researcher and accepted, edited, or rejected. The defining characteristic of this level is that the AI generates code or text but neither executes nor iterates on the results. The researcher remains responsible for all design decisions, and the AI accelerates the writing process without closing the loop between implementation and evaluation. Getting started: Install a code editor plugin (e.g., Cursor, or VS Code with GitHub Copilot). Level 3: AI as Collaborator. The full implementation and execution are delegated to a CLI cod- ing agent, i.e., a terminal-based tool (e.g., Claude Code (Anthropic), OpenCode (Anomaly), Codex CLI (OpenAI)) that can read and edit files, execute shell commands, and iterate on results within a persistent project context. This differs qualitatively from Levels 1ā2 because the agent possesses a much broader set of capabilities, including file modifications, code execution, and iteration based on results it has obtained, all within a single conversation. For a prompt like āImplement the Frank- Wolfe algorithm for the semidefinite relaxation of max-cut, with step size Ī³ t = 2/(t + 2)ā or āIm- plement a learning rate scheduler with linear warmup,ā the agent reads the codebase, implements the algorithm, runs it, and re-evaluates if convergence shows unexpected behavior. The researcher describes each task in natural language and provides the necessary context, such as an existing codebase. After each completed task, the researcher reviews the output, decides what to do next, and assigns the next task; the agent handles how. At no point does the agent independently set the research direction. Getting started: Install a CLI coding agent and start a session in the project directory. Level 4: AI as Research Associate. The highest degree of autonomy in our taxonomy. The re- searcher arrives with a research idea (initial intuitions, failed strategies, partial results, or simply a well-posed question) and outlines a research plan: goals, metrics, constraints, approaches al- ready tried, and promising directions to explore. The agent then formulates a detailed plan and autonomously executes an experiment loop: formalizing mathematical ideas, implementing ap- proaches, running evaluations, recording results, analyzing outcomes, and updating both a structured research report and a TODO.md. It iterates this loop, continuously refining and expanding the plan, operating for hours to days to achieve the research goal or uncover something unexpected. To operate for extended periods, structured and clear instructions that govern scientific rigor, docu- mentation, and verification are needed: our framework (Section 3) provides exactly these. The key difference from Level 3 is that the agent does not wait for human input between experiments but follows a research plan and a set of commandments encoding the norms of good scientific practice: one variable per experiment, structured reporting, staged evaluation (from quick sanity checks to full benchmarks), and verification protocols, among others (cf. Section 3). Intermittent human review and course correction are an integral part of Level 4, not a fallback to Level 3: the researcher period- ically inspects the report, adjusts priorities, and refines the research plan while the agent continues to execute autonomously. The researcherās role shifts from execution to direction-setting, periodic review, and evaluation. Level 4 is most appropriate when the search space is large. 4 Concept Research Question Problem formulation, hypotheses, objectives, evaluation criteria Tools, Methods & Data Software stack & packages, datasets, compute resources, custom scripts Prior Work & Domain Knowledge Existing codebase, L A T E X notes & derivations, references, preliminary results In practice Examples: CASE STUDY A Deep Learning Improve LLM pretraining: exploit Muonās memory savings over AdamW PyTorch, CUDA, uv, FineWeb dataset, multi-GPU allocation LLM pretraining benchmark codebase CASE STUDY D Mathematics Prove lower bounds for Frank-Wolfe on uniformly convex sets Python, Julia, uv Two recent lower-bound proofs for the strongly convex case as references Figure 2: Setting up a research project. Top: the three categories of input the researcher provides, with their conceptual role (dark) and concrete realization (light). Bottom: two examples from our case studies: a deep learning project (Section 4.1) and a mathematics project (Section 4.4). Despite the guardrails described in Section 3, limitations remain. The agent may pursue an unpro- ductive direction for too long, especially when the research plan lacks sufficient detail. Verification is only partially solved: while we provide strategies for symbolic and numerical verification of math- ematical claims and implementations, a high (to full) degree of certainty requires the researcher to perform a rigorous review of the work. We consider this a feature, not a bug. Similarly, while the agent is instructed to search the literature, it cannot guarantee that its ideas are genuinely novel. Thorough knowledge of the related work remains the researcherās responsibility. As such, the re- searcher still faces a non-trivial amount of work both throughout and toward the end of a project: reviewing intermediate results and providing steering, verifying correctness, deciding what results merit publication, and confirming originality as well as adding context and interpretation. However, instead of conducting the entire research process alone, the researcher now externalizes parts of the work to a capable research associate who delivers a structured, well-documented report. This report then requires careful and rigorous review with subsequent steering and guidance. Through repeated interactions of this kind, new results emerge in a process of Human-AI co-creation. Getting started: Clone the project repository 2 and follow the setup instructions in the README.md. The setup takes a couple of minutes, and the first autonomous experiments can begin immediately. A detailed description of the framework initialization is given in Section 3.1. 3THE AGENTIC RESEARCH FRAMEWORK We describe our core contribution: the agentic research framework, its design principles, and the ten commandments, distilled from our own experience, that guide the agentās behavior. The instructions described in the following subsections are provided to the agent through a persistent instruction file (INSTRUCTIONS.md) that is read at the start of every session. This configuration file contains universal instructions as well as a final section that serves as a template placeholder for project- specific instructions; these are automatically filled in by the agent once the researcher provides the research instructions. 3.1OVERVIEW AND WORKFLOW To start a new project, the researcher provides three things (Figure 2): a research question (problem formulation, hypotheses, evaluation criteria), the tools, methods, and data needed to investigate it (software stack, packages, datasets, compute resources), and any prior work or domain knowledge that should inform the investigation (existing codebase, L A T E X notes with derivations, references, preliminary results). In the following, we will use the term experiment to refer to one (broad) agentic iteration loop with the researcher: depending on the context, this can be one proof attempt, an actual computational experiment, or the design of a new algorithm. The framework is built around 2 github.com/ZIB-IOL/The-Agentic-Researcher 5 CLI coding agents, e.g., Claude Code (Anthropic), Codex CLI (OpenAI), Gemini CLI (Google), or OpenCode (Anomaly), which operate inside a sandboxed container that provides a secure, isolated workspace. Starting a new project. The typical workflow is as follows: 1. The researcher begins in a project directory that contains the practical-layer materials described above (Figure 2). From this directory, they launch the sandbox and provide the research instruc- tions to the agent. The more detailed the instructions, the better; we found it especially useful to provide a working codebase if one exists, along with a L A T E X write-up of the research problem and previously tried approaches. 2. The agent asks clarifying questions about scope, constraints, and evaluation metrics. 3. After this back-and-forth, the agent explores all relevant files and writes the final project-specific instructions into a persistent instruction file (INSTRUCTIONS.md), alongside the universal commandments that are already in place (Section 3.2). 4. The agent creates a plan and initializes report.tex and TODO.md, the two main artifacts of the research process. Upon approval by the researcher (or after further refinement of the plan), the agent begins autonomous execution and only requires human intervention in case of unexpected behavior or when the research plan needs adjustment. Why CLI agents. Across our research workflows, three practical requirements arose repeatedly. CLI agents are easy to use: they fit naturally into local working environments, can be launched inside an existing project, and operate directly on local files without additional infrastructure. They remain fully interactive: the researcher can intervene at any point to inspect progress, redirect the investigation, stop execution, or restart with revised instructions. Finally, they are extensible: the toolchain can be readily extended with custom utilities; in our case, this included scripts for handling literature and L A T E X sources, extracting relevant algorithmic sections, and running specialized search and verification routines. The same mechanism also supports hard guardrails: automated checks can be triggered after file edits or experiment runs, enforcing formatting, running tests, or updating reports. Because CLI agents are maintained by model providers and evolve with model capabilities, while our rules sit on top, the framework automatically benefits from improvements to the underlying tools. Figure 1 shows an autonomous session in practice. Infrastructure. Because the framework is built around CLI agents, the surrounding infrastructure can remain intentionally minimal. The sandbox confines all actions to a container, enabling unat- tended sessions without the risk of damaging the host system. For compute-intensive projects, a multi-node launcher dispatches independent experiments to remote Slurm nodes. We recommend using reproducible, project-local package managers (uv for Python, Juliaās Pkg, among others). Structured reporting and experiment tracking. All experimental progress is recorded in a single L A T E X file (report.tex) that accumulates experiments, derivations, and analysis, complemented by a TODO.md checklist for open questions, unverified claims, and deferred work. Each experiment subsection must contain the following fields, enforced by the commandments (Section 3.2): Listing 1: Required fields for each experiment in report.tex. Goal What problem are we solving? Hypothesis Why should this approach work? Method Mathematical formulation with proper notation. Implementation Files and lines changed. Results Table with method, model/instance, metric, delta. Analysis Why it worked or didnāt. What it reveals. Next Steps What to try based on these results. Rather than introducing a separate experiment-tracking system, we use Git directly. Each experiment is recorded as a commit with a structured message of the form exp(EXXX): <description> -- <metric>=<value>. Branches group related experiments, tags mark important outcomes, and Gitās worktree feature allows multiple agent sessions to run concurrently on separate copies of 6 Researcher Instruction File CLAUDE,GEMINI,AGENTS.md CLI Agent Sandbox Python, L A T E X, Git, GPU promptsgoverns runs in reports back 1 Explore 2 Plan 3 Implement 4 Evaluate 5 Analyze 6 Record 7 Commit 8 Iterate Experiment Loop VI: one variable VIII: bound expectations V: make it work I: honest evaluation VII: three tiers X: verify before claiming I: verify citations IX: record everything I: keep promises IV: complete all work Git history report.tex /TODO.md All steps governed by the Ten Commandments in Section 3.2. Figure 3: Overview of the agentic research framework. Top: The researcher writes a persistent instruction file that governs the CLI agent operating within a sandboxed environment. Bottom: Each experiment follows an eight-step loop. the codebase without interference. This keeps the full experimental history lightweight, portable, and directly searchable through Git logs. Once running, each experiment follows the eight-step loop shown in Figure 3: Exploreā Planā Implement ā Evaluate ā Analyze ā Record ā Commit ā Iterate. At the beginning of every session (or after a context window reset), the agent re-reads report.tex, TODO.md, and the git log to restore continuity. 3.2THE TEN COMMANDMENTS At the core of our framework are the lessons we distilled through experimentation into ten com- mandments that apply independently of the specific domain and research problem. They form a major part of the instructions given to the agent. The full instructions are available in our repository. In deriving the ten commandments through continuous improvement of the agentās behavior, we followed three guiding principles: (1) explicit over implicit: language models follow instructions literally; implicit expectations (āobviously you should record your resultsā) are reliably violated, so every important behavior must be stated as a rule; (2) falsifiable over aspirational: ābe rigorousā is not a commandment, āchange exactly one variable per experimentā is, allowing both human and agent to assess compliance; (3) failure-driven over theory-driven: every commandment exists be- cause we observed a specific failure mode in practice, not because it seemed theoretically desirable. The commandments are grouped into categories, each addressing a specific aspect of the research process. Below, we state each rule and describe the failure mode it addresses. We present slightly shortened versions for brevity; the full prompts are available on GitHub. At the implementation level, each commandment is a prompt-engineering directive; we found that naming and structuring these behaviors as explicit rules makes them significantly easier to maintain, debug, and iterate on. 7 3.2.1INTEGRITY AND TRUST The following three commandments address the integrity of the agentās promises and announced actions. I. Never Break a Promise If you say āI will do X,ā do it. Under-promise, over-deliver. Failure mode: In early experiments, the agent frequently stated intentions (āI will now run the full evaluationā) and then skipped steps or moved on to different tasks. After adding the commandment, the agent either follows through on all stated tasks or states upfront which tasks will be deferred and why. I. Never Manipulate Evaluation Do not change metrics, test sets, fixed hyperparameters, or problem definitions. Do not hard- code results or cherry-pick seeds. Failure mode: The agent subtly changes evaluation conditions to make results look better. The LLM may adjust evaluation parameters āhelpfullyā to reach its goal, but this is not a genuine improvement. For instance, the agent changed the number of evaluation samples to āspeed up evaluationā, which happened to produce better metrics and created an unfair advantage over baseline methods. I. Never Fabricate Citations Every bibliography entry must be verified against the actual source before adding it. Search for the paper via web search. Confirm the exact title, full author list, year, venue, and identifier from the source. If you cannot find the paper, do not guess. Never write a citation from memory alone. Failure mode: This commandment aims to address a well-known limitation of these systems: they hallucinate plausible but incorrect bibliographic entries. 3.2.2AUTONOMY AND EFFICIENCY A major problem we encountered was that, despite having a long todo-list of potential tasks and experiments, the agent consistently stopped to ask whether it should continue. The following two commandments aim at maximizing productive work within each session. IV. Complete All Autonomous Work Before Reporting Finish every task that does not need user input. Report once with all results. Never skip work because you estimate it ātakes too long to implementā. Failure mode: The agent frequently stops to ask whether it should continue, even when the research plan specifies many more experiments that could be executed without additional input from the researcher. A related failure mode is that the agent often discards approaches because they āwould take too long to implementā and potentially āonly have modest impactā. Modest impact aside, agents drastically underestimate their own coding speed; in fact, the implementation typically takes less than a minute. The only valid time concern is actual compute runtime measured in days. V. Make It Work Before Moving On An experiment crash is a bug, not a bad idea. Do not discard methods because of implementa- tion failures. Investigate, fix, and re-run. Failure mode: When encountering an implementation failure, agents often claim that the approach ādoesnāt workā and move on to an alternative. In practice, however, most of these crashes are simple bugs that can be fixed easily. For instance, when hitting an out-of-memory error, the agent concluded that the method ādoesnāt scaleā. Upon further investigation, it found an unnecessary materialization 8 of a memory-intensive matrix, replaced it, and the method ran successfully, yielding significant improvements over the baseline. 3.2.3SCIENTIFIC RIGOR The following three commandments ensure that the agent follows the norms of scientific practice. VI. One Variable per Experiment Change exactly one thing per experiment. If two things change and the metric improves, you cannot know which helped. Failure mode: If one experiment is successful and the agent has an idea for further improvement, it is often tempted to combine both the successful change and the new idea simultaneously in the next experiment. This makes it impossible to determine which change caused the improvement. VII. Evaluate in Tiers Tier 1 (seconds): does it run without crashing? Tier 2 (minutes): any signal on a small subset? Tier 3: full evaluation, i.e., the real metric that goes into the report. Use small-scale runs to catch bugs only. Never draw conclusions from small-scale results. Failure mode: We want the agent to iterate quickly and distinguish between trivial and meaningful improvements. Consequently, we enforce that the agent (a) does not run a full, potentially expensive evaluation after every minor code change, and (b) does not discard ideas based on unsuccessful small-scale runs on toy problem instances. VIII. Bound Your Expectations Before implementing a heuristic, identify the theoretical best case, even if it is not realizable in practice. If you are ācorrectingā something, measure how much correction is theoretically possible. Failure mode: To decide whether a method is successful, it is crucial to understand a theoretical upper bound on the possible improvement. The agent often observes a small improvement and reports it as a success, without assessing proximity to the theoretical maximum. 3.2.4DOCUMENTATION AND REPRODUCIBILITY The following two commandments ensure that the agent documents its work reproducibly. This is one of the most important categories, as it enables restarting the research process from any given point. IX. Record Everything Every experiment gets a subsection in the report: goal, hypothesis, method, results table, anal- ysis, next steps. Include failures. If it is not in the report, it did not happen. Visualize, donāt just describe: create plots for distributions, comparisons, and scaling. Maintain TODO.md as a living checklist for open questions, unverified claims, and deferred work. Failure mode: Without the rule, the agent runs experiments, observes results, and keeps them in its context window. As soon as this context window is compacted or cleared, the information is lost. At the same time, the strict rule āif it is not in the report, it did not happenā ensures that the agent does not mistakenly believe it has already obtained a result that was never recorded. Apart from the report, which we save as a L A T E X document, we also maintain a TODO.md file, which is equally critical, as it prevents the agent from forgetting about open questions, unverified claims, and deferred work. 9 X. Verify Before Claiming Assume you are wrong until verified. Write verification scripts, not just explanations. Actively try to falsify your own claims, test edge cases, randomize inputs, search for counterexamples. Grade claims: verified, partially verified, or unverified. Failure mode: Mathematical verification remains a major challenge for LLMs. We observed signif- icant improvements when enforcing at least numerical verification of claims. For instance, the agent derives a formula whose derivation contains an error (e.g., a missing factor of two), but the results look plausible. A verification script that checks the formula against a brute-force computation on small instances catches this immediately and prevents the agent from continuing its argument on a false premise. This active falsification, i.e., the process of deliberately trying to break your own hypothesis before confirming it, often reveals the key structural insight that makes the proof work. 3.3DOMAIN-SPECIFIC COMMANDMENTS The ten commandments presented above are intended to be universal. In addition, we found it beneficial to provide domain-specific commandments tailored to the research style of the domain, whether primarily theoretical or empirical. Beyond these broad categories, further specialization is useful: for instance, research in a specific subfield of mathematics benefits from commandments tailored to its particular challenges. Domain: Compute-Intensive Research. For empirical projects involving GPU experiments, deep learning, or large-scale numerical simulations, we apply the following additional command- ments: ā¢ One experiment per GPU; use them all (C1). Check nvidia-smi before every batch of work. Assign each independent experiment to its own GPU. Never leave GPUs idle when independent tasks remain. ā¢ Context window hygiene (C2). Prefer redirecting long-running output to log files and monitoring with tail. Only investigate logs in detail if something looks wrong. ā¢ Memory management (C3). When observing out-of-memory (OOM) errors, do not conclude that the method ādoes not scaleā. Instead, systematically reduce memory: clear the GPU cache be- tween experiments (torch.cuda.empty cache()), enable gradient checkpointing, or pro- cess layers sequentially instead of in parallel. Print torch.cuda.memorysummary() to identify the allocation that causes the spike. Only after these mitigations fail is it valid to report a genuine scaling limitation. ā¢ Discover nodes first; dispatch independent experiments (C4). When a multi-node Slurm allo- cation is active, discover available nodes at session startup and dispatch independent experiments to remote nodes via remote-run. Each dispatched job runs in its own container on the tar- get node with full GPU access. Never dispatch dependent work: only experiments that are fully independent may run on remote nodes. Domain: Mathematical Research. For theory-heavy projects involving proofs and derivations, we apply the following additional commandments: ā¢ Derivations before code (M1). Write derivations step-by-step before implementing. Cross- reference paper equations. Before implementing a new method, search for prior work to flag potential rediscovery. ā¢ Precise notation (M2). Use precise index notation (G j , not G j , for diagonal elements of a matrix). Define all notation before first use; dimensions, ranges, scalar vs. vector vs. matrix. Apply the same rigor to negative results as to positive ones. ā¢ Counterexample-first reasoning (M3). Before attempting a proof, actively search for coun- terexamples: randomize inputs, test boundary cases, enumerate small instances exhaustively. If a counterexample exists, the search finds it faster than a failed proof attempt reveals the obstruction. If no counterexample survives, the search often exposes the structural property that makes the proof work. 10 4CASE STUDIES We present case studies demonstrating the framework across different research domains and integra- tion levels. The first three (AāC) deal with LLM-related research questions: pretraining, pruning, and quantization. The remaining three (DāF) concern mathematical research: convex optimization, combinatorial optimization, and algebraic geometry. Each case study follows a consistent structure: domain, problem, what the agent did, results, and lessons learned. Throughout, we include fig- ures, screenshots, and excerpts from the agentās reports as they were produced (indicated by a thin border); minor errors or rendering artifacts are preserved and marked with [sic] where appropriate. 4.1SYSTEMATIC OPTIMIZER EXPLORATION FOR LLM PRETRAINING This case study demonstrates the frameworkās core experimental loop on a computationally intensive deep learning task: systematic, single-variable experimentation across a non-trivial optimizer design space, with multiple GPUs running independent experiments in parallel. Domain and problem. AdamW (Kingma & Ba, 2014; Loshchilov & Hutter, 2017) has long been the dominant optimizer for language model pretraining. It maintains two buffers per parameter (first and second moments), requiring additional memory 2N compared to vanilla Stochastic Gradient Descent (SGD), where N is the number of parameters. The Muon optimizer (Jordan et al., 2024) takes a fundamentally different approach: instead of adaptive step sizes, it computes a momentum vector M t = Ī¼M tā1 + G t and then applies Newton-Schulz (NS) orthogonalization to approximate UV ā¤ from the Singular Value Decomposition (SVD) of the momentum buffer M t = U Ī£V ā¤ , so that W t+1 = W t ā Ī· Ā· NS(M t ). This operation equalizes all singular values of the update and achieves strong results on LLM pretraining while using only N additional memory units (one momentum buffer) compared to SGD, half of AdamWās 2N . A natural question arises: can the spare N memory budget be exploited to make Muon better? The agent was given this open-ended research question, the codebase of Semenov et al. (2025) as a standardized LLM pretraining benchmark (124M-parameter Llama on FineWeb, 10,000 iterations), and a multi-GPU compute allocation. What the agent did. After establishing baselines (Muon, AdamW), the agent explored modifica- tions to the Muon update rule, changing exactly one variable per experiment (Commandment VI). The central insight was that Muon converges faster when the vector it orthogonalizes is well- conditioned: normalizing the momentum buffer before orthogonalization means the same number of iterations yields a better update. The agent tested multiple normalization strategies, swept hy- perparameters one at a time, and discovered two independent improvements: (1) a normalization technique applied before orthogonalization, and (2) the addition of weight decay to Muonās matrix parameters. Weight decay is a standard regularization technique and its benefit is not surprising in itself; however, the reference codebase implemented Muon without it, and because the agent tested each modification in isolation (Commandment VI), it was able to quantify this contribution separately and still identify the normalization improvement on top of it. A zero-overhead variant re- quiring no extra buffer was found to achieve nearly identical results. Following Commandment IX, each of the more than 40 experiments was documented in the agentās report.tex with goal, hypothesis, method, results table, and analysis. The agent also identified several independent papers exploring normalization in the context of Muon: NorMuon (Li et al., 2025), AdaMuon (Si et al., 2025), and Muon+ (Zhang et al., 2026), each propos- ing a different normalization strategy. It implemented two of these methods in its codebase and ran a detailed comparison, analyzing the theoretical and empirical differences between the approaches (Commandment V). The existence of multiple concurrent works exploring the same design space underscores the need to carefully characterize how the agentās approach relates to and differs from each of them. While the agent conducted thorough literature searches, we cannot guarantee that its specific combination of modifications is truly novel. Accordingly, we keep the presentation at a high level and view these results primarily as initial directions to build on: the experiments are limited to a single architecture and dataset, and a full comparison across model scales, training se- tups, and concurrent methods would be necessary to draw any definitive conclusions. A standalone publication would further require a more in-depth prior-art investigation to establish precisely which aspects, if any, are new. 11 33.033.534.034.535.035.536.036.537.0 Final validation perplexity (lower is better) AdamW Muon row-norm (lr=0.01) pre-NS (lr=0.01) pre-NS + wd=0.1 row-norm + wd=0.1 row-norm + wd=0.05 pre-NS + wd=0.03 pre-NS + wd=0.05 36.254 35.128 34.075 (3.0%) 34.018 (3.2%) 33.705 (4.1%) 33.698 (4.1%) 33.427 (4.8%) 33.423 (4.9%) 33.352 (5.1%) Muon baseline (35.128) AdamW (36.254) Figure 4: Final validation perplexity [sic] from the agentās report in Section 4.1. Lower is better. The dashed line marks the Muon baseline; the agentās modifications achieve ā¼5% improvement over Muon andā¼8% over AdamW. 02k4k6k8k10k Training iteration 30 40 50 60 70 80 90 100 Validation perplexity (a) Full training Muon AdamW NewMuon (pre-NS) NewMuon (best) NewMuon (row-norm) 7k7k8k8k9k9k10k Training iteration 33 34 35 36 37 38 39 40 Validation perplexity 35.13 33.35 (b) Final 3000 iterations Figure 5: Training curves [sic] from the agentās report in Section 4.1. Left: full training run. Right: final 3,000 iterations (zoomed). The agentās optimizer modifications consistently outperform both Muon and AdamW baselines throughout training, not only in the final iterations. Note that here, the agent named the new method NewMuon, which is inconsistent with the naming in Figure 4. Results. Across more than 40 experiments documented in the agentās report.tex, the best configuration achieved a ā¼5% improvement in validation perplexity over Muon (and ā¼8% over AdamW) at the same 2N memory budget as AdamW (Figure 4). The two improvements are nearly additive: normalization alone providesā¼3%, weight decay aloneā¼2%, and the combinationā¼5% (Figure 5). The zero-overhead variant achievesā¼4.8% improvement at the same N memory foot- print as baseline Muon, within a fraction of a perplexity point of the full method. Results were replicated across random seeds and a broader hyperparameter sweep. Lessons learned. The one-variable-at-a-time commandment (Commandment VI) was critical in this design space: the agent discovered that normalization and weight decay provide independent, nearly additive improvements only because it tested each in isolation before combining them. A 2Ć2 factorial ablation (normalizationĆ weight decay) confirmed the near-additivity, which would have been obscured by testing them jointly from the start. An interesting aspect of the agentās research behavior is that, while the task explicitly granted an extra N memory budget, the agent proactively 12 explored whether the same gains could be achieved without it, and found a zero-overhead variant that nearly matched the full method at the same N memory footprint as baseline Muon. The entire ses- sion ran for over twenty hours without human intervention. With multiple GPUs available, the agent ran independent experiments in parallel (one per GPU, Commandment C1); the frameworkās multi- node dispatch capability (Section 3.3) enables large-scale concurrent experiments across compute nodes. Despite the long wall-clock time, actual token consumption remained modest: most time was spent waiting for training runs to finish while the agent redirected output to log files and monitored progress with lightweight commands (Figure 1), as encouraged by Commandment C2. The frame- workās emphasis on literature verification (Commandment I) prompted the agent to proactively search for related work, identify concurrent papers, and implement their methods for comparison. While this is a useful first step, the limitations noted above show that such automated searches are not a substitute for the thorough prior-art investigation a human researcher would conduct before claiming novelty or asserting that the resulting method truly outperforms concurrent approaches. 4.2WEIGHT RECONSTRUCTION IN LARGE LANGUAGE MODEL PRUNING This case study illustrates a characteristic side effect of the agentic framework we propose: the agent was tasked with one research objective and discovered a different, more effective technique along the way (i.e., we observed serendipity). Domain and problem. Pruning large language models (LLMs) reduces memory and compute costs by zeroing out weights, i.e., selecting a binary sparsity mask M ā 0, 1 d out Ćd in per weight matrix (cf., e.g., Zimmer et al., 2023a; Frantar & Alistarh, 2023; Sun et al., 2024). The constraints on M determine the sparsity pattern and, with it, the potential for hardware acceleration: unstructured sparsity removes arbitrary individual weights (Han et al., 2015; Zimmer et al., 2023b; 2024; 2025), while semi-structured patterns such as N :M (Mishra et al., 2021; Zhang et al., 2023; Lasby et al., 2025) impose structure that is more amenable to hardware acceleration. The core challenge across all settings is mask selection: choosing which weights to zero out so that the pruned networkās output remains close to the original (Roux et al., 2025; Zimmer et al., 2026). Once a mask is fixed, the pruned modelās performance degrades compared to the dense original; one way to counteract this is weight reconstruction, i.e., adjusting the surviving weights to compensate for the removed connections (Frantar & Alistarh, 2023). Calibration data is drawn from C4 (Raffel et al., 2020); quality is measured by perplexity on the WikiText (Merity et al., 2016) test set (lower is better). The project started with a concrete task: we had developed a pruning approach that aimed to find better masks, but it produced inconsistent results, sometimes failing catastrophically. The agent was provided with an existing codebase containing implementations of several pruning methods and the L A T E X derivation of our approach, and instructed to analyze why it failed, fix or replace the method, and empirically beat a set of baselines (Sun et al., 2024; Zhang et al., 2023) at 60% sparsity. What the agent did. The agent first established that the existing approach was mathematically flawed and could not be repaired. While analyzing why it failed, the agent studied how pruning distorts the post-layer activations of each weight matrix and observed a severe imbalance: some rows lose over 50% of their activation-weighted output magnitude while others lose less than 10%. This byproduct of debugging led the agent to propose a simple post-pruning weight correction that restores the activation balance across rows and columns. Following Commandment VIII, the agent first computed an oracle bound via least-squares reconstruction to determine the theoretical limit, then validated the new method through the tiered evaluation protocol (Commandment VII) across five model scales. Results. The method consistently reduces perplexity by 18ā50% across five model scales (125M to 9B parameters), three architectures (OPT, Qwen, Gemma), and two pruning methods (RIA, Wanda). It requires only 10 lines of code, adds less than 1% computational overhead, and needs no hyper- parameter tuning. The oracle comparison shows that this simple heuristic captures 92% of the im- provement achievable by full least-squares reconstruction, leaving little room for more sophisticated approaches. Across 27 experiments documented in the agentās report, the improvements are robust and transfer to every model and pruning method tested. Figure 6 shows the scaling behavior across model sizes, reproduced [sic] from the agentās report; note, for instance, that the 50% sparsity line 13 125M1.5B3B7B9B Model Size (Million Parameters) 20 10 0 10 20 30 40 50 Perplexity Improvement (%) Peak: 49.4% Stable ~20% improvement RIA+Recon Scaling Behavior Across Model Sizes 60% sparsity 50% sparsity opt-125m Qwen-1.5B Qwen-3BQwen-7B gemma-9B Model 0 10 20 30 40 50 60 70 Perplexity (WikiText-2) 70.3 44.7 22.7 13.0 17.3 57.0 22.6 15.7 10.4 13.9 Absolute Perplexity: RIA vs RIA+Recon at 60% Sparsity RIA RIA+Recon Figure 6: Plots [sic] from the agentās report for Section 4.2, produced by the agent. Left: relative perplexity improvement vs. model size. Right: absolute perplexity comparison showing that the weight reconstruction method consistently outperforms the baseline across all tested model sizes. in the left panel ends at 1.5B because the agent found the 60% setting more promising and did not complete the remaining experiments. Lessons learned. The original task was to fix a broken pruning mask; the actual outcome was a novel weight reconstruction method. The commandments forced the agent to analyze why the approach failed rather than simply trying the next idea, and this systematic analysis led to the dis- covery. Computing the oracle baseline (Commandment VIII) early on established that 92% of the theoretical optimum was already achieved, preventing wasted effort on a nearly closed gap. Finally, several extensions showed no benefit on small models but 7ā11% improvement at 1.5ā7B scale; the tiered evaluation protocol (Commandment VII) caught this systematically. 4.3COLUMN ORDERING IN LLM QUANTIZATION This case study shows the framework operating as a systematic empirical researcher: given a well- defined design space, the agent mapped it comprehensively and discovered that the most important finding was not which method wins, but when and why it matters. Domain and problem. Post-training quantization compresses a pretrained language model by rep- resenting its weights in lower precision, substantially reducing the memory footprint and enabling deployment on consumer-grade hardware. GPTQ (Frantar et al., 2023), a widely used method, processes each weight matrix W āR d out Ćd in column by column to minimize the layer-wise re- construction error ā„(W ā Ė W )Xā„ 2 F , where Ė W denotes the quantized matrix and X āR d in Ćn are calibration activations. Each columnās rounding error is propagated to subsequent columns via the inverse of the Hessian H = 2X ā¤ āR d in Ćd in . The order in which columns are processed affects the final quality. A post-publication variant known as āact-orderā 3 sorts columns by descending Hes- sian diagonal, with the intuition that high-sensitivity columns benefit from having more subsequent columns available for error compensation. The agent was tasked with investigating whether better orderings exist, how the effect depends on model architecture, and validating findings across model families. Calibration data is drawn from C4 (Raffel et al., 2020); quality is measured by perplexity on the WikiText (Merity et al., 2016) test set (lower is better). What the agent did. The agent began with a mathematical analysis of why column ordering matters, then implemented and compared seven ordering strategies, first on single weight matrices, then at full model scale. Following Commandment X, it created verification scripts for all error propagation and refinement formulas before running any benchmarks (Figure 7). Cross-architecture validation (Commandment VII) across five model families (Qwen, Llama, Gemma, Mistral, Yi) revealed the central finding: the ordering effect varies by more than two orders of magnitude across architectures. 3 Commit a4c3c89, March 2023, in https://github.com/IST-DASLab/gptq. 14 Verification What:GP T Q new error propagation and refinement formulas Method:Numeric tests on small matrices (32Ć64, 32Ć128) Script:scripts/verifygptqnew.py Outcome:All 5 tests pass. No bugs found. One known approximation documented (within-chunk propagation inGP T Q new ). Status:Complete. Figure 7: A screenshot [sic] from the agentās report in Section 4.3. Before running any benchmarks, the agent audited all error propagation and refinement formulas through numeric tests on small matrices (Commandment X). Results. Column ordering is the single most impactful improvement to GPTQ, but its magnitude is entirely architecture-dependent: it reduces perplexity by 74% on Llama-3.1-8B but only 0.1% on Gemma-2-9B at 4-bit. This finding would have been missed without systematic multi-architecture validation: on Qwen-1.5B alone, the effect is 20%, giving no indication that it ranges from 0.1% to 74% across architectures. Among the seven ordering strategies tested, alternatives that incorporate the quantization error magnitude alongside column sensitivity occasionally outperformed act-order (e.g., at 3-bit on certain architectures), but no single strategy dominated consistently across all archi- tectures and bit widths. Nine of the 24 experiments produced negative results, each documented with the same rigor as positive ones (Commandment IX): many approaches failed because GPTQās error propagation via Ordinary Least Squares (OLS) already minimizes the correlations these methods would exploit. A critical implementation bug in group quantization was caught because the agent investigated a failure rather than abandoning the method (Commandment V): pre-computing scale parameters from initial instead of error-propagated weights produced catastrophic results (perplexity 437 vs. 9.22 after the fix). The agentās report documents all 24 experiments and 11 key findings. Lessons learned. The negative results (9 of 24 experiments) were more informative than the posi- tive ones: each failure clarified why simpler methods work, revealing that GPTQās OLS-based error propagation already handles what sophisticated alternatives attempt. With four GPUs, the agent ran independent model evaluations in parallel (one per GPU, Commandment C1), efficiently covering five model families with multiple configurations each. The āMake It Workā commandment (Com- mandment V) prevented a false negative: group quantization initially appeared broken on Llama, but investigation revealed a subtle implementation bug whose fix turned a catastrophic failure into the best result. 4.4TIGHT LOWER BOUNDS FOR FRANK-WOLFE ON UNIFORMLY CONVEX SETS This case study demonstrates the framework on a problem in convex optimization, where the agentās primary output is the proof of a new theorem. Unlike the computational and empirical case stud- ies, the research here required sustained interaction between numerical exploration and theoretical development: the agent discovered the correct proof strategy through systematic experimentation before formalizing it. Domain and problem. The Frank-Wolfe (FW) algorithm minimizes a smooth convex function over a convex constraint set using only a linear minimization oracle (LMO). On strongly convex sets, the knownO(1/T 2 ) upper bound was recently shown to be tight: Halbey et al. (2026) gave a lower bound for vanilla FW in dimension 2 by analyzing the dynamics of the iterates on a worst-case instance. Shortly after, Grimmer & Liu (2026) proved an information-theoretic lower bound in the high-dimensional setting for a broad class of LMO-based algorithms. For uniformly convex sets of order p > 2 (e.g., ā p -balls), Kerdreux et al. (2021) established an upper bound ofO(1/T p/(pā1) ), but no matching lower bound was known. The goal was to prove lower 15 bounds for the uniformly convex setting based on the techniques used by Halbey et al. (2026) or Grimmer & Liu (2026). What the agent did. The agent began by studying both existing lower-bound techniques and at- tempting to generalize the high-dimensional construction by Grimmer & Liu (2026) to ā p -balls. This did not succeed: the construction relies on decomposing strongly convex sets as intersections of shifted Euclidean balls, and the agent did not find a direct analogue for uniformly convex sets of order p > 2. Following Commandment IX, the agent documented this negative result and pivoted to the alternative approach of Halbey et al. (2026), which analyzes the FW iterates directly on a worst-case instance. The agent derived the FW dynamics on ā p -balls in closed form and verified each component numerically (Commandment X). Experiments across multiple values of p revealed that the iterates alternate in sign and settle onto a low-dimensional curve whose shape can be char- acterized analytically, which suggested the right proof strategy. The agent first estimated the key constants numerically, then derived them in closed form, and finally assembled a rigorous proof for pā„ 3 with explicit convergence rates. Each proof step was accompanied by Julia verification scripts using BigFloat arithmetic, totaling over 30 individual checks. The case pā (2, 3) was identified as qualitatively different: sign alternation breaks down intermittently, and the proof technique does not apply. Results. The main result establishes a lower bound of ā¦(1/T p/(pā1) ) for vanilla FW on p- uniformly convex sets for any p ā„ 3, matching the upper bound of Kerdreux et al. (2021) and resolving the open question for this regime. The proof provides explicit convergence constants, all verified numerically to < 0.2% relative error. The case pā (2, 3) remains open: numerical evidence supports the same rate, but the proof technique does not extend. 10 0 10 1 10 2 10 3 10 4 10 5 Iteration t 10 9 10 8 10 7 10 6 10 5 10 4 10 3 10 2 10 1 Primal gap h t = x t e 1 2 p = 3, u 0 = 0.01 x 0 = e 2 ( =1.500, R 2 =1.0000) x 0 = x slow (u 0 ) ( =1.497, R 2 =1.0000) ref t 1.50 10 0 10 1 10 2 10 3 10 4 10 5 Iteration t 10 8 10 7 10 6 10 5 10 4 10 3 10 2 10 1 p = 4, u 0 = 0.01 x 0 = e 2 ( =1.333, R 2 =1.0000) x 0 = x slow (u 0 ) ( =1.329, R 2 =1.0000) ref t 1.33 10 0 10 1 10 2 10 3 10 4 10 5 Iteration t 10 7 10 6 10 5 10 4 10 3 10 2 10 1 p = 6, u 0 = 0.01 x 0 = e 2 ( =1.200, R 2 =1.0000) x 0 = x slow (u 0 ) ( =1.193, R 2 =1.0000) ref t 1.20 Figure 8: A plot [sic] from the agentās report: Log-log convergence ofā„x t ā e 1 ā„ 2 for pā3, 4, 6 starting from x 0 = e 2 (blue) and from x 0 = x slow 0 (10 ā2 ) (orange) where x slow 0 is the worst-case initialization from the proof and Ī± is the fitted coefficient of t āĪ± . Lessons learned. The correct proof strategy emerged from the agentās numerical exploration: pat- terns observed in the iterates suggested the right analytical approach, and the key constants were first estimated computationally before being derived in closed form. This āconjecture from computation, then proveā loop, enabled by the frameworkās emphasis on creating verification scripts alongside every mathematical claim (Commandment X), is a natural workflow for this type of problem. The failed generalization of Grimmer & Liu (2026) was equally informative: it helped us understand which parts of the proof are hard to extend to the uniformly convex setting, guiding the pivot to the successful approach. Following Commandment IX, this negative result was documented thoroughly. 4.5MULTI-VARIABLE DUAL TIGHTENING FOR MIXED-INTEGER OPTIMIZATION This case study demonstrates the framework in combinatorial optimization. Its main contribution is a multi-variable generalization of dual tightening, together with a prototype implementation in the Boscia solver. The case study spans the full research cycle: deriving the result, proving it, implementing it, and evaluating it computationally. 16 Domain and problem. Boscia (Hendrych et al., 2025) is a Frank-Wolfe-based branch-and-bound solver for mixed-integer nonlinear optimization over polytopes (min xāXā©Z J f (x) with f smooth convex), where X āR n . A key pruning mechanism is dual tightening. At a relaxed solution x t with gradientg =āf (x t ) and Frank-Wolfe dual gapĪ³(x t ) = max vāX āØg,x t āvā©, convexity implies that any feasible point x ā X with objective value at most some upper bound UB (e.g., from an incumbent) satisfies g j (x j āā j )ā¤ RHS for each variable j, where RHS : = UBāf (x t )+Ī³(x t ) and ā j is the lower bound of x j . This allows variables to be fixed one at a time. The project investigated whether this extends to subsets: for a set S of variables at their lower bounds, P jāS g j (x j ā ā j ) ā¤ RHS, so when the combined gradient contribution exceeds the budget, a conflict constraint prevents all variables from simultaneously deviating from their current bounds. For binary variables, a pairwise conflict g i +g j > RHS implies x i +x j ā¤ 1 (a conflict graph edge); higher-order conflicts (triples, quadruples) capture interactions that pairwise constraints miss. The goal was to derive the mathematical result, implement it as a conflict graph with constraint propagation integrated into Boscia via callbacks, and benchmark on a diverse set of Mixed-Integer Nonlinear Programming (MINLP) instances. What the agent did. The agent started from Bosciaās existing single-variable dual tightening re- sult (Theorem 3 of Hendrych et al. (2025)), identified the natural generalization via the convexity inequality, and formulated and proved a multi-variable dual tightening theorem with corollaries for pairwise and higher-order binary conflicts. Before implementation, the agent first tried to verify the proof both symbolically, using Symbolics.jl with 2,387 checks, and numerically, using a script that exhaustively enumerated all 2 n feasible points for small instances (487 checks). This verification caught an error in the initial derivation: the bound for the at-least set constraint had been inverted, which would have led to overly aggressive fixings for upper-bound variables. The agent then implemented a ConflictGraph data structure with constraint propagation and integrated it into Boscia via two callbacks (Figure 9), requiring no source modifications beyond fixing a pre- existing Dict type bug. A key design decision made by the agent was to derive conflicts only at the root node. Because these conflicts use the global Frank-Wolfe gap, they remain valid throughout the search tree, but are more conservative than conflicts derived locally at child nodes. The agent also explored tighter child-node conflicts, but early tests suggested that the additional overhead and numerical instability were not worth the potential gain. Results. Across 33 instances in six problem categories (n = 12 to n = 300, 10-minute time limit), partition-constrained instances show the strongest improvement (up to 18.9% node reduction, from 127 to 103 nodes on a 48-variable instance), where partition constraints create tight cross-block coupling that the conflict graph captures. The root-only design is deliberately conservative, and most instances show 0% node reduction because the root budget is loose. However, this guaran- tees correctness, which is critical for an exact mixed-integer convex optimization solver, and all 33 instances produce identical optimal objectives in both modes. As expected, separable quadratic in- stances show no benefit because diagonal objectives create no cross-variable coupling, confirming the theoretical prediction. Lessons learned. This case study shows that the framework is effective for projects that com- bine theorem proving, verification, implementation, and experiments in a single workflow. The verification-first approach (Commandment X) was crucial for the overall correctness. It caught the inverted at-least bound bug before it entered the experiment phase. The negative results were useful as well. The lack of improvement on separable instances matched the theory, while the 26Ć over- head on a sparse regression instance with 150 indicator variables exposed a concrete bottleneck and pointed to straightforward fixes, including better data structures and a cap on propagated conflicts. Following Commandment IX, these outcomes were all documented in the report, which made the evaluation more transparent and more useful for guiding future improvements. 4.6FINDING MAXIMAL REAL SOLUTIONS IN K 7 POWER NETWORKS This case study shows the framework operating as a computational scientist for discovery. Starting from a published method for characterizing typical behavior, the agent reconstructed the pipeline and repurposed it for directed extremal search, discovering an improved lower bound. 17 4.1 Callback architecture The conflict graph is integrated via two standard Boscia callbacks.No Boscia source modifications are required beyond the existing Dict type fix for settings.tightening(commitc8f86437b). propagatebounds(tree, node) Called at each nodebeforethe Frank-Wolfe solve. Propagates conflict- implied fixings from the root-derived conflict graph intonode.local.bounds, rebuilds the LMO, and cleans the active set (see Section 4.2). bnbcallback(tree, node) Calledaftereach node is processed. At the root (node.std.id= 1): derives conflicts into the global graph and stores a gradient/iterate snapshot for re- scanning. At non-root nodes: checks whether the incumbent improved and, if so, re-scans the root snapshot with the tighter RHS = UB new āf(x t root ) + ĻĀ·Ī³ root . Figure 9: A screenshot [sic] from the agentās report: The callback architecture in Section 4.5. The conflict graph is integrated into Boscia via two standard callbacks, propagatebounds (before each Frank-Wolfe solve) and bnbcallback (after each node), without modifying Bosciaās source code. Domain and problem. Electrical power grids can be modeled as networks of buses connected by transmission lines, where the physics imposes a system of polynomial equations whose real solutions correspond to feasible operating states. Solutions to these power flow equations define the operating points of the network and underpin decisions ranging from long-term planning and capital investment to day-to-day resource scheduling, market operations, and real-time stability analysis. The equations depend on tunable parameters (susceptances), which appear as coefficients in the system. This motivates a natural structural question, raised explicitly by Lindberg et al. (2020): for a fixed network topology, what is the maximum number of feasible operating states over all parameter choices? Lindberg et al. (2020) characterized the distribution of solution counts for several topologies, including K 7 (seven buses, every pair connected), using a continuation pipeline orders of magnitude faster than naive solving. However, they did not target extremal instances, i.e., those with a maximal number of real solutions, explicitly. Our goal is therefore to adapt the sampling technique from Lindberg et al. (2020) to identify parameter settings that yield extremal instances. What the agent did. The agent first reconstructed the pipeline of Lindberg et al., which was a nontrivial task. Reproducing the published results required several rounds of refinement to align the implementation with the paperās symmetry conventions, parameterization choices, and solution- counting bookkeeping. Once this baseline was validated, the agent adapted the pipeline from sam- pling to extremal search. To explore the parameter space effectively, the agent combined several heuristic search strategies, including hill climbing, simulated annealing, and warm starts from the best susceptance vectors found so far. These methods were used iteratively to bias the search toward regions of parameter space with unusually large numbers of real solutions, with each successful run informing the next. Results. Random sampling of 1.4 million parameter vectors, following the original paperās sam- pling protocol, found at most 120 (nontrivial) feasible states. Targeted search instead identified a parameter vector with 192 feasible states. The agent also perturbed this parameter vector to verify that the 192-solution count is not confined to an isolated parameter point, but persists in a neigh- borhood of parameter space. Figure 10 supports this interpretation by showing that, when only b 1 , b 8 , and b 9 are varied and the remaining 18 parameters are fixed, the 192-solution configuration lies in a small region with constant solution count. The maximum real solutions problem for K 7 re- mains open. However, adapting Lindberg et al.ās continuation pipeline for extremal search yields a substantially stronger computational lower bound. Lessons learned. This case study highlights the importance of verifiable intermediate artifacts: published tables and solution-count distributions were essential for checking that the reconstructed 18 1.00 0.75 0.50 0.25 0.00 0.25 0.50 0.75 1.00 b 1 1.00 0.75 0.50 0.25 0.00 0.25 0.50 0.75 1.00 b 8 1.00 0.75 0.50 0.25 0.00 0.25 0.50 0.75 1.00 b 9 30 44 60 74 90 104 120 134 150 164 180 192 Nontrivial real solutions Figure 10: A plot [sic] from the agentās report: a three-parameter slice of the 21-dimensional K 7 susceptance space, obtained by varying b 1 , b 8 , and b 9 while fixing the remaining 18 parameters at the values of the best-found instance. Each point is colored by the number of nontrivial feasible operating states. Although the color map appears nearly continuous, it represents discrete solution counts and reveals a localized high-count region around the 192-solution configuration. This sug- gests that the best-found parameter vector lies in a small but open region of parameter space rather than at an isolated point. pipeline matched prior work before launching the extremal search (Commandment X). It also under- scored the value of staged evaluation (Commandment VII): because individual searches can run for hours, the agent benefited from first validating correctness on cheaper checks and only then scaling up to long-running optimization runs. More broadly, the study shows that the agent need not rely on an existing codebase to begin exploration. 5DISCUSSION AND CONCLUSION We have presented a practical framework for AI-assisted research in mathematics and machine learn- ing, organized around a taxonomy of five integration levels, an open-source framework for working with general-purpose CLI coding agents, and case studies demonstrating this framework in practice. A central claim of this paper is that effective agentic research does not require a specialized system built from scratch. Instead, it can be built around existing general-purpose agents, provided they are embedded in a disciplined and inspectable workflow. In our setup, the agent operates with persistent instructions, a sandboxed environment, written progress reports, TODO.md files, and a small set of methodological rules: change one variable at a time, evaluate in stages, and verify results before reporting them, among others. In practice, these additions were sufficient to extend the agent from a tool for isolated coding tasks into a useful research collaborator for exploratory and implementation-heavy work. Our experience suggests a simple conclusion: model capability matters, but workflow design matters just as much. These systems are only useful when their outputs can be checked and their intermediate steps revisited. This keeps the researcher responsible for direction, judgment, and verification, even when substantial exploratory or technical work is delegated. At the same time, this approach does not eliminate the need for expert oversight or final verification. In our framework, however, oversight is not reserved only for the end of the process; it is built into the workflow itself. A central requirement is that the agent must be able to test, challenge, and potentially refute its own claims through staged evaluation, intermediate checks, and explicit internal validation procedures. In our experience, these internal verification mechanisms are crucial. Without them, experiments can easily become structured to simply confirm an initial hypothesis. 19 Final expert verification remains necessary, but it is far more reliable when supported by a workflow that already produces inspectable and continuously tested intermediate results. We emphasize that the case studies and reports do not constitute finished papers that are ready for publication, but rather records of meaningful research progress. To make this approach usable by others, we release the instruction set, templates, and container definitions, with the broader goal of making AI-assisted research more systematic, reproducible, and accessible. 5.1LIMITATIONS Verification. A fundamental limitation of our framework, shared with other agentic systems, is result verification. Natural-language proofs remain difficult to verify and require manual inspection. While code is usually easier to check, subtle implementation errors can still invalidate conclusions. Citations must also be verified carefully, since agents may hallucinate references or bibliographic details. This is not only a technical limitation but also a matter of responsible use: researchers must invest substantial effort in verifying agent outputs, especially because such outputs may be even harder for others to assess independently. As Su (2022) argue, researchers are often the best reviewers of their own papers; likewise, we argue that they are ultimately responsible for verifying the work produced by their agents. Context. Long experimental sessions with many runs and large outputs can exceed a modelās con- text window and trigger compaction. Because compaction is inherently lossy, the agent may forget details from earlier in the session, revisit failed approaches, or miss important observations. Practi- cal mitigations include routing long outputs to log files and monitoring them with tail, manually invoking compaction commands such as /compact, and relying on persistent artifacts such as report.tex and TODO.md as re-entry points and external memory. We also tested autonomous compaction, but found it to have no positive impact. Robust context management remains an open challenge. Cost. Long autonomous sessions with frontier models can incur nontrivial API costs. In practice, however, these costs are often relatively small since much of the wall-clock time in Level 4 ses- sions is spent waiting for experiments to finish rather than generating tokens. Still, cost remains a meaningful limitation, particularly for long-running studies and large-scale evaluations. 5.2FUTURE DIRECTIONS Extension to other domains. While our paper focuses on the application of our framework to machine learning and mathematical research, in principle it could be applied more broadly to other disciplines, such as physics, chemistry, economics, or the social sciences. Adapting the framework to these settings would require domain-specific tools, evaluation protocols, and safety checks, but the general paradigm of iterative experimentation, artifact management, and human verification may transfer well beyond our current case studies. More robust memory. Another important direction is improving how the system stores, retrieves, and updates information over long research sessions. Better memory mechanisms could help agents maintain continuity across experiments, avoid revisiting failed approaches, and make more effective use of prior observations. This would be especially valuable for complex projects that unfold over many iterations and generate substantial intermediate state. Multi-user collaboration. Our setup is currently designed for a single user interacting with a single main agent. An important future direction is extending this setting to support collaboration among multiple users, multiple agents, or both. Such a setting raises new challenges in coordination, communication, provenance tracking, and conflict resolution, but it could also make agentic research workflows more effective for team-based projects. 20 6RELATED WORK We survey three bodies of work: AI systems that produce mathematical results autonomously (Sec- tion 6.1), research on mathematicians actively using AI in their workflow (Section 6.2), and agentic frameworks for scientific discovery (Section 6.3). For broader surveys of AI for mathematics and scientific discovery, we refer to Ju & Dong (2026), Carbone (2025), and Zheng et al. (2025b). 6.1AI GENERATING MATHEMATICS Competition-level mathematics. In recent years, progress in AI mathematical reasoning has been especially visible in competition-level mathematics, where performance is relatively easy to com- pare because problems typically have a single, closed-form final answer that can be scored auto- matically. 4 Early results came from specialized systems: AlphaProof (Hubert et al., 2025) com- bined reinforcement learning with the Lean proof assistant to reach silver-medal performance at the 2024 IMO, while AlphaGeometry (Trinh et al., 2024) and AlphaGeometry2 (Chervonyi et al., 2025) paired a neural model with a symbolic deduction engine to achieve gold-medalist perfor- mance on historical olympiad geometry. More recently, the emphasis has shifted toward off-the- shelf frontier models strengthened by verification and refinement: Huang & Yang (2025) report a model-agnostic pipeline that, with Gemini 2.5 Pro, Grok-4, or GPT-5, solves five out of six problems on the 2025 IMO under contamination-avoiding protocols. In parallel, proprietary sys- tems such as Aristotle (Achim et al., 2025) combine informal reasoning with formal verification to achieve gold-medal-equivalent performance on the 2025 IMO. Finally, the same verification-first approach is now claimed at the undergraduate level: AxiomMath (2025) reports that AxiomProver produced Lean-checked solutions to all Putnam 2025 problems (a perfect 120/120). 5 To move be- yond competition-style evaluation, recent benchmarks increasingly probe research-level questions arising in active mathematical workflows, such as the encrypted, author-curated problem set in First Proof (Abouzaid et al., 2026). Constructions and algorithms.Beyond proving theorems, AI has generated novel mathematical constructions and faster classical algorithms by searching over programs: an LLM proposes can- didate code, an automated evaluator scores it, and an iterative loop improves the best candidates. FunSearch (Romera-Paredes et al., 2024) introduced this template, yielding new constructions for the cap set problem and improved online bin packing heuristics. AlphaEvolve (Novikov et al., 2025) scales the same evolutionary idea; in large-scale mathematical experiments it rediscovered best-known solutions across 67 problems and improved several, including autocorrelation inequal- ities (Georgiev et al., 2025). Recent open-source works have proposed methodological extensions, including OpenEvolve, ShinkaEvolve, ThetaEvolve, DeltaEvolve, and AdaEvolve (Sharma, 2025; Lange et al., 2025; Wang et al., 2025b; Jiang et al., 2026; Cemri et al., 2026). Most such systems are closed-loop and largely non-interactive: progress comes from automated proposeāevaluate iter- ations rather than back-and-forth dialogue with a human. Related approaches have also produced faster algorithms: AlphaTensor (Fawzi et al., 2022) discovered efficient tensor decompositions for matrix multiplication, and AlphaDev (Mankowitz et al., 2023) found improved sorting routines now deployed in production software. Data-driven and learning-augmented mathematics. A complementary line of work uses AI to generate candidate mathematical objects from data, whose correctness is then verified either auto- matically (via symbolic or optimization-based methods) or by human experts. Examples include data-driven conjecturing and candidate filtering (Davies et al., 2021; Mishra et al., 2023; Chuharski et al., 2024), learning-augmented Lyapunov, Sum-of-Squares, and Border basis pipelines (Alfarano et al., 2024; Zou et al., 2025; Pelleriti et al., 2025; Kera et al., 2025), neural-guided discovery of six-colorings for the HadwigerāNelson problem (Mundinger et al., 2024; 2025), and ML+high- precision optimization uncovering unstable self-similar solutions in fluid dynamics (Wang et al., 2025c). Symbolic regression further extracts interpretable laws from data (Udrescu & Tegmark, 2020; Ruan et al., 2026). 4 Correct final answers need not imply correct proofs (Dekoninck et al., 2026). 5 cf. https://axiommath.ai/territory/from-seeing-why-to-checking-everything 21 Formal theorem proving and autoformalization. A rich ecosystem of LLM-based formal prov- ing tools has emerged around Lean 4 (de Moura & Ullrich, 2021). LeanDojo (Yang et al., 2023) provides an interface to Lean proof states and retrieval over mathlib (mathlib Community, 2020), while Lean Copilot (Song et al., 2025) integrates LLM assistance into the Lean workflow. Dedicated provers include DeepSeek-Prover (Xin et al., 2024), which leverages large-scale synthetic proof data, and DeepSeek-Prover-V2 (Ren et al., 2025), which adds reinforcement learning with explicit subgoal decomposition and introduces ProverBench for evaluation. Goedel-Prover-V2 (Lin et al., 2025) scales expert iteration with scaffolded data synthesis and verifier-guided self-correction. Com- plementary directions focus on knowledge reuse and structured reasoning: LEGO-Prover (Wang et al., 2023) builds and reuses a growing library of verified lemmas, while Hilbert (Varambally et al., 2025) connects informal reasoning with formal verification through recursive decomposition. TheoremLlama (Wang et al., 2024) and Mathesis (Xuejun et al., 2025) explore adapting general- purpose models and end-to-end pipelines from natural language to Lean proofs. Recent agentic frameworks emphasize tool use and iterative compiler-feedback loops rather than one-shot gener- ation: APOLLO (Ospanov et al., 2025) performs modular proof repair and sub-lemma isolation, Ax-Prover (Breen et al., 2025) uses multi-agent tool-based proving across scientific domains, and LeanAgent (Kumarappan et al., 2025) studies continual adaptation across evolving repositories. In a different direction, LeanProgress (George et al., 2026) guides search by predicting proof progress to improve performance on long proofs. On the data side, MUSTARD (Huang et al., 2024) generates uniform theorem-and-proof training data with formal verification. For evaluation, miniF2F (Zheng et al., 2022) and PutnamBench (Tsoukalas et al., 2024) provide competition-style benchmarks, while SorryDB introduces a dynamically updating stream of open sorry tasks mined from real-world Lean projects, mitigating contamination. Autoformalization, i.e., translating informal mathematics into machine-checkable form, was shown to be feasible with LLMs by Wu et al. (2022). Recent work addresses this through dependency-graph decomposition (Wang et al., 2025a), chain-of-states proof translation (Wang et al., 2025d), and evaluation on real-world mathematical definitions (Zhang et al., 2025b). Agentic end-to-end pipelines such as MerLean (Ren et al., 2026) extend this to scientific domains. We refer to Weng et al. (2025) for a comprehensive survey. Frontier systems and research-level evaluation suites. Beyond competition benchmarks, several recent efforts target research-level mathematics. First Proof (Abouzaid et al., 2026) introduces an author-curated set of ten questions arising naturally in the authorsā research, with answers not publicly released. Other benchmarks include continuously refreshed collections drawn from arXiv papers (RealMath (Zhang et al., 2025a)) and curated sets of exceptionally challenging, unpublished problems reviewed by domain experts (FrontierMath (Glazer et al., 2025)). Aletheia was evaluated directly on First Proof : roughly three weeks after the challenge was introduced, Feng et al. (2026a) report that Aletheia autonomously solved six out of ten problems. Notably, some of these results are now accompanied by machine-checked proofs: for example, Sothanaphan (2026) provide a Lean formalization of a resolution of an Erd Ģ os problem attributed to Achim et al. (2025). 6.2MATHEMATICIANS USING AI Frameworks and perspectives. The literature on AI and mathematical practice is broad, so we highlight only those lines of work most directly relevant to our framework. Haase & Pokutta (2026) propose four levels of human-AI co-creativity: Digital Pen, AI Task Specialist, AI Assistant, and AI Co-Creator. These categories provide a conceptual vocabulary that we build on in Section 2. Their treatment is intentionally broad and domain-agnostic, serving primarily as a conceptual template to which domain-specific details can be added. Henkel (2025) offer a complementary perspective from mathematics, arguing that AI should augment rather than replace mathematical reasoning and proposing five guiding principles for its responsible use. Noorani et al. (2025) formalize the comple- mentary strengths of humans and AI in uncertainty quantification, providing theoretical guarantees for collaborative prediction. Most recently, Avigad (2026) consider recent developments in AI- driven mathematics and argue that mathematicians should remain actively involved in the use of these systems. Our work shares these perspectives but addresses a different question: given these emerging capabilities, how should a working researcher use them in practice? Documented case studies. Over the past several months, a growing number of papers have doc- umented how mathematicians interact with chat-based AI systems to obtain new research results 22 (Bubeck et al., 2025; Diez et al., 2025; Alexeev & Mixon, 2026; Ivanisvili & Xie, 2025; Feldman & Karbasi, 2025; Salim, 2025; Dobriban, 2025; Schmitt, 2025). More specialized agentic systems with varying degrees of autonomy are also being developed (Liu et al., 2025; Feng et al., 2026b) and have already produced new mathematical results (Lee & Seo, 2026; Feng, 2026). AI coding agents provide yet another pathway by enabling large computational searches: Knuth (2026) report that Claude solved an open Hamiltonian cycle decomposition problem through iterative exploration. These examples likely represent only a small fraction of emerging workflows. 6.3AGENTIC RESEARCH FRAMEWORKS Automated scientific discovery. Lu et al. (2024) introduced The AI Scientist, an end-to-end sys- tem that generates hypotheses, runs experiments, and writes papers; its successor (Yamada et al., 2025) reported an AI-generated paper accepted at a peer-reviewed workshop. Subsequent systems explore adjacent design points, from semi-automated, code-centric experimentation (CodeScien- tist (Jansen et al., 2025)) to end-to-end agent pipelines that incorporate explicit mechanisms for human feedback and cumulative reporting (Schmidgall et al., 2025; Schmidgall & Moor, 2025). Al- phaApollo (Zhou et al., 2026) combines multi-turn tool use, reinforcement learning, and iterative evolution with tool-assisted verification, showing improved performance on several mathematical reasoning benchmarks. As these pipelines grow more complex, rigorous benchmarking has emerged as a central challenge, with recent work proposing evaluations that target both full workflows and their individual steps (Chen et al., 2025; Bragg et al., 2025). Taken together, these works highlight a common requirement: agent outputs must be checkable (e.g., as code, logs, or derived claims) and include explicit points for verification and human steering, rather than being treated as opaque end-to-end generations. Karpathyās autoresearch exemplifies a minimalist variant: an agent itera- tively modifies a single file, runs fixed-budget training, and keeps or discards based on validation performance (Karpathy, 2026). Our framework targets the complementary regime of multi-file, multi-objective research with structured reporting and verification. For broader context, we refer to recent surveys (Ferrag et al., 2025; Zheng et al., 2025a). Agentic coding tools. Terminal-based coding agents such as Claude Code, OpenCode, Codex CLI, and Gemini CLI (Anthropic; Anomaly; OpenAI; Google) extend AI assistance beyond chat by enabling users (Handa et al., 2025-12-04, 2025) (software engineers, analysts, and researchers alike) to delegate work within a persistent local project. These agents can read and edit files and invoke development tools (e.g., shells, test runners, linters, and formatters) from within a CLI in- terface, producing inspectable artifacts such as patches, diffs, and test outputs. This inspectable, file-based workflow is central to our setting: it enables reproducible iteration and makes it possi- ble to attach verification hooks (tests, proofs, consistency checks) directly to the agentās actions. A key recent development is the growth of long-running autonomy: in Claude Code, the 99.9th- percentile turn duration nearly doubled from under 25 to over 45 minutes between October 2025 and January 2026 (McCain et al., 2026), reducing the need for constant supervision while increas- ing the importance of robust guardrails. Finally, these tools separate the underlying model from a repository-scoped instruction file, allowing us to express our framework as a portable, model- and harness-agnostic procedure that applies across Claude Code, OpenCode, Codex CLI, and related CLI agents. ACKNOWLEDGMENTS The frameworks, approaches, and insights presented here have been developed in the context of the MATH+ project Agentic AI in Mathematics. 6 This research was partially supported by the Deutsche Forschungsgemeinschaft (DFG) through the DFG Cluster of Excellence MATH+ (EXC- 2046/1, EXC-2046/2, project id 390685689), as well as by the German Federal Ministry of Research, Technology and Space (research campus Modal, fund number 05M14ZAM, 05M20ZBM) and the VDI/VDE Innovation + Technik GmbH (fund number 16IS23025B). 6 https://iol.zib.de/project/agentmath.html 23 REFERENCES Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, and Lauren Williams. First Proof, February 2026. Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Math Ģ ıs F Ģ ed Ģ erico, Sergei Gukov, Daniel Halpern- Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Ri- ley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. Aristotle: IMO-level Automated Theorem Proving, October 2025. URL https://arxiv. org/abs/2510.01346v2. Boris Alexeev and Dustin G. Mixon. Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof, January 2026. Alberto Alfarano, Franc Ģ§ois Charton, and Amaury Hayat. Global Lyapunov functions: A long- standing open problem in mathematics, with symbolic transformers, October 2024. URL http: //arxiv.org/abs/2410.08304. Anomaly. Opencode, February . URL https://github.com/anomalyco/opencode. Anthropic. Claude code. URL https://code.claude.com/docs/en/overview. Jeremy Avigad. Mathematicians in the Age of AI. 2026. AxiomMath.AxiomProver reports perfect score on Putnam 2025, 2025.URL https:// github.com/AxiomMath/putnam2025. GitHub repository, accessed 2026-03-06. Jonathan Bragg, Mike DāArcy, Nishant Balepur, Dan Bareket, Bhavana Dalvi, Sergey Feldman, Dany Haddad, Jena D. Hwang, Peter Jansen, Varsha Kishore, Bodhisattwa Prasad Majumder, Aakanksha Naik, Sigal Rahamimov, Kyle Richardson, Amanpreet Singh, Harshit Surana, Aryeh Tiktinsky, Rosni Vasu, Guy Wiener, Chloe Anastasiades, Stefan Candra, Jason Dunkelberger, Dan Emery, Rob Evans, Malachi Hamada, Regan Huff, Rodney Kinney, Matt Latzke, Jaron Lochner, Ruben Lozano-Aguilera, Cecile Nguyen, Smita Rao, Amber Tanaka, Brooke Vlahos, Peter Clark, Doug Downey, Yoav Goldberg, Ashish Sabharwal, and Daniel S. Weld. AstaBench: Rigorous Benchmarking of AI Agents with a Scientific Research Suite, October 2025. Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens, and Dirk Englund. Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics, November 2025. S Ģ ebastien Bubeck, Christian Coester, Ronen Eldan, Timothy Gowers, Yin Tat Lee, Alexandru Lup- sasca, Mehtaab Sawhney, Robert Scherrer, Mark Sellke, Brian K. Spears, Derya Unutmaz, Kevin Weil, Steven Yin, and Nikita Zhivotovskiy. Early science acceleration experiments with GPT-5, November 2025. Lisa Carbone. Advancing mathematics research with generative AI, December 2025. URL http: //arxiv.org/abs/2511.07420. Mert Cemri, Shubham Agrawal, Akshat Gupta, Shu Liu, Audrey Cheng, Qiuyang Mang, Ashwin Naren, Lutfi Eren Erdogan, Koushik Sen, Matei Zaharia, Alex Dimakis, and Ion Stoica. AdaE- volve: Adaptive LLM Driven Zeroth-Order Optimization, February 2026. Ziru Chen, Shijie Chen, Yuting Ning, Qianheng Zhang, Boshi Wang, Botao Yu, Yifei Li, Zeyi Liao, Chen Wei, Zitong Lu, Vishal Dey, Mingyi Xue, Frazier N. Baker, Benjamin Burns, Daniel Adu- Ampratwum, Xuhui Huang, Xia Ning, Song Gao, Yu Su, and Huan Sun. ScienceAgentBench: Toward Rigorous Assessment of Language Agents for Data-Driven Scientific Discovery, March 2025. URL http://arxiv.org/abs/2410.05080. Yuri Chervonyi, Trieu H. Trinh, Miroslav Ol Ė s Ģ ak, Xiaomeng Yang, Hoang Nguyen, Marcelo Mene- gali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, and Thang Luong. Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2, December 2025. URL http://arxiv.org/abs/2502.03544. 24 Jake Chuharski, Elias Rojas Collins, and Mark Meringolo. Mining math conjectures from LLMs: A pruning approach. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPSā24, 2024. URL https://openreview.net/forum?id=aYlKvzY6ob. Alex Davies, Petar Veli Ė ckovi Ģ c, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Toma Ė sev, Richard Tanburn, Peter Battaglia, Charles Blundell, Andr Ģ as Juh Ģ asz, Marc Lackenby, Geordie Williamson, Demis Hassabis, and Pushmeet Kohli.Advancing mathematics by guid- ing human intuition with AI.Nature, 600(7887):70ā74, December 2021.ISSN 1476- 4687. doi: 10.1038/s41586-021-04086-x. URL https://w.nature.com/articles/ s41586-021-04086-x. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Andr Ģ e Platzer and Geoff Sutcliffe (eds.), Automated Deduction ā CADE 28, p. 625ā635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5. Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Mari- nov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, Nikolay Drenchev, Lazar Todorov, Kalina Nikolova, Nikolay Georgiev, Vanesa Kalinkova, and Margulan Ismol- dayev. The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs, January 2026. Charles-Philippe Diez, Luis da Maia, and Ivan Nourdin. Mathematical research with GPT-5: A Malliavin-Stein experiment, September 2025. Edgar Dobriban. Solving a Research Problem in Mathematical Statistics with AI Assistance, De- cember 2025. URL http://arxiv.org/abs/2511.18828. Alhussein Fawzi, Matej Balog, Aja Huang, Thomas Hubert, Bernardino Romera-Paredes, Moham- madamin Barekatain, Alexander Novikov, Francisco J. R. Ruiz, Julian Schrittwieser, Grzegorz Swirszcz, David Silver, Demis Hassabis, and Pushmeet Kohli. Discovering faster matrix mul- tiplication algorithms with reinforcement learning. Nature, 610(7930):47ā53, October 2022. ISSN 1476-4687. doi: 10.1038/s41586-022-05172-4. URL https://w.nature.com/ articles/s41586-022-05172-4. Moran Feldman and Amin Karbasi. G Ģ odel Test: Can Large Language Models Solve Easy Conjec- tures?, September 2025. Tony Feng. Eigenweights for arithmetic Hirzebruch Proportionality, February 2026. Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, Chiang-Chiang Tsai, David Woodruff, Adel Javanmard, Aryan Mokhtari, Dawsen Hwang, Yuri Chervonyi, Jonathan N. Lee, Garrett Bingham, Trieu H. Trinh, Vahab Mirrokni, Quoc V. Le, and Thang Luong. Aletheia tackles FirstProof autonomously, February 2026a. Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-Tze Cheng, Demis Hassabis, Koray Kavukcuoglu, Quoc V. Le, and Thang Luong. Towards Autonomous Mathemat- ics Research, February 2026b. URL http://arxiv.org/abs/2602.10177. Mohamed Amine Ferrag, Norbert Tihanyi, and Merouane Debbah. From LLM Reasoning to Au- tonomous AI Agents: A Comprehensive Review, April 2025. Elias Frantar and Dan Alistarh. Sparsegpt: Massive language models can be accurately pruned in one-shot. In International Conference on Machine Learning, p. 10323ā10337. PMLR, 2023. Elias Frantar, Saleh Ashkboos, Torsten Hoefler, and Dan Alistarh. GPTQ: Accurate Post-Training Quantization for Generative Pre-trained Transformers, March 2023. URL http://arxiv. org/abs/2210.17323. Robert Joseph George, Suozhi Huang, Peiyang Song, and Anima Anandkumar. LeanProgress: Guid- ing Search for Neural Theorem Proving via Proof Progress Prediction, January 2026. 25 Bogdan Georgiev, Javier G Ģ omez-Serrano, Terence Tao, and Adam Zsolt Wagner. Mathematical ex- ploration and discovery at scale, November 2025. URL https://arxiv.org/abs/2511. 02864v3. Elliot Glazer, Ege Erdil, Tamay Besiroglu, Diego Chicharro, Evan Chen, Alex Gunning, Car- oline Falkman Olsson, Jean-Stanislas Denain, Anson Ho, Emily de Oliveira Santos, Olli J Ģ arviniemi, Matthew Barnett, Robert Sandler, Matej Vrzala, Jaime Sevilla, Qiuyu Ren, Eliza- beth Pratt, Lionel Levine, Grant Barkley, Natalie Stewart, Bogdan Grechuk, Tetiana Grechuk, Shreepranav Varma Enugandla, and Mark Wildon. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI, December 2025. Google. Build, debug & deploy with AI. URL https://geminicli.com/. Benjamin Grimmer and Ning Liu. Lower bounds for linear minimization oracle methods optimizing over strongly convex sets. arXiv preprint arXiv:2602.22608, 2026. Jennifer Haase and Sebastian Pokutta. Human-AI Co-Creativity: Exploring Synergies Across Levels of Creative Collaboration. p. 205ā221. 2026. doi: 10.1016/B978-0-443-34073-4.00009-5. URL http://arxiv.org/abs/2411.12527. Jannis Halbey, Daniel Deza, Max Zimmer, Christophe Roux, Bartolomeo Stellato, and Sebastian Pokutta. Lower bounds for frank-wolfe on strongly convex sets. arXiv preprint arXiv:2602.04378, 2026. Song Han, Jeff Pool, John Tran, and William Dally. Learning both weights and connections for efficient neural network. Advances in neural information processing systems, 28, 2015. Kunal Handa, Michael Stern, Saffron Huang, Jerry Hong, Esin Durmus, Miles McCain, Grace Yun, AJ Alt, Thomas Millar, Alex Tamkin, Jane Leibrock, Stuart Ritchie, and Deep Ganguli. Introducing anthropic interviewer: What 1,250 professionals told us about working with AI. https://anthropic.com/research/anthropic-interviewer, 2025-12-04, 2025. Deborah Hendrych, Hannah Troppens, Mathieu Besanc Ģ§on, and Sebastian Pokutta. Convex mixed- integer optimization with FrankāWolfe methods. Mathematical Programming Computation, 17 (4):731ā757, December 2025. ISSN 1867-2957. doi: 10.1007/s12532-025-00288-w. URL https://doi.org/10.1007/s12532-025-00288-w. Jonas Henkel. The Mathematicianās Assistant: Integrating AI into Research Practice, August 2025. URL http://arxiv.org/abs/2508.20236. Yichen Huang and Lin F. Yang. Winning Gold at IMO 2025 with a Model-Agnostic Verification- and-Refinement Pipeline, September 2025. Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data, May 2024. URL http://arxiv.org/abs/2402.08957. Thomas Hubert, Rishi Mehta, Laurent Sartran, Mikl Ģ os Z. Horv Ģ ath, Goran Ė Zu Ė zi Ģ c, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, Ottavia Bertolli, Tom Za- havy, Amol Mandhane, Jessica Yung, Iuliya Beloshapka, Borja Ibarz, Vivek Veeriah, Lei Yu, Oliver Nash, Paul Lezeau, Salvatore Mercuri, Calle S Ģ onne, Bhavik Mehta, Alex Davies, Daniel Zheng, Fabian Pedregosa, Yin Li, Ingrid von Glehn, Mark Rowland, Samuel Albanie, Ameya Velingker, Simon Schmitt, Edward Lockhart, Edward Hughes, Henryk Michalewski, Nicolas Sonnerat, Demis Hassabis, Pushmeet Kohli, and David Silver. Olympiad-level formal mathe- matical reasoning with reinforcement learning. Nature, p. 1ā3, November 2025. ISSN 1476- 4687. doi: 10.1038/s41586-025-09833-y. URL https://w.nature.com/articles/ s41586-025-09833-y. Paata Ivanisvili and Xinyuan Xie. Counterexample to majority optimality in NICD with erasures, October 2025. Peter Jansen, Oyvind Tafjord, Marissa Radensky, Pao Siangliulue, Tom Hope, Bhavana Dalvi Mishra, Bodhisattwa Prasad Majumder, Daniel S. Weld, and Peter Clark. CodeScientist: End- to-End Semi-Automated Scientific Discovery with Code-based Experimentation, March 2025. 26 Jiachen Jiang, Tianyu Ding, and Zhihui Zhu. DeltaEvolve: Accelerating Scientific Discovery through Momentum-Driven Evolution, February 2026. Keller Jordan, Yuchen Jin, Vlado Boza, You Jiacheng, Franz Cesista, Laker Newhouse, and Jeremy Bernstein. Muon: An optimizer for hidden layers in neural networks, 2024. URL https://kellerjordan. github. io/posts/muon, 6(3):4, 2024. Haocheng Ju and Bin Dong. AI for Mathematics: Progress, Challenges, and Prospects, February 2026. URL http://arxiv.org/abs/2601.13209. Andrej Karpathy.autoresearch, 2026.URL https://github.com/karpathy/ autoresearch. GitHub repository, accessed 2026-03-08. Hiroshi Kera, Nico Pelleriti, Yuki Ishihara, Max Zimmer, and Sebastian Pokutta. Computational Algebra with Attention: Transformer Oracles for Border Basis Algorithms, May 2025. Thomas Kerdreux, Alexandre dāAspremont, and Sebastian Pokutta. Projection-free optimization on uniformly convex sets. In International conference on artificial intelligence and statistics, p. 19ā27. PMLR, 2021. Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014. Donald E. Knuth. Claudeās cycles, 2026. URL https://w-cs-faculty.stanford. edu/ Ģ knuth/papers/claude-cycles.pdf. Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar. LeanAgent: Lifelong Learning for Formal Theorem Proving, March 2025. Robert Tjarko Lange, Yuki Imajuku, and Edoardo Cetin. ShinkaEvolve: Towards Open-Ended And Sample-Efficient Program Evolution, September 2025. Mike Lasby, Max Zimmer, Sebastian Pokutta, and Erik Schultheis. Compressed sparse tiles for memory-efficient unstructured and semi-structured sparsity. In Sparsity in LLMs (SLLM): Deep Dive into Mixture of Experts, Quantization, Hardware, and Inference, 2025. URL https:// openreview.net/forum?id=iso0KV2HVq. Joonkyung Lee and Jaehyeon Seo. Lower bounds for multivariate independence polynomials and their generalisations, February 2026. Zichong Li, Liming Liu, Chen Liang, Weizhu Chen, and Tuo Zhao. Normuon: Making muon more efficient and scalable. arXiv preprint arXiv:2510.05491, 2025. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction, August 2025. Julia Lindberg, Alisha Zachariah, Nigel Boston, and Bernard C. Lesieutre. The Distribution of the Number of Real Solutions to the Power Flow Equations, October 2020. Yuanhang Liu, Beichen Wang, Peng Li, and Yang Liu. AI Mathematician as a Partner in Advancing Mathematical Discovery ā A Case Study in Homogenization Theory, October 2025. URL http: //arxiv.org/abs/2510.26380. Ilya Loshchilov and Frank Hutter.Decoupled weight decay regularization.arXiv preprint arXiv:1711.05101, 2017. Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune, and David Ha. The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery, September 2024. URL http://arxiv.org/abs/2408.06292. 27 Daniel J. Mankowitz, Andrea Michi, Anton Zhernov, Marco Gelmi, Marco Selvi, Cosmin Padu- raru, Edouard Leurent, Shariq Iqbal, Jean-Baptiste Lespiau, Alex Ahern, Thomas K Ģ oppe, Kevin Millikin, Stephen Gaffney, Sophie Elster, Jackson Broshear, Chris Gamble, Kieran Milan, Robert Tung, Minjae Hwang, Taylan Cemgil, Mohammadamin Barekatain, Yujia Li, Amol Mandhane, Thomas Hubert, Julian Schrittwieser, Demis Hassabis, Pushmeet Kohli, Martin Riedmiller, Oriol Vinyals, and David Silver.Faster sorting algorithms discovered using deep reinforcement learning.Nature, 618(7964):257ā263, June 2023.ISSN 1476- 4687. doi: 10.1038/s41586-023-06004-9. URL https://w.nature.com/articles/ s41586-023-06004-9. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, p. 367ā381, January 2020. doi: 10.1145/3372885.3373824. Miles McCain, Thomas Millar, Saffron Huang, Jake Eaton, Kunal Handa, Michael Stern, Alex Tamkin, Matt Kearney, Esin Durmus, Judy Shen, Jerry Hong, Brian Calvert, Jun Sh- ern Chan, Francesco Mosconi, David Saunders, Tyler Neylon, Gabriel Nicholas, Sarah Pollack, Jack Clark, and Deep Ganguli.Measuring AI agent autonomy in practice. https://anthropic.com/research/measuring-agent-autonomy, 2026. Stephen Merity, Caiming Xiong, James Bradbury, and Richard Socher. Pointer sentinel mixture models. arXiv preprint arXiv:1609.07843, 2016. Asit Mishra, Jorge Albericio Latorre, Jeff Pool, Darko Stosic, Dusan Stosic, Ganesh Venkatesh, Chong Yu, and Paulius Micikevicius. Accelerating sparse deep neural networks. arXiv preprint arXiv:2104.08378, 2021. Challenger Mishra, Subhayan Roy Moulik, and Rahul Sarkar. Mathematical conjecture generation using machine intelligence, June 2023. URL http://arxiv.org/abs/2306.07277. Konrad Mundinger, Sebastian Pokutta, Christoph Spiegel, and Max Zimmer. Extending the contin- uum of six-colorings. Geombinatorics Quarterly, XXXIV, 2024. URL https://geombina. uccs.edu/past-issues/volume-xxxiv. Konrad Mundinger, Max Zimmer, Aldo Kiem, Christoph Spiegel, and Sebastian Pokutta. Neural discovery in mathematics: Do machines dream of colored planes? In Forty-Second International Conference on Machine Learning, 2025. URL https://openreview.net/forum?id= 7Tp9zjP9At. Sima Noorani, Shayan Kiyani, George Pappas, and Hamed Hassani. Human-AI Collaborative Un- certainty Quantification, October 2025. URL http://arxiv.org/abs/2510.23476. Alexander Novikov, Ng Ė an V Ģ u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. AlphaEvolve: A coding agent for scientific and algorithmic discovery, June 2025. URL https://arxiv.org/abs/2506.13131v1. OpenAI. Codex| AI Coding Partner from OpenAI. URL https://openai.com/codex/. Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning, November 2025. Nico Pelleriti, Christoph Spiegel, Shiwei Liu, David Mart Ģ ınez-Rubio, Max Zimmer, and Sebastian Pokutta. Neural Sum-of-Squares: Certifying the Nonnegativity of Polynomials with Transform- ers, October 2025. Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J Liu. Exploring the limits of transfer learning with a unified text-to-text transformer. Journal of machine learning research, 21(140):1ā67, 2020. Yuanjie Ren, Jinzheng Li, and Yidi Qi. MerLean: An Agentic Framework for Autoformalization in Quantum Computation, February 2026. 28 Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yux- uan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition, July 2025. Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models. Nature, 625(7995):468ā475, January 2024. ISSN 1476- 4687. doi: 10.1038/s41586-023-06924-6. URL https://w.nature.com/articles/ s41586-023-06924-6. Christophe Roux, Max Zimmer, Alexandre dāAspremont, and Sebastian Pokutta. Donāt be greedy, just relax! pruning llms via frank-wolfe. arXiv preprint arXiv:2510.13713, 2025. Kai Ruan, Yilong Xu, Ze-Feng Gao, Yang Liu, Yike Guo, Ji-Rong Wen, and Hao Sun. Discovering physical laws with parallel symbolic enumeration. Nature Computational Science, 6(1):53ā66, January 2026. ISSN 2662-8457. doi: 10.1038/s43588-025-00904-8. URL https://w. nature.com/articles/s43588-025-00904-8. Adil Salim. Accelerating mathematical research with language models: A case study of an interac- tion with GPT-5-Pro on a convex analysis problem, October 2025. Samuel Schmidgall and Michael Moor. AgentRxiv: Towards Collaborative Autonomous Research, March 2025. Samuel Schmidgall, Yusheng Su, Ze Wang, Ximeng Sun, Jialian Wu, Xiaodong Yu, Jiang Liu, Michael Moor, Zicheng Liu, and Emad Barsoum. Agent Laboratory: Using LLM Agents as Research Assistants, June 2025. Johannes Schmitt. Extremal descendant integrals on moduli spaces of curves: An inequality discov- ered and proved in collaboration with AI, December 2025. Andrei Semenov, Matteo Pagliardini, and Martin Jaggi. Benchmarking optimizers for large language model pretraining. arXiv preprint arXiv:2509.01440, 2025. Asankhaya Sharma. OpenEvolve: An open-source evolutionary coding agent. GitHub, 2025. Chongjie Si, Debing Zhang, and Wei Shen. Adamuon: Adaptive muon optimizer. arXiv preprint arXiv:2507.11005, 2025. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean, May 2025. URL http://arxiv.org/abs/2404. 12534. Nat Sothanaphan. Resolution of Erd Ģ os Problem #728: A writeup of Aristotleās Lean proof, January 2026. Weijie J. Su. You Are the Best Reviewer of Your Own Papers: An Owner-Assisted Scoring Mecha- nism, June 2022. Mingjie Sun, Zhuang Liu, Anna Bair, and J. Zico Kolter. A Simple and Effective Pruning Approach for Large Language Models, May 2024. URL http://arxiv.org/abs/2306.11695. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geom- etry without human demonstrations. Nature, 625(7995):476ā482, January 2024. ISSN 1476- 4687. doi: 10.1038/s41586-023-06747-5. URL https://w.nature.com/articles/ s41586-023-06747-5. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition, November 2024. 29 Silviu-Marian Udrescu and Max Tegmark. AI Feynman: A physics-inspired method for symbolic regression. Science Advances, 6(16):eaay2631, April 2020. doi: 10.1126/sciadv.aay2631. URL https://w.science.org/doi/10.1126/sciadv.aay2631. Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. Hilbert: Recursively Building Formal Proofs with Informal Reasoning, September 2025. URL http: //arxiv.org/abs/2509.22819. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. LEGO-Prover: Neural Theorem Proving with Growing Libraries, October 2023. URL http: //arxiv.org/abs/2310.00656. Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, and Bin Dong. Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph, October 2025a. URL http://arxiv.org/abs/2510.04520. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. The- oremLlama: Transforming General-Purpose LLMs into Lean4 Experts, October 2024. URL http://arxiv.org/abs/2407.03203. Yiping Wang, Shao-Rong Su, Zhiyuan Zeng, Eva Xu, Liliang Ren, Xinyu Yang, Zeyi Huang, Xue- hai He, Luyao Ma, Baolin Peng, Hao Cheng, Pengcheng He, Weizhu Chen, Shuohang Wang, Simon Shaolei Du, and Yelong Shen. ThetaEvolve: Test-time Learning on Open Problems, November 2025b. Yongji Wang, Mehdi Bennani, James Martens, S Ģ ebastien Racani ` ere, Sam Blackwell, Alex Matthews, Stanislav Nikolov, Gonzalo Cao-Labora, Daniel S. Park, Martin Arjovsky, Daniel Worrall, Chongli Qin, Ferran Alet, Borislav Kozlovskii, Nenad Toma Ė sev, Alex Davies, Pushmeet Kohli, Tristan Buckmaster, Bogdan Georgiev, Javier G Ģ omez-Serrano, Ray Jiang, and Ching-Yao Lai. Discovery of Unstable Singularities, September 2025c. URL http://arxiv.org/abs/ 2509.14185. Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang, Shihao Zhou, Bin Dong, and Zaiwen Wen. Translating Informal Proofs into Formal Proofs Using a Chain of States, December 2025d. URL http://arxiv.org/abs/2512.10317. Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, and Tiancheng Zhang. Aut- oformalization in the Era of Large Language Models: A Survey, May 2025. URL http: //arxiv.org/abs/2505.23486. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with Large Language Models, May 2022. URL http: //arxiv.org/abs/2205.12615. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large- Scale Synthetic Data, May 2024. URL http://arxiv.org/abs/2405.14333. Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haox- iong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, and Zhenguo Li. Mathesis: Towards Formal Theorem Proving from Natural Languages, June 2025. URL http://arxiv.org/abs/2506.07047. Yutaro Yamada, Robert Tjarko Lange, Cong Lu, Shengran Hu, Chris Lu, Jakob Foerster, Jeff Clune, and David Ha. The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search, April 2025. URL http://arxiv.org/abs/2504.08066. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models, October 2023. URL http://arxiv.org/abs/2306.15626. 30 Jie Zhang, Cezara Petrui, Kristina Nikoli Ģ c, and Florian Tram ` er. RealMath: A Continuous Bench- mark for Evaluating Language Models on Research-Level Mathematics, October 2025a. Lan Zhang, Marco Valentino, and Andre Freitas. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions. In Christos Christodoulopoulos, Tanmoy Chakraborty, Carolyn Rose, and Violet Peng (eds.), Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, p. 1720ā1738, Suzhou, China, November 2025b. Association for Computational Linguistics. ISBN 979-8-89176-332-6. doi: 10.18653/v1/2025.emnlp-main. 90. URL https://aclanthology.org/2025.emnlp-main.90/. Ruijie Zhang, Yequan Zhao, Ziyue Liu, Zhengyang Wang, and Zheng Zhang. Muon+: Towards better muon via one additional normalization step. arXiv preprint arXiv:2602.21545, 2026. Yingtao Zhang, Haoli Bai, Haokun Lin, Jialin Zhao, Lu Hou, and Carlo Vittorio Cannistraci. Plug-and-Play: An Efficient Post-training Pruning Method for Large Language Models. In The Twelfth International Conference on Learning Representations, October 2023. URL https: //openreview.net/forum?id=Tr0lPx9woF. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A cross-system benchmark for formal Olympiad-level mathematics, February 2022. Tianshi Zheng, Zheye Deng, Hong Ting Tsang, Weiqi Wang, Jiaxin Bai, Zihao Wang, and Yangqiu Song. From automation to autonomy: A survey on large language models in scientific discov- ery. In Christos Christodoulopoulos, Tanmoy Chakraborty, Carolyn Rose, and Violet Peng (eds.), Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, p. 17733ā17750, Suzhou, China, November 2025a. Association for Computational Linguistics. ISBN 979-8-89176-332-6. doi: 10.18653/v1/2025.emnlp-main.895. Tianshi Zheng, Zheye Deng, Hong Ting Tsang, Weiqi Wang, Jiaxin Bai, Zihao Wang, and Yangqiu Song. From Automation to Autonomy: A Survey on Large Language Models in Scientific Dis- covery, September 2025b. URL http://arxiv.org/abs/2505.13259. Zhanke Zhou, Chentao Cao, Xiao Feng, Xuan Li, Zongze Li, Xiangyu Lu, Jiangchao Yao, Weikai Huang, Tian Cheng, Jianghangfan Zhang, Tangyu Jiang, Linrui Xu, Yiming Zheng, Brando Mi- randa, Tongliang Liu, Sanmi Koyejo, Masashi Sugiyama, and Bo Han. AlphaApollo: A System for Deep Agentic Reasoning, March 2026. Max Zimmer, Megi Andoni, Christoph Spiegel, and Sebastian Pokutta. Perp: Rethinking the prune- retrain paradigm in the era of llms. arXiv preprint arXiv:2312.15230, 2023a. Max Zimmer, Christoph Spiegel, and Sebastian Pokutta. How I Learned To Stop Worrying And Love Retraining. In The Eleventh International Conference on Learning Representations, 2023b. URL https://openreview.net/forum?id=_nF5imFKQI. Max Zimmer, Christoph Spiegel, and Sebastian Pokutta. Sparse model soups: A recipe for improved pruning via model averaging. In The Twelfth International Conference on Learning Representa- tions, 2024. Max Zimmer, Christoph Spiegel, and Sebastian Pokutta. Compression-aware Training of Neu- ral Networks using Frank-Wolfe, p. 137ā168.De Gruyter, Berlin, Boston, 2025.ISBN 9783111376776.doi: doi:10.1515/9783111376776-010.URL https://doi.org/10. 1515/9783111376776-010. Max Zimmer, Christophe Roux, Moritz Wagner, Deborah Hendrych, and Sebastian Pokutta. Spars- eSwaps: Tractable LLM Pruning Mask Refinement at Scale, February 2026. URL http: //arxiv.org/abs/2512.10922. Haohan Zou, Jie Feng, Hao Zhao, and Yuanyuan Shi. Analytical Lyapunov Function Discovery: An RL-based Generative Approach, June 2025. URL http://arxiv.org/abs/2502.02014. 31