Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
Honghao Lin, David Woodruff and colleagues at Google Research and Carnegie Mellon University build Stellar Colosseum, a model-agnostic many-agent harness that allocates inference across long-horizon research in mathematics and theoretical computer science, and use it with Gemini 3.1 Pro to obtain several new results on open problems.
Ask this paper
Research pipeline: Colosseum explores alternative proof strategies first, applies a readiness gate before decomposing a route, splits the proof plan into interdependent section-level subproblems, and sends verifier findings back to the section they affect.
Inside each stage: Candidates are generated in parallel, attacked with targeted falsification, and merged with their critiques through overlapping random-sample tree aggregation into one research artifact.
Research output: The paper reports new results on problems from FOCS and JMLR papers, including coresets for subspace approximation, a condition-number barrier in sparse least squares and dimension lower bounds for inner-product embeddings, plus case studies on a long proof for Knuth cycles and an independent rediscovery of a recent Erdos unit-distance result.
Benchmarks: On TCS-Bench, research-level theorem-proving tasks drawn from FOCS, STOC and SODA papers, Colosseum reaches 71.0% with Gemini 3.1 Pro and Gemini 3.7 Flash. In a Codeforces evaluation the proof-oriented pipeline with execution feedback solves 218 of 222 problems.
Deployment: The workflow is integrated into Google Antigravity as the Long Proof pattern of its Teamwork framework.
Abstract
Language models can produce plausible short proofs, but may still be unreliable on long-horizon research problems, where progress depends on a sequence of uncertain and interdependent decisions. We introduce Stellar Colosseum, a model-agnostic harness for allocating inference across research in mathematics and theoretical computer science. Colosseum explores alternative strategies before proof construction, uses a readiness gate to decide when a route is mature enough to decompose, represents the proof plan as interdependent section-level subproblems, and routes verifier findings back to the affected part of the argument. Across these stages, it generates candidates in parallel, attacks them with targeted falsification, and combines candidates and their critiques into a single research artifact through overlapping random-sample tree aggregation. The Colosseum workflow has also been integrated into Google Antigravity's Teamwork framework as the Long Proof pattern. We demonstrate the capabilities of Colosseum through open-ended research and evaluations on theorem-proving and competitive programming benchmarks. Using Colosseum with Gemini 3.1 Pro, we obtain several new results that address open problems arising from papers published at top venues such as FOCS and JMLR. On TCS-Bench, a benchmark of research-level theorem-proving tasks drawn from papers published at FOCS, STOC, and SODA, Colosseum achieves 71.0% accuracy using Gemini 3.1 Pro and Gemini 3.7 Flash. In a separate Codeforces evaluation using Gemini 3.1 Pro, the proof-oriented pipeline with execution feedback solves 218 of 222 problems.