导语：当AI不再只是润色论文、检索文献，而是能够生成由证明助手逐步核验的数学证明，科研评价体系便遇到一个前所未有的问题：证明通过了机器检查，是否就等于完成了数学发现？模型开发者、提示与流程设计者、命题提出者、形式化工程师和最终审阅者，谁应获得成果署名与学术荣誉？与此同时，同行复现也不再只是“读懂推导”，而要面对软件版本、依赖库、算力预算和模型访问权限等新变量。🤖📐

从“看起来正确”到“可以机器核验”

传统语言模型可能生成结构流畅却暗藏逻辑跳步的证明，而形式化证明要求每一个推理步骤都符合明确的逻辑规则，并由Lean等证明助手检查。Google DeepMind公布的AlphaProof与AlphaGeometry 2曾解决2024年国际数学奥林匹克竞赛六道题中的四道，达到银牌水平；其中部分题目先由人工翻译成形式语言，系统求解时间从数分钟到数日不等，说明“可验证”并不等于“完全自动化”或“低成本”。相关过程可参见官方介绍[1]及其后发表的研究论文[2]。

机器核验主要回答的是：在给定公理、定义、依赖库和形式化命题的前提下，这串证明项能否通过检查。它并不能自动保证形式化命题准确表达了原始问题，也不能判断证明是否具有解释力、原创性和理论价值。因此，验证器给出的“通过”应被视为可靠性证据，而不是对科研贡献的完整裁决。✅

成果归属为何变得复杂

第一种意见强调人类责任原则。AI无法承担研究不端、错误更正、利益冲突披露和学术答辩责任，因此不宜成为作者。现有出版规范大多沿用这一思路。例如，AIP Publishing明确规定AI工具不能列为共同作者；当AI使用可能影响研究发现或结论时，作者需要说明工具、版本、用途及使用理由，详见AI政策[3]。

第二种意见关注实际智力贡献。若研究者只输入一个公开命题，模型独立搜索出此前未知的证明，人类署名是否会夸大贡献？反过来，如果人类完成了问题选择、关键引理设计、搜索空间约束、失败路径分析和结果解释，那么模型更接近复杂科研仪器。争议的核心不是“AI算不算作者”这一道选择题，而是现有署名方式能否准确展示不同参与者的贡献。

更可行的办法，是将“作者身份”与“贡献记录”分开：作者仍由能够承担责任的人担任，同时在贡献声明中列出命题提出、形式化、模型配置、证明搜索、人工干预、独立核验和论文撰写等角色。模型名称、版本、运行日期和调用方式则写入方法部分或专门的AI使用声明。这样既避免把工具人格化，也减少把机器产出全部包装成人类原创的风险。⚖️

复现不能只提交一段证明代码

形式化证明能够编译，只能证明最终产物在特定环境中有效。同行若要复现完整科研过程，至少需要获得以下材料：

• 命题层：原始自然语言问题、形式化命题以及两者对应关系的说明。
• 环境层：证明助手版本、逻辑内核、依赖库版本、构建配置和操作系统信息。
• 模型层：模型名称与版本、系统提示、主要提示词、采样参数、工具调用权限及上下文材料。
• 过程层：候选证明生成数量、失败记录、人工修改位置、搜索终止条件和资源消耗范围。
• 结果层：可编译证明文件、依赖锁定文件、校验脚本、运行日志与便于人类阅读的解释。

如果模型是闭源服务，仅给出提示词往往无法保证重复生成相同结果，因为服务端模型可能更新，输出还可能具有随机性。此时，论文不应宣称“完全可复现”，而应区分结果可验证、计算可重复和发现流程可复现三个等级。即使外部研究者无法重新生成证明，也应能够在独立环境中检查最终证明，并确认其中没有未声明的公理、占位符或不可信扩展。🔍

同行评审需要“双轨检查”

未来的数学论文评审可以采用技术轨与学术轨并行的方式。技术轨检查代码能否构建、依赖是否完整、形式化陈述是否忠实、证明是否调用了不恰当的假设；学术轨则评估命题的重要性、证明策略的新颖性、与既有工作的关系以及对领域的解释价值。机器检查可以减轻逐行排错负担，却不能替代专家对“为什么值得发表”的判断。

期刊和会议还可设置最低披露清单：只要AI参与了关键引理发现、证明搜索或形式化转换，就应披露其作用；若研究结论依赖无法访问的私有模型，应提供经过独立验证的最终产物，并说明复现限制；若人类对模型输出进行了筛选或修补，也应记录关键干预，而不是笼统写成“使用AI辅助”。

总结：荣誉跟随贡献，责任必须落到人

AI产出可验证数学证明，确实提高了结果可信度，却没有自动解决成果归属、原创性判断和科研复现问题。较稳妥的共识应是：AI不承担作者责任，人类作者必须对命题、方法、验证和解释负责；贡献则通过细粒度声明如实记录，不能把模型的实质作用藏在“辅助工具”四个字后面。

真正成熟的标准，不应只问“证明有没有通过”，还应追问“证明了什么、由谁推动、依赖什么条件，以及别人能够复核到哪一步”。

当可验证性、透明度和责任链同时建立，AI数学成果才可能从令人惊叹的演示，转化为能够被引用、被复查、被扩展的公共知识。🧭