主要证据
- Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided GraphsS1 · 主要研究来源 · 论文 · 2026-10-05
- Truly Subquadratic 3SUM and Truly Subcubic APSP — Lean 4 formalizationS1 · 主要研究来源 · 形式化工件
Claude 被归因于发现真正次二次 3SUM 与真正次三次 APSP 算法
论文的方法部分说明，Anthropic 员工最初让内部研究模型研究一个基于 average-case Zero-k-Clique 的密码学问题。Claude 在约 1,600 万 output tokens、无人类输入的 session 中意外发展出新算法，先处理平均情形，再推广到最坏情形。
发生了什么？
Alman 与 Vassilevska Williams 报告 deterministic algorithms：在其 word-RAM 模型中，对多项式大小整数输入的 3SUM 达到 O(n^1.9992)，对多项式有界整数权重的 APSP 达到 O(n^2.99942)，并同时改进 Exact Triangle、min-plus product 与 zero-weight k-Clique。论文称这些是在相应设定下首次真正次二次与真正次三次算法， 并由此推翻 fine-grained complexity 中常用的 3SUM 与 APSP hypotheses。
论文的方法部分说明，Anthropic 员工最初让内部研究模型研究一个基于 average-case Zero-k-Clique 的密码学问题。Claude 在约 1,600 万 output tokens、无人类输入的 session 中意外发展出新算法，先处理平均情形，再推广到最坏情形。Anthropic 将结果 提供给 Alman 与 Vassilevska Williams；两位作者随后重新理解论证、简化方法、 改进常数与指数、推出更多后果并撰写论文。论文完成后，Anthropic 又使用研究模型 把主要 deterministic claims 形式化到 Lean 中。
为什么重要？
本事件为“前沿数学算法由长程自主模型运行产生、随后经专家重新理解”的过程提供了罕见的 明确 provenance。它不是 benchmark 提升，而是改变 fine-grained complexity 的 猜想格局，并迫使研究者重新审视建立在 3SUM 与 APSP 假设上的归约和困难性框架。 配套 Lean artifact 还使部分 headline claims 可以接受机械检查。
重要性说明：该结果被列为 Historical Milestone，因为它报告了 3SUM 与 APSP 的首次多项式级 指数改进，而这两个问题长期以来的近二次与近三次复杂度假设塑造了 fine-grained complexity 的研究框架。论文把核心算法发现归因于一个 Anthropic 研究模型在无人类 输入的长程 session 中完成；随后 Josh Alman 与 Virginia Vassilevska Williams 独立理解、简化、强化并扩展该方法。Anthropic 又公开了主要 deterministic claims 的大规模 Lean 形式化。
历史脉络
更早进展
—
后续进展
—
相关里程碑
—
证据与状态一览
- 重要性
- H1 · 历史里程碑
- 验证状态
- 核验中
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 新结果
- 接口
- 非形式化, 形式化, 符号, 混合
- AI 贡献
- 论文把核心算法发现归因于 Anthropic 研究模型在约 1,600 万 output tokens 且 无人类输入的 session 中完成。人类作者随后独立理解该方法、简化并强化论证、 推出新的后果，并对最终论文负责。该分类描述的是公开披露的发现流程，并不表示 最终论文中的每个定理和阐释选择都由模型完成。
- 人类贡献
- Josh Alman 与 Virginia Vassilevska Williams 重新构建模型算法、简化并强化方法、 改进定量界、发展进一步后果并撰写论文；Anthropic 研究人员提供模型运行以及后续 形式化基础设施。
- 验证状态
- 核验中 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-10-07
技术细节
- 系统
- claude, lean, comparator, nanoda
- 机构
- anthropic
- 数学问题
- three-sum, all-pairs-shortest-paths
- 方法
- fine-grained-algorithms, sparse-lopsided-triangles, word-ram, formal-verification
全部来源与工件
- Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided GraphsS1 · 主要研究来源 · 论文 · 访问于 2026-10-07
- Truly Subquadratic 3SUM and Truly Subcubic APSP — Lean 4 formalizationS1 · 主要研究来源 · 形式化工件 · 访问于 2026-10-07
验证历史
- 2026-10-05 · 论文已发布 · E2 · 研究记录
研究论文公开陈述算法结果，并明确记录 AI 发现流程及随后的人类重建过程。
- 2026-10-07 · 核验中 · E3 · 可检查工件
Anthropic 的公开 Lean 项目证明五项 headline deterministic claims，其中包括 3SUM 与 APSP 的 word-RAM 界，并记录 Comparator/Nanoda 检查流程。仓库也明确 列出未在同一机器模型中形式化的论文主张。Chronicle 尚未找到足以支持 independently_verified 状态的外部独立重放或专业审查。
更正
当前没有记录的更正。