コンピュータが解いた：機械が解決を助けた有名な数学の問題（1976〜2026年）

1976年、イリノイの2人の数学者が、どんな地図も4色あれば塗り分けられることを証明したと発表しました。しかも証明の一部は、コンピュータにしか確かめられないものでした。多くの数学者は強い違和感を覚えました。人間が全部を読めないものを、本当に証明と呼べるのか？それから50年、問いは逆転しました。2026年には、専門家が何十年も見つけられなかった成果の鍵となるアイデアを、AIシステムが見つけたのです。この記事ではその歴史を順に追い、有名な問題ごとに機械が何をしたのかを正確に示します。「コンピュータが解いた」という言葉は、まったく違う意味になりうるからです。

1976年：4色と、誰にも読めない証明

GCSE基礎

問題は小学生にもわかるほど単純です。隣り合う国が同じ色にならないように地図を塗り分けるとき、何色あれば足りるか？フランシス・ガスリーは1852年、4色だと予想しました。4色が必要になる場合があることはすぐわかります（下の図を見てください）。しかし、ありうるすべての地図で4色が「いつでも」足りると証明することは、124年間も数学者を拒み続けました。

ケネス・アッペルとヴォルフガング・ハーケンは、5色が必要な地図があるとすれば、2,000近い特別な配置のどれかを必ず含むこと、そしてそれぞれの配置は「取り除ける」ことを示す方法を見つけました。すべてを手で確かめるのは不可能だったので、コンピュータが1,000時間以上かけて確かめました。定理は証明されましたが、それは「証明」の実際の意味を変えるやり方でした。

疑いはどう晴らされたか： 1996年にはより短いコンピュータ証明が続き、2005年にはジョルジュ・ゴンティエとバンジャマン・ヴェルネが証明支援系Coqの中で論証全体を検証しました。今では数学で最も徹底的に検証された定理の1つです。

1996年：コンピュータが自力で見つけた最初の証明

学部発展

ロビンス予想は、3つの短い規則が、あらゆるコンピュータチップの中にある真偽の論理、つまりブール代数とまったく同じ代数を表すかどうかを問うものでした。アルフレト・タルスキをはじめとする一流の論理学者たちが、60年かけても決着をつけられませんでした。1996年、ウィリアム・マッキューンの自動定理証明器EQPは、ありうる推論の連鎖を約8日間探索し、証明を見つけました。これは1976年とは質の違う出来事でした。論証がどうあるべきかを、誰もコンピュータに教えていなかったのです。

1998〜2014年：ケプラーのオレンジ

1611年、ヨハネス・ケプラーは、八百屋がオレンジを積むやり方（各段を下の段のくぼみに載せる）こそが、同じ大きさの球の最も密な詰め方だと主張しました。この詰め方は空間の約74%（正確にはπ/√18）を埋めます。

トマス・ヘイルズはサミュエル・ファーガソンとともに、問いを何千もの最適化問題に変えてコンピュータで解き、1998年に証明を発表しました。論文誌の査読者は「99%確信している」としながらも、すべての計算は確かめられないと述べました。ヘイルズはこれに応え、証明支援系ですべてを検証し直すFlyspeckプロジェクトを率い、2014年に完了させました。

2016年：200テラバイトの証明

GCSE基礎

自分で試せるパズルがあります。すべての整数を赤か青に塗ります。ピタゴラス数（3、4、5のように a² + b² = c² となる3つの数）が1色だけにならないように塗れるでしょうか？

ロナルド・グラハムは答えに100ドルの賞金を出していました。2016年、マレイン・ヒューレ、オリバー・クルマン、ヴィクター・マレクは、「SATソルバー」（真偽の巨大な論理パズルを解くソフトウェア）をスーパーコンピュータStampedeで約2日間走らせました。答えは、1から7,824まではどの数も問題なく塗れるが、1から7,825では塗れない、というものでした。7,825個の数のどの塗り方もうまくいかないことの証明は200テラバイトに達し、当時『Nature』は史上最大の数学の証明と報じました。同じ手法は2019年、7次元の空間を立方体で敷き詰めるケラー予想にも決着をつけました。

2025〜2026年：AIがアイデアを見つけ始める

大学院発展

ここまでの例はすべて、コンピュータを確認のために、あるいは人間が設計した枠組みの中での探索のために使っていました。2025年からは、大規模言語モデルを土台にしたシステムが数学的なアイデアそのものを提案し始め、それを証明支援系Leanと組み合わせることで、結果をただ信じるのではなく機械で検証できるようにしました。

単位距離予想（2026年5月）。 1946年、ポール・エルデシュは問いました。平面上にn個の点を置くとき、距離がちょうど1になる点の組はいくつありうるか？彼は、その数はnよりほんの少し速く増えるだけだと考えていました。OpenAIの社内モデルは、代数的整数論の深い道具を使って、それをnの本当のべき乗分だけ上回る点の集合の無限の族を見つけました。フィールズ賞受賞者のティモシー・ガワーズとジェイコブ・ツィメルマンを含む一流の数学者9人がこれを確かめて補足の論文を書き、ウィル・ソーウィンがその差を具体的な形で示しました。ギル・カライは、その重要性を1976年の四色定理の証明になぞらえています。

AlphaProof Nexus（2026年5月）。 Google DeepMindは、GeminiモデルとLeanを組み合わせた自社のエージェントに、エルデシュ問題データベースの353個の未解決問題を解かせました。9問を解決し、そのうち2問は56年間未解決でした。さらにオンライン整数列大辞典（OEIS）の予想44個を証明しました。どの証明もLeanでコンパイルされます。ただし成功率には注意が必要で、約2.5%です。

Astra（2026年8月）。 OpenAIは、未公開の次世代モデルによる10の成果を発表しました。その中には、ミハイル・グロモフが1999年に提起した問いに答える「非ソフィック群」の初めての構成、エルデシュ問題3問、そして1978年以来初めてとなる球の詰め込みの一般的な上界の改良が含まれます。どの成果にもLeanの証明書が付いていました。独立した人間による監査では主要な成果に確認された重大な誤りは見つかりませんでしたが、1つの成果には専門家から大幅な修正の要請があり、執筆時点では論文誌の査読は完了していませんでした。

50年を1つの年表で

数学を学んでいる人にとっての意味

この記事のどの成果も、やはり人間に頼っていました。誰かが問題を正確に述べ、どの方法を試す価値があるかを判断し、コンピュータが証明した定理が本当に大事なものかを確かめ、それがなぜ正しいのかを説明しなければなりませんでした。それこそ、学校の数学が「途中の考え方を書きなさい」と求めるときに育てている力であり、私たちの記事AIは本当に数学ができるのか？のテーマでもあります。まだ未解決の問題と、ここで紹介した解決済みの問題のカード一覧は、私たちの未解決の数学ミステリー・ハブにあります。