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

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

精选理由

腾讯混元的 Hyra 跑了24小时就证出加法组合学50年难题,还公开了 Lean 证明,比此前 AI 辅助搜索明显更进一步。

AI 摘要

腾讯混元科研智能体 Hyra 为加法组合学中一个悬而未决 50 多年的问题给出完整答案:证明和集与差集扩张指数的最优上确界是 2。此前最佳构造纪录从 1969 年的 1.0290 提升到 2013 年的 1.1259,近一年 AI 辅助搜索达到 1.1449,内部实验中 Codex(GPT-5.5)达到 1.2851。Hyra 用约 24 小时提出基于十二进制数字结构、循环群对称加法基与中国剩余定理的显式构造,使指数可以任意逼近 2。论文预印本和 Lean 4 形式化证明均已公开。

原文 · IT之家

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

IT之家 7 月 31 日消息,腾讯混元今日发文宣布,科研智能体 Hyra 找到了一个关键构造, 为加法组合学中一个悬而未决半个多世纪的开放问题给出了完整答案 。 目前,论文预印本、显式构造和形式化证明均已公开: 论文: https://arxiv.org/abs/2607.27199 Lean 形式化证明: https://github.com/linhaowei1/sum-diff-proof IT之家附该问题如下: 先取一个至少包含两个元素的有限整数集合,记作  A。把其中任意两个元素相加,收集所有不同的结果,得到“和集” (A+A);把任意两个元素相减,收集所有不同的结果,得到“差集” (A-A)。 由于重复结果只计算一次,一个自然的问题是:经过加法和减法之后,这个集合分别会扩张多少? 数学家用两个量来衡量这种扩张: 前者是和集的扩张倍数,后者是差集的扩张倍数。经典的和差集不等式告诉我们: 为了衡量这个指数,可以定义 于是经典不等式给出 。真正的问题是: 2 只是一个宽松的上界,还是能够被任意逼近的最优指数 ? 半个多世纪以来,数学家不断构造新的集合,试图让 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 形式化证明。

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