GPT-6 Astra取得哥德巴赫猜想重大突破，这一突破含金量有多高？数学家会被AI取代吗？

2026年9月17日，项目作者Captain Sude在X平台上宣布，GPT-6 Astra无条件证明了哥德巴赫猜想的刘维尔弱化版本，相关2026年9月16日验证记录显示证明已通过Lean 4形式化验证。该结论覆盖所有大于2的偶数，无需依赖广义黎曼猜想。这一突破含金量有多高？数学家会被AI取代吗？

GPT-6 Astra这次拿到的结果，是数论领域一次很漂亮的阶段性胜利，但绝对不等于哥德巴赫猜想被拿下。

网上很多标题直接喊出AI攻破百年猜想，属于把一个精妙的替身结果，包装成皇冠本身。

这个刘维尔弱形式猜想到底是什么？

很多人第一眼会把它和原版哥德巴赫猜想混为一谈，二者的差距，是概念上的关键门槛。原版猜想的要求，是任何大于2的偶数，都可以拆成两个素数相加。而刘维尔函数版本，只是把素数替换成了满足特定条件的整数。

刘维尔函数λ(n)的规则很简单，统计一个数字全部质因子的总个数，个数是奇数，λ值等于负一，偶数则等于一。素数天然只有一个质因子，所以素数的λ值必然是负一。可反过来，λ等于负一的数字不一定是素数，像数字8，拆解质因子是2乘2乘2，一共三个质因子，它的λ同样等于负一，但8是合数。

2018年这个类哥德巴赫问题被正式提出，它只要求大于2的偶数，能够写成两个λ等于负一的数字之和。原版猜想如果成立，这个弱形式自然成立，但弱形式成立，完全推不出原版猜想的结论。

在此之前，数学家Mangerel在2024年给出了当时最优的成果，只能在广义黎曼猜想成立的前提之下，证明足够大的偶数满足条件。这个证明有两个硬限制，依赖尚未证实的猜想，同时无法覆盖全部偶数。

Astra直接拿掉了这两个枷锁，完成无条件证明，适用范围覆盖全部大于2的偶数。整篇证明只有两页，没有堆砌海量算力暴力检索，推理路径干净简练。这份证明被写成Lean4代码，通过形式化验证，独立复现编译时，代码内不存在sorry占位符，没有额外新增公理，机器会逐行核验每一步逻辑推导，只要编译通过，逻辑链条就不会存在人为疏漏。

这次突破含金量有多高？

含金量要分开来看，一层是数学本身，另一层是AI做数学这件事。

单看数学结论，它算不上数论史上里程碑级别的大结果，只是解决了一个开放的弱猜想。但放在AI辅助数学的赛道，分量完全不一样。

过往大模型做数学，大多是检索已有论文，拼凑步骤，或是依靠大规模算力穷举试错。Astra这次，是自主找到一条人类之前没能想到的证明路线，选用Mangerel的无条件相关性界限，搭配下降法，依靠反证构建矛盾完成闭环。AI不再只是刷题工具，它开始独立寻找证明策略，挑选合适工具，串联起完整的逻辑链条。

Lean4验证这一环，是这次事件的点睛之处。人类数学家写出的论文，依旧存在逻辑漏洞、隐藏假设、笔误的可能性，同行评审只能做人工有限度检查。

形式化证明则是交给程序，从底层公理开始逐句核验，不存在理解偏差。这次AI直接产出可编译的形式化证明，打通了猜想发现到机器核验的整条链路。我觉得，这件事最大价值不在于搞定刘维尔猜想，而是验证了AI有能力产出可以被机器完整核验的原创数论证明。

数学家会被AI取代吗？

我认为不会，AI更像一个强悍的数学助理，而不是能顶替研究者的角色。

数学研究，从来不止是写出一段正确证明。真正的数学工作，包含提出猜想、判断方向、挑选值得研究的问题，看懂结论背后的深层含义，在不同分支之间建立联系。

这些环节依赖人的洞察力、审美和对整个学科脉络的理解。AI可以完成在固定问题框架内寻找证明路径的任务，但它不会凭空意识到，哪一类问题值得投入数年精力去攻坚。

就拿这次案例来讲，问题本身是人类数学家提出，由网友Captain Sude发起项目，AI负责寻找证明方案。AI擅长在给定目标下试出逻辑通路，却很难判断这个问题在整个数论版图里，到底占据什么位置。

菲尔兹奖得主群体此前联名发出提醒，他们担心企业拿攻克难题当成大模型营销指标，会扭曲数学研究的节奏，但他们同样承认AI具备加速数学探索的潜力。AI可以帮数学家快速试错，筛选无效思路，完成繁琐的形式化编码，省下大量重复劳动。

人类数学家的核心价值，是提问，是洞察，是把零散结论编织成理论体系。AI负责在划定的范围内，快速挖掘逻辑链条。二者的分工，更像是探险家和测绘员，测绘员可以快速绘制路径，可往哪个方向出发，要寻找什么宝藏，依旧需要探险家来定。

AI离真正拿下原版哥德巴赫猜想还有多远？

依旧有不小的距离，不要因为这次弱版本的突破，就觉得原版猜想近在眼前。

刘维尔版本只是简化后的类比问题，放宽了核心约束。原版猜想要锁定素数，素数分布的规律，远比刘维尔函数的符号规律更加棘手。AI这次证明用到的工具，适配刘维尔函数的性质，没法直接平移到素数场景。就算未来AI持续产出更多经过Lean4验证的数论成果，它依旧要面对素数本身那层难以逾越的壁垒。

AI的优势是组合逻辑，寻找短证明，可哥德巴赫猜想如果存在证明，其逻辑深度，大概率远超当前AI能够稳定驾驭的范围。模型可以生成看起来合理的文字推导，但面对超长篇的深层推理，幻觉陷阱依旧很难根除。形式化验证可以卡住错误，但前提是AI能先找到那条正确的证明路径。

往后数学圈会出现越来越多AI参与完成的证明，新的研究范式正在成型。AI不会抹掉数学家，它会改变数学家每天的工作内容，把大量时间从枯燥的推导校验中释放，用来思考更深层的问题。

未来数论领域，更多猜想的证明，会变成人和AI协同完成的产物。至于哥德巴赫猜想最终花落谁家，没人能给出确定时间表，但可以确定，就算哪天完整证明出现，解读它，理解它背后全新数学思想的，依旧是人。