《GPT-6 Astra取得哥德巴赫猜想新进展：刘维尔弱形式实现无条件证明》

GPT-6 Astra取得哥德巴赫猜想新进展：刘维尔弱形式实现无条件证明

AI又向数学无人区迈了一步。

近日，网友 Captain Sude 公布了一项由其归因于 **GPT-6 Astra** 的数学证明：针对哥德巴赫猜想的一个**刘维尔函数弱化版本**，项目声称已经给出了覆盖所有大于2偶数的无条件证明，并提供了完整的 Lean 4 形式化代码。

更关键的是，这次结果并不是经典意义上的“哥德巴赫猜想被证明”。

它解决的是一个把“两个加数必须都是素数”放宽后的版本：对于每个大于2的偶数 \(N\)，都存在正整数 \(a,b\)，使得

N = a + b，且 λ(a)=λ(b)=-1。

公开项目目前已经提供论文、Lean 4 形式化实现以及独立技术复现材料。相关技术审查显示，冻结版本可以重新编译，并报告没有使用 `sorry` 或额外自定义数学公理。不过，AI究竟贡献了多少原创数学思路，以及这项证明的数学地位，仍需要更广泛的独立数学家审查。

经典哥德巴赫猜想，依然没有被攻克

1742年，哥德巴赫向欧拉提出著名猜想：

每个大于2的偶数，都可以表示成两个素数之和。

这就是如今所说的经典二元哥德巴赫猜想。

人类数学家研究了近三个世纪，陈景润等人的工作已经把问题推进到“1+2”形式，但真正的“1+1”，也就是两个素数之和，目前仍未被证明。

所以这次新闻标题里最容易产生误解的地方就是：

Astra并没有证明经典哥德巴赫猜想。

它处理的是一个更宽松的替代问题。

什么是刘维尔函数？

这里要引入一个数论中的重要工具——**刘维尔函数 λ(n)。

简单来说，把一个整数分解成质因数以后，统计质因子的总个数，并考虑重数。

如果这个数量是偶数：

λ(n)=1

如果是奇数：

λ(n)=-1

例如：

但反过来并不成立。

例如某些合数同样可能满足 λ(n)=-1。

于是，数学家把经典哥德巴赫问题中的“两个素数”，放宽成：

两个 λ 值都等于 -1 的正整数。

这样问题就从“寻找两个素数”，变成了研究刘维尔函数的正负符号在加法结构中如何分布。

这个问题此前已经有研究

2024年，数学家 Alexander P. Mangerel 发表了关于刘维尔函数哥德巴赫型问题的研究。

论文研究了类似

[ \sum_{n<N}\lambda(n)\lambda(N-n) ]

这样的卷积和，并证明对于足够大的 (N)，可以得到严格的相关性界限。论文随后发表于 *International Mathematics Research Notices*。

这类结果与刘维尔版哥德巴赫问题密切相关。

而此次 Astra 项目声称的突破，是进一步去掉“足够大”等限制，并将结论推广到所有大于2的偶数。

Astra的第一步：先攻克4的倍数

根据公开项目披露，Astra最初得到的是一个更窄的结果：

所有能够被4整除的正整数，都可以表示为两个 λ 值为 -1 的正整数之和。

证明思路并不是简单进行大规模穷举，而是采用反证法。

假设某个符合条件的偶数无法完成这种分解，然后利用刘维尔函数本身的乘法性质：

[ \lambda(ab)=\lambda(a)\lambda(b) ]

进一步观察乘以2、乘以4之后符号如何变化。

在此基础上，证明通过构造特定的加法分解，再利用差值最小等条件，把假设一步步逼向矛盾。

项目公开材料将这条路线描述为一种结合相关性界限和下降法的证明。

第二步：从4的倍数推广到所有偶数

真正有意思的是第二阶段。

项目方随后公布了另一条证明路线，将结果从4的倍数推广到了：

所有大于2的偶数。

