Ten Claude Opus 5.5 agents produced a faster shortest-path algorithm, C-HD, with a formal proof in Lean

A Faster Shortest Path Algorithm

Vals had ten Claude Opus 5.5 agents collaborate over 15 hours to produce C-HD, a shortest-path algorithm for directed graphs with non-negative real weights. Within the certified density range m ≤ n⌊(log₂ n)^(3/4)⌋, its proven bound is O(n + m + m log(2 + m/(n+1)) + m^(1/3)(n log(n+2))^(2/3)). When m ≈ n(log n)^(3/4), the leading term drops from n log n to n(log n)^(11/12); at n=2^1000 the theoretical ratio is about 1.78. The algorithm uses bounded local searches that count non-improving edges as unexplored leaves to limit repeated work, and falls back to Bellman–Ford outside the certified range. Both correctness and the complexity bound are formally verified in Lean. The post does not report large-scale benchmarks—only small correctness simulations—and notes the constants are not yet optimized.

Why it matters: Ten Claude Opus 5.5 agents collaborating to produce a formally verified shortest-path algorithm in 15 hours is novel enough to clear H and K. But it's pure theory with no engineering hook, so R is absent — right at the featured threshold. The post doesn't give concrete perform...