Vals AI

Problem

Shortest paths is a very simple problem. There is a graph of vertices and (possibly directed) edges that connect them. Each edge has a real number weight. Starting from some vertex, for every other vertex in the graph you want to find the minimum total weight of a path, or report that it is unreachable.

In the version I considered, the graph was directed, I required exact answers and was given non-negative real weights for the edges.

I assume that real number weights can be compared and added. Any operations the shortest path algorithm does internally (such as counting how many nodes are visited or storing distances on intermediate vertices) counts towards running time.

With this setup, the classic Dijkstra’s shortest path algorithm runs in O(m+nlog⁡n)O(m+n\log n) time, where n≥2n \ge 2 is the number of vertices and mm is the number of edges in the input graph. This is achieved using a suitable priority queue data structure, such as a Fibonacci heap. For m≥nm\ge n, other deterministic algorithms achieve O(mlog⁡2/3n)O(m \log^{2/3} n), first introduced in this 2025 breakthrough paper, and O(mlog⁡n+mnlog⁡nlog⁡log⁡n)O(m \sqrt{\log n} + \sqrt{mn \log n \log\log{n}}) (this 2026 follow up).

Given these bounds, there’s a broad area of the parameter space for mm as a function of nn where Dijkstra is better. So I invited my agents to figure out what’s possible if the weights were non-negative reals, and to prove correctness and efficiency using Lean, the formal verification tool.

Solution

After about 15 hours and 733 messages on the message board, the team had completed a proposed new algorithm for finding exact shortest-path distances in the directed graph setting. This algorithm, called C-HD, is presented in this Lean proof.

The algorithm handles local search which encounter unproductive edges quite well. It still uses priority comparisons, but a newly encountered vertex can count towards a search’s size limit as an unexplored leaf. The algorithm maintains local invariants (rules that stay true after each update), with careful edge deletion and a bounded local search. This enables it to achieve this bound within its certified range:

O ⁣(n+m+mlog⁡ ⁣(2+mn+1)+m1/3(nlog⁡(n+2))2/3).O\!\left(n+m+m\log\!\left(2+\frac{m}{n+1}\right)+m^{1/3}\bigl(n\log(n+2)\bigr)^{2/3}\right).

where n≥2n \ge 2 is the number of vertices in the input graph and mm is the number of edges. The certified range is m≤n⌊⌊log⁡2n⌋3/4⌋m\le n\lfloor\lfloor\log_2 n\rfloor^{3/4}\rfloor. For this analysis, I also add overhead of allocating memory, sorting edges, reading the input graph, and outputting results.

An intuitive explanation of why C-HD has a better bound than Dijkstra or the listed SOTA algorithms in the relevant regime is that it reduces repeated search and data-structure work. The idea is:

1. Start from the source and the current frontier of vertices.
2. Run bounded local searches along outgoing edges.
3. Count newly encountered vertices towards the search limit, including unexplored leaves when an edge does not improve a distance estimate.
4. Use the resulting search trees and pivots to organize the recursive work.

This deterministic procedure limits repeated work. The algorithm C-HD implements carefully handles local invariants so that even if it revisits the same endpoint/vertex a few times, repeated processing can be bounded. In this way, C-HD achieves a better bound on total work in the stated regime, even though it doesn’t know the order of visiting vertices beforehand. It still reads the entire input graph.

Note the algorithm relies on sorted outgoing-edge lists, which it constructs as part of its own charged preprocessing. To handle small inputs and inputs outside the certified density range, the agents added a separate algorithm, Bellman–Ford, with the O((n+1)(m+1))O((n+1)(m+1)) runtime bound, selected at the beginning of the execution. Bellman–Ford is not a variant of Dijkstra.

Below I show an excerpt from the theorem that was proved, along with the actual runtime target achieved.

-- From namespace Frontier.CHD.Final:
theorem chd_CHDTarget : GateCTarget.CHDTarget GateCCalc.F :=
  ⟨chdProgram, chd_exact_within.1,
    bodyC KcC + 65536 * 9 + 100, chd_exact_within.2⟩

theorem chd_gateC : Frontier.GateC :=
  GateCTarget.chdTarget_F_imp_gateC chd_CHDTarget


