AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明
AIの支援を受けて作られた「コラッツ予想を反証する証明」が定理証明支援システムのLeanに受理されたものの、実際にはLeanの中核部分に存在した不具合を利用していたことが分かりました。Leanの開発者であるレオナルド・デ・モウラ氏が問題の経緯を公開し、証明は数学的に成立していないと説明しています。
Postmortem for Kernel Soundness Bug #14576 - Leonardo de Moura
コラッツ予想は任意の正の整数に対し「偶数なら2で割る」「奇数なら3倍して1を足す」という操作を繰り返すと、最後には必ず1に到達するという予想です。例えば6から始めると「6→3→10→5→16→8→4→2→1」と進みます。計算ルールは簡単ですが、記事作成時点では証明も反例も見つかっていない未解決問題です。
コラッツ予想を反証するには、操作を何度繰り返しても1に到達しない正の整数が少なくとも1つ存在すると示す必要があります。2026年7月25日に、形式検証を専門とするラマナ・クマール氏が「AIの支援を受けてコラッツ予想を反証した」とするプロジェクトをGitHub上で公開しました。
GitHub - xrchz/CollatzLean: Collatz conjecture in Lean · GitHub
https://github.com/xrchz/CollatzLean
問題になったプロジェクトは具体的な整数を提示するのではなく「1に到達しない数が存在する」とLean上で証明したと主張していました。
Leanは数式や論理をプログラムとして記述し、証明に間違いがないかをコンピューターで確認するための定理証明支援システムです。利用者が記述したLeanコードは「エラボレーター」と呼ばれる処理系によってカーネルが検査できる内部表現に変換され、最後に中核の検査プログラムである「カーネル」が型の整合性を確認します。複雑な自動証明機能に不具合があっても、カーネルが不正な証明を拒否することで信頼性を保つ設計です。
今回のプロジェクトは未完成の証明を仮置きする記述「sorry」や追加の公理には依存しておらず、外見上は正式な証明に見えました。
しかし、クマール氏が反証の内容を調査していたところ、コラッツ予想とは関係なく偽を表す命題「False」をLeanに受理させられることが判明。形式検証を専門とする研究者のキラン・ゴピナタン氏が問題を小さな再現コードにまとめ、7月28日にLeanの開発チームへ報告しました。
前提なしでFalseを証明できる状態になると、論理上はどのような命題でも証明できてしまいます。つまり「コラッツ予想は誤り」という結論だけでなく「コラッツ予想は正しい」という反対の結論さえ作れるため、受理されたコードはコラッツ予想の反証にはなりません。
原因は「入れ子になった帰納型」と呼ばれる複雑なデータ構造をカーネルが処理する部分にありました。データ構造の構成要素に直接現れない「ファントム型パラメーター」が生成された補助型から抜け落ち、本来なら型が合わない引数が検査を免れる場合があったとのこと。型の合わない引数を与えると、カーネルに矛盾した証明を受理させることが可能でした。
通常のLeanコードを入力した場合はカーネルより前の処理で型の不一致が検出されます。不具合を利用するには、Leanの内部表現を組み立てるメタプログラミング機能を使い、細工した宣言をカーネルへ直接送る必要がありました。デ・モウラ氏はLeanの論理体系そのものに穴があったのではなく、カーネルの実装上の検査漏れだったと説明しています。
元のプロジェクトはLeanとは別にRustで作られた独立検査器「Nanoda」による確認も通過していました。しかし、使用されていた旧版のNanodaにも射影ノードで型名を検証しない別の不具合があり、Leanカーネルの不具合によって検査を免れた式が、旧版Nanodaの別の不具合でも受理される形に証明が組み立てられていました。LeanとNanodaという2つの実装に存在した無関係な不具合が同時に利用されたというわけです。
クマール氏は2つの不具合が同時期に利用可能だったのは偶然だと考えているものの、AIモデルが事前にNanodaの不具合報告を学習していた可能性は否定できないとしています。一方でLeanの開発に携わるヨアヒム・ブライトナー氏は、高性能なAIモデルが利用できるようになったことで複雑な不具合を発見できた可能性を挙げています。
Leanの開発チームは報告から約1時間後に修正用のプルリクエストを作成し、問題の引数が正しい型かどうかをカーネル内で確認する処理を追加しました。修正を含むLean 4.32.2は2026年7月28日に公開されています。独立検査を利用する場合は最新版のNanodaへ更新することも推奨されています。
Leanの開発を担う非営利研究組織のLean FROは再発防止用のテストを追加し、カーネル内部の前提条件をさらに厳しく検査する作業を進めています。OpenAIのダニエル・セルサム氏がセキュリティに特化したAIを使ってLean FROの調査に協力した結果、別の実装ミスも複数見つかり、記事作成時点では全て修正済みとのこと。
コラッツ予想の反証は成立しませんでしたが、AI支援で作られたコードは結果としてLeanとNanodaの不具合を明らかにしました。デ・モウラ氏は今後も新しい独立カーネルや検査器の開発を支援し、証明検査の仕組みを強化していくと述べています。
