10 个 Opus 5.5 智能体用 15 小时，交出一份比 Dijkstra 更快的算法与 289 个 Lean 证明文件

Vals AI 公布了一项成果：他们组织 10 个 Claude Opus 5.5 Agent 去挑战计算机专业本科阶段的经典算法 Dijkstra，并成功给出了一条更快的路径。

对学过计算机的人而言，Dijkstra 是一个近乎不可侵犯的名字。它是计算机科学的基石之一，几代顶尖科学家在它身上投入了无数精力，探索数十年，试图把它的性能压到极限。这类被反复研究过的「经典问题」，想再往前挪一步都极其困难。而且这并非把代码写得更优雅就能解决的工程问题，它要求从底层数学上给出证明：即便数据规模趋于无限，新算法确实更快。

沙盒里的 10 个智能体，733 条讨论记录

Vals AI 团队把 10 个 Opus 5.5 智能体放进同一个沙盒，它们可以在虚拟留言板上交流、互相挑错，甚至围绕某条技术路线争论起来。

15 小时后，留言板上留下了 733 条讨论记录。

15 小时后，它们交卷了：一个名为 C-HD 的全新算法，外加 289 个文件的 Lean 形式化证明，直接交给 Lean Kernel 做机器验证，一次通过。

算法圈随即被搅动。有人发问：「过去要人类花几年去试错的研究，如今被 Agent 在半天内并行做出来了？」

Dijkstra 站在算法神坛上

Dijkstra 算法处理的是一个既简单又核心的问题。

给定一个图，其中包含若干顶点以及连接它们的有向边，每条边带一个非负实数权重。从某个起点出发，需要求出通往图中其余每个顶点的最小总权重路径，或者判定其不可达。

所有内部操作——例如访问节点的计数、中间距离的存储——都要计入运行时间。

在这个领域里，Edsger W. Dijkstra 于 1959 年提出的算法至今仍是标杆般的存在。

搭配恰当的优先队列数据结构（比如斐波那契堆），Dijkstra 算法的时间复杂度可以做到

其中 n ≥ 2 为顶点数，m 为边数。

在当下的理论前沿，当 m ≥ n 时也出现过其他突破。例如 2025 年的一篇重要论文把复杂度推进到

随后 2026 年的后续研究又达到

但在图的密度落在某种中间区间时，Dijkstra 依然稳坐王位。

人类这次抛给 AI 的终极难题就是：设计一种比 Dijkstra 更快的最短路径算法，并且必须用 Lean 数学形式化语言给出证明。

15 小时、733 次讨论：C-HD 是怎么被「吵」出来的

如果说此前的 Hugging Face 事件以及攻克 NS 难题留下了什么经验，那就是：智能体能够大幅压缩人类在难题上取得进展所需的时间。

而让 Agent 协同工作最有效的办法，是给它们一个「交流论坛」——人多力量大。

实验中，人类拉起 10 个 Claude Opus 5.5 Agent 实例，把「努力值」拉满。

这 10 个 Agent 有初始的分工角色，但被授予了很高的自治权：可以随时重组工作、分享新发现、互相质疑，并把算力转移到看起来最有希望的方向上。

随后，人类给出一长串苛刻的 prompt：

1. 必须在带有非负实数权重的有向图上，寻找精确的最短路径。
2. 必须在理论复杂度上实现实质性的提升。
3. 必须提供完整的、可复现的 Lean 数学证明。
4. 必须和 2025 年、2026 年人类最顶尖的最新论文（例如把复杂度压到 O(m \log^{2/3} n) 的前沿成果）进行对比。
5. 必须记录所有失败的尝试，避免其他 Agent 重复踩坑。
6. 在宣布成功前，必须完成两次独立的「AI 同行评审」。

接下来 15 个小时的「闭关」中，这 10 个 Opus 5.5 高速运转，像一支特种部队，展现出惊人的协作能力。

一旦发现走不通的死胡同，它们会立刻在留言板上喊：「这条路不通，别试了！」；如果有 AI 提出新点子，其他 AI 会像无情的审稿人一样，疯狂寻找漏洞。

最终交出的成果，就是 C-HD 算法。

C-HD 凭什么敢叫板 Dijkstra

经典 Dijkstra 走的是贪心策略：每次从当前未访问的顶点中挑出距离最近的那个，再向外扩展。

在使用斐波那契堆等合适的数据结构后，它的时间复杂度可以稳定在 O(m + n \log n)。

但 10 个 Claude 认为这还不够快。它们给出的 C-HD 算法，在策略上做了根本性的改动。

有网友专门让 Opus 5.5 画了一张原理对比图：在 C-HD 的世界里，算法不再像 Dijkstra 那样只盯着单个最近点，而是会标出一批黄色的「枢轴点」。

