Open Research Index

Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization

anthropics

Lean projectlean/anthropics__formal-math__3sum-apspAug 6, 2026cs.DSscore 1👍 1

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/lean/anthropics__formal-math__3sum-apsp
curl -X POST /api/v1/records/lean/anthropics__formal-math__3sum-apsp/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/lean/anthropics__formal-math__3sum-apsp/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'