当人工智能不再只会解竞赛题，而是开始参与长期开放数学问题的探索，“AI破解难题”的新闻正在把数学界推向一个新阶段。真正值得讨论的，不只是模型能否给出答案，而是这份证明应该怎样复核、谁有资格为其负责，以及成果究竟应当署谁的名字。🤖📐
从“生成答案”到“参与研究”
传统数学研究往往经历提出猜想、寻找思路、撰写证明、同行审查等环节。AI加入后，这条流程出现了明显变化：模型可以检索相关概念、尝试跨领域工具、批量生成候选引理，甚至把自然语言论证转写成形式化代码。它更像一台高速“证明路线搜索器”，能够探索人类研究者因时间有限而未曾尝试的组合。
不过，“生成了一份证明”不等于“难题已经解决”。历史上，不少开放问题都出现过后来被发现存在漏洞的长篇论证。对于AI产出的结果，研究者更要区分三个层次：结论看起来合理、推导在形式系统中成立、原始数学问题确实被完整解决。三者不能混为一谈。🔍
机器验证通过，为何仍需人工复核
Lean等证明辅助工具能够把证明拆成严格的形式步骤，并由较小的可信内核检查推理是否符合既定规则。其价值在于减少“显然可得”“容易验证”等隐藏跳步，使其他研究者能够重复运行检查。关于验证AI生成证明时应排查未完成证明、额外公理和异常依赖等问题，可参考Lean验证指南。
但机器验真并非万能。验证器确认的是“形式化命题能否由指定公理推出”，不能自动判断形式化命题是否忠实表达了原来的开放问题。例如，漏掉一个边界条件、误写量词范围，或者使用了未经说明的强假设，都可能让代码顺利通过，却没有真正回答原问题。
一份可信的AI证明至少应接受四层检查
- 命题核对：由领域专家逐项比较原始问题与形式化陈述，检查定义、量词和边界条件。
- 依赖审计：公开软件版本、定理库、额外公理及全部源码，排除隐藏占位符或循环依赖。
- 独立复现：由未参与项目的团队在独立环境中重新编译，并尝试寻找反例。
- 数学解释：把机器代码整理成人类可读的证明，说明核心洞察、新方法及适用范围。
这意味着，未来的同行评审可能不再只是阅读论文，还要同时审查提示记录、候选证明筛选过程、形式化仓库与运行环境。证明生产速度越快，专家复核能力越可能成为新的稀缺资源。
署名争议的核心是责任，而非“功劳排行榜”
如果关键构造由AI提出，直接把全部成果归给操作者，可能掩盖模型的实际作用；但把AI列为作者，又会遇到责任问题。作者不仅获得声誉，还必须确认内容、披露利益冲突、回应质疑并承担研究伦理责任。目前美国数学学会的政策明确表示，AI工具不能作为论文作者，因为它无法承担上述责任；研究者应披露所使用的工具和具体用途，并对全部内容负责。参见美国数学学会AI使用政策。
更稳妥的办法，是采用“人类作者负责、AI贡献分级披露”的模式：作者栏只列能够承担责任的人；方法部分说明模型名称、版本、使用日期和任务；贡献声明区分问题选择、提示设计、证明生成、形式化实现与人工复核；对决定性机器输出保存可审计记录。这样既不把AI伪装成普通软件，也不赋予它无法履行的作者身份。🧾
数学共同体需要建立新的证据标准
- 新闻稿和预印本应使用“提出候选证明”“通过形式检查”等准确表述，避免在同行评议前直接宣布破解。
- 论文应提供完整证明、代码、依赖版本和复现说明，不能只展示模型对话截图。
- 期刊可引入“数学审稿人＋形式化审稿人”的双轨评审。
- 引用既有成果时，应追溯模型所采用的关键定理和构造，避免把文献重组误称为原创发现。
- 机构应提前制定AI研究记录、数据保密、署名和责任追究规范。
总结
AI参与长期数学难题研究，带来的不是“机器取代数学家”的简单故事，而是证明生产、验证和责任分配的重新组合。机器可以扩大搜索范围，形式化工具可以加强逻辑检查，但问题是否被准确表达、成果是否真正原创、论文由谁承担责任，仍需要人类共同体判断。✅
未来最可信的数学成果，未必来自纯人类或纯机器，而可能来自一条透明的人机协作链：AI负责探索，证明器负责核验，人类负责解释、复现与担责。
