Four color theorem 四色定理
4色定理は「世界で初めて、コンピュータを本質的に使用して解決された未解決の重要問題」とされています。それ以前にも「コンピュータを使って計算する」ことはありましたが、4色定理が他と決定的に違ったのは、「コンピュータによる検証がなければ、証明自体が成立しなかった（人間には不可能だった）」という点です。
1. 4色定理以前のコンピュータの役割
1976年以前、数学におけるコンピュータはあくまで「補助道具（電卓の延長）」でした。
- 素数探索: 巨大な素数（メルセンヌ素数など）を見つけるために計算機が使われていましたが、これは「発見」であり、理論的な「証明」とはみなされませんでした。
- 数値計算: 物理学や工学のシミュレーションには使われていましたが、数学の厳密な論理構築においては脇役でした。
2. 4色定理が「初」と言われる理由
4色定理の証明において、アペルとハーケンは以下のことを行いました。
- 有限個への絞り込み: 人間の手で「この1,482個のパターンさえ調べれば、理論上すべての地図を網羅できる」ことを論理的に示しました。
- 全件調査の丸投げ: しかし、その1,482個が本当にすべて4色で塗れるかを確認するのは、人間の寿命では足りないほど膨大な作業でした。そこでコンピュータに「論理の最終的な穴埋め」を任せたのです。
このように、「証明の核心部分をコンピュータが担った」例は、それ以前には存在しませんでした。
3. 「証明」という概念の変容
4色定理の登場によって、数学界には「コンピュータ証明（Computer-aided proof）」という新しいカテゴリーが誕生しました。
その後、4色定理の影響を受けて以下のような重要なコンピュータ証明が続きました。
- ケプラー予想 (1998年): 「球体を最も効率よく積み上げる方法は、八百屋さんのオレンジの積み方である」という、300年以上未解決だった問題の証明。
- エドワーズ・ロビンスの予想: 組み合わせ論の問題。
4. 4色定理より「前」にあった例外的な動き
あえて「以前」のものを探すと、証明そのものではありませんが、1950年代から「自動定理証明（Automated Theorem Proving）」の基礎研究は始まっていました。
- Logic Theorist (1956年): ラッセルとホワイトヘッドの『数学原理』にある定理をいくつかコンピュータに解かせる試みがありましたが、これは既に「人間が解いたことがある問題」の再現に過ぎませんでした。
四色問題（四色定理 Four color theorem）は、シンプルな問いから始まり、解決まで100年以上を要した数学史上最も有名な難問の一つです。
1. 提唱（1852年）：フランシス・ガスリー
この問題は、ロンドン大学の学生だったフランシス・ガスリー（Francis Guthrie）が、イギリスの地図を塗り分けているときに気づいた素朴な疑問から始まりました。
- 提唱者: フランシス・ガスリー
- 広めた人物: 彼の弟フレデリックが、師事していた数学者オーガスタス・ド・モルガンにこの疑問を伝え、そこから数学界に知れ渡ることになりました。
当時の問い（予想）: 「平面上のいかなる地図も、隣接する国が同じ色にならないように塗り分けるには、4色あれば十分か？」
2. 混迷の時代（19世紀後半〜20世紀前半）
解決されるまでの間、二つの「証明された！」という大ニュースが流れましたが、後にどちらも誤りであることが判明しました。
- 1879年: アルフレッド・ケンプが証明を発表。11年間正しいと信じられましたが、1890年に誤りが指摘されました。
- 1880年: ピーター・テイトが別の証明を発表しましたが、こちらも1891年に誤りが見つかりました。
しかし、彼らが考案した手法（ケンプの鎖など）は、最終的な証明の重要な土台となりました。
3. 証明（1976年）：アペルとハーケン
ついに120年以上の時を経て、イリノイ大学の二人の数学者によって決着がつけられました。
- 証明者: ケネス・アペル (Kenneth Appel) と ヴォルフガング・ハーケン (Wolfgang Haken)
- 手法: コンピュータによる膨大な計算彼らは、あらゆる地図のパターンを、約1,500個の「基本的な形（不可避集合）」に分類しました。そして、それらすべてが4色以内で塗り分け可能であることを、当時のスーパーコンピュータを使って1,200時間以上かけて検証しました。
数学界への衝撃
この証明は、当時の数学界に論争を巻き起こしました。
- 「人間が検算できない」証明: 数学の証明は、論理のステップを人間が追うことで納得するものでしたが、これは「コンピュータの結果を信じるしかない」という新しい形でした。
- 美しさの欠如: 「エレガントな数式」ではなく「力技（ブルートフォース）」で解いたことへの抵抗感がありました。
現在では、この「コンピュータ支援証明」は一つの正当な手法として確立されており、四色定理はその先駆けとして歴史に刻まれています。19世紀の「手書き地図」から始まった疑問が、20世紀の「電子計算機」で解かれたという流れは、数学が抽象論理から計算科学へと融合していく象徴的な出来事と言えます。
1. 証明に使われたアルゴリズムの仕組み
四色定理の証明は、大きく分けて2つのアルゴリズム的ステップで構成されています。
- 不可避集合（Inevitable Set）の生成:平面上のどんな地図にも、必ず含まれる「特定のパーツ（部分グラフ）」のリストを作るプロセスです。
- 還元的（Reducible）かどうかの判定:「そのパーツを含む地図がもし5色必要なら、そのパーツを取り除いたもっと小さな地図も5色必要になるはずだ」という矛盾を突くチェックです。
もし「1,480個（現在はもっと少ない）のパーツすべてが還元的である」ことが確認できれば、「5色必要な地図はこの世に存在し得ない（＝4色で足りる）」ことが証明されます。アペルたちはこのチェックをコンピュータ・プログラム（アルゴリズム）に実行させたのです。
2. 「塗り分けるための」アルゴリズム
「4色で塗れることを証明する」のと、「実際に4色で塗り分ける」のは別ですが、具体的な塗り分けアルゴリズムも存在します。
- 多項式時間アルゴリズム:1996年にロバートソン、サンダース、シーモア、トーマスによって、与えられた地図（グラフ）を O(n^2) の時間（地図の国の数の2乗に比例する時間）で4色に塗り分けるアルゴリズムが考案されました。
- バックトラッキング:単純なプログラムでは、1つの国を塗って隣と被ったらやり直す「試行錯誤（バックトラッキング）」を行いますが、最悪の場合、計算時間が膨大になります。しかし、四色定理に基づく効率的なアルゴリズムを使えば、現実的な時間で必ず塗り分けが完了します。
3. アルゴリズムによる「証明の検証」
アペルたちの初証明は「プログラムにバグがあったらどうするんだ？」という批判にさらされました。しかし、2005年にジョルジュ・ゴンティエがCoqという「定理証明支援ソフト」を用いて、証明プロセス全体を厳密な論理アルゴリズムとして再構築しました。
これにより、「人間の計算ミス」も「プログラムのバグ」も入り込む余地のない、完全に機械的に検証された証明が完了しました。
まとめ：アルゴリズムが数学を変えた
四色定理は、「数学的な直感」を「アルゴリズム的な検証」が追い越した歴史的ケースです。
- 証明: アルゴリズムによって「4色で十分」と確定。
- 実践: アルゴリズムによって「どんなに複雑な地図も即座に」塗り分け可能。
「人間には理解しきれないほど複雑な組み合わせも、正しいアルゴリズムと計算機があれば真理に到達できる」という事実は、現代数学における一つの大きな転換点となりました。
平面であること」の絶対的な制約
4色で済む理由は、平面という「2次元の広がり」が持つ構造的な限界にあります。
- 5つの国が「お互いすべてに接する」ことができない: 平面上では、5つの国を配置して「どの国も他の4つの国すべてと直接境界線を接するようにする」ことが物理的に不可能です（オイラーの多面体定理から導かれます）。
- つまり、5色目が必要になるような「究極の密集状態」を平面上に作ることはできないのです。
- ただし、円の中心のように点が接点の場合は同じ色で塗り分けるという制約があります。
ただし、例外となる「歪さ」
「2次元平面」というルールを少しでも外れると、4色では足りなくなります。ここが数学の面白いところです。
- 飛び地がある場合: もし一つの国が「Ａ地点」と、遠く離れた「Ｂ地点」に分かれている（飛び地）場合、この定理は崩壊します。現実の世界地図で塗り分けが難しいのは、この「飛び地」があるためです。
- ドーナツ型（トーラス）の表面: 平面ではなく、穴の空いたドーナツのような形の表面に地図を描く場合、最大で7色必要になることが証明されています。