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

1 Introduction

• The pipeline separates strategy exploration, proof decomposition, subproblem solving, and global verification, with explicit dependencies and parallel work on independent subproblems.Rejected proofs can be revised or returned to exploration.Source: §1 · p. 3
• At each stage, diverse candidates are targeted for falsification and combined through overlapping tree aggregation that retains synthesized content and evidence against it.This is designed to preserve both proposals and their associated critiques during synthesis.Source: §1 · p. 3
• Colosseum contributed to several research results reported in companion papers and is illustrated through long-form proof construction and independent strategy rediscovery.The open-ended research demonstrations use Gemini 3.1 Pro.Source: §1 · p. 3
• 71.0% accuracy on TCS-Bench [15] and 218 accepted solutions on a 222-problem Codeforces suite are reported for Colosseum evaluations.The TCS-Bench result uses critique-based selection between runs with Gemini 3.1 Pro and Gemini 3.7 Flash; the Codeforces case uses implementation and execution feedback.Source: §1 · p. 3
• The workflow has been integrated into Google Antigravity’s Teamwork framework as the Long Proof pattern.Source: §1 · p. 3

2.1 Search, Critique, and Aggregation

• Search over reasoning paths and intermediate states, critique, debate, and falsification offer complementary ways to use additional inference; Colosseum retains falsification reports with proposals through later workflow stages.Source: §2.1 · pp. 3–4

2.2 Discovery Guided by Verifiers and Evaluators

• Verifier-guided systems use formal proof checking or executable tests, while Colosseum also reviews provisional strategies, intermediate claims, and natural-language proof drafts.Source: §2.2 · p. 4

2.3 Autonomous and Collective Research Workflows

• Autonomous research systems vary in their roles and shared-state designs, and differences in human involvement, disclosure, and evaluation make individual workflow contributions difficult to isolate.Source: §2.3 · pp. 4–5

2 Related Work

• Colosseum connects strategy exploration with long-proof development and repair through a readiness gate, critique-preserving aggregation, and shared drafts and research knowledge.Source: §2 · p. 3, §2.3 · p. 5

3 Colosseum Overview

• Long-horizon research combines uncertain proof routes, interdependent technical bottlenecks, long outputs with accumulating errors, and failed attempts that may still contain useful partial progress.Source: §3 · p. 5

3.1 Research Pipeline

• A readiness gate selects a sufficiently concrete strategy for decomposition into a sectioned proof skeleton and dependency graph; independent sections can proceed in parallel, while local or global failures trigger repair or renewed exploration.Unaffected subproblems need not be restarted after a local section failure.Source: §3.1 · p. 5

3.2 Inference within a Stage

• Within a difficult stage, Colosseum generates candidates, targets them for falsification, and synthesizes random subsets with their critiques through an overlapping sampling tree.The candidate type varies by stage, but the inference pattern is reused.Source: §3.2 · p. 6

3.3 Context across Stages

• The workflow carries current strategies, proof plans, section bodies, and verifier findings across stages and rounds, alongside reusable results retained in a shared knowledge directory.Source: §3.3 · p. 6

4.1.1 Parallel Candidate Generation

• Candidates are varied across mathematical choices such as representation, principal lemma, proof technique, and bottleneck, with seeds, prompts, tools, and assumed attacks providing further variation.Stage-specific schemas can make proposals comparable and expose claims for review.Source: §4.1.1 · p. 6

4.1.2 Targeted Falsification

• Reviewers target counterexamples, invalid implications, circularity, misuse of results, mismatches with the target, and missing assumptions or dependencies.Falsification records stay attached to candidates; failure to find a defect does not establish correctness.Source: §4.1.2 · pp. 6–7

4.1.3 Tree-Structured Aggregation

• Each aggregation node independently samples distinct inputs from the current population, and different groups may overlap rather than partitioning it.The reduction tree avoids comparing every candidate and critique in one prompt; aggregation contexts remain small while candidates can contribute multiple times.Source: §4.1.3 · p. 7
• Intermediate aggregation can merge compatible components, retain competing branches, repair localized flaws, or preserve unresolved conflicts and objections in the root artifact.Source: §4.1.3 · p. 7

4.2.1 Strategy Exploration and Readiness

• Parallel strategy exploration exposes each route’s requirements, conjectural steps, and technical difficulties; a readiness gate checks whether uncertainty is localized within a stable proof architecture.A route may pass with a difficult central lemma if its statement, role, and expected path to proof or verification are explicit.Source: §4.2.1 · p. 8

4.2.2 Decomposition and Parallel Proof Construction

• The decomposer maps a selected route into section-level subproblems and a dependency graph, allowing eligible independent sections to be solved in parallel.Local review checks each section against its assigned task and dependencies; retries target the affected subproblem while preserving completed work elsewhere.Source: §4.2.2 · p. 8

4.2.3 Global Verification and Feedback

• Multiple global reviews assess the assembled proof, aggregate distinct objections, and localize defects; a fatal concrete defect rejects the proof rather than being outvoted.The system revises a still-viable strategy, but returns to exploration when verifier findings undermine it.Source: §4.2.3 · pp. 8–9

