导语｜🤖 当“答案正确”不再是终点
近期，AI模型在若干长期开放的数学与理论计算机科学问题上给出证明或取得实质进展，引发广泛关注。相比“AI是否胜过数学家”的热闹讨论，真正棘手的问题其实是：机器生成的证明应当如何复核？成果应该署谁的名字？如果证明通过形式化系统检查，却没有人能够完整解释其中的关键思想，它是否已经成为数学共同体可以接受的知识？
🔍 机器验证通过，不等于争议结束
数学证明的机器复核，通常需要先把自然语言论证翻译成Lean等形式化语言，再由证明助手逐步检查推导是否符合既定公理和规则。这种方法能够发现隐藏的逻辑跳步、条件遗漏和符号误用，为AI生成的大规模证明提供确定性较强的技术检查。
但形式化验证只能确认“被输入的命题能够由给定前提推出”，不能自动保证形式化命题与原始难题完全一致。若问题在翻译过程中被缩小范围、放宽条件或改变定义，即便程序成功通过，验证的也可能不是大家最初关心的那个问题。因此，机器复核至少应同时检查命题对应关系、依赖库、使用公理、形式化代码和运行环境。
一个可以编译的证明，说明其形式结构经受住了检查；一个被数学界接受的证明，还需要说明它解决了什么、为什么重要，以及关键思想能否被其他研究者理解和复用。
🧩 人类审稿仍有不可替代的任务
AI可能在短时间内生成大量候选证明，但同行评审的速度并不会同步增长。专家不仅要检查正确性，还要追踪引用来源、识别已知结论的重新组合，并判断所谓“突破”究竟是完整解决、部分推进，还是旧方法在特殊条件下的延伸。由此产生的新风险不是没有证明，而是证明数量迅速超过共同体的消化能力。
更稳妥的复核方式应当采用分层流程：先由独立团队运行形式化代码，再由领域专家核对命题和已有文献，随后要求研究团队提供自然语言版本、关键引理说明及失败路径记录，最后才进入公开评议。若结论尚未完成同行评审，传播时应明确使用“候选证明”“预印本结果”或“尚待独立验证”等表述，避免把技术演示包装成已经盖棺定论的成果。
✍️ 署名争议的核心是责任，而非礼貌
传统论文署名不仅代表荣誉，也意味着作者能够解释研究过程、回应质疑、修改错误，并承担学术责任。AI模型目前无法独立履行这些义务，因此，多数学术规范并不把生成式AI视为可以承担责任的正式作者。不过，如果模型贡献了核心构造、关键引理甚至完整证明，仅在致谢中写一句“使用了AI工具”，又可能掩盖成果的真实生产过程。
2026年发布的“人工智能与数学莱顿宣言”提出，应维护可归属的作者身份、透明且可独立验证的论证，以及人类对正确性的责任。该倡议并非要求数学研究排斥AI，而是强调工具使用披露、来源归属和共同评议的重要性，可参阅莱顿大学说明及牛津大学数学研究所介绍。
📋 更可执行的署名与披露方案
- 人类作者署名：只列入能够理解核心结论、审查证明并承担责任的研究者。
- AI贡献说明：披露模型名称或版本、主要用途、提示策略、人工修改范围，以及AI是否提出关键思路。
- 来源追踪：对证明依赖的论文、定理库和已有构造进行逐项引用，不能用“模型生成”替代文献溯源。
- 保存审计材料：在条件允许时公开提示记录、候选答案、形式化仓库、依赖版本和验证命令。
- 区分贡献层级：明确AI是用于检索、润色、猜想生成、证明搜索，还是完成了主体论证。
⚖️ 原创性判断面临新的技术难题
AI可以同时吸收大量论文中的方法和表达方式，其输出可能既不是简单复制，也未必属于完全独立的原创发现。若模型组合了多项既有成果，却没有给出可靠引用，人类研究者就必须承担更严格的检索与比对义务。判断原创性时，不应只比较最终文字，还应核查关键构造、引理链条、证明策略和时间线。
这也意味着，模型供应商、研究机构和期刊需要共同建立可审计标准。封闭模型如果无法说明训练材料、检索来源和推理过程，外部研究者就很难判断成果是否真正新颖。商业机密可以得到合理保护，但不能成为跳过独立复核、模糊学术贡献或提前宣传重大突破的理由。
🌱 数学家的价值正在转移，而非消失
当证明生成成本持续下降，稀缺资源将从“写出更多证明”转向“提出值得解决的问题、筛选重要结果、解释关键机制并建立统一理论”。数学家的工作可能更像研究架构师：设定问题边界，监督AI探索，核对形式化表达，再把机器发现转化为可以教学、推广和继续生长的人类知识。
总结｜✅ 争议最终指向一套新的信任机制
AI攻克长期数学难题的意义，不只是增加了一个结论，更迫使学界重新定义证明、作者与责任。现阶段较合理的原则是：机器可以生成和检查证明，人类必须核对命题、追踪来源、解释意义并承担责任。只有把AI贡献披露、形式化复核、独立同行评审和人类可理解性结合起来，一项令人震撼的机器输出，才可能真正沉淀为可信、可继承的数学成果。
