Navier-Stokes方程式の誰も話していない部分
The part of Navier-Stokes no one is talking about (johndcook.com)
要約
OpenAIが発表した流体力学のNavier-Stokes方程式に関する長年の疑問を解決した証明は大きな話題を呼んでいます。しかし、この記事では、OpenAIが従来の人間が読める形式の証明と同時に、Lean 4による形式証明も公開した側面に注目しています。近年、AIによって多くの数学的予想が解決されており、特にLean 4を用いた形式証明が伴っています。以前は、機械検証可能な形式証明の生成は非常に手間がかかる作業でしたが、OpenAIの証明検証には17時間しかかからず、これはコストを4桁削減する革命的な変化です。
全文翻訳
誰も話題にしていないナビエ・ストークス方程式の部分
昨日、OpenAIは流体力学におけるナビエ・ストークス方程式に関する長年の未解決問題を解決した証明を発表しました。予想通り、この発表は大きな話題を呼んでいます。しかし、OpenAIの仕事の側面で、私が誰も話していないと感じていることがあります。それは、人間が読める従来の証明と同時に、Lean 4による形式的証明も公開したことです。
最近、AIを用いて解決された数学上の予想は数多くあり、それらも特にLean 4を用いた形式的証明を伴っています。
ごく最近まで、機械検証可能な形式的証明を生成することは極めて退屈な作業でした。2005年、Henk BarendregtとFreek Wiedijkは次のように書いています。
フォーマライゼーションにどれだけの作業が必要かを示すために、学部レベルの数学の教科書の1ページをフォーマライズするには、約1週間の労働（1日8時間労働で5日）がかかると推定しています。
これが経験則でした：1ページあたり40時間。これは学部レベルの教科書の場合です。研究論文は教科書よりもはるかに密度が高いです。さらに、教科書の100ページは、おそらく1ページから99ページまでの内容に主に依存しています。研究論文の一文は、それ以前に発表されたあらゆるものを引用する可能性があります。
研究論文は、学部レベルの教科書の1ページをフォーマライズするよりも20倍の労力がかかると仮定します。すると、OpenAIの166ページの論文をフォーマライズするには、132,800人時がかかることになります。OpenAIがLeanで証明を検証するのにかかった時間は17時間でした。「革命的」という言葉を使うのをためらいますが、コストを4桁（1万倍）も削減することは革命的です。
私は、ちょっとしたブログ記事のために、自分の仕事を確認するためにAIを使って形式的証明を生成したことがあります。もし自分の仕事を確認するために誰かに1週間の給料を支払わなければならないとしたら、そんなことは夢にも思わなかったでしょう。
形式検証は数学に限定されません。例えば、一連のセキュリティポリシーが一貫しており、特定の仮定の下で目的を達成することを確認するために、形式的に検証することができます。スマートコントラクトが特定の最大負債を課していることを形式的に検証できます。ミッションクリティカルなアルゴリズムの正しさを検証できます。これらの問題は、数学研究をフォーマライズするよりも簡単であり、投資収益率（ROI）を定量化することも容易です。