十月的最后一周，AI 在数学版面上交了六份答卷：分工、署名与一声叹息
10 月 30 日，追踪 AI 辅助数学成果的网站 PostCutoff 完成了一次清点：10 月 29 日至 30 日两天，arXiv 上有 374 篇提及 AI 的论文，编辑们浏览了全部 AI 声明、细读约 35 份 PDF，挑出六项单独立目的成果。两天，六项，每一项背后都站着一个具体的模型和一个具体的人类作者…
10 月 30 日，追踪 AI 辅助数学成果的网站 PostCutoff 完成了一次清点：10 月 29 日至 30 日两天，arXiv 上有 374 篇提及 AI 的论文，编辑们浏览了全部 AI 声明、细读约 35 份 PDF，挑出六项单独立目的成果。两天，六项，每一项背后都站着一个具体的模型和一个具体的人类作者，分工方式各不相同。
📜 六份答卷，六种分工
| 问题 | 提交者 | AI 的角色 | arXiv |
|---|---|---|---|
| Murty-Simon 猜想 | Das 与 Fox | GPT-5.6 Sol 找到上界 | 2610.39032 |
| C* 代数谱等距猜想 | Colbrook 与 Stepaniants | GPT-6 Astra 出证明，Lean 验证 | 2610.40470 |
| 在线 Steiner 森林贪婪比 | 相关团队 | GPT Astra 参与，Lean 验证 | 2610.40569 |
| Laczkovich 李普希茨映射问题 | Gaspar | ChatGPT 给出关键命题 | 2610.38834 |
| 纯半单性猜想反例 | Ren | GPT-6 Astra 出构造，Lean 验证 | 2610.39883 |
| Petty 猜想五维情形 | 腾讯 hyprover 智能体 | 智能体主证 | 2610.39967 |
小贴士：Lean 是一种证明助手，数学证明写成代码后由计算机逐行检查。过了 Lean 这关，意味着推理链条在形式系统里无懈可击，但证明背后的想法是否深刻、定理是否重要，仍然只有人类数学共同体能裁决。
🔍 单枪匹马的那两份
清单里有两个条目格外扎眼。一个是单作者：福州大学的 Xinheng Lin，17 页论文证明 Alon-Seymour-Thomas 分离猜想，1990 年提出的 O(h·根号n) 上界。作者声明证明在其指导下用 ChatGPT 6 Pro 完成，每个公式与定理都亲手核对过，GPT-6.1 Sol 的 Max 档被用来反复查证。PostCutoff 编辑部的处理意见写得很直白：单作者，17 页，猜想在业内赫赫有名，在专家发表意见之前一律当 claim 对待。另一个是纯粹的反例：Ren 用 GPT-6 Astra 构造出纯半单性猜想的反例，同样过了 Lean。
把这两份答卷和四份合作卷并排放着看，AI for Math 的分工光谱已经拉开：从「模型找关键引理，人类组织证明」到「模型出完整证明，人类消化核对」，再到「智能体独立署名」，三个月前的主流还停在第一档。速度之外更值得记下的是验证手段的统一，Lean 正在变成这一波成果的公共裁判，六项里过闸的四项自带一层机器背书，没过闸的两项则悬置在 claim 状态等待同行裁决。
🌫️ 同一周的另一场争论
数学家对这波浪潮的态度，恰好也在同一周摆上了台面。菲尔兹奖得主邓煜公开评论 AI 公司的反蒸馏条款：不能只在自己蒸馏全人类知识的时候支持蒸馏。另一边，斯坦福的一场演讲里奥尔特曼说，数学家们的情绪已经从「我们完了」转向接受 AI。两句话放在一起，是同一场变革的两个视角：从模型侧看，数学是符号推理的最后堡垒之一，攻下它的示范效应远超单个定理；从数学家侧看，证明的稀缺性正在坍缩，剩下的问题是品味与选题。
清点本身还有一个容易被漏看的细节：这 374 篇只是「提及 AI」的论文，真正的底数应该更大，因为不是每个作者都声明了 AI 的使用。六份答卷是下限不是全景。数学共同体的评审机器还没跟上这个速度。期刊的 AI 披露政策怎么定，Lean 验证结果算不算期刊认定，AI 参与署名的资格如何裁，都还是悬而未决的空白。10 月的最后一周没有给出答案，只是把题面又抄了一遍，字更大了。
信源与限定：PostCutoff 10 月 30 日清点（编辑团队用 Claude Opus 5.5 在 Claude Code 里撰写，人工编辑 Adam Bicz 署名，自标「等待评审」状态）；六篇论文的 arXiv 摘要页；邓煜与奥尔特曼的言论来自 10 月 30 日中文 AI 早报转述，未核到演讲原文。分离猜想论文的证明未经专家评审，单作者声明未获独立核实；「374 篇」为该网站统计口径。
#数学 #人工智能 #AIforMath