Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science

Authors: Honghao Lin, David P. Woodruff, Yuan Deng, Jieming Mao, Song Zuo, Vahab Mirrokni (Google Research / Carnegie Mellon University)

---

Summary (Overview)

• Stellar Colosseum is a model-agnostic, many-agent inference harness designed for long-horizon research problems in mathematics and theoretical computer science, addressing the unreliability of language models on tasks requiring sequences of uncertain, interdependent decisions.
• The system introduces a five-stage research pipeline (strategy exploration, readiness gate, proof decomposition, subproblem solving, global verification) combined with a stage-level adversarial inference procedure featuring parallel candidate generation, targeted falsification, and overlapping random-sample tree aggregation.
• The workflow contributed to five new research results addressing open problems from papers at FOCS and JMLR, including improved coresets for $\ell_p$ subspace approximation, a condition-number barrier in sparse least squares, and dimension lower bounds for maximum inner product embeddings.
• On TCS-Bench (300 research-level theorem-proving tasks from FOCS/STOC/SODA), Colosseum achieves 71.0% accuracy via cross-model selection between Gemini 3.1 Pro and Gemini 3.7 Flash, surpassing direct model baselines (best direct: 68.0% for GPT-5.6 Pro).
• In a Codeforces evaluation of 222 problems (difficulty ≥ 1500), the proof-oriented pipeline with execution feedback solves 218 problems (performance rating 4263), demonstrating transfer from theorem proving to executable algorithmic tasks.

---

Introduction and Theoretical Foundation

Motivation

Language models have made substantial progress in mathematical reasoning, solving olympiad-level problems [52, 29] and contributing to new research results [21, 56]. However, long-horizon research problems remain challenging because progress depends on a sequence of uncertain and interdependent decisions. Key difficulties include:

• Strategic Uncertainty: The route to a proof may be unclear; finding useful representations, reductions, or intermediate targets requires exploration.
• Distributed Technical Difficulty: Proofs may contain several interdependent bottlenecks; resolving one difficulty can expose another.
• Long Outputs and Error Accumulation: Long proofs exceed single-response output budgets, and definitions/assumptions must remain consistent across distant sections.
• Failure and Partial Progress: Failed attempts may yield useful counterexamples or intermediate results that must be recorded as specific claims rather than generic failure judgments.

Theoretical Basis

The work builds on inference-time scaling principles: sampling multiple reasoning paths [55], searching over intermediate states [60], iterative critiquing [44], and multi-agent debate [18]. However, the authors argue that flat voting over final answers offers limited guidance for proofs because agreement among candidates can hide shared errors. The challenge is to use additional computation to choose between approaches, uncover specific gaps, and preserve useful work after failures.

Relationship to Prior Work

Colosseum extends the parallel exploration and iterative verification architecture of Woodruff et al. [56], adding:

• Explicit control over research stages
• Dependency-aware proof construction
• Aggregation that preserves critiques alongside synthesized content

It differs from formal-proof systems (e.g., LeanMarathon [61], Danus [42]) in that it works with natural-language proof drafts, using formal checks and executable tests as evidence alongside model-generated critiques when available.

---

Methodology

4.1 Adversarial Generation and Tree-Structured Aggregation

Parallel Candidate Generation

Colosseum generates a population of candidates at each stage, varying:

• Representation, principal lemma, proof technique, case split, interpretation of evidence, or location of the main bottleneck
• Seeds, temperatures, prompt perspectives, tool access, and assumed lines of attack

Each candidate follows a typed schema (e.g., a strategy proposal states its mechanism, required lemmas, expected bottleneck, and a falsifiable test).

Targeted Falsification

Adversarial reviewers examine each candidate for:

• Counterexamples and boundary cases
• Invalid implications or silently strengthened hypotheses
• Circularity and undeclared dependencies
• Misuse of theorems, computations, or external references
• Mismatch between proved statement and target claim
• Missing assumptions needed by later sections

Tree-Structured Aggregation

Let $z_i$ denote a candidate bundled with its falsification records, and let:

$$C^{(0)} = \{z_1, \ldots, z_n\}$$

The tree shape is specified by population widths $(m_0, m_1, \ldots, m_L)$ with $m_0 = n$, $m_L = 1$. For the transition from level $\ell$ to $\ell+1$, each of the $m_{\ell+1}$ aggregation nodes independently draws $k_\ell$ distinct inputs uniformly:

