{"id":"lean/anthropics__formal-math__3sum-apsp","url":"https://github.com/anthropics/formal-math/tree/main/3sum-apsp","repo":"https://github.com/anthropics/formal-math","tags":["3sum","apsp","lean4","formal-verification","fine-grained-complexity"],"score":1,"title":"Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization","source":"lean","authors":["anthropics"],"reviews":0,"subject":"cs.DS","summary":"This formalization accompanies the paper *Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs* by Josh Alman and Virginia Vassilevska Williams. It states results of the paper as theorems of Lean 4, in the paper's notation and numbering, and proves these theorems.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-08-06","reactions":{"up":1,"👍":1},"formalized":true}