Lean kernelの健全性バグ #14576 の事後分析

2026年7月25日、Ramana KumarがCollatz予想の「反証」をsory-freeな形でAI支援により公開した。しかしこれは有効な証明ではなく、Lean kernelの入れ子帰納型（nested inductive types）処理のバグを悪用したものだった。7月28日、Kiran Gopinathanがこれを小さなFalseの証明に還元し、issue #14576として報告。報告から1時間以内に修正PR #14577が公開され、Joachim Breitnerのレビューを経てマージされた。

バグの内容は、kernelが帰納型Tのネストされた出現を除去する際、パラメータDsがコンストラクタフィールドで使われないファントムパラメータの場合、生成される補助型から消えて型チェックを回避できるというもの。このバグはメタプログラミング経由でのみ到達可能で、フロントエンドは通常これを検出する。

独立チェッカーのnanoda（Rust実装）も旧バージョンでは検出できなかったが、これはnanoda自身にも別の無関係なバグが存在したためで、Jeremy Chenにより1週間前に報告・修正済みだった。lean4leanも同じkernelバグの影響を受けている。FROはKernel Arenaに回帰テストを追加し、フォローアップPR #14582でパラメータの動作検証を強化した。