ナビエストークスのミレニアム問題

OpenAIによると、流体のナビエスｔ－クス方程式に関するミレニアム問題を、Ｌｅａｎ（証明システム）と生成ＡＩで解いたそうです。（コチラ など参照）。

ミレニアム問題の中では、もっともとっつきやすい問題ではあると思っていましたが（たまたま、無風凧のなじみの領域だった）、もう生成ＡＩで解かれてしまうとは、、、虚無感を感じます。

すこし「さもしい考え」ではありますが、Ｌｅａｎの証明過程に「何らかのエラーが有ってほしい」と願う自分が居たります。

フェルマーの最終定理も、Ｌｅａｎでの証明が公開されたばかり。

勿論、Ｌｅａｎに理解させるための問題解読が大変であることは分かりますが、それでも、最終的には条件を与えてあとは計算機任せ。出てきた結果を吟味するだけ、、、、

なんとなく、数学ではなくなった、という感じで寂しさを感じるのは無風凧だけでしょうか。

追伸：今日は、菊の日＝重陽の節句。五節句の中で、無風凧が一番好きな日。なのに、上記はちょっと嫌なニュースです。わが「コラッツ問題（角谷問題）」も、生成AIの軍門に下るのでしょうか、、、、