「どんな地図も、4色あれば隣り合う国同士が同じ色にならずに塗れるのか？」
この、ちょっとした疑問から始まったのが四色問題です。
一見シンプルだけど、数学史においては大論争を巻き起こしたトピックの一つ。現在では証明済みなので、『四色定理』とも呼びます。
今回は、四色問題の誕生から解決まで、そしてその後の考察までを、楽しく振り返っていきましょう！
四色問題の証明の歴史を詳しく！
四色問題の証明の歴史を、その発端から見ていきましょう。
すべてはガスリー兄弟のひらめきから始まった！
時は19世紀半ば、イギリス。
数学者フランシス・ガスリーが地図を塗っていたとき、ふとこう思ったのです。
「これって、もしかして4色あればどんな地図でも塗り分けられるんじゃ？」
実はこのアイデア、兄のフレデリック・ガスリーが先に気づき、それを弟に話したのがきっかけと言われています。
弟ガスリーは1852年にその話をド・モルガン（数学者・論理学者）に伝え、そこから学界の興味をひきつけることになりました。
このとき、地図塗り分け問題として初めて文献に登場したんです。
幻の証明、そして大混乱の時代へ
1880年、イギリスの数学者アルフレッド・ケンプが「四色問題を証明した！」と発表。
このとき、多くの数学者たちは「ついに解決か！」と喝采をあげました。
…が、9年後。
1889年にヘイウッドがケンプの証明に致命的なミスを発見。ケンプの方法で塗り分けできない反例を見つけ証明は撤回されることに。
ケンプが提唱した「ケンプ鎖」のアイデア自体は良かったのですが、それを使った証明には穴があったのです。
ただし、ケンプ鎖を応用して、「5色あれば必ず塗れる」という5色定理はこのときに証明されました。
ちょっと残念だけど、部分的な前進ですね。
新しい考え方「不可避集合」と「可約配置」
その後、四色問題をどうにかしようと多くの数学者が奮闘。
1897年にはヴェルニッケが「不可避集合」という新しいアプローチを考案。
1913年にはバーコフが「可約配置」というアイデアを研究し始めます。
この2つは後の決定的な展開につながるキーワード。
とくに、四色問題を有限個の構成パターン（地図の部分）に分解して、それぞれを検証する方法として重要でした。
ついにコンピュータの出番！
1935年ごろ、ハインリヒ・ヘーシュという数学者が「放電法」と呼ばれるアイデアを思いつきます。
この放電法、地図をパターンごとに分けて処理する技術のベースになり、いよいよコンピュータで四色問題を解く流れができてきます。
1967年、ケネス・ハーケンがヘーシュのもとで研究をスタート。
1970年には、「全部で8900種類の地図パターンを調べればよい」と示されました。これがいわゆる四色問題の有限化。
つまり、「無限にある地図の全パターンを確認しなくても、8900個を調べれば充分」ということ。
それでも、人力では無理なので…そう、ここでついにコンピュータの出番です！
そして1976年、四色問題は（やっと）証明される
1972年、ハーケンの研究に協力を申し出たのがウォルフガング・アッペル。
彼はプログラムを高速化し、コンピュータによる検証作業を進めていきます。
そして1976年、ハーケンとアッペルがついに四色問題の完全解決を発表！
すべてのパターンをコンピュータで解析し、どんな地図でも4色で塗れることが証明されたのです！
これは数学界で歴史的な出来事でした。
ただし、「人間がすべての論証を追えるわけではない」という点で、いろんな議論も巻き起こしました。
ここからは、四色問題の証明が巻き起こした波乱と、残したものを見ていきます。
コンピュータによる証明は“美しくない”…？
この証明は、世界で初めて「コンピュータがなければ証明できなかった」と言われる数学の大問題のひとつ。
でも一方で、「バグがあったらどうするの？」「証明の美しさがない」といった批判もありました。
しかし、その後に証明を独立したチームが何度も再検証したり、プログラム自体が公開されたりすることで、信頼性は高まっていきました。
いまでは「コンピュータ支援による証明」も立派な数学的手法のひとつとして認められています。
いまも続く、四色問題のロマン
実は、現在に至るまで「コンピュータを使わない、人力での四色問題の証明」は発見されていません。
不可避集合＋可約配置以外の方法で突破できるのか？
それともまったく新しいアプローチが必要なのか？
多くの数学者は「ほかの方法があるなら、すでに誰かが見つけていそうだが…」と半信半疑。
でも、新しい証明が出てきたら、それはそれで歴史に残る大発見になること間違いなし！
ケプラー予想にもつながった！
四色問題のコンピュータ証明は、その後の「ケプラー予想の解決」にも良い影響を与えました。
ケプラー予想とは、「球を一番ぎっしり詰めるにはどんな配置がベストか？」という問題。
これもまた、コンピュータでの大規模検証が必要でした。
四色問題で先に「機械による証明」が受け入れられたことで、ケプラー予想のコンピュータ証明にも理解が集まりやすくなったのです。
まとめ：四色問題の証明の歴史
振り返ってみれば、四色問題はただの「地図ぬりえ問題」ではありませんでした。
人間の論理、ひらめき、そしてコンピュータの力が交差した、壮大な数学ミステリーだったのです。
今日、私たちがあたりまえに「どの国も違う色で塗れるね〜」と見ている地図。その背後には、150年以上の探究と、数学者たちの汗と涙があったんです。
最後に要点をまとめます！
- 1852年にガスリーが四色問題を着想、ド・モルガンを通じて学会に伝わる
- 1880年にケンプが証明と発表するも、1889年に誤りが発覚
- 可約配置・不可避集合の概念が19〜20世紀初頭に登場
- 1976年、ハーケン＆アッペルがコンピュータを使って証明に成功
- 証明をめぐる議論が数学の「証明とは何か？」という問いを浮き彫りにした
- 四色問題の解決は、その後のケプラー予想など、コンピュータ数学の発展に大きく貢献
これからはうまく塗り分けられている地図をみかけたら、数学者たちの汗と涙に思いをはせてみてください！
