深圳热线

腾讯混元:科研智能体Hyra攻克加法组合学50年未解难题

2026-07-31 16:26:36 来源:IT之家


(资料图片仅供参考)

IT之家 7 月 31 日消息,腾讯混元今日发文宣布,科研智能体 Hyra 找到了一个关键构造,为加法组合学中一个悬而未决半个多世纪的开放问题给出了完整答案。

目前,论文预印本、显式构造和形式化证明均已公开:

  • 论文:https://arxiv.org/abs/2607.27199
  • Lean 形式化证明:https://github.com/linhaowei1/sum-diff-proof

IT之家附该问题如下:

半个多世纪以来,数学家不断构造新的集合,试图让 C (A) 尽可能大。1969 年的早期构造达到约 1.0290,1973 年提高到 1.0598,2013 年的构造进一步达到 1.1259 。近一年来,多项 AI 辅助搜索将这一数值推进到 1.1449。在论文记录的一项内部探索实验中,Codex(GPT-5.5)配合人类引导又将它提高到 1.2851。

而 Hyra 与 Hy3 迈出了决定性的一步。它给出的是一族显式构造的有限整数集,满足

这意味着:无论给定一个多么接近 2 的目标,都能构造出相应的集合使指数超过它。因此,2 确实是这个问题的上确界。

此前,Georgiev、Gómez-Serrano、陶哲轩和 Wagner 等研究者曾借助 AlphaEvolve 优化搜索算法和候选集合。这类方法依赖对有限集合的显式枚举,随着规模增长,计算和内存成本会迅速上升,也难以自然过渡到可证明的渐近构造。

据介绍,腾讯混元首先用 Hyra 在有限搜索中将最好结果从约 1.14 提高到 1.21,随后转向用自然语言提出数学构造和论证。使用 LLM judge 为探索过程提供反馈。

经过约 24 小时运行,Hyra 提出了论文的核心思路:利用十二进制数字结构和一个精巧的构造控制差集,再结合循环群上的对称加法基与中国剩余定理,使和集以接近平方的速度扩张。官方独立检查并整理了完整证明,同时给出了 Lean 4 形式化证明。

关键词: 混元 加法 构造 差集 显式 腾讯 不等式

热门推荐