Organizations: Department of Computer Science, The University of Texas at Austin · Amazon · Department of Statistics and Data Science, The Wharton School, University of Pennsylvania
Large language models perform strongly on competition mathematics, but their research-level reasoning remains difficult to evaluate systematically. Theoretical computer science (TCS) connects algorithm design to explicit guarantees and fundamental limits, providing a setting for evaluating whether models can justify computational improvements with arguments humans can inspect. We introduce TCSAlgBench, a benchmark and reusable pipeline for natural-language proof discovery, comprising 398 theorem-level challenges from 138 STOC and COLT 2026 papers. Expert-designed rules complete paper-specific context, preserve computational assumptions and quantitative guarantees, and withhold constructions when discovering an algorithm is part of the task. For each task, prover systems receive theorem statements and access to cited prior work. The pipeline supports fresh, versioned challenge batches from newly released papers. We evaluate ten model configurations from four families under direct inference and prover-verifier discussion, and compare four agent workflows under matched model-call opportunities. All evaluations use the full benchmark. In the model comparison, GPT-5.6 Sol max achieves the highest five-run verifier-accepted coverage at 23.6% after 10-round discussion. Discussion and repeated sampling improve coverage. In the separate agent comparison using GPT-5.5 xhigh, decomposition improves coverage over discussion, and agentic planning achieves the highest five-run verifier-accepted coverage at 25.4%. TCSAlgBench provides a refreshable testbed for measuring progress in model reasoning and studying how agent workflows support research-level proof discovery.
Figures & tables
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
Topic
Retained
Total
Algorithmic fairness
17
30
Differential privacy
11
33
Learning theory
61
101
Optimization
25
52
Sampling
22
38
Other
85
144
Appendix
Table 1: Candidate Lean-statement retention by topic after compilation and automated semantic filtering. The rows follow the topic order used in Table 4 . Retention is a construction diagnostic, not expert-validated formalization accuracy.
Benchmark
Metric
GPT-5.5 xhigh
Opus 4.8 max
AIME 2026
Final-answer accuracy
100.00
100.00
HMMT February 2026
Final-answer accuracy
98.48
95.45
Apex
Final-answer accuracy
80.21
81.25
Apex Shortlist
Final-answer accuracy
98.40
90.43
ArXivMath June 2026
Final-answer accuracy
83.63
69.97
TCSAlgBench
Five-run proof coverage
18.1
4.5
Appendix
Table 2: Published MathArena results and TCSAlgBench five-run coverage with 10-round discussion, in percent. Metrics and evaluation protocols differ.
Configuration
Seed 1 acceptance
10-run coverage
Avg. input tokens
Avg. output tokens
GPT-5.6 Sol max
23 (5.8%)
55 (13.8%)
17K
19K
GPT-5.6 Sol xhigh
19 (4.8%)
43 (10.8%)
17K
16K
GPT-5.6 Sol high
19 (4.8%)
41 (10.3%)
16K
10K
GPT-5.5 xhigh
13 (3.3%)
28 (7.0%)
15K
17K
GPT-5.5 high
8 (2.0%)
21 (5.3%)
16K
16K
Opus 4.8 max
3 (0.8%)
7 (1.8%)
20K
9K
Appendix
Table 3: Direct-inference results for Figure 5 (a) on all 398 challenges, using three-voter majority voting. Entries are accepted-challenge counts, with percentages in parentheses. Seed 1 reports one run; 10-run coverage counts challenges accepted in any of ten independently seeded runs. Input and output tokens are averaged per prover call; K denotes thousands.
Configuration
AF (30)
DP (33)
LT (101)
Opt. (52)
Samp. (38)
Other (144)
All (398)
Panel A: First run (seed 1; N=398 )
Opus 4.8 high
3
0
2
1
1
1
8
Opus 4.8 xhigh
4
0
2
1
2
1
10
Opus 4.8 max
3
0
2
1
2
1
9
GPT-5.5 high
9
1
9
3
6
14
42
GPT-5.5 xhigh
8
1
12
5
6
13
45
Appendix
Table 4: Verifier-accepted proofs by topic on all 398 TCSAlgBench challenges after 10-round discussion. Panel A reports seed 1, and Panel B reports five-run coverage. AF denotes algorithmic fairness; DP, LT, Opt., and Samp. abbreviate differential privacy, learning theory, optimization, and sampling, respectively. Parenthesized column-header values give category totals.
Configuration
Three-voter majority
Opus 4.8 verifier
Δ
Opus 4.8 high
14
14
0
Opus 4.8 xhigh
15
16
+1
Opus 4.8 max
18
18
0
GPT-5.5 high
66
60
-6
GPT-5.5 xhigh
72
68
-4
GPT-5.6 Sol high
79
77
-2
Appendix
Table 5: Five-run coverage for the eight model configurations evaluated under both the primary three-voter majority rule and an alternative Opus 4.8 verifier, using the same generated proofs. Δ is Opus-verifier coverage minus majority-vote coverage.
Models
Cutoff
Pre-cutoff
Post-cutoff
All
Panel A: First run (seed 1; N=398 )
Opus 4.8 high
2026-01-01
3/201 (1.5%)
5/197 (2.5%)
8/398 (2.0%)
Opus 4.8 xhigh
2026-01-01
3/201 (1.5%)
7/197 (3.6%)
10/398 (2.5%)
Opus 4.8 max
2026-01-01
2/201 (1.0%)
7/197 (3.6%)
9/398 (2.3%)
GPT-5.5 high
2025-12-01
19/188 (10.1%)
23/210 (11.0%)
42/398 (10.6%)
GPT-5.5 xhigh
2025-12-01
24/188 (12.8%)
21/210 (10.0%)
45/398 (11.3%)
Appendix
Table 6: Verifier-accepted proofs before and after the assumed model-family knowledge cutoff on all 398 challenges. Panel A reports seed 1, and Panel B reports five-run coverage. Percentages use the corresponding pre- or post-cutoff column total; percentages in the All column use all 398 challenges.
Panel A: Opus 4.8 and GPT-5.5
Opus 4.8: xhigh vs. max
GPT-5.5: high vs. xhigh
Overlap
xhigh only
max only
Overlap
high only
xhigh only
Before cutoff
5
1
2
29
2
9
After cutoff
9
0
2
31
4
3
Total
14
1
4
60
6
12
Panel B: GPT-5.6 Sol and Fable 5
Appendix
Table 7: Complementarity of five-run verifier-accepted coverage on all 398 challenges, partitioned by the model-family knowledge cutoff. Overlap counts challenges accepted under both effort settings, while the setting-only columns count challenges accepted uniquely under one setting. For Fable 5, the high/xhigh union contains 32 challenges before the cutoff, 37 after it, and 69 overall.
Workflow
Seed 1
Five-run coverage
Avg. input tokens
Avg. output tokens
Decomposition with MCTS search
77 (19.3%)
96 (24.1%)
27.4M
3.9M
Discussion, no decomposition
60 (15.1%)
84 (21.1%)
12.1M
1.0M
Discussion, root-only decomposition
73 (18.3%)
93 (23.4%)
25.6M
3.9M
Discussion, agentic planning
72 (18.1%)
101 (25.4%)
60.4M
9.0M
Appendix
Table 8: Call-matched agent-design comparison using GPT-5.5 xhigh and the same external verifier; Appendix C details the budgets. Acceptance counts use all 398 challenges, with rates in parentheses. Seed 1 reports one run; five-run coverage counts challenges accepted in any of five independently seeded runs. Tokens are averaged per challenge–seed run over 10 randomly selected challenges and five independent seeds; M denotes millions.
Model configuration
Acceptance (%) ↑
RMS-CE (%) ↓
GPT-5.6 Sol max
18.1
10.8
GPT-5.6 Sol xhigh
15.6
4.3
GPT-5.6 Sol high
12.1
11.7
GPT-5.5 xhigh
10.8
19.1
GPT-5.5 high
10.1
17.3
Claude Opus 4.8 xhigh
2.3
2.0
Appendix
Table 9: Verifier acceptance and RMS calibration error (RMS-CE), in percent, on all 398 challenges. These runs are separate from the main model comparison. Both metrics use the same proof outputs, with confidence elicited during proof generation before external verification.