$$G_j^{(\ell)} \sim \text{Unif}\{G \subseteq C^{(\ell)} : |G| = k_\ell\}, \quad j = 1, \ldots, m_{\ell+1}$$

Each node computes:

$$s_j^{(\ell+1)} = \mathcal{A}\left(x, K, G_j^{(\ell)}\right), \quad C^{(\ell+1)} = \{s_j^{(\ell+1)}\}_{j=1}^{m_{\ell+1}}$$

where $\mathcal{A}$ is the stage-specific aggregator, $x$ the current input artifact, and $K$ contextual evidence. The expected reuse of a node is:

$$\mathbb{E}[R_i^{(\ell)}] = \frac{m_{\ell+1} k_\ell}{m_\ell}$$

Ordinary contraction layers use expected reuse of roughly 2–3 (e.g., 128→64 nodes with sample size 5 gives expected reuse 2.5). Aggregation is constructive (merging compatible components, retaining competing branches, repairing localized flaws) rather than a vote or ranking.

4.2 The Research Pipeline

Stage 1 – Strategy Exploration: Parallel attempts develop routes based on different reformulations, intermediate claims, and connections to known results.

Stage 2 – Readiness Gate: Tests whether a route is concrete enough to support a proof plan: the central reduction is stable, unresolved claims are precise enough to assign to sections, and no unresolved bridge is likely to change the target or architecture.

Stage 3 – Proof Decomposition: Produces a numbered, sectioned proof skeleton with a directed acyclic graph (DAG) of dependencies. Document order controls exposition; the dependency graph controls the order of mathematical work.

Stage 4 – Subproblem Solving: Independent sections solved in parallel. Local reviewers check each section; failed sections are retried locally without restarting unaffected work.

Stage 5 – Global Verification: Evaluates the assembled proof as a whole, checking for: wrong assumptions in dependency usage, notation drift, omitted cases, mismatched conclusions, and silently inherited conditional claims. Rejected proofs enter revision (replace sections or modify outline) or re-exploration (if the central strategy is undermined).

4.3 Shared Research Knowledge

Two complementary memory forms:

1. Retained prior attempts: The latest draft and verifier feedback pass directly into the next round.
2. Knowledge directory: A curator records four kinds of reusable knowledge:
   • Theorems and lemmas (with hypotheses, arguments, applications)
   • Failed approaches (precise failure points, conditions for viable variants)
   • References (relevant literature with statements and hypotheses)
   • Observations (structural properties, computational findings)

4.4 Inference Configurations

---

Empirical Validation / Results

5.1 Strong Coresets for $\ell_p$ Subspace Approximation ($p > 2$)

For $A \in \mathbb{R}^{n \times d}$, the goal is to preserve simultaneously for every subspace $F$ of dimension at most $k$:

$$\|SA(I - P_F)\|_{p,2}^p = (1 \pm \varepsilon)\|A(I - P_F)\|_{p,2}^p$$

Woodruff and Yasuda obtained coreset size $\tilde{O}_p(k^{p/2}\varepsilon^{-p})$ [57]. Colosseum's proof shows the same sampling rule supports coreset size $\tilde{O}_p(k^{p/2}\varepsilon^{-2})$ with running time $\tilde{O}_p(\text{nnz}(A) + d^\omega)$, by keeping the truncation in sampling probabilities when bounding surviving rows [40].

5.2 Condition-Number Barrier in Sparse Least Squares

Under the randomized exact-volume Small-Set Expansion Hypothesis, for every fixed $\gamma \in (0,1]$, no randomized polynomial-time algorithm can return $x$ with:

$$\|Ax - b\|_2^2 \leq \min_{\|z\|_0 \leq k}\|Az - b\|_2^2 + \varepsilon \quad \text{and} \quad s = O\left(\frac{k\kappa^{1-\gamma}}{s} + k\right)$$

where $\kappa_r$ is the restricted condition number at sparsity level $r$ and $s = \|x\|_0$ [38].

5.3 Dimension Lower Bounds for Maximum Inner Product Embeddings

For every fixed $\delta \in (0,1)$ and sufficiently large $m$, any single-vector representation approximating all maximum inner products to additive error $\varepsilon$ must have dimension:

$$D \geq \frac{m^{c_\delta/\varepsilon^{2-2\delta}}}{}$$

for a constant $c_\delta > 0$, nearly closing the gap between $1/\varepsilon$ and $1/\varepsilon^2$ in the exponent of $m$ [31].

5.4 Single-Stage Hadamard Quantization

