cs.AINov 5, 2026
SaveTCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research
Organizations: Tsinghua University · Moonshot AI · Shanghai Qizhi Institute
Abstract
Can large language models (LLMs) advance theoretical computer science and resolve its long-standing open conjectures? To study progress toward this goal, we introduce TCSExam, a unified framework and benchmark covering the full range of TCS research. It evaluates theorem proving, solver engineering, and constructions alongside direct attempts to resolve open conjectures, capturing both concrete research accomplishments and progress toward long-standing research goals. TCSExam-Full contains 100 expert-reviewed tasks, with submissions checked by the Lean kernel or an executable task checker. TCSExam-Lite selects 20 tasks, five per track, reducing the number of task attempts by 80% at the same per-attempt budget. We evaluate eight agents on Full and nine on Lite. The TCSExam Index combines all four tracks: GPT-6 Astra leads Full (71.9), and Opus 5.5 leads Lite (72.3). Full and Lite rankings are strongly aligned across eight shared agents (Spearman's ), supporting Lite as a compact, discriminative benchmark. The evaluations yield improved solver outputs and mathematical constructions, together with independently verified special cases and bounds from open-conjecture attempts. TCSExam provides an extensible framework with task sources, Docker build recipes, and evaluation tools for reproducible use.
Figures & tables
Figure 1: TCSExam covers the full range of TCS research through four evaluation tracks. Arrows show how proving, searching, and constructing can contribute to one another and to resolving open conjectures. The examples illustrate tasks within each track; research areas can span multiple tracks.
| Benchmark / track | # Tasks | Theorem proving | Solver engineering | Constructions | Open conjectures |
|---|---|---|---|---|---|
| TCS-BENCH | 300 | ✓ | ✗ | ✗ | ✗ |
| FormalTCS | 143 | ✓ | ✗ | ✗ | ✗ |
| FrontierCS | 240 | ✗ | ✓ | ✓ | ✗ |
| FrontierCS 2 | 48 | ✗ | ✗ | ✗ | |
| EdgeBench-Formal | 13 | ✓ | ✗ | ✗ | |
| EdgeBench-Optimization | 19 | ✗ | ✓ | ✗ |
Table 1: Coverage of selected benchmarks.
Figure 2: Task curation and validation. Expert selection is followed by agent-assisted authoring and review, executable checks, and trial evaluation. Statement mismatches, scorer errors, and unexpected results prompt revision and re-testing. Tasks are included after expert approval; exceptional results trigger verification and source re-checks.
| Agent | Theorem proving Success (%) | Solver Relative (%) | Constructions Task score (%) | Open conjectures Resolved (%) | Index Points |
|---|---|---|---|---|---|
| GPT-6 Astra | 70.0 | 64.7 | 104.9 | 0.0 | 71.9 |
| Kimi K3.1 Pro | 38.3 | 54.1 | 98.6 | 1.1 | 57.4 |
| Kimi K3 | 11.7 | 48.7 | 95.5 | 0.0 | 46.8 |
| DeepSeek V4.1 Flash 1017 | 6.7 | 53.1 | 91.8 | 5.6 | 46.0 |
| GLM-5.3 | 5.0 | 49.1 | 97.7 | 0.0 | 45.5 |
| Qwen3.8 Max (0902) | 5.0 | 49.2 | 95.1 | 0.0 | 44.8 |
Table 2: TCSExam-Full results on 100 tasks. Tasks receive equal weight within each track. Solver uses the Kimi K3-relative metric; construction scores of 100.0% match the task reference. Index is defined in Section 3.3 . Accepted conjecture submissions adapt OpenAI's published counterexamples and proofs (Section 5.6 ).
Figure 3: Full task-level results for eight agents. Rows are tasks; columns are agents. (a) Complete-proof success rates. (b) Kimi K3-relative Solver means; dots mark task-best means, including ties. (c) Cells stack one to three construction attempts vertically, colored below, at, or above the 100.0% task reference (relative tolerance ). Scores appear in Appendix E .
| Agent | Theorem proving Success (%) | Solver Relative (%) | Constructions Task score (%) | Open conjectures Resolved (%) | Index Points |
|---|---|---|---|---|---|
| Opus 5.5 | 80.0 | 60.5 | 100.4 | 0.0 | 72.3 |
| GPT-6 Astra | 60.0 | 63.0 | 100.4 | 0.0 | 67.0 |
| Kimi K3.1 Pro | 40.0 | 50.0 | 88.3 | 0.0 | 53.5 |
| Kimi K3 | 33.3 | 48.9 | 79.8 | 0.0 | 48.6 |
| GLM-5.3 | 20.0 | 46.1 | 90.7 | 0.0 | 47.0 |
| Qwen3.8 Max (0902) | 20.0 | 51.0 | 80.3 | 0.0 | 45.4 |
Table 3: TCSExam-Lite results on 20 tasks, with five per track. Tasks receive equal weight within each track. Solver uses the Kimi K3-relative metric; construction scores of 100.0% match the task reference. Index is defined in Section 3.3 .
Figure 4: Full and Lite rankings are strongly aligned. Among the eight shared agents, both suites give the same top three and agree on 26 of 28 pairs ( ). Agents are ordered by Full Index.
Figure 5: Two constructions submitted by Kimi K3. (a) All 124 vertices and 630 edges of a graph with no 3- or 4-cycles, exceeding the 629-edge task reference. Green highlights a shortest cycle. (b) The 18 stabilizer generators of a quantum code, improving the reference distance from 5 to 6. Each row specifies an operator on 25 qubits; white cells denote the identity . Both panels are drawn directly from submitted certificates.
Figure 6: Astra’s proof certificate for the nine-dimensional Alon–Jaeger–Tarsi case over . (a) Coordinate pairs fall into seven classes; numbered cells give the unique nonzero with . Class counts sum to nine and yield pair constraints. (b) The actual certificate has nonnegative coefficients on two arrays of weight counts and four pair terms. Combined with the counting identities, it forces a nonnegative sum to equal after positive rescaling, excluding a minimal counterexample. Colored cells mark positive coefficients; pale cells mark zeros.
Appendix figures & tables34 assets
Supplementary material from the paper’s appendix.
Appendix
| Theorem | Source paper | Steps | Domain |
|---|---|---|---|
| corners-quasipoly | Quasipolynomial Bounds for the Corners Theorem ( Jaber et al., 2025 ) | 8 | additive combinatorics |
| dijkstra-universal | Universal Optimality of Dijkstra via Beyond-Worst-Case Heaps ( Haeupler et al., 2024 ) | 8 | algorithms |
| discrepancy-beyond-banaszczyk | Decoupling via Affine Spectral-Independence: Beck-Fiala and Komlós Bounds Beyond Banaszczyk ( Bansal & Jiang, 2025 ) | 7 | discrepancy theory |
| discrete-bidding-games | Mean-Payoff and Energy Discrete-Bidding Games ( Avni & Sadhukhan, 2026 ) | 8 | games |
| folded-rs-gsb | Explicit Folded Reed-Solomon and Multiplicity Codes Achieve Relaxed Generalized Singleton Bounds ( Chen & Zhang, 2025 ) | 8 | coding theory |
| gg26-proximity | Optimal Proximity Gaps for Subspace-Design Codes and (Random) Reed-Solomon Codes ( Goyal & Guruswami, 2025 ) | 6 | coding theory |
| Task | Problem | Source | Objective |
|---|---|---|---|
| ahc058-atcoder | Hierarchical production planning | AtCoder Heuristic Contest 058: Apple Incremental Game | maximize |
| bpp-bpplib | One-dimensional bin packing | BPPLIB | minimize |
| ce-pace2021 | Cluster editing | PACE 2021 (heuristic track) | minimize |
| celar-rlfap | Radio link frequency assignment (RLFAP) | CALMA/CELAR benchmarks (ZIB archive; MiniZinc Challenge) | minimize |
| christmas-tree-ahc041 | Christmas-tree forest partitioning | AtCoder Heuristic Contest 041: Christmas Tree Cutting | maximize |
| coloring-dimacs | Graph coloring | DIMACS / COLOR02 benchmark (+ gc_instances) | minimize |
| Task | Construction | Reference in source snapshot | Domain |
|---|---|---|---|
| ramsey-r55 | R(5,5) lower-bound construction | N = 42 (R(5,5) in [43, 46]) ( Exoo, 1989b ) | Ramsey theory |
| ramsey-r46 | R(4,6) lower-bound construction | N = 35 (R(4,6) in [36, 40]) ( Exoo, 2012 ) | Ramsey theory |
| ramsey-r3-10 | R(3,10) lower-bound construction | N = 39 (R(3,10) in [40, 41]) ( Exoo, 1989a ) | Ramsey theory |
| vdw-w27 | van der Waerden number W(2,7) lower bound | n = 3703 ( Rabung & Lotts, 2012 ) | Ramsey theory |
| capset-d7 | Maximum cap set in dimension 7 | 236 points (upper bound 288; earlier bound 291) ( Calderbank & Fishburn, 1994 ; Thackeray, 2022 ; Versluis, 2017 ) | additive combinatorics |
| covering-code-k10 | Binary covering code K(10,1) (minimize codewords) | 120 codewords (K(10,1) in [107, 120]) ( Östergård, 1991 ) | coding theory |
| Task | Conjecture | Source | Domain |
|---|---|---|---|
| aaronson-ambainis | Aaronson-Ambainis conjecture | ( Aaronson & Ambainis, 2014 ) | quantum computing |
| alon-jaeger-tarsi | Alon-Jaeger-Tarsi conjecture (prime-field form) | ( Nagy & Pach, 2025 ) | combinatorics |
| bin-packing-mirup | MIRUP conjecture (modified integer round-up property, 1-D bin packing) | ( Scheithauer & Terno, 1995 ) | integer programming |
| caccetta-haggkvist | Caccetta-Häggkvist conjecture | ( Caccetta & Häggkvist, 1978 ) | graph theory |
| d-vs-r-total-functions | D(f) C·R(f)ˆ2 for all total Boolean functions | ( Nisan, 1991 ) | query complexity |
| evasiveness-graph-properties | Evasiveness conjecture (Karp’s conjecture) | ( Rosenberg, 1973 ) | query complexity |
| Check | Evidence | Failure addressed |
|---|---|---|
| Source correspondence | Source location, formal statement, reconciliation | Omitted assumptions or changed quantifiers |
| Definition behavior | Hand-checkable examples and executed checks | Degenerate or incorrectly encoded objects |
| Submission integrity | Fixed-region and proof-dependency checks | Changing the task or assuming the result |
| Checker behavior | Valid, invalid, and empty test outputs | Accepting an invalid answer or rejecting the documented interface |
| Version consistency | Versioned statements, environments, and scoring rules | Mixing incompatible statements or score definitions |
Table 8: Task-validation checks and the evidence used to assess each failure mode.
| Model | Harness | Effort | Full | Lite |
|---|---|---|---|---|
| GPT-6 Astra | Codex 0.154.0 | max | 1 | 1 |
| Kimi K3.1 Pro | Kimi Code 0.43.0 | max | 3 | 3 |
| Kimi K3 | Kimi Code 0.43.0 | max | 3 | 3 |
| GLM-5.3 | Claude Code 2.1.257 | max | 1 | 1 |
| Qwen3.8 Max (0902) | Claude Code 2.1.257 | max | 1 | 1 |
| Grok 4.6 | Grok Build 1.0.41 | xhigh | 1 | 1 |
Table 9: Model and harness configurations. Counts are attempts per task in each suite.
| Task | Source | Public | Hidden | Budget |
|---|---|---|---|---|
| AtCoder AHC058 | Competition | 105 | 45 | Each 2 |
| Bin packing | Library | 90 | 39 | Pool 1,170 |
| Cluster editing | Competition | 100 | 100 | Each 600 |
| Frequency assignment | Library | 13 | 8 | Each 1,200 |
| AtCoder AHC041 | Competition | 105 | 45 | Each 2 |
| Graph coloring | Library | 132 | 72 | Each 180 |
Table 10: Solver instance sets and final execution budgets. Budgets are in seconds: Each is a per-instance limit; Pool is the total for the final set.
Table 11: Token usage and duration per attempt in the Full main evaluation. Means use recorded values; gives attempts with measurements over total attempts. M and k denote millions and thousands of tokens.
| Task | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|
| 1. Corners theorem | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| 2. Small-depth negations | 1/1 | 3/3 | 3/3 | 0/1 | 1/1 | 0/1 | 0/3 | 0/3 |
| 3. Universal Dijkstra | 1/1 | 2/3 | 2/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| 4. Three taxis | 1/1 | 2/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| 5. Monotonicity testing | 1/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| 6. QMA–QCMA separation | 1/1 | 3/3 | 0/3 | 0/1 | 0/1 | 0/1 | 1/3 | 0/3 |
Table 12: Theorem-proving results on TCSExam-Full. Entries give complete proofs / attempts.
| Task | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|
| Production planning | 83.8 | 73.0 | 50.1 | 48.3 | 52.4 | 45.4 | 47.9 | 67.3 |
| Bin packing | 56.1 | 50.4 | 50.0 | 48.4 | 44.2 | 44.5 | 50.3 | 48.4 |
| Cluster editing | 50.3 | 50.0 | 50.0 | 50.2 | 50.0 | 49.1 | 50.2 | 50.1 |
| Frequency assignment | 53.8 | 51.2 | 50.2 | 52.5 | 53.8 | 53.8 | 53.4 | 50.6 |
| Tree partitioning | 85.4 | 60.0 | 50.0 | 54.1 | 69.5 | 23.2 | 66.8 | 19.0 |
| Graph coloring | 54.9 | 50.4 | 50.1 | 52.6 | 49.0 | 50.2 | 52.5 | 51.5 |
Table 13: Solver results on TCSExam-Full. Entries are mean Kimi K3-relative scores (%).
| Task | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|
| Ramsey R(5,5) | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 0.0 | 100.0 | 100.0 |
| Ramsey R(4,6) | 100.0 | 66.7 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 |
| Ramsey R(3,10) | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 66.7 |
| Van der Waerden W(2,7) | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 66.7 |
| Cap sets (dimension 7) | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 |
| Covering codes | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 |
Table 14: Construction results on TCSExam-Full. Entries are mean task scores (%).
| Task | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|
| Aaronson–Ambainis | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Alon–Jaeger–Tarsi | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Bin packing MIRUP | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 3/3 | 0/3 |
| Caccetta–Haggkvist | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Deterministic vs. randomized queries | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Evasiveness | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
Table 15: Open-conjecture results on TCSExam-Full. Accepted proofs or refutations / attempts.
Figure 7: Complete theorem proofs across individual attempts. Each cell represents one scheduled attempt: 100.0% denotes an accepted complete proof and 0.0% denotes no accepted complete proof. The eight agents contribute 320 attempts on the same 20 theorems. Columns number independent attempts within each agent. Task indices and theorem names match Table 12 .
Figure 8: Construction scores across individual attempts. The matrix contains all 320 scheduled Full attempts across eight agents. Cells show percentage scores to one decimal; outlines identify unrounded scores above the reference of 100.0%. Color follows a common score scale, while mathematical parameters and scoring functions differ by task. Evaluation conditions are documented in Appendix D .
| Model | Relative (%) | Task score (%) | Failed / judged |
|---|---|---|---|
| GPT-6 Astra | 64.7 | 107.1 | 44/1870 |
| Kimi K3 | 48.7 | 78.1 | 313/5610 |
| GLM-5.3 | 49.1 | 81.1 | 108/1870 |
| Qwen3.8 Max (0902) | 49.2 | 64.7 | 86/1870 |
| Grok 4.6 | 43.8 | 74.6 | 227/1870 |
| DeepSeek V4.1 Flash 0910 | 48.3 | 77.9 | 347/5610 |
Table 16: Solver scores and unsuccessful evaluations. Task scores use unbounded difference ratios or solve rates. Failed evaluations include rejected solutions, crashes, and timeouts; counts cover all judged instances.
| Model | Validity (%) | Full sets / attempts | Certified (%) |
|---|---|---|---|
| GPT-6 Astra | 99.3 | 24/27 | 90.1 |
| Kimi K3 | 97.2 | 75/81 | 72.1 |
| GLM-5.3 | 97.5 | 25/27 | 68.8 |
| Qwen3.8 Max (0902) | 97.2 | 25/27 | 77.7 |
| Grok 4.6 | 93.9 | 23/27 | 81.6 |
| DeepSeek V4.1 Flash 0910 | 97.2 | 74/81 | 68.2 |
Table 17: Validity and instance coverage of submitted solvers. Validity gives equal weight to each of the 27 optimization tasks; Full sets count attempts with valid results on every instance. Certified averages completion rates for quantified Boolean formulas, syntax-guided synthesis, and vertex-cover certificates.
| Task | Astra | Kimi K3 | GLM | Qwen3.8 Max (0902) | Grok | DeepSeek V4.1 Flash 0910 | ||||
|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 1 | 2 | 3 | 1 | 1 | 1 | 1 | 2 | 3 | |
| AtCoder AHC058 | 100.1 | 96.3 | 97.3 | 97.2 | 96.7 | 97.1 | 95.9 | 98.8 | 97.8 | 98.5 |
| Bin packing | 100.0 | 78.8 | 79.1 | 78.8 | 73.5 | 68.6 | 69.0 | 69.1 | 78.2 | 77.9 |
| Cluster editing | 100.4 | 100.4 | 100.3 | 100.2 | 100.4 | 100.2 | 100.0 | 100.3 | 100.3 | 100.3 |
| Frequency assignment | 100.3 | 99.1 | 100.3 | 100.2 | 100.1 | 100.3 | 100.3 | 100.0 | 100.3 | 100.3 |
| AtCoder AHC041 | 101.3 | 99.6 | 99.1 | 98.2 | 99.2 | 100.1 | 97.3 | 92.1 | 96.8 | 98.4 |
Table 18: Per-attempt Solver task scores (%). Optimization tasks use unbounded difference ratios; decision tasks use solve rates.
| Task | Model | Instance | Score (%) | |||
|---|---|---|---|---|---|---|
| Treewidth | GPT-6 Astra | he134 | 249 | 248 | 201 | 4800.0 |
| Logic synthesis | Qwen3.8 Max (0902) | ex37 | 698 | 106 | 273 020 | -46000.3 |
Table 19: Raw objectives and ratio scores for two minimization instances. : baseline; : task reference; : attained objective.
Figure 9: Solver results across individual attempts. All 480 Full attempts across eight agents are shown on the Kimi K3-relative scale; a task uses the same eligible instances for all models. Table 18 gives original unbounded scores for the initial six agents.
Figure 10: Kimi K3 performance across proof settings. (a) The six largest absolute guided-minus-ladder mean differences among 20 theorems. Circles show individual attempts; diamonds mark means, with differences in percentage points. (b) Universal Dijkstra and discrete bidding games, which retains bare success with incomplete ladder/guided attempts. Each marker is an independent attempt; stars identify complete proofs. Bare receives binary credit, while ladder/guided also award partial checkpoint credit. Horizontal offsets separate the three attempts. Full results and checkpoint details appear in Appendix E.3 .
| Model | Outcome | Bare | Ladder | Guided |
|---|---|---|---|---|
| Kimi K3 | Successful attempts | 7/60 (11.7%) | 7/60 (11.7%) | 18/60 (30.0%) |
| Theorems solved | 3/20 | 4/20 | 7/20 | |
| DeepSeek V4.1 Flash 0910 | Successful attempts | 0/60 (0.0%) | 2/60 (3.3%) | 11/60 (18.3%) |
| Theorems solved | 0/20 | 2/20 | 6/20 |
Table 20: Complete proofs under bare, ladder, and guided settings. Each agent has three attempts on each of 20 theorems. A theorem is solved if at least one attempt proves it completely.
| Kimi K3 | DeepSeek V4.1 Flash 0910 | ||||||
|---|---|---|---|---|---|---|---|
| # | Theorem | Guided | Ladder | Guided | Ladder | ||
| 1 | Corners theorem | 25.0 | 20.8 | +4.2 | 25.0 | 25.0 | +0.0 |
| 2 | Negations in small-depth circuits | 100.0 | 81.0 | +19.1 | 61.9 | 57.1 | +4.7 |
| 3 | Universal Dijkstra | 100.0 | 79.2 | +20.8 | 41.7 | 41.8 | -0.2 |
| 4 | Three taxis | 83.7 | 75.0 | +8.7 | 79.2 | 66.7 | +12.5 |
| 5 | Monotonicity testing | 91.7 | 58.3 | +33.3 | 70.7 | 62.5 | +8.2 |
Table 21: Proof-guidance scores on 20 theorems. Scores are percentages averaged over three attempts; is guided minus ladder in percentage points.
| Theorem | Bare | Ladder (%) | Guided (%) |
|---|---|---|---|
| Universal Dijkstra | 2/3 | 75.0, 75.0, 87.5 | 100.0, 100.0, 100.0 |
| Discrete bidding games | 2/3 | 38.0, 25.0, 88.0 | 62.0, 0.0, 0.0 |
| Small-depth negations | 3/3 | 57.1, 85.7, 100.0 | 100.0, 100.0, 100.0 |
Table 22: Proof-guidance outcomes for the three theorems solved by Kimi K3 in the bare setting. Bare gives complete proofs / attempts; ladder and guided list task scores (%). Attempts are independent across settings.
Figure 11: Complete-proof and checkpoint acceptance for the Kimi K3 cases. The top row records complete proofs. Each lower row is a conditional checkpoint, including the main-theorem slot. Columns number independent attempts within each setting; gray denotes checkpoints absent from bare. Dijkstra’s third guided submission has an accepted complete proof despite failures in seven isolated checkpoint checks. In bidding’s third ladder attempt, all intermediate checkpoints pass while the main slot does not.
Figure 12: Kimi K3 task scores across individual attempts. Each cell shows a package score as a percentage, rounded to one decimal. Mean differences use the unrounded scores and are given in percentage points. The 20 paired theorems contribute 60 attempts per setting. Scores combine partial checkpoint credit with full credit for accepted complete proofs; complete-proof outcomes are shown separately for selected cases in Figure 11 .
Figure 13: Two constructions submitted by GPT-6 Astra. (a) A 124-vertex, 630-edge graph without 3- or 4-cycles, with a shortest cycle highlighted. (b) The 18 submitted stabilizer generators of a quantum code. Both panels use Astra’s actual submissions; they attain the same parameters as Kimi K3’s constructions in Figure 5 .
Figure 14: An unresolved Paley graph attempt. (a) Auxiliary statements and remaining obligations. (b) A witness excluding only. All 36 edges of the nine-vertex clique are independently verified.
Table 23: Subject coverage of the 20 TCSExam-Lite tasks.
| Metric | Same strict order | Reversed | Tied in both | Tied in one |
|---|---|---|---|---|
| Index | 26 | 2 | 0 | 0 |
| Theorem proving | 22 | 3 | 3 | 0 |
| Solver engineering | 22 | 6 | 0 | 0 |
| Constructions | 25 | 3 | 0 | 0 |
| Open conjectures | 0 | 0 | 15 | 13 |
Table 24: Full–Lite ranking agreement across 8 shared agents. Each row compares 28 agent pairs using unrounded scores.
| Task | Opus 5.5 | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|---|
| Corners theorem | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Discrete bidding games | 1/1 | 1/1 | 3/3 | 2/3 | 1/1 | 0/1 | 1/1 | 1/3 | 0/3 |
| Folded RS codes | 1/1 | 1/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Small-depth negations | 1/1 | 1/1 | 3/3 | 3/3 | 0/1 | 1/1 | 0/1 | 0/3 | 0/3 |
| Quantum cryptography | 1/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
Table 25: Theorem-proving results on TCSExam-Lite. Entries give complete proofs / attempts.
| Task | Opus 5.5 | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|---|
| Bin packing | 56.1 | 56.1 | 49.3 | 50.5 | 49.3 | 48.1 | 41.1 | 47.0 | 48.5 |
| Course timetabling | 86.2 | 86.6 | 56.5 | 47.5 | 63.3 | 47.5 | 27.5 | 67.8 | 47.9 |
| Maximum cut | 54.0 | 53.6 | 51.0 | 49.8 | 48.8 | 52.2 | 50.4 | 50.5 | 49.0 |
| Machine reassignment | 71.3 | 70.5 | 60.2 | 63.1 | 41.7 | 69.6 | 58.5 | 67.8 | 64.6 |
| Quantified Boolean | 34.8 | 48.4 | 32.9 | 33.7 | 27.2 | 37.3 | 27.2 | 38.6 | 42.0 |
Table 26: Solver results on TCSExam-Lite. Entries are mean Kimi K3-relative scores (%).
| Task | Opus 5.5 | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|---|
| Binary code A(24,10) | 100.0 | 100.0 | 106.3 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 |
| No 3- or 4-cycles | 102.1 | 102.1 | 102.1 | 101.4 | 100.0 | 102.1 | 102.1 | 101.4 | 100.7 |
| Kissing number (13D) | 100.0 | 100.0 | 99.9 | 97.6 | 93.8 | 99.5 | 94.3 | 99.8 | 97.6 |
| Ramsey R(4,6) | 100.0 | 100.0 | 66.7 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 | 100.0 |
| Metric TSP | 100.0 | 100.0 | 66.7 | 0.0 | 60.0 | 0.0 | 0.0 | 0.0 | 0.0 |
Table 27: Construction results on TCSExam-Lite. Entries are mean task scores (%).
| Task | Opus 5.5 | GPT-6 Astra | Kimi K3.1 Pro | Kimi K3 | GLM-5.3 | Qwen3.8 Max (0902) | Grok 4.6 | DeepSeek V4.1 Flash 1017 | DeepSeek V4.1 Flash 0910 |
|---|---|---|---|---|---|---|---|---|---|
| Log-rank | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Evasiveness | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Frege proof length | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Online matching | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
| Branching programs | 0/1 | 0/1 | 0/3 | 0/3 | 0/1 | 0/1 | 0/1 | 0/3 | 0/3 |
Table 28: Open-conjecture results on TCSExam-Lite. Accepted proofs or refutations / attempts.
Figure 15: All 340 Lite task attempts across nine agents. Columns number attempts within each agent. All scores are percentages rounded to one decimal. Theorem and open-conjecture outcomes are 0.0 or 100.0; construction outlines mark unrounded scores above the 100.0 reference.