Claude Opus 5.5 agents proved a faster shortest-path search in Lean in 15 hours

Vals AI assembled ten agents based on Claude Opus 5.5, gave them a shared message board and a task: find a faster algorithm for shortest-path search in a directed graph with non-negative real weights and exact answers — and fully prove its correctness and running-time bound in Lean. The agents started with assigned roles, but they could redistribute effort, share findings, challenge one another's ideas, and record dead ends so they wouldn't repeat them.

After roughly 15 hours and 733 messages, the team presented the C-HD algorithm. Before success could be declared, a reproducible Lean build and two independent reviews were required; had the improvement proved unprovable, the agents were to preserve partial progress and list what remained unsolved.

The improvement is asymptotic and holds only within a certain range of graph density. Along the profile where the number of edges is close to n·(log n)^(3/4), the C-HD bound is on the order of n·(log n)^(11/12) versus n·log n for Dijkstra; the ratio of the leading terms grows as the twelfth root of the logarithm. The author immediately cautions: this is an upper bound on complexity, not a measured speedup.

The algorithm's core idea is a bounded local search along outgoing edges: newly encountered vertices, including unvisited leaves at failing edges, count toward the search limit, while local invariants and careful edge deletion keep repeated work bounded. For small inputs and outside the proved range, the agents added a separate algorithm — Bellman–Ford.

The running-time bound was checked with the Lean Comparator tool: it confirms that exactly the stated theorem was proved, that only permitted axioms are used, and that the result is accepted by the Lean kernel.

The limitations are stated honestly: the algorithm was not benchmarked on large real-world graphs, the constants in the formal construction are enormous, and at a different graph density the improvement over the best known bounds is not proved. The author released the full proof package publicly.

Image:

Image: Michel Bakni CC BY-SA 4.0 · License

Translation editor: Салтанов А.