A Faster Shortest Path Algorithm

gist

Geby Jaff describes a ten-agent Claude Opus 5.5 effort that produced C-HD, a formally checked exact shortest-path algorithm for directed graphs with non-negative real weights. In a restricted sparse-density regime, its proven bound improves on Dijkstra and two recent deterministic results by reducing repeated local-search and data-structure work. The result is asymptotic, not empirical: only small correctness simulations were run, constants are enormous, and Bellman–Ford handles other inputs.

ideas

• The gain is regime-specific. C-HD improves the leading bound along a sparse graph profile, with a certified range that does not cover every edge density.
• Local search controls repeated work. Bounded searches, unexplored-leaf accounting, pivots, and edge deletion keep recursive processing from multiplying unnecessarily.
• Formal verification makes the claim inspectable. Lean and the Comparator establish the runtime target, exactness, permitted axioms, and the stated asymptotic comparisons.
• The theorem is not a benchmark. The author ran only small correctness simulations; huge constants mean the proof does not establish a practical speedup.
• A message board made parallel research composable. Ten agents could reorganize roles, share discoveries, challenge claims, and preserve failed approaches while pursuing a reproducible proof.

quotes