Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
Honghao Lin, David P. Woodruff, Yuan Deng, Jieming Mao, Song Zuo, Vahab Mirrokni
cs.AI, cs.CL, cs.LG
2026-09-15
Colosseum explores strategies and decomposes proofs into a DAG. Gemini 3.1 Pro + 3.7 Flash selection hits 71.0% on TCS-Bench and 218/222 Codeforces with execution feedback.
Language models already write plausible short proofs. Long-horizon research fails in a different place: which route to take, how to cut lemmas, and whether to abandon a line after a local collapse. Those choices depend on one another. A shared bug can survive a vote over final drafts, because many traces can be wrong in the same way.
Prior systems split exploration, decomposition, and verification across roles, or they pin every step to a Lean checker. Colosseum targets the setting where the strategy is still unstable and the argument is still in natural language. Proofs can outrun a single model response. Failed attempts may still leave counterexamples, restrictions, and intermediate claims. If those are not stored as specific objections, the next round starts from the original problem again.
Stellar Colosseum is a model-agnostic many-agent harness from Google Research and CMU. It runs at two levels.
The outer loop is a research pipeline. Parallel explorers try different reformulations, intermediate claims, and links to known results. A readiness gate does not ask whether the proof is already done. It asks whether the central mechanism is stable, whether leftover claims can be assigned to sections, and whether an unresolved bridge would rewrite the architecture. Once a route passes, a decomposer turns it into a sectioned DAG: document order is for exposition, the dependency graph is for who can compute first. Independent sections run in parallel. A local reviewer that rejects a section retries only that subproblem. After the skeleton is filled, a global verifier reads the assembled document as one argument, checking wrong assumptions on a dependency, drifting notation, missing cases, and a final claim that does not match the original target. One concrete fatal defect is enough to reject. Majority acceptance is not. If the strategy still looks viable, the system revises sections or the outline; if the spine is gone, it returns to exploration.
Inside a hard stage, the same adversarial pattern repeats. Candidates are generated in parallel, varying representation, main lemma, technique, and assumed line of attack. Reviewers hunt for defects: boundary counterexamples, silently strengthened hypotheses, circularity, misused theorems or citations, and a proved statement that is not the target. Falsification records stay attached. Aggregation is an overlapping random-sample tree: each node draws k distinct inputs from the current population, groups are independent and may overlap. Intermediate nodes construct rather than vote. They may merge compatible pieces, keep competing branches, patch a local flaw, or carry an unresolved conflict upward. Critiques are not averaged away.
Memory across rounds is split. The latest full draft plus verifier notes go into the next attempt. A knowledge directory separately stores theorems and lemmas, failed routes with their exact failure points, literature statements, and observations with evidence. Open-ended research can use exploration trees with slightly more than 100 leaves; later stages stay at 16 leaves. For TCS-Bench and Codeforces, exploration widths are (32, 16, 8, 5, 1) and remaining stages (16, 8, 5, 1), with k=5.
On open problems, the workflow contributed to five later papers. For ℓp subspace approximation with p>2, the same sampling rule supports a strong coreset of size Õp(k^{p/2} ε^{-2}) instead of ε^{-p}, at Õp(nnz(A)+d^ω) time. For sparse least squares, a linear dependence on the restricted condition number cannot be replaced by any fixed sublinear power, assuming the randomized exact-volume Small-Set Expansion Hypothesis. A dimension lower bound for maximum-inner-product embeddings nearly closes the 1/ε versus 1/ε² gap in the exponent. A single-stage Hadamard quantizer removes the residual-stage O(d)-bit payload and cuts the leading constant in the proved bound by about 5.93. For prefix-matrix factorizations, γ{2,1}(Q) is Ω(log^{3/2} n / (log log n)^{3/2}), a (log log n)^{3/2} factor from the dyadic upper bound.
Two case studies stress length and isolation. Knuth's cycles produced 46-page and 75-page proof drafts for two constructions. On the Erdős unit-distance problem, with internet access disabled, Gemini 3.1 Pro ran 15 exploration rounds and wrote a 22-page draft that independently reached an architecture close to the OpenAI solution.
TCS-Bench has 300 theorem-proving tasks from FOCS, STOC, and SODA papers (2020–2026). A reference-assisted grader scored more than 90% on a held-out set of 100 expert-labeled proofs.
| Method | TCS-Bench accuracy |
| Gemini 3.1 Pro, direct | 30.3% |
| Gemini 3.1 DeepThink | 52.0% |
| GPT-5.6 Pro (max) | 68.0% |
| Colosseum + Gemini 3.1 Pro | 54.0% |
| Colosseum + Gemini 3.7 Flash | 55.0% |
| Cross-model selection | 71.0% |
| Oracle best-of-two | 77.3% |
Selection: Gemini 3.7 Flash samples eight critiques of the Pro proof; if at least five call it correct, Pro is submitted, otherwise Flash. The chosen proofs solve 213 problems, 48 more than the stronger single run. Critique scores separate grader-correct from grader-incorrect proofs at AUC 0.896. Routing with Pro's internal verifier alone reaches 64.7%.
The Codeforces suite matches the Gemini 3 Deep Think cut: 222 problems with clist.by difficulty above 1500, from 52 contests numbered 2084–2162, median 2381. Acceptance requires the original checker on the full hidden tests. Gemini 3.1 Pro with a C++ execution probe (public samples and model-generated stress tests) records 218/222 and a corpus-level rating of 4263; without the probe, 213/222 and 3918. The two arms also differ in revision budget, so the five-problem gap is not a causal estimate of the probe.
The workflow is now the Long Proof pattern inside Google Antigravity's Teamwork framework.
For anyone building research agents, the useful piece is the join between "which route is ready" and "how a long proof is written and patched in parallel." Keeping critiques on the candidates they attack, and writing failed routes into a knowledge directory, is aimed at the intermediate work that long-horizon runs usually drop. On competitive programming, the DAG ends in one C++ program rather than software modules, which is a transfer test, not a new code-specific controller.
Read the scores as two different claims. Single-model Colosseum at 54.0% and 55.0% sits just above DeepThink at 52.0% and well below GPT-5.6 Pro (max) at 68.0%. The 71.0% figure is complementary errors plus critique routing. There is no compute-matched comparison with DeepThink.
The research bullets are written as contributions of the workflow. Full proofs live in companion papers. That is not the same as fully autonomous discovery.
There is no dedicated limitations section. The gaps that can be checked in the text are these.
The main artifact is natural-language proof. Formal checks and executable tests count as evidence when they exist; Lean certificates are not the pass condition. TCS-Bench numbers go through an automated grader that is only a bit above 90% on 100 expert labels.
The single-model lift over DeepThink is small, and without a compute-matched baseline it is unclear whether those extra points are the harness or extra inference. Cross-model 71.0% still trails the 77.3% oracle by 6.3 points, so the router kills some good proofs. The Codeforces arms are not isolated: revision budgets differ, and the probe-to-revision path was not validated on its own.
The five research results, the Knuth drafts, and the Erdős rerun all mix human involvement with the harness. The Erdős run recovered a nearby architecture offline in 22 pages; it is not a human-verified published proof.
The paper's own future-work list names the rest: minority strategies can vanish inside a mixed population, a bad section cut can only be retried as-is, tree widths are frozen before a run, and using trajectories for post-training still has a credit-assignment problem.