AI数学证明刷纪录：条件验证与署名责任

近期，某研究团队公开了一项与素数间距上界有关的成果：公开材料中的上界数字从此前刷新过的 240 进一步压到 186。消息传播后，标题迅速变成“AI 证明了素数间距新纪录”。但细读技术说明会发现，情况并非一句“证明”可以概括：形式化部分依赖若干显式声明的外部输入，数值部分依赖独立证书脚本重算，而脚本说明也明确表示，运行过程并不解除任何一条假设。于是真正需要讨论的问题不是“形式化工程有没有价值”，而是“已验证”与“已证明”之间那条被传播标题省略掉的边界。

一、事件本质：数字纪录不等于无条件定理

素数间距研究关心的是相邻素数之间间隔的上界。把某个上界从 240 压到 186，当然是值得关注的进展，但它至少包含几个不同层次的工作：构造或改进估计、把推理过程形式化、用数值证书验证某些中间界、把工程管线跑通、以及对外传播。每一层都有价值，但每一层的结论强度不同。

形式化验证的强项，是把一条推理链变成机器可检查的对象。它可以显著降低推导步骤出错、遗漏分支、变量范围写错等风险。然而，形式化检查器并不自动证明外部文献中的估计，也不自动证明数值脚本的输入数据真实可靠。若证明脚本以若干外部命题为前提，那么机器验证通过的对象并不是“结论无条件成立”，而是“在这些前提成立时，结论成立”。这是一条蕴含命题，而不是一条无条件定理。

因此，看到“186”这个数字时，专业读者应先问三个问题：这个数字对应的是无条件定理、条件性定理，还是候选构造？条件列表是否完整？条件本身是否经过独立审计？如果这三个问题没有答案，那么“AI 证明了新纪录”就是过度压缩的表述。

二、机器到底验证了什么：条件性验证的技术拆解

条件性形式化的核心结构可以抽象为：

Claim: prime_gap_upper_bound <= 186
Assumptions:
  A1: external_estimate_type_1
  A2: external_estimate_type_2
  A3: external_estimate_type_3
Certificate:
  recompute_numeric_bounds(inputs) -> output_hash
Verification:
  assert formal_derivation(Claim) under {A1, A2, A3}
  assert certificate.output_hash == expected_hash
  assert not discharge_assumption(A1, A2, A3)

这段伪代码表达了三件事。第一，形式化检查器验证的是“在 A1、A2、A3 以及证书重算通过的前提下，Claim 成立”。第二，证书脚本负责重算某些数值上界，但它不负责证明 A1、A2、A3。第三，脚本明确声明“不解除任何假设”，这本身是诚实的工程说明，但它也意味着结论仍然是条件性的。

这里的“公理”或“假设”需要放在工程语境中理解。形式化系统通常有一个很小的信任内核，所有推导都建立在内核规则和显式声明的公理之上。若某条外部估计被作为公理引入，机器只能检查后续推导是否合法，不能检查这条估计在原始文献中是否适用、常数是否正确、误差项是否覆盖所有边界情形。数值证书同样如此：脚本可以重算输出，但脚本自身、输入数据、浮点精度、区间算术实现和运行环境都需要被审计。信任链上任何一层没有闭合，最终结论就仍然是条件性的。

一个成熟的发布材料应当把信任链拆开写清楚：

• 形式化内核是否固定版本、固定配置；
• 每条外部假设的来源、适用范围、审计状态；
• 数值证书的输入、输出、哈希、精度策略和失败样例；
• 验证日志是否可复现；
• 哪些结论已被机器检查，哪些仍依赖人工审阅；
• 是否存在未解除的假设。

只有这些信息完整，读者才能判断“已验证”到底验证了什么。

三、为什么“已验证”容易变成“已证明”

在数学语境中，“证明”是一个强承诺：它通常意味着结论在明确前提下无条件成立，并且有可追责的作者对论证负责。在形式化工程语境中，“验证通过”是一个相对弱的承诺：它可能只意味着某条推导在给定假设下通过了检查器。两者并不是同一个概念，但在传播中很容易被压缩成同一句话。

原因并不复杂。第一，标题需要短，条件说明天然不利于传播；第二，“186”这样的数字有强烈的新纪录暗示，读者容易把它理解为“悬案被推进”；第三，机器验证带有“自动正确”的直觉光环，非专业读者很难意识到公理和证书也是信任根；第四，发布者如果以机构名义发布，公众会默认机构已经完成了内容审核，而实际上审核责任可能仍悬空。

对外表述至少应区分三类结论：

1. 无条件定理：所有前提已证明或已由公认可信的基础推出，且经过同行审阅；
2. 条件性定理：在显式假设下形式化验证通过，但假设尚未被独立审计或解除；
3. 候选构造或待验证形式化：数值或构造上有启发，但形式化、证书和外部输入尚未闭合。

