Vals AI 用 10 个 Claude Opus 5.5 agents 提出 C-HD shortest-path 算法，并给出 Lean 验证的复杂度改进

Vals AI 9 月 20 日发布 C-HD：10 个 Claude Opus 5.5 agents 在约 15 小时、733 条共享消息后提出一个针对有向、非负实权单源最短路的确定性算法，并生成 Lean 4 正确性与运行时间证明。冻结 proof package 记录了 2,548-job full build、fresh-copy rebuild，以及两次分别检查 18,994 个 project constants 的 kernel replay；形式化改进适用于特定稀疏密度区间，例如沿 m≈n·log^(3/4)n 时给出 O(n·log^(11/12)n) 上界。