AI支援でつくられた「コラッツ予想の反証」は無効。定理証明支援システム「Lean」のバグを突いていたことが判明

コラッツ予想
任意の正の整数に対し「偶数なら2で割る」「奇数なら3倍して1を足す」という操作を繰り返すと、最後には必ず1に到達するという予想
例　6　「6→3→10→5→16→8→4→2→1」

AIの支援を受けて作られた「コラッツ予想を反証する証明」が定理証明支援システムのLeanに受理されたものの、実際にはLeanの中核部分に存在した不具合を利用していたことが分かりました。Leanの開発者であるレオナルド・デ・モウラ氏が問題の経緯を公開し、証明は数学的に成立していないと説明しています。
コラッツ予想は任意の正の整数に対し「偶数なら2で割る」「奇数なら3倍して1を足す」という操作を繰り返すと、最後には必ず1に到達するという予想です。例えば6から始めると「6→3→10→5→16→8→4→2→1」と進みます。計算ルールは簡単ですが、記事作成時点では証明も反例も見つかっていない未解決問題です。

コラッツ予想を反証するには、操作を何度繰り返しても1に到達しない正の整数が少なくとも1つ存在すると示す必要があります。2026年7月25日に、形式検証を専門とするラマナ・クマール氏が「AIの支援を受けてコラッツ予想を反証した」とするプロジェクトをGitHub上で公開しました。

問題になったプロジェクトは具体的な整数を提示するのではなく「1に到達しない数が存在する」とLean上で証明したと主張していました。

Leanは数式や論理をプログラムとして記述し、証明に間違いがないかをコンピューターで確認するための定理証明支援システムです。利用者が記述したLeanコードは「エラボレーター」と呼ばれる処理系によってカーネルが検査できる内部表現に変換され、最後に中核の検査プログラムである「カーネル」が型の整合性を確認します。複雑な自動証明機能に不具合があっても、カーネルが不正な証明を拒否することで信頼性を保つ設計です。

今回のプロジェクトは未完成の証明を仮置きする記述「sorry」や追加の公理には依存しておらず、外見上は正式な証明に見えました。

しかし、クマール氏が反証の内容を調査していたところ、コラッツ予想とは関係なく偽を表す命題「False」をLeanに受理させられることが判明。形式検証を専門とする研究者のキラン・ゴピナタン氏が問題を小さな再現コードにまとめ、7月28日にLeanの開発チームへ報告しました。
前提なしでFalseを証明できる状態になると、論理上はどのような命題でも証明できてしまいます。つまり「コラッツ予想は誤り」という結論だけでなく「コラッツ予想は正しい」という反対の結論さえ作れるため、受理されたコードはコラッツ予想の反証にはなりません。

原因は「入れ子になった帰納型」と呼ばれる複雑なデータ構造をカーネルが処理する部分にありました。データ構造の構成要素に直接現れない「ファントム型パラメーター」が生成された補助型から抜け落ち、本来なら型が合わない引数が検査を免れる場合があったとのこと。型の合わない引数を与えると、カーネルに矛盾した証明を受理させることが可能でした。

通常のLeanコードを入力した場合はカーネルより前の処理で型の不一致が検出されます。不具合を利用するには、Leanの内部表現を組み立てるメタプログラミング機能を使い、細工した宣言をカーネルへ直接送る必要がありました。デ・モウラ氏はLeanの論理体系そのものに穴があったのではなく、カーネルの実装上の検査漏れだったと説明しています。

元のプロジェクトはLeanとは別にRustで作られた独立検査器「Nanoda」による確認も通過していました。しかし、使用されていた旧版のNanodaにも射影ノードで型名を検証しない別の不具合があり、Leanカーネルの不具合によって検査を免れた式が、旧版Nanodaの別の不具合でも受理される形に証明が組み立てられていました。LeanとNanodaという2つの実装に存在した無関係な不具合が同時に利用されたというわけです。

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/