知识卡片：腾讯新推出的Hyra智能体攻克加法组合学五十年未解难题

英文标题：待核实
英文关键词：Hyra; AI agent; additive combinatorics; Lean 4（基于内容提炼，原文未明确列出）
原始来源：腾讯研究院AI速递 20260803（https://m.sohu.com/a/1057954093_455313）

一句话结论

腾讯基于开源Hy3模型的科研智能体Hyra，为加法组合学中悬置半个多世纪的和差集问题给出完整答案，并公开了论文预印本、显式构造及Lean 4形式化证明。

事件概述或研究问题

• 研究问题：加法组合学中的“和差集问题”，该问题已悬置半个多世纪。
• 事件概述：腾讯科研智能体Hyra运行约24小时，提出核心构造，证明相关上确界确为2。

方法/产品要点

• Hyra基于开源Hy3模型构建，定位为科研智能体。
• 运行约24小时提出核心构造。
• 利用十二进制结构与中国剩余定理完成证明。
• 成果并非暴力搜索。
• 论文预印本、显式构造及Lean 4形式化证明均已公开。

主要结果或产业意义

• 为五十年未解的和差集问题给出完整答案。
• 公开可验证的形式化证明，便于学界检验和复现。
• 表明AI智能体在纯数学前沿能够提出核心构造，而非仅靠穷举搜索。

为什么重要

• 这是科研智能体在纯数学领域的重要进展，区别于已有卡片中SIMA 2的3D具身代理、Together编码智能体的推理性能优化，以及Cursor Design Mode的UI修改代理。
• 增量信息：本条展示了agent从辅助编码、操作界面走向独立提出数学构造，并以Lean 4形式化证明公开，增强了结果的可验证性。

局限与不确定性

• 材料为摘要信息，未提供Hyra的模型参数量、具体训练方式、运行环境及完整推理流程，待核实。
• 未提供论文预印本链接及同行评审状态，待核实。
• 和差集问题的具体数学定义、“上确界确为2”的详细含义以及此前研究脉络，待核实。
• 英文标题在原文中未明确给出，待核实。

可用于图书/PPT/简报的角度

• AI科研智能体在数学难题上的突破：从暴力搜索到结构构造。
• 形式化证明在AI可验证性中的作用。
• 中国科技企业参与基础数学研究的AI应用案例。

与既有脉络的关系

• 已有相关卡片覆盖了SIMA 2（虚拟3D世界AI代理）、Together推理引擎（编码智能体推理性能）和Cursor Design Mode（UI代理交互）。本条Hyra属于“AI代理做数学研究”的新分支，体现agent应用场景从软件工程、具身交互向科学发现延伸。