导语：近日，社交平台 X 上一个名为 Captain Sude 的匿名账号引发数学圈关注。该账号称，GPT-6 Astra 已“无条件证明”哥德巴赫猜想的 Liouville 版本，并公开论文、Lean 代码与机器审计记录。需要指出的是，这并非经典哥德巴赫猜想本体，而是一个条件更宽松的弱化版本。
8 天连发 6 个证明，匿名账号成焦点
据原内容，从 9 月 7 日到 16 日，该账号 GitHub 上新增 12 个证明仓库；短短 8 天内，连续发布 6 个数学证明，包括 Stoneham 常数之和正规性、Copeland–Erdős 常数强正规性等长期悬置问题。随后，目标转向哥德巴赫猜想的 Liouville 版。
从有条件到无条件：两天拆掉两道限制
Liouville 函数 λ(n) 像只认单双的开关：n 的质因数个数为奇数记 -1，偶数记 1。2018 年，MathOverflow 上有问题提出：每个大于 2 的偶数 N，是否总能拆成 a+b，且 λ(a)=λ(b)=-1。2024 年，数学家 Alexander P. Mangerel 在广义黎曼猜想成立的前提下，证明所有充分大的偶数满足该猜想。Captain Sude 和 Astra 则分两天拆除两个限制：第一天处理 4 的倍数，用反证法与乘以 4 不改变 λ 值、乘以 2 翻转 λ 值的性质，撞上 Mangerel 论文中的已发表界限；第二天处理 4k+2 型偶数，将问题映射到有限域乘法结构，逼出局部缺陷，再以乘法可交换抹平缺陷，最终由二次剩余性质导出 1 等于 -1 的矛盾。
Lean 验证成匿名者入场券
宣布证明是一回事，让人信是另一回事。此次论文后附有 Lean 4 完整形式化验证。知乎 UP 主 @SUNNY99 对开源 v1.0.0 版本独立复核：代码可重新编译，最终定理与论文主张一致，没有一处 sorry，没有自造数学公理，249 个偶数的数值冒烟测试全部通过。Lean 验证证明的是，从公理出发每一步推导逻辑成立；它不判断重要性，但在匿名账号没有信用可抵押的现实里，机器可复核性成了入场券。
边际成本骤降，长尾问题被重新估值
比单个证明更值得注意的是打法：翻论文，找悬置开放问题，扔给 Astra，让它写出 Lean 形式化证明，跑通机器验证，传到 GitHub，然后找下一题。9 月 7 日到 16 日，该账号 GitHub 上多出 12 个证明仓库。单个问题成本是几个小时试错加一单 API 账单，换来的却可能是一个悬置 8 年开放问题的终结。VibeMathed 已追踪 721 个开放问题，494 个被标记为完全解决，155 个通过机器形式化验证，悬置时间累计 10650 年。数学论文末尾的 Open Problems，正在变成可执行待办清单。
判断题比证明题稀缺
这不等于数学家失业。回看供应链：选题来自 MathOverflow，关键不等式来自 Mangerel，验证依赖人类几十年构建的 Mathlib 库。问题、工具和裁判都是人类的，AI 交出的是执行。当猜想、解题、验证都能被机器排进流水线，人的位置在清单够不到的地方：提出问题，判断价值，把单次证明升级为可复用方法。原版哥德巴赫猜想仍未解决，这个弱形式突破能否成为通往它的钥匙，同样要人来判断。
数学竞赛的规则正在改写。赢家不再是解题最快的人，而是知道该解哪道题、以及解完说明什么的人。这一局，AI 解了题；判卷才刚刚开始。