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

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.