{"id":"palomar/PALOMAR-2026-10-08-000003","url":"https://github.com/qawbecrdtey/ImprovedExponents/tree/0725f2477587d67212936777b8a264c9793ac7bb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-08-000003-v1.json","repo":"https://github.com/qawbecrdtey/ImprovedExponents","tags":["cs.DS","cs.LO","msc:68Q25","msc:68W40","msc:68V20","fine-grained-complexity","3sum","apsp","lean-formalization"],"score":0,"title":"Improved exponents for 3SUM and APSP from triangles in sparse lopsided graphs","trust":"high","domain":"cs.DS","source":"palomar","authors":["Jihoon Hyun"],"reviews":0,"subject":"cs.DS","summary":"A sorry-free Lean 4 formalization of improved running-time exponents for 3SUM, Exact Triangle, the (min,+)-product and all-pairs shortest paths (APSP), on the word RAM of the published formalization (anthropics/formal-math, 3sum-apsp) of the paper of Alman and Vassilevska Williams, \"Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs\" (arXiv:2610.06783). That paper gives deterministic algorithms for 3SUM in time O(n^1.9992) and for the (min,+)-product and APSP in time O(n^2.99942), through Exact Triangle in time O(n^(3 - 0.0017)). The project analyzes the…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-08","reactions":{},"formalized":true}