GPT-6 Astra 攻克类哥德巴赫猜想：Lean 形式化验证已全部通过

数学家们大概是全世界对 AI 幻觉最没有耐心的群体，毕竟推导里只要错了一个符号，整座大厦就会跟着坍塌。但如果把推导过程直接扔进严格的机器证明系统里跑一遍，事情就不一样了。

研究者 Captain Sude 在 GitHub 上公开了一个数学项目，宣布借助 GPT-6 Astra 成功攻克了一项关于刘维尔函数（Liouville function）的类哥德巴赫猜想。更关键的是，整套证明已经完全写成了 Lean 4 代码，并通过了严格的形式化机器验证。

把偶数拆成两个奇数质因子的数

很多人都知道著名的哥德巴赫猜想：任何大于 2 的偶数，都可以写成两个质数之和。质数本身只有它自己一个质因子，数量正好是 1，也就是奇数个。

这次被证明的问题，其实是哥德巴赫猜想的一个著名近亲。在数论中，刘维尔函数 $\lambda(n)$ 用来标记一个正整数包含多少个质因子。如果把重数也算进去，质因子总数是奇数，函数值就等于 -1；如果是偶数，函数值就是 1。

这次证明的核心定理是：每一个大于 2 的偶数，都能表示成两个刘维尔函数值都是 -1 的正整数相加。也就是说，$N = a + b$，且 $a$ 和 $b$ 的质因子个数都是奇数。

这个问题早在 2018 年 8 月就被用户 Pablo 提到了数学论坛 MathOverflow 上，数学家 Mangerel 的论文则将其归功于 Shusterman。此前数学界已经有了一些积累，包括 Bloom 的尺度观察，以及 Mangerel 的刚性和交换缺陷论证。

据项目介绍，GPT-6 Astra 给出的是一条初等证明路线，巧妙利用了两个交换对称性、一种下降法以及经典的二次互反律，最终把这块硬骨头啃了下来。

Lean 4 零漏洞把关，不给幻觉留退路

AI 做数学题最怕的是一本正经地胡说八道。但这次研究者没给它留任何钻空子的机会，而是把整套数学论证完整搬进了交互式定理证明器 Lean 4 里。

代码锁定了 Lean v4.34.0-rc2 和 mathlib 的特定提交版本。项目记录的本地构建、公理审计和证明路径审计全部显示通过。

根据公开的公理审计日志，最终定理只依赖了 Lean 语言核心内置的三条基础逻辑公理：命题外延性（propext）、经典选择公理（Classical.choice）和商健全性（Quot.sound）。

整套证明里没有任何写着「sorry」的未完工漏洞，也没有人为偷塞任何未经检验的额外数学假设。每一次提交还会通过 GitHub Actions 触发全新的自动构建和双重审计，确保每一步推理都坚如磐石。

为什么重要

我们认为，这项成果最亮眼的地方，在于它再次验证了大模型与形式化验证工具结合的巨大威力。

过去大模型参与数学研究，最让人头疼的就是人工验算的成本，往往需要顶尖数学家花上几个星期去挑刺和排查幻觉。现在借助 Lean 这样的定理证明器，AI 负责发散思维寻找巧妙的证明路径，机器内核负责像编译器一样死守逻辑防线。只要代码跑通、审计绿灯，整个数学界就能直接承认结论的正确性。

对于纯数学研究者来说，这套工作流正在从实验性玩具变成真正的生产力工具。它不仅能帮学者验证猜想，甚至能从以往数学家留下的半成品框架中，自己摸索出一条兼顾下降法与互反律的初等路径。

从大模型的竞争格局来看，OpenAI 等前沿厂商把 Astra 级别的推理能力推向形式化定理证明，直接切中了逻辑推理的最硬核战场。比起写写营销文案或生成代码，这种能在严格公理系统里从头到尾走通长链条演绎的能力，才是通用人工智能迈向严谨科学研究的核心分水岭。