The 3SUM hypothesis: is 3SUM solvable in truly subquadratic time?
Given integers in , decide whether three of them sum to zero. The 3SUM hypothesis asserts that no algorithm on a word RAM with -bit words solves this in time for any . Hundreds of conditional lower bounds in computational geometry and fine-grained complexity rest on it. Is there a truly subquadratic algorithm?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Fine-grained complexity; algorithms
- Posed by
- Anka Gajentaan and Mark Overmars (3SUM-hardness, 1995); the integer word-RAM form as used today is Patrascu's (2010)
- Year posed
- 1995
- Years open
- 31y
- 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
- 50 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Yes: a deterministic algorithm for 3SUM on polynomially bounded integers on the word RAM, refuting the hypothesis, and a Las Vegas algorithm for real inputs using only additions, subtractions and comparisons. The core is a new algorithm for wanted entries of thin matrix products (a modified Coppersmith rectangular algorithm with a Schönhage identity), which solves Lopsided All-Edges Sparse Triangle; known reductions give 3SUM. The same paper refutes the APSP hypothesis, catalogued separately. The constants are enormous, so the impact is on the theory: the conditional lower bounds built on 3SUM no longer stand as stated. 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.