读懂｜月之暗面的定理考卷，GPT-6 Astra 证出 14 道

清华与月之暗面的 TCSExam 用 Lean 判分：GPT-6 Astra 证出 20 道研究定理中的 14 道，自家 Kimi 为 38.3%，公开猜想无一被独立解开。

一张由机器判分的研究级定理考卷，把模型之间的差距拉得比多数榜单都大，出题方自家的模型也没能缩小它。

据 11 月 5 日上传 arXiv 的 TCSExam 论文，GPT-6 Astra 在 20 道不给中间引理的理论计算机定理上证出 14 道，成功率 70.0%。排第二的是月之暗面的 Kimi K3.1 Pro，38.3%；其余六个模型都不超过 11.7%。

这份考卷由清华大学、上海期智研究院和月之暗面的研究者合写，作者里有姚期智和月之暗面的杨植麟。出题方在自家考卷上落后 31.7 个百分点，这是全文最该记住的数。

Lean 判分的 14 道最硬

证明这一列为什么可信：每份提交都要过 Lean 内核检查，证完得满分，差一步就是零分，没有评分模型打印象分。20 道题取自 2023 至 2026 年的论文，覆盖 13 个子领域。

各家的成绩按论文表 2 列出：

Anthropic 的 Opus 5.5 只跑了 20 题的精简版，5 道定理证出 4 道，Astra 在同一组里证出 3 道，精简版总分 Opus 以 72.3 排第一。

样本只有 5 道题、一次尝试，但方向清楚：能稳定交出研究级 Lean 证明的，是这两家的顶级模型。

总分是另一回事。论文的指数按 30、30、30、10 的权重把四项加总。其中求解器一项以多次运行 Kimi K3 的平均成绩为 50 分基准来换算。Kimi 和 DeepSeek 每题跑三次，其余模型只跑一次；精简版的 20 道题是参照最初六个模型的表现挑出来的。

论文自己写明，有 40 多道定理在试跑中被模型证出后退出题库，所以题库受筛题模型的结果影响，但没有写出筛题用的是哪一家。

这些设计都公开了，不算暗箱，但它让 Astra 71.9、Kimi K3.1 Pro 57.4 的总分更像出题方的一种加权方式，不能当作模型座次直接引用。

30 道公开猜想要求完整证明或推翻。Crypto Briefing 11 月 8 日的报道，标题写的是 Astra 在 30 道公开猜想上一道没解。

表里 Kimi K3.1 Pro 有 1.1%、DeepSeek V4.1 Flash 有 5.6%，但项目页写明，这两家是在联网条件下取回 OpenAI 已公开的 Ryser 与 MIRUP 反例和 Lean 证明，再改写成题目要求的形式。

独立解开的公开猜想是零道。Astra 在这一项交出的是局部结果：它把 Alon–Jaeger–Tarsi 猜想在五元域上成立的维度从 8 推到 9，并经独立的 Lean 验证；在构造题上把一类二元码的上界从 84 压到 82。这两项都是论文作者核验的结果，还没有经过同行评审。

出题方自家模型在自家考卷上落后三十多个百分点，这个差距不是榜单噪声。证明一列只认 Lean 内核，判分没有偏好可言，出题的月之暗面也没有理由压低自家模型，这是分析推断，依据是论文公开的判分规则和作者名单。

要让模型写出能过 Lean 的研究级证明，现在该先用 GPT-6 Astra 或 Opus 5.5；指望任何一家模型独立解开公开猜想，这张考卷给出的答案是零。