Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Truly subcubic all-pairs shortest paths

Lax350013.APSP · concepts/Lax350013/APSP.lean · lax-350013

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    All-pairs shortest paths in a directed graph with nn vertices, polynomially bounded integer edge weights and no negative cycles can be computed deterministically in O(n2.99942)O(n^{2.99942}) word-RAM steps (Theorem 22). Each output pair contains a reachability flag and, when reachable, the minimum weight of a path. Paths may repeat vertices.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Lax350013.PolynomialTime
    15
    16/-!
    17---
    18title: Truly subcubic all-pairs shortest paths
    19type: theorem
    20---
    21All-pairs shortest paths in a directed graph with nn vertices, polynomially bounded integer edge weights and no negative cycles can be computed deterministically in O(n2.99942)O(n^{2.99942}) word-RAM steps (Theorem 22). Each output pair contains a reachability flag and, when reachable, the minimum weight of a path. Paths may repeat vertices.
    22-/
    23
    24namespace Lax350013.APSP
    25
    26open Lax350013.PolynomialTime
    27
    28/-- A path and its total weight; it may repeat vertices. -/
    29inductive Path {n : Nat} (w : Fin n → Fin n → Option Int) : Fin n → Fin n → Int → Prop
    30 | nil (i : Fin n) : Path w i i 0
    31 | cons {i j k : Fin n} {d e : Int} : w i j = some d → Path w j k e → Path w i k (d + e)
    32
    33/-- Input: the 0/1 matrix of the edges, then the weights, with 0 for no edge. Output, two cells for each `(i, j)`: 1 if
    34there is a path, else 0; then the distance. -/
    35def APSP : Problem where
    36 Instance n := {w : Fin n → Fin n → Option Int // ∀ i d, Path w i i d → 0 ≤ d}
    37 input := fun ⟨w, _⟩ => rowByRow (fun i j => if (w i j).isSome then 1 else 0) ++ rowByRow fun i j => (w i j).getD 0
    38 output := fun {n} ⟨w, _⟩ out => ∀ i j : Fin n,
    39 let flag := out (2 * (i.val * n + j.val))
    40 let dist := out (2 * (i.val * n + j.val) + 1)
    41 (flag = 1 ∧ Path w i j dist ∧ ∀ e, Path w i j e → dist ≤ e) ∨ (flag = 0 ∧ ∀ e, ¬ Path w i j e)
    42
    43/-- Theorem 22: «APSP on directed n-vertex graphs … and no negative cycles», in time «O(n^2.99942)». -/
    44def Theorem_22_APSP : Prop :=
    45 APSP.SolvedInTime 2.99942
    46
    47/-- Truly subcubic all-pairs shortest paths: Theorem 22 APSP. -/
    48axiom algorithm : Theorem_22_APSP
    49
    50end Lax350013.APSP
    51
    Show Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…