AI agents design and Lean-verify new shortest-path algorithm beating published bounds

Ten Claude Opus 5.5 agents were tasked with finding a faster exact shortest-path algorithm for directed graphs with non-negative real weights and proving it correct in the Lean theorem prover. Over roughly 15 hours and 733 messages, the agents produced an algorithm called C-HD, which its creators say formally improves on previously published complexity bounds, including Dijkstra's algorithm and two recent 2025 and 2026 papers.