腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

2026年07月31日,19时32分43秒 科技新知 阅读 3 views 次

腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

智东西

作者 | 茄子

编辑 | 程茜

智东西7月31日消息,昨日,腾讯首席AI科学家姚顺雨转发腾讯混元的一篇论文并喊话:“Hy AI4S is hiring :)”,公开招募AI for Science方向人才。

腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

7月29日由腾讯混元科研智能体Hyra参与破解数学难题的论文发布在arXiv上。依托Hyra强大的推演与探索能力,腾讯研究团队取得关键进展,破解了加法组合学领域一道持续50余年的公开难题。

姚顺雨的评论区里,有位网友称,Hyra/Hy3的论文“太疯狂了”,用显式构造解决一个数十年未解的和集问题,完全没想到这会出现在一条招聘帖里。

腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

还有人畅想:“下一位菲尔兹奖得主会是AI吗?”

腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

值得注意的是,今天下午腾讯招聘平台也发布了由姚顺雨带队的AI Infra团队招聘的消息。

腾讯科研智能体攻破50年未解数学难题,姚顺雨喊话正在招人

7月21日,腾讯混元推出了科研智能体Hyra。它基于本月开源的Hy3模型,该模型总参数量为2950亿、激活参数量为210亿。Hyra在破解这道难题时承担的是自动化探索工作,并帮助研究者挖掘潜在数学构造思路。

Hyra先是通过搜索优化现有有限集合案例,之后进一步提出一套可无限拓展的参数化构造方案:依靠十二进制结构约束差集规模,结合循环群对称加法基与中国剩余定理,实现和集更快扩张。AI输出候选方向后,研究人员校验思路、推导完整严谨证明,并借助Lean4完成形式化验证。

这道加法组合学问题研究的是,整数集合经过加法和减法运算后,规模扩张之间到底存在怎样的关系。

比如,给定一个有限整数集合A,将集合中任意两个元素相加,并去除重复结果,可以得到“和集”A+A;同样,将任意两个元素相减,可以得到“差集”A-A。数学家长期关注的问题是:一个集合经过加法扩张后,和集规模能够增长多少?这种增长能力与差集扩张之间是否存在某种固定规律?

为了衡量这种扩张关系,数学家定义了两个指标。其中,σ(A)=|A+A|/|A|用于表示和集相对于原集合的扩张倍数,δ(A)=|A-A|/|A|表示差集扩张倍数,并进一步定义C(A)=logσ(A)/logδ(A),用来衡量和集扩张能力相对于差集扩张能力的比例。

已有数学理论证明,C(A)≤2。但过去50多年,数学家一直无法回答一个关键问题:2是否只是一个理论上的宽松上界,还是能够通过构造特殊集合无限逼近的最优结果?

围绕这一问题,数学界持续尝试寻找更接近2的集合构造。1969年,相关结果约为1.0290;1973年提升至1.0598;2013年进一步达到1.1259。近一年,AI辅助搜索开始参与这一问题的探索,将已有数值推进到1.1449。该论文还记录了一项内部实验,Codex(GPT-5.5)在人类引导下将这一数值进一步提升至1.2851。

但这些探索都存在一个限制:找到一个更优的集合,并不意味着找到了能够证明理论极限的方法。此前的结果更多是在不断刷新具体案例,而无法回答C(A)是否真的可以无限接近2。

Hyra的突破在于,它没有停留在寻找更优样本,而是进一步发现了一套可以推广的数学构造方法。

研究团队首先让Hyra进行有限集合搜索,将已有最好结果从约1.14提升至1.21。但随着集合规模扩大,暴力搜索面临计算量和内存限制,同时搜索结果也难以转化为严格的数学证明。

随后,团队让Hyra尝试自主提出数学构造和推理方案,并通过LLM judge对探索过程进行反馈。经过约24小时探索后,Hyra提出论文中的核心思路:利用十二进制数字结构控制差集规模,再结合循环群上的对称加法基与中国剩余定理,让和集规模实现接近平方级增长。

换句话说,Hyra找到的并不是一个“更大的答案”,而是一种可以不断扩展的构造规律。

基于这一方法,研究团队构造出一族有限整数集合AK,并证明随着参数K不断增加,C(AK)会无限接近2。这也意味着,数学家长期寻找的答案得到解决:2确实是该问题的理论上界,但不存在任何有限整数集合能够真正达到2。

这也不是一次简单的暴力搜索。研究团队最初让Hyra进行有限集合搜索,将最好结果从约1.14提高至1.21。但显式枚举会受到计算量和内存限制,也很难转化成可以严格证明的通用构造。

随后,研究团队对证明过程进行了人工检查和整理,并公开了Lean 4形式化证明。目前,该论文仍为arXiv预印本,尚未经过同行评议。

结语:AI不只寻找答案,也开始提出新方法

从推出Hyra,到用Hy3辅助解决50多年未解的数学问题,再到姚顺雨团队招人,腾讯混元正在把大模型能力延伸到科学发现领域。

此次工作更值得关注的地方,是AI从“搜索更好的答案”走向了“提出可以被证明的数学构造”。在AI提出思路、人类检查整理、形式化工具验证的协作模式下,AI4S正在成为大模型竞争的新战场。

相关链接:

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

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

Hyra:https://hy.tencent.ai/research/hyra

来源:腾讯混元、X

(来源:新浪科技)

标签:


用户登录