原帖对"GPT-5.6 Sol Pro 写证明 + Lean 零 sorry"这件事的产业含义讲得不错,但漏了几条硬细节——这件工作的真实分量要拆开看才能看透。
补漏 1:这篇论文的另一作者 Yuxin Chen 和第一作者 Jianhao Ma 来自清华与沃顿师生关系——Jianhao Ma 现为 UC Berkeley IEOR 教学教授,PhD 应用数学背景,长期研究方向就是不同 setting 下的 complexity lower bound。这事不是"两个学生 + AI 偶然跑出来的",而是"AI 数学研究者用 AI 工具攻击自己研究了一年的 open problem"。换言之,这是"领域专家 + AI 工具"的标准范本,不是"AI 自主科研"。
补漏 2:148 分钟这个数字比"零 sorry"更炸裂。Jianhao Ma 在自己博客(gokawiil.com)披露:GPT-5.6 Sol Pro 用一份约 10 页的 prompt(模仿 OpenAI CDC 项目的方法论)在 148 分钟不间断工作里给出主证明;Ma 用 GPT-5.4 / GPT-5.5 长期未解,直到看到 OpenAI CDC 公告后改写 prompt 才一举突破。注意:这件事的"难度"不在 prompt 本身,而在"知道该问什么"——Ma 自己在论文里把 prompt 完整附录,意味着任何人都可以复制流程,但能否"问对问题"仍取决于研究者品味。
补漏 3:这不是"AI 写出证明",是"AI 把作者卡了一年的下界做出来了"。问题是确定性的零阶凸优化 oracle complexity:Protasov 1996 给出上界 Q(d,ε) = O(d²),此前最强的下界只有 Ω(d)(从一阶 oracle 模型继承),中间差了一个 d 的线性 gap——30 年没人填。Ma 自己说"spending long sessions trying to solve it with GPT-5.4 and GPT-5.5 with no luck"。GPT-5.6 Sol Pro 在 d⁻⁴ 精度要求下证明了 quadratic lower bound,准确度到 d⁻³——这件事的真正意义是"证明 AI 在下界证明这种创造性任务上能突破人类瓶颈",不是"AI 会写证明"这种泛泛说法。
补漏 4:零 sorry 是验证完整性的硬指标,但还漏了一个关键质量信号——Lean 代码与论文逐行对照的 TRACEABILITY.md。代码在 https://github.com/jianhaoma/gd-lower-bound-lean 公开,任何怀疑者可独立编译。这意味着复现门槛不是"相信论文作者",而是"跑一遍 Lean"——这种可审计性才是"AI 写证明"模式能否被学界接受的关键。
补漏 5:同一周内出现的另一条主线是 Reconstruction 基准(陶哲轩提的"仅凭参考文献清单还原论文核心思想")——前沿模型成功率只有 3%-15%。这意味着"给定明确命题写证明"和"自己想出值得证的命题"之间,还隔着一整个科研品味问题。AI 擅长前者,后者仍是人类的地盘。下一波 AI 数学工具的真正战场,是能否帮研究者"找问题"而非仅仅"证问题"。
下一根钉子:盯 arXiv:2608.10418 这篇论文 30 天内的独立复现报告。如果有 2 个以上独立小组用 Lean 复现通过,这篇论文就从"AI 辅助的成果"升级为"被学界接受的定理";反之,如果 Ben Grimmer(原帖提到的长期研究 silver stepsize 的学者)的"1.2716 是真正天花板"判断是对的,那么下界还可以继续收紧——这意味着真正的极限点还没到。