10 агентов Claude за 15 часов доказали в Lean алгоритм быстрее Дейкстры
A Faster Shortest Path Algorithm
Автор запустил 10 агентов Claude Opus 5.5 на общей доске сообщений, чтобы найти точный алгоритм кратчайших путей для ориентированных графов с неотрицательными весами. За 15 часов и 733 сообщения команда предложила алгоритм C-HD с асимптотической оценкой O(n(log n)^{11/12}) на профиле m ≈ n(log n)^{3/4}, что строго быстрее Дейкстры. Полное доказательство проверено в Lean с помощью Comparator. Практического ускорения нет — константы огромны.
Если инцидент OpenAI с Hugging Face и его результат по Навье–Стоксу меня чему-то и научили, так это тому, что агенты могут радикально сократить время, необходимое для прогресса в решении задачи.