研究者列举 AI 生成 LEAN 证明的四种翻车方式

研究者 gklambauer 在系列帖子中列举 AI 辅助 LEAN 形式化证明可能出问题的四种情形：一是形式化了另一个问题，证明的并非论文声称的问题；二是形式化偏差未被核查，并点名 OpenAI 存在此类问题；三是证明本身正确但「外星化」到人类难以解读；四是利用 LEAN kernel 的 bug，形式上通过实为错误。该系列提醒社区不能盲信 AI 生成的形式化证明。

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