A benchmark built out of research, not coursework
A group at Tsinghua University, Moonshot AI and the Shanghai Qizhi Institute has released TCSExam, a benchmark that asks language-model agents to do theoretical computer science rather than answer questions about it. The paper went up on arXiv on 5 November; its authors include Zhilin Yang of Moonshot AI and Andrew Chi-Chih Yao of Tsinghua.
The Full set is 100 expert-reviewed tasks across four tracks. Twenty are research theorems to be proved in Lean 4, where the kernel decides whether a submission counts. Thirty are solver-engineering problems, where the agent submits a reusable program that is run across instance families. Twenty are constructions, scored against documented records. The last thirty are open conjectures: prove the statement or its negation, and nothing short of a complete proof counts as a resolution.
The table
Eight agents were run on the Full set. GPT-6 Astra leads the combined TCSExam Index at 71.9, ahead of Kimi K3.1 Pro at 57.4, Kimi K3 at 46.8, the October build of DeepSeek V4.1 Flash at 46.0, GLM-5.3 at 45.5, Qwen3.8 Max at 44.8, Grok 4.6 at 40.5 and the September DeepSeek build at 40.4.
A 20-task Lite subset, five per track, cuts the number of attempts by 80% at the same per-attempt budget. Nine agents were run on it, and Opus 5.5 — which was not run on Full — tops it at 72.3, ahead of GPT-6 Astra’s 67.0. The two sets rank the eight shared agents almost identically, at a Spearman’s rho of 0.93.
Nobody closed a conjecture
The open-conjecture track is where the benchmark is most useful and least flattering. The authors report no accepted complete solution to any open conjecture.
Two submissions were accepted, and the paper is explicit about what they were. Kimi K3.1 Pro and the October DeepSeek build retrieved counterexamples and Lean proofs OpenAI had already published for Ryser’s conjecture and the modified integer round-up conjecture, and adapted them to the task definitions. The paper notes the tasks were written before OpenAI’s release.
The one genuinely new result is narrower and better evidenced. GPT-6 Astra proved the Alon–Jaeger–Tarsi conjecture over the field of five elements for every n up to 9, using counting identities and an exact integer certificate to rule out a minimal counterexample. The paper says independent Lean verification confirms it using only standard axioms, and that it extends prior results that reached n ≤ 7 and n ≤ 8. Four further verified special cases sit in the appendix.
Read the authorship line
The scores are the benchmark team’s own, and two of the authors work at Moonshot AI, whose Kimi models take second and third on Full. Opus 5.5 appears only on Lite, so its 72.3 cannot be set against GPT-6 Astra’s 71.9 on Full.
What the benchmark is actually measuring is worth keeping straight. A Lean-checked proof of a special case is a verifiable contribution; retrieving a published counterexample and reformatting it is not the same thing, and TCSExam is one of the few evaluations that distinguishes the two in print.
