AI 参与解开 57 年数学题，真正值钱的是验收
一张论文表格里，前一行还是 1969，后一行已经跳到 2026。
中间隔了 57 年。
问题属于加法组合数学，研究的是一组整数两两相加、两两相减后，能得到多少不同结果。这个方向看着离日常开发挺远，但新论文里出现了一套很熟悉的工程组合。
一个研究智能体负责找路，一个更强的模型负责给候选方案打分，人类研究者检查推导，收尾再把证明交给 Lean 4。
好家伙，数学研究被搭成了一条有测试、有评审、有验收的 Agent 流水线。
Haowei Lin 和 Shanda Li 的论文给出一族显式整数集合，把经典和集差集不等式中的最优通用指数钉在了 2。论文写得很克制，基于开源 Hy3 的研究智能体 Hyra 参与了构造和证明的开发，GPT-5.6 Sol 用于引导探索，还帮助把自然语言证明转成 Lean 4。
但论文没有把数学正确性扔给模型。
作者独立检查了构造和证明，修订表述，手工整理出自包含论证，并公开了形式化证明仓库。
这句话得先放在前面。不是 AI 独自关门算了一天，出来宣布自己解决了 57 年难题。更准确的画面是，AI 把搜索空间里一条极难看见的路挖了出来，人类沿着路重新走一遍，再让证明助手检查每一块石头有没有松。
我自己的判断是，这项工作的价值不只在答案。它把 AI 科研最可能先规模化的形状露出来了。
先被改写的，未必是公认最难的问题，而是那些答案能够被便宜、确定地验收的问题。
先把这道题翻译成人话
假设有个整数集合 (A)。
(A+A) 是从集合里任取两个数相加后得到的所有结果，(A-A) 则是两两相减的所有结果。数学家关心的是，这两个新集合相对原集合会膨胀多少。
论文把和集的膨胀倍数记作 (\sigma(A))，把差集的膨胀倍数记作 (\delta(A))。经典不等式给出一个边界，粗略理解就是，两边不会毫无约束地乱长，它们之间存在一个指数关系。
问题卡在这个指数还能不能继续收紧。
过去几十年，研究者不断找到更好的有限集合。1969 年的结果是 1.0290，1973 年推到 1.0598，2013 年的集合家族做到 1.1259。到了智能体时代，AlphaEvolve、LoongFlow、SimpleTES、OpenHands、OpenClaw、Codex、EvoMaster 全都下过场，公开结果大多还在 1.1 左右打转。
这很像跑 benchmark。
模型搜到一个更高的小数，大家鼓掌，然后下一轮继续卷。可这篇论文没有把 1.14 提成 1.15，它直接构造出一整个集合家族，让指标可以无限逼近 2，并证明 2 就是通用上界。
从找出一个更强样例，到解释为什么一整类构造都成立，中间不是多跑几张卡那么简单。前者像 fuzzing，不断变异输入，盯着分数往上爬。后者要从偶然结果里抽出结构，把结构写成任何人都能复查的证明。
这一下才真的有点子牛逼。
论文里的构造组合了十二进制数字装置、三状态进位自动机、循环群里的对称加法基，以及中国剩余定理。读不懂这些名词没关系，重点在于它不是一个只对某组数字有效的魔术，而是一台可以按参数 (K) 持续生成集合的机器。
每个正偶数 (K) 都对应一个显式集合 (A_K)。作者证明，(K) 越大，指标越靠近 2。
这才让「最好结果是多少」变成了「最优边界为什么就是它」。
24 小时不是最惊人的数字
论文披露的探索过程特别值得做 Agent 的人看。
早期系统会直接枚举有限集合，再计算每个集合的分数。问题也很直白，集合一大，内存和枚举成本就往上炸。暴力搜索可以把局部山头摸得很细，却很难看见山脉的形状。
团队于是允许 Hyra 用自然语言提出构造和论证，不再把行动空间锁死在一串 Python 整数列表里。
这一步相当于把 Agent 的输出从「候选答案」升级成「可执行假说」。
Hyra 基于腾讯开源的 Hy3 模型，在自主有限搜索轨迹里把最好结果从约 1.14 推到约 1.21。随后团队让 GPT-5.6 Sol 充当判断器，运行 Hyra 约 24 小时，得到论文的核心构造。
注意，论文专门划了一条线。
模型判断只负责引导探索，不负责认证数学正确性。
这跟生产里的 Agent 很像。让模型判断「哪个方向更有希望」，容错空间可以很大。它偶尔看走眼，最多浪费一轮搜索预算。让模型判断「这个证明一定正确」，错误成本完全换了一个量级。
很多 Agent 项目栽就栽在这里。规划器、执行器、验收器全是同一个模型，同一份上下文，同一种盲区。代码写完，它自己看一眼说棒棒的，然后把 bug 连着赞美一起交付。
论文没有这么干。
探索阶段可以用概率判断追求召回率，多捞一些怪想法。证明阶段换成人类独立检查，把自然语言里的跳步、含混和自信先清掉。形式化阶段再交给 Lean 4，把每一步变成机器能核验的对象。
这三层不是重复劳动，而是三种不同的错误模型。
探索器怕漏掉好路线，判断器怕把预算烧在烂路线，证明器怕一个微小跳步污染整条结论。把它们拆开，系统才有机会让错误在边界上暴露。
顺着这个思路回看Hyra 官方页面和腾讯对 Hy3 的公开介绍，模型参数反而不是这次最重要的部分。更关键的是，研究任务被改造成了能搜索、能比较、能回滚、能验收的工作流。
这玩意跟模型聪不聪明有关，但不只跟模型聪不聪明有关。
有裁判的赛道会先跑起来
论文表格里还有一个挺扎眼的细节。
AlphaEvolve 在 2025 年找到 1.1219，SimpleTES 在 2026 年做到 1.1449，几套 GPT-5.4 Agent 在同年 7 月跑出的结果大多也在 1.08 到 1.12。Hyra 的有限搜索先到 1.21，最终论文却不是再报一个更高的小数，而是用显式构造把上确界证明成 2。
前面的系统更像运动员，后面的系统终于把赛道图纸画了出来。
公开构造与智能体搜索结果，数据来自论文第三节。最终结果是上确界，不与有限样例的小数完全同类。
为什么是这类数学题先出现突破？
我不敢把一篇新论文说成科研范式已经改朝换代，但它有一个非常清楚的优势，候选答案能被层层验收。
有限集合可以直接算分。构造可以写成明确公式。证明可以由同行复查。关键步骤还能翻译成 Lean 4，让内核给出通过或失败。
探索空间很大，验收规则却足够硬。
这个组合太适合 Agent 了。
软件工程里也有同样的分界。给 Agent 一个有完整测试集、静态检查、类型系统、可复现构建的仓库，它可以大胆改。给它一份「把产品做得更高级」的需求，连高级是什么都没有定义，模型再强也只能猜老板心情。
科研任务也一样。
能写成损失函数的，先被搜索系统吃掉。能写成模拟器的，接着被自动实验吃掉。能写成形式化约束的，更容易把模型的大胆猜测和严格证明接起来。
那些真正开放、评价延迟很长、连同行都无法快速判断方向好坏的问题，依然难。不是因为模型没有灵感，而是系统没有一个足够便宜的裁判。
同一个模型不要同时当选手和终审裁判，分层之后，每一层只承担自己能被追责的判断。
所以这篇论文给做 Agent 的人留下的，不是「换 Hy3 就能破数学题」这种采购建议。
真正能抄的是架构。
先把任务改成可以批量产生候选，把低成本模型放在宽搜索层。再设计一个允许误判但能控制预算的判断器。候选一旦越过门槛，就切换到独立检查。收尾尽可能用测试、类型、形式化证明或可复现实验收口。
如果收尾一步只能让另一个大模型读一遍，说它看起来没问题，那还不叫验收，只叫第二意见。
当然，形式化证明也不是魔法。自然语言证明转成 Lean 代码时，规格写错、定理陈述偷换、遗漏现实假设，照样可能出现「证明全绿，问题答偏」。证明助手只能保证代码表达的命题被推出，不能替人决定那个命题是不是原本想问的事。
人类仍然要守住规格。
这份工作最让人兴奋的地方，恰好不是 AI 把人挤出了研究。论文里的分工很诚实，Hyra 扩大搜索，人类纠正与整理，Lean 4 守住局部正确性。每一方都没有假装自己包办全场。
57 年的问题被推进，不是因为终于来了一个不会犯错的天才。
是因为团队把犯错放在了可以被发现的地方。