Пакет формальных доказательств на Lean 4 для улучшенной оценки времени работы алгоритма кратчайших путей из одного источника.
Репозиторий — снимок от 20 сентября 2026 года с формальным доказательством теоремы об алгоритме поиска кратчайших путей из одного источника в ориентированном графе с неотрицательными весами. Доказанная оценка времени работы — O(n·log(n)^(11/12)) при определённом соотношении рёбер и вершин, есть проверенный запасной вариант на основе Bellman-Ford. Сборка и два независимых прогона ядра Lean подтвердили более 18 тысяч используемых утверждений.
Описание автора:C-HD: Lean 4 proof package for a directed single-source shortest-path bound (snapshot 2026-09-20)
