May 21, 2026

数学という人類最後の砦が突破された——でもコンピュータ証明は別に今に始まった話じゃない

OpenAIの汎用推論モデルが代数整数論でErdősの80年の予想を覆した。人類の知の最後の砦が突破された。でもコンピュータ証明は1976年からある。今回は違うのは、機械が人間の代わりに計算したのではなく、道を探索したことだ。

数学は人類の知の最後の砦だった。チェスは1997年、絵画は2022年、コードは昨年陥落した。だが数学——洞察が必要で、美しさが必要で、誰も思いつかなかった繋がりを見つけ出すあの数学——だけは、まだ人間だけの領域だった。

もう違う。OpenAIの汎用推論モデルが、1946年から未解決だったErdősの単位距離予想を覆した¹。フィールズ賞受賞者のTim Gowersは「Annals of Mathematicsに躊躇なく推薦する」と述べた²。今回は本物だ——昨年11月、Kevin Weilが「GPT-5が10の未解決Erdős問題を解いた」と吹いたのは既存論文の再発見だったことが判明し、Erdős Problemsサイトを管理するThomas Bloomは「劇的な誤報」と呼んだ³。今回はBloom自身が付随論文の共著者だ²。

だが話は「また一つAIが領域を征服した」だけじゃない。コンピュータ証明は別に新しい話じゃないから。

コンピュータ証明は1976年からある

1976年、AppelとHakenがコンピュータで四色定理を証明した——どの地図も4色で隣接区域を区別できる⁴。数学界は揺れた。証明には千以上の場合のコンピュータ列挙が必要で、人間が一行一行確認するのは不可能だった。

多くの人が居心地が悪かった。「本物の証明じゃない」と言う人もいた。読めないから。機械は人間が指示したことをやっただけで、数学的洞察はないと言う人もいた。

その通りだった。だが四色定理は今でも「純粋に手で」証明されていない。50年経って、数学界はコンピュータが証明道具になりうることを受け入れた。Coq、Lean、Isabelle——証明支援系は数学のワークフローに組み込まれている⁵。2026年1月以降、AIは15のErdős問題を「未解から解決済」に移した⁶。

だから問題は「機械は証明できるか」じゃなかった。半世紀前からできていた。

問題は：機械はあなたの代わりに計算しているのか、それともあなたの代わりに考えているのか？

今回どう違うか

Erdősの単位距離問題はシンプルだ。平面上にn個の点を置くとき、距離がちょうど1の組は最大いくつできるか？¹

誰もが答えはだいたい線形だと思っていた。正方格子が2n組を出す。Erdős自身の構成はもう少し良くて——n^(1+C/log log n)——でも線形よりほんの少しだけ速い¹。最良の上界O(n^(4/3))は1984年のSpencer、Szemerédi、Trotterに由来する⁷。42年動かなかった。

Erdősはu(n) ≤ n^(1+o(1))と予想した⁴。誰もがそう信じていた。

表1：80年、動かず ¹⁷

年	結果	誰
1946	最良の下界：n^(1+C/log log n)	Erdős本人
1984	最良の上界：O(n^(4/3))	Spencer, Szemerédi, Trotter
2026	覆された：u(n) ≥ n^(1+δ)、δ=0.014	OpenAIモデル + Will Sawin改良

モデルはどうやったか？反例を探索した。

当たり前に聞こえるが、この問題に取り組んだ全員がどうしていたか考えてみてほしい——彼らは予想が正しいことを証明しようとしていた。モデルの思考の連鎖は、計算量の大部分を反例の構成に費やしていた²。モデルは「みんなが正しいと思っている」に縛られなかった。社会的合意を知らなかったから、人間が集団的に排除した方向を試した。

Gowersが気づいた：「思考の大部分が反例の構成を試みており、証明を試みていない。これはモデルが、ある種の直感と、コミュニティがロングショットと見なすアプローチを試みる意欲を持っていることを示している。」²

これが「vibe数学」だ——LLMとの対話で定理を反復的に開発する⁵。命題を与えて証明が出てくる、という話じゃない。試して、確認して、直して、また試す。道が見つかるまで。

代数整数論が裏口から入ってきた

誰も予期しなかった部分がここだ。

モデルは組合せ幾何に留まらなかった。一見全く関係なさそうな分野——代数整数論——に飛んだ。ErdősのGaussian整数（a + bi）をもっと複雑な代数体で置き換え、無限類体塔やGolod-Shafarevich理論を使った¹²。

代数整数論の中では基本道具だ。だがユークリッド平面上の点の問題に適用するなど、誰も思いつかなかった。

表2：人間とAIは違う扉を見ていた ¹²

	人間	AI
どこを探索したか	組合せ幾何	代数整数論
使った道具	組合せ的議論	類体塔、Golod-Shafarevich
戦略	予想を証明する	反例を構成する
結果	証明できなかった	n^(1+0.014)

