数学におけるAIが提起する大きな問い

AIマガジンの特集 AIが数学をするとき、数学者であることの意味 研究者たちがモチベーション、目的、そして分野の未来を議論する ベンジャミン・スキューズ 2026年6月25日 10分読書 カリフォルニア大学ロサンゼルス校のテレンス・タオは、AIが人間と機械が複雑な問題に協力して取り組む「ビッグ・マスマティクス」の時代を到来させる可能性があると信じている。ピーター・アダムス ダークブルー1 2000年代半ば、キラーズやフランツ・フェルディナンドの音楽があらゆるパブやナイトクラブから鳴り響いていた頃、私は応用数学の博士課程で日々夜々格闘していました。私の研究は、液晶中の特殊な光波がどのように相互作用するかをシミュレートし、単純な方程式を使ってそれらの相互作用を近似し理解することに焦点を当てていました。今、自分の論文を振り返ると、液晶技術はもはや時代遅れであり、私の仕事はAIの助けがあれば数日—おそらく数時間—で完了できるだろうと想像します。しかし、エディンバラ大学で狭いオフィスを共有していた純粋数学の博士課程の学生たちの仕事については、同じことは言えません。当時、私はこれらの同僚たちに同情していました。彼らは毎日机に向かい、髪をかきむしっているように見え、何の進展もないようでした（私も苦しんでいましたが、少なくとも常に何らかの進歩はしていました）。私たちが修了し、それぞれの道に進んだとき、中にはまだ論文を一本も発表していない者もいました。 今、振り返ると、彼らがなぜ世界でほんの一握りの人しか関心を持たない抽象的な数学の問題に何年も苦労したのか、ようやく理解できました。当時私が思っていたような傲慢さではありませんでした。彼らは、一見手に負えない数学の問題を最初に解くことで、自分の優れた知性を証明しようとしていたわけではありません。それはマゾヒズムの一種でさえありませんでした（これが私の二番目の推測でした）—想像上の不十分さに対する償いとしてではありません。彼らは理解への長い道のりから喜び、満足、そして意味を見出していたことに気づきました。 Gluekit「時には、理解が非常に美しいと感じられることがある。」 —ジェレミー・アヴィガド、カーネギーメロン大学 「時には、理解が非常に美しいと感じられることがある。時にはマラソンを完走したような達成感もある」とカーネギーメロン大学の数学者ジェレミー・アヴィガドは思索します。「しかし、そのどちらでもない。複雑で難しいことについて長く深く考え、そして突然、すべてが一つにまとまる瞬間は、本当に素晴らしい感覚だ。」この感覚が、歴史を通じて数学者たちを駆り立ててきました。同様に、数学者たちがその感覚を追求する方法は、何世紀にもわたってほとんど変わっていません。彼らは、数、形、あるいは論理構造の中に、つながり、パターン、あるいは特性に気づいたり想像したりします。これから、彼らは予想—彼らの推測の未証明の記述—を書きます。彼らや他の数学者たちは、しばしば創造的な方法で論理的推論と数学のツールを使って、これらの予想を証明または反証します。最後に、さらに他の数学者たちが証明を検証します（または異議を唱えます）。 当然のことながら、このプロセスには膨大な思考時間が必要です。「私は純粋数学のキャンプに参加し、授業では難しい数学の問題に30分間座っても誰も何も言わず、みんなただ考えているだけでした」と、バーモント大学で博士号を取得しようとしている数学者でコンピューター科学者のクリスタル・モーハンは言います。「しかし、その後、私たちは協力して問題を解き明かしていきました。」 これが、数学の古くからの喜びが発揮されているところです。しかし、今日のAIシステムは、このゆっくりとした熟慮のプロセスを迂回しようと試み始めています。この傾向を論理的に考えると、AIが数学者の苦闘を完全に不要にした場合、何が起こるでしょうか？AIは人類を完全に脇に追いやる可能性さえあるのでしょうか？ 数学におけるAIの役割の増大 何十年もの間、計算は数学の進歩を加速させてきました。これは50年前、数学者たちがコンピューターを使って四色定理を証明したときに始まりました。四色定理は、隣接する領域が同じ色を共有しないように、どの地図も4色以下で着色できるかという問いです。答えはイエスであり、コンピューターはそれを、人間には現実的に検証できない1,936のケースをチェックすることによって、物議を醸しながらも証明しました。 しかし、この計算の時代を通じて、膨大な計算リソースに依存する証明においてさえ、人間の数学者の役割は中心的なままでした。人間は直感に導かれて予想を提案します。創造性と経験に導かれて、それらを証明する戦略を考案します。そして人間は、それらの証明が正しいかどうかを検証します。 今、AIは現状に挑戦しています。わずか数年で、大規模言語モデル（LLM）は、インターネットからスクレイピングされた基本的な数学を繰り返す程度の能力しか持たない「確率的なオウム」から、高度な数学的推論マシンへと進化しました。昨年の夏、Google DeepMindとOpenAIのシステムは、国際数学オリンピックで金メダルの地位を獲得し、世界で最も数学的に才能のある高校生と同等のレベルに達しました。この毎年恒例のコンテストでは、出場者は数学の様々な分野からの悪名高いほど難しい6つの問題を解かなければなりません。 今年初め、Google DeepMindの実験的AIシステムAletheiaは、自律的に博士号レベルの研究成果を発表可能にするという、さらに重要なマイルストーンを達成しました。この研究自体は数学的には難解で、算術幾何学における構造定数の計算ですが、その重要性は、未解決の数学的問題に取り組む際に示した複雑な推論にあります。さらに最近では、OpenAIの新しい汎用AIシステムが組合せ幾何学の重要な予想を反証しました。この結果は、もし人間が著者であったならば主要な数学雑誌に掲載されるに値するものであり、トップの数学者たちはこの偉業を数学におけるAIのマイルストーンとして称賛し、独立した独創的で洗練された思考を示したと評価しました。 もう一つの変化は、LLMと、10年以上前から存在する「証明アシスタント」として知られる数学ツールを組み合わせることから生まれました。Isabelle、Lean、Rocqなどのこれらのシステムは、数学的証明を段階的にチェックし、その論理的な正確性を検証する特殊なプログラミング言語です。従来、数学者は自分の定理や証明をこの機械可読形式に手作業で翻訳する必要があり、これは形式化と呼ばれる骨の折れるプロセスでした。現在、LLMはこのボトルネックを取り除き始め、非公式な証明を証明アシスタントが検証できる形式コードに自動的に翻訳しています。 人間の証明から形式的な証明へ 素数が無限に存在するというユークリッドの有名な証明は、証明アシスタントであるLeanで形式化されると、非常に異なるものに見えます。人間の数学者は日常的に手順を省略し、共有された理解に頼ります。形式化はすべての仮定と推論を明示的にし、コンピューターが証明を検証できるようにします。 人間の証明 すべての自然数nに対して、n以上の素数pが存在することを示したい。n! + 1の最小の素因数をpとする。これは明らかに素数である。pがn以上であることを示すために、矛盾を仮定して、そうではないと仮定する。するとpは明らかにn!を割り切るので、(n! + 1) - n! = 1も割り切る。しかしこれは不可能である。pは素数であり、1には素因数がない。したがって、pはn以上である。 Leanによる証明 ```lean /- Euclid’s theorem on the **infinitude of primes**. Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/ theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p := let p := minFac (n ! + 1) have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _ have pp : Prime p := minFac_prime f1 have np : n ≤ p := le_of_not_ge fun h => have h1 : p ∣ n ! := dvd_factorial (minFac_pos _) h have h2 : p ∣ 1 := (Nat.dvd_add_iff_right h1).2 (minFac_dvd _) pp.not_dvd_one h2 ⟨p, np, pp⟩ ``` ❶ 定義は明示的でなければならない。この証明は、pをn! + 1の最小の素因数として正式に定義してから、その量を使用できる。 ❷ 形式的な証明は、以前の形式的な証明に基づいて構築される。ここでLeanは、pが素数であることを示す以前に検証された定理を呼び出している。 ❸ 隠れた論理ステップが明示的になる。人間の数学者は、そのように書くことができる。