局所的厳密性は、全体の確定を意味するのか（ナビエ・ストークス方程式）

「証明」という言葉は、なにを意味するのか

OpenAIが、ナビエ・ストークス方程式に関するミレニアム懸賞問題を
「解決した」と主張した。

証明論文がある。
形式化された証明もある。
Leanによる検証経路も公開されている。

少なくとも、AIがそれらしい答えを一つ出して終わった話ではない。
かなり重い根拠が置かれている。

それでも、私は一つの言葉が気になった。

「解決した」という言葉だ。

構造を見つけることと、証明すること

数学を少し覗いてみると、「証明した」という言葉は簡単には使えなくなる。

「こういう構造が見える」
「この条件ではこうなる」
「この根拠から、こういう可能性を提案できる」

ここにはまだ開いた領域がある。

観測位置が変われば別の構造が見えるかもしれない。
条件を広げれば成立しないかもしれない。
論証の途中に見落としがあるかもしれない。

ところが、「証明した」と言った瞬間、言葉の性質が変わる。

自分にはこう見えた、ではない。

ある前提と定義のもとで、

この命題は成立する。そこまでを引き受ける言葉になる。

局所的厳密性

今回のOpenAIの発表には、非常に強いものがある。

解析的な証明がある。
形式化された証明がある。
proof checkerによる検査経路もある。

これらは軽視できない。

むしろ、かなり真面目に数学的な厳密性を取りにいっているように見える。

しかし、ここで一度分けてみたい。

ある論理体系の内部で厳密に検証されたこと

と、

その体系へ入れた定義が、元の数学的問題を正確に表現していること
は、同じなのだろうか。

さらに、その形式化が正しいこと
ナビエ・ストークス問題そのものが解決されたことも、
本当に同じなのだろうか。

局所的な厳密性を積み重ねれば、全体の確定になる。

そう考えたくなる。

しかし、その接続部分にもまた、検証すべき境界が存在する。

厳密性の外側

仮にLeanが一つの証明を完全に検証したとする。

それは非常に強い事実だ。

だが、その瞬間に世界中の数学者が「ナビエ・ストークス問題は解決した」と認識しなければならないわけではない。

定式化は正しいのか。

前提は元の問題と一致しているのか。

既存数学との接続に問題はないのか。

形式化されていない境界は残っていないのか。

そして、その証明は数学者によって理解され、独立に検証できるのか。

一つの厳密性の外側には、別の厳密性がある。

だから、局所的厳密性 ≠ 全体的確定なのかもしれない。

「解決した」という言葉

これはOpenAIが間違っている、という話ではない。

現時点で私には、その証明が正しいとも間違っているとも判断できない。

だから、そこは確定しない。

問題は別のところにある。

OpenAIは、証明論文を公開した。
形式化した。
Leanによる検証経路も公開した。

そのうえで、

“This resolves the Navier–Stokes Millennium Prize problem.”
「これはナビエ・ストークス・ミレニアム懸賞問題を解決するものです」

と結論を置いた。ここに、私は一つの矛盾を見る。

OpenAIは内部では、非常に厳密な検証を積み重ねている。

それなのに外部への言葉では、その厳密さを支えてきた数学共同体による検証が終わるより先に、「解決した」という全体を確定する言葉を置いている。

今回の問題は、証明の根拠が弱いことではない。

むしろ逆だ。

これだけ厳密性を重ねた企業が、なぜ最後の「解決した」という言葉だけは、数学が長く守ってきた確認の過程より先に置いたのか。

そこが一番気になる。

構造を発見した。
証明候補を作った。
形式化した。
形式検証した。
専門家が検証した。
数学共同体に定着した。

これらは似ているようで、同じではない。

それぞれの間には境界がある。

そして数学は、その境界を簡単に飛び越えないことで厳密性を作ってきたのではないだろうか。

証明は、誰のものなのか

さらにもう一つ、問いが残る。

証明の正しさを最終的に数学共同体の検証へ開くのであれば、
問われるのは論理的な正しさだけなのだろうか。

数学では、証明は単に結論を保証する装置ではない。

なぜ成立するのか。

どの構造が本質なのか。

既存の数学とどう接続するのか。

そこから何が新しく見えるのか。

そうした「理解」もまた、証明を読むことで共有されてきた。

では、巨大なAI探索によって生成され、形式化され、機械によって検証された証明が現れたとき、

論理的に正しいことと、数学として理解されたことは同じなのだろうか。

そして、その理解がまだ数学共同体に共有されていない段階で、

誰が「解決した」と言えるのだろう。

局所的には、極めて厳密なのかもしれない。

しかし、局所的厳密性と、全体的確定は同じではない。

「証明」という言葉は、数学界では決して軽いものではない。

だからこそ今回問われているのは、AIに証明ができるかどうかだけではない。

AIによって証明が作られる時代に、私たちは何をもって数学の問題が「解決した」とするのか。

OpenAIが置いた「解決した」という一言は、証明そのものと同じくらい、その問いを数学界に投げ込んでいるように見える。

数式上の解決と、現象の解明

ナビエ・ストークス方程式には、もう一つ独特の事情がある。

これは純粋に数式だけのために作られた対象ではない。

水や空気のような流体が、どのように動くのか。

その物理現象を記述するための方程式である。

だから、ここではさらに二つの「解決」を分けて考える必要がある。

数式上の解決と、物理現象の解明だ。

ある定式化について数学的な証明が成立したとしても、それだけで現実の流体現象そのものが解明されたとは限らない。

証明されるのは、あくまで定義された数学的対象についての命題である。

一方、現実の流体には、モデル化の前提、近似、境界条件、観測可能性、物質固有の性質などが存在する。

つまり、方程式の中で何が成立するか

と、現実世界で何が起きているかの間にも、もう一つ境界がある。

ここでもまた、

局所的厳密性 ≠ 現象全体の解明という構造が現れる。

もし「ナビエ・ストークス問題を解決した」という言葉が、数学的定式化に対する解決だけを意味するのであれば、それはその範囲で読むべきだ。

しかし社会に出た瞬間、その言葉はしばしば、

人類が流体の謎を解いたという意味にまで膨らんで受け取られる。

数学的証明の確定と、物理的実態の理解。

この二つを同じ「解決」という言葉で閉じてしまってよいのか。

ここにもまた、言葉の重さがある。