AIは問題を解くのを助けるが、問題を解くこと自体が目的なのか？

AIが速く書けるのは表面的な話に過ぎない。証明が滞る本当の理由は、「問題を解くこと」がこの業界で求められている唯一のものではないからだ。

タオ氏は講演で、数学研究を行う理由を列挙しました。多すぎて1枚の図に収まりません。

同氏は、これまでこれらの目標はほぼ同じ方向を向いていたと述べた。1つで進展があれば、通常、他も連動して進む。そのため、1つか2つを他の目標の代理指標として使うことができ、多くの目標は言葉に出すまでもなく暗黙のうちに十分だった。

しかし、すべての指標を極限まで最適化しようとすると、グッドハートの法則にぶつかる。「測定基準が目標になると、それはもはや良い測定基準ではなくなる」というものだ。

ここでタオ氏は、「生成AI自体は『根拠がない』（その出力は事実に基づいておらず、発言が真実であることを保証する内在的なメカニズムもない）」とし、さらにAI企業の金銭的インセンティブが加わることで、AIツールの使用がこの法則を引き起こしやすいと指摘しました。

その結果、過度なAI最適化により、これまでほぼ一致していた目標が互いに乖離し始める。講演では、3ページにわたる図を使ってこのことを説明した。

この図は、自分が属する業界と照らし合わせて見る価値があります。どの業界でも、このような目標を列挙でき、そのうちの1つか2つを他の代理指標として使うことに慣れています。なぜなら、これまでは確かに連動して動いてきたからです。そしてAIは、そのうちの特定の1つの指標を単独で極限まで引き上げるのが最も得意です。

では、一体何を重視すべきなのでしょうか？ 次に、この講演の本題に入ります。タオ氏は聴衆の前で、目標を5回修正しました。

問題解決から教科書掲載まで、AIが加速するのは最初のステップだけ

同氏が選んだのは「問題解決」という1つの側面だ。同氏は、これはこの業界の一面に過ぎず、理論構築は同様に重要なもう一つの側面であり、別途分析が必要だと述べた。しかし、問題解決はAIの影響を最も受けやすい部分だ。

以下のパイプラインは、同氏が5回修正してできたものです。タブをクリックすると、どのように構築されていったかを見ることができます。

第1版：未解決問題をできるだけ多く解く

この目標は一見問題ないように聞こえ、ネットワークも単純です。一端は未解決問題、もう一端は解、その間をつなぐ矢印は「証明の生成」と呼ばれます。

リスクはAIが登場するずっと前から知られていました。重要な問題に対する誤った解答が大量に寄せられるということです。数論を専門とする人なら誰でも、リーマン予想を証明したと主張するメールを受け取ったことがあるでしょう。

第2版：「それらが正しいことを検証する」を追加

パイプラインに2番目のセグメントが追加されます。生成されたものはまず「未検証の解」と呼ばれ、検証されて初めて正式な解となります。

この部分では、AIは確かに役立ちます。Lean、Rocq、HOLなどの証明支援システムは、証明をコンピューターが1行ずつ検証できるコードに変換できます。AIにこの変換を行わせることを自動形式化と呼びます。

タオ氏は、生成と検証の両方の側面で、AIはすでに多くの場合に大幅な加速を実現しており、作業仮説によれば、この加速は今後も続くだろうと述べました。

そして、同氏は問いかけます。「もしAIが非常に長い証明を生成し、それを誰も（問題を与えた人を含めて）理解できない場合、どうすればよいのか？」

これは、冒頭のエルデシュ問題サイトに積まれているものと同じです。機械は検証できるかもしれませんが、「私が理解し、保証します」と名乗り出る人間は誰もいません。

第3版：「明確に伝えられ、理解される」を追加

パイプラインにさらにセグメントが追加されます。検証済みの解は「よく書かれた解」になる必要があります。この中間ステップは証明の記述と呼ばれます。

そして、このステップでのAIのパフォーマンスは最も奇妙です。

書きすぎると、読者はかえって学べない

現在のAIによる数学の記述に対するタオ氏の評価は、分裂的です。

同様の観察は他の場所でも見られます。First Proofの盲検審査員の報告書には、同じ問題が繰り返し記録されていました。AIの解答は、ルーチン的な部分を極めて詳細に扱う傾向がある一方、最も難しいステップでは言葉少なに流し、時には重要な結論を「標準的な議論により得られる」とだけ述べて理由を示さず、引用した論文に実際には存在しない結果を参照することもありました。

