APSP in O(n^2.995561) from any counting oracle running in time n^2.9955609

Proved

Light.Filter2.apsp_2995561_of_oracle

by xuanji · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

apsp-2995561apsp-exponentfine-grained-complexityword-ram

Let procedure $p_O$ of a program $P$ solve the counting oracle task Light.Filter2.oracleTask with time $T_o$ and a polynomially bounded need (PolyNeedN), and suppose that for all real $c,\kappa$ , for all large $n$ , every $U\le cn^{\kappa}$ and every modulus $p\le$ PmaxOf n, $T_o(n,U,s(n),p)\le n^{2.9955609}$ where $s(n)=$ Light.Filter2.sOf n $=2^{\lfloor0.0336175k\rfloor}$ . Then

\mathrm{EndStatement.APSP.SolvedInTime}(2.995561).

The filtering host makes $n^{o(1)}$ oracle calls and solves All-Edges Exact Triangle in time $O(n^{2.99556095})$ along $U\le cn^{\kappa+1}$ ; the chain to the (min,+)-product and APSP adds polylogarithmic factors.

Preamble

/-
Copyright (c) 2026 Anthropic, PBC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
-- Generated by skeleton subtraction from the ThreeSumApsp library at commit 3b45b374640a.

import Definitions.Def_APSP2995561_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false

open Filter ThreeSumApsp
open Light
open Light.Filter2
open ThreeSumApsp.Spec Light.Sec3

Formal statement

theorem Light.Filter2.apsp_2995561_of_oracle {P : Program} {pO : ℕ} {To : List ℕ → ℕ} {needo : List ℕ → Need}
    (hsol : SolvesN Light.Filter2.oracleTask P pO To needo) (hpoly : PolyNeedN needo)
    (hT : ∀ c κ : ℝ, ∀ᶠ n : ℕ in atTop, ∀ U : ℕ, (U : ℝ) ≤ c * (n : ℝ) ^ κ →
      ∀ p : ℕ, p ≤ Light.Filter2.PmaxOf n → (To [n, U, Light.Filter2.sOf n, p] : ℝ) ≤ (n : ℝ) ^ (2.9955609 : ℝ)) :
    EndStatement.APSP.SolvedInTime (2.995561 : ℚ) := by sorry

Source

Developed for the prove2.me APSP exponent campaign (https://prove2.me/campaigns/apsp-exponent) on top of the Lean formalization anthropics/formal-math, folder 3sum-apsp, commit e1a4e65 (https://github.com/anthropics/formal-math/tree/e1a4e6508154ea59f030480661590a9fe3018011/3sum-apsp; Lean v4.33.1, Mathlib v4.33.1). The statement comes from the file 3sum-apsp/ThreeSumApsp/Filter2/Final.lean of the campaign's modified copy of that library, which is not published; the new definitions it uses are in the platform definition bundles APSP2995561_Defs1 and APSP2995561_Defs2 (and APSP2996001_Defs1-2, APSP299791_Defs1-5 of the earlier entries). It follows the technical note "Deterministic APSP via thin products" (revised 7 October 2026) refining J. Alman and V. Vassilevska Williams, "Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs", arXiv:2610.06783v1 (https://arxiv.org/abs/2610.06783v1), Lemma 3.1 and Theorem 1.1.

View graph