A Faster Shortest Path Algorithm

A new deterministic shortest-path algorithm called C-HD solves exact single-source shortest paths on directed graphs with nonnegative real weights by combining bounded local searches, careful edge deletions, and maintenance of local invariants. The procedure treats newly encountered vertices (including unexplored leaves) as part of search-size limits, uses sorted outgoing-edge lists built in charged preprocessing, and organizes work with search trees and pivots to limit repeated processing. Within the certified density range m ≤ n⌊⌊log2 n⌋^{3/4}⌋ the algorithm is proven to run in O(n + m + m log(2 + m/(n+1)) + m^{1/3}(n log(n+2))^{2/3}). Along the profile m ≈ n log^{3/4} n this simplifies to O(n log^{11/12} n), an asymptotic improvement over Dijkstra’s O(n log n) and over recent m log^{2/3} n and related bounds in that regime; a Bellman-Ford fallback covers small or out-of-range inputs.

Ten Claude Opus 5.5 agents developed C-HD and produced a formal Lean proof within roughly 15 hours of collaborative messaging; the proof was checked with the Lean Comparator and accepted by Lean’s kernel, establishing the stated runtime guarantee. The formal construction carries enormous constants and only small correctness simulations were run, so no empirical speedup is claimed. Full Lean sources, the informal writeup, and verification records are available on GitHub for inspection.