プリンストンのWill Sawinがδ = 0.014に特定した²。小さく見える。だが「線形より少し速い」じゃない——「固定された多項式の優位性」だ。漸近分析では、これは本質的な違いだ。

Alonは遠慮しなかった：「AIがここでやったのは、優秀な人間の研究者が何人も試みて失敗したことだ。」²

Bloomはもっと遠くまで書いた：「AIは何世紀にもわたって築いた数学の大聖堂をより完全に探索するのに役立っている。他にどんな目に見えない驚異が控えているのか？」¹

だがGowersは冷たい水を注いだ——正直に。

証明されたんじゃない、覆されたんだ

GowersはこれをGuthとKatzが2005年にErdősの距離問題を証明した時と比較した。あの証明は多項式区分法という真に新しい道具を導入し、全体の方向を切り開いて、その後いくつもの問題を解決した。

今回の構成はそれをしていない。数論から引っ張ってきた架け橋であって、新しい幾何理論ではない。「強力な新しい幾何学的道具も、予期されていなかった構造的結果も導入していない」²。

Gowersの判断：反例は検索で見つかる可能性がある。証明には本当の理論構築が必要だ。「今見ているのはAIが人間の数学者を追い越すということではなく、特定の問題スタイルで明らかな優位性があるということかもしれない——百科的な知識があり、時間管理を気にせず、成立しそうにない命題を真剣に試す余裕がある。」²

要約：AIは検索が得意。構築はまだ。

これはコンピュータ証明の歴史と軌を一にする。1976年の四色定理も検索だった——千以上の構形を列挙した。ただ今回は、検索の対象が構形の数じゃなかった。数学の分野だった。

Leanで検証されていない

注目すべき詳細：証明は形式的に検証されていない。LeanもCoqもない。9人のトップ数学者が読んで確認した²。

四色定理は最終的にCoqで形式化された（2005年、Georges Gonthier）。多くのAI生成Erdős解もLeanで検証されている⁵。だが今回の証明は自然言語で、人間が一語一語確認した。

これは「コンピュータ証明」か？どこに線を引くかによる。「機械の出力を人間が確認した」なら、四色定理は1976年にコンピュータ証明だった。「機械が形式体系の中で命題からQEDまで全リンクを独力で完了した」なら、今回はまだ該当しない。

だが今回の証明は四色定理がしなかったことをした：人間が見つけられなかった道を見つけ出した。 四色定理：人間が戦略を考え、機械が実行した。今回は：機械が自分で代数整数論への扉を見つけた。

参考文献

まとめ

数学は機械がまだ手をつけていなかった人類最後の硬い骨だった。それが突破された。だが振り返れば——1976年の四色定理がコンピュータ証明だった。CoqもLeanも研究に組み込まれている。コンピュータ証明は新しい話じゃない。AIがErdős問題を解くのも今日始まったことじゃない。

違うのは：前はコンピュータがあなたの代わりに計算していた。今回は機械が道を探索した——そして代数整数論から離散幾何への、人間が見逃した道を見つけ出した。難しすぎたからじゃない。「みんなが証明できるはずだと信じていた」からだ。

だがGowersは正直に言った：反例は検索で見つかる。本当の理論構築は検索じゃ見つからない。機械が見つけたのは反例であって、新しい理論ではない。

今後数カ月で、代数整数論者が離散幾何の他の未解決問題に目を向けるだろう²。その扉の向こうにさらなる反例がいれば——まあ、AIはより速い検索エンジンってことだ。GuthとKatzが見つけたような新しい理論がいれば——その時こそ本当に違う話になる。

OpenAI公式ブログ — An OpenAI model has disproved a central conjecture in discrete geometry https://openai.com/index/model-disproves-discrete-geometry-conjecture/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷
Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood — 付随論文 — 人間可読版証明と専門家解説 https://arxiv.org/abs/2605.20695 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹²
TechCrunch —「今回は本物」— 以前の誤った主張の背景 https://techcrunch.com/2026/05/20/openai-claims-it-solved-an-80-year-old-math-problem-for-real-this-time/ ↩
Gil Kalai —「Erdősの単位距離問題が覆された！」— 1976年の四色定理との比較 https://gilkalai.wordpress.com/2026/05/21/amazing-erdos-unit-distance-problem-was-disproved-it-was-achieved-by-ai/ ↩ ↩²
arXiv 2602.18918 —「vibe-proving」：LLMとの反復対話で定理を開発 https://arxiv.org/abs/2602.18918 ↩ ↩² ↩³
CryptoBriefing — 2026年1月以降15のErdős問題が解決、うち11がAI https://cryptobriefing.com/openai-ai-solves-erdos-math-conjecture/ ↩
Spencer, Szemerédi, Trotter (1984) — 上界O(n^(4/3))、42年不変付随論文で引用 ↩ ↩²