Zero: A Meta-Agent for Mathematical Research

A mathematician using AI tools must decide which systems to use, how to combine them, and how to verify their results. Published benchmarks offer limited guidance for an open research problem, while testing every alternative is often far too expensive. We call the problem of finding and adapting a suitable resource configuration the _capability estimation problem_ ($\texttt{CEP}$). To address the $\texttt{CEP}$, we introduce Zero, a meta-agent that uses published research and evidence from its own attempts to select resources. Zero constructs workflows for agents and tools and revises them during execution, allowing researchers to inspect and interactively steer the work. In a formalization campaign, unsuccessful attempts prompt trials of alternative provers and revisions to execution budgets. Using Zero, we also resolve open questions on Lagrangian relaxation through counterexample construction and Lean formalization. Finally, we extend existing research harnesses with formal verification of a machine-learning theory result and reproduce optimization computations using open solvers.