Leanカーネルの健全性バグは修正済み、独立チェッカーも最新版が必要
これは何?Leanは、証明項を小さな信頼済みカーネルで型検査する定理証明支援系です。
入れ子の帰納型でphantom parameterが補助型から消え、metaprogrammingから不正な宣言を直接渡すとLeanカーネルがFalseの証明を受理する実装バグが報告されました。Issue #14576はopenから1時間で修正PRが作られ、merge済みでpatch releaseも公開されています。通常のfrontendは不正項を拒否し、Leanのmeta-theoryの穴ではありません。
proof checkerの信頼境界はelaboratorの制限では代替できず、kernel自身が不正な項を拒否する必要があります。独立実装も同じ入力群による継続的な差分検査と迅速な更新がなければ、二重化だけでは十分ではありません。
- 読むべき人
- 形式手法・定理証明の利用者、compiler・kernel開発者、AI生成証明を検証する研究者
- HN
- 114 points / 40 comments