Collatz Conjectore WAS faulse.

昨日、コラッツの記事を書いたばかりですが、今日は心臓が縮み上がるような記事が。

なんと、論理証明プログラム「Lean」が、コラッツ予想は「正しくない」と証明した、、、、のは、Leanのバグだったとか（コチラ 参照）。

最近、生成AIで数学の「難問」が次々と証明されていっています。ついにコラッツも人工知能の牙城に落ちたか、と思ったのですが、実は証明プログラムのバグだったという話。

エルディッシュじゃないですが、それほどまでにコラッツ予想は難的なわけで、証明プログラムのバグ迄見つけてしまう程。

無風凧の老後の楽しみはまだ健在！というわけです。

ところで、リーンを使って証明しいた他の難問たちは、このバグの影響はなかったのでしょうか？（人間が証明を確認しているでしょうから、間違いはないと思うのですが、、、）