AI Co-Mathematician: From Proof Assistants to Research Partners

Paper: 2605.06651 Authors: Daniel Zheng, Ingrid von Glehn, Yori Zwols, Iuliya Beloshapka, Lars Buesing, Daniel M. Roy, Martin Wattenberg, Bogdan Georgiev, Tatiana Schmidt, Andrew Cowie Categories: cs.AI

The Gap

Existing AI for mathematics has focused on narrow tasks: theorem proving (Lean, Coq), symbolic computation (Mathematica), or benchmark problem-solving. These tools treat mathematics as a linear pipeline—state a conjecture, prove it, done. But real mathematical research is exploratory and iterative: you chase hunches, hit dead ends, pivot based on computational experiments, search literature for related work, and refine vague intuitions into precise statements. Current AI systems don’t support this messy, asynchronous workflow. They’re calculators, not collaborators.

The gap: no system provides holistic support for the full research cycle—ideation, literature search, computational exploration, theorem proving, and theory building—while managing uncertainty, tracking failed attempts, and maintaining state across sessions.

Problem: Math research is exploratory          Assumption: AI can mirror human
         and iterative, not linear                        collaborative workflow
                |                                                |
                v                                                v
         Current AI: task-specific            Method: Stateful workbench with
         tools (provers, CAS)          -->    async agents + uncertainty mgmt
                                                               |
                                                               v
                                              Evidence: 48% on FrontierMath Tier 4
                                                       + open problem solutions
                                                               |
                                                               v
                                              Conclusion: AI can be research
                                                         partner, not just tool

The Increment

One sentence: Before this paper, AI helped mathematicians solve stated problems; after, AI helps mathematicians discover what problems to solve.

Core Mechanism

The AI co-mathematician is a stateful workspace where multiple AI agents operate asynchronously on behalf of the user. When you give it a vague research direction, it spawns agents to explore different angles: one searches literature, another runs computational experiments, a third attempts formal proofs. Each agent maintains its own state and can run for hours or days. The system tracks hypotheses, records failures (so you don’t repeat them), and refines your intent through interaction.

The workspace outputs native mathematical artifacts: Lean proofs, computational notebooks, literature summaries, conjectures with supporting evidence. Agents communicate through a shared context that includes your research notes, previous attempts, and domain knowledge. When an agent hits uncertainty (ambiguous notation, multiple interpretations), it flags the issue and asks for clarification rather than guessing.

User intent (vague)
        |
        v
   [Workspace State]
        |
        +---> Agent 1: Literature search -----> Papers, references
        |
        +---> Agent 2: Computation -----------> Numerical evidence
        |
        +---> Agent 3: Theorem proving -------> Lean proofs
        |
        +---> Agent 4: Theory building -------> Conjectures
        |
        v
   [Shared Context]
   - Research notes
   - Failed hypotheses
   - Refined intent
        |
        v
   Mathematical artifacts
   (proofs, notebooks, summaries)

Think of it like a research group where you’re the PI. You give a broad direction at a Monday meeting. Your grad students (agents) go off and work independently—one hits the library, another runs simulations, a third tries to formalize something in Lean. They don’t need you to micromanage every step. On Friday, they report back with results, questions, and dead ends. You refine the direction based on what worked, and the cycle continues. The key difference from a single AI assistant: parallelism, persistence, and memory of what didn’t work.

Key Concepts

• Stateful workspace: Most AI interactions are stateless—each query starts from scratch. A stateful workspace remembers everything: your research notes, previous conversations, failed attempts, computational results. It’s like having a lab notebook that never closes. When you return after a week, the system knows where you left off and what you’ve already tried. This persistence is critical for research, where insights emerge over months, not minutes.

• Asynchronous agents: Instead of waiting for one task to finish before starting the next, agents run in parallel and report back when done. If literature search takes 10 minutes and a proof attempt takes 2 hours, you don’t sit idle. The system manages multiple threads of exploration simultaneously, just like a human researcher juggling several subproblems. Agents can also run overnight or across sessions—you check in when convenient.

• Uncertainty management: When an agent encounters ambiguity (e.g., “Does ‘smooth’ mean C^1 or C^∞?”), it doesn’t guess or hallucinate. It flags the uncertainty, presents options, and waits for clarification. This prevents the system from confidently pursuing the wrong interpretation. It’s the difference between a collaborator who asks “What did you mean by X?” and one who assumes and wastes a week on the wrong problem.

Framework Shift

Before (task-specific tools):        After (AI co-mathematician):

User: "Prove theorem X"              User: "I'm interested in property Y"
  |                                    |
  v                                    v
[Theorem Prover]                     [Workspace spawns agents]
  |                                    |
  v                                    +---> Literature
Success or failure                     +---> Computation
                                       +---> Proving
(One-shot, stateless)                  +---> Theory building
                                       |
                                       v
                                     [Shared context tracks progress]
                                       |
                                       v
                                     Artifacts + refined questions
                                     
                                     (Iterative, stateful, exploratory)

From single-task execution to multi-threaded exploration, the core shift is treating AI as a research partner that manages its own subgoals rather than a tool that executes your commands.

Expert Assessment

Problem choice: This is a real gap. Anyone who’s done mathematical research knows the pain of context-switching between Lean, Mathematica, Google Scholar, and scratch paper. The field has been stuck in “AI for X” mode (AI for theorem proving, AI for symbolic math) rather than “AI for research.” The timing is right—foundation models are finally capable enough to handle the reasoning required.

Method maturity: The architecture is sound but not groundbreaking. Stateful workspaces and asynchronous agents are well-understood in software engineering. The novelty is in the application and integration, not the underlying techniques. That said, the uncertainty management is clever—most systems either hallucinate or refuse to act, but flagging ambiguity and asking for clarification is the right middle ground.

Experimental integrity: The 48% on FrontierMath Tier 4 is impressive and verifiable. The open problem anecdotes are compelling but anecdotal—we don’t know how many problems were attempted vs solved. The paper would be stronger with failure rate analysis and a breakdown of where the system struggles. Baselines are fair (comparing to other AI systems on the same benchmark), but there’s no comparison to human mathematicians’ workflows, which would be the real test.

Writing quality: The abstract and introduction are strong. The technical sections are vague—how exactly do agents communicate? What’s the prompt structure? How is uncertainty represented? The paper reads like a product announcement more than a research contribution. Section 3 (system architecture) needs to be twice as long with concrete examples of agent interactions.

Verdict: weak accept — Addresses a real problem with a practical solution and strong benchmark results, but lacks technical depth and rigorous evaluation of the exploratory workflow claims.

Takeaways

Stateful context for long-running tasks: If you’re building AI assistants for any domain with iterative workflows (design, research, debugging), maintain state across sessions. Don’t make users re-explain context every time. Store failed attempts explicitly so the system doesn’t repeat mistakes.

Asynchronous agent architecture: For tasks with multiple independent subtasks, spawn parallel agents rather than sequential execution. This maps naturally to how humans work—we don’t finish one thing before starting another; we juggle.

Uncertainty as a first-class citizen: When your system encounters ambiguity, don’t guess. Flag it, present options, and ask. This prevents compounding errors and builds trust. Implement this as a structured output type, not just a text response.

Benchmark design insight: FrontierMath Tier 4 is interesting because it requires multi-step reasoning and exploration, not just pattern matching. If you’re evaluating AI for complex domains, design benchmarks that reward exploration and penalize lucky guesses.