从“素数间距新纪录”看形式化证明的边界

一、先区分三个容易混淆的概念

围绕“素数间距新纪录”的报道，最常见的问题不是计算错误，而是概念被压缩得过于简单。至少需要区分以下三个命题：

1. 是否存在无穷多对相邻素数，其间距不超过某个常数；
2. 是否存在无穷多对素数，间距恰好为 2；
3. 是否已经完成了一个完全无条件、可独立检查的数学证明。

第一个命题属于有界素数间距问题。假设某项研究得到结论：

[
\liminf{n\to\infty}(p{n+1}-p_n)\leq 186,
]

其中 (p_n) 表示第 (n) 个素数，那么它表达的是：素数之间存在无穷多个间距不超过 186 的位置。

这并不等价于孪生素数猜想。孪生素数猜想要求无穷多次出现间距为 2 的素数对，属于更强的结论。即使将上界从 240 压缩到 186，也只能说明研究者在“无穷多次出现较小素数间距”这条路线上取得了进展，不能直接推出间距 2 的情形已经解决。

因此，标题中“人工智能证明了孪生素数猜想”的说法，通常已经越过了原始数学结论本身。

二、数字变小，究竟意味着什么

对于素数间距问题，记录数字的下降通常来自一条非常复杂的解析数论推导。证明过程往往需要构造一组权重，对某个筛选和进行估计，再将问题转化为指数和、相关性和或积分表达式的上界。

抽象地说，研究者可能需要证明如下结构：

[
S(x)=\sum_{n\leq x} w(n)\,F(n)\geq 0,
]

其中 (w(n)) 是精心设计的权函数，(F(n)) 则编码了若干整数同时具有素数性质的条件。如果能够证明 (S(x)) 在足够大的范围内保持正值，就可能推出某类素数构型无限次出现。

但最终的常数并不是由单一公式决定的。它通常取决于多个环节：

• 权函数如何选择；
• 筛参数如何分配；
• 不同误差项之间如何平衡；
• 指数和或相关性和能得到多强的上界；
• 某些积分是否可以通过更精细的区间划分降低；
• 数值优化结果能否转化为严格不等式。

因此，“240 变成 186”并不意味着找到了一个简单的计算技巧，更可能意味着整个证明管线中的参数配置、估计常数和数值证书都得到了一轮优化。

三、形式化验证到底验证了什么

形式化证明系统的价值，在于把数学陈述、定义、推理规则和依赖关系编码成机器可以逐步检查的对象。只要输入的公理、定义和中间引理被接受，系统就能验证最终结论是否按照规则推出。

但这里有一个必须明确的逻辑形式：

[
A_1\land A_2\land\cdots\land A_k
\Longrightarrow C.
]

如果系统验证的是上式，那么它确认的是：

在 (A_1,\ldots,A_k) 全部成立的前提下，结论 (C) 成立。

它并没有自动证明每一个 (A_i)。

在素数间距问题中，这些前提可能包括：

• 某类三阶指数和的上界；
• 某种特征和之间的相关性估计；
• 多重积分的严格数值上界；
• 某些参数范围内的单调性；
• 从离散和到连续积分时使用的误差控制；
• 外部文献中已经得到、但尚未完整形式化的定理。

如果这些内容以“公理”“外部假设”或受信任输入的方式进入形式化工程，那么最终结论就是条件性的。形式化系统验证了推理链条，却没有替这些输入承担证明责任。

四、为什么“脚本通过”不能等于“全部证明完成”

这类项目通常还会配套一个数值证书程序，用来重新计算大量积分、区间上界或参数约束。它的作用很重要，因为复杂证明中常常存在数百个需要核验的数值不等式。

例如，某个参数优化可能要求确认：

[
I_j(\theta)\leq B_j,\qquad j=1,2,\ldots,m,
]

并且这些不等式要在一组区间内同时成立。证书程序可以执行高精度计算、区间算术或分段验证，输出“所有检查通过”的结果。

然而，这种程序的通过通常只能说明：

1. 程序按照既定算法完成了计算；
2. 计算结果满足预先设定的数值条件；
3. 形式化证明可以把这些结果作为输入继续推导。

它不能说明：

• 外部数学定理已经被证明；
• 公式转录过程中没有遗漏前提；
• 数值模型与原始解析表达式完全一致；
• 所有隐含的极限交换、积分交换或一致收敛条件都已经处理；
• 形式化系统使用的公理本身是无条件成立的。

