14/02/22 11:24:13.83
ウルフガング・ハーケン博士は、四色問題にシフトし、これを解決した。1976年のこと
URLﾘﾝｸ(ja.wikipedia.org)
いかなる地図も、隣接する領域が異なる色になるように塗るには4色あれば十分だという定理である。
解決前は四色問題と呼ばれており、未解決の期間が長かったため現在でも四色問題と呼ばれることがある。
1976年にケネス・アッペル (Kenneth Appel) とヴォルフガング・ハーケン (Wolfgang Haken) は、「放電」と呼ばれる手続きを考案し、1405個の不可避集合に対してコンピュータを利用した演算を行った結果、四色定理を証明するに至った[1][2][3]。
当初は、あまりに複雑なプログラムのため他人による検証が困難であることや、ハードウェアおよびプログラムのバグの可能性を考慮して、この証明を疑問視する声があった。
その後、1996年にニール・ロバートソン (Neil Robertson) らによりアルゴリズムやプログラムの改良が行われ、より簡易な手法（従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えた）による再証明が行われた[4]。
更に、2004年にはジョルジュ・ゴンティエ (Georges Gonthier) が定理証明支援系言語であるCoqを用いて、よりシンプルな証明を行った[5]。その結果、現在では四色問題の解決を否定する専門家はいなくなっている。
四色定理は実用的には地図作製だけでなく、携帯電話の基地局配置にも応用されている。周波数の同じ電波同士で混信してしまうFDMA・TDMA方式の携帯電話システムでは、隣接する基地局同士に同じ周波数を割り当てないように、配慮している。