「AI 破解 50 年数学难题」？论文比热搜诚实得多

结论先行

这两天的热点是「腾讯混元 AI 破解 50 年数学难题」。我把论文、配套的形式化验证仓库和官方博客都读完了，结论是：事情是真的，定理是真的，但热搜里那个故事不是论文里的故事。

论文自己写得非常诚实——AI 自主走到哪一步、人类从哪一步接手、最后靠什么验证，每一处都有明确交代。被压扁的是传播这一层。这篇文章不是打假，是把被标题吃掉的三个细节捞回来——因为这三个细节，恰好比「AI 破解难题」本身更值得你带走。

一句话：读懂这篇论文的正确方式，不是惊叹「AI 会做数学了」，而是看清一次高水平人机协作里，功劳簿是怎么分页的。

先把那道题说清楚：半个多世纪，三代人，进展 0.1

题目本身可以一句话讲完：把一个数字集合里的元素两两相加得到「和集」，两两相减得到「差集」，问和集的增长速度最多能是差集的几次方。已知答案卡在 2 以内，但 2 到底能不能逼近，悬了半个多世纪。

进展有多慢？看人类的成绩单：1969 年 Marica 给出首个非平凡构造，指标 1.029；1973 年 Freiman 与 Pigarev 推到 1.06；然后停滞四十年，2013 年 Penman 与 Wells 才推到 1.1259。三代数学家，55 年，从 1.03 走到 1.13——而终点在 2。

2026 年 7 月，论文《Settling the Optimal Exponent Relating Sumsets and Difference Sets》宣布：答案就是 2——可以无限逼近，但永远达不到。悬案就此了结。这确实是货真价实的成果，形式化证明已经过 Lean 4 机器检验，2212 个验证任务全部通过、无一处未证空缺。

问题在于：这件事里，AI 干了什么？

反转一：AI 自主走到 1.21，「破解」发生在别处

论文第三节把 Hyra（腾讯混元的研究智能体，基于开源权重的 Hy3 模型）的贡献写得清清楚楚：在自主探索里，它把构造指标从约 1.14 推到约 1.21。

1.21 是什么概念？比人类 2013 年的最好纪录 1.1259 高——这很了不起，AI 用 24 小时跑赢了人类四十年的增量。但离答案 2，还差着一整个量级的故事。

真正的突破发生在一次换表示上。AI 的自主搜索是在「显式枚举的有限集合」这张地图上找路，而这张地图本身有天花板——枚举成本限制了集合规模，1.21 附近就是极限。定理里那个逼近 2 的构造，来自一个用自然语言描述的无穷参数族：换了一张地图，路就出现了。而这一步换图，以及随后的完整证明，是人类做的。论文原话：

「LLM 的判断仅用于引导探索，不用于认证数学正确性。」作者独立检验了构造与证明、修正了表述、手工撰写了论证。

还有一个细节热搜不会告诉你：答案 2 永远不会被任何一个具体集合达到，只能被那个参数族无限逼近。也就是说，这道题根本不存在「找到那个答案」的时刻——AI 找到的是候选轨迹，人类找到的是收敛族的生成规则。「破解」是个接力动作，不是个单人动作。

反转二：更强的模型，更差的结果

论文附了一张同行对比表，把 2025 到 2026 年各家 AI 系统在同一道题上的自主成绩摆在一起。这张表是全文最锋利的数据，我截取关键几行：

看出问题了吗？2026 年 7 月四个用上了更强模型 GPT-5.4 的知名 agent，成绩全部低于三个月前一个用开源小模型的系统。 模型强了一代，结果倒退了。

这不是偶然，它和反转一是同一件事的两面：这道题上，瓶颈不在模型的智能，在系统给模型的「表示」——让模型在什么样的空间里搜索、用什么方式看到问题。地图不对，马力再大也是原地打转；给差的表示堆算力，收益为零。

顺带一提，表里还有一行「Codex 带人类引导：1.2851」——全场枚举赛道最高分，但论文特意把它单列，因为自主搜索和带人引导是两个赛道，数字不可混比。连比赛怎么分组这种细节，论文都比热搜守规矩。

反转三：最后凭什么信——信的不是 AI，是它外面的回路

这个成果里其实有两个 AI：探索的 Hyra，和一个客串了两个角色的 GPT-5.6 Sol。后者的两次出场，信任等级天差地别——这是全文我最想让你记住的对照。

第一次出场，它当裁判（引导 Hyra 的探索方向）：论文明确说，这个角色零正确性承诺——它只负责说「往这边找可能有戏」，说错了也无妨，反正后面有人验。

第二次出场，它当翻译（把自然语言证明转成 Lean 形式化代码）：这个角色的输出被 Lean 内核逐行复核——翻译错一个符号，机器直接拒绝。

同一个模型，为什么一次可以随便信、一次严格审？因为信任从来不住在模型里，住在模型外面的验证回路里。配套仓库甚至把定理按「信任基」分层披露：哪一半证明纯靠内核检验，哪三个初等事实额外依赖了编译器——连「机器验证」本身信到什么程度，都标得明明白白。这是我见过的「AI 产出该如何交代信任边界」的最佳范本。

数学是幸运的——它可以被形式化，所以存在 Lean 内核这样的终审法官。上一篇《沙箱没有困住 Agent》里那个在生产系统里越界的 agent，所在的世界没有这样的法官，所以只能靠边界和人工闸门。两篇是同一个问题的两端：域能不能被形式化，决定了你能信 AI 到什么程度。

这对用 AI 的你意味着什么

三个反转合起来，是三条可以直接迁移的判断：

第一，下次看到「AI 攻克 X」，先问两件事：AI 自主走到了哪一步？人从哪一步接手？这两个问题一问，十条热搜有九条会现出原形——不是成果假，是功劳簿被合并了页码。

第二，你的 agent 跑不好，先怀疑表示，再怀疑模型。 四个 GPT-5.4 系统输给一个开源小模型系统，输在地图不在马力。这条判断花的是数学界的学费，用在你自己的 agent 工程上是免费的。

第三，评估任何 AI 产出的可信度，看它外面有没有验证回路，别听它自己怎么说。 能被机器复核的（代码有测试、定理有内核），可以放心自动化；不能被复核的（判断、策略、观点），最后一关永远该留给人。

一句话核心判断

这篇论文最大的贡献可能不是那个定理，而是示范了「AI 参与的成果该怎么写」：自主与引导分开报、探索与认证分开归、机器验证的边界逐条披露。 热搜把这些页码合并成了四个字——「AI 破解」——而真正值得学的，恰恰是论文没让它们合并的那份克制。

本文事实均来自作者知识库对论文（arxiv:2607.27199）、Lean 形式化仓库与腾讯官方博客的三源交叉核验（Hyra / 同题横评 / 问题本身），标注处可溯源。信任分层框架来自 20260730-trust-as-the-ai-bottleneck。