AI 把 32 年没动的拉姆齐数下界再推一步：ScaleAutoResearch-Ramsey 到底做对了什么
AI 把 32 年没动的拉姆齐数下界再推一步：ScaleAutoResearch-Ramsey 到底做对了什么
主要信源：https://github.com/ypwang61/ScaleAutoResearch-Ramsey 交叉验证：https://raw.githubusercontent.com/ypwang61/ScaleAutoResearch-Ramsey/main/r3_17_record_summarized.md ，https://raw.githubusercontent.com/ypwang61/ScaleAutoResearch-Ramsey/main/r4_15_record_summarized.md ，https://www.qbitai.com/2026/05/415031.html 事件日期：2026-05-10
速查卡
| 项目 | 内容 |
|---|---|
| 一句话总结 | 研究者用 Claude Code / Codex 驱动的大规模自主搜索框架，把 R(3,17) 下界从 92 推到 93，并把 R(4,15) 从 159 推到 160。 |
| 大白话版 | 这不是“AI 帮忙写个证明草稿”，而是让一群代码 Agent 持续改搜索程序、跑验证器、记录实验、跨分支继承最强中间结果，最后在经典组合数学问题里真的找到更好的构造。 |
| 核心数字 | R(3,17) ≥ 93 是 32 年来首次刷新；R(4,15) ≥ 160 超过 AlphaEvolve 的 159；R(3,17) 的关键近前沿状态从 12 冲突一路推进到 0，连续跨越 12 个台阶。 |
| 影响评级 | A — 不是单篇炫技案例，而是“多智能体自主科研 + 可靠程序验证”开始打进真正的开放数学前沿。 |
| 利益相关方 | 数学搜索研究者、AutoResearch/Agent 框架、AI for science 团队、组合优化与 SAT/局部搜索社区 |
事件全貌
发生了什么？
ScaleAutoResearch-Ramsey 是一个公开仓库，不是传统论文。它给出的核心交付物有三类：
- 新的 witness 文件：
R(3, 17) >= 93.txt与R(4, 15) >= 160.txt - 两份详细的实验记录：
r3_17_record_summarized.md与r4_15_record_summarized.md - 一个来自 AlphaEvolve 体系的验证 notebook
verify_bounds.ipynb
仓库作者 Yiping Wang 的做法很直接：把 Claude Code / Codex 放进一个 autoresearch 式 scaffold 里，让大量独立 agent 围绕同一问题反复试验。每个 agent 都拿着只读 verifier、程序骨架、记录文件和结果表持续迭代；表现好的分支会被别的分支继承或 fork，实验级别的“优胜劣汰”则通过 GitHub branch/记录来实现。
这件事值得认真对待的原因，不是它又找到了两个数字，而是它把“AI 做科研”从一句口号压成了一条可检查的流水线：候选构造 → 验证器检查 → 记录失败原因 → 改算法 → 扩宽/加深搜索 → 继承最强前沿。
时间线
- 1994-00-00 — Wang–Wang–Yan 给出
R(3,17) ≥ 92，之后 32 年未再前进 - 2026-03-00 — Google DeepMind AlphaEvolve 只追平
R(3,17) ≥ 92，并把R(4,15)推到159 - 2026-04-19 左右 —
R(3,17)主实验 run0419_cc_r3_s17_5启动 - 2026-04-22 / 04-27 —
R(4,15)搜索从初始 run 延续到apr27_codex_r4_s15_99 - 2026-05-10 — 量子位报道该结果；仓库已公开 witness 与 summarized records
- 当前 —
R(3,17)已继续探索n=93、R(4,15)已继续探索n=160
关键人物/项目说了什么？
仓库 README 的关键表述有三句，信息量很大：
- “New lower bound after 32 years:
R(3, 17) >= 93.” - “Another new lower bound:
R(4, 15) >= 160.” - “Method: Claude Code / Codex + simple autoresearch + scaling by width and depth.”
这三句话等于把这件事的核心摊开了：
- 目标不是写解释，而是找 witness
- 评判标准不是主观好坏，而是 verifier 是否通过
- 关键手段不是单个超级 agent，而是“大量独立 agent + 宽度和深度扩展”
技术解析
技术方案
先说数学对象本身。对 Ramsey 数 R(r,s)，如果你能构造一个 n 个顶点的图，使得：
- 图里没有
r-clique - 图里没有大小为
s的 independent set
那么就证明了：
所以问题被转成了“找一个合法图”。这类搜索的难点是：
- 搜索空间巨大
- 局部改一条边，可能同时破坏多个约束
- 靠纯随机或普通局部搜索很容易卡在局部最优
ScaleAutoResearch-Ramsey 不是去训练一个模型直接“猜答案”，而是围绕这个构造搜索过程做系统化自动研究。
其统一实验 scaffold 大致是：
只读 verifier
+ 初始程序/构造
+ program.md 风格研究指令
+ 机器可读 results.tsv
+ 人类可读 record.md / summarized record
+ 多个独立 agent 并行运行
+ 强分支被复制、继承、再扩展作者自己把方法概括成“scale width and depth”：
- width：同时跑很多独立 agent，增加探索多样性
- depth：对表现好的状态持续 fork、继续爬山、继续修复
这个设计极其关键，因为开放数学搜索的主要问题不是“没有一个聪明步子”，而是“单一路线太容易卡死”。
R(3,17)：为什么前半程全卡住，后半程突然连破 12 级？
仓库记录把 R(3,17) 的过程写得非常完整，几乎就是一篇“AI 自主研究失败学”。
第一阶段：传统三角自由（triangle-free）搜索全线卡死
最开始，系统沿着很自然的方向做：
- 从随机初始化出发
- 用各种 simulated annealing、k-swap、局部修补、Cayley graph 搜索
- 尝试扩展已有 Exoo 构造
- 做交叉、替换、ghost vertex 等变体
结果很统一：几乎所有方法都卡在 α = 18，而目标需要 α ≤ 16。这意味着搜索虽然离合法构造不算天文距离，但就是跨不过去。
记录里给出的一个非常重要的结论是：在 n=92 的 Cayley 图家族上，不管是 Z_92、D_46、Z_23 ⋊ Z_4 还是别的群结构，全部都卡在同一个地板 α=18。这说明不是参数没调好，而是这条结构性路线本身已经接近走到头。
第二阶段：范式切换——从“零三角”反过来做“零独立集冲突”
真正的突破来自“反着做”。
平行参考搜索先给出一个极强近前沿种子：在 n=92 上只有 12 个冲突，而且这 12 个冲突全部是三角形，没有 17-independent set 冲突。于是思路彻底反转：
- 不再从“完全 triangle-free，但 independent set 太大”的图出发
- 而是从“已经满足
α ≤ 16，但还有少量三角形”的图出发 - 然后通过
compound drop-repair去掉三角边，再补修因去边产生的新 independent-set 违例
这个思路的含义非常大：
- 之前的方法在一个极深的局部盆地里打转
- 新方法承认“短期内先变差也没关系”，允许临时 uphill
- 真正关键不是单步最优，而是多步链式修复
记录里最漂亮的洞察，是把 h_walk 和 compound_drop_repair 的差别说透了：
h_walk用的是绝对阈值keep_totalcompound_drop_repair用的是相对阈值keep_uphill
后者允许搜索短暂经过高冲突状态，再换来更低的新盆地。对于这种组合爆炸问题，这相当于从“贪心爬山”切到“可控翻山”。
R(3,17) 的关键推进链
| 阶段 | 状态 | 关键意义 |
|---|---|---|
| 传统 TF / Cayley 搜索 | 卡在 α=18 | 证明老路基本走不通 |
| 参考种子 | 12 冲突 | 首次把问题压到很近前沿 |
12 → 11 → 10 → 9 | 同日连破 | 新范式有效 |
9 → 8 | 5 步 compound 链 | 证明必须允许中途冲突暴涨 |
8 → 7 → 6 → 5 | magic-formula cdr | 参数组合出现稳定逃逸模式 |
5 → 4 → 3 → 2 → 1 → 0 | 短时间内连破 | 说明已进入连续可修复区间 |
| 最终结果 | R(3,17) ≥ 93 | 32 年来首次刷新 |
最终 witness 的性质也很漂亮：
- 92 个顶点
- 727 条边
α = 16- 0 triangle
- 度分布 min/max/avg = 15 / 16 / 15.80
它不是“瞎碰出来”的怪物，而是非常接近 16-regular 的精致构造。
R(4,15)：另一条路线说明“局部搜索 + SAT 诊断”同样重要
R(4,15) 的故事不完全一样，但更能说明这套方法论不是偶然。
一开始，搜索把 158 顶点的已知 witness 固定住，只搜索新增顶点的一行邻接关系。这条路先是很成功，从数百冲突一路压到 18，但随后 SAT 直接证明：
- 在冻结 158-vertex base 的条件下
- 想靠只调新顶点那一行做到 0 冲突
- 是 UNSAT
这一步特别硬。它不是“我感觉这条路不行”，而是把“不行”正式证明掉。于是整个 search family 被废弃，研究方向切到 full-graph exact-delta 搜索。
后续的关键转折包括：
- full-graph exact delta 不再冻结基图
- 用 verifier-consistent 的精确冲突增量
- 对 exact-6、exact-3、exact-1 等 plateau 做 SAT/CEGAR 诊断
- 最终引入 bounded uphill，跨过 exact-6 和 exact-1 的能障
最后旧分支 run_070_delta_uphill_exact3 被重新核验时，发现其实已经到 0，正式证明 R(4,15) ≥ 160。
这个故事说明两件事：
- Agent 不是胡乱试，而是在“搜索—证明不可行—换范式”之间迭代
- SAT/CEGAR 这种传统严肃工具，并没有被大模型取代，反而成了 Agent 研究链路的硬锚点
关键指标
| 指标 | 数值 | 对比 | 说明 |
|---|---|---|---|
R(3,17) 新下界 | 93 | 旧值 92 | 32 年来首次推进 |
R(4,15) 新下界 | 160 | AlphaEvolve 的 159 | 再向前推 1 |
R(3,17) 关键前沿 | 12 冲突 → 0 | 传统方法长期卡死 | 新范式连续突破 12 级 |
R(3,17) 最终边数 | 727 | Wang 91 顶点构造 728 边 | 更大规模下仍保持高质量结构 |
R(3,17) 最终平均度 | 15.80 | 近 16-regular | 结构并不杂乱 |
R(4,15) row-only 路线 | SAT 判 UNSAT | 非经验判断 | 精确证明单顶点扩展路走不通 |
与之前的区别
| 维度 | 之前主流路线 | 本次方法 | 为什么更强 |
|---|---|---|---|
| 研究主体 | 人手工设计/少量算法试验 | 大量自主 agent 并行 + 继承 | 宽度和多样性显著更高 |
| 搜索驱动 | 固定算法或单一路线 | 允许算法本身被 agent 改写 | 搜索器也在被研究 |
| 正确性保障 | 事后人工核查 | 每次都过只读 verifier | 减少“看起来进步，实际错了” |
| 失败处理 | 人类总结经验 | results.tsv + record 系统化记忆 | 可以跨分支复用失败教训 |
| 过局部最优 | 保守局部搜索 | bounded uphill / compound repair | 能跨能障而不是原地打转 |
产业影响链
[ScaleAutoResearch-Ramsey 成功]
├→ [AI agent 能做真实研究搜索] → [AutoResearch 范式可信度上升] → [更多数学/科学开问题尝试代理化]
├→ [程序验证器成为核心锚点] → [AI for science 更重视 verifier-first workflow]
└→ [宽度+深度扩展有效] → [多 agent 并行科研基础设施需求上升]谁受益？
- AutoResearch / AI for science 团队： 这给了一条非常具体的路线图——不是“让模型思考得更像科学家”，而是“让模型围绕 verifier 持续改程序、继承前沿状态”。
- 组合优化与 SAT 社区： 这类传统方法没有被替代，反而和 agent 形成更强互补。
- 开源 agent 工具链： Claude Code、Codex、autoresearch 风格 scaffold 的价值被实证放大。
谁受损？
- 纯 demo 式 AI 科研叙事： 以后再说“AI 帮科学家 brainstorm”，门槛被抬高了。因为这里已经拿出实打实的新 SOTA witness。
- 把大模型当纯文本机器的视角： 这次真正起作用的不是语言修辞，而是程序迭代、验证闭环和大规模实验管理。
对开发者/研究者的影响
最直接的启示是：如果你的问题有可编程 verifier，哪怕搜索空间巨大，agent 就有机会真正干活。关键不在“让模型一次猜中”，而在于：
- 给它只读判定器
- 让它写和改搜索程序
- 把失败路径记录下来
- 允许分支继承与并行探索
竞争格局变化
变化前
AlphaEvolve 把“LLM/agent + 搜索 + 形式验证”这条路线打响了，但外界仍可能认为：
- 它需要 DeepMind 级基础设施
- 可复制性不强
- 普通研究者很难靠开源工具复现类似成果
变化后
ScaleAutoResearch-Ramsey 给出的新事实是：
- 不必靠超大 GPU 集群
- 可以主要依赖代码 Agent、CPU 服务器、公开 verifier
- 关键是实验组织方式，而不是单点模型神力
这会让“AI 自动科研”的竞争重心，从“谁的模型更会讲 reasoning”往“谁的研究 scaffold 更强、谁更会管理多分支实验”转移。
预期各方反应
- DeepMind/AlphaEvolve 路线： 会更强调结构性 mutation、严格验证与科学问题模板化。
- 开源 agent 社区： 会更关注 results ledger、branch inheritance、实验回放这些基础设施。
- 学术界： 一部分人会开始认真把 agent 当搜索器和实验员，而不是写作助手。
历史脉络
把这件事放在更长时间线里，它属于“AI 从解释知识走向生成知识”的一小步，但这次不是模糊叙事，而是非常扎实的一步。
过去几年里，AI 在数学上的高光大多集中在：
- 辅助证明草稿
- 做题 benchmark
- 生成直觉解释
而 Ramsey 这类问题的价值在于，它几乎没有语义水分：
- 你要么给出合法图
- 要么给不出来
- verifier 一跑就知道
所以这里的成果尤其硬。它不是“像懂数学”，而是“真的把数学前沿往前推了一格”。
批判性分析
被忽略的风险
- 仍然是窄领域成功。 Ramsey 搜索非常适合 verifier-first 流程，但不代表所有数学领域都能照抄。
- 记录是仓库记录，不是同行评审论文。 虽然 witness 与 verifier 很硬，但更系统的方法学评估仍需外部复核。
- 工程运气成分仍存在。 哪个参数组被称为“magic formula”，说明经验调参与大量尝试仍不可避免。
乐观预期的合理性
乐观派说“AI 已经能做科研发现”，这次是站得住脚的，但要把句子说完整：
- 前提是问题有可编程验证器
- 前提是你愿意付出大规模并行搜索成本
- 前提是有好的实验记录与状态继承机制
悲观预期的合理性
悲观派会说“这只是 brute force 搜索，不算真正理解”。这话有一半对：
- 它确实不是像人类那样给出优雅新定理
- 但在构造型数学问题里，能稳定把搜索、验证和算法改写闭环起来，本身就是一种有效研究能力
如果一个系统能持续提出更好的算法、识别旧路线不通、切换范式、最终拿到新 witness，那你很难再把它贬成“只是自动枚举”。
独立观察
- 这次最值得学的，不是 Claude Code 或 Codex 谁更强，而是“验证器优先”的研究架构。
- 真正的创新可能不在模型本身，而在实验组织学：results.tsv、summarized record、branch inheritance 这些看似土味的东西，决定了系统是否能累积前沿。
- 这件事和 AdaMARP 这类“多 agent 分层协作”工作形成呼应：复杂任务已经越来越不适合交给单一大模型一口吃掉。
- 对动动最有价值的一句判断是：AI 科研现在最真实的突破口，不是让模型写更漂亮的解释，而是围绕 verifier 把“搜索—诊断—继承—再搜索”流水线做厚。