6 天用 Lean 证完 OpenAI 次线性乘法结果，248 模块 13 万行代码
RexDouglass · x · 2026-10-16
platypii 发起项目，将 OpenAI 的整数乘法 sub-n log n 复杂度结果形式化为 Lean 证明，6 天后在 jdb1729 协助下完成。附论文摘要显示：证明针对 Mathlib 的 Turing.FinTM2 多带图灵机，验证了 CRT 重排、chrip 乘积、复卷积等每个阶段都有显式步数上界，总计 O(n(log n)^(1-κ))；开发包含 248 个模块、134,932 行代码，主定理仅依赖 propext、Classical.choice 和 Quot.sound。
所属事件:社区 6 天用 Lean 形式化 OpenAI 次线性乘法结果(2 条相关)→
「研究」频道最新
- TUM 发布 Tadpole：自编码器当 3D PDE 基础模型，NeurIPS 论文 — jiqizhixin · 2026-10-23
- Arc Institute 发布 COMPASS:用基因组语言模型绘制非编码 DNA 功能图谱 — anshulkundaje · 2026-10-23
- FDA 批准个性化新抗原癌症疫苗：每位患者产品皆不同 — alex_peys · 2026-10-23
- VIPerturb-seq 更新:10x Genomics 将推商业化单细胞 CRISPR 筛选产品 — anshulkundaje · 2026-10-23
- 新论文用二次模型复现 Transformer 训练 loss 尖峰，直指成因本质 — CSProfKGD · 2026-10-23
- 扩散模型教科书团队将把教程升级为 NeurIPS 2026 扩散 LLM 专场 — mittu1204 · 2026-10-23