Lean kernelの健全性バグ#14576 事後報告
मूल शीर्षक: Postmortem for Kernel Soundness Bug #14576
यह क्यों महत्वपूर्ण है
定理証明支援系Leanのkernel健全性バグは数学的形式検証の信頼性に直接影響するため、形式検証コミュニティ全体にとって重大な問題である。
2026年7月25日、Ramana KumarがAI支援によりCollatz予想の「反証」を公開。これはLean kernelのネスト帰納型処理のバグを悪用したものであり、7月28日にKiran Gopinathanがバグを特定・報告、1時間以内にLean開発チームが修正を完了した。
2026年7月25日、Ramana KumarはAI支援によって作成されたCollatz予想の「sorry-free反証」を含むリポジトリを公開した。しかしこれは有効な証明ではなく、Lean kernelのネスト帰納型処理に存在するバグを利用したものであった。
7月28日、Kiran Gopinathan がこれをFalseの小さな証明に還元し、issue #14576 として報告した。Lean開発チームは報告から1時間以内に修正(#14577)を完了し、Joachim Breitnerのレビューと改善提案を経てマージされた。新しいパッチリリースも公開済みである。
バグの内容：kernelがパラメータDsを持つ帰納型Tの下でネストされた出現を除去する際、これらのパラメータがphantom（コンストラクタフィールドで参照されない）である場合、生成される補助型から消失し、型チェックを逃れる。これにより、不正な型の引数を用いてFalseの証明をkernelに受け入れさせることが可能となる。このバグはmetaprogrammingを通じてのみ到達可能であり、フロントエンドは引数を確認して不正な項を検出する。これはLeanのメタ理論の欠陥ではなく、実装上のバグである。
独立チェッカーnanoda（RustでChris Baileyが実装）も同リポジトリを通過したが、これはnanoda自体にも別の無関係なバグが存在したためである。nanodaのバグはJeremy Chenにより報告・修正済みであったが、古いバージョンでは検出されなかった。2つの独立した実装に別々のバグが必要であったため、独立kernelによる検証の有効性は維持されているが、最新バージョンの使用が必要となる。
Mario Carneiroのlean4leanも同じkernelバグの影響を受けており、帰納型の検証はまだ完了していないため、この段階で発見されることとなった。
metaprogrammingの制限という提案に対し、開発チームはelaboratorは設計上信頼されないコンポーネントであり、健全性はそれに依存すべきでないと回答している。