Lean証明器のカーネル健全性バグ#14576事後分析

Lean証明器の開発者Leonardo de Mouraが、2026年8月1日付けでカーネル健全性バグ#14576の詳細な事後分析を公開した。

発端は2026年7月25日、Ramana KumarがAIの支援を受けて生成したsorry-freeの「Collatz予想反証」リポジトリを公開したことだ。これは有効な証明ではなく、カーネルのネスト帰納型処理のバグを悪用したものだった。7月28日、Kiran Gopinathan がそれを小さなFalseの証明に絞り込んでissue #14576を開き、報告から1時間以内に修正コミット#14577がプッシュされた。Joachim Breitnerのレビューと改善提案を経てマージされ、パッチリリースが公開された。

バグの技術的詳細：カーネルがパラメータDsを持つ帰納型Tの下でネストされた出現を除去する際、これらのパラメータがコンストラクタフィールドで参照されないファントム型の場合、生成される補助型から消えてしまい型検査を逃れる。この結果、不正な型の引数を通じてカーネルにFalseの証明を受け入れさせることが可能となる。このバグはメタプログラミング経由でのみ到達可能で、フロントエンドは引数を検査するため通常は防がれる。これはLeanのメタ理論の欠陥ではなく実装上のバグである。

独立外部チェッカーのnanodaも関連バグの影響を受けていた。nanodaはChris Baileyが開発したRust製の独立カーネルだが、2つの無関係なバグが絡み合っており、Lean公式カーネルはネスト帰納型のチェックが欠如し、nanodaはプロジェクションノードの型名検証が不足していた。nanodaのバグはJeremy Chenによって報告され、Leanバグ報告の約1週間前に修正済みだった。

Mario Carneiroのlean4leanはLeanの型理論の形式化プロジェクトだが、帰納型の検証はまだ未完のため同バグが含まれていた。

メタプログラミングを制限すべきという提案についてde Mouraは「誤った方向性」と明示し、カーネルは信頼されていないコンポーネントとは独立して不正な宣言を拒否しなければならないと述べた。FROは再現テストをKernel Arenaに追加し、後続PR #14582でパラメータの振る舞いを検証する追加チェックを実装している。