4.3 Shared Research Knowledge

• Across research rounds, the latest proof attempt remains in full while a shared knowledge directory preserves reusable findings from the wider search.The draft grounds the next round in the argument actually attempted; the directory retains useful results that candidate aggregation might otherwise discard.Source: §4.3 · p. 9

4.3.1 Retaining Prior Attempts

• When a round lacks an accepted proof, its draft and verifier feedback enter the next round, supporting targeted revision or reconsideration of the strategy.Retaining a draft does not endorse its claims; attached feedback identifies steps or assumptions that still require work.Source: §4.3.1 · p. 9

4.3.2 Knowledge Directory

• The knowledge directory records theorems and lemmas, failed approaches, references, and observations, retaining each entry’s source and relevant caveats.It is updated across rounds and made available to later agents to reuse results and avoid repeating approaches whose failure is known.Source: §4.3.2 · p. 9

• Open-problem strategy exploration uses a range of tree configurations, some with slightly over 100 leaf nodes; remaining stages use 16 leaf nodes.The 16-leaf configuration is shared across those remaining stages.Source: §4.4 · pp. 9–10
• Table 1 summarizes strategy-exploration configurations for open-problem research, TCS-Bench, and Codeforces, alongside the shared configuration for other stages.At level ℓ, the table caption defines effective sample size as min{k, mℓ}.Source: §4.4 · p. 10, Table 1 · p. 10
• The configurations specify population widths and aggregation fan-in, not exact total model calls, which also depend on proof sections, local retries, and global revision rounds.Source: §4.4 · p. 10

5.1 Strong Coresets for ℓp Subspace Approximation When p > 2

• The same ridge-leverage-score sampling rule supports coreset size eOp(kp/2ε−2) with eOp(nnz(A) + dω) running time, improving the prior ε−p dependence.The analysis retains truncation in the sampling probabilities, changing the recurrence’s fixed point from ε−p to ε−2.Source: §5.1 · p. 10

5.2 The Condition-Number Barrier in Sparse Least Squares

• Under the randomized exact-volume Small-Set Expansion Hypothesis, no randomized polynomial-time algorithm achieves the stated least-squares guarantee; thus no fixed sublinear power of the condition number replaces linear dependence [9].The result is conditional and applies to least-squares objectives.Source: §5.2 · pp. 10–11

5.3 Dimension Lower Bounds for Maximum Inner Product Embeddings

• The new lower bound nearly closes the gap between the 1/ε and 1/ε2 exponents of m for single-vector representations, even for data-dependent representations, and extends to Chamfer similarity [30].Source: §5.3 · p. 11

5.4 Single-Stage Hadamard Quantization

• Pairwise-independent dithers across Hadamard coordinates yield an unbiased single-stage estimator with the same 1/(d4b) mean-squared-error scaling, removing an O(d)-bit residual-stage payload.The proved upper-bound leading constant is reduced by approximately a factor of 5.93.Source: §5.4 · p. 11

5.5 Lower Bounds for Prefix-Matrix Factorizations

• The prefix-matrix factorization lower bound is log3/2 n (log log n)3/2, within a factor of (log log n)3/2 of the dyadic upper bound O(log3/2 n).The proof combines right-sided Haar projections with a scale-dependent numerical-sparsity decomposition and aggregates estimates across dyadic scales.Source: §5.5 · p. 12

5.6 Case Study: Long-Form Proof Construction for Knuth’s Cycles

• For Knuth’s cycles problem, Colosseum produced 46-page and 75-page proof drafts for two even-case constructions, illustrating a persistent, revisable proof organized around explicit dependencies.The earlier construction had a complete proof; the newer construction was computationally verified through m ≤2000, while a rigorous arbitrary-even-m proof remained open.Source: §5.6 · p. 12

5.6 Case Study: Independent Rediscovery of the Erdős Unit-Distance Breakthrough

• With internet access disabled, a 15-round Colosseum run independently developed a number-theoretic approach to the Erdős unit-distance problem and arrived at the central architecture of the OpenAI solution [1].Its 22-page draft pursued u(n) ≥n1+ε0 for infinitely many n, with ε0 > 0 given explicitly.Source: §5.6 · p. 13

6 Research-Level Evaluation on TCS-Bench

• The benchmark contains 300 tasks from FOCS, STOC, and SODA papers published between 2020 and 2026, requiring self-contained proofs of target theorems.A reference-assisted grader, optimized on a separate set of 100 expert-labeled proofs, reported more than 90% accuracy; all benchmark accuracies use this grader.Source: §6 · p. 13
• Eight Gemini 3.7 Flash critiques assessed each Gemini 3.1 Pro proof; the system submitted it if at least five judged it correct, otherwise submitting the Flash proof.The benchmark grader scored selected proofs but did not participate in the selection rule.Source: §6 · p. 13
• 213 problems solved—48 more than the stronger individual run—made cross-model selection the highest-accuracy evaluated non-oracle method on TCS-Bench.The critique signal distinguished grader-labeled correct and incorrect proofs with an AUC of 0.896; Gemini 3.1 Pro’s internal verifier alone yielded 64.7% accuracy.Source: Table 2 · p. 13, §6 · p. 14

