Navier-Stokes方程式の誰も話していない部分

昨日、OpenAIは流体力学におけるNavier-Stokes方程式に関する長年の疑問を解決した証明を発表しました。予想通り、この発表は大きな話題を呼んでいます。しかし、OpenAIの仕事には、誰も話していない側面があります。それは、従来の人間が読める形式の証明と同時に、Lean 4による形式証明も公開したことです。最近、AIを使用して解決された数学的予想は数多くありますが、これらもまた、特にLean 4を使用して形式証明を伴っています。 ごく最近まで、機械検証可能な形式証明を生成することは、非常に骨の折れる作業でした。2005年にHenk BarendregtとFreek Wiedijkは、形式化に必要な作業量を示すために、「学部レベルの数学の教科書1ページを形式化するには、約1週間（8時間労働の5日）かかる」と推定しました。これは経験則であり、1ページあたり40時間でした。そしてこれは学部レベルの教科書の文脈での話です。研究論文は教科書よりもはるかに密です。さらに、教科書の100ページは、おそらく1ページから99ページまでの資料に依存しています。研究論文の一文は、過去に公開されたものなら何にでも引用される可能性があります。研究論文を形式化するには、学部レベルの教科書の1ページよりも20倍の労力がかかると仮定します。そうすると、OpenAIの166ページの論文を形式化するには、132,800人時かかることになります。OpenAIがLeanで証明を検証するには17時間かかりました。 「革命的」という言葉を使うのをためらいますが、何かのコストを4桁削減することは革命的です。私は、ちょっとしたブログ記事のために、自分の仕事を確認するためにAIを使って形式証明を生成したことがあります。もし自分の仕事を確認するために誰かに1週間の給料を支払わなければならないとしたら、そんなことを夢見ることはないでしょう。形式検証は数学に限定されません。例えば、一連のセキュリティポリシーが一貫しており、特定の仮定の下で目的を達成することを確認するために、形式的に検証することができます。スマートコントラクトが特定の最大責任を課していることを形式的に検証できます。ミッションクリティカルなアルゴリズムの正しさを検証できます。これらの問題は、数学の研究を形式化するよりも簡単であり、投資収益率を定量化することも容易です。 関連記事 自動化と検証 形式手法により、隅々まで探求できる 形式手法は、労力に見合う価値があるのはいつか？ Ross 2026年9月9日 08:58 あなたが説明したセキュリティとポリシーに関する作業は、巨大で、ジューシーで、甘い領域です。GoogleとAWSは、おおよそ「形式化されたバグ発見」に関する作業を行っており（例: S3とDynamoDBのパフォーマンス検証、TPU設計）、10年以上前から行われています。TLA+が多く使われ、私が知る限り、TLA+を使うことはLEANを使うことを公園を散歩するようなものに感じさせます。それは機能し、何年もプレイされています。しかし（再びおおよそ）「敵対的なバグ発見」は、あなたが話している完全な検証ではありません。バックエンドでは、私が知る限り、形式検証ツールのすべてがSAT/SMTソルバーの何らかのバリエーションです。それが今「主流」になったのは良いことです。良い時代です。