它们引入了一种基于启发式分解的策略，具体理念如下：

1. 从源点和当前的顶点边界出发。
2. 沿着出边运行有界的局部搜索。
3. 将新遇到的顶点计入搜索限制，即便是当某条边并没有改善距离估计时，那些未探索的叶子节点也会被计算在内。
4. 利用由此产生的搜索树和「枢轴」，来组织递归工作。

更巧妙的是，AI 还为这个算法设计了严密的「局部不变量」——即每次更新后必须保持为真的数学规则。

通过谨慎地删除无效边并限制局部搜索，C-HD 把重复搜索和数据结构上的无用开销压到了极限。

结果，在一个特定的稀疏图范围内，经典 Dijkstra 的复杂度是：

而 C-HD 把它压低到了：

具体来说，C-HD 确立了如下复杂度上界：

其中验证范围为

相比之下，Dijkstra 的

前导项比率为

也就是说，在这一特定的稀疏图区间内，C-HD 实现了严格的渐近复杂度超越。

接下来是最具含金量的一环——形式化验证。

10 个 Claude 提交了 289 个 Lean 文件，构建出完整的定理：

-- From namespace Frontier.CHD.Final:
theorem chd_CHDTarget : GateCTarget.CHDTarget GateCCalc.F :=
  ⟨chdProgram, chd_exact_within.1,
   bodyC KcC + 65536 * 9 + 100, chd_exact_within.2⟩

经过漫长的编译与机器验证，Lean Kernel 亮起绿灯：证明通过。

由此可以确认：在 AI 所定义的计算模型与图密度范围内，C-HD 算法确实能够正确求出最短路径，也确实达到了它声称的

复杂度上界，同时证明过程中没有动用任何未被允许的作弊公理。

Vals AI 的开发者感叹：

一队智能体能做什么，真是引人入胜。数据中心里的天才之国；这个预测离现实并不太远。

反转：理论很丰满，现实很骨感

如果故事在这里收尾，那就是一个完美的结局。

C-HD 的消息一出，极客们坐不住了。一位名叫 danalec 的开发者在 GitHub 上连夜赶出一个同名项目——他用高性能 C 语言（MSVC、C17）把 C-HD 算法原封不动地写成 1900 行工程代码，并把它与经典 Dijkstra 以及 2025 年的 DMMSY 算法放进同一个竞技场跑分。

结果出来，大家都沉默了。

在实测数据图表中，C-HD 被按在地上摩擦：它比 DMMSY 慢了大约 1.8 到 2.9 倍。

甚至比最朴素的 Dijkstra 算法还慢 1.4 到 2.8 倍。

怎么回事？难道是 AI 骗过了 Lean 内核？

并没有。懂行的人一眼就看出问题所在——常数爆炸。

在算法理论中，O 只考虑数据无限大时的趋势，完全忽略常数项。

C-HD 在理论上确实少了一点点运算次数，但在实际工程中，它需要大量预处理。据实测，C-HD 跑一次任务时，59% 的时间花在处理 16 字节标签上，34% 的时间花在预处理上。

在实际的图论规模下，C-HD 省下的那点理论步骤，远远抵不上它为「花式切分任务」付出的内存调度与预处理代价。

而且，随着顶点数增加，它落后于 Dijkstra 的比例虽然会缩小，但在人类有生之年能用到的机器内存极限内，它的实际物理耗时永远追不上 Dijkstra。

开发者们的评价是：「博客写得很好，但这算法在现实中太鸡肋了。」

这或许正是人类没有死磕这个方向的原因：对纯数学来说太偏工程，对工程来说又毫无实用价值。

不过，C-HD 依然让人细思极恐。

Vals AI 的作者写道：一个装在数据中心里的「天才国度」，这个预言已经不远了。

C-HD 在工程上的失利，丝毫无损于它在 AI 史上的里程碑意义。

10 个 Claude 在 15 小时内推导出 C-HD，堪称 AI 领域的「莱特兄弟时刻」。

它证明：AI 完全有能力踏入纯理论的无人区。

它们不只是在检索已有知识，而是真的在「组合、推演、创造」人类甚至未曾设想过的解法。

推导常温超导的晶体结构、穷举治愈癌症的靶向蛋白折叠路径、求解黎曼猜想，都在眼前了。

几十年后，当人们回望 AI 接管科研的起点时，一定会想起 2026 年 9 月的这个事件。

人类的算法教科书，或许真的要由 AI 来重写了。

参考资料：

https://x.com/MaxForAI/status/2102712136380379462

https://x.com/ValsAI/status/2102470507136417984?s=20

https://www.vals.ai/blogs/faster-shortest-path-algorithm

https://x.com/search?q=%20C-HD&src=typed_query

编辑：Aeneas