数学界重大突破！
就在最近，GPT-6 Astra又在哥德巴赫猜想上取得新进展了。
网友Captain Sude宣布：Astra已成功证明了关于刘维尔函数的一项类哥德巴赫猜想！
具体来说，它无条件证明了哥德巴赫猜想的Liouville弱形式。
更惊人的是，跟我们的想象不同，这一次，Astra并不只是靠着大力出奇迹的算力碾压——它做出l非常优雅的逻辑推理。
并且，这个证明现在已经通过了Lean 4的形式化验证。
摘不下的明珠
在这之前，哥德巴赫猜想这个幽灵，已经折磨了人类数学家近三个世纪。
1742年，哥德巴赫在欧拉的信中提出这个猜想：「任一大于2的偶数，都可以写成两个素数之和。」
为了它，无数人耗尽心血。从哈代、李特尔伍德，到陈景润证明「1+2」，人类始终无法皇冠上的明珠——「1+1」。
这是因为，素数的分布太诡异了！
既然死磕行不通，数学家们脑洞大开，搞出一套「替身文学」——刘维尔版本的哥德巴赫猜想。
为了模拟素数，数学家们引入了一个奇妙的工具：刘维尔函数。
这个函数记作 ，其中的代表一个数字包含的质数因子的总个数。
它的规则就像一个只认「单双数」的开关：如果一个数包含的质数块个数是偶数，那么λ(n)=1。
如果包含的质数块个数是奇数，那么λ(n)=-1。
所有的纯质数（比如2, 3, 5, 7, 11），它们的刘维尔函数值*都是 -1！然而，反过来并不成立，比如8、12的λ值也是 -1。
2018年，在知名数学论坛MathOverflow上，有人提出了一个弱化版哥德巴赫猜想：
对于每一个大于2的偶数N，是否总能找到两个正整数 a和b，使得 N=a+b，并且 λ(a)=λ(b)=−1。
如果经典的哥德巴赫猜想是对的，那么这俩素数的刘维尔值必然都是-1，所以这个「刘维尔猜想」也*是对的。
但现在，数学家们放宽了条件：加数不一定非得是纯素数，只要它的质因子个数是奇数就行！
黎曼阴影下的突围：AI给出惊天两页纸
既然放宽了条件，应该很容易证明吧？结果，它依然难得令人发指！
问题的核心在于，数学家想要研究这种正负交替的符号在加法组合下，会不会像抛硬币一样互相抵消，从而揭示隐藏在加法底下的深层秩序。这关乎打通数学中「乘法积木」与「加法组合」的桥梁。
直到2024年，数学家 Alexander P. Mangerel 终于有了突破。在一篇论文中，他证明了：对于所有足够大的偶数，这个猜想是成立的。
但是！它的证明带着两个限制。
1.「足够大」：意味着它不包括那些比较小的偶数。
2.「GRH」：他的证明严重依赖于广义黎曼猜想。也就是说，只有在广义黎曼猜想成立的前提下，他的结论才成立。
而这一次，Astra 和 Captain Sude 的团队，直接把这两个枷锁突破了！
一开始，Astra丢出了一份仅仅只有2页纸的PDF。
这份精悍的论文中，Astra 宣布——
无需广义黎曼猜想，可以无条件证明：所有能被4整除的正整数，都可以表示为两个刘维尔值为-1的正整数之和！
在PDF中，Astra巧妙地利用了Mangerel论文中的一个「无条件相关性界限」，结合了一个极其精妙的下降法。
定理的核心逻辑，是用反证法：假设存在一个奇数 m（不被3整除），并且在4m这个规模下，没有任何一对和为4m的数字的刘维尔值都是 -1。
接下来，Astra开始步步紧逼。
1.因为乘以4不会改变刘维尔值，所以m本身也不能被拆成两个负号的数。
2.因为乘以2会翻转刘维尔值（多了一个质因子2），所以 2m 不能被拆成两个正号的数。
3.接着，AI通过构造 a+b=m 且 λ(a)=λ(b)=1的情况，并选取差值 b−a 最小的一对，利用它们与 3的整除关系，强行推导出了一个矛盾！
它发现，如果你假设 4m没有这样的拆分，那么通过乘法与加法的交错逼近，最终会在局部迫使所有的数字都带有相反的符号，这直接违背了Mangerel之前证明的界限。
就这样，仅仅用初等的代数推导（甚至高中生都能看懂推导过程），Astra就这样发现了无条件成立的情况。
48小时，彻底终结全偶数域
而且，还没结束。
据项目作者 Captain Sude 透露，Astra 在*天证明了「4的倍数」情形后，第二天，它又找到了一条全新的初等证明路线，直接把结果推广到了全部大于2的偶数！
这一次，它给出这个核心主张：
其中，没有任何「充分大」的限制，没有有限例外集，所有偶数，无条件成立！
而它的证明思路，更是让人拍案叫绝。
它并没有使用暴力穷举，也没有靠把以前的解析估计压缩得更紧，而是玩了一步漂亮的「结构转化」。
AI的逻辑链条如下。
*步：寻找替罪羊。 AI先证明，对于每一个大于3的素数p ，都存在正整数u,v，使得2p=u+v，并且它们的刘维尔值都是1。如果不成立会怎样？这就构成了「加法符号模式的缺失」。
第二步：逼迫现出原形。 把刘维尔函数延拓到有限域Fp上，定义一个函数G。因为前面的「加法分解不存在」，这个函数G在局部被逼出了乘法对称性缺陷（Defects）。
第三步：*的交换律。 这是证明中最惊艳的一笔！因为乘以 -2 再乘以 -3，和乘以 -3 再乘以 -2 是一样的。AI利用这个「可交换」的性质，让两条路径互相抵消，最终把所有的非零缺陷全部消灭！
第四步：向全局传染。 利用一个下降引理，把局部成立的乘法规则，像病毒一样传播到整个有限域，强迫函数G变成一个全局严格的乘法对象。
第五步：致命一击（二次剩余制造矛盾）。 既然G变成了严格的乘法函数，那么任何数的平方，其G值必须是 1。然而，根据二次互反律，能在有限域内找到一个素数ℓ，它明明是个「平方数」，但因为它是素数，它本身的刘维尔值又必须是 -1。
于是，1 = -1。矛盾爆发！
至此，一开始「分解不存在」的假设被彻底粉碎。Liouville–Goldbach 猜想在全偶数域无条件成立！
这条把加法阻碍转化为乘法刚性的论证路线，简直太优雅了，体现了高度抽象和直觉的*思维。
已通过Lean 4形式化验证
这一次，Astra还同时提交了Lean 4的完整形式化验证。
通过Lean 4验证，就意味着逻辑上*正确。
知乎上UP主@SUNNY99 立马对 Astra 开源的 v1.0.0 版本进行了独立复核。结果令人震撼：Lean 证明可以*重新编译！
其中，最终定理与论文主张完全一致。代码里没有任何「sorry」（在Lean中代表未填补的坑）、没有乱造的自定义数学公理、所有的公理依赖完全正常，249个偶数的数值冒烟测试全部通过。
看到这里，可能有些朋友会问：那这代表哥德巴赫猜想彻底被解决了吗？
我们必须严谨地说：还没有。
目前解决的，是哥德巴赫猜想的刘维尔弱化版本。
从「质因数个数为奇数的合数」跨越到「纯正的质数」，中间仍然隔着天堑。经典的哥德巴赫猜想，依然是那颗高高悬挂的果实。
但是，这绝不意味着这次突破不伟大。
首先，在纯数学意义上，它为整个数论搭起了一座打通「乘法积木」与「加法组合」的宏伟桥梁。
这可能就是未来攻克原版哥德巴赫猜想的核心钥匙。
其次，在AI意义上，这是一个历史性的奇点时刻。
一直以来，我们认为AI擅长的是海量记忆和暴力计算，比如下围棋、算蛋白质折叠。但这一次，Astra 展现出了惊人的数学直觉和品味。
它像一位*天赋数学家，写出一篇让人类数学家直呼优雅的证明。