*English translation of a Chinese forum post on zhichai.net discussing arXiv:2609.15983.*

Stellar Colosseum: When a Hundred AIs Do Mathematical Research in an Arena

Paper: *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 & CMU) arXiv: 2609.15983

Why "doing research" is much harder than "answering questions"

Asking an AI to prove a research-level theorem — say, one from a FOCS paper — requires more than answering a problem. A human mathematician first explores (what known results and techniques apply?), then decomposes (which lemmas are needed, and what are their dependencies?), then attacks each piece, checks consistency, and finally reads the whole proof end to end.

For AI, each step is hard:

• Strategic uncertainty: no intuition about which direction will work.
• Distributed technical difficulty: multiple bottlenecks with complex, web-like dependencies.
• Long outputs and error accumulation: research proofs run dozens of pages; keeping notation and assumptions consistent is difficult.
• Failure and partial progress: a failed attempt may still yield a useful counterexample, a restricted true statement, or a graftable lemma.

Colosseum answers these with adversarial reasoning workflows, tree-based aggregation, and shared knowledge across rounds.

Architecture: two layers

Layer 1: The research workflow

1. Strategy Exploration — multiple candidate research strategies are generated in parallel, each stating its core mechanism, required lemmas, expected bottlenecks, and a verifiable test. 2. Readiness Gate — a decision point: is some route concrete enough to start proof construction (stable core structure, precisely stated unresolved claims)? If not, keep exploring. 3. Decomposition & Parallel Construction — the chosen strategy becomes a numbered proof skeleton whose sections form a DAG. Independent sections are solved in parallel, each solver receiving completed sections as context. Once a section passes local review, it is committed; if review finds problems, only that section is re-solved. 4. Global Verification — independent reviewers read the full argument, checking cross-section consistency, notation drift, and dependency usage. Defects are localized to specific sections, making repairs local rather than restarting from scratch.

Layer 2: Adversarial reasoning within each stage

• Parallel candidate generation with diverse representations, main lemmas, techniques, seeds, temperatures, and prompt perspectives.
• Targeted falsification: adversarial reviewers hunt for counterexamples, invalid inferences, circular reasoning, misused theorems, and missing assumptions. Falsification records stay attached to candidates.
• Tree aggregation: with, e.g., 128 candidates, overlapping random sampling combines 5 candidates per node (each candidate participates ~2.5 times on average) into 64 nodes, then recursively upward. Intermediate aggregations are constructive — merging compatible parts, keeping competing branches, fixing local defects. Crucially, objections are not averaged away: a specific fatal flaw vetoes a candidate, while generic acceptances cannot dissolve it.

Cross-round shared memory

• Full preservation of previous attempts: rejected proof drafts and reviewer feedback carry into the next round.
• Knowledge Directory: a knowledge curator organizes reusable material into four categories — theorems/lemmas (with assumptions and applications), failed approaches (with exact failure points), references, and observations with evidence.

Real results, not just benchmarks

• Strong coresets: for l_p subspace approximation (p > 2), Colosseum improved the coreset size under the same sampling rule from O(k^{p/2} ε^{-p}) to O(k^{p/2} ε^{-2}), by preserving the truncation term in sampling probabilities when bounding surviving rows.
• Sparse least squares: helped establish a conditional lower bound — under a randomized exact-volume small-set expansion assumption, no fixed sublinear power of the condition number can replace the linear dependence on κ in output sparsity.
• Maximum inner product embeddings: new dimension lower bound m^{c_δ/ε^{2-2δ}} for single-vector representations under Chamfer similarity, nearly closing the gap between 1/ε and 1/ε² exponents.
• Knuth's cyclic problem: produced a 46-page proof draft for the even case and a 75-page draft for a subsequent construction — far beyond a single model output.
• Erdős unit distance problem: offline (no internet), using Gemini 3.1 Pro, Colosseum independently rediscovered the core architecture of a counterexample construction (based on divergence towers and relative unit groups) over 15 rounds, yielding a 22-page research draft.

Benchmark results

• TCS-Bench (300 theorem-proving tasks distilled from 2020–2026 FOCS/STOC/SODA papers): 71.0% accuracy using Gemini 3.1 Pro and Gemini 3.7 Flash with a critic-based selection between two runs.
• Codeforces: 218 of 222 problems solved with the proof-oriented pipeline plus execution feedback on Gemini 3.1 Pro.

Why it works

1. Diversity beats raw strength: many varied candidates give adversarial verification something to work with. 2. Failure is valuable: structured failure records turn "wasted" compute into assets. 3. Global view plus local repair: DAG decomposition allows fixing defects without restarting the proof. 4. Adversarial verification beats consensus: voting hides shared blind spots; a concrete counterexample outweighs a hundred "looks right" judgments.

Limitations

• No correctness guarantee: outputs are natural-language proof drafts without formal verification; best used as a human collaborator, not an independent researcher.
• Resource cost: full pipelines with 128-leaf tree aggregation and multi-round verification require many API calls.
• Dependence on base models: orchestration cannot compensate if the underlying model lacks intuition in a domain.
• No human feedback loop: a mathematician's one-line guidance can be worth more than dozens of automated exploration rounds.

Closing thoughts

Colosseum suggests a new shape for AI research: not a single model toiling alone, but an organized team — explorers marking unknown territory, skeptics scrutinizing every gap, synthesizers distilling reliable conclusions, and memory keepers preventing repeated dead ends. The goal is not to replace mathematicians, but to give them a tireless research team so that creativity and intuition can be spent on the most promising directions.

References

1. Lin, H., Woodruff, D. P., Deng, Y., Mao, J., Zuo, S., & Mirrokni, V. (2026). Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science. *arXiv:2609.15983*.