腾讯开源模型Hy3破解半世纪数学难题，完整证明已通过机器验证

腾讯混元的研究智能体 Hyra，使用自家的开源模型 Hy3，协助两名研究者解决了一个悬而未决 50 多年的组合数学问题。问题是：一个整数集合的「和集」，最多能比「差集」增长多快。数学界早已证明，相关指数不会超过 2，但一直不知道 2 是不是最优答案。Hyra 让 Hy3 先搜索具体集合，再尝试提出通用构造。约 24 小时后，AI 找到了论文最终采用的核心方案。研究者随后核对、修正并整理证明，GPT-5.6 Sol 协助转成 Lean 4 验证。最终论文证明，这个指数可以无限接近 2，所以上界 2 已经是最优答案。虽然 AI 没有包办整篇论文，但最关键的构造确实是 Hy3 找到的。[原文链接](动察 Beating)