C_HD_bound, within the certified range:
O(n + m + m * log(2 + m/(n+1)) + m^(1/3) * (n*log(n+2))^(2/3))

To compare against prior work, let’s look at graphs with roughly m=nlog⁡3/4nm = n \log^{3/4} n edges. The runtime bound for Dijkstra is O(nlog⁡n)O(n \log n); the C-HD algorithm gets O(nlog⁡11/12n)O(n \log^{11/12} n). Though this seems like a minor improvement, it means that I’ve achieved a better asymptotic upper bound as these graphs grow.

For instance, if n=21000n = 2^{1000}, the ratio of the leading expressions nlog⁡2nn\log_2 n and n(log⁡2n)11/12n(\log_2 n)^{11/12} is 10001/12≈1.781000^{1/12}\approx1.78, ignoring constants and lower-order terms. This is not a measured speedup. This improvement scales polylogarithmically with the input size: squaring nn multiplies that ratio by 21/122^{1/12}.

Actual Performance

Of course, this is still only an upper bound of the complexity — a mathematical promise. It may be that even though the algorithm is theoretically better in this regime, it will actually perform worse when run. For this run, I ran small correctness simulations but did not benchmark the implementation on large real graphs. Based on my analysis, the approach has a better asymptotic bound than the listed prior bounds in the proved regime. The constants in the formal construction are enormous, so this does not establish a practical speedup.

Formal Verifications

I also successfully verified a bound on the performance of the algorithm within the certified range:

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

which simplifies to O(nlog⁡11/12n)O(n\log^{11/12}n) along the profile m≈nlog⁡3/4nm\approx n\log^{3/4}n.

I checked the proof using the Lean Comparator tool. The Lean proof establishes the runtime bound and a strict asymptotic improvement over nlog⁡nn\log n along the stated density profile. Substituting that profile into the published bounds also shows that the bound is smaller than mlog⁡2/3nm\log^{2/3}n and mlog⁡n+mnlog⁡nlog⁡log⁡nm\sqrt{\log n}+\sqrt{mn\log n\log\log n}.

The Comparator checks that the submitted proof proves the specified theorem, uses only permitted axioms, and is accepted by Lean’s kernel. This helps ensure the formal performance guarantee matches the stated target.

How much improvement does C-HD deliver?

If you’re thinking, “but how much time will this actually save?”, here’s what the proof establishes:

Along the profile m≈nlog⁡3/4nm\approx n\log^{3/4}n, the ratio of the leading bound expressions is (log⁡n)1/12(\log n)^{1/12}. The proof does not give measured runtimes or exact iteration counts for graphs with a trillion vertices. When m=10nm = 10n, the graph is in a different density regime, and this result does not establish an improvement over the best known bounds there.

Elicitation

If OpenAI’s Hugging Face incident and its Navier–Stokes result have taught me anything, it’s that agents can dramatically compress the time it takes to make progress on a problem. And one simple way to get agents to work together is to give them a way to talk to each other, i.e. a message board.

What I did here was spawn 10 Claude Opus 5.5 agents at maximum effort and give them a simple message board. They had initial roles, but could reorganize their work, share discoveries, challenge each other’s ideas, and shift effort toward whichever approach looked most promising.

I gave them somewhat of a long prompt explaining exactly what I was looking for: a substantial theoretical improvement for exact shortest paths on directed graphs with non-negative real weights, backed by a complete Lean proof. They could pursue several directions: remove logarithmic factors, find a better exponent, find a linear-time algorithm, or prove a fundamental lower bound on what any algorithm could achieve.

Lastly, I also asked them to compare their result against the recent papers, record failed approaches so other agents wouldn’t repeat them, and challenge each other’s claims. Before declaring success, they needed a reproducible Lean build and two separate peer reviews. If they couldn’t prove an improvement, they were told to preserve the partial progress and say what remained unresolved.

It’s fascinating what a team of agents can do. A country of geniuses in a datacenter; That prediction wasn’t too far off.

---

The full proof package (Lean sources, informal paper, and verification records) is available at github.com/spicylemonade/c-hd-proof.