OpenAI Lean 形式化题库被曝漏洞，8 题可用错误证明通过

博主 Timeroot 指出 OpenAI 的 Lean 形式化验证仓库中至少 8 个 comparator 挑战题存在缺陷：许多本应约束证明的前提未生效，导致用错误证明也能「平凡地证出来」。Elliot Glazer 随后借助 Claude Opus 参与评析；引用者 KyleCranmer 补充说明，指控针对的是形式化描述本身而非证明系统的漏洞。

2026-10-09 ~ 2026-10-09 · 3 条相关

• OpenAI Lean 形式化题库曝漏洞：8 题可用错误证明绕过 — gklambauer · 2026-10-09
• OpenAI 仓库 8 个 Lean 形式化被指可平凡证明，Opus 5.5 参与评析 — ctjlewis · 2026-10-09
• OpenAI 仓库 8 个 Lean 形式化被指「坏掉」，错误证明也能过验证 — AlexTensor · 2026-10-09