共计 1160 个字符，预计需要花费 3 分钟才能阅读完成。
陶哲轩质疑 OpenAI 公司:719 篇 AI 数学证明, 人类真的理解了吗?
OpenAI 在 10 月公开了一批 AI 生成的数学成果, 规模不小:719 份手稿, 覆盖 372 个结果族, 牵涉数百个开放研究问题。但这份成绩单很快引发争议——焦点不在“AI 能不能做数学”, 而在于这些证明有没有被人类真正看懂、验证和消化。
📌 从 722 到 719: 一次发布后的连续调整
时间线并不复杂。10 月 6 日,OpenAI 在 GitHub 上首次放出 722 份 AI 数学手稿; 仅一天后, 因为一处符号错误及其连锁影响,3 份被撤回, 公开目录缩至 719 份。
🔍 顾问小组的建议, 与执行之间的距离
AGMAI 曾建议前沿实验室不要在专有、外界无法访问的模型上测试高难度数学问题, 同时披露模型名称、提示词、推理链、耗时与计算成本。而此次 OpenAI 仍使用专有模型, 附有模型推理链的手稿只有 10 份。
在可理解性方面,顾问小组希望 AI 生成的证明便于数学家审查与学习。但据报道, 约 42% 的证明未作形式化处理, 也缺少把自然语言证明与形式化产物对应起来的机器可读元数据。AGMAI 同时声明, 其咨询角色不构成对 OpenAI 发布这些结果的认可, 最终仍要由数学界判断建议是否得到充分执行。
💡 陶哲轩: 反对的不是 AI, 而是“速通难题”的目标设定
10 月 7 日, 菲尔兹奖得主陶哲轩在 mathstodon 发帖回应。他明确表示并不反对 AI 做数学, 自己也是 AI 辅助研究的积极使用者; 他真正反对的, 是把“用 AI 快速攻克著名难题”当成主要目标或产品展示。
他描述了传统数学的节奏: 一个长期猜想被突破,作者会做报告、参加研讨、与同行交流, 随后证明被简化、解释、写进教材, 并催生新的问题、合作者和研究方向。而在提示者驱动 AI 自主解题的模式下, 目标一旦“解决”, 后续的理解、报告和领域建设往往很少发生。
更让他担心的是,把纳维–斯托克斯方程这类千禧年难题当作模型能力基准, 等于用“解出多少、多快解出”替代“理解与洞见”。他强调, 问题一旦被公开“解决”, 几乎无法恢复为“未解决”, 哪怕只是想寻找另一条路径, 也会被“答案已知”这一事实干扰。在他看来, 这是一种不可持续的大规模“收割”。
📊 几个值得关注的看点
- 透明度: 模型、提示词、推理链、成本是否公开, 决定成果能否被复核。
- 形式化: 未形式化的证明越多, 机器辅助验证的价值就越难发挥。
- 学术节奏: 数学进步依赖讨论与传播, 而不只是答案本身。
- 不可逆性: 公开“已解决”会改变后续研究的探索空间。
🚀 总结
这场争论的核心,其实是评价标准之争: 当 AI 能在极短时间内产出成百上千份证明, 数学界该用什么衡量“有价值”?OpenAI 的 719 份手稿展示了能力上限, 陶哲轩的质疑则提醒, 如果没有理解、验证和同行讨论, 再多的证明也只是待消化的库存。
