摘要:
2026年9月11日,陶哲轩发表《A Severe Misalignment of AI in Mathematics》,与多位菲尔兹奖得主共同指出,AI公司把解决著名未解问题当成能力展示,与数学共同体追求可理解、可验证、可传承知识的目标出现了严重错位。争议迅速发酵,是因为它触碰了一个比“AI会不会取代数学家”更具体的问题:当一家实验室拥有大规模算力、封闭模型和传播渠道,它可能在研究者尚未完成论文、同行评议或概念整理之前生成答案并宣布突破。此时,优先权如何确认,署名如何分配,证明由谁验证,失败成本由谁承担,数学研究是否会被少数平台的发布节奏重塑,都没有现成规则。
数学成果不只是一个真假标签
公众常把数学想象成答案明确的竞赛:猜想要么被证明,要么没有被证明;谁先给出正确证明,谁就赢得荣誉。真实研究远比这复杂。一个重要证明通常包含新定义、新方法、多个中间命题、对旧理论的重新组织,以及让其他研究者能够复用的解释框架。最终定理只是知识生产链的一个终点。同行需要检查论证、找到隐含条件、比较不同路线、把方法推广到相邻问题,并通过讲座、课程和后续论文把它转化为共同理解。
这也是为什么一份形式上正确但极难理解的证明,未必能立刻改变数学。计算机辅助证明早已存在,四色定理、开普勒猜想等案例说明,机器计算可以成为严格证明的一部分;形式化证明工具又进一步把自然语言论证转成由小型可信内核检查的表达。但这些实践通常强调可复核的计算过程、公开的代码或形式化对象,以及人类对证明结构的解释。大模型生成的长篇自然语言证明处于另一种状态:文本可能流畅,局部步骤也像数学,却会在微妙处偷换条件、循环论证或引用不存在的结论。即使模型偶然找到正确路线,人类仍需付出大量劳动验证和整理。
因此,陶哲轩等人的担忧不能简化为数学家害怕竞争。声明所说的“misalignment”是目标函数错位:AI公司的产品目标倾向于制造可传播的里程碑,基准需要明确、醒目、可以比较;数学共同体的目标则包括可靠性、理解、信用、人才培养和长期知识积累。一个模型在媒体发布会上“解出”著名问题,对公司品牌价值极高;但如果证明没有充分审阅、研究者的未公开工作被吸收、错误由社区免费排查,收益与成本就落在不同主体上。
从纳维—斯托克斯争议看“优先权”为什么脆弱
本轮讨论与OpenAI宣布纳维—斯托克斯问题相关进展的事件交织在一起。对具体数学结论,应等待完整论文、严格审稿和独立验证,不能把新闻标题等同于千禧年难题已经正式解决。更值得关注的是流程:重大问题可能已有数学家投入多年,部分想法通过预印本、研讨会、邮件、评审或私下交流传播;AI实验室又可能让模型广泛阅读公开材料,并通过与专家互动获得提示。当模型最终生成一条证明路线时,很难用传统的“第一个完成者”规则划清贡献边界。
科学优先权制度原本就不完美,但它至少建立在相对可追踪的论文、预印本、报告和通信记录上。生成式AI引入了新的不透明层。模型训练数据通常无法逐条追溯,推理过程未必公开,提示词与人工筛选可能涉及几十名工程师和数学顾问,实验室还可能选择只发布成功结果。在这种情况下,“模型独立发现”是一项需要证据支持的主张,而不是一句营销描述。若相关研究者正在解决同一问题,实验室是否有义务联系他们、延迟宣传或明确引用,也成为新的伦理问题。
这里还存在一种“发现—验证不对称”。模型或大规模智能体系统可以以极低边际成本生成成千上万条猜想和证明草案,而数学家验证每条路线仍需高成本。发布者可以从正确的那一条获得声誉,却把大量错误候选的筛查成本转嫁给社区。若没有清晰的证据包、机器可检查形式和负结果记录,数学界可能被迫在噪声中寻找少数真成果。这与软件安全中的漏洞报告类似:提交一个未经验证的高危声明很容易,复现、定位和修复却需要专业团队投入时间。
“证明正确”与“理解为什么”之间的距离
数学研究的价值之一,是压缩复杂性。好的理论不是简单堆叠推导步骤,而是找到使大量事实同时变得自然的概念。黎曼几何、群论、概率论和范畴论之所以重要,不只是它们证明了若干定理,而是它们提供了一套看问题的语言。大模型若通过超长搜索或组合已有技巧找到证明,可能先给出“可验证答案”,后续人类再提炼概念。这并非没有价值,但发现顺序改变后,科研组织方式也会改变:验证者、解释者和形式化工程师的重要性会上升,而传统上聚光灯集中于“解题者”的奖励机制需要调整。
有人以望月新一的abc猜想工作为例,认为数学共同体本来就有消化巨型、陌生证明的能力。这个类比提示我们保持乐观,却也说明消化过程可能持续多年,并消耗大量顶尖人才时间。AI若把此类输出从罕见事件变成日常现象,社区无法对每个声称的重大结果投入同等资源。未来的关键基础设施也许不是更大的“数学答案生成器”,而是一套证明分诊系统:先检查定义与依赖,再形式化关键引理,标注与现有文献的重合,最后把最可信、最具新意的结果交给专家。
形式化证明在这里可能扮演重要角色。Lean、Coq、Isabelle等系统允许证明由小型内核逐步核验,能显著降低“文字看似合理但逻辑有洞”的风险。不过形式化并不自动解决所有问题。把自然语言数学转成形式语言需要大量工程劳动;定理陈述本身可能遗漏了研究者真正关心的语义;一个通过内核的证明也可能依赖不合理公理,或以极其冗长的方式掩盖缺乏概念创新。形式验证提供的是正确性底线,不是学术价值的全部评价。
数学家的信用应该怎样重新分配
如果未来重大证明由人和AI共同完成,简单地把AI列为作者并不能解决问题。作者身份通常意味着能够对方法负责、回应质疑并确认利益冲突,而模型不具备这种责任主体地位。更可行的做法,是像实验科学披露仪器和计算流程那样,详细记录模型名称、版本、提示策略、工具链、搜索预算、人工筛选过程、外部专家输入和最终修改。真正承担研究判断与责任的人仍应署名,但机器贡献需要可审计。
优先权也应从单点“谁先宣布”转向贡献谱系。提出关键猜想、构造决定性例子、发现核心引理、完成机器搜索、验证证明、给出概念化简化和建立后续理论,可能分别由不同团队完成。期刊、奖项和招聘体系若仍只奖励最终定理的首个发布者,就会鼓励实验室追求抢发,而不鼓励解释、复现和公共基础设施建设。数学界需要更细粒度的贡献声明,类似软件项目记录设计者、实现者、审阅者和维护者。
训练数据权利同样绕不开。公开论文可以供人阅读,不代表任何规模、任何用途的自动化抽取都不存在规范争议;未公开草稿、评审材料和私下交流则更敏感。研究机构应明确哪些材料可以进入模型环境,商业实验室应说明是否保存专家交互用于训练,学术会议也需要更新保密与评审政策。如果数学家为了避免想法被模型吸收而减少开放交流,整个领域反而会失去最珍贵的合作传统。
AI公司需要怎样的“科研发布协议”
一套最低限度的协议可以包括六项。第一,重大数学主张发布前必须经过独立专家评估,不能只由参与项目的顾问背书。第二,同时发布足够完整的证明文本、依赖资料和可复现实验,使外界能够判断而非相信。第三,披露模型、计算预算、搜索空间、人工提示和筛选过程,避免把团队工程包装成模型的瞬间灵感。第四,主动进行文献与贡献溯源,对高度相关的在研工作给予合理通知和引用。第五,为错误更正和撤回建立显眼机制,不让轰动标题长期存在而修正藏在角落。第六,承担验证成本,例如资助独立形式化团队,却不以资助换取结论。
这些规则不会阻止AI做数学,反而能提高成果进入知识体系的速度。技术史反复表明,工具被共同体接受通常不是因为它能力最强,而是因为它形成了可重复、可问责的实践。计算机代数系统、数值模拟和形式化证明都经历过类似过程。大模型的特殊之处在于生成速度与传播速度极快,所以规范建设不能等到争议自然平息。
对科研机构和年轻研究者的现实建议
高校与研究院应把AI使用规范从“是否允许”推进到“如何记录”。研究组可以保存模型对话、提示词、代码执行轨迹和人工修改历史;论文中明确AI用于检索、猜想、证明草案、形式化还是语言润色;对核心结论,要求作者能够脱离模型解释每个关键步骤。敏感项目采用本地或受控环境,防止未公开结果通过第三方服务泄露。
年轻研究者不必在“拒绝AI”和“完全依赖AI”之间二选一。更稳健的能力组合是:用AI扩大探索面,用传统训练维持判断力,用形式工具提高验证强度,再用清晰写作把结果转化为他人可理解的知识。未来稀缺的可能不是生成十种证明路线的能力,而是判断哪条路线真正新颖、为什么有效、能推广到哪里,以及如何把它放回数学传统之中。
对工业研发的旁照
这场数学争论与工业智能并不遥远。在CAD、CAE、工艺设计和故障诊断中,智能体也可能迅速生成“答案”:一个结构方案、一组仿真参数、一条工艺路线或一个维修结论。但工业组织真正需要的是可追溯的依据、约束满足情况、责任人审批和可复用的工程知识。如果只奖励智能体给出最快结果,工程师的隐性经验可能被吸收却得不到记录,错误验证成本则由现场承担。
因此,工业数字工匠平台应从一开始保留贡献链:谁提出问题,模型调用了哪些知识,使用了哪个求解器,哪些约束由规则引擎检查,工程师修改了什么,最终由谁批准。数学界正在争论的信用、理解和验证,恰好也是工业智能体走向生产系统时必须解决的治理问题。
结语
陶哲轩的公开声明不是一道要求世界停止使用AI的禁令,而是一份关于科研目标的提醒。数学不只是一座等待机器插旗的难题清单,它是一套由人共同建造、检查、解释和传承的理解体系。AI完全可能成为这个体系中极具力量的新成员,但前提是平台的速度、资本与传播优势不能替代证据、信用和责任。真正成熟的“AI数学”不会以人类是否被击败来衡量,而会看机器生成的成果能否被共同体理解、验证、归因,并继续长成新的知识。
参考资料
- 陶哲轩:A Severe Misalignment of AI in Mathematics
- Math and AI Declaration
- Horizon 2026年9月12日中文汇总
- Lean定理证明器
- Clay数学研究所千禧年难题