Ten agents, a message board and a Lean gate produce a checked shortest-path bound

Jaff writes that he chose to "spawn 10 Claude Opus 5.5 agents at maximum effort and give them a simple message board." The agents started with assigned roles but could reorganize. They were told to record failed approaches so others would not repeat them, and they could not declare success without "a reproducible Lean build and two separate peer reviews." After about 15 hours and 733 messages they produced C-HD, an algorithm for exact single-source shortest paths on directed graphs with non-negative real weights. Its proved bound along one density profile is O(n log^(11/12) n), against O(n log n) for Dijkstra. Jaff states the limits himself: "This is not a measured speedup." The constants are enormous, and the result says nothing about denser graphs such as m = 10n.

The proof package on GitHub is more careful than the post on one point. Its README reports that the full build passed (2,548 jobs) and that two kernel replays each checked 18,994 constants. It also says the two reviews "are reviews by the research agents, not outside peer review," that the second is a snapshot with reproduction fields still pending, and that novelty is a matter for external experts. We read the README; we did not rebuild the proof. The post is dated September 20 and names Claude Opus 5.5, which Anthropic announced on September 22. It does not say how the author had access. The Hacker News submission had 29 points and 7 comments at about 22:10 UTC.

Why it matters: The part that held up is the part no agent could argue with: the Lean kernel accepts the theorem or it does not. The review step, by the package's own account, was agents grading agents. If you run a multi-agent loop on work that matters, put a mechanical check at the finish line and do not let agent-to-agent review stand in for it.