Benchmarks usually output nothing but a leaderboard. TCSExam, posted to arXiv on November 5 (2611.07962), is different: this exam produced two formally verified research artifacts on top of scores — a 630-edge graph construction and a stronger quantum error-correcting code. The 52-page paper counts Turing Award winner Andrew Chi-Chih Yao among its authors, and the code lives under the MoonshotAI organization.
A machine-graded exam for TCS research
TCSExam-Full contains 100 expert-reviewed tasks across four tracks: 20 theorem-proving tasks require a complete Lean proof of a published result; 30 solver-engineering tasks require an algorithm implementation judged on hidden instances; 20 construction tasks require an object or bound with formally verified properties; 30 open-conjecture tasks accept a complete Lean proof or refutation. Grading needs no human discretion: submissions are checked by the Lean kernel (with axiom checks) or an executable task checker. A 20-task Lite version picks five tasks per track and cuts the number of attempts by 80% at the same per-attempt budget; rankings align strongly across the eight agents shared by both suites (Spearman ρ=0.93), supporting Lite as a compact yet discriminative benchmark.
The composite TCSExam Index weights the four tracks at 30/30/30/10; construction scores can exceed one, so the Index is measured in points and may exceed 100. The harness runs Kimi Code as the default agent, also supports Claude Code, Codex and Grok Build, and uses Harbor 0.22.0 to run evaluations and collect outputs.
The scoreboard and two surprise results
On the TCSExam leaderboard, GPT-6 Astra leads Full at 71.9 and Opus 5.5 leads Lite at 72.3. More interesting is what the runs produced: Kimi K3 constructed a 630-edge graph on 124 vertices with no triangles or four-edge cycles, one edge beyond the 629-edge construction from Goedgebeur et al. (2025) — a concrete advance on a lower bound in extremal graph theory. GPT-6 Astra produced a [[25,7,6]] quantum error-correcting code: the same 25 physical qubits protecting 7 logical qubits, with detection distance raised from 5 (the Grassl table reference code) to 6. The project site hedges the claims carefully: "these constructions improve on the best previously known results, to the best of our knowledge." The paper also reports independently verified special cases and bounds from open-conjecture attempts.
Why it matters
The debate over whether AI can do real research has never lacked opinions — it lacked checkable evidence. TCSExam hands grading to the Lean kernel: a proof either passes the kernel or it does not, with no reviewer filter. Solver tasks build on benchmarks from real research communities (PACE, DIMACS, ROADEF/EURO), and the repository ships Docker build recipes and evaluation tooling; code is Apache-2.0 and task statements CC BY 4.0, so the whole thing is reproducible (GitHub). Once "how much research got done" becomes a task-by-task verifiable fact, the next question is how many real theorems these models can stack up beyond the score.