OpenAI 仓库 8 个 Lean 形式化被指「坏掉」，错误证明也能过验证
AlexTensor · x · 2026-10-09
@Timeroot 指出 OpenAI 仓库中 8 个 Lean 形式化存在问题：可以用错误证明「平凡地证出来」。引用者 @KyleCranmer 补充说明，指控并非证明本身有错，而是验证流程可被 hack——定义被加入了白名单因而可被覆写，导致错误的证明仍能通过形式验证。
这对依赖 Lean/formal verification 的 AI 数学证明工作流（如 LLM 自动形式化验证）是一个值得警惕的信号：验证器的配置与定义管理可能成为漏洞来源。
所属事件:OpenAI Lean 形式化题库被曝漏洞，8 题可用错误证明通过(3 条相关)→
「研究」频道最新
- Simons 研究所 2027 秋启动扩散模型与流学期项目,博士后招募开启 — giannis_daras · 2026-10-10
- 前 OpenAI Operator 研究员展示真实世界 RL 高精度任务训练成果 — ZhaoMandi · 2026-10-10
- 斯坦福 Mulligan:瞄准失败初始状态采数据,2550 次盲评超越均匀采集 — ZhaoMandi · 2026-10-10
- 随机对照试验:AI 当辅导老师提升成绩并持续,代写则一周后效果消退 — emollick · 2026-10-10
- Nvidia 发布 ARC：不加新数据不改架构，机器人推理成功率提升 5 倍 — arankomatsuzaki · 2026-10-10
- 警惕 AI 解释出错:归因分数校验法 Captum 误差达 1,Tangermeme 仅 10⁻⁷ — bravo_abad · 2026-10-10