把第二类写成第一类，会把工程进展包装成数学定论；把第三类写成第一类，则会透支公众信任。更稳妥的表述是“候选构造”“条件性形式化”“待独立审计的数值证书”“在若干外部估计下的新上界”。这些说法并不掉价，反而更专业。

四、责任归属：机构署名不能替代人类责任人

机构当然可以作为发布主体。公司出资金、出算力、出工程团队，理应在成果中留名。但数学内容需要责任机制。论文作者署名之所以重要，不只是为了分配荣誉，更是为了明确谁对哪一部分论证负责。若发布材料只有机构名，作者栏没有人类责任人，读者就无法判断：谁核对了外部文献？谁确认了常数和误差项？谁对“结论级别”的表述负责？

如果顾问团队中包含资深数学家，那么最合理的做法不是只把名字放在顾问名单里，而是安排真正熟悉解析数论的人逐条核对输入：外部估计的适用条件是否匹配、常数是否落在可用范围、误差项是否覆盖所有边界、引用版本是否一致、是否存在循环依赖。这样的审计未必需要很长时间，几天工作量就可能完成。成本不高，但它能把“条件性形式化”推进到“假设已审计的条件性定理”。

不做的观感则很微妙：功劳归机构，验证归社区。社区当然可以复核，但发布者有责任先完成基本审计，而不是把最关键的信任根留给外部读者自行背书。尤其当传播标题已经使用“证明”一词时，发布者更应主动列出人类责任人、审计范围和未解决问题。

五、可复现发布规范：从仓库到可审计报告

对于AI辅助数学、形式化验证和数值证书类成果，建议把发布材料做成可审计报告，而不是只放一个代码仓库。一个最小发布清单可以包括：

项目	必须说明	目的
结论级别	无条件定理、条件性定理、候选构造	防止语义升格
假设列表	编号、来源、适用范围、审计状态	明确信任根
数值证书	输入、输出、哈希、精度策略、失败样例	支持重算
验证环境	检查器版本、配置、依赖锁定、运行日志	支持复现
人类责任人	数学审阅人、工程审阅人、审阅范围	明确责任
限制说明	未解除假设、未同行评审、未审计输入	管理预期
对外标题	不得省略条件	统一传播口径
复现入口	一键脚本、预期输出、哈希比对	降低复核成本

可复现性不只是“脚本能跑”。它还包括环境固定、依赖锁定、随机种子、数值精度、输入数据版本、输出哈希和日志留存。证书脚本需要独立复核，不能自证；验证日志应能对应到具体结论；失败样例和边界情形也应公开，因为真实审计往往从边界开始。团队协作时，可以把证明制品、证书输出、环境清单和验证日志放入对象存储并版本化，用日志服务记录验证过程，用监控告警跟踪复现流水线是否偏离预期。这些都是通用工程能力，不依赖特定产品。

六、评价AI辅助数学的合理框架

评价此类成果，建议采用分层框架，而不是只看一个数字。可以把贡献分为五层：

• 数学构造层：是否提出新的估计、构造或改进思路；
• 形式化层：是否把关键推导转成机器可检查的证明脚本；
• 证书层：数值界是否有独立重算路径和可复现输出；
• 审计层：外部假设是否经人类专家逐条核对并签名；
• 传播层：对外表述是否准确区分已验证、假设成立和候选构造。

也可以给出成熟度等级：仅有口头结论是最低层；有可重算证书进一层；有条件性形式化再进一层；假设经独立审计后进入较高层；最终经同行评审或无条件证明才达到最高层。用这个框架看“186”，它可能是一项有价值的形式化工程进展，但若外部假设尚未审计，就不能等同于“无条件证明新纪录”。

七、结论：把“如果”写回来

形式化工程值得肯定。它把推理链变成可检查对象，让错误更容易暴露，也让后续审计有抓手。但形式化验证不是魔法，它验证的是给定前提下的蕴含关系。公理、外部估计、数值证书和人工审计共同构成信任链，任何一环没有闭合，结论就仍然是条件性的。

因此，AI 公司或研究团队发布数学成果时，至少应做到：主动列出愿意为内容负责的人类作者；把“已验证”和“假设成立”分清楚写；给出可复现的原始输出和审计记录；对外标题不省略“如果”。做不到，就不应使用“证明”一词，而应使用“候选构造”“待验证的形式化”或“条件性新上界”。数学这行当，结论对不对是一回事，敢不敢署名、愿不愿意把条件写清楚，是另一回事。把“如果”写回来，不会削弱成果，反而会让成果更可信。