AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明

AI支援で作成されたコラッツ予想の反証証明が、定理証明支援システムLeanのバグを突いていたことが判明しました。証明は数学的に成立していません。

• AI支援で作られたコラッツ予想の反証が、Leanのカーネルバグを突いていたために無効とされた。
• 発見された反証は、数学的な証明ではなく、ソフトウェアの欠陥を利用したものであった。
• AIによる数学的発見の検証プロセスにおける課題が浮き彫りになった。