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 团队在解决复杂数学问题上的惊人潜力。