Vals publishes a buildable Lean proof for the shortest-path algorithm its ten agents wrote

The two bounds differ by a factor of (log n)^(1/12) at the density Vals chose for its comparison ^[5]. That factor grows slowly. Take a graph with 2^20 vertices: log2 n is 20, and 20^(1/12) is about 1.28 ^[16]. So around a million vertices the proved bound sits roughly 22 percent below Dijkstra's, and Vals says practical speed still needs separate scrutiny ^[16][19].

Density is where the claim gets narrow. The formal program's certified condition is m <= n floor((floor(log2 n))^(3/4)) ^[6]. At 2^20 vertices, floor(20^(3/4)) is 9, so the theorem covers graphs of at most nine edges per vertex, about 9.4 million edges on 1,048,576 vertices ^[17]. Vals says the comparison targets a band of densities where a 2025 paper and a 2026 follow-up on deterministic directed shortest paths left room to improve ^[14].

I would check the accounting first, and it holds up. The method runs bounded searches from a frontier of discovered vertices, and a newly encountered vertex can count against a local search limit even when the edge leading to it fails to improve a distance estimate ^[8]. Search trees and pivots then organize the work that follows ^[8]. The stated bound also charges sorting outgoing edges, reading the input and producing the output ^[7]. Vals makes the point itself: a proposed algorithm can appear faster if preparation is treated as free ^[7].

Krishnan and Nashold built Vals on the premise that model buyers need evaluations grounded in actual work ^[15]. The record of this run is researcher Geby Jaff's own account. He gave the agents roles and a message board where they could exchange ideas, challenge proposed approaches and redirect their work, and he counted 733 messages before they finished C-HD ^[9]. Over about 15 hours that is roughly 49 messages an hour, one every 74 seconds ^[18]. He also instructed them to compare the result against recent research and obtain reproducible verification before claiming success ^[10]. The run was not a controlled comparison of agent teams against human researchers; Vals presents it as Jaff's description of how the work was conducted ^[10].

C-HD itself solves a well-defined problem: exact shortest paths from a single starting vertex in a directed graph with non-negative real edge weights, deterministically ^[3]. The yardstick is Dijkstra's algorithm at O(m + n log n) with a suitable priority queue ^[4]. Jaff said he asked the agents for two reviews; the repository identifies one completed internal agent review and describes the second as provisional, with reproduction fields pending ^[13]. Lean certifies the theorem inside its own formal computational model, and it does not settle whether the algorithms being compared charge work in equivalent ways ^[12].