跑基准通常只产出一个排行榜。11月5日出现在arXiv的TCSExam（2611.07962）不太一样：这张考卷除了给分，还真的跑出了两件经形式验证的研究产出——一个630条边的图构造，和一个更强的量子纠错码。论文52页，作者名单里有图灵奖得主姚期智（Andrew Chi-Chih Yao），代码开在MoonshotAI组织下。
一张机器判卷的理论CS考卷
TCSExam-Full收录100道专家审定任务，分四条赛道：定理证明20题，要求给出已发表结果的完整Lean证明；求解器工程30题，要求实现算法并在隐藏实例上评测；构造20题，要求交出性质经形式验证的对象或界；公开猜想30题，接受完整的Lean证明或反驳。判卷不靠人工裁量：提交由Lean内核（含公理检查）或可执行任务检查器判定。另有20题的Lite版，每条赛道抽5题，在同等单题预算下把尝试次数砍掉80%；Full与Lite共有的八个agent排名高度一致（Spearman ρ=0.93），支撑Lite当一张紧凑但有区分度的卷子用。
综合分TCSExam Index按30/30/30/10加权四条赛道，构造赛道得分可以超过1，所以指数以点计、允许超过100。评测框架默认用Kimi Code当agent，也支持Claude Code、Codex和Grok Build，由Harbor 0.22.0负责跑评测、收产物。
成绩单与两个意外收获
榜单本身：在TCSExam上，GPT-6 Astra以71.9分领跑Full，Opus 5.5以72.3领先Lite。更有意思的是"考出来的东西"：Kimi K3在124个顶点、禁止三角形和四边环的约束下构造出630条边的图，比Goedgebeur等人2025年给出的629边构造又多了一条边——这是极值图论下界的一次具体推进；GPT-6 Astra则构造出[[25,7,6]]量子纠错码，同样用25个物理比特保护7个逻辑比特，把检错距离从Grassl码表参考码的5提到6，同样规模下能多检出一类错误。项目站对这些成果的措辞很克制："据我们所知，改进了此前已知的最佳结果。"论文还报告了公开猜想尝试中若干经独立验证的特殊情形与界。
为什么值得在意
"AI能不能做理论研究"这场争论，缺的从来不是观点，是可核对的证据。TCSExam把判卷权交给Lean内核：证明要么过内核，要么不过，没有评委滤镜。求解器赛道的题目源自PACE、DIMACS、ROADEF/EURO等真实研究社区的基准，仓库配套Docker构建配方与评测工具，代码Apache-2.0、题面CC BY 4.0，整体可复现（GitHub）。当"做出了多少研究"第一次变成逐题可验证的事实，下一个问题才是：跑分之外，这些模型还能攒出多少真定理。