AI 团队用 Lean 证明新最短路径算法
A Faster Shortest Path Algorithm
我召集了 10 个 Claude Opus 5.5 智能体，在一个共享的 message board 上协同工作，仅用 15 小时就设计并证明了名为 C-HD 的新最短路径算法。该算法在特定图密度下，将时间复杂度从经典的 Dijkstra 算法的 O(n log n) 提升到了 O(n log^11/12 n)。整个过程完全由智能体自主探索、辩论并完成，最终通过 Lean 形式化验证工具证明了其正确性与效率。虽然常数项巨大，但这在理论上确立了新的渐进上界，展示了 AI 团队在解决复杂数学问题上的惊人潜力。
如果 OpenAI 的 Hugging Face 事件及其 Navier-Stokes 结果教会了我什么，那就是智能体可以极大地压缩解决问题所需的时间。
HN 评论区
10- throwway262515
例如，若 n = 2^1000，主导项 n lg n 与 n (lg n)^(11/12) 的比值为 1000^(1/12) ≈ 1.78（忽略常数和低阶项）。这并非实测的加速效果。
难道那个看似更复杂算法的常数因子减速，不太可能完全掩盖掉这 1.78 倍的提升吗？
> 形式化构造中的常数极大，因此这并不能证明有实际的加速效果。
可惜作者没再多写几句。
- swiftcoder
如果我理解没错的话，这属于那种理论上的改进，但带来的实际加速效果微乎其微。不过我倒是很好奇，未来几个月里，计算机科学中还有多少算法的界限会被打破。
- EdSchouten
如果这篇文章用 |V| 和 |E| 来代替 m 和 n，给出的时间复杂度会更容易阅读。