Evaluation Setup

• The evaluation uses 222 problems with corpus difficulty estimates above 1500, drawn from contests held between April and October 2025; those estimates have a median of 2381 and range from 1530 to 4599.Solutions are compiled and checked against the complete hidden test set using each problem’s original checker; every test must pass.Source: §7 · p. 14, Table 3 · p. 14

Rating Calculation

• The reported corpus-level performance rating is explicitly defined from evaluation-corpus difficulty estimates rather than treated as an official Codeforces contestant rating.The paper describes a solve-probability function and defines the rating as the unique solution to an equation over the corpus’s difficulty estimates.Source: §7 · p. 14

Case Study Motivation

• The case study tests whether proof-oriented exploration and decomposition transfer to executable programming without replacing them with a code-specific controller.Prior competitive-programming systems include candidate-population filtering and iterative execution-based feedback.Source: §7 · p. 14

Architecture Transfer

• Colosseum retains its proof-oriented architecture: exploration selects a strategy, then a dependency-graph decomposer breaks it into mathematical and algorithmic subproblems ending in one C++ implementation.Table 4 gives an example decomposition for Codeforces 2084F.Source: §7 · p. 15, Table 4 · p. 15

Execution Feedback

• A C++ execution probe compiles and runs candidate implementations on public samples and model-generated stress inputs, returning checker outcomes and time and memory measurements to verification and revision.Hidden tests remain inaccessible to the workflow and are used only for final grading.Source: §7 · p. 15

Results

• 218 accepted solutions and a corpus-level performance rating of 4263 were recorded with execution feedback, versus 213 accepted solutions and 3918 without it.The comparison covers the same 222-problem suite.Source: Table 5 · p. 15, §7 · p. 15

8 Conclusion and Future Directions

• Colosseum connects exploration, proof construction, and revision through shared research state, while tree aggregation combines candidates with their critiques.The harness contributed to new research results and performed strongly on TCS-Bench and in competitive programming.Source: §8 · p. 15

8.1 Adapting the Inference-Time Workflow

• Clustering strategies by mechanism, reduction, or representation could preserve less common directions for later comparison and integration.Preliminary, non-systematic runs suggest this organization can preserve productive minority directions, but more systematic work is needed to determine how to form and update clusters, allocate inference, and merge directions.Source: §8.1 · p. 16
• A local restructuring step could revise a small dependency-graph neighborhood after repeated failure, without regenerating completed sections outside it.Possible changes include splitting a subproblem, changing adjacent tasks, adding an intermediate section, or redirecting local dependency edges.Source: §8.1 · p. 16
• A future controller could allocate inference using workflow signals to expand uncertain branches, retry unstable sections, and stop stabilized stages.Compute-matched evaluation would be needed to distinguish improved allocation from simply using more inference.Source: §8.1 · p. 16

8.2 Learning from Research Trajectories

• Externally validated research trajectories could train the base model, but credit assignment must identify which intermediate steps contributed to progress.The recorded trajectories include strategies, critiques, aggregation decisions, dependency graphs, drafts, and revision histories.Source: §8.2 · pp. 16–17, §8 · p. 16

A Selected Prompt Templates and Information Flow

• The prompt templates show what each stage does, receives, and passes onward, while omitting repeated instructions and implementation details.Items in braces are filled in at runtime.Source: A Selected Prompt Templates and… · p. 22

A.1 Strategy Exploration

• Strategy exploration produces a concrete strategy card with primary and backup routes, evidence, risky lemmas, active obligations, and a readiness assessment.A route is ready for decomposition only when no unresolved fatal obligation remains.Source: §A.1 · p. 22
• Paired falsifiers attack proposed routes, while the readiness gate checks fatal bridges and classifies whether to decompose, explore further, or reject.A strategy with a fatal unresolved bridge may proceed only with a stable architecture and explicit proof or verification paths for remaining minor obligations.Source: §A.1 · pp. 23–24

A.2 Decomposition into Subproblems

• Decomposition converts an approved strategy into a LaTeX skeleton and dependency DAG, with earlier dependencies listed for each subproblem.Unresolved bridge lemmas and certificate obligations remain explicit in the plan.Source: §A.2 · pp. 24–25

A.3 Subproblem Solving and Aggregation

• For each subproblem, solvers and falsifiers produce paired candidate sections; aggregation retains useful progress and unresolved objections across retries.Sections identify their result, bridge claims, remaining obligations, and completion status; computational evidence counts only when a code probe is executed.Source: §A.3 · pp. 25–26
• Falsifiers reject sections that prove the wrong target or rely on false or constraint-dropping bridges, and classify surviving work as ready, conditional, or rejected.Conditional sections retain explicit unresolved bridges or obligations.Source: §A.3 · pp. 25–26

A.4 Global Verification and Revision

• The global verifier checks the assembled proof against the original problem, then localizes defects for targeted outline or section revision and renewed verification.Revisions preserve correct material and explicitly mark any remaining gap.Source: §A.4 · pp. 26–27