四色定理 四色定理の概要

ウィキペディア

四色定理

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/03/23 13:51 UTC 版)

4色に塗り分けられている（常にさらに外側の領域を想定することで、地図の外縁部は3色で塗り分け可能で、球面においても四色定理が成立することがわかる）

定理の正確な定式化

グラフ理論的に言えば、この定理はループのない平面グラフに対して次のことを述べている。平面グラフ${\displaystyle G}$

この地図では、Aと書かれた二つの地域は同じ国に属している。もしこれらの領域に同じ色を与えたいならば、5つの色が必要になる。なぜなら、2つのA領域は一緒になって他の4つの領域に隣接し、それぞれの領域は他のすべての領域に隣接しているからである。なお別々の領域に同じ色を持たせることは、平面の外側にそれらをつなぐ'ハンドル'を追加することでモデル化できる。

このような構成によって、この問題はトーラス（種数1の曲面）上の地図の色付け問題と等価になる。

よってまず、日常的な直感から離れた表現で記述し直すと「境界線によって囲まれたいくつかの領域からなる平面図形があり、境界線の一部を共有する（隣り合った）領域は異なった色で塗らなければならない、としたとき、4色あれば十分である」となる。

グラフ理論でとらえると、

「平面グラフは4彩色可能である」

という定理になる（後述）。

なお、境界線ではなく、点のみを共有する領域は隣り合っているものとはみなされず、互いに同色で塗ってもよい（飛び地の場合と同じく、この条件なしではやはり何色あっても足りなくなる。現実の地図では稀だが、有名なものでは米国に、1点に4州が接する「フォー・コーナーズ」という地点がある）。また平面だけでなく、球面の場合も同様である（平面の地図に、全周囲となる領域を加え、それを反対側の1点に集めるようにして球にすればよい。逆も同様）。しかし、ドーナツや「繋がったドーナツ」のような、穴がある形状の表面については同様とはいかない（これも後述）。

証明される前は四色問題と呼ばれることもあり、1975年に証明されたのだが、未証明の期間が長かったため現在でも四色問題と呼ばれることがある。

3つの境界線が1点に集まっている場所があるため、3色必要であることはただちに明らかである。続いて、ある領域の周囲にいくつかの領域がある場合（日本地図では長野県のような場合）を考える。周囲の領域の個数が偶数であれば3色で塗り分けできるが（長野県の場合はそうなる^{[注 1]}）、奇数個の領域で囲まれている場合は3色での塗り分けは不可能で、どうしても4色が必要である。そして、4色あればどんな場合でも塗り分け可能なのか？　ということが問題である。

前述のように、グラフ理論により「平面グラフは4彩色可能である」という定理となる（証明もグラフ理論によってなされている）。参考例を図に示すが、まず、地図の境界線をグラフの辺、境界線が接続する点をグラフの頂点としたグラフを作る。その双対グラフにおける頂点の彩色が、元の地図の塗分けと同じ問題となる。

また、このような領域の塗り分けが有限の色数で必ず可能となるのは平面（二次元）以下の次元までであり、三次元以上では領域の取り方次第でいくらでも色数が必要な例が作れる。

歴史

（海や他国領土の色を除いて）4色に塗り分けられたアメリカ合衆国の州

1852年に法科学生のフランシス・ガスリーが数学専攻である弟のフレデリック・ガスリー（英語版）に質問したのを発端に問題として定式化され、19世紀後半になって数学者がその話を聞いて証明を試みたが、多くの数学者の挑戦をはねのけ続けていた。

1879年、アルフレッド・ケンプ（英語版）による証明が『アメリカ数学ジャーナル』誌上で発表された。この証明は妥当と見なされていたが、1890年になってパーシー・ヒーウッド（英語版）により不備が指摘された。しかし、ケンプの証明で使われた論理に沿って、地図を塗り分けるには5色で十分であることが証明された。これは五色定理と呼ばれている。4色で十分かどうかは、グラフ理論における最も有名な未解決問題として残った。

1976年にケネス・アッペル（英語版）とヴォルフガング・ハーケンは、ハインリヒ・ヘーシュ（英語版）により考案された「放電法」と呼ばれる手続きを改良し、コンピュータを利用して約2000個の（後に1400個あまりに整理された）可約な配置からなる不可避集合を見出し、四色定理を「証明」するに至った^[1][2][3]。

これは一応は認められたが、人手による実行が（事実上）不可能なほどの複雑なプログラムの実行によるものであることから、ハードウェアやソフトウェア（コンピュータやそのプログラム）のバグの可能性などの懸念から、その確実さについて疑問視する向きもあった。たとえば、東京女子大の小西善二郎講師は、元のSystem/370は現在入手不可能だが、等価回路で元のアセンブラによるプログラムの欠陥がないとは言えない、としている。

しかしその後、1996年にニール・ロバートソン（英語版）らによりアルゴリズムやプログラムの改良が行われ、より簡易な手法（従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えた）による再証明が行われる^[4]など、第三者による複数の改良された証明が行われ、証明は確実視されるようになっていった。2004年にはジョルジュ・ゴンティエ（英語版）が定理証明系Coqを用いて、よりシンプルな証明を行うなど^[5]、コンピュータの応用手法の洗練により、より確かな手続きで証明が行われるなどしているため、現在では四色問題は解決していると捉えられている。