哥德巴赫猜想这颗数学皇冠上的明珠，被AI撬开了一道缝。
9月21日，网友Captain Sude宣布，GPT-6 Astra成功证明了关于刘维尔函数的一项类哥德巴赫猜想——刘维尔-哥德巴赫猜想的弱形式，并且证明已通过Lean 4形式化验证。更关键的是，这次Astra并非靠算力暴力碾压，而是给出了一段极其优雅的逻辑推理。它先是在第一天证明了4的倍数情形，第二天又找到一条全新初等证明路线，直接把结果推广到了全部大于2的偶数。
这不是经典哥德巴赫猜想的完整证明，但距离那个目标，人类近三百年来第一次看到了钥匙的形状。
1742年，哥德巴赫在给欧拉的信中提出：任一大于2的偶数，都可以写成两个素数之和。从哈代、李特尔伍德到陈景润证明1+2，人类始终无法攻克1+1。
既然死磕行不通，数学家们搞出一套替身文学——刘维尔版本的哥德巴赫猜想。刘维尔函数λ(n)是一个只认单双数的开关：如果一个数包含的质数因子个数是偶数，λ(n)=1；如果是奇数，λ(n)=-1。所有纯素数，它们的刘维尔值绝对都是-1。
2018年，有人在MathOverflow上提出一个弱化版猜想：对于每一个大于2的偶数N，是否总能找到两个正整数a和b，使得N=a+b，并且λ(a)=λ(b)=-1。如果经典哥德巴赫猜想是对的，那么这个刘维尔猜想也绝对是对的。但数学家们放宽了条件：加数不一定非得是纯素数，只要它的质因子个数是奇数就行。
2024年，数学家Alexander P. Mangerel取得了突破，证明了对于所有足够大的偶数，这个猜想成立。但他的证明带着两个枷锁：一是只覆盖足够大的偶数，不包括较小的偶数；二是严重依赖于广义黎曼猜想。
Astra和Captain Sude的团队，直接把这两个枷锁都突破了。
Astra丢出的第一份证明只有两页纸。在这份精悍的论文中，Astra宣布：无需广义黎曼猜想，可以无条件证明所有能被4整除的正整数，都可以表示为两个刘维尔值为-1的正整数之和。它巧妙地利用了Mangerel论文中的一个无条件相关性界限，结合一个极其精妙的下降法，通过反证法推导出矛盾。
仅仅一天后，Astra又找到了一条全新的初等证明路线，直接把结果推广到了全部大于2的偶数。核心主张是：没有任何充分大的限制，没有有限例外集，所有偶数，无条件成立。
证明思路让人拍案叫绝。它没有暴力穷举，也没有靠把以前的解析估计压缩得更紧，而是玩了一步漂亮的结构转化：寻找替罪羊、逼迫现出原形、利用可交换性质让两条路径互相抵消、向全局传染、最后用二次剩余制造矛盾。一开始分解不存在的假设被彻底粉碎。
这一次，Astra同时提交了Lean 4的完整形式化验证。通过Lean 4验证，就意味着逻辑上绝对正确。知乎上UP主对Astra开源的v1.0.0版本进行了独立复核，结果令人震撼：Lean证明可以完美重新编译，最终定理与论文主张完全一致，代码里没有任何sorry，没有乱造的自定义数学公理，249个偶数的数值冒烟测试全部通过。
必须严谨地说：经典哥德巴赫猜想还没有被彻底解决。目前解决的是哥德巴赫猜想的刘维尔弱化版本。从质因数个数为奇数的合数跨越到纯正的质数，中间仍然隔着天堑。
但这绝不意味着这次突破不伟大。在纯数学意义上，它为整个数论搭起了一座打通乘法积木与加法组合的宏伟桥梁。这可能就是未来攻克原版哥德巴赫猜想的核心钥匙。
在AI意义上，这是一个历史性的奇点时刻。一直以来，我们认为AI擅长的是海量记忆和暴力计算。但这一次，Astra展现出了惊人的数学直觉和品味。它像一位极具天赋的数学家，写出一篇让人类数学家直呼优雅的证明。
