共计 1081 个字符，预计需要花费 3 分钟才能阅读完成。
导语:当 AI 能在短时间内生成数百页数学证明,数学界面对的问题已不只是“能不能解”, 而是“谁来理解、如何验证、为谁服务”。OpenAI 最新一批数学与科学结果, 再次把这场争论推到台前。
📌 事件: 成果密集发布, 验证却跟不上
10 月 26 日,OpenAI 公布了数学、计算机科学与物理学领域的三项新发现。与以往不同, 公司没有把它们直接包装成定论, 而是称为有待进一步理解的原始研究材料, 并邀请外部专家核查和解释。
几乎同时,人类数学协会 (AHM) 公布的名单显示, 已有 1008 位全球成员加入, 其中 654 人加入“无 AI 研究小组”, 承诺不发表 AI 生成论文、不与前沿实验室合作、不在研究中使用 AI。今年 10 月初,OpenAI 曾一次性发布 722 份 AI 生成数学手稿, 陶哲轩当时转载 AHM 的客座声明, 呼吁数学界集体行动。分歧由此公开化。
🔍 陶哲轩的判断: 解题进步, 不等于理解进步
菲尔兹奖得主陶哲轩在接受《新科学家》采访时承认,AI 在解题上的进步惊人, 但他担心数学中更重要的部分被忽略。数学不仅是给出答案, 也关乎理解世界、建立联系, 以及知道一个结论为什么成立。
围绕 OpenAI 涉及纳维—斯托克斯问题的一个版本,陶哲轩提到, 相关 AI 生成证明长达约 100 页, 却几乎没有带来数学洞见; 有同事借助 AI 钻研数日, 也只能解释其中一半。他形容这种做法像“自动化掠夺式开采”: 快速拿走结果, 却把理解和后续研究方向留给人类慢慢清理。
💡 两条路线: 开放基础设施与形式化验证
陶哲轩并不主张简单拒绝 AI。他在《Nature》文章中提出“Math 2.0”构想, 认为数学家需要重新评价贡献方式, 也不能完全依赖大型 AI 企业。他倡导 SAIR 开放数学模型计划, 希望数学共同体拥有可参与训练、检查和改进的研究基础设施。
另一条路线来自 Axiom Math。10 月 26 日, 该公司称 AxiomProver 在 Lean 4 中完成有限单群分类定理的形式化证明, 并在过程中发现 34 处原文献中的显著差异, 其中一处需要新的数学推导。这说明 AI 不仅可能“做题”, 也可能帮助梳理知识、检查逻辑漏洞。
- 对研究者:AI 可加速探索, 但验证成本、署名规则和合作边界需要更清晰。
- 对数学共同体:开放模型与研究工具比单纯调用闭源模型更重要。
- 对产业界:“必须加速, 否则对手抢先”的囚徒困境, 可能放大安全风险。
📊 影响与看点: 数学家的角色需要重写
陶哲轩还提醒,AI 擅长解谜, 也意味着它可能擅长寻找系统漏洞。Lean 等证明助手并非完美, 若缺少监督,AI 可能利用漏洞构造看似通过的假证明。因此, 数学训练、形式化验证与安全防护需要同步推进。