報告書には、さらに悪い出来事も記録されています。ある問題に対するいくつかのAI解答は、出題者自身が以前に発表した論文の表現を一行ごとに借用し、造語（T-patterns、bends）や式番号（B、T、D、H）までコピーしていたのに、論文を一度も引用していませんでした。審査員のコメントは、「これが人間による提出物なら、盗用と判断されるだろう」というものでした。

より深い層：記述も最適化されすぎる可能性がある

記述は、検証よりもはるかに曖昧な最適化目標です。作業仮説によれば、AIはいずれ記述能力を向上させるでしょう。しかし、たとえ向上したとしても、もう一つの問題があります。記述自体も過度に最適化される可能性があるということです。

証明が滑らかに書きすぎられる可能性があります。論証のルーチン的な部分と本当に難しい部分が、同じように消化しやすく提示されるのです。

人間が書いた証明では、著者が難しかったと感じた箇所に、通常、何らかの自然な摩擦が残ります。文章がぎこちなくなり、ステップが飛び、トーンが緊迫します。これらの痕跡は、読者に「ここはゆっくり読んで、もう少し注意して見てください」と注意を促します。

過度なAIによる推敲は、両方の摩擦を取り除きます。人為的なもの（著者の怠慢、不明瞭さ）と、自然なもの（ここが元々難しい）です。平準化されると、読者はスムーズに読み流してしまいますが、論証の重要なアイデアを本当に理解するようには促されません。同氏は「逆説的だが」という表現を使い、人間の記述における「欠陥」が、最終的には読者の助けになる可能性があると述べました。

この説明の後、同氏は1枚の写真を公開しました。

スライド33ページ。タオ氏はこの写真について、「1991年のBourgainの論文に、ずっと若かった私が注釈を付けたものです」とだけ説明しました。Jean Bourgain氏はベルギー出身の数学者、フィールズ賞受賞者で、調和解析の大家、2018年死去。

同じページの部分拡大（当サイトによる切り出し）。印刷された「We skip the details.」（詳細は省略する）に横線が引かれ、その下にAARGH!と書かれています。右側には3つの大きな疑問符、さらに右には「Sobolev norms!」。上の行の手書きは「I hate Jean Bourgain.」（Jean Bourgainが嫌いだ）です。

この写真は、その論点の具体的な証拠です。

Bourgain氏が「詳細は省略する」と書いた箇所で、若き日のタオ氏は行き詰まりました。彼は線を引き、疑問符を付け、「Sobolev norms!」と書いて、どの方向に考えるべきかを自分に思い出させ、最後に余白に「Jean Bourgainが嫌いだ」と書きました。

30年以上後、彼はこのページを写真に撮り、国際数学者会議のスクリーンに映しました。彼を行き詰まらせた箇所こそが、彼にゆっくりと学ばせ、その内容を本当に習得させたのです。すべてのステップが同じようにスムーズな証明は、読者にそのような場所を提供しません。

続いて同氏は、William Thurston氏が1994年に発表した「数学における証明と進歩について」からの一節を引用しました。

私たちは、定義、定理、証明の抽象的な生産ノルマを達成しているわけではありません。私たちの成功の尺度は、私たちの活動が、人々が数学をより明確に、より効果的に理解し、考えることを可能にするかどうかです。

William Thurston、「On proof and progress in mathematics」、1994

証明は増えたが、数学は速くなっていない

読者に理解できるように書くことは、まだ3番目のステップに過ぎません。

第4版：「コミュニティに消化・受容される」を追加

証明がその分野に真に貢献するには、正しくて読みやすいだけでは不十分です。他の数学者がそれを消化し、自分の研究に取り入れる必要があります。

著者ができることはあります。自分がどこで詰まったか、どうやって理解したか、なぜこの道を選んだかを説明することで、他の人がより早く理解できるようになります。しかし、現在のAIツールは自身の求解プロセスについて非常に不透明であり、特に内部動作が営業秘密である専用モデルはそうです。

一方、コミュニティによる受容は、本質的に遅く、人間的なプロセスです。優れた記述と丁寧な執筆はそれを促進できますが、結局のところ外部プロセスであり、著者と彼のAIが一方的に最適化できるものではありません。

