Google researchers have published Stellar Colosseum, a many-agent harness that allocates inference across mathematics and theoretical computer science research, reporting 71.0% accuracy on a benchmark of research-level theorem-proving tasks drawn from FOCS, STOC and SODA papers. The paper, from a team including Honghao Lin, David P. Woodruff and Vahab Mirrokni, describes a system that is model-agnostic by design and has already been folded into Google Antigravity.
The premise is a familiar failure mode. Language models produce plausible short proofs but degrade on long-horizon problems, where progress depends on a chain of uncertain, interdependent decisions and one bad early commitment poisons everything downstream. Colosseum's answer is to stop treating a proof as a single trajectory.
Key takeaways
- Stellar Colosseum scores 71.0% on TCS-Bench, a set of research-level theorem-proving tasks pulled from FOCS, STOC and SODA papers, using Gemini 3.1 Pro paired with Gemini 3.7 Flash.
- In a separate Codeforces evaluation with Gemini 3.1 Pro, the proof-oriented pipeline with execution feedback solved 218 of 222 problems.
- The workflow now ships inside Google Antigravity's Teamwork framework as the Long Proof pattern, available as a preview command on paid plans.
How the harness spends its compute
Colosseum runs several stages before it commits to writing a proof. It first explores alternative strategies rather than descending into the first one that looks promising, then applies a readiness gate that decides whether a given route is mature enough to decompose. Only then does it represent the proof plan as a set of interdependent section-level subproblems.
Verification is wired back into that structure. When a verifier flags a problem, the finding is routed to the specific part of the argument it affects instead of forcing a restart. Across every stage the harness generates candidates in parallel, attacks them with targeted falsification, and merges candidates and their critiques into a single research artifact through what the authors call overlapping random-sample tree aggregation.
That is a different bet from scaling a single agent's context and letting it think longer. It is closer to running a small adversarial research group, where the expensive resource being scheduled is inference rather than researcher time.
What the benchmark numbers say
TCS-Bench is a harder target than the contest-math sets that dominate model announcements, since its tasks are taken from papers accepted at three of the field's top theory venues. The 71.0% figure comes from a mixed configuration: Gemini 3.1 Pro alongside the cheaper Gemini 3.7 Flash, which suggests the harness recovers quality through coordination rather than by routing everything to the largest model.
The Codeforces result is narrower but striking β 218 of 222 problems solved with execution feedback in the loop. Both numbers come from the authors' own evaluation, and neither has been independently reproduced. The benchmark caveat that applies to every agent-scaffold paper applies here too: harness results are notoriously sensitive to prompt and tooling details that rarely survive reimplementation.
From paper to product
Unlike most research scaffolds, this one already has a shipping surface. Google says the Colosseum workflow is integrated into Antigravity's Teamwork framework as the Long Proof pattern, one of five patterns the system selects between, and that Teamwork has produced seven open-problem results including a sparse convex optimization question from JMLR and Knuth's Cycles Conjecture, verified in Lean.
The paper claims new results addressing open problems from FOCS and JMLR papers. That is a meaningfully different claim from benchmark accuracy, and it is the one the field will scrutinize hardest β as it did with OpenAI's 10,000-agent Navier-Stokes attempt, where the asterisks mattered more than the headline. Formal verification in Lean gives Google a stronger footing on at least part of that claim.
FAQ
What is TCS-Bench?
TCS-Bench is a benchmark of research-level theorem-proving tasks drawn from papers published at FOCS, STOC and SODA, three leading theoretical computer science venues. It targets open-ended research problems rather than competition exercises. Stellar Colosseum reports 71.0% accuracy on it using Gemini 3.1 Pro with Gemini 3.7 Flash.
Is Stellar Colosseum tied to Gemini?
No. The authors describe the harness as model-agnostic β it is a scheduling and aggregation layer over whatever model serves the calls. The published evaluations use Gemini 3.1 Pro and Gemini 3.7 Flash, so its reported numbers are specific to those models, not to the architecture itself.
Can developers use it today?
Indirectly. The Colosseum workflow is available inside Google Antigravity's Teamwork framework as the Long Proof pattern, offered as a preview command on paid plans. The paper itself is a preprint on arXiv and has not been peer reviewed.
