T1#research#ethics#labor

エルデシュ問題が AI で解かれ始める ──「数学の死」論争まで

1985年、アデレード大学でソファに座り資料を見せる Paul Erdős と、その横で考え込む10歳の Terence Tao
出典Billy or Grace Tao (Wikimedia Commons) · CC BY-SA 2.0 · Commons で見る ↗

メタデータ

日付
年代
2020s
Tier
T1
出典数
14
関連項目
05
Tags
#research#ethics#labor

2026年1月、ハンガリーの数学者 Paul Erdős が残した未解決問題の一つ、エルデシュ問題第728問が、OpenAI の GPT-5.2 Pro と、Harmonic 社の Lean 証明系 Aristotle を使って解かれた。1月6日に形式証明が完成し、翌7日、UCLA の Terence Tao は、エルデシュ問題が問題の趣旨に沿って AI によってほぼ自律的に解かれ、その結果は知る限り既存の文献にない、と書いた。ここから、AI がエルデシュ問題を次々に解く波が始まり、年の後半には「AI は数学を終わらせるのか」という論争にまで広がった。

エルデシュ問題と erdosproblems.com

Erdős は生涯に膨大な問題を論文や手紙で出し、しばしば自腹の懸賞金を付けた。Quanta Magazine によれば、1996年に彼が亡くなった後も、アイオワの財団が懸賞金を引き継ぐと約束している。

これらを一か所に集めたのが、マンチェスター大学の Thomas Bloom である。2023年初め、自分用に問題を整理しようとサイト erdosproblems.com を立ち上げ、そのコードは ChatGPT に書かせた。2025年8月にコメント機能を加えると、職業数学者でない愛好家も含む共同体が育った。2026年8月時点で、サイトには解決済み565問、未解決652問が載る。問題の難しさも重要性もまちまちで、一つのサイトにまとまっていたことが、AI の能力を測る格好の目安になった。

前史 ── 解いたという主張の誤り

最初の騒ぎは失敗だった。2025年10月、OpenAI の幹部 Kevin Weil が、GPT-5 が未解決のエルデシュ問題10問の解を見つけたと X に投稿した。The Decoder によれば、Bloom は、サイトの「未解決」は自分が解を知らないという意味にすぎないと説明し、実際には GPT-5 は既存の論文を見つけただけだった。投稿は削除され、Google DeepMind の Demis Hassabis はこの件を「embarrassing(恥ずかしい)」と評した。

12月には、学生の Kevin Barreto らが AI で解いたと発表した第333問の答えが、1977年の Erdős 自身の論文にあったことが判明した。Tao はこうした例を受けて、AI は最も低い枝に実った果実、つまり標準的な手法で短く解ける問題を摘み取れるようになったが、そうした問題こそ目立たない文献ですでに解かれている可能性が高い、という見立てを示した。

第728問 ── 何が新しかったか

日付出来事
2025年10月GPT-5 が10問を解いたとする投稿が誤りと判明
2025年12月25日第333問の AI 解答、既存文献にあると判明
2026年1月4日Barreto が GPT-5.2 Pro と Aristotle による証明を発表(当初の解釈で)
2026年1月6日趣旨に沿った版の形式証明が完成
2026年1月10〜11日第729問・第401問も AI で解決
2026年2月11日Tao、2か月で50問近くが解決済みになったと報告
2026年5月第1196問の論文、DeepMind の AlphaProof Nexus、OpenAI の 単位距離予想の反証

第728問は、Erdős らが1975年に二項係数の素因数分解を研究した際に出した、階乗の割り切れ方に関する問いである。Tao によれば問題文はあいまいで、AlphaProof のチームが自明な解があると指摘した後、サイトの参加者が趣旨に沿う形に条件を補っていた。Nat Sothanaphan が arXiv にまとめた経緯によると、Barreto は1月4日に GPT-5.2 Pro の論証を Aristotle で形式化した証明を発表し、5日に補った条件版への拡張を GPT-5.2 Pro に求め、6日に Aristotle が Lean の形式証明を出した。Tao はこの件で、解法そのものより、AI が解説文を素早く書き直す能力のほうが興味深いとも書いている。

ただし留保もついた。Tao は3月に投稿を追記し、この AI の手法は Carl Pomerance の2014年の論文にとても近く、Pomerance 自身がその方法で第728問が解けることを示す短い覚え書きを出したと記した。それでも、この問題を明示的に扱ったのは AI の解が最初だった、という。

波の大きさ ── 成功率は1〜2%

その後、第729問(1月10日)と第401問(1月11日)も AI で解かれ、のちにどちらも第728問の論法を改造すれば解けることが分かった。Tao は2月11日、人間・AI・その混成による解決が押し寄せ、2か月ほどで50問近くが新たに解決済みになったと書いている。一方で、AI ツールの真の成功率は1〜2ポイント程度にすぎないとも推計した。成功例ばかりが SNS で拡散し、失敗は報告されないからである。解決は、難易度の低い端に大きく偏っていた。

5月には、Tao、Jared Duker Lichtman、Barreto、Liam Price らが、愛好家の AI 実験から始まった第1196問の解決を論文にした。Quanta は、Bloom が驚いたこととして、新しい結果の多くが大企業の研究所ではなく、公開の LLM を使う愛好家や学部生から来ていた点を挙げている。この構図は、5月に DeepMind と OpenAI が相次いで大きな成果を出したことで変わった。

「数学の死」をめぐる論争

成果が増えるほど、数学の営みそのものへの問いが強まった。

