GPT-6 Astra 在数论领域取得一项可验证的进展。据网友 Captain Sude 公布，Astra 无条件证明了哥德巴赫猜想的一个弱化版本——刘维尔（Liouville）形式：对于所有大于 2 的偶数，都能找到两个刘维尔函数值为 -1 的正整数之和。该证明已通过 Lean 4 形式化验证，并被独立复核确认可完整重新编译。
要理解这项成果的分量，需要回到问题的源头。1742 年，哥德巴赫在给欧拉的信中提出：任一大于 2 的偶数都可写成两个素数之和。近三个世纪以来，从哈代、李特尔伍德到陈景润证明「1+2」，人类始终未能拿下「1+1」这颗明珠。素数分布过于诡异，直接强攻难以奏效。
于是数学家另辟蹊径，引入刘维尔函数 λ(n) 作为素数的「替身」：一个数含有的质因子个数为偶数时 λ(n)=1，为奇数时 λ(n)=-1。所有纯素数（2、3、5、7、11 等）的 λ 值都是 -1，但反过来不成立，比如 8、12 的 λ 值也是 -1。2018 年，数学论坛 MathOverflow 上有人提出弱化版猜想：对每个大于 2 的偶数 N，是否总能找到 a+b=N，且 λ(a)=λ(b)=-1。若经典哥德巴赫猜想成立，这一命题必然成立；但它放宽了条件，允许加数是质因子个数为奇数的合数，而非必须是纯素数。
放宽条件后，问题依然极难。其核心在于研究正负交替的符号在加法组合下是否互相抵消，这关乎打通数学中「乘法结构」与「加法组合」的桥梁。2024 年，数学家 Alexander P. Mangerel 在一篇论文中证明：对所有足够大的偶数，该猜想成立。但该证明带有两个限制：一是只覆盖「足够大」的偶数，不包含较小的情形；二是严重依赖广义黎曼猜想（GRH），只有在 GRH 成立的前提下结论才成立。
Astra 此次的突破正在于同时拆掉了这两道枷锁。它先给出了一份仅两页的 PDF，宣布无需广义黎曼猜想，即可无条件证明：所有能被 4 整除的正整数，都可表示为两个刘维尔值为 -1 的正整数之和。证明思路是反证法：假设存在一个不被 3 整除的奇数 m，使得在 4m 这个规模下不存在符合条件的拆分，再借助 Mangerel 论文中的一个无条件相关性界限，通过乘以 4 不改变刘维尔值、乘以 2 会翻转刘维尔值等性质，构造差值最小的一对加数，利用其与 3 的整除关系推出矛盾。整个推导只用初等代数，步骤简洁到高中生也能看懂。
据项目作者 Captain Sude 透露，Astra 在第一天证明「4 的倍数」情形后，第二天又找到一条全新的初等证明路线，把结果推广到全部大于 2 的偶数，且没有任何「充分大」限制、没有有限例外集。其证明采用「结构转化」而非暴力穷举：先证明对每个大于 3 的素数 p，都存在 2p=u+v 且 λ(u)=λ(v)=1；再把刘维尔函数延拓到有限域上定义函数 G，利用乘以 -2 与乘以 -3 的可交换性让两条路径互相抵消，消去局部缺陷；随后通过下降引理把局部乘法规则传播到整个有限域，迫使 G 成为全局严格的乘法对象；最后用二次互反律找到一个在有限域内是平方数、但本身是素数因而刘维尔值为 -1 的元素，导出 1=-1 的矛盾，从而推翻初始假设。
验证环节同样关键。Astra 同时提交了 Lean 4 的完整形式化验证。知乎用户 @SUNNY99 对 Astra 开源的 v1.0.0 版本做了独立复核，结果显示 Lean 证明可完美重新编译，最终定理与论文主张一致，代码中没有「sorry」（Lean 中代表未填补的漏洞），没有自定义数学公理，所有公理依赖正常，249 个偶数的数值冒烟测试全部通过。
需要严谨指出的是，这并不等于经典哥德巴赫猜想已被解决。目前拿下的是其刘维尔弱化版本，从「质因子个数为奇数的合数」跨越到「纯正素数」之间仍隔着天堑。但这项成果在两方面意义显著：在纯数学层面，它为「乘法结构」与「加法组合」之间搭起了一座桥梁，可能成为未来攻克原版猜想的钥匙；在 AI 层面，它展示出模型可以给出被形式化工具确认的优雅推理，而非仅靠算力或记忆取胜，这与以往 AI 在围棋、蛋白质折叠等任务上的表现路径明显不同。