OpenAIは2026年9月9日、Navier-Stokes方程式に関する長年の未解決問題を解決した証明を発表し、人間が読める通常の証明と同時にLean 4の形式証明を投稿しました。166ページの論文の証明について、OpenAIがLeanで検証した時間は17時間とされています。OpenAIは汎用人工知能の社会実装を掲げる企業で、GPTモデル群やコーディングエージェントのCodexを提供しています。
何が新しいか
記事の執筆者Johnは、発表の話題性の中で誰も触れていない側面として、通常の証明とLean 4形式証明が同時に公開された点を挙げています。AIによって最近解決された他の数学的予想にも形式証明が伴っており、特にLean 4が使われていると記事は説明しています。
数値で見るコスト差
Henk BarendregtとFreek Wiedijkは2005年に、学部数学教科書1ページの形式化に約1work-week(8時間労働日5日=40時間)を要するという目安を示していました。記事はこれを出発点に、研究論文は教科書より密度が高く、教科書の1ページに比べて20倍の労力がかかると仮定すると、166ページの論文の形式化は132,800人時に達すると試算しています。
| 項目 | 数値 |
|---|---|
| OpenAIの論文ページ数 | 166ページ |
| 2005年の目安(学部教科書1ページ) | 約40時間(8時間×5日) |
| 上記に基づく166ページ論文の試算 | 132,800人時 |
| OpenAIがLeanで証明を検証した時間 | 17時間 |
記事はこの差を「4桁のコスト低下」と表現しています。
数学以外への応用
記事は形式検証が数学に限らないとして、セキュリティポリシー群の整合性と、一定の仮定の下で目的を達成することの検証、スマートコントラクトが課す最大責任額の検証、ミッションクリティカルなアルゴリズムの正当性検証を挙げています。これらは数学研究の形式化より容易で、投資対効果の定量化もしやすいとしています。
この記事はHacker Newsで110ポイント・108コメントを集めています。
まだコメントはありません。