Ten Claude Opus 5.5 agents produce a Lean-verified shortest-path algorithm, C-HD