Shortest paths is a simple problem. Given a directed graph with non-negative real edge weights, Dijkstra's algorithm runs in O(m + n log n) time using a Fibonacci heap. For m ≥ n, other deterministic algorithms achieve O(m log^{2/3} n) (2025 breakthrough) and O(m √log n + √(mn log n log log n)) (2026 follow-up).

After about 15 hours and 733 messages, my agents proposed a new algorithm, C-HD, verified in Lean. It handles local search well, using priority comparisons and counting newly encountered vertices as unexplored leaves. It maintains local invariants with careful edge deletion and bounded local search, achieving O(n + m + m log(2 + m/(n+1)) + m^{1/3} (n log(n+2))^{2/3}) within the certified range m ≤ n⌊⌊log₂ n⌋^{3/4}⌋.

C-HD reduces repeated search and data-structure work by running bounded local searches from the source and frontier, counting newly encountered vertices, and using search trees and pivots to organize recursive work. It relies on sorted outgoing-edge lists. For small or out-of-range inputs, a separate Bellman–Ford algorithm with O((n+1)(m+1)) runtime is selected at the start.