公开描述的核心思路，可以简单理解为把一个原本的“加法分解不存在”问题，转换成有限域中的一种乘法结构约束。

证明大致经过几个步骤：

对于满足条件的素数 (p)，构造与 (2p) 有关的加法分解。

如果这种分解不存在，就会形成一种特殊的“符号缺失”。

通过在有限域上构造相关函数，将原本关于刘维尔函数的加法问题转化成代数结构问题。

证明中一个关键想法，是利用不同乘法路径之间的交换关系。

简单说就是：

先乘以一个数再乘另一个数，与反过来的操作结果相同。

利用这种结构，可以让部分局部“缺陷”相互抵消。

局部得到的乘法性质进一步被推广到整个有限域。

如果最初的假设成立，那么这个函数最终会被迫表现出非常严格的乘法结构。

当这种结构被强制到足够严格之后，再结合二次剩余和二次互反律，可以得到与刘维尔函数原本性质冲突的结果。

最终形成类似：

1 = -1

这样的矛盾。

于是最初“某个偶数无法完成分解”的假设被否定。

这就是公开材料所描述的核心证明路线。

Lean 4验证，到底意味着什么？

这也是这次事件里非常值得关注的一点。

项目不仅公布了数学论文，还给出了 Lean 4 形式化证明。

Lean 是一种可以把数学定理和证明步骤写成机器可检查形式的证明助手。

如果形式化代码成功通过检查，意味着：

代码中的逻辑推导符合Lean所使用的形式化规则。

公开的独立技术复现报告称，冻结版本能够重新构建，并报告没有发现 `sorry`、额外自定义定理公理或 `native_decide` 等情况。

但这里仍然需要区分两件事。

Lean验证的是形式化证明。

它并不能单独证明：

“这一定是AI独立发现的。”

目前公开记录并没有完整披露人类在选题、提示、证明修正、Lean形式化等环节中分别做了多少工作。因此，Astra到底贡献了多少原创数学思路，目前仍然需要更多独立研究者进行判断。

这离真正的哥德巴赫猜想还有多远？

答案很简单：

还差得非常远。

经典哥德巴赫猜想要求：

[ N=p+q ]

其中 (p) 和 (q) 都必须是素数。

而刘维尔版本只要求：

[ N=a+b ]

并且：

[ \lambda(a)=\lambda(b)=-1 ]

问题就在这里。

所有素数都满足 λ(p)=-1，但满足 λ(n)=-1 的数字并不只有素数。

因此：

素数集合是刘维尔值为 -1 的数字集合的一个子集。

把“两个素数”放宽成“两个 λ=-1 的整数”，难度自然下降了一个层级。

所以，这次结果不能直接推出经典哥德巴赫猜想。

但这次AI证明仍然值得关注

真正值得关注的，其实不是“AI终于证明哥德巴赫”这种标题。

而是另一件事情：

AI开始越来越深入地参与形式化数学证明。

过去大家更容易把AI的数学能力理解成计算、搜索、模式匹配或者大量尝试。

而这次公开项目展示的，是另一种路线：

寻找结构 → 构造反证 → 转换问题 → 建立代数约束 → 推出矛盾 → 用Lean进行形式化验证。

尤其是最后一步非常重要。

人类数学家可以判断一个证明“看起来很漂亮”，但形式化系统不会因为证明写得漂亮就放过任何一个逻辑漏洞。

每一步都必须满足形式系统的规则。

当然，目前这项成果仍处于公开项目和独立技术复现阶段，距离传统数学意义上的广泛同行评审还有距离。

因此，更准确的说法应该是：

GPT-6 Astra被公开归因于发现了一个刘维尔版哥德巴赫问题的无条件证明，并已有Lean 4形式化和独立技术复现支持；但这并不等于经典哥德巴赫猜想已经解决。

这或许才是这次事件真正值得关注的地方：

AI还没有摘下哥德巴赫猜想这颗“明珠”，但它正在越来越接近数学家真正工作的方式。