The APSP hypothesis: are all-pairs shortest paths computable in truly subcubic time?
Given a directed graph on vertices with integer edge weights in and no negative cycles, compute all pairwise shortest-path distances. Floyd-Warshall does it in time, and decades of improvements removed only subpolynomial factors. The APSP hypothesis asserts that no algorithm on a word RAM with -bit words runs in time for any ; a large class of problems is subcubically equivalent to it. Is there a truly subcubic algorithm?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Fine-grained complexity; graph algorithms
- Posed by
- Virginia Vassilevska Williams and Ryan Williams (subcubic equivalences, FOCS 2010); the question of truly subcubic APSP is as old as Floyd-Warshall (1962)
- Year posed
- 2010
- Years open
- 16y
- Solved
- 2026-10-05
- Model
- Claude (internal Anthropic research model, unnamed)
- Vendor
- Anthropic
- Collaborators
- Josh Alman, Virginia Vassilevska Williams
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 55 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Yes: deterministic algorithms for APSP and for the (min,+)-product with polynomially bounded integer weights on the word RAM (the Lean development states ), and Exact Triangle in , refuting the APSP and Exact Triangle hypotheses; a Las Vegas version works for real weights. The core is a new thin-matrix-product algorithm solving Lopsided All-Edges Sparse Triangle, with known reductions giving the rest. The same paper refutes the 3SUM hypothesis, catalogued separately. The constants are enormous; the impact is on the theory of subcubic equivalences, not on practice. SETH and Orthogonal Vectors are unaffected.
What the AI did
From the abstract: "Claude, an AI model developed by Anthropic, discovered the algorithm that refutes the 3SUM, APSP, and Exact Triangle hypotheses." The methodology section adds that an Anthropic employee had set an internal research model to verify and improve cryptographic constructions based on the average-case hardness of Zero-k-Clique; instead it developed this algorithm, first for the average case and then the worst case, in one session of 16 million output tokens with no human input. Anthropic shared it with the authors in September 2026. Alman and Vassilevska Williams simplified, strengthened and extended it, derived further consequences and wrote the paper; an internal model later produced the Lean formalisation.
Verification
Read here on 6 October 2026, not rebuilt. The paper's Theorem 2 was compared with the standard hypotheses as its own introduction states them (word RAM with O(log n)-bit words, integers of absolute value n^O(1)) and matches. The Lean development (anthropics/formal-math, folder 3sum-apsp, commit e1a4e65; Lean 4.33.1 with mathlib, about 102,000 lines) proves correctness and running time of explicit programs on a word-RAM machine defined in Lean, a weaker machine than the standard word RAM, which only strengthens upper bounds. Its five headline claims are stated in a 139-line file with no imports. No sorry outside the deliberate Challenge folder, no axiom declarations, native_decide, implemented_by or unsafe. The statement file was written by the same party as the proof and has not been audited independently, and no Comparator run is recorded. No uninvolved expert has commented yet; the authors are the leading researchers of the area and are not independent reviewers.