TCSExam Reveals LLMs' Differentiated Research Skills: Theorem Proving Strong, Autonomy Weak

Benchmark Design: Verifiable Research Outputs

TCSExam evaluates LLMs on four theoretical computer science research task types: theorem proving (submit complete Lean 4 proofs), solver engineering (submit reusable programs that run on specified instance sets), mathematical construction (submit explicit objects with property certificates), and open conjectures (require full proof of proposition or its negation). The full version contains 100 tasks, each allowing up to 12 hours of tool use, programming, and environment feedback. Results are verified by Lean 4 kernel or executable checkers , not by another LLM judging answer similarity. Tasks undergo creation by an authoring agent, independent review agent, trial runs, and expert confirmation to catch mismatches, checker bugs, and anomalies.

Results: Capability Profiles Diverge Across Task Types

On the full leaderboard, GPT-6 Astra scores 71.9 (rank 1) and Kimi K3.1 Pro scores 57.4 (rank 2). However, aggregate scores mask sharp differences across task categories. Astra solves 14/20 theorems without intermediate lemmas (70% success rate); Kimi K3.1 Pro achieves 38.3% (23 successes in 60 attempts covering 9 distinct theorems); the other six agents stay below 11.7%. Yet Kimi K3.1 Pro solves the PCP alphabet reliability task in all three attempts, while Astra fails it. DeepSeek V4.1 Flash 0910 completes zero bare theorem proofs but constructs graphs exceeding the task's reference value.

New Verifiable Results: Beyond Reproducing Known Answers

Kimi K3 produces two notable constructions: a 124-vertex, 630-edge triangle-free and quadrilateral-free graph for the Erdős girth-5 extremal problem, surpassing the 629-edge reference; and a [[25, 7, 6]] quantum stabilizer code , raising the minimum distance from 5 to 6. Astra independently achieves both parameters. Astra also proves A(22,10) ≤ 82 , tightening the published upper bound of 84. These outputs are independently verifiable objects, parameters, or proofs—not merely plausible new answers. The paper cautions that exceeding reference values does not equal solving the entire mathematical problem or finding global optima, but demonstrates that agents with long budgets and tool support can produce verifiable local improvements.

Ablation: Guidance Helps but Can Constrain Search

A controlled experiment varies context for the same theorem-proving goals: Bare (only proposition and definitions), Ladder (adds intermediate lemmas), Guided (adds proof sketches). Kimi K3 achieves 7/60 full successes in both Bare and Ladder, rising to 18/60 under Guided; distinct theorems solved at least once increase from 3 and 4 to 7. DeepSeek V4.1 Flash 0910 shows 0/60, 2/60, and 11/60 respectively. This indicates that some failures stem from missing task decomposition and research strategy, not absence of raw capability. Human-provided lemmas and proof sketches significantly improve search efficiency. However, guidance is not universally beneficial: several tasks perform worse under Guided, suggesting overly strong constraints can limit the model's own search.

Open Conjectures: Partial Progress and Verified Special Cases

On open conjectures, only Kimi K3.1 Pro and DeepSeek V4.1 Flash 1017 (with internet access) retrieve and adapt OpenAI's published counterexamples and Lean proofs—these do not count as independent solutions. The remaining 28 conjectures receive no accepted full solution. Nevertheless, Astra proves all n ≤ 9 special cases of the Alon–Jaeger–Tarsi conjecture over F₅ , extending the previous classical result of n ≤ 7 and a recent preprint's n ≤ 8, with independent Lean verification. Special-case proofs do not resolve the full conjecture but provide new starting points for further research.

Conclusion: A Terrain Map of AI Research Capability

The paper concludes that TCSExam acts as an AI research capability terrain map : models can now complete partial proofs, program optimizations, and construction improvements under well-defined problems, sufficient compute budgets, and verifiable feedback. However, autonomous research direction selection, value judgment of results, and solving major open problems still require human involvement. The work neither proves the arrival of an AI mathematician nor merely produces another leaderboard; rather, it shows that AI has begun leaving verifiable, real research artifacts in the scientific workflow.

TCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research
arXiv:2611.07962v1

The project is open source. Model and harness selections are also public: Codex, Kimi Code, Claude Code, Grok Build.