テクノロジーメディアのGigazineは昨日（8月3日）、AIを利用して完成させ、コラッツ予想を反証したと主張していたLeanの形式化証明が無効であると報じました。
注：コラッツ予想（別名、偶奇正規化予想／3n+1予想）は、ドイツの数学者ロタール・コラッツ（Lothar Collatz）が1937年に提唱したもので、表現は非常に単純ですが、現在も未解決の数学上の難問です。任意の正の整数に特定の規則で反復計算を行うと、最終的には必ず1に戻ると主張しています。
計算規則は、任意の正の整数nについて次のとおりです：
nが偶数の場合、2で割ります（n ÷ 2）。
nが奇数の場合、3倍して1を加えます（3n + 1）。
新しい数が得られたら、結果が1になるまで上記の手順を繰り返します。
数字6を例にすると：
6は偶数なので、2で割ると3になります
3は奇数なので、3倍して1を加えると10になります
10は偶数なので、2で割ると5になります
5は奇数なので、3倍して1を加えると16になります
16を順に2で割ると、8、4、2、1になります
最終的な経路は、6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1です。
形式化検証の専門家であるRamana Kumar氏は7月25日、GitHubでプロジェクトを公開し、当初はAIを利用してコラッツ予想を反証したと主張しました。このプロジェクトは具体的な反例となる整数を示さず、Lean（定理証明支援システム）上で「1に到達しない数が存在する」ことを証明しただけでした。
Leanは、ユーザーが数学的な公式や論理をプログラムとして記述し、コンピューターによって証明の正確性を検証できる定理証明支援システムです。ユーザーが記述したLeanコードは、数学的命題と証明を検査可能なプログラムとして表現し、カーネルが型と論理の整合性を検証します。
しかし、その後に反証内容を調査したところ、関連する手法によってLeanが「False」（偽の命題を表す）を無条件に受け入れてしまうことさえ判明しました。そのため、現時点では関連コードはコラッツ予想を反証できません。
形式化検証の研究者であるKiran Gopinathan氏は問題を小規模な再現コードに縮小し、2026年7月28日にLean開発チームへ報告しました。
脆弱性は「ネストした帰納型」の処理をカーネルが行う部分にあり、場合によって「幽霊型パラメーター」（データ構造の構成要素に直接現れないパラメーター）を無視していたため、本来なら誤りと判定されるはずのパラメーターが検証をすり抜けていました。Lean開発者のLeonardo de Moura氏は、問題はカーネルの実装で必要な検査が完了していなかったことにあると説明しました。
Leanチームは報告を受けて約1時間後に修正プルリクエストを作成し、7月28日にLean 4.32.2をリリースして、この問題を修正しました。