懸念する側。Princeton 大学の Noga Alon は Quanta に対し、AI が解き始めてからはもう意味がないと語り、エルデシュ問題に取り組むのをやめた。Bloom は、数学の素養がない人が AI に証明を書かせ、AI に検査させた、誰も読まない100〜200ページの論文が増えていることを大きな課題だと述べた。Tao は4月、数学は「証明の欠乏」から「証明の過剰」の時代に移りつつあり、人が検証も消化もしていない AI の証明は、問題を「解決済み」にすることで、かえって人の関心を失わせうると書いた。7月には、Lean で形式証明はあるが人間が消化していない問題を「open (Lean)」と分類し始めている。

6月2日には、16人の研究者がまとめた ライデン宣言が公表され、国際数学連合(IMU)が支持した。Leiden 大学によれば、宣言は AI の禁止を求めるものではなく、AI 使用の開示や、AI を著者ではなく道具として扱うことなどの規範を求めている。IMU 副会長の Ulrike Tillmann は「Mathematics is, and should always remain, a profoundly human endeavour.」(数学はこれまでも、そしてこれからも深く人間的な営みであるべきだ)と書いた。9月11日には、Tao を含むフィールズ賞受賞者らが声明「A Severe Misalignment of AI in Mathematics」を出し、AI 企業の目標と数学界の目標は深刻にずれていると訴えた。

楽観する側・中間の立場。Tao と Tanya Klowden は3月の論文で、AI を、考えを生み、整理し、広めるために人類が作ってきた道具の自然な進化とみなし、開発と利用は人間中心であるべきだと論じた。AI は人の成果を点検する役には比較的安全に使えるが、検証の及ばない構想を任せるのは危険だ、という使い分けも示している。愛好家の Wouter van Doorn は、AI のほうが自分より数学ができると認めつつ、ピアノが好きなら演奏機械を雇わずに自分で弾くのと同じで、自分は数学を楽しみ続けると語った。Alon も、優れた数学者の多くはいずれ AI を使うだろうと見ている。

誰にとって何が変わったか

得をしたのは、まず大学の外の愛好家だった。Quanta は、Bloom のサイトが肩書きを問わない共同研究の場になったと描いている。一方で、熟練の研究者には、長年の問題が魅力を失うという喪失が生まれた。人材の移動も起きた。Quanta によれば、2026年7月、フィールズ賞を受けた当日に Jacob Tsimerman が学界を離れ OpenAI に移ると発表している。

AI 企業の側も対応を迫られた。OpenAI は10月、新たな数学の成果を公開するにあたり、高等研究所(IAS)の独立した諮問グループと公開の作法を協議したと説明し、AI の成果を数学者が検討・理解するための Simons 財団の新事業に500万ドルを拠出すると発表した。計算機と証明の関係をめぐる問いは、四色定理(1976年)から半世紀を経て、規模を変えて戻ってきた。流れは AI と数学の年表、社会との関わりは AI と社会の年表 にまとめている。

よくある質問

エルデシュ問題とは何ですか。
ハンガリーの数学者 Paul Erdős(1996年没)が論文や手紙で出した数多くの問題で、しばしば懸賞金が付けられていました。英国の数学者 Thomas Bloom が2023年から erdosproblems.com に集めて整理し、2026年8月時点で解決済み565問、未解決652問が載っています。
AI が解いた最初のエルデシュ問題はどれですか。
Terence Tao は2026年1月、第728問を、問題の趣旨に沿って AI がほぼ自律的に解き、既存の文献にも見当たらない例だと評しました。GPT-5.2 Pro の論証を Harmonic 社の Aristotle が Lean で形式証明にしたものです。それ以前の AI の解答の多くは、後から文献に答えが見つかっていました。
AI は数学を終わらせるのですか。
見方は割れています。Noga Alon は AI が解き始めてからエルデシュ問題に取り組む意味がなくなったと語り、フィールズ賞受賞者らの声明は AI 企業と数学界の目標が深刻にずれていると警告しました。一方、Tao と Klowden は AI を人類の道具の自然な進化とみなし、人間中心で使うべきだと論じ、AI の助けで数学を楽しむ愛好家もいます。

出典

  1. 一次資料Terence Tao on Mathstodon: Erdős problem #728 solved more or less autonomously by AI — January 7, 2026

    問題の趣旨に沿った AI によるほぼ自律的な解決、既存文献に見当たらない、問題が不正確に定式化されていた

    取得日: 2026-10-17

  2. 一次資料Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof — Nat Sothanaphan, arXiv:2601.07421

    1月4日の Barreto の発表、1月6日の Aristotle による形式証明、#729(1月10日)と #401(1月11日)

    取得日: 2026-10-17

  3. 一次資料Erdős Problem #728 — erdosproblems.com

    取得日: 2026-10-17

  4. 一次資料Terence Tao on Mathstodon: true success rate of AI tools on Erdős problems — January 17, 2026

    Erdős 問題での AI の実際の成功率は1〜2ポイント程度

    取得日: 2026-10-17

  5. 二次資料Why the Legendary Erdős Problems Are Falling to AI — Konstantin Kakaes, Quanta Magazine, August 3, 2026

    Bloom のサイトの成り立ち、#333 の失敗と #728、Alon・van Doorn・Bloom の言葉、解決済み565問・未解決652問

    取得日: 2026-10-17

  6. 一次資料Sharing AI progress in mathematics — OpenAI, October 6, 2026 (updated October 15, 2026)

    高等研究所(IAS)の諮問グループと結果公開の作法を協議、Simons 財団の新事業に500万ドル

    取得日: 2026-10-17

最終更新:

共有