- エルデシュ問題 #728が最近、AIツールによってほぼ自律的に解決され、数学研究の自動化における新たなマイルストーンとなった
- この問題はもともと Erdős, Graham, Ruzsa, Strauss が1975年に提起した 二項係数の素因数分解に関する問い で、曖昧な条件のため長らく明確に扱われてこなかった
- ChatGPT が調整された制約条件の下で証明を生成し、Aristotle がそれを Lean 形式証明 として定式化しつつ誤りを自動修正した
- その後、複数の参加者が ChatGPTを使って自然言語で書き直し、文献との接続や叙述構成を強化した版を反復的に改善した
- Terence Tao はこの過程について、AIの迅速な証明作成・修正能力 が研究論文の書き方そのものを変える可能性を示していると評価した
AIが解いたエルデシュ問題 #728
- 最近、AIツールの活用がエルデシュ問題の解決に新たな進展をもたらし、問題 #728 が ほぼ自律的にAIによって解決 された
- 初期の試行後、フィードバックを反映して修正した版で成功した
- 結果は既存文献で同一の形では再現されておらず、類似手法による近い結果だけが存在していた
- この事例は、ここ数か月で AIの数学的問題解決能力が実際に向上 していることを示している
- 過去にもAIがエルデシュ問題を解いた例はあったが、その多くは後に文献中に既に存在する解だと判明した
- 今回の問題は、もともとのエルデシュの記述が 誤った形で提示されており、最近になってようやく意図された形に再構成された
- そのため、既存文献に関連研究が少なかったことの説明にもなっている
問題の歴史と初期アプローチ
- 1975年に Erdős, Graham, Ruzsa, Strauss は 二項係数
(2n choose n) の素因数分解を研究し、複数の関連問題を提示した
- そのうちの一つが、a!b! | n!(a+b−n)! の条件と a+b > n + C log n を満たす無限個の a, b, n が存在するかを問う問題だった
- ただし Cの大きさ（小さいか大きいか） など、複数の点で記述が不明確だった
- 数か月前、AlphaProof チーム がこの問題の単純な解を見つけたが、これは意図された問題の趣旨に合わなかったため、a,b ≤ (1−ε)n という制約を追加した
- その後のAI支援による文献検索でも、関連研究はほとんど見つからなかった
ChatGPTとAristotleの協働
- 1月4日、ChatGPT が調整された制約条件の下で 小さい C の場合に対する証明を生成した
- この証明は Aristotle によって Lean 形式証明 として定式化された
- その後、原論文を再検討した結果、元の論文がすでに小さい C の場合を扱っていたことが確認された
- 別の参加者が Lean 証明をChatGPTで自然言語に変換 し、追加の対話を通じて 改善版 を作成した
- この版は一部の証明の空白を埋めたものの、依然として AI特有のぎこちない文体 や 文献引用の不足 が残っていた
- それでも 核心的なアイデアを理解できる程度には読める水準 に達していた
大規模な書き直しと改善された成果物
- 追加のプロンプトにより、ChatGPT が 大きい C の場合まで拡張した証明を生成した
- 一部に誤りはあったが、Aristotle が自動修正し、Lean で検証済みの証明 を完成させた
- 3人目の参加者が Lean 証明を圧縮 した後、別の参加者が ChatGPTと長時間対話 しながら
- 文献との接続や叙述構成を強化した完成度の高い論文形式 に書き直した
- その成果物は AI生成物らしさが薄れた、研究論文に近い品質 と評価された
- Tao はこのテキストをエルデシュ問題フォーラムで検討したと述べている
AIが変える研究論文の書き方
- Tao は、最終的な論文でもなお 核心部分は人間が書く必要がある と見ているが、
- AIとLeanの組み合わせ が 証明の作成と修正の速度 を飛躍的に高めたと評価している
- これまでは、論文一本を読みやすく仕上げるのに多くの時間がかかり、
- 査読者フィードバックに基づく修正も 局所的な変更 にとどまることが多かった
- しかし今では、AIのテキスト生成・修正能力 と 形式証明ツールの検証機能 が結びつくことで、
- さまざまな精度や叙述レベルで新しい版の論文を素早く生成 できるようになっている
- 一つの「正式な論文」だけでなく、AIが生成した多数の補助版 が存在しうることで、
- 多様な観点や追加的な価値 を提供できる可能性も示されている
コミュニティの反応
- 一部のユーザーは、AIが生成した文書の追加的な価値 を「別の角度から見られる能力」だと説明した
- 別の数学者たちは、AIの成果の独創性測定 や 既存文献との類似性評価 の必要性を提起した
- 例えば、Lean 形式証明の長さ比較 による定量的な類似性測定の提案があった
- また別のコメントでは、AIはコードのリファクタリングのように論文を大域的に書き直せる ため、
- 研究者は より高いレベルで文書構造を設計すること に集中すべきだという意見も示された
- 一部では、AIが数学者の役割を代替する可能性 に懐疑的な反応も見られたが、
- 他方ではこれを 協働と発想拡張の新しい機会 と評価する声もあった
1件のコメント
Hacker Newsの意見
私はHarmonicで働いており、私たちが作った Aristotle についていくつか誤解を正したい
Aristotleは最新の AI手法 を積極的に活用しており、言語モデリングも含んでいる
英語の非形式的な証明を入力すると、その証明が正しければLeanへ翻訳される確率が高い。つまり、英語の証明が堅牢であることの強いシグナルになる
ひとたびLeanで形式化されれば、その証明が正しいことに疑いの余地はない。これが私たちの中核的なアプローチだ — AIベースの探索で答えを見つければ、その複雑さに関係なく結果の正確性を保証できる
Rustはメモリ安全性を保証するために固定されたルール集合を使っているが、このルールは単純で制限的だ。もしAristotleのようなシステムがコンパイラに統合され、コードの 正確性の証明 が可能なら自動的に通せるようになれば本当にすごいと思う
Harmonicが人間の書いた数学の大半を形式化できるようになるまで、どれくらいかかるのか気になる。競合のChristian Szegedyは今年中に可能だと言っていたが
Terence Taoの説明を見ると、人間が2つのAIツールの間で結果をやり取りし、AIが人間の見つけた 隙間を埋める役割 を果たしたように見える
完全な自律的解決というよりは、人間とAIの 協業 に近い。つまり、専門家が主導しAIが補助する形だ
既存の証明を再構成したり新しいやり方で組み合わせたりする作業は、人間にとっては 退屈または複雑な過程 だが、AIはそれを超人的な速度でこなせる
このアプローチはAGI以前の段階でも非常に大きな可能性を開くはずだ。数学者がAIを道具として使い、ミレニアム懸賞問題 のような難問に取り組む時代が来ると思う
LLMの本当の価値は、言語で表現できるテーマに対して 新しい視点 を示すことにある
実際に問題を解いた人が書いた説明文を見ると、巨大なパイプラインなしに、わずか数個のプロンプトだけで 結果を得たという点が印象的だ
最近のモデルははるかに多くの計算資源を使うが、これはむしろ 下限レベルの成果 に見える
Terence Taoが「AI contributions to Erdős problems」というwikiページを作った
GitHubページとMathstodon投稿を見ると、今回の結果（問題728）はそのページ最初の 『緑色の項目』 、つまりAIが実際に解いた最初の事例だ
物理学や数学のような複雑な分野の専門家たちも、AIと対話しながら助けを得ているのか気になる
分野別に見ると、有用性はプログラミング > 応用ML > 統計/応用数学 > 純粋数学の順で下がる
今すぐAristotleを直接使える — https://aristotle.harmonic.fun/
また、Stanfordの個人ページへのリンクが間違っている（wwwを外す必要がある）
今回の結果は整数に関する定理で、Mathlibインフラ がよく支援している領域だ
使われた定義も複雑ではなく、この種の証明は成功確率が高い。それでも本当に驚くべき成果だ
LLMを超えた 特化型AIアプローチ の可能性を示す事例だ
Aristotleの論文は arXiv:2510.01346 にある
Transformerアーキテクチャを使ったからといって、すべてがLLMというわけではない — 言語データで学習していなければ LLMとは呼べない
つまり、全段階がLLMベースだ
2026年にはAIが数学の 未解決問題 をますます多く扱うようになる気がする
今回の事例も完全自律ではないが、人間のフィードバック後はAIがほぼ自力で解いた水準だ
もう「LLMは単なる確率的オウム」という議論は終わったと思う。これからは どう実用化するか が本当の議論の中心になるはずだ