Claude Opus 5.5挑战Dijkstra：10个AI Agent 15小时做出C-HD，Lean形式化验证

10个Claude Opus 5.5 Agent，15小时，733条讨论记录。

这次AI干的事情有点不一样。

它们没有去刷一道普通编程题，也没有单纯优化一段代码，而是被丢进了一个计算机科学研究级难题：

能不能设计出一个在理论复杂度上超过经典Dijkstra的最短路径算法？

最终，10个Agent给出了一个名为 **C-HD** 的新算法，并进一步用Lean 4对算法的正确性和运行时间上界进行了形式化验证。

不过先把最容易误解的一点说清楚：

这并不意味着Dijkstra已经被AI“干掉”了。

C-HD目前证明的是，在一个特定的稀疏图密度区间内，它拥有更低的渐近复杂度；官方材料同时明确表示，这并不是一次实际运行速度上的胜利，而且证明中的常数非常大。

但即便如此，这件事依然相当有意思。

因为这一次，AI碰到的已经不是“写代码”，而是**算法研究本身**。

Dijkstra为什么这么难动？

最短路径问题看起来非常简单。

给定一个有向图，每条边拥有一个非负实数权重。从一个起点出发，需要计算到其他顶点的精确最短距离。

这就是计算机科学里经典到不能再经典的问题。

1959年，Edsger W. Dijkstra提出了著名的Dijkstra算法。

在合适的数据结构下，经典Dijkstra可以达到：

O(m + n log n)

其中，n是顶点数量，m是边数量。

几十年来，研究人员一直在尝试突破最短路径问题的复杂度极限。

2025年的研究已经把有向单源最短路径问题推进到了 **O(m log^(2/3)n)**；之后还有进一步的理论改进。

也就是说，今天再想在这个领域往前挪一步，已经不是“优化一下代码”那么简单。

你得证明：

在足够大的数据规模下，新算法的增长速度确实比旧算法更低。

这也是这次实验真正有意思的地方。

10个Opus 5.5，被关进了同一个“研究室”

Vals AI的做法并不是给一个Claude扔一个超长Prompt。

他们启动了 10个Claude Opus 5.5 Agent，让它们共享一个虚拟留言板。

Agent之间可以：

最终，这10个Agent大约运行了 **15小时**，留下了 **733条协作消息**。

这个过程其实很像一个小型算法研究团队。

有人负责寻找方向，有人负责证明，有人专门挑错，还有Agent负责检查此前已经失败的路线，避免团队重复踩坑。

最后，它们把多个方向收敛成了一个叫做 **C-HD** 的算法。

这可能才是整个实验最值得关注的部分：

AI不是单独完成一道题，而是在模拟一个小型研究团队。

C-HD到底比Dijkstra快在哪里？

这里一定要把“快”两个字拆开。

C-HD并不是说：

目前并没有这样的结论。

它真正突破的是**渐近复杂度**。

C-HD最终证明的运行时间上界为：

O(n + m + m log(2 + m/(n+1)) + m^(1/3)(n log(n+2))^(2/3))

而Dijkstra配合斐波那契堆的经典复杂度为：

O(m + n log n)

C-HD的改进只在特定的图密度范围内成立。

形式化验证所覆盖的条件大致为：

**m ≤ n · log^(3/4)n**

在这个特殊区间附近，如果把复杂度统一换算成log n的幂次，可以得到：

注意这里最关键的是最后一列。

11/12 < 1。

也就是说，在这个特定稀疏图区间内，C-HD的理论增长率低于Dijkstra。

这就是这次实验真正意义上的“突破”。

但它和“实际跑得更快”，完全是两回事。

C-HD的核心思路是什么？

Dijkstra最经典的思路，是不断寻找当前距离最小的顶点，然后继续向外扩展。

C-HD则尝试把搜索过程重新组织。

它会进行有界局部搜索，从源点和当前边界向外探索。

搜索过程中，新遇到的顶点会被纳入搜索限制，即使某些边最终没有改善距离估计，相关的未探索节点也会计入搜索过程。

