OpenAIがミレニアム懸賞問題ナビエ・ストークス方程式にAI生成の解答を公開した。賞金100万ドル、25年以上未解決の超難問である。だが私は素直に拍手する気になれない。先行研究への便乗疑惑、Lean証明という体裁の巧妙さ、そして「AIが数学を解いた」という物語が独り歩きする危うさ。経営者はこの祝祭ムードを一度冷やして受け止めるべきだ。
何が起きたか
OpenAIは、クレイ数学研究所が設定した7つのミレニアム懸賞問題のひとつ、ナビエ・ストークス方程式に対するAI生成の解答を公開した。ナビエ・ストークスは水や空気の流れを記述する偏微分方程式で、解の存在と滑らかさの証明が25年以上未解決のまま残されてきた、数学界の最難関のひとつである。今回OpenAIが公開した証明は、Lean（リーン）という形式証明言語で書かれており、機械が論理の正しさを自動でチェックできる形式になっている。つまり「AIが書いた文章を人間が査読して真偽を判定する」というプロセスをスキップし、機械同士で検算が完結する構造だ。OpenAIはこれを「AIが人類未踏の数学的領域に足を踏み入れた象徴的一歩」として提示している。一方、現場の数学者からは「別の研究者の先行成果に依拠しており、独立した貢献としては疑問がある」との声が既に上がっている。
なぜこのニュースが重要か
このニュースの重みは、100万ドルの賞金でも、ナビエ・ストークスという看板でもない。重要なのは「Lean形式証明という機械可読な体裁を纏うことで、AIの成果に対する人間の批判プロセスを事実上バイパスできる」という前例が作られた点だ。従来、数学の証明は数年かけて査読され、他の数学者が納得して初めて認められた。ところが「Leanでチェック済み」と言われた瞬間、多くの人は「じゃあ正しいんだろう」と思考停止する。ここに罠がある。Leanが保証するのは論理の内部整合性であって、証明の新規性でも、問題設定の妥当性でも、既存研究との差分でもない。極端に言えば「他人の証明をLeanに書き写しただけ」でも機械は正しいと判定する。今回の発表がまさにその境界線を突いてきた。AI企業は今後、この「機械検証済みだから議論の余地なし」というレトリックを乱発するだろう。経営者が警戒すべきは技術そのものより、この検証構造の政治利用である。
過剰評価への反論
まず率直に言おう。今回の発表は「AIがナビエ・ストークスを解いた」わけではない。OpenAIの公開ページのタイトルも「On the Navier–Stokes Millennium Prize Problem」であって、「Solved」ではない。ミレニアム問題本体はより一般的な設定での解の存在と滑らかさを問うており、部分的・条件付きの結果は過去にも数多く存在する。今回の成果がその延長線上のどこに位置するのか、独立した数学コミュニティによる評価が固まるまで、賞金100万ドルという数字と結び付けるのは端的にミスリードだ。
さらに看過できないのが、先行研究への依拠疑惑である。数学の世界で「別の数学者の成果に基づく」と指摘されることは、貢献度が定量的に減点されることを意味する。仮にAIが既存の人間の証明の一部を再構成しただけなら、それは「AIが数学を進歩させた」ではなく「AIが数学を要約した」に過ぎない。この差は死活的だ。OpenAIがこの疑義に対して透明性のある応答を出さない限り、私はこの発表を「技術デモを装ったマーケティング」と評価する。100万ドルという数字を発表資料の近くに置くこと自体、意図的な印象操作の疑いがある。称賛より先に、まず疑うべきだ。
経営者として次に取るべき動き
第一に、社内で「AIが出した成果」を評価する際、Leanのような形式検証ツールで裏付けられているか否かを問う前に、「その成果は既存の何に依拠し、何が新規なのか」を必ず問う仕組みを整えること。機械検証は正しさの証明であって、新規性の証明ではない。
第二に、研究開発部門や専門職チームに対し、AIが提出する成果物を「先行研究トレース必須」で運用すること。AIは既存文献を巧妙に再構成することに長けており、放置すれば「AIが解いた」という誤った成功体験が組織に根付く。トレーサビリティを制度化すべきだ。
第三に、AIベンダーからの「機械検証済み」「賞金級」といったマーケティング用語を意思決定資料から排除すること。数字と権威付けの近接配置は、判断力を鈍らせる典型的手法である。導入判断は、あくまで自社ユースケースでの実測値で行う。祝祭に踊らされた企業から、静かに競争力を失っていく。