中国研究者取得突破：开源AI智能体Hyra解决AlphaEvolve、GPT和Claude未能解决的数学难题

arXiv 上发布的一篇新预印本，题为《解决和集与差集关系中的最优指数问题》，作者为林浩伟（腾讯混元）和李珊达（卡内基梅隆大学），解决了加性组合学中一个核心问题，该问题曾难倒包括 Google DeepMind 的 AlphaEvolve、GPT 和 Claude 在内的领先人工智能系统。该问题涉及限制和集与差集增长率的比值，此前基于人工智能的研究仅达到约 1.14 的指数，但真正的上界被证明恰好是 2。这一突破源于研究人员允许人工智能代理 Hyra 用自然语言提出构造和证明草图，而非仅提供显式列表，从而得出了一个新颖的构造，随后通过人工验证和 Lean 4 形式化证明进行了确认。Hyra 是腾讯基于 Hy3 模型（一个以 Apache 2.0 协议发布的 295B 参数 MoE 模型）开发的开源研究代理，大约工作了一天，期间使用 GPT-5.6 Sol 作为评判者来引导搜索，但最终构造由人类独立检查。数学家 Thomas Bloom 以对人工智能声明进行严格审查而闻名，他验证了该结果，甚至重新表述了定理，并将作者列为“Lin, Li 和 Hyra”，从而承认了人工智能作为共同作者。尽管该预印本尚未经过同行评审，但机器验证的 Lean 证明与独立人工验证相结合，使其成为人工智能对数学的罕见且可信的贡献，尤其值得注意的是，这一成果来自开源模型，与之前的闭源模型成就形成对比。