Un equipo de diez agentes de IA, coordinados mediante un tablero de mensajes, ha desarrollado un nuevo algoritmo determinista llamado C-HD para calcular distancias de caminos más cortos en grafos dirigidos con pesos reales no negativos. Este avance, respaldado por una verificación formal completa en el lenguaje Lean, logra un límite superior de complejidad asintótica que supera al del clásico algoritmo de Dijkstra en ciertos regímenes de densidad del grafo. El nuevo método, presentado en un repositorio de GitHub, reduce la redundancia en el procesamiento de nodos mediante búsquedas locales acotadas y invariantes locales, logrando una mejora teórica de un factor polilogarítmico en grafos con aproximadamente m² aristas. Aunque el límite teórico es superior, los constantes en la construcción formal son enormes, lo que impide confirmar una aceleración práctica inmediata en implementaciones reales. El proyecto destaca la capacidad de los agentes de IA para colaborar de forma autónoma, compartiendo descubrimientos y validando pruebas matemáticas, un enfoque que ha demostrado ser eficaz para resolver problemas complejos de teoría de la computación en un tiempo reducido.
