# Vals AI Says Ten Claude Opus 5.5 Agents Found A Faster Shortest-Path Algorithm, And Proved It Formally In 15 Hours > Source: > Published: 2026-09-23 07:12:28+00:00 AI is continuing to make breakthroughs in math and computing. AI evaluation firm Vals AI says it set ten instances of Claude Opus 5.5 loose on one of computer science’s oldest problems, and came away with a new algorithm plus a machine-checked proof that it actually works. Shortest paths is about as foundational as it gets. Given a graph of points connected by weighted edges, the question is simple: what’s the cheapest way to get from a starting point to everywhere else? It’s the math underneath GPS routing, network packet delivery, and logistics planning. The standard answer for six decades has been Dijkstra’s algorithm, which runs in roughly O(m + n log n) time for a graph with n vertices and m edges. Researchers have chipped away at that bound for specific ranges of graph density since — a 2025 paper improved it for dense graphs, and a 2026 follow-up pushed further — but there’s still a wide zone where nothing beats Dijkstra. Vals AI researcher Geby Jaff wanted to know what was possible in that zone if the edge weights were non-negative real numbers, so he spun up ten Claude Opus 5.5 agents at maximum effort, gave them a shared message board, and told them not to declare victory until any improvement was proven correct and efficient in Lean, the formal verification tool mathematicians use to have proofs checked line-by-line by a computer rather than taken on faith. The agents started with assigned roles, then reorganized as promising leads emerged, posting 733 messages over about 15 hours, logging failed approaches so they wouldn’t be repeated, and requiring two internal peer reviews before calling anything finished. What came out is an algorithm called C-HD, with the full Lean proof package published on GitHub. For graphs whose edge count stays under a specific density threshold, C-HD’s certified runtime works out to a bound that simplifies, along a representative graph density, to O(n log^(11/12) n) — against Dijkstra’s O(n log n). It’s a genuine asymptotic improvement, though a modest one: run the numbers on a graph with 2^1000 vertices and the gain comes out to roughly 1.78x on the leading term, widening only slowly as graphs get bigger. Step outside the certified density range — say, once a graph has ten times as many edges as vertices — and the proof no longer applies; the team kept old-school Bellman-Ford on hand as a fallback for graphs outside that window or too small to bother with the new machinery. Jaff is candid about the limits of the result. Nobody benchmarked C-HD against real-world graphs — the team ran small correctness checks, not performance tests — and the constants buried inside that asymptotic bound are, by his own account, enormous, meaning there’s no claim here about anything running faster in practice today. The verification itself is the more solid part of the story: an independent tool called the Lean Comparator rebuilt the proof from a clean copy and confirmed the final theorem depends on nothing but Lean’s standard axioms, with no shortcuts. Of the two peer reviews Jaff required, one was fully completed by another agent; the second was left provisional, with some reproduction steps still open — a caveat he flags rather than papers over. Vals AI, the two-year-old startup behind the experiment, was built by Stanford computer science alumni Rayan Krishnan and Langston Nashold, backed by Andreessen Horowitz, specifically to measure what frontier AI systems can actually do. This experiment is a step past the benchmark-scoring Vals is best known for — instead of grading an AI’s answers against a fixed test, it handed a team of them an open problem and a formal bar for success, and let them sort out the division of labour themselves. The model doing the work is the same one that’s [currently sitting at the top of the Artificial Analysis Intelligence Index](https://officechai.com/ai/claude-opus-5-5-creates-5-point-lead-over-gpt-6-astra-jumps-to-top-spot-on-artificial-analysis-intelligence-index/), ahead of GPT-6 Astra, after [Anthropic released Claude Opus 5.5](https://officechai.com/ai/claude-opus-5-5-benchmarks/) with what the company called leading scores on most benchmarks. Whether C-HD ever earns a footnote in an algorithms textbook is a separate question from whether ten agents, a message board, and 15 hours can clear the bar of a real formal proof. On the second count, at least, Vals AI has the receipts.