Lean カーネル健全性バグ（#14576）の発生、修正，そして対策について

2026 年 8 月 1 日時点で確認されている事実です。Lean のカーネルにおける健全性バグ（Issue #14576）は、7 月 27 週間に報告され、速やかに修正されました。この出来事は、Zulip や X、LinkedIn、Mastodon などのソーシャルメディア上で広く共有されました。

---

何が起きたか？

事象の経過

• 7 月 25 日
  • Ramana Kumar 氏（AI の支援を得て）が、Collatz 予想に対する「反証」を含むリポジトリを公開しました。
  • 提供されたコードには

    sorry

    が含まれておらず、正当な証明ではなかったことが後に判明しました。
• 7 月 28 日
  • Kiran Gopinathan 氏が、この事実を示す簡潔な証明へと簡約化を行いました。
  • 問題報告 #14576 を発行し、わずか 1 時間後に修正パッチ（PR #14577）をマージしました。
  • Joachim Breitner 氏のレビューおよび改善提案を受け、新しいパッチ版がリリースされました。

バグの技術的詳細

• 原因:
  • カーネルが帰納型

    T

    のパラメータ

    Ds

    下にあるネストされた出現（occurrence）を展開する際、これらのパラメータが**幻影的（phantom）**である場合（つまり、コンストラクタのフィールドには現れない）、生成される補助型からそれらが消えてしまいました。
  • その結果、型チェックが回避され、型付けされていない不正な引数を「偽」の証明として受け付ける状態になりました。
• 発生条件:
  • メタプログラミング（Elaborator）を通じてのみ到達可能な脆弱性です。
  • 帰納型の宣言を直接カーネルに送ることで誘発されます（フロントエンド側では通常、型付けされていない項が検出されるため）。
• 本質:
  • これは実装上のバグであり、Lean のメタ理論の欠陥ではありません。

---

なぜ nanoda で検出されなかったのか？

検証ツールの状況

• nanoda の概要:
  • Chris Bailey 氏による Rust 実装の独立したカーネル（証明・型チェッカー）。
  • リポジトリは、主要チェッカーである nanoda の1 ヶ月前のバージョンでも通過しました。
• 二重のバグ:
  • 公式カーネル: ネストされた帰納型のサポートにおけるチェックが不足していました。
  • nanoda: 該当箇所をチェックしていましたが、プロジェクションノード（projection node）内の型名確認処理が行われていませんでした。

偶然か？

• Jeremy Chen 氏の指摘:
  • nanoda のバグは証明が公開される 1 ヶ月前に修正されていました。
  • この証明は、カーネルが決して検査しない表現を生成しており、当時の旧バージョンの nanoda はこれを許容していました。
• Joachim Breitner 氏の分析:
  • Ramana 氏はタイミングを偶然と捉えていますが、モデルが nanoda の報告を学習していた可能性も否定し難いと指摘しています。
  • 強い AI モデルは、単なる偶然によるタイムラグではなく、特定のバグを検出する能力を持つと考えられています。

実用的な影響

• 独立したカーネルを用いた検証は依然として有効です（2 つの実装にまたがる異なるバグが必要だったため）。
• 条件: この手法を利用するには、両方の最新バージョンを使用する必要があります。
• lean4lean: このカーネルバグの影響も受けていました（帰納型の処理を標準実装からのポートとして実装していたため）。

---

検証とメタプログラミングについて

lean4lean の現状

• Mario Carneiro 氏の

  lean4lean

  は、型理論の形式化とカーネルの実装証明に向けた継続的なプロジェクトです。
• 現状では一貫性の証明は帰納型をカバーしておらず、対象実装も公式カーネルと同じバグを抱えていました（同様の検証完了時に発見されるべきでした）。

メタプログラミングの制限に関する議論

• 提案の誤り: 「攻撃を防ぐためにメタプログラミングを除去・制限する」は正策ではありません。
  • エラボレータ（Elaborator）は設計上信頼できないコンポーネントです。
  • 健全性は、「信頼できないコンポーネントが悪意ある項の構築を拒否するかどうか」に依存できません。
• 攻撃の多様性:
  • 悪意のある攻撃者は、

    .olean

    ファイルを直接書き換えるか、メモリを変更することでエラボレータをバイパス可能です。
• 分離と孤立化の重要性:
  • カーネルはプロセス内で型付けされていない宣言を独自に却下する必要があります。
  • この懸念の分離こそが、証明項（proof terms）の主な利点です。

---

Lean FRO による対応策

具体的な措置

• Regression テストの実施:
  • Arthur Adjedj 氏が提起した「パラメータが一様でない場合」のテストを

    Kernel Arena

    に配置しました。
• カーネルの改良（PR #14582）:
  • カーネルがネストされた出現のパラメータが、単に再型チェックされるのではなく、実際にパラメータとして振る舞っているか確認するように変更されました。
• AI を活用したバグ発見:
  • OpenAI の Daniel Selsam 氏がサイバーセキュリティ特化の AI を導入し支援を行いました。
  • これによりカーネル内の他のプログラミングミスが複数発見され、すべて修正済みです（対応 PR: #14607, #14608, #14609, #14613, #14615, #14616）。
  • これらのバグもまた、メタプログラミングを通じてのみ到達可能です。
• 不変条件（Invariants）の強化:
  • より堅牢な不変条件を設定するための PR を提出しました（#14621, #14631, #14632）。
• nanoda のデフォルト化と更新:

  • comparator.live

    は現在、デフォルトで nanoda を実行しています。
  • Upstream 修正後でも、nanoda が毎日追跡・更新されるよう確保されています。
• コミュニティへのアプローチ:
  • 新たなバグ発見、新カーネル開発、理論・検証可能なカーネル開発に従事する専門家への支援を継続しています。

---

おわりに

この投稿のレビューおよび助言に際し、Joachim Breitner 氏とSebastian Ullrich 氏に心より感謝申し上げます。