Vals AI's Claude Opus 5.5 Agents Prove Faster Algorithm

Vals AI deployed ten instances of Anthropic's Claude Opus 5.5 at maximum-effort settings to collaborate on a complex mathematical challenge. Over a 15-hour period, the agents exchanged 733 messages on a shared message board to design a new shortest-path algorithm called C-HD. The algorithm computes exact single-source shortest paths in directed graphs with non-negative edge weights. Crucially, the agents also wrote a complete proof of its complexity bound in the Lean theorem prover, which was successfully verified by the Lean Comparator tool.

The resulting C-HD algorithm achieves a complexity bound of O(n + m + m log(2 + m/(n+1)) + m^(1/3)(n log(n+2))^(2/3)). This formula beats Dijkstra's algorithm with a Fibonacci heap, which runs in O(m + n log n) time, as well as a 2025 breakthrough bound of O(m log^(2/3) n) for m >= n. It also improves upon a later bound of O(m * sqrt(log n) + sqrt(m * n * log n * log log n)). However, this improvement only applies within a narrow, certified sparse density regime, specifically near m ≈ n log^(3/4) n. Outside this range, the program falls back to a verified Bellman-Ford algorithm.

While mathematically verified, the practical utility of C-HD remains unproven. The algorithm's construction contains massive constants, meaning its real-world performance may not be competitive. No large-scale benchmarks were run on actual graphs; testing was limited to small correctness simulations. For example, at a theoretical vertex count of n = 2^1000, the ratio of the leading terms between C-HD and its competitor is only about 1.78, representing an incredibly slow rate of asymptotic improvement.

The experiment's success lies in its multi-agent architecture. The ten Claude Opus 5.5 agents began with assigned roles and dynamically redistributed tasks. To prevent errors, the system enforced strict collaboration rules: agents recorded failed paths, challenged each other's intermediate claims, and conducted two separate internal peer reviews before compiling the final Lean code. This structured workflow highlights how automated verification tools can reliably gate and validate the output of generative AI models.