この仕組みは現在、何に依存しているのでしょうか？ 人間の編集者と査読者による自発的なサービスです。タオ氏は次のように指摘しました。この仕事は、証明を生成することほど名声があるとは見なされないことが多いが、それは不可欠な部分であり、数学者の個人的な成果を集団的な進歩と理解に変換する方法なのです。

AIはここでフィルターとして機能できます。例えば、ジャーナルは検証が不十分または記述が不適格とマークされた原稿を自動的に差し戻すことができます。しかし、フィルターは受容そのものを代替することはできません。

第5版：「その分野の定説に組み込まれる」を追加

たとえ発表されたとしても、それが常に解の終着点であるとは限りません。重要な結果は、最終的にその分野の権威ある教科書や参考資料に組み込まれ、次世代の学生に教える標準的な説明になります。タオ氏はこのステップを正典化（canonicalization）と呼びました。

これはすべての段階の中で最も遅く、コミュニティ全体による広範な、審議を経た合意が必要であり、AIによる最適化に最も適さない部分でもあります。

しかし、同氏は、これはプロセス全体の中で最も価値のある部分だと言います。理由は2つあります。第一に、多くの応用は、基礎となる数学が完全に消化されて初めて実現可能になります。第二に、そしてより重要なのは、今日のAIツールの数学における成功は、人間の数学者が何世紀にもわたって築き上げてきた正典的な理論に決定的に依存しているということです。モデルが問題を解けるのは、先人たちがこの分野を、モデルが学習できる形に整理してきたからです。

5つのステップを経て、診断が明らかになる

もしAIがこれらの作業を実際に行うことができ、政策や文化がそれに応じて変わらなければ、このパイプラインの至る所で「インピーダンスミスマッチ」（impedance mismatch）が発生するでしょう。これは電気回路の用語で、2つのセクションのインターフェースが一致せず、エネルギーが接合部で詰まって通過できないことを指します。同氏はよりわかりやすい表現も使いました。「証明の消化不良」です。

具体的には、4つの場所で詰まりが発生します。

一言で言えば、私たちは「証明が不足する時代」から「証明が過剰になる時代」へと移行するでしょう。

これらの兆候はすでに現れ始めています。同氏は、実際には現代のAIが登場するずっと前から、圧力は蓄積していたと述べました。

同氏自身が使った、より分かりやすい例え

3ヶ月前、同氏はソーシャルメディアでこのパイプラインを料理に例えました。

同じ一連の投稿で、同氏はスライドのどの記述よりも直接的な観察結果を示しました。証明生成側の大規模な加速は、実際には数学の進歩自体の顕著な加速をもたらしていないということです。

同氏はまた、副作用にも言及しました。問題がAIによって「解決」されたが誰も理解できない場合、他の人がそれを研究し続ける意欲をそいでしまう可能性があるということです。何しろ、誰もその解を理解していないにもかかわらず、それはもう「解決済み」なのですから。

では、数学者は何をすべきか

遅い後半のステップに問題があるなら、力を注ぐ場所を変えるべきです。

同氏は出発点としてライデン宣言を推奨しました。このイニシアチブは今年6月2日に公開され、その起点は2025年9月にライデン大学で開催されたワークショップで、ケンブリッジ、コロンビア、オックスフォード、ライデン、チューリッヒ工科大学などの機関から集まった16人の数学者からなる作業部会によって起草されました。これはすでに国際数学連合の支持を得ています。つまり、今回の会議を主催したのと同じ組織です。

タオ氏は宣言から4つの項目を選び、3つのコメントを添えました。

言うまでもなく、ライデン宣言自体は、タオ氏が取り上げたこれら4つの項目よりもはるかに広範です。宣言には、戦争、大規模監視、民主主義の破壊、環境コストへのAIの使用に関する専用のセクションがあり、AI産業への公的監視の強化を求めており、政策立案者への勧告の1つは「誇大広告を信じるな」というものです。今回の講演では、その運用面の部分のみが取り上げられました。同氏が話したのは、数学コミュニティ自身がどう働くべきかということでした。

同氏自身、スライドで2回の開示を行った

最初のページの脚注には、「これらのスライドのすべてのダッシュは手動で入力されました」とあります。長いダッシュは現在、AIによる執筆のマーカーと見なされることがよくあります。

「開示の標準化」について説明したページには、脚注で「このスライドは、テキストの自動補完と図の生成にAIツールを使用しました」とあります。

どちらも本文には入れず、フッターに置かれていました。

最後に

