读遍 OpenAI 数学仓库 242 份 Lean 说明：至少 10 个头条结论未被形式化验证
MysteriousAvocado580 · reddit · 2026-10-11
一位 Reddit 用户逐条阅读了 OpenAI 数学仓库（openai/math，commit fd4aeeb，10 月 8 日）中 372 个结果家族里带「(Lean)」标注的 242 份 scope note，发现至少 10 个结果家族的说明明确写道：标题所称的核心结论并不在 Lean 形式化验证范围内，但标题仍保留「(Lean)」标注。
具体案例包括：
- #266「六维空间恰好三个互不偏基」：Lean 实际只证明了弱得多的界（每族至多 5 个成员）
- #195「小 Cohen–Macaulay 模猜想反例」：只验证了候选环本身，未证明其缺少该类模
- #312「Grothendieck 同伦假设」：只形式化了基础扩张定理，半模型结构与完整比较未包含
- #084「Erdős 相似性猜想几何情形」：标题称对所有 q∈(0,1) 成立，Lean 只覆盖 q=1/2
- 另有熵阈值、重建阈值、可分商问题独立性、量子密钥蒸馏等家族的头条主张都在形式化语句之外
作者强调这与已有的「Lean 验证的是某个语句而非原命题」的一般性批评不同：这是 OpenAI 自己的 scope note 明文承认头条结论超出形式化范围，却仍标注 (Lean)。其中 4 个家族（027、066、195、312）对应的论文也存在问题。
「研究」频道最新
- Lean 联合创始人 Avigad 长谈：AI、形式验证与数学未来 — EchoShao8899 · 2026-10-11
- NeurIPS 2026 位置论文：LLM 缺乏认知控制机制，难达长期自主 — AndrewLampinen · 2026-10-11
- 基于 Jacobian Lens 开源 PENDULUM，模型可解释性工具换上新 UI — Extraaltodeus · 2026-10-11
- 东南大学团队 LeaP 被 CoRL 2026 接收:让扩散动作生成的起始分布随机器人状态自适应 — jiqizhixin · 2026-10-11
- 手把手教程：不依赖大模型，自己搭一个决策模型 — softwaredoug · 2026-10-11
- Krea2 Turbo 2 步蒸馏 LoRA 终版：速度 4 倍，细节达教师模型 92% — TimeTruth2490 · 2026-10-11