Vals AI 公布了一项围绕最短路径问题的研究实验：10 个 Claude Opus 5.5 Agent 在一个可协作的沙盒环境中工作 15 小时，围绕经典的 Dijkstra 最短路径算法展开挑战，最终给出一套名为 C-HD 的新算法，并附上 289 个 Lean 形式化证明文件，提交给 Lean Kernel 后一次性通过验证。
这项结果在算法圈引发广泛关注。按照报道中的描述，实验目标不是单纯改写代码实现，而是要在理论复杂度上提出比 Dijkstra 更快的方法，同时给出完整、可复现的数学证明。
Dijkstra 仍是最短路径问题的经典基线
Dijkstra 算法由 Edsger W. Dijkstra 于 1959 年提出，问题定义是：在一个带非负实数权重的有向图中，从给定起点出发，求到其余各顶点的最小总权重路径，或判断其不可达。报道提到，在该问题中，访问节点计数和中间距离存储等内部操作都会计入运行时间。
在配合合适的优先队列数据结构时，例如斐波那契堆，Dijkstra 算法的时间复杂度可达到 O(m + n log n)，其中 n≥2 表示顶点数，m 表示边数。报道还提到，在理论研究前沿，当 m≥n 时，2025 年有论文将复杂度推进，2026 年的后续研究又继续改进，但在图密度处于某些中间状态时，Dijkstra 仍然是难以撼动的基准方案。
这也构成了此次实验的人类设题：设计一种比 Dijkstra 更快的精确最短路径算法，并且必须用 Lean 数学形式化语言证明。
10 个 Agent 在沙盒中协作 15 小时
根据报道，Vals AI 在实验中启动了 10 个 Claude Opus 5.5 Agent 实例。它们最初有分工角色，但具备较高自治权，可以自行调整工作、共享发现、相互质疑，并把算力转向更有希望的研究路线。
人类研究者给出的约束条件包括：
- 必须在带非负实数权重的有向图上寻找精确最短路径；
- 必须在理论复杂度上实现实质性提升；
- 必须提供完整、可复现的 Lean 数学证明；
- 必须与 2025 年、2026 年的人类最新论文结果对比；
- 必须记录所有失败尝试，避免其他 Agent 重复试错；
- 在宣布成功前，必须完成两次独立的 AI 同行评审。
这 10 个 Agent 被放进一个带虚拟留言板的沙盒里，可以围绕技术路线展开交流、质疑和分工重组。15 小时后，系统留下了 733 次讨论记录，最终形成 C-HD 算法方案。
C-HD 的设计思路
报道将 Dijkstra 的核心策略概括为贪心式扩展：在当前未访问顶点中选出距离最近者，再继续向外扩展。在合适数据结构支持下，这一方案稳定达到 O(m + n log n)。
相比之下，C-HD 试图从策略层面重构搜索过程。文中给出的描述是，它不再只盯住单个最近点，而是引入一批被称为「枢轴点」的节点，并基于启发式分解来组织搜索和递归工作。具体理念包括：
- 从源点和当前顶点边界出发；
- 沿出边运行有界局部搜索；
- 把新遇到的顶点计入搜索限制，即便某条边没有改善距离估计，未探索的叶子节点也会被计入；
- 利用由此形成的搜索树和「枢轴」组织递归。
报道还提到，C-HD 为这些步骤配套设计了严格的「局部不变量」，也就是每次更新后都必须保持成立的数学规则。借助删除无效边和限制局部搜索的安排，它试图压缩重复搜索以及数据结构上的额外开销。
形式化证明一次性通过 Lean Kernel 验证
在理论结果之外，这次实验最受关注的部分，是它提交了完整的形式化验证材料。报道称，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 开发者在文中表示：「一队智能体能做什么，真是引人入胜。数据中心里的天才之国；这个预测离现实并不太远。」
工程复现结果并不占优
不过，这一结果并没有在实际运行性能上直接战胜现有方案。报道提到，消息公布后，一名名为 danalec 的开发者在 GitHub 上实现了名为 C-HD 的项目，使用高性能 C 语言（MSVC、C17）将该算法写成约 1900 行工程代码，并与经典 Dijkstra 以及 2025 年的 DMMSY 算法放在同一环境中测试。
实测结果显示，C-HD 在工程性能上仍落后于对比算法：它比 DMMSY 慢约 1.8 至 2.9 倍，也比最朴素的 Dijkstra 慢 1.4 至 2.8 倍。
报道给出的解释是，这不是 Lean Kernel 验证出错，而是典型的常数项问题。渐近复杂度只讨论输入规模趋于无限大时的增长趋势，不反映现实工程中的预处理、内存调度和数据标签开销。根据实测，C-HD 单次运行中，59% 的时间花在处理 16 字节标签，34% 的时间花在预处理上。在实际图论规模下，它节省的理论步骤不足以覆盖这部分成本。
理论突破与工程价值被分开看待
报道提到，随着顶点数继续增加，C-HD 相对 Dijkstra 的落后比例虽然在缩小，但在现实可用的机器内存限制内，仍无法追上 Dijkstra 的实际物理耗时。开发者对这一复现结果的评价是：「博客写得很好，但这算法在现实中太鸡肋了。」
文中据此指出，这条路线可能正处在一个尴尬位置：从纯数学角度看，它带有较强工程色彩；从工程落地角度看，又缺乏足够实用性。
这项实验的意义仍集中在 AI 研究能力本身
尽管工程测试不占优，报道仍将这次实验视为 AI 研究能力的一次重要展示。核心原因不在于 C-HD 已经成为新的实用最短路径标准，而在于 10 个 Claude Opus 5.5 Agent 在 15 小时内完成了并行探索、失败记录、同行评审和形式化证明，最终产出一个此前未被提出的算法框架。
从报道给出的结论看，C-HD 的工程失利并未削弱其在 AI 发展脉络中的象征意义。文章把这次实验称作 AI 进入纯理论问题空间的一次标志性案例，并援引 Vals AI 作者的判断，认为「数据中心里的天才国度」这一图景已经不远。
参考资料包括 MaxForAI、Vals AI 在 X 上发布的内容，Vals AI 博客文章，以及 X 上围绕 C-HD 的相关讨论。本文来自微信公众号「新智元」，作者为 Aeneas。