arxiv-2609-15983 SRC-0295 · paper

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

Created: 2026-09-14 · Ingested: 2026-09-19

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 a

Referenced by

Claims in this catalog that draw on this source, and whether as support or counterpoint.

supportsOn research-level theorem-proving tasks drawn from recent FOCS/STOC/SODA papers, wrapping a frontier model in a staged harness that explores strategies, gates when to decompose, solves section-level subproblems along a dependency graph, and routes verifier findings back to the affected section raises graded proof accuracy far above prompting the same model directly (30.3% to 54.0% for Gemini 3.1 Pro on TCS-Bench), and two such runs with different backbones make complementary errors, so selecting between them by sampled critiques reaches 71.0% against an oracle ceiling of 77.3%.