AIがコラッツ予想を「証明」、実際はLean 4のバグを利用

先日、数学とコンピュータサイエンスのコミュニティで、AIがコラッツ予想（3n+1問題）を「証明」したというニュースが話題になりました。あるユーザーが大規模言語モデル（LLM）を使って、Lean定理証明器による形式証明を生成し、コラッツ予想を解決したと主張しました。しかし、調査の結果、この証明は正しい数学的推論に基づくものではなく、Lean 4カーネルの深刻なバグを悪用したもので、任意の命題（真偽を問わず）を証明できることが判明しました。

この出来事は、TwitterユーザーGro-Tsenによって最初に共有され、彼はこの「証明」が単にLeanカーネルのバグを利用したものであると指摘しました。Gro-Tsenはその後のツイートで、投稿者がこのバグを認識しており、コラッツ問題の真の解決としてではなく、意図的に問題を示すために使用したことを明らかにしました。Jason Ruteなどの他のユーザーもこれを確認し、定理証明コミュニティでは既知のバグを使って問題をデモする前例があると述べています。

それにもかかわらず、この事件は広範な懸念を引き起こしました。ユーザーAntoine Ducrosは、このようなバグが存在するならば、以前にLeanで検証された他の証明にも気づかれない類似の問題があるのではないかと疑問を呈しました。これは形式検証システムの信頼性と信頼の基盤に直接挑戦するものです。Gro-Tsenはまた、形式証明が非形式的な理解と一致しない可能性や、証明自体が人間にとって読めず実用的価値を失うといった他の一般的な問題も指摘しました。

今回の出来事は、形式証明ツールが数学的検証において大きな可能性を秘めている一方で、完璧ではないことを改めて思い起こさせます。AIが生成した証明は特に注意深く扱う必要があり、システムの根底にある欠陥を隠す可能性があります。数学界とコンピュータサイエンス界はこれらのツールを改善し続け、結果に対する批判的な検討を維持する必要があります。

この事件はさらに、AI支援による数学証明が普及するにつれて、形式の正確性とシステムの安全性をどのように確保するかという重要な問題を提起しています。コミュニティは定理証明器の監査を強化し、バグの透明な報告を奨励することで、同様の誤解を招く出来事を防ぐことを求めています。