社区 6 天用 Lean 形式化 OpenAI 次线性乘法结果

开发者 platypii 发起项目，将 OpenAI 的整数乘法 sub-n log n 复杂度结果形式化为 Lean 证明，并在 jdb1729 协助下仅用 6 天完成，涉及 248 个模块、约 13 万行代码。0xdoug 评价称这「令人难以置信」，因为同类形式化工作通常需要数年，而 Lean 在数学界已相当普及，这一速度展示了社区协作与形式化工具的潜力。

2026-10-16 ~ 2026-10-16 · 2 条相关

• 同类工作常需数年，这次 6 天搞定：Lean 形式化为何这么难 — RexDouglass · 2026-10-16
• 6 天用 Lean 证完 OpenAI 次线性乘法结果，248 模块 13 万行代码 — RexDouglass · 2026-10-16