腾讯混元 Hyra + 数学家林浩威/李善达:50 年加法组合学猜想最优指数被钉死在 2

2026 年 7 月 29 日,腾讯混元的研究智能体 Hyra 与卡内基梅隆大学/北大数学家林浩威、李善达合作,把加法组合学里悬了 57 年的一个问题彻底关上:有限整数集 A 的和集 |A+A| 与差集 |A-A| 之间的最优指数,就是 2。

这道题在问什么

先用人话说一下问题。

取一个有限整数集 A,做出两个导出集合:A+A(所有两两求和)、A-A(所有两两求差)。

1969 年,经典不等式给出了范围:

|A+A|^{1/2} ≤ |A-A| ≤ |A+A|^2

右边那个指数 2 早被证明是「顶到天花板」的。但左边那个指数 1/2,也就是问 C(A) = log σ(A) / log δ(A) 这个比值最大能到多少,50 多年没人能给出明确构造——之前最好的显式构造只能让 C(A) 略大于 1.1。

悬了 50 多年的问题是:C(A) 真的能逼近 2 吗?还是被某个未知上限挡在 1.x?

证明给的是什么

林浩威、李善达给出的显式构造 A_K(K 为正偶数)满足:

C(A_K) > 2K / (K+3)

当 K → ∞,这个下界趋近于 2。结合经典不等式的上界,这就是说最小指数 c(使得对所有有限整数集 A 都有 |A+A| ≤ |A-A|^c 成立)正好是 2。

构造用到四件套:12 进制数字 gadget、3 状态进位自动机、对称加法基、中国剩余定理乘积结构。完整证明附带 Lean 4 / Mathlib 形式化验证,跑了 2,212 次构建任务,所有核心定理的证明都通过了 no-sorry 检查。

Hyra 在其中做了什么

Hyra 是腾讯混元自研的「研究智能体」,底层是开源权重模型 Hy3。它的工作流是 SimpleTES 评估循环 + 自主搜索:

• 自动构造候选 A,跑 C(A) 评分,把分数最高的解反馈给自己做下一轮变异。
• 在林、李接手前,Hyra 已经把已知最佳自动搜索值从约 1.14 推到 1.21。
• 林、李基于 Hyra 给出的高 C 值候选做了手工精化,推导出闭式构造并补完证明。
• Lean 4 形式化本身也是混元团队跑出来的,确保「no-sorry」。

arXiv 论文(2607.27199)的致谢里点名了 Hyra 团队,作者署名是林浩威(腾讯混元 + CMU)和李善达(腾讯混元),论文发表在 arXiv 上。这不是「AI 单独完成的证明」,而是「AI 把搜索空间从 1.14 推到了 1.21,然后人类数学家封顶到 2」的协作模型。

为什么这件事值得专门写一篇

50 年悬而未决的纯数学问题被 AI 参与的显式构造证掉,这有几层意义:

1. 加法组合学第一次有了 AI 可信的入口。之前 AlphaEvolve、SimpleTES、EvoMaster 这类自动搜索工具都只能把记录推高到 1.14–1.28 区间,这次直接逼近理论上限,说明研究智能体+ Lean 形式化的链路已经能稳定做出可发表的成果。 2. 「AI 是工具,不是作者」的边界明确。arXiv 论文作者是数学家,Hyra 在致谢里。这给学术界一个可复制的样板:AI 把自动搜索能力做到极限,人类做证明闭合。 3. Lean 4 形式化不再是「加分项」,而是「必做项」。2212 次构建、no-sorry 验证,这种强度的形式化保障在 5 年前的 AI 数学项目里几乎不存在。 4. 腾讯混元在 AI for Math 的卡位清晰。AngelSpec 投机解码给中国 AI 推理补基础设施,Hyra 给中国 AI for Math 立一个事实标准。两件事相隔 24 小时落地,不是巧合。

几个需要打折扣的地方

• 同行评审尚未完成,目前是 arXiv 预印本;
• Hyra 没有独立完成证明,1.21 离 2 还差 0.79,这部分是数学家手工做的;
• 同样的指数问题在其它群(Z^n、有限域)上是否同样成立,这次没碰。

但作为「研究智能体能稳定推动纯数学前沿」的样本,这是 2026 年目前最有说服力的一例。Lean 形式化 + 自主搜索 + 人类封顶的三段式,可能成为 AI for Math 的标准流水线。

参考:

• arXiv 论文: https://arxiv.org/html/2607.27199v1
• Hyra 项目主页: https://hy.tencent.com/research/hyra
• 腾讯混元 X 公告: https://x.com/TencentHunyuan/status/2082655737541726636