What was already known
The Alman–Vassilevska Williams paper and Anthropic formalization gave deterministic 3SUM O(n^1.9992) and APSP O(n^2.99942) in the same scoped word RAM model. Their algorithmic framework, reductions and core sparse-lopsided triangle method are the starting point.
AI involvement
The maintainer states Claude Fable 5.1 wrote every new Lean, Python and LaTeX line and derived the new cost refinements under his direction. He chose the goals and reviewed outputs; the original algorithmic framework came from Alman and Vassilevska Williams.
Jihoon Hyun chose the paper, goals and statement framing, while Claude wrote all new Lean, Python and LaTeX and derived the exact leaf-count, true middle-size, pruned-encoding and all-edges refinements. Alman and Vassilevska Williams supplied the original algorithmic framework.
Importance
Tightens exponents within a recent AI-assisted framework and formally checks the added cost analysis and reductions. It is an incremental improvement rather than a new refutation of the 3SUM or APSP hypotheses.
Limitations
Jihoon Hyun chose the source paper, goals and statement framing, while Claude wrote all new code and manuscript material under his direction. The project reuses a pinned port of Anthropic’s upstream formalization; the algorithmic framework belongs to Alman and Vassilevska Williams. The source reports Comparator acceptance with Lean, NanoDa and con-ron. A separate Oct 7 expert blog reports a similar AI-suggested 3SUM numerical improvement but later removed its details, so this record does not claim sole priority for the 1.99896 exponent. The result has not been assessed for practical performance.
Technical verification
The source reports successful Lean and Comparator checks of the new exact statements on the pinned upstream word RAM model, with NanoDa and con-ron independent kernel replay. AIProofWatch did not rerun the checks.
Formal checking
Source reports Oct 7 Comparator acceptance with Lean kernel, NanoDa and con-ron for exact matched statements.
- Checker
- Lean 4 Comparator, NanoDa and con-ron as run by the project maintainer
- Scope
- 3SUM O(n^1.99896) and APSP O(n^2.99791) on the pinned upstream word RAM model with polynomially bounded integer inputs
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Hyun reports reviewing model outputs but the available source does not document a human explanation of the cost refinements or their proof. Few is the evidence default, not a claim that humans cannot understand them.
Correction and publication history
Claim-level review of incremental AI-generated improvements, exact formal model, upstream human/AI credit, source-reported complete checks and contemporaneous priority caveat.
Read this published revision