所以，最准确的表述应当是“数值证书验证通过，并且在给定数学假设下，形式化推导成立”，而不是笼统地说“机器完成了整个证明”。

五、如何评估这类成果的可信度

评价人工智能参与的数学成果，不能只看最终数字，也不能只看是否存在形式化代码。更可靠的方法是进行依赖分层。

1. 查看最终定理的逻辑形式

首先要确认最终陈述到底是：

[
C
]

还是：

[
A_1\land A_2\land\cdots\land A_k\Rightarrow C.
]

两者的数学地位完全不同。前者是无条件结论，后者是条件性结论。很多争议都源于摘要只展示了 (C)，却没有显式展示前提集合。

2. 区分定理、引理、公理和计算事实

一个成熟的形式化项目应该清楚标注每个输入属于哪一类：

• 已在当前系统中完成证明的定理；
• 由其他已验证结果推出的引理；
• 暂时作为公理使用的外部结论；
• 由独立程序计算得到的数值事实；
• 依赖人工审查的转录结果。

如果所有内容都被放在同一个“已验证”标签下，读者就很难判断证明的真实覆盖范围。

3. 检查是否存在可信基扩张

形式化证明并非天然等于绝对可靠。系统仍然依赖底层逻辑、内核实现、解析器和若干受信任机制。更重要的是，如果项目允许额外声明未经证明的公理，那么可信基就会扩大。

这并不意味着使用公理是不合规的。数学研究经常引用成熟理论作为黑箱。关键在于必须明确披露：

• 使用了哪些公理；
• 公理来自哪里；
• 它们是否已经在同一基础上形式化；
• 如果移除某条公理，结论是否仍然能够推出。

4. 检查可复现性，而不只是“能运行”

可复现性至少应包括：

• 明确的版本和依赖说明；
• 参数配置与输入数据；
• 生成证书的过程；
• 独立环境中的重新验证；
• 对关键中间结果的单独测试；
• 对异常情况和边界情况的说明。

如果只能运行一个总程序并得到“成功”，却无法定位每个假设和每个数值不等式，那么这种复现更接近演示，而不是完整审计。

六、人工智能在其中真正发挥了什么作用

人工智能可能在多个环节显著提高效率：

• 自动搜索合适的中间引理；
• 将非形式化数学转换成机器可读表达；
• 发现参数配置和优化方向；
• 生成重复性的证明脚本；
• 检查大量边界条件；
• 对文献中的复杂估计进行结构化整理。

这些能力很有价值，尤其适合处理形式化证明中机械、冗长且容易出错的部分。但“生成证明步骤”与“确认输入命题为真”是两件事。

如果人工智能把一组外部估计当作前提，并成功构造出从前提到结论的形式化推导，那么它完成的是证明工程和推理验证，而不是独立解决所有基础数学问题。换句话说，人工智能可能让证明更快、更规范、更容易复核，但它不能通过改变表达方式自动消除未证明假设。

七、怎样更准确地向公众表述

对于此类成果，推荐使用分层表述：

第一层，说明数学结果：

某项研究将有界素数间距问题中的一个已知上界进一步压低。

第二层，说明验证范围：

该结论已经在形式化系统中完成条件性推导，并通过独立数值证书检查。

第三层，说明限制条件：

推导依赖若干尚未在当前项目中展开证明的解析估计，因此不能表述为完全无条件地解决了孪生素数猜想。

这种表述既不会低估形式化工程的价值，也不会把条件性结果包装成悬而未决问题的最终答案。

八、这类工作的长期价值

即使外部假设尚未全部形式化，这项工作仍然可能具有重要意义。

首先，它把复杂证明拆分成清晰的依赖图，使研究者能够准确知道瓶颈位于哪条估计，而不是停留在“整体上似乎可行”的层面。

其次，它能暴露传统论文中容易被忽略的细节，例如参数范围、常数传播、边界条件和积分分割。很多错误在非形式化推导中不易察觉，但在机器检查时会直接显现。

再次，形式化结果具有更好的可继承性。未来如果某条指数和估计得到改进，只需替换相应模块，就可能自动推动最终素数间距上界继续下降。

因此，真正值得关注的不是一句“人工智能证明了什么”，而是它是否建立了可审计、可复用、可逐步扩展的数学证明基础设施。对于素数间距这样长期存在的难题，透明地标明“已经证明的部分”和“仍然依赖的部分”，本身就是比单纯刷新一个数字更重要的进展。