Contexte technique

Le problème du plus court chemin consiste à déterminer, dans un graphe orienté à poids réels non négatifs, la distance minimale depuis une source vers chaque sommet. L’algorithme de Dijkstra, avec une file de priorité adaptée (par exemple un tas de Fibonacci), atteint la borne O(m + n log n) où n désigne le nombre de sommets et m le nombre d’arêtes. Des travaux récents (2025, 2026) ont proposé des algorithmes déterministes avec des complexités O(m log^{2/3} n) ou O(m log n + m n log n log log n), mais ces bornes ne sont avantageuses que dans certaines régions du plan (m en fonction de n).

Description de l’algorithme C‑HD

Après quinze heures de collaboration entre dix agents Claude Opus 5.5, un nouveau procédé nommé C‑HD a été formalisé et vérifié dans le système de preuve Lean. L’algorithme conserve la phase de recherche locale, mais chaque sommet nouvellement découvert compte comme une feuille non explorée, limitant ainsi la taille de la recherche. Il maintient des invariants locaux grâce à une suppression d’arêtes contrôlée et à une organisation hiérarchique des arbres de recherche. Le pré‑traitement consiste à trier les listes d’arêtes sortantes, opération facturée explicitement dans le modèle de coût.

theorem chd_CHDTarget : GateCTarget.CHDTarget GateCCalc.F := ⟨chdProgram, chd_exact_within.1, bodyC KcC + 65536 * 9 + 100, chd_exact_within.2⟩

Ce fragment montre la déclaration Lean du théorème principal, liant le programme chdProgram à la cible de complexité CHDTarget et incluant les constantes de surcharge introduites par la vérification.

Analyse de la complexité

Dans la plage certifiée m ≤ n ⌊⌊log₂ n⌋^{3/4}⌋, C‑HD atteint la borne
O(n + m + m·log(2 + m/(n+1)) + m^{1/3}(n·log(n+2))^{2/3}).
En considérant le cas typique m ≈ n·log^{3/4} n, cette expression se simplifie en O(n·log^{11/12} n), alors que Dijkstra reste à O(n·log n). La différence provient du facteur log^{11/12} n, qui croît plus lentement que log n. L’amélioration est purement asymptotique : elle se manifeste uniquement lorsque n devient exponentiellement grand (par exemple n = 2^{1000}, où le rapport des termes dominants vaut environ 1,78).

Pour les graphes en dehors de la densité certifiée, C‑HD bascule automatiquement vers Bellman‑Ford, dont la complexité O((n+1)(m+1)) garantit la correction sans compromettre la preuve formelle.

Limitations et perspectives

La preuve formelle ne fournit qu’une promesse d’ordre supérieur ; les constantes cachées dans le modèle de coût sont très élevées, ce qui rend improbable un gain de performance observable sur des instances réelles. Aucun benchmark pratique n’a été réalisé, et l’algorithme nécessite le tri préalable des arêtes, opération qui peut dominer le temps d’exécution pour des graphes peu denses. De plus, la portée de la certification est restreinte à la région m ≤ n·log^{3/4} n. Au‑delà, le recours à Bellman‑Ford rétablit la complexité quadratique.

Malgré ces réserves, C‑HD constitue une première démonstration que la vérification assistée peut conduire à des améliorations théoriques mesurables dans un problème fondamental de l’informatique. Les travaux futurs pourraient viser à réduire les constantes de la construction Lean, à étendre la plage certifiée et à implémenter un prototype performant pour valider empiriquement les gains asymptotiques.