Source-linked AI summary
AI co-mathematician: Accelerating mathematicians with agentic AI
Daniel Zheng, Ingrid von Glehn, Yori Zwols, Iuliya Beloshapka, Lars Buesing, Daniel M. Roy, Martin Wattenberg, Bogdan Georgiev, Tatiana Schmidt, Andrew Cowie, Fernanda Viegas, Dimitri Kanevsky, Vineet Kahlon, Hartmut Maennel, Sophia Alj, George Holland, Alex Davies, Pushmeet Kohli
TL;DR
Mathematical research requires long-term orchestration of exploratory, iterative, and collaborative activities beyond isolated problem solving. The AI co-mathematician provides a stateful workspace that coordinates agents with human researchers, and early tests include resolving an open problem and achieving 48% accuracy on FrontierMath.
Problem
Existing AI-for-mathematics systems under-support long-term, stateful orchestration of uncertainty, literature, artifacts, and branching hypotheses in mathematical research.
Method
The AI co-mathematician is a stateful workbench where a project coordinator delegates tasks across parallel workstreams while users interact with evolving research.
Results
The system helped resolve an open mathematical problem and achieved 48% accuracy on FrontierMath, solving 23 of 48 problems.
Takeaways & Limitations
The system demonstrates an interactive, human-in-the-loop paradigm for AI-assisted mathematical discovery.
Takeaways & Limitations
Reviewer constraints can rarely produce arguments that remain flawed but evade reviewer detection, violating explicit uncertainty acknowledgement.
Abstract
from arXiv · showhide
We introduce the AI co-mathematician, a workbench for mathematicians to interactively leverage AI agents to pursue open-ended research. The AI co-mathematician is optimized to provide holistic support for the exploratory and iterative reality of mathematical workflows, including ideation, literature search, computational exploration, theorem proving and theory building. By providing an asynchronous, stateful workspace that manages uncertainty, refines user intent, tracks failed hypotheses, and outputs native mathematical artifacts, the system mirrors human collaborative workflows. In early tests, the AI co-mathematician helped researchers solve open problems, identify new research directions, and uncover overlooked literature references. Besides demonstrating a highly interactive paradigm for AI-assisted mathematical discovery, the AI co-mathematician also achieves state of the art results on hard problem-solving benchmarks, including scoring 48% on FrontierMath Tier 4, a new high score among all AI systems evaluated.
1. Introduction
Mathematical research is exploratory and iterative, but existing AI-for-mathematics systems under-support its long-term orchestration. The AI co-mathematician introduces a stateful, interactive workbench that coordinates agents and complements existing reasoning and search systems.
- Mathematical research involves testing intuitions, finding counterexamples, and repeatedly revising definitions and proofs beneath polished publications.
- Existing AI systems support autonomous reasoning and exploratory search, but long-term orchestration of these capabilities remains under-supported.
- Standard chat interfaces are transient, while specialized engines lack broader context, forcing researchers to connect brainstorming, formal provers, and computational scripts manually.
- The AI co-mathematician is a workbench for interactively leveraging AI agents in open-ended mathematical research.
- A stateful workspace lets a project coordinator delegate tasks across parallel workstreams while users direct and interact with evolving research.
- The system is designed to complement frontier reasoners and evolutionary iterators, although its current release is limited.
2. Design Principles for AI-Assisted Mathematics
The AI co-mathematician is designed around the iterative, collaborative reality of mathematical discovery rather than isolated theorem proving. Its principles preserve context, expose uncertainty, and support flexible human steering across parallel work.
- The system supports mathematics as a holistic process involving question refinement, literature search, brainstorming, calculations, simulations, and theorem proving.
- It supports iterative refinement of research questions, definitions, and conjectures as discovery changes the mathematician’s intent.
- A living working paper replaces transient chat logs or prematurely polished manuscripts and records the evolving project state.
- Asynchronous specialized agents work in parallel, allowing substantial computation without blocking user interaction.
- The user can steer the project coordinator directly, while the system flags roadblocks and requests assistance when agents stall.
- Progressive disclosure separates high-level strategy from low-level execution logs to manage cognitive load.
- Version history tracks how claims evolve or become questioned, while failed goals and workstreams remain durable parts of the project record.
3. AI co-mathematician in practice: a walkthrough
The walkthrough shows a workspace in which users refine research goals before agents pursue parallel literature, computational, and search workstreams. Reports, reviews, constraints, and user intervention connect these activities into an auditable workflow.
- Walkthrough: The prototype walkthrough follows an open computational-geometry problem about upper bounds for a sofa moving around left- and right-handed right-angle corners.
- Workspace: A hierarchy of agents shares files and messages, with a project coordinator delegating work and maintaining escalation pathways.
- Initial Exploration: Interactive onboarding converts an initial user request into formally approved research questions and goals through dialogue and revision.
- Branching the Research: The coordinator assigns parallel workstreams to approved goals, allowing multiple workstreams per goal and dependencies between them.
- Workstreams: Workstreams cover literature review, computational-framework design, and branch-and-bound search, with agents producing references, code, tests, and scaled computations.
- Limitations: The current prototype uses standard agent primitives for computational searches, while evolutionary search such as AlphaEvolve is proposed as a future addition.
- Interactive Steering and Hard Constraints: Hard programmatic constraints and active human steering target invalid shortcuts, hallucinated lemmas, hand-waved details, and premature success claims.
- The Final Output: Each completed workstream produces a compiled and reviewed LaTeX write-up rather than a transient chat message.
4. The Evaluation of Interactive Mathematical Agents
Static benchmarks remain common, but the paper argues that interactive mathematical agents should also be evaluated on broader research capabilities and with humans in the loop. It presents this framing as a response to improving raw problem-solving performance.
- AI-for-mathematics evaluation has historically relied on static problem-solving benchmarks such as IMO ProofBench, FrontierMath, PutnamBench, MATH, and GSM8K.
- As frontier systems reach or exceed expert-human performance on raw problem solving, improving that capability may provide diminishing incremental value.
- The paper calls for wider evaluation across capabilities analogous to mathematical research, including fact-finding and mistake-finding.
- AI-for-mathematics systems should be considered human-in-the-loop by default and assessed accordingly.
5. Early Results with Mathematicians
Early mathematicians used the AI co-mathematician across topology, group theory, representation theory, and Hamiltonian systems, with workstreams supporting exploration, proof development, and literature-guided research. These independently produced cases included an open-problem resolution, two conjecture proofs under human review, and a key lemma that essentially resolved another question.
- Scope of early use: Early users applied the system to diverse research tasks, including literature navigation, numerical exploration, conjecture testing, theorem proving, and theory development.The tool was used by a small number of professional mathematicians directly, without supervision or intervention from GDM researchers.
- Kourovka problem: One topology and group theory investigation resolved Problem 21.10 from the Kourovka Notebook, whose answer was affirmative.The problem asks whether every finite group admits a just finite presentation.
- Kourovka problem: The Kourovka workstream combined computational search, literature analysis, adversarial review, and a pivot from a sharper conjecture to a positive proof strategy.Reviewer agents identified a proof method after the initial computational and theoretical exploration did not settle the conjecture; the mathematician then completed the argument and revised the paper.
- Stirling coefficients: For Stirling coefficients, the system established proofs for two conjectures in separate workstreams, while also providing computational evidence for proved and unproved claims.The proofs were undergoing detailed human review, and a marginal comment surfaced a key insight that the researcher followed up in chat.
- Hamiltonian systems: In a Hamiltonian-systems subproblem, the system produced a carefully checked proof containing an elegant key lemma that essentially resolved the question.The workflow included specialized literature review and follow-up queries before a proof-writing agent produced the result.
- Observed value: Across these cases, users reported practical value from reaching dead ends faster and obtaining comparatively high-quality correct proofs, while integrating the system into exploratory workflows.Rezchikov specifically described moving on from an unproductive approach sooner and rated the aesthetic quality of correct proofs highly.
6. Problem-Solving Benchmark Results
The AI co-mathematician outperformed single-call Gemini baselines on internal research mathematics problems and achieved a 48% score on FrontierMath Tier 4. Its examples illustrate how persistent, tool-using, parallel workflows support computational reductions, literature retrieval, and iterative error correction.
- Internal evaluation: The AI co-mathematician significantly outperformed single calls to Gemini 3.1 Pro and Gemini Deep Think on the internal benchmark.The system uses more compute, including agents built on Gemini 3.1 Pro and a prover agent that can use Gemini Deep Think.
- Representative examples: On a geometric-tilings problem, the system reduced the task to Boolean satisfiability and solved it using the PySAT library.The required adaptations favored persistent filesystems and agentic code-writing over purely theoretical solution attempts.
- Representative examples: On a representation-theory problem, literature-search tools retrieved exact theorem statements and matched their conditions to the problem’s assumptions.Other models attempted broader theorems without literature access to verify precise statements.
- Representative examples: On a combinatorics problem, parallel theoretical and computational workstreams used reviewer spot-checks to identify and correct logical errors before assembling the final report.The project coordinator combined the corrected components into a correct solution.
- FrontierMath: 48% accuracy: the AI co-mathematician correctly solved 23 of 48 FrontierMath Tier 4 problems, excluding two public samples.Epoch AI conducted the evaluation blind, with direct access to the system UI.
7. Challenges and Limitations
The paper identifies limitations in review dynamics, autonomy, representation, and the broader mathematical ecosystem. These include flawed consensus, non-terminating disagreement, reduced controllability, semantic ambiguity, and pressures on literature and peer review.
- Agent dynamics: Reviewer constraints can drive a flawed argument toward apparent consensus when errors become undetectable to the reviewer agent.The authors describe this reviewer-pleasing bias as relatively rare but still a violation of reliable reasoning.
- Agent dynamics: Iterative review can fail to terminate when agents cannot reach consensus, producing revision cycles that may degrade into hallucinated reasoning.The authors call this failure mode a “death spiral” and note that users learn to down-weight affected outputs.
- Autonomy: Long autonomous runs make user control difficult because current models’ judgment on unplanned difficulties remains behind human capabilities and expectations.Mathematical research often cannot be fully planned in advance because finding the correct sequence of steps can itself be the solution.
- Representations: Well-typeset documents can falsely suggest rigor because language models generate polished LaTeX while struggling with rigorous logical verification.The system currently addresses this by labeling outputs as working documents with marginalia, while the authors call for more intuitive representations.
- Ecosystem risks: AI-generated mathematical output could increase semantic noise and burden peer review if used as autonomous generation without auditable paper trails.The paper notes that AI can produce a 20-page proof attempt in minutes while human experts may need days to verify it.
8. Conclusion
AI systems that solve static mathematical problems do not yet cover the messy, collaborative process of frontier research. The AI co-mathematician addresses this gap while motivating evaluation of collaborative efficacy, stateful exploration, and uncertainty management.
- Frontier mathematical research involves unproven intuition, branching hypotheses, and complex human collaboration beyond static problem solving.The paper frames benchmark success as only part of the solution to accelerating discovery.
- The AI co-mathematician captures failed tests, synthesized literature, and idea refinement in a living working paper for user-steered research.It combines hierarchical delegation, uncertainty management, native mathematical artifacts, and hard programmatic constraints.
- Early users resolved open problems and found novel proofs through bidirectional exchange that let humans steer AI past difficult bottlenecks.
- Current benchmarks evaluate final answers to curated problems but omit interactive hypothesis pruning, niche-literature synthesis, and uncertainty disclosure when scaling fails.
- The paper calls for complementary evaluation frameworks measuring collaborative efficacy, stateful exploration, and rigorous uncertainty management.
Contributions
The system and its interface were developed through contributions spanning prototype design, core-system development, research, testing, workflow design, visual language, and external access.
- Y.Z. designed the initial system prototype, while a broader team continued core-system and user-interface development.
- The team performed research on improving capabilities and incorporated input on research ideas, testing, and prototype iterations.
- Contributions also covered user-interface workflow, visual language, and routes for external users to access the system.