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

腾讯混元科研智能体 Hyra 攻克加法组合学 50 年未解难题 这条更新来自 ithome.com，发布时间为 2026-07-31，Aioga 保留原文入口以便核验。

摘要：腾讯混元基于 Hy3 模型的科研智能体 Hyra 为加法组合学中悬而未决半个多世纪的开放问题给出完整答案，证明 2 是该问题指数的上确界。Hyra 经约 24 小时运行提出核心思路，将最好结果从约 1.14 提高到 1.21，并给出显式构造、论文预印本及 Lean 4 形式化证明。

背景：材料将问题表述为有限整数集合的和集与差集规模关系，并追问经典不等式中的指数 2 是否可被任意逼近。正文称，该问题已悬而未决半个多世纪，既有构造曾逐步提高相关数值。

Aioga 观察：Aioga 判断，这一消息的核心价值不只在于数值改进，而在于其宣称同时提供构造、论文预印本和 Lean 4 形式化证明。值得关注的是，材料中的结论主要来自腾讯混元公告及 IT之家报道，仍应以论文与证明的独立核验为准。

影响与后续：若预印本论证和形式化证明经数学界审阅确认，这将为 AI 参与研究级数学探索提供一个可复查案例。材料也显示，AI 辅助搜索已被用于推进该类构造问题，但不能据此推断其已具备普遍解决开放数学问题的能力。 后续应重点核对预印本中的定理陈述、显式构造与指数上确界证明是否一致，并审阅公开的 Lean 4 代码能否复现。还应关注同行评议、研究者复核以及对“完整答案”范围的进一步说明。

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

论文： https://arxiv.org/abs/2607.27199 ：https://arxiv.org/abs/2607.27199

Lean 形式化证明： https://github.com/linhaowei1/sum-diff-proof ：https://github.com/linhaowei1/sum-diff-proof

先取一个至少包含两个元素的有限整数集合，记作 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 形式化证明。