同氏は、問題解決は一側面に過ぎないと言います。同じ分析は、教育、学生指導、採用、助成金申請、公衆への情報発信においても必要です。いくつかの分野（特に教育と訓練）では、仕事における人間の側面を強調し、AIツールの使用を厳しく制限する必要があります。他の分野では、独自の条件でこれらのツールをワークフローに組み込む方法を積極的に定義する必要があります。また、従来のものを補完する新しいワークフローと新しいインフラストラクチャも必要ですが、それは別の講演の話題です。

同氏が聴衆に残した最後の言葉は、「私たちのコミュニティは、AIの能力と私たちの目標と価値観について、オープンで誠実な議論を行うために、一堂に会する必要がある」というものでした。

本編の最後のページで、同氏はコメントを追加せず、ライデン宣言の第7条のみを掲載しました。

スライド51ページ、本編全体の最後のページです。この項目のみが表示され、テキストは添えられていません。日本語訳は以下。

同氏は講演で、数学を行う理由をいくつか挙げました。未解決問題を解くこと、理論を構築すること、知識を応用すること、コミュニティを形成すること、次世代を育成すること、永続的な美的価値を生み出すことなどです。これまで、これらの目標はほぼ同じ方向を向いていました。1つを推せば他も連動するため、1つか2つを残りの代理指標として使うことができました。

問題は、指標を極限まで最適化しようとするときに起こります。生成AIの出力は事実に基づいておらず、発言が真実であることを保証する内在的なメカニズムもありません。さらにAI企業の金銭的インセンティブが加わることで、特定の1つの指標だけを極端に引き上げ、他を置き去りにしがちです。

この対比は、自分が属する業界と照らし合わせて見る価値があります。どの業界でも、このような目標を列挙でき、そのうちの1つか2つを他の代理指標として使うことに慣れています。

同氏はその場で「未解決問題をできるだけ多く解く」という目標を5回修正しました。要件を1つ追加するたびにパイプラインが1段伸び、AIが人間に代わって実行できる部分が前に縮んでいきます。これは、この講演で最も持ち帰るべきポイントです。

タオ氏のAIによる数学記述の評価は分裂的です。綴り、文法、書式はほぼ完璧で、同氏は脚注で「完璧すぎると言ってもよい」と述べました。しかし、些細な点を長々と書き、論証で最も興味深く斬新な部分をさっと流したり隠したりし、既存文献との関係も示さないことがよくあります。First Proofの盲検審査報告書は、同じ問題を独立して記録しています。重要なステップを「標準的な議論により得られる」と一言で済ませたり、出題者自身の以前の論文の表現や造語を一行ごとに借用しながら一度も引用しなかったり。審査員のコメントは「これが人間による提出物なら、盗用と判断されるだろう」というものでした。

左側の手書きの注釈は本物です。同氏はスライドで、若い頃にBourgain氏の1991年の論文に書き込んだ写真を公開しました。印刷された「詳細は省略する」に線が引かれ、その下に「AARGH」、隣に3つの疑問符、上の行には「Jean Bourgainが嫌いだ」とあります。30年以上後、彼はこのページを写真に撮って会議のスクリーンに映しました。彼を行き詰まらせた箇所こそが、彼にゆっくりと学ばせ、その内容を本当に習得させたのです。

後半の2つのステップは最も遅いです。査読承認は人間の編集者と査読者による自発的なサービスに依存しており、この仕事は証明を生成することほど名声があるとは見なされないことが多いですが、個人の成果を集団的な進歩に変える方法です。正典化は最も遅く、コミュニティ全体の合意形成が必要で、AIによる最適化に最も適していません。しかし、最も価値があります。AIが今日問題を解けるのは、先人たちが何世紀にもわたってこの分野を、モデルが学習できる形に整理してきたからです。4つの場所で詰まりが発生します。検証待ち、記述待ち、査読の量による圧迫、そして多すぎて定説に統合できないこと。この分野は「証明の不足」から「証明の過剰」へと移行します。

数字は誰が測定したか：7/10はFirst Proof第2弾レポート（約30人の専門家による二重盲検審査）によるものです。エルデシュ問題の積み残し量とすべての見解は、タオ氏自身の講演とMastodonの投稿からのものです。なお、同氏自身は、テストされた4つのシステムのうちの1つ（UCLA Moonshot Harness）のチームメンバーであり、スライドではこの点に触れられていません。