当形式化工程被称作“证明”：一次素数间距纪录传播事件的深度复盘

一、事件轮廓：一个仓库引发的标题狂欢

某研究机构在代码托管平台上公开了一个形式化仓库，主题围绕素数间距（prime gaps）的一个数值纪录展开。仓库的核心内容是用交互式定理证明器（以依赖类型论为基础的语言）对某个结论进行机器检查。消息扩散后，大量标题采用了一个高度简化的表述：“AI 证明了素数间距新纪录”。

这个表述在传播学上极其成功，在数学上则值得推敲。把仓库说明文档往下翻过两屏，画风立刻转变：整个形式化部分是有条件的——它依赖若干条显式声明的公理，包括来自解析数论专著的三阶 Kloosterman 和界、某类特征和的相关性估计，以及上百条外层与内层物理积分上界，这些上界由一段脚本配合数值证书重新计算。脚本自身的说明写得相当坦诚：运行通过“不解除任何一条公理”。

换句话说，机器验证的命题是：“若这些输入成立，则结论成立”。这是一个条件蕴含式，而不是无条件定理。

二、“条件定理”不是缺陷，但“吃掉如果”是

必须先说清楚：依赖文献中的估计作为黑箱，是数学研究的标准操作。任何一篇解析数论论文都在引用他人结果，区别只在于引用是否被逐条核对、是否有人为正确性背书。形式化工具把“引用”变成了显式的公理声明，这本身是透明度的提升，而非退步。

真正的问题出在对外表述上。数学命题有两种状态：

• 无条件成立：所有前提都已被证明，结论可直接使用；
• 条件成立：在若干未验证假设下结论成立，使用时必须携带假设。

形式化仓库精确地记录了第二种状态，而传播标题把它压缩成了第一种。一个不熟悉数论的读者看到“186”这个数字，会以为人类两千年的悬案又被推进了一步；实际上被推进的是形式化工程——把已有论证链翻译成机器可检查的语言，并暴露出所有隐含输入。输入那一半，仍然躺在别人的论文里，没有人替它逐条背书。

这种“条件被吃掉”的现象，在技术传播中有一个通用名字：结论漂移。它不是造假，但它让读者对确定性的估计系统性地偏高。

三、署名责任：机构可以做载体，但不能做责任人

仓库挂在机构名下，作者栏里没有人类姓名。机构当然可以出资、出算力、出工程师，理应留名。但数学几百年来的底线是：内容的正确性必须有责任人。

这条底线不是形式主义。数学结论的可信度，很大程度来自“有人愿意把自己的学术声誉押上去”。当一份成果只有机构署名时，出问题时无法追责到具体判断，读者也无法评估“是谁在什么背景下做了这个判断”。

如果顾问名单里确实坐着一批一流数学家和奖项得主，那么合理的做法是请两位解析数论方向的研究者，把那几条公理输入对着原始文献逐条核对，签名确认，成本不过是几天工作量。这件事不做却急着发通稿，观感自然变成：功劳归机构，验证归社区。

四、给技术读者的四个核查维度

面对任何“机器验证了某数学结论”的宣称，可以用下面四个问题快速定位其真实强度。这套方法对形式化数学、对软件形式化验证、对任何“AI 产出可验证结果”的场景都适用。

维度一：定理的类型是蕴含式还是闭式？

打开形式化源码，看主定理的陈述。如果它形如 theorem main (h1 : A) (h2 : B) : C，那么它证明的是“A 且 B 蕴含 C”。此时要追问：A、B 从哪来？是被证明了，还是被 axiom 声明了？

-- 条件定理的典型形态：结论依赖外部假设
axiom kloosterman_bound : ∀ n, K3 n ≤ f n
axiom correlation_bound : ∀ x, R x ≤ g x
theorem prime_gap_record :
  ∀ x ≥ X0, gap x ≥ 186 := by
  intro x hx
  -- 证明在此处调用上述公理
  ...

看到 axiom 关键字，就应该明白：机器检查的是推理链，不是前提。

维度二：公理数量与来源是否可追溯？

仓库说明里提到的公理，应当能一对一映射到具体文献的定理编号。104 条外层上界、45 条内层上界这类批量输入，通常由数值证书脚本生成。此时要问：脚本的输入是什么？舍入误差如何处理？区间算术是否覆盖了全部参数范围？

维度三：证书脚本验证了什么、没验证什么？

数值证书脚本的典型职责是：给定一组参数，用高精度或区间算术重算某个不等式，输出“通过/不通过”。它不验证数学推导的正确性，只验证数值不等式。仓库说明中“运行通过不解除任何一条公理”这句话，正是对这一边界的诚实声明。读者应当把这句话当作核心信息，而不是脚注。

维度四：是否有具名人类对内容负责？

这是最容易被忽略、却最具判别力的一条。有具名作者，意味着有人愿意承担判断责任；没有具名作者，意味着可信度只能依赖机构声誉，而机构声誉无法在具体技术争议中替代专业核对。

五、表述规范：把“已验证”和“假设成立”分开写

对于产出此类成果的团队，一套可执行的披露规范并不复杂：

1. 主动列出愿意为内容负责的人类作者，哪怕只有一两位；
2. 在摘要第一段就区分两种状态：“已机器验证的推理链”与“未验证的外部输入”，各自列出清单；
3. 给出可复现的原始输出，包括证书脚本的完整运行日志与版本锁定；
4. 慎用“证明”一词。当结论携带未验证前提时，用“候选构造”“条件性形式化”“待核验的推导链”并不掉价，反而提升了可信度。

六、结语：结论对不对是一回事，敢不敢署名是另一回事

形式化工具的真正价值，不是让标题更响亮，而是让假设无处藏身。它把“我们引用了某个估计”变成一行显式的 axiom，这恰恰是它最诚实的部分。问题从来不在工具，而在使用工具的人是否愿意把工具暴露出的条件，原样传递给读者。

数学这行当，结论对不对是一回事，敢不敢署名是另一回事。对做 AI 的技术团队而言，这条老规矩依然适用：机器可以检查推理，但责任无法自动化。把“如果”写回去，把名字签上去，比任何通稿都更能赢得长期信任。