姚期智、杨植麟联合出题：9个大模型同考理论计算机科学，GPT-6 Astra拿70分却在开放猜想交白卷

AI会做数学题，早就不是新闻。AI能做研究级的数学，能被严格验证吗？一篇署名论文给出了目前最完整的一份答卷。

一场由图灵奖得主监考的”统一考试”

11月初，图灵奖得主、清华大学交叉信息研究院院长姚期智团队，联合月之暗面创始人杨植麟等学者，在arXiv发布论文《TCSExam：在TCS研究的全范围内评估前沿大型语言模型》。

考试对象是9个前沿大模型：OpenAI的GPT-6 Astra、月之暗面的Kimi K3.1 Pro和Kimi K3、DeepSeek V4.1 Flash两个版本、智谱GLM-5.3、阿里Qwen3.8 Max、xAI的Grok 4.6。

考卷叫TCSExam，共100道专家评审题，分四个赛道：

• 定理证明：20道研究级定理，证明必须用Lean 4写成，由Lean内核逐行机器验算，不认任何含糊表述。
• 求解器工程：写通用解题程序，跑隐藏测试数据，不能背答案。
• 构造：交出具体数学对象加”证书”，机器核对对象与凭证。
• 开放猜想：30个几十年没人证明也没人推翻的难题，要求完整证明或完整反证。

定理证明：GPT-6 Astra一骑绝尘

最受关注的是定理证明赛道。在”裸考”条件下——只给主定理，不给中间引理——GPT-6 Astra完整证出20道题中的14道，成功率70%。Kimi K3.1 Pro以38.3%排名第二，其余六个模型大多只有个位数，甚至为零。

综合四个赛道的TCSExam指数上，GPT-6 Astra以71.9分居首，Kimi K3.1 Pro拿57.4分，Kimi K3、DeepSeek V4.1 Flash 1017、GLM-5.3分别在46.8、46.0和45.5分一线。Anthropic的Claude Opus 5.5只在20题的Lite版参测，以72.3分领跑。

构造赛道出现了超越人类记录的结果。Kimi K3造出一个124顶点、630条边、既无三角形也无四边形的图，超过论文引用的629条边参考记录。GPT-6 Astra则改进了一个二进制编码上界：长度22、最小距离10的编码最多82个码字，比此前发表的84更紧。所有结果都经过独立核验。

开放猜想：九个大模型集体失败

戏剧性的一幕出现在猜想赛道。30个开放猜想，只有6次提交被接受，而且全部是同一套路：AI联网检索到OpenAI已公开发表的Ryser和MIRUP反例，再改写成Lean证明。论文直言，其余28个猜想没有任何完整解决，未来应在断网条件下评测当时仍开放的猜想。

换句话说，模型在开放研究上交了白卷，”查资料查到的”成绩撑起了全部得分。

失败并非全无价值。GPT-6 Astra在攻关Alon-Jaeger-Tarsi猜想时，独立证明了该猜想在一个五元有限域上对所有不超过9维的情形成立，把此前已知的8维推进一步，且通过Lean独立验证。攻不下”大Boss”，顺手清掉几个”小怪”，这是当前AI做研究的真实写照。

“递小抄”有效，AI缺的是脚手架

论文还有个对开发者实用的发现：给模型补充中间引理和证明思路，成绩明显上升。Kimi K3解出的定理数从3道涨到7道，DeepSeek V4.1 Flash从0道涨到6道。

这说明模型的推理能力并不缺位，缺的是任务分解。对用AI做复杂工程的人，结论类似：与其丢一个巨型问题让模型裸跑，拆成带提示的子步骤，产出质量提升立竿见影。

三条值得记住的信号

一、可机器验证是AI科研的硬门槛。TCSExam的每一道题都由Lean内核或可执行检查器判定，不靠人类评审打分。这种”结果可验证”的评测思路，正在从数学扩散到代码、安全各领域。

二、前沿模型已能产出实质研究成果。研究级定理证明、超纪录构造、通用求解器，三个赛道都有真材实料。姚期智和杨植麟的联合署名，本身说明学界认可这批结果的分量。

三、真正的科学发现还很远。9个最强模型，没有1个独立解决任何一个开放猜想。 DeepMind研究负责人Pushmeet Kohli最近称AI科研进入”相变”阶段，这份考卷提醒大家：训练数据里的题目解得再漂亮，未知的疆域仍是另一回事。

AI能考进理论计算机科学的”奥林匹克”决赛圈了。拿金牌，还得再等几年。