Lean カーネルの健全性バグ #14576、ネストされた帰納型の型検査漏れで False の証明が可能に

要約

Lean カーネルに型検査の脆弱性が発見され、7 月 28 日に修正された。バグは帰納型の phantom パラメータ (コンストラクタで使われない引数) が生成される補助型から消失し、型検査をすり抜けられる仕組みだった。メタプログラミング経由でのみ到達可能で、フロントエンドの検査は機能していたが、カーネル自体は不正な型付けの宣言を受け入れてしまった。同様のバグが他に 6 件見つかり、すべて修正済み。