ARTICLE · 1054570
AI证明了Liouville版哥德巴赫猜想后,有什么现实风险?
数学突破很容易引发这样的联想。毕竟，证明一道难题，似乎比写文章、画图片更接近我们心目中的“智慧”。
但从一道证明，直接跳到机器觉醒，中间省略了太多问题。
最近受到关注的“刘维尔版哥德巴赫猜想”，提供了一个具体案例。CaptainSude 公开的项目给出了论文、Lean 形式化代码和验证记录；知乎答主 SUNNY99 也报告，自己独立重新编译了固定版本，并检查了最终定理与公理依赖。
与其停留在“AI真厉害”，不如看看：这份证明为什么能够走通，AI又可能怎样参与找到这条路线？
下面的引用模块保留少量数学细节，不喜欢公式的读者可以直接跳过。
一、它不是经典哥德巴赫猜想
经典哥德巴赫猜想要求：每个大于二的偶数，都能写成两个素数之和。
刘维尔版本放宽了条件。
把一个数拆成素数相乘，再数一数用了多少个素因子，重复的也算。比如，八由三个二相乘得到，十二由两个二和一个三相乘得到，都是三个素因子。
现在给数字贴标签：
奇数个素因子，贴红色。 偶数个素因子，贴蓝色。
所有素数都是红色，但八、十二这样的合数也属于红色。新问题变成：
每个大于二的偶数，能不能拆成两个红色的正整数相加？
数学模块一｜准确的定义
记素因子总数为 ，重复因子计入总数。刘维尔函数定义为：
要证明的是：对每个大于二的偶数 ，存在正整数 ，满足：
一没有素因子，按零个计算，属于蓝色。
这个问题是经典哥德巴赫猜想的一个弱化版本，但不是通常所说的“弱哥德巴赫猜想”，后者研究三个素数之和。
可选的数更多了，问题却没有自动解决。要保证所有偶数都能拆分，不能只靠检查大量例子。
按照仓库论文对前人工作的梳理，Mangerel 的一项无条件结果，保证了某些同号、异号搭配的存在，却没有保证同号搭配一定是两个负号；另一项直接针对所需负号搭配的“充分大”结果，则依赖广义黎曼猜想。
这份新论文要完成的，是不依赖这类猜想，也不留下“充分大”的门槛。
二、第一步：不急着找答案，先换一个问题
这份证明先研究了一个看似相反的问题：
一个大于三的素数，它的两倍，能不能拆成两个蓝色数？
最后需要红色，为什么先找蓝色？
因为颜色可以通过乘法转换。一个数乘以二或三，就多了一个素因子，颜色随之翻转。一对蓝色数经过适当放大，就可能变成所需的红色数。
这个缩放观察已经由 Thomas Bloom 在原始讨论中提出，论文明确承认了它的来源。
这里值得理解的AI思路，是寻找辅助问题：暂时不碰最难的目标，先找到一个更容易控制、又能通向目标的命题。
大模型在训练中学习了大量定理关系和证明模式，因此可能提出“换一个对象”“改变条件”“先证辅助命题”等候选步骤。结合文献和检查工具，这些路线还能进一步筛选。
不过，最终论文不是完整研究日志。本文对 AI 思路的解释，是说明这类系统可能怎样工作，并非还原 Astra 每一步的实际发现过程。
三、第二步：假设没有答案，看看会发生什么
证明采用反证法。
假设某个数就是不能拆成两个蓝色数，那么所有加起来得到它的数对，都不能同时是蓝色。
这条限制可以继续传递：知道一个数的颜色，就可能约束另一个；再结合乘以二、三时的颜色翻转，越来越多的位置被迫遵守严格规则。
这里的转向是：不再逐个寻找答案，而是追查“没有答案”会造成什么后果。
对证明搜索来说，这很重要。直接寻找两个加数，可能毫无头绪；否定它们的存在，却会给所有候选加上一条共同限制。
这不是靠大量试数碰运气，而是在改变问题的表达方式，让原本隐藏的约束显露出来。
四、第三步：专门研究“不合规则的地方”
接下来，证明只看数字除以那个素数后的余数。
可以借钟表理解：走过一圈，会回到同一个刻度。不同整数也可能因为余数相同，落在同一个位置。
论文保留一段小整数的原始颜色，再为整个余数系统构造新标记。某些乘法规律已经成立，剩下少数位置可能有偏差。
证明没有硬算所有位置，而是把偏差单独记录下来，研究它只能出现在哪里。
这是一种有用的搜索策略：不直接证明“处处正确”，先弄清“如果不正确，能错在哪里”。
然后，乘法交换律派上了用场：先乘负二再乘负三，与交换顺序之后，必须到达同一个位置。两条路线的变化必须一致。
再结合此前得到的范围和方向限制，所有偏差最终都被排除。
数学模块二｜交换律如何参与证明
用 表示余数系统上的新标记，定义两种偏差：
两个乘法变换可交换，因此：
这条关系必须与偏差的区间限制一起使用，才能推出偏差全部为零。交换律本身并不足以完成证明。
这段论证并非所有思想都由 AI 首创。论文明确指出，Mangerel 的工作已经包含从缺失的加法搭配推导严格乘法结构的策略，也出现了可交换变换的偏差论证。
AI参与数学研究的价值，可以是把已有工具接成一条此前未完成的路线，而不必是凭空创造所有工具。
五、第四步：把规则推到底，直到出现矛盾
消除偏差后，证明再用下降法，将局部乘法规律推广到整个余数系统。
基本想法是：假如还有障碍，就选最小的一个，再借助足够小的代表，把它带回已经能够处理的范围，最后说明这个障碍也不成立。
到这里，新标记被迫遵守严格的乘法规则。于是，所有非零平方的位置都必须是蓝色。
但利用二次互反律，证明可以找到一个小素数：它与某个平方落在同一个余数位置，同时又保留着素数原来的红色标签。
同一个位置，必须既蓝又红。矛盾出现了。
最后一步的思路，是把假设逼出的规则，与对象已经确定的性质正面对照。两者无法兼容，最初的假设就必须放弃。
随后通过缩放和少数基本拆分，便能覆盖所有大于二的偶数。
数学模块三｜矛盾在哪里
新标记的乘法性要求：
证明找到一个小素数 ，它在余数系统中是平方，因此应该满足：
但它又位于保留原始刘维尔值的范围内，而素数的刘维尔值为负一：
两种要求冲突，所以最初“不存在所需拆分”的假设不能成立。
这也解释了，为什么不能把成果直接搬到经典哥德巴赫猜想上。
整套论证依赖于一种性质：知道两个数的颜色，就能确定乘积的颜色。素数没有这样的规则，两个素数相乘，得到的反而是合数。
把“红色数”换回“素数”，证明不能照搬。
六、这算推理，还是只是在做计算？
这两件事并不矛盾。
大模型通过数值运算，根据上下文逐步生成内容。这说明它如何运行，却不能单凭这一点判断输出有没有推理价值。
一段文字可能只是看起来像证明，也可能真的构成有效证明。区别在于：每个步骤是否成立，条件有没有漏掉，结论是否确实由前提推出。
AI可以提出候选路线，形式化检查则约束“哪些路线真的成立”。
Lean 的意义正在这里。它不需要相信模型聪明，只按规则检查形式化证明。当然，还必须核对：代码中的定理，是否确实对应原来的数学问题。
至于“只给 AI 1900年以前的知识，它能否独立发现相对论”，这次工作并没有回答。要检验这个问题，必须排除训练材料中的答案泄漏，也不能提前提示后来的关键结论。
完成一个明确目标的证明，与自主发现值得研究的问题、选择实验、建立新的物理解释，并不是同一项测试。
我们可以承认这份数学产物的价值，同时不把它扩大成对意识、独立意志或全部科学能力的认证。
七、AI的风险，不需要等到“觉醒”才会出现
从参与一道证明，到拥有自己的意志，再到必然毁灭人类，并没有充分依据。
现实中的风险，要具体得多。
1. 把流畅的回答误当成可靠的判断
模型可能给出错误信息，却表达得完整而自信。在医疗、法律和公共决策中，往往没有一个类似 Lean 的检查器，能自动判断全部答案。
表达流畅，不代表判断可靠。用户越依赖它，就越需要知道它何时可能出错。
2. 让错误获得直接行动的权限
一个只能提出建议的模型，与一个能够转账、删除文件、修改生产系统的模型，后果完全不同。
连续自动执行还可能让一次误判成为后续操作的前提。
权限越大、执行越快，错误造成的损失就可能越大。敏感操作需要授权，关键步骤需要确认，系统需要日志、停止机制和回滚能力。
3. 降低诈骗、攻击和操纵的成本
伪造声音、批量编写诈骗话术、制造虚假内容，都不需要机器拥有恶意。
人类使用者已经有动机，AI可能让他们更便宜、更大规模地行动。
4. 把决策交给系统，却不愿承担责任
为了降低成本而仓促部署，出事后又归咎于“算法自动生成”，会让收益与责任脱节。
谁批准上线、谁检查结果、谁有权叫停、损失由谁承担，都必须说清楚。
模型的可靠性、工程上的权限边界，以及制度上的责任约束，需要一起考虑。
这份数学工作的可取之处，是公开了论文、代码和验证材料，让其他人有机会检查结论。现实应用同样需要这种可检查性，只是还要检查它做过什么、能影响谁，以及出错后如何补救。
需要防范的，不是想象中的“机器突然产生仇恨”，而是不可靠的判断被赋予过大的权力，以及掌握这种权力的人缺乏约束。
资料来源
项目与论文：CaptainSude / Liouville-Goldbach https://github.com/CaptainSude/Liouville-Goldbach
数学证明提纲：lean/PROOF.md https://github.com/CaptainSude/Liouville-Goldbach/blob/main/lean/PROOF.md
最终 Lean 定理：lean/LiouvilleGoldbach/Main.lean https://github.com/CaptainSude/Liouville-Goldbach/blob/main/lean/LiouvilleGoldbach/Main.lean
仓库验证记录：lean/verification.json https://github.com/CaptainSude/Liouville-Goldbach/blob/main/lean/verification.json
SUNNY99 的分析与独立复核报告 https://www.zhihu.com/question/2083895373177931200/answer/2084099614551102975
资料核对说明：本文核对了仓库原始论文、证明提纲、最终定理和所附验证记录，未自行重新编译 Lean。数学模块压缩了技术细节，完整论证以原文为准。