OpenAI 矩阵乘法 ω≤9/4 证明被推广到任意域，Lean 形式化验证通过
thomasahle · x · 2026-10-07
一项新工作将 OpenAI 的快速矩阵乘法指数界 ω≤9/4 的 Lean 证明从复数域推广到任意域。作者 Sela Navot 在消费级 GPT-6 Astra 与 GPT-6.1 Sol 协助下找到并形式化了推广证明，Lean 检查通过，代码以 Apache-2.0 开源。
- 方法上的新颖点：新 FMM 论文一改以往「对 CW 张量取幂再裁剪」的路线，转而在张量上定义一个势函数（potential function），通过研究简单的卷积张量以反证法完成整个证明，被认为出乎意料地优雅。
- 意义：原证明只覆盖复数域，推广到任意域意味着结论的普适性更强；作者猜测 n^{9/4} 可能就是矩阵乘法真正的正确指数。
「研究」频道最新
- 新预印本：信息密集合成方法将生成模型带进化学分子发现 — anshulkundaje · 2026-10-07
- 用标准工具调用即可套出 GPT-6 等模型隐藏思维链 — jiqizhixin · 2026-10-07
- 新预印本：信息密集合成把分子发现实验数从 O(d) 降到 O(log d) — anshulkundaje · 2026-10-07
- UCLA 首次系统研究混合注意力 LLM 的多语言能力,发现层序可改 — UCLA · 2026-10-07
- NYU 提出 RGPO:自适应理由脚手架缓解 RL 奖励稀疏 — newyorkuniversity · 2026-10-07
- UCLA 借 MoE 路由输出做跨语言对齐,提升多语言性能 — UCLA · 2026-10-07