AI agents deliver Lean-verified shortest-path algorithm with tighter bound than Dijkstra

A team of ten autonomous AI agents has produced a new exact shortest-path algorithm together with a machine-checked proof of its running time, according to a Vals AI blog post that circulated on the front page of Hacker News. The algorithm, called C-HD, improves on the asymptotic worst-case bound of Dijkstra's classic method for directed graphs within a specific density range. Vals AI is candid about the limits of the result: the gain is purely theoretical, and no real-world speedup has been demonstrated.

The setting and the new bound

The problem is single-source shortest paths on a directed graph whose edges carry non-negative real weights, with exact answers required. Dijkstra's algorithm, paired with a priority queue such as a Fibonacci heap, solves this in O(m + n log n) time, where n is the vertex count and m the edge count.

Vals AI points to two recent deterministic results for m ≥ n: an O(m log^(2/3) n) algorithm from a 2025 paper and an O(m√log n + √(mn log n log log n)) follow-up published in 2026. Between these bounds lies a broad stretch of the density spectrum — relatively sparse graphs — where Dijkstra still wins. That gap is what C-HD targets.

Within its certified range of roughly m ≤ n(log₂ n)^(3/4), C-HD achieves:

O(n + m + m log(2 + m/(n+1)) + m^(1/3)(n log(n+2))^(2/3))

According to Vals AI, this accounting also covers memory allocation, sorting edges, reading the input graph and writing the output. Along the profile m ≈ n log^(3/4) n, Dijkstra's bound is O(n log n) while C-HD's simplifies to O(n log^(11/12) n) — a smaller asymptotic ceiling as graphs grow.

How the algorithm works

C-HD is deterministic and built around bounded local searches launched from the source and the current frontier of vertices. Newly encountered vertices count against a search's size budget, and an edge that fails to improve a distance estimate still contributes an unexplored leaf to that budget. The algorithm maintains local invariants across updates, deletes edges carefully, and uses the resulting search trees and pivots to structure recursion, which keeps revisits of the same vertices bounded. It depends on sorted outgoing-edge lists that it constructs itself, with that preprocessing charged to its own running time.

Inputs outside the certified density range, along with small inputs, are routed to a plain Bellman–Ford implementation with an O((n+1)(m+1)) bound, chosen at the start of execution. Vals AI notes that this fallback is not a Dijkstra variant.

What is actually proven

The result is an upper bound on complexity — a mathematical promise about worst-case growth — not a benchmark. Vals AI illustrates the scale of the improvement: at n = 2^1000, the leading terms n log₂ n and n(log₂ n)^(11/12) differ by a factor of 1000^(1/12) ≈ 1.78, and that factor grows only polylogarithmically, since squaring n multiplies it by 2^(1/12).

The author ran small correctness simulations but did not benchmark the implementation on large real graphs, and states that the constants baked into the formal proof are huge, so a practical speedup is not established. For denser graphs such as m = 10n, the result claims no improvement over the best known bounds at all.

The performance claim was formalized in Lean and checked with a Lean Comparator tool, which verifies that the submitted proof establishes the stated theorem, draws only on allowed axioms, and passes Lean's kernel checks.

An agent-built result

The algorithm emerged from an experiment in orchestrating AI research agents. Vals AI spawned ten Claude Opus 5.5 agents at their maximum effort setting and gave them a shared message board. They started with assigned roles but were free to reorganize, share discoveries and challenge one another's approaches. After roughly 15 hours and 733 messages, the team had a proposed algorithm and a complete Lean proof covering both correctness and the runtime target. The original prompt asked for a substantial theoretical improvement on exact shortest paths for directed graphs with non-negative weights, backed by formal verification.

Why it matters

Shortest-path computation sits inside routing engines, network protocols, compilers, build systems and logistics software, nearly always via Dijkstra or a descendant. A better asymptotic bound in the sparse regime — even one with impractical constants — is the kind of result that often seeds further refinements.

Two other angles stand out. First, the claim is machine-checked: the deliverable is a Lean theorem accepted by a proof kernel, not a prose argument that readers must take on trust. Second, the work adds to growing evidence that coordinated AI agents can compress research timelines dramatically, turning what is typically a multi-month theoretical effort into roughly a day of agent time. The honest framing from Vals AI — an asymptotic win with no demonstrated real-world speedup — is the right way to read it: a verified theoretical advance, and a data point on where agent-driven research is heading.