数学のその後

私の研究や解説論文の最新情報、未解決問題の議論、その他の数学関連トピック。 ホーム 経歴に関するアドバイス 執筆について 書籍 Mastodon+アプレット フィードを購読する 数学のその後 2026年9月12日 ゲストブログ、math.GM、意見 | タグ: Eamon Duede, 哲学, Silvia De Toffoli | 投稿者: Terence Tao [これはSilvia De ToffoliとEamon Duedeによるゲスト投稿です。このブログ記事は当初、異なるファイル形式で書かれ、AIを使用して変換されました。— T。] Silvia De Toffoli (Pavia高等研究学校) Eamon Duede (プリンストン大学およびパデュー大学) 2026年9月8日、OpenAIは、7つのミレニアム懸賞問題の一つであるナビエ・ストークス方程式の存在と滑らかさの問題に対するAI生成による解を生成したと発表しました。この発表は、功績の配分と、その結果に対する人間と機械のそれぞれの貢献に関する議論を引き起こしました。さらに、この発表は、人間の知的能力を例証すると考えられていた領域における、以前のAIの征服との比較を激化させました。 最近の声明で、ナビエ・ストークス問題の経緯に関わった数学者の一人であるTristan Buckmasterは、「これはディープ・ブルー対カスパロフの瞬間だ」と述べました。数学における実存的な問いが自然に続きます。AIが数学の最先端の問いに答えられるようになった今、多くの人がチェスや囲碁について言ったように、この学問分野は「解かれつつある」のでしょうか？チェスや囲碁のプレイヤーのように、数学者もただ「プレイし続ける」べきで、その実践を再編成すべきなのでしょうか？ 「プレイし続ける」という応答には、何か正しいところがあります。哲学者C. Thi Nguyen (2019) が主張しているように、ゲームをプレイする目的は、その目標（勝利）によってすべてが尽くされるわけではありません。本当のポイントは結果だけでなく、プロセスです。これは、チェスよりも、例えばパーティーゲームであるツイスターの方がより明確かもしれません。ツイスターをプレイする目的は、確かに勝利ではありません。しかし、同様のことが、チェスや囲碁のような深い知的ゲームにも当てはまります。例えば、囲碁をうまくプレイすることは、敗北の中での達成感となり得ます。しかし、数学の実践という文脈では、これは不必要な後退のように感じられます。代わりに、私たちはより力強い一歩を踏み出すことができます。つまり、後退を必要不可欠に見せるゲームとして数学を特徴づけることを拒否することです。したがって、問題は、AIが最も難しい問いに答えられるようになった後の数学に何が続くのか、ということだけではありません。それはまた、そもそも私たちが数学を行う際に、何を目指しているのか、ということです。 AIが数学を「解いた」という物語は、魅力的でもっともらしく、しかし両方とも間違っている2つの仮定に基づいています。1つ目は、AIが本当に数学の問題を解いたという仮定、2つ目は、数学は問題解決のみに関するものであるという仮定です。 最初の仮定は間違っています。なぜなら、数学の問題を真に解決するには、単に答え（たとえ形式的に認証されたものであっても）を提供するだけでは不十分だからです。欠けているのは、人間の数学者が理解し、数学の目標を進歩させるために使用できる、理解可能な証明です。そして、以下で論じるように、たとえAIがまさにそれを提供したとしても、物語は終わりません。なぜなら、2番目の仮定が間違っているからです。数学は明らかに、問題解決よりもはるかに広範な事業です。数学者は、新しい概念や理論を開発し、新しい問いを立てて答えること、異なる領域を統一すること、学術コミュニティを教育し維持すること、そしてその美しさと深さによって評価される仕事を生み出すことに努めます。したがって、私たちはAIが数学で人間に打ち勝ったという物語を拒否し（そして拒否すべきです）、数学が本当に何であるか、そして私たちがそれをどうありたいのかについて真剣に考え始めることができます。 すべての答えが解決策ではない OpenAIは、ナビエ・ストークス方程式が特異点を発生させうるかという問いに対する答えを生成しました。答えは「はい」でした。ダグラス・アダムスの『銀河ヒッチハイク・ガイド』では、ディープ・ソートは「生命、宇宙、そして万物についての究極の疑問」に対する答えを生成しました。その答えは「42」でした。どちらも、私たちが本当に望んでいたものではありません。 もちろん、OpenAIは「はい」以上のものを提供しました。ディープ・ソートは数値を提示しただけでしたが、OpenAIは多くの人が証明と呼ぶことをいとわない2つの成果物を生成しました。1つ目は、妥当性を認証するLeanの形式化です。これには、対応する非形式的な証明を含む原稿が伴っていました。では、なぜこれがまだ不満足なのでしょうか？その理由は、証明そのものの根本的な概念に関係しています。 実際、証明には2つの概念があります。論理的な概念と理解可能な概念です。現代論理学は、証明を演繹的な妥当性の観点から特徴づけており、証明は、数学的な議論の理解を必要としない機械的な手順によってチェックできます。Leanの形式化はこれらの基準を正確に満たしており、ナビエ・ストークス問題の結果のLean形式化は、したがって、本質的で重要な貢献です。論理的な証明の要求を満たすことによって、それは確実性を確保します。 しかし、数学者は証明に別のものを求めています。彼らは理解を求めています (Thurston 1994)。彼らは、命題が真である理由を知りたいのです。この種の知識は、彼らが把握し、他の専門家と共有し、既存の知識と結びつけ、さらなる進歩に利用できる数学的なアイデアを扱います。これが理解可能な証明の概念です。現時点では、OpenAIの結果が、理解可能な証明の概念から期待される価値を数学界に提供したかどうかは明らかではありません。 真の証明は、論理的かつ理解可能な証明の両方です。歴史的に、この2つの概念は一致する傾向がありました。なぜなら、数学者は、定理を真にしている共有可能な主要なアイデアを最初に把握することなしには、非常に複雑な論理的な証明を生成できなかったからです。論理的な証明の概念は、主に理解可能な証明の正確性を検証するために使用されていました (Burgess and De Toffoli 2022)。しかし、AIによって、これらの2つの概念は劇的に乖離する可能性があります。私たちは、理解可能な証明から切り離された形式的な証明を持つことになるかもしれません。 これは形式証明への批判ではありません。逆の問題は少なくとも同様に深刻です。理解可能な数学的な議論は、結果が実際に真であることを確立することに失敗しながら、壮大なアイデアを伝えることができます。JaffeとQuinn (1993) は、Hakenの3多様体に対するThurstonの幾何化定理を例として有名に使用しました。不十分に完全な証明を伴う主要な洞察は、「インスピレーションというよりは障害」となる可能性があります。そして、HalesのFlyspeck形式化プロジェクトの動機の一つは、ケプラー予想のために提示された理解可能（しかしチェックが難しい）証明が、実際に真の証明であったことを検証することでした (Hales et al. 2009)。したがって、論理的または理解可能な概念のいずれかを満たさないことは、真の証明が進歩への道を開くところに障害を作り出します。 真の数学的解決策には、論理的な正確さと理解可能性の両方が必要です。これは、7つのミレニアム懸賞問題の場合に特に明らかです。それらは、数学者が単に7つの答えを求めていたからではなく、有用な解決策を求めていたから選ばれたのではありません。Clay Mathematics Institute自身が、ナビエ・ストークス問題の場合に証明がなぜ重要なのかを説明しています。「証明は確実性だけでなく、理解も提供するからです。」 OpenAIが私たちに提供したのは答えです。しかし、彼らが有用な解決策を提供したかどうかは明らかではありません。おそらく、彼らがそうしたことが判明するかもしれませんが、現時点では、状況は明確ではありません。真の解決策は、結果を信じるための十分な根拠を提供すると同時に、結果が数学者によって理解され実践される数学の一部となることを可能にする、理解可能な数学的議論を提供します。 それにもかかわらず、OpenAIが提供したものが単なる答えにすぎないことが判明した場合でも、数学が直面している実存的な脅威を払拭するには十分ではありません。将来のAIシステムは、形式的に認証され、数学者にとって完全に理解可能な、真の証明を生成する可能性が高いです。したがって、数学がAIによって「解かれつつある」という現在の懸念は、単に真の解決策を主張するだけでは完全に払拭されるわけではありません。