图灵奖得主姚期智与月之暗面创始人杨植麟第一次联合署名，交出的不是一篇模型论文，而是一张考卷。这套评测集叫TCSExam，科目是理论计算机科学，共100项研究任务，全部采用机器验算，不靠人工打分。题目分成几类：需要逐行形式化验证的定理证明、需要构造出满足条件对象的构造题、以及一批悬置多年的开放猜想。九个前沿模型参加了这场考试，成绩单出来之后，最值得看的不是最高分，而是分数在不同题型上的断崖。
评测大模型最难的一件事是判分。写文章好不好、答得有没有道理，都需要人来判断，而人的判断有主观性，也有成本。这导致多数评测要么样本量小，要么评分标准模糊，结论的说服力有限。
理论计算机恰好绕开了这个难点。定理证明的每一步可以被形式化系统逐行检查，证明对不对是二值的，没有中间地带。构造题更干脆：要一个124个顶点、630条边的图，既不含三角形也不含四边形，构造出来了就检查一遍，符合条件就算对，不符合就算错。
这种可验证性让评测的规模可以放大。100项任务听起来不多，但每一项都要机器验算到底，等于把"评分"这件事从人工搬到了编译器。这也是这套卷子最有价值的地方：它给出的不是印象分，是可复现的结果。
更关键的是它可以被反复跑。评价一个模型有没有进步，最怕的是换了题库、换了评分人，前后不可比。机检的好处是同一套题目、同一套验算程序，今年跑和明年跑用的是同一把尺子。这类评测对行业的价值往往不在当次排名，而在于它建立了一条能长期观测的基准线。
定理证明题共20道，使用Lean 4逐行机检。成绩最好的是GPT-6 Astra，裸考证出14道，成功率70%；Kimi K3.1 Pro以38.3%排在第二。这个分布本身就说明问题：第一名与第二名的差距超过30个百分点，不是同一个档位。
七成的成功率容易被读成"AI已经能替代数学家做证明"，这个推论过头了。卷子里的证明题是从已知定理库里挑出来的，也就是说，这些命题在数学上已经被证明过，证明过程大概率出现在训练数据里。模型的任务更接近"复现一个见过的证明"，而不是"发现一个新证明"。
真正的难点在于形式化的那一步。一段用自然语言写的数学证明，转化为Lean 4能接受的代码，中间要补上大量省略的步骤、声明所有引理、处理类型细节。这一步过去是人工的重活，一个中等难度的定理可能要几天。模型能把这个过程自动化，价值已经很大，但它替代的是"翻译与补全"，不是"想出证明思路"。
所以70%这个数字的正确读法是：在已知命题的形式化上，最好的模型已经能独立完成七成。这是一条很高的工程基线，但它与"能做原创数学"之间还隔着一整层。
整份成绩单里最硬的成果在构造题。Kimi K3造出了一个124个顶点、630条边的图，既没有三角形也没有四边形，把人类已知的参考纪录629条边往前推了一条。GPT-6 Astra把某个二进制编码的上界从84改进到82，同时把Alon-Jaeger-Tarsi猜想的已知成立范围从8维推到9维。
这三项成果的性质与前一类完全不同。证明已知命题是复现，改进纪录是产出新知识。而且这类改进有明确的历史坐标：参考纪录629条边是数学家们用几十年时间一点点推上去的，模型在此基础上加了一条，虽然只是一条，但方向是对的。
为什么构造题更容易出成果？因为它的搜索空间是可枚举的。找一个满足若干约束的图，本质是在巨大的组合空间里搜索，而搜索正是机器的强项。人类数学家的优势在于直觉与结构洞察，能跳过大量无效方向直接猜对区域；机器的优势在于不知疲倦，能把人懒得试的方向全部试一遍。
这两种优势在构造题上恰好可以互补。所以出现"顺手破了纪录"的结果并不意外，意外的是幅度还这么小。一条边、两个上界、一个维度，说明这类问题的前沿已经推得很紧，剩下的空间需要的不只是算力。
真正的分水岭在最难的那一档：30个悬置多年的开放猜想。结果是全军覆没，没有一个模型独立解决。整场考试里仅有6次提交被判定通过，而这6次全部是检索到了已被公开的反例，然后改写提交的。
这6次通过的细节值得细看，因为它暴露了当前模型能力的一个精确边界。模型没有想出反例，它找到了别人想出的反例。这在信息获取层面是有效的，在知识生产层面是零。区别就像一个人能背下所有已知的数学结论，与一个人能推导出新结论。
开放猜想难在哪？难在它没有明确路径。已知命题的证明可以按套路推进：归纳、反证、构造辅助函数、估计上下界，这些套路在训练数据里出现过无数次。而开放猜想之所以开放，是因为所有已知套路都试过了，剩下的需要新的工具或者新的视角。这类突破无法通过增加采样次数获得。
把整份成绩单连起来看，得到的是一个清晰的画像：模型在"路径已知"的任务上已经很强，在"路径未知"的任务上仍然为零。70%的证明成功率、三项构造纪录、以及开放猜想的全军覆没，这三组数据说的其实是同一件事。
这个画像对科研流程的现实意义在于分工。既然模型擅长把已知路径执行到底，那就应该把它放在流程的中段：形式化、验证、穷举搜索、检查边界情况、把猜想在小规模上验证一遍。这些环节过去消耗研究者大量时间，现在可以交出去。
而流程的两端仍然要靠人。前端是想出该问什么问题、该往哪个方向试，后端是判断一个结果重不重要、值不值得继续追。这两件事目前看不到被替代的迹象，因为它们依赖的是品味与判断，而不是搜索。
对做AI for Science的公司来说，这份考卷给出的提示也很直接：不要在"能不能做原创发现"上讲故事，先把"能不能可靠地完成研究流程里的脏活"做扎实。前者目前无法证伪，后者客户明天就能验收。