Các nhà nghiên cứu Trung Quốc đạt đột phá: tác tử AI mã nguồn mở 'Hyra' giải được bài toán khiến AlphaEvolve, GPT và Claude bó tay

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