9 月 21 日，新智元报道了一个足以写进数论编年史的消息：网友 Captain Sude 宣布，GPT-6 Astra 无条件证明了哥德巴赫猜想的刘维尔弱形式，不再依赖广义黎曼猜想这一前提。更关键的是，整套证明已通过 Lean 4 形式化验证，并有第三方独立复核确认可以完整重新编译。数学界悬了近三百年的那颗明珠，被 AI 咬下了实打实的一口。
替身文学：三百年的迂回战
1742 年，哥德巴赫在写给欧拉的信中提出：任一大于 2 的偶数都可以写成两个素数之和。从哈代、李特尔伍德到陈景润的「1+2」，人类始终没能跨过最后的「1+1」。难点众所周知：素数的分布太诡异，直接死磕行不通。
于是数学界玩起了「替身文学」。2018 年，有人在 MathOverflow 上提出了一个弱化版本：把加数从纯素数放宽为刘维尔函数值为 -1 的正整数，也就是质因子个数为奇数的数。这个版本与原猜想同向：如果经典哥德巴赫成立，刘维尔弱形式必然成立。可即便放宽到这个程度，问题依然难得离谱。直到 2024 年，数学家 Mangerel 才证明「所有足够大的偶数」满足该猜想，而且证明严重依赖广义黎曼猜想（GRH）这一未证前提。两个枷锁，一戴就是两年。
两页纸，48 小时
Astra 的证明只有两页 PDF。第一步，它先攻下「4 的倍数」情形：巧妙利用 Mangerel 论文中那条不依赖 GRH 的无条件相关性界限，结合一个精妙的下降法，用高中生都能看懂的反证法推导出矛盾。没有任何「充分大」的限制，无条件下成立。
更让人意外的是第二天。Astra 没有在原路上继续压缩估计，而是换了一条全新的初等路线，把结果直接推广到全部大于 2 的偶数：先证明每个大于 3 的素数 p 都能让 2p 分解为两个刘维尔值为 1 的正整数；再把刘维尔函数延拓到有限域上，利用「乘以 -2 再乘 -3 与次序无关」这一交换性质，让两条路径的缺陷互相抵消；最后靠下降引理把局部性质传染成全局乘法结构，用二次剩余制造出 1 等于 -1 的致命矛盾，假设崩塌，全偶数域无条件成立。整条路线没有暴力穷举，没有算力碾压，是把加法阻碍转化为乘法刚性的结构转化，人类数学家看后的评价是两个字：优雅。
Lean 4 过了，但别急着宣布猜想已死
这次的硬通货是形式化验证。Astra 同步提交了 Lean 4 完整证明，知乎 UP 主 SUNNY99 随即对开源的 v1.0.0 版本独立复核：Lean 证明完美重新编译，最终定理与论文主张一致，代码里没有任何代表未填坑的 sorry，没有私造的公理，249 个偶数的数值冒烟测试全部通过。这意味着至少在逻辑层面，这个结果挑不出毛病。
但必须严谨地说：被解决的是刘维尔弱形式。从「质因子个数为奇数的合数」跨越到「纯正的素数」，中间仍隔着天堑，经典的 1+1 依然高悬。要说这次突破的价值，它为整个数论搭起了一座打通乘法积木与加法组合的桥，这可能正是未来攻克原版猜想的核心钥匙。
写在最后
过去我们默认 AI 擅长的是海量记忆和暴力计算，下围棋、折蛋白质都算「大力出奇迹」。这一次不同，Astra 展现出的是数学直觉和品味，它写出了一篇让人类数学家直呼优雅的证明。对数学界，这是一座新桥；对 AI 行业，这可能是真正意义上的奇点时刻：机器第一次在人类智力的最高殿堂里，靠的不是算力，是审美。
配图说明：本文封面为 AI 生成图像。
参考：新智元《刚刚，GPT-6 Astra取得哥德巴赫猜想重大突破》报道，本文为基于公开信息的独立评述。