形式化验证与“条件证明”的边界：从素数间距新纪录说起

一、事件回顾：一个被标题简化的结论

近日，某研究机构公开发布了一个形式化验证仓库，声称把孪生素数相关问题的最好上界推进到 186。消息传播时，标题大多简化为一句“AI 证明了素数间距新纪录”。但如果真正打开仓库、逐行阅读说明文档，会发现画风与标题并不一致：整个形式化部分是有条件的，依赖若干条显式声明的公理，以及上百条由外部脚本重算的数值上界。脚本自身的说明也写得很克制——运行通过并不解除任何一条公理。

换句话说，机器验证的是这样一个命题：“如果这些输入成立，那么结论成立。”这本身在数学实践中完全正当，把文献中的估计当作黑箱引用是标准操作。真正的问题出在对外表述上：那句“如果”被吃掉了，只剩下“证明了”。对不熟悉形式化方法的读者而言，186 这个数字很容易被误读为人类悬案又被推进了一大步；而实际上被推进的是形式化工程本身，输入那一半仍然躺在别人的论文里，没有人替它背书。

这篇文章想做的，是把这件事拆开讲清楚：形式化验证到底验证了什么，条件证明的边界在哪里，以及工程团队在类似场景中应当如何设计流程、如何对外表述。

二、形式化验证究竟在验证什么

2.1 证明助手的基本契约

以 Lean 4 这类依赖类型论的证明助手为例，其核心契约非常清晰：编译器检查的是“给定这些定义与公理，目标命题是否存在一个类型正确的证明项”。这里有两个关键点常被忽略。

第一，公理是允许存在的。任何形式化系统都建立在公理之上，选择公理、排中律在不同库中取舍不同。声明一条新公理并不等于作弊，它等于明确标注“此处不再往下追溯”。

第二，数值计算通常不进入内核。像“某个积分上界为 X”这类命题，如果直接在内核里展开计算，代价极高。工程上的通行做法是：由外部脚本算出结果，生成一份证书，再由形式化代码验证证书的正确性。证书脚本与形式化证明是两套东西，前者出错不会被后者自动发现。

2.2 条件证明的合法性与风险

条件证明在数学史上源远流长。大量经典结果都是“在某某猜想成立的前提下”。它的合法性来自透明度：前提被写清楚，读者自行判断可信度。

风险则来自传播环节。一旦“前提”在对外表述中被省略，条件证明就会被误读为无条件证明。这不是形式化方法自身的缺陷，而是表述契约被破坏。对于一个以机构名义发布、作者栏没有具体责任人的仓库，这种破坏的代价尤其高——因为没有人能在出问题时承担内容正确性的责任。

三、拆解这个仓库的四层结构

把这个仓库抽象一下，可以清楚看到四层依赖关系：

第 4 层  最终结论：素数间距上界 186
           ↑ 由形式化代码机械检查
第 3 层  外层/内层数值上界（上百条）
           ↑ 由外部脚本重算并生成证书
第 2 层  若干条显式声明的解析数论公理
           ↑ 引自公开文献，未在仓库内验证
第 1 层  证明助手内核与基础库
           ↑ 由社区长期维护

每一层都有各自的信任假设。第 1 层信任的是内核实现与基础库；第 2 层信任的是文献作者；第 3 层信任的是脚本实现与运行环境；只有第 4 层是真正被机器逐条检查过的。对外宣称“证明了”，实际上只覆盖了第 4 层，而第 2、3 层才是结论成立的实质内容。

这也是为什么脚本说明里那句“运行通过不解除任何一条公理”值得尊重：它诚实地交代了信任边界。

四、工程视角：把条件证明纳入可管理流程

对于在业务系统中使用形式化方法或类似“可验证计算”的团队，这件事提供了几条可直接落地的经验。

4.1 显式声明信任边界

任何验证产物都应当附带一份“信任清单”，逐条列出：哪些命题被当作公理、来源是什么、由谁复核过、失效条件是什么。清单应当作为产物的第一部分，而不是藏在脚注里。

4.2 数值证书要可复现

外部脚本生成的数值证书，至少应满足：固定随机种子、锁定依赖版本、记录运行环境、输出可独立校验的中间结果。理想情况下，证书校验器本身也应当形式化，避免“验证器与被验证物同源”的循环信任。

4.3 责任人必须落到人

机构可以作为发布载体，出资、出算力、出工程师都合理。但内容的正确性需要具体责任人。这不是形式化领域独有的要求，而是所有技术产出的底线。仓库作者栏留空，等于把判断成本转嫁给了读者。

4.4 对外表述与内部结论分离

内部可以写“在 A、B、C 三条公理下，结论成立”。对外则应写成“在某框架下完成了形式化验证，结论依赖若干公开文献中的估计”。两者的差别不是文字游戏，而是防止误读的必要手段。

五、给技术团队的一份检查清单

如果团队计划发布类似的可验证成果，建议在发布前逐项核对：

• 结论的完整命题是否以自然语言与形式语言各写一遍，两者是否一致？
• 所有公理是否集中声明、逐条标注来源与复核状态？
• 数值证书是否可独立复现，校验器是否与被验证代码解耦？
• 是否指定了具体的内容责任人，而非仅挂机构名？
• 对外摘要是否保留了全部前提条件，是否存在被断章取义的风险句式？
• 是否准备了面向非专业读者的解释材料，说明“条件证明”的含义？

六、结语

形式化验证是一项严肃且有价值的工程实践，它把“结论是否成立”转化为“结论在何种前提下成立”，这本身就是一种进步。但进步的价值取决于表述的诚实程度。当“如果”被省略，再精密的机器检查也会在传播中失去意义。对开发者而言，真正的专业性不在于把结论说得更响亮，而在于把边界划得更清楚——无论你验证的是素数间距，还是业务系统里的一条不变式。