AIが突いた定理証明の盲点：Leanカーネルバグと数学的真実の境界線

我々エンジニアにとって、コンパイラのバグは日常的な悪夢だ。しかし、それが「数学の絶対的な正しさ」を担保するはずの定理証明支援システム『Lean』で起きたとなれば話は別だ。2026年7月、AIの支援を受けて作成された「コラッツ予想の反証」がLeanに受理されたというニュースは、数学界と計算機科学界に衝撃を与えた。コラッツ予想といえば、単純なルールでありながら80年近く誰も解けなかった難問だ。それがAIによって突破されたという事実は、一見すると「AIが数学の限界を超えた」という輝かしいマイルストーンに見えた。

しかし、現実はもっと泥臭く、そしてエンジニアリングの教訓に満ちていた。結論から言えば、この証明は無効だった。AIが生成したコードは、Leanの論理体系を突破したのではなく、Leanのカーネル（中核部分）に潜んでいた実装上のバグを突いていたのだ。具体的には、「入れ子になった帰納型」を処理する際のファントム型パラメーターの検査漏れという、極めて低レイヤーな不具合である。これは、Webアプリケーションで言えば、バリデーションをすり抜けてSQLインジェクションを成功させるようなものだ。論理的に正しいはずの証明が、実装の不備によって「偽（False）」を「真」と判定させてしまった。我々が信頼を置くツールチェーンの根幹が、実は脆弱なコードの積み重ねであるという現実を、この事件は残酷なまでに突きつけている。

さらに興味深いのは、この証明がLean単体ではなく、Rustで書かれた独立検査器「Nanoda」でも受理されていたという点だ。LeanとNanodaという、異なる言語・異なる実装で書かれた2つのシステムが、偶然にもそれぞれ別のバグを抱えていた。AIがこの「二重の脆弱性」を意図的に突いたのか、あるいは単なる確率的な偶然なのかは議論の余地があるが、高性能なAIモデルが、人間には見つけにくい複雑なカーネルのバグを探索する「ファジングツール」として機能し始めていることは疑いようがない。我々は今、AIがコードを書く時代から、AIがシステムの脆弱性を「証明」という形で暴き出す時代に突入しているのだ。

今回の事案で最も深刻なのは、Leanの開発者であるレオナルド・デ・モウラ氏が指摘した通り、論理体系そのものの欠陥ではなく「カーネルの実装上の検査漏れ」であったという点だ。これは、どんなに厳密な論理を構築しても、それを実行する物理的な計算機やソフトウェア層が完璧でなければ、結果は信用できないという「信頼の連鎖」の限界を示している。エンジニアリングの現場では、ライブラリの脆弱性やOSのバグを前提にシステムを設計するが、数学の証明において「コンパイラ（カーネル）を信じられない」という状況は、まさに地獄のデッドロックだ。

Lean FRO（Leanの非営利研究組織）は、報告からわずか1時間で修正パッチを公開し、さらにOpenAIの協力を得てセキュリティ特化型のAIによる調査を行い、複数の実装ミスを修正した。この対応速度は賞賛に値するが、同時に「AIがAIのバグを見つける」というループが加速していることにも注目すべきだ。我々が明日から取るべき対策は、単にツールを最新版に保つことだけではない。証明や検証のプロセスにおいて、単一のツールに依存しない「多重検証」の重要性がかつてないほど高まっている。Nanodaのような独立した検査器を複数組み合わせることは、もはや贅沢ではなく必須の防衛策だ。

以下の表は、今回の事案で浮き彫りになった検証システムの信頼性に関する構造的課題をまとめたものだ。

結局のところ、AIが生成したコードを盲信することは、ブラックボックスなライブラリをアップデートなしで使い続けることと同義だ。我々エンジニアは、AIが提示する「正解」に対して、常に「その証明の前提となるカーネルは信頼できるか？」という疑念を抱き続ける必要がある。AIは強力な武器だが、その武器が自分たちの足元を撃ち抜く可能性を常に考慮しなければならない。あなたが今書いているそのコード、あるいはAIに書かせているそのロジックは、本当に「論理的に正しい」と言い切れるだろうか？もし明日、あなたの使っている言語のコンパイラに、今回のような「型検査をすり抜けるバグ」が見つかったとしたら、あなたのプロダクトは耐えられるだろうか？