OpenAI 数学仓库新增 6 个 Lean 形式化,已覆盖约 42% 顶线结果
petrusenko_max · x · 2026-10-09
OpenAI 更新其 GitHub 数学形式化仓库:新增 6 个 Lean 形式化、19 处修改,并撤下三篇稿件(包括关于 Weil 类和 K3 曲面的内容)。目前该仓库已形式化约 42% 的顶线(top-line)结果,反映 OpenAI 在自动定理证明/数学形式化方向上的持续推进。
所属事件:OpenAI 数学仓库因符号错误撤回 3 篇霍奇猜想论文(5 条相关)→
「研究」频道最新
- TIDE 论文:把训练数据归因蒸馏成低维嵌入,查询即最近邻 — serrjoa · 2026-10-09
- DeepMind 报告：1500 万次 Gemini 交互揭示科学家如何用 AI 加速发现 — JMateosGarcia · 2026-10-09
- ENPIRE 让编码 Agent 自主做机器人研究,灵巧任务成功率 99% — chris_j_paxton · 2026-10-09
- ICLR 2027 让 AC 自查审稿人冲突，被指根本无从下手 — shaohua0116 · 2026-10-09
- Dietterich 谈 OpenAI 数学模型：像整理已故数学家的笔记 — tdietterich · 2026-10-09
- 论文：写明罚款反而让 AI 智能体更不守规矩，合规率差 46 个百分点 — niloofar_mire · 2026-10-09