然后，算法利用局部搜索产生的搜索树以及“枢轴”结构，把后续工作组织成递归任务。

简单理解：

Dijkstra更像是不断找“当前最近的一个点”；C-HD则试图把局部搜索、搜索树和枢轴组织起来，减少重复探索。

真正复杂的地方在后面。

算法还需要建立一套严格的局部不变量，证明每一次边删除、距离更新和递归操作都不会破坏最终正确性。

所以它最后交出来的并不是：

“我感觉这个算法应该可以。”

而是：

把整个算法写进Lean，让机器检查它到底有没有按照数学规则工作。

289个Lean文件，机器把证明重新检查了一遍

这可能是整个事件里最硬核的一部分。

C-HD项目公开了完整的Lean 4证明包。

冻结版本包含 **289个Lean文件**，完整工程构建通过了 **2548个任务**。

最终定理还进行了独立的Kernel Replay，对最终定理依赖的项目常量进行了再次检查。

结果通过。

这意味着：

在它定义好的计算模型、输入条件和图密度范围内，机器确实验证了C-HD程序能够计算精确的单源最短路径，并满足声明的运行时间上界。

这里需要特别注意“定义好的”四个字。

Lean证明的是：

你写下来的数学命题是否成立。

它并不会自动告诉你：

这些仍然需要人类研究者进一步判断。

而且，目前项目里的评审主要也是Agent自己的内部评审，并不等于已经经过外部理论计算机科学家的正式同行评审。:chatgpt-content-reference{index="1"}

最有意思的反转：理论赢了，实际速度却没赢

如果故事到这里结束，确实很像“AI改写算法教科书”。

但现实马上泼了一盆冷水。

有人把C-HD进一步实现成了工程代码，并拿它与Dijkstra以及其他最短路径算法进行实际测试。

结果并没有出现“AI算法吊打经典算法”的戏剧性场面。

恰恰相反：

C-HD在实际运行中并没有表现出优势。

这其实一点都不奇怪。

因为算法理论里的O大O符号，主要描述的是：

当数据规模趋近于无限大时，算法增长速度如何变化。

它并不负责告诉你：

今天这台电脑跑100万个节点，到底谁更快。

而C-HD的问题正是——

理论上的改进非常小，但工程实现中的常数非常大。

复杂的预处理、数据结构操作以及额外的内存访问，都可能把理论上省下来的那一点复杂度优势吃掉。

Vals AI自己也明确强调，C-HD是一个**渐近复杂度结果，而不是实测性能提升**，并且其形式化构造带有巨大的常数。

所以现在的情况其实非常有意思：

数学意义上，它确实往前迈了一步。

工程意义上，它暂时没有成为Dijkstra的替代品。

AI真正突破的，可能不是Dijkstra

所以这次事件真正值得讨论的，并不是：

这个说法太简单，也不准确。

真正值得关注的是：

10个AI Agent能不能组成一个能够进行理论研究的协作系统？

这次实验至少展示了一种可能。

一个Agent提出想法。

另一个Agent找漏洞。

第三个Agent尝试形式化。

第四个Agent检查复杂度。

第五个Agent继续寻找反例。

然后所有结果重新回到共享环境里。

最终，它们在大约15小时里完成了一套包含算法、复杂度分析和Lean形式化验证的完整成果。

这和让AI写一个排序函数，已经不是一个量级的问题。

当然，现在距离“AI接管科研”还差得远。

C-HD的结果仍然需要人类理论计算机科学家审视其新颖性、计算模型以及与既有研究的关系；它的工程性能也远未证明能够取代成熟算法。

但有一点已经越来越明显：

AI开始进入的不只是“使用算法”的阶段，而是“尝试设计算法”的阶段。

这次C-HD没有真正让Dijkstra退休。

但它至少给出了一个非常有意思的信号：

经典算法的理论边界，已经开始成为AI Agent可以主动探索的东西。

而这，可能比一次单纯的跑分第一更值得关注。