A single-stage estimator using $b$ bits per coordinate satisfies:

$$\mathbb{E}\left[|\langle y, \hat{x} - x\rangle|^2\right] \leq \left(\frac{3\pi\sqrt{3}}{2} + o(1)\right)\frac{\|y\|_2^2}{d 4^b}$$

removing the residual-stage $O(d)$-bit payload and reducing the leading constant by ~5.93× [41].

5.5 Lower Bounds for Prefix-Matrix Factorizations

For the lower-triangular all-ones matrix $Q$ with $\gamma_{2,1}(Q) = \inf_{Q=AB}\|A\|_{2\to\infty}\|B\|_{1\to1}$:

$$\gamma_{2,1}(Q) = \Omega\left(\frac{\log^{3/2} n}{(\log\log n)^{3/2}}\right)$$

matching the upper bound $O(\log^{3/2} n)$ up to a $(\log\log n)^{3/2}$ factor [39].

5.6 Case Study: Knuth's Cycles

The workflow produced a 46-page proof draft for an earlier even-case construction and a 75-page proof draft for a new simpler construction [11], demonstrating how proofs far beyond single-response length can be developed as persistent, revisable documents with explicit dependency structure.

5.7 Case Study: Erdős Unit-Distance Breakthrough

With internet access disabled, Colosseum using Gemini 3.1 Pro independently arrived at the central architecture of the OpenAI solution to Erdős's unit-distance conjecture [1], producing a 22-page draft [16] via a number-theoretic approach based on unramified towers and relative unit groups, proceeding through 15 exploration rounds with accumulated knowledge carried forward.

6. TCS-Bench Evaluation

The critique signal distinguishes correct/incorrect proofs with AUC = 0.896. Cross-model selection solves 213 problems, an improvement of 48 over the stronger individual run.

7. Codeforces Evaluation

Difficulty estimates range from 1530 to 4599 (median 2381). The performance rating $\hat{x}$ solves:

$$\sum_{i=1}^{222} \frac{1}{1 + 10^{(r_i - \hat{x})/400}} = n_{\text{solved}}$$

---

Theoretical and Practical Implications

Theoretical Contributions

1. New mathematical results: The workflow produced proofs for five open problems, including improving the $\varepsilon^{-p}$ to $\varepsilon^{-2}$ dependence in $\ell_p$ coresets and nearly closing the gap in maximum inner product embedding lower bounds.

2. Architecture for long-horizon reasoning: Colosseum formalizes research as a pipeline separating strategy from execution, with explicit dependency tracking and critique-preserving aggregation. The mathematical formulation of overlapping tree aggregation provides a principled framework for combining candidate solutions.

Practical Implications

1. Scalable research assistance: The system demonstrates that language models can contribute to research-level mathematics when organized into structured workflows, not just solve isolated problems.

2. Cross-domain transfer: The same proof-oriented architecture transfers from theorem proving to competitive programming with only an execution probe added, achieving 218/222 solutions on hard Codeforces problems.

3. Industry adoption: The workflow has been integrated into Google Antigravity's Teamwork framework as the Long Proof pattern [7], indicating practical deployability.

4. Reproducibility: Case studies with disabled internet access (unit-distance problem) demonstrate that the system can independently rediscover research results, supporting scientific validity.

---

Conclusion

Main Takeaways

Colosseum provides a model-agnostic, many-agent harness that connects strategy exploration, proof construction, and revision through shared research state, using tree-structured aggregation that preserves critiques alongside synthesized content. It achieved strong results on research-level theorem proving (71.0% on TCS-Bench), competitive programming (218/222 on Codeforces), and contributed to five new mathematical results.

Future Directions

Within-run adaptations:

1. Clustered exploration of distinct research directions to preserve minority strategies that might otherwise disappear during aggregation.
2. Local restructuring after subproblem failure—revising small neighborhoods of the dependency graph (splitting subproblems, changing adjacent section tasks, introducing intermediate sections) while maintaining acyclicity.
3. Adaptive inference allocation using signals like strategy diversity, unresolved objections, and repeated failures to expand uncertain branches or stop stabilized stages.

Across-run learning: 4. Post-training from research trajectories: Using structured records (candidate strategies, critiques, aggregation decisions, dependency graphs, revision histories) as training data, with intermediate states providing supervision for strategy selection, decomposition, and objection handling. The main challenge is credit assignment—determining which intermediate strategies were responsible for progress; the branching structure may help by comparing candidates sharing context but leading to different outcomes.