Ten AI agents produced a Lean-verified shortest-path bound

Vals AI reports that ten Claude Opus 5.5 agents spent about 15 hours and exchanged 733 messages while designing a shortest-path algorithm and proving its complexity bound in Lean. The resulting algorithm, C-HD, computes exact single-source distances in directed graphs with non-negative real edge weights.

The Vals AI report presents C-HD as a new asymptotic improvement within a narrow graph-density range. Lean verifies the stated theorem and its permitted assumptions; novelty and comparisons with prior literature still depend on external review.

The bound C-HD claims

The target problem is the standard exact single-source shortest-path problem. Given a directed graph with n vertices, m edges, and non-negative weights, the algorithm must return the minimum path weight from one source to every reachable vertex.

Dijkstra’s algorithm with a Fibonacci heap runs in O(m + n log n) time. A 2025 paper improved the bound to O(m log^(2/3) n) for m ≥ n. Vals AI also compares C-HD with a later bound of:

O(m * sqrt(log n) + sqrt(m * n * log n * log log n))

The agents produced a proof repository for the following C-HD bound:

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

The improved guarantee applies when:

m ≤ n * floor(floor(log₂ n)^(3/4))

The submitted program checks that condition at startup. Graphs outside the certified range use a verified Bellman-Ford fallback, so the improved complexity claim applies only to the C-HD branch.

A narrow asymptotic advantage

C-HD’s largest stated advantage appears near m ≈ n log^(3/4) n. Along that profile, the ratio between the compared leading terms grows as (log n)^(1/12), an unusually slow rate.

For the theoretical example n = 2^1000, the leading-term ratio is about 1.78. That figure describes asymptotic expressions rather than elapsed time.

How C-HD controls repeated work

C-HD organizes the search through bounded local explorations, priority comparisons, search trees, and recursively selected pivots. Its accounting treats a newly encountered vertex as part of a local search even when that vertex remains an unexplored leaf because the incoming edge failed to improve its current distance estimate.

1. Begin with the source and the current frontier of discovered vertices.
2. Explore outgoing edges through bounded local searches.
3. Count newly encountered vertices toward each search limit, including unexplored leaves.
4. Build search trees and choose pivots that divide the remaining recursive work.
5. Maintain local invariants that bound repeated processing when a vertex appears in several searches.

That accounting limits work spent on edges that produce no distance update. The proof then combines the local bounds across the recursive structure to derive the stated running time without assuming a known vertex-processing order.

How the agents divided the research

Vals AI ran ten instances of Claude Opus 5.5 at the model’s maximum-effort setting and connected them through a shared message board. The agents began with assigned roles, then redistributed work as they found promising approaches or identified failures.

The initial prompt allowed several research directions, including removing logarithmic factors, improving an exponent, finding a linear-time algorithm, or proving a lower bound. The orchestration imposed concrete checks on the collaboration:

• Record failed approaches so other agents can avoid repeating them.
• Challenge intermediate claims before incorporating them into the shared result.
• Produce a reproducible Lean build before declaring success.
• Complete two separate internal reviews of the proposed proof.
• Preserve partial results and open questions if no improvement survives verification.

The proof’s trust boundary

Lean’s kernel checked that the submitted terms prove the specified theorem, and the Lean Comparator tool checked that the proof targets the required statement and uses only permitted axioms. This process catches invalid deductions regardless of how confidently an agent presents them.

Kernel acceptance covers the formal statement as encoded. Human reviewers must still examine whether that statement faithfully represents the intended algorithm, whether the complexity model matches the paper’s claims, and whether earlier work already contains the same result.

A reusable pattern for agent research

For developers building long-running agent systems, the experiment provides a concrete architecture: multiple workers share intermediate results, adversarial reviewers inspect candidate solutions, and an external checker decides whether the final artifact satisfies a precise specification.

Formal proof assistants offer especially strong checks for mathematical work. Compilers, test suites, model checkers, and simulators can serve a similar role in software and systems research, provided their specifications cover the properties being claimed.

The evidence from this run remains specific: ten agents produced one formally accepted shortest-path result in roughly 15 hours, with no demonstrated production speedup and no independent confirmation of novelty. The reproducible proof makes those remaining questions easier to investigate because reviewers can inspect the theorem, assumptions, algorithm, and build rather than reconstructing the agents’ reasoning from their conversation.