tsujimotterのノートブック

日曜数学者 tsujimotter の「趣味で数学」実践ノート

四色定理の証明 〜コンピュータを用いていかに解決されたか

今日は 四色定理 についてです。


「どんな平面地図でも4色あれば塗り分けられる。」


とても単純そうな主張ですが、この問題の解決には長大な年月がかかりました。そしてついに証明され、現在では定理となっています。

そのとき使われたのが、なんと コンピュータ でした。


しかし、ここで一つ疑問が湧きます。

地図なんて無限に作れるのに、
どうやってコンピュータで証明するの?


実は、四色定理の証明の面白さはまさにこの点にあります。

今回は、数学者たちがこの難問をどのようなアイデアで解決したのか、その証明の概略を紹介したいと思います。



この記事は、2024年12月1日に公開した下記の記事の再編集版です。
主題を四色定理の証明に変更して、読みやすい記事を目指しました。

tsujimotter.hatenablog.com


四色問題とは

四色問題は、地図の色の塗り分けに関する数学的な問題です。

「隣り合う国同士は異なる色で塗り分けるというルールで平面地図を塗ったときに、どんな平面地図であっても4色あれば塗り分けられることを証明せよ」
という問題です。

地図ではなく「平面地図」とわざわざ書いたのは、平面でない場合に(たとえばトーラス上の地図で)5色以上必要な例が作られてしまうからです。


日本地図はもちろん4色で塗り分けられます。

「どんな平面地図であっても」とあるので、日本地図や世界地図などの現存する地図が塗り分けられたからよいわけではないのがミソです。考え得るありとあらゆる地図 に対して4色で塗り分けられることを確認しないと、四色定理を証明できたことになりません。

たとえば、以下の図は適当に作った人工的な平面地図です。

果たしてこの地図も4色で塗り分けられるでしょうか?
(問題の解答例は記事の末尾にあります。よかったら考えてみてください。)

以上の例のように、現実のことを考えなければ地図なんて無限に考えられるわけで、こんな問題をいったいどうやって証明するのだろうと思うのが自然です。



なんと四色問題は現在では解決しており、四色定理と呼ばれています。
1976年、アッペルとハーケンはコンピュータの大きな助けを借りてこの問題を解決しました。
四色問題を提唱したのは1852年のガスリーなので、実に 124年間も未解決 だったことがわかります。相当な難問ですね。


この問題は単なる難問なだけでなく、物議を醸した問題でもあります。
実は四色定理の証明は、当時としては極めて異例だった コンピュータ を本質的に用いた証明なのです。

現在でも、コンピュータを用いない四色定理の証明は実現されていません。四色定理の証明は「数学の証明とは何か」という価値観を揺さぶる証明でした。



画像は計算に用いられた機種の一つ、IBM System/370


もちろん、コンピュータを使ったからと言って、数学的な要素が全くないというわけでもありません。
コンピュータが得意なのは有限の範囲の探索なので、1個1個の地図を素朴に塗り分けるだけでは、いくら待ってもプログラムが停止しません。地図は無限にあるので。

無限にある地図の可能性を、いかにして有限の範囲に押し込んで議論できるようにするか。
そこに数学者の技量があったわけで、いったいどのようなアイデアがそこにあったのか、興味を惹かれるところではないでしょうか。

その点を次の節で明らかにしていきましょう。


四色問題への4つのキーアイデア

四色問題はいかなる方法で解決されたのでしょうか。そこにバーコフのダイヤモンドを紐解くヒントがあります。

四色問題の証明に向けた、4つの重要なキーアイデアを紹介しましょう。


まず1つめのキーアイデアは、地図を グラフ で表すことです。

グラフとは、簡単に言ってしまえば点と線によって表された図形のことです。
「x軸y軸を引いて一次関数のグラフ〜」のようなグラフのことではありません。

たとえば、以下の九州の地図は、各県の真ん中に点を置いて、隣接する県同士の点を結ぶというルールによって、グラフで表現できます。

これを地図のグラフということにしましょう。

四色問題は「線で結ばれた点同士は異なる色で塗り分けるというルールで地図のグラフの点を塗ったときに、どんな地図のグラフであっても4色あれば塗り分けられることを証明せよ」という問題に、言い換えることができます。


このようにすることで、純粋に国同士の隣接関係のみに注目することができるようになり、見通しがよくなります。

なお、地図と地図のグラフの関係は、双対 の関係にあるとも言われます。


グラフを扱う数学の分野を「グラフ理論」といいます。

グラフ理論においては、特に「次数」という概念が重要です。点の次数とは、その点に接続されている線の本数のことです。

たとえば、先ほどの九州のグラフにおいて、それぞれの点の次数は次の図のようになります:

熊本県は4つの県に隣接していますので、次数が4ということになります。



2つめのキーアイデアは、背理法 を使うことです。

背理法により「四色問題は成り立たない」と仮定します。すると、四色で塗れない地図が存在することになります。

これらはいくつかあるかもしれないですが、特に四色で塗れない「最小」の反例があるはずです。これを最小反例ということにしましょう。

ここでいう最小とは、地図のグラフにおける「点の数」が最小であるということです。

この最小性から、これより「点の数」の少ない地図は、すべて4色で彩色できることになります。



四色定理最大のアイデア ―不可避集合と可約配置―

3つめと4つめのキーアイデアは、不可避集合 と 可約配置 を考えることなのですが、これらは素晴らしいアイデアです。

まとめて紹介しますが、定義は次の画像のとおりです:

画像に書いたとおり、もし仮に可約配置だけを要素に持つ不可避集合が作れたとすると、四色定理が証明できたことになります。実際、次のように証明できます。

まず、背理法により四色問題が誤りである、すなわち最小反例が存在すると仮定します。
最小反例というのは(定義より)可約配置を含みません。一方で、不可避集合の要素は必ず1つは含むはずですが、今考えている不可避集合の要素はすべて可約配置であるので、矛盾します。

したがって、反例が存在するという仮定が誤り、すなわち四色定理が証明できたことになります。


「可約配置だけを要素に持つ不可避集合」という有限の存在を作ることが四色定理の証明のキーというわけです。


不可避集合とは、どんな地図も必ず不可避集合を避けては通れない配置の集合ということになりますが、そんなもの作ることができるのでしょうか?

たとえば、次のような集合が不可避集合です。

実際、オイラーの多面体定理を用いると、

「任意の地図のグラフは次数5以下の点を必ず持つ」

が示せます。したがって、どんな地図であっても、上記の不可避集合の要素のいずれかは避けることができないというわけです。

こんなことに(「世界で二番目に美しい数式」で有名な)オイラーの多面体定理が使えるというのは驚きですし、結果も非自明で面白いですね。こんなふうに不可避集合を作ることができます。


しかしながら、上記の不可避集合では四色定理の証明はできません。

次数0〜4までは可約配置であることが示せます。

つまり、次数0〜4の点  v が最小反例に含まれるとしましょう。このとき、点  v を除いてできる地図は最小反例より小さい地図なので4色で塗り分けられます。
この状態で  v を戻したとき、次数0〜3の点の場合は周りの色と異なる色を塗れば良いですし、次数4の場合も周りをうまく塗り直すことで全体を4色で塗り分けることができます。
こんな具合で元の地図が4色で塗り分けられることが分かり、元の地図が反例であるという仮定に反します。

しかしながら、「次数5の点を1つ含む」という配置そのものは、残念ながら可約配置ではありません。

つまり、最小反例が次数5の点を含むとき、 v を除く周りは4色で塗り分けられるわけですが、この状態で  v を戻して再度4色で塗り直すということができないのです。


このような不可避集合によって四色問題の解決に挑んだのが ケンぺ という数学者です。ケンペはこの方法によって四色定理を証明したと考え、1879年にその証明を発表しました。
残念ながらその証明(次数5が可約配置であることの証明)が誤りであることが、1890年のヒーウッドによって指摘され、ケンぺの試みは失敗に終わりました。


そんなわけでケンぺの不可避集合では失敗したわけですが、すべての要素が可約配置であるような不可避集合が見つかりさえすれば四色定理が証明できます。実際、そんなうまい不可避集合を見つけることができるのでしょうか。


可約配置の例:バーコフのダイヤモンド

キーアイデア3と4を改めて再掲します。

私はこのアイデアを聞いたとき、感動しました。なるほど、こんな天才的な方法で、無限に思える四色問題を有限に押し込めることができるのかと。


実は、上記の「可約配置を用いて最小反例を排除する」という枠組みを早い段階で明確に打ち出したのが バーコフ という数学者です。さらに後年、ヘーシュらによって「不可避集合を作り、そのすべてを可約であると示す」という戦略が発展し、これがアッペルとハーケンの証明へつながります。

そしてそのバーコフが見つけた、(次数0〜4の点以外の)最初の可約配置が バーコフのダイヤモンド というわけです。


バーコフのダイヤモンドを見てみましょう。

左側が地図上の形を表していて、右側がその地図のグラフを表しています。これらは双対の関係にあります。


バーコフのダイヤモンドは次数5の点が4つ組み合わさって構成されています。実際には地図の中に配置されているわけですが、周囲には6つの点と接しています。

バーコフのダイヤモンドは可約配置なので、つまりこの配置は最小反例には含まれないということです。
これがとても重要な性質なわけですが、これを示すためにはバーコフのダイヤモンドが最小反例に含まれると仮定して矛盾を導く必要があります。

実際、最小反例に含まれると仮定すると、それより小さな地図は4色で塗り分けられることが保証されるわけです。
そこで、バーコフのダイヤモンドの部分を除いて、より小さな地図(下の図の右)を作ります。すると、4色で塗り分けることができます。

バーコフのダイヤモンドを元の地図に戻して、改めてバーコフのダイヤモンドの部分を4色で塗り分けられるか検討します。
実際には、バーコフのダイヤモンドの部分以外の部分も改めて塗り直す必要があり、塗り直して4色で塗り分けられることが示せます。

したがって、バーコフのダイヤモンドを含む最小反例が、実は4色で塗り分けられてしまったということが示されます(矛盾)。このことより、バーコフのダイヤモンドが最小反例には含まれない(可約配置であること)が証明されると言う寸法です。


しかしながら、ここで完全な証明をするためにはやや込み入った話になってしまいますので、またいつか別の記事で紹介したいと思います。

ここで伝えたいのは、バーコフのダイヤモンドは最初に見つかった非自明な可約配置であるということです。



四色定理の完遂

上で例に挙げたバーコフのダイヤモンドは、四色定理の証明に向けたアプローチの中で証明された最初の可約配置というわけですが、実は最終的な四色定理の証明にも関わっています。

最終的に、1976年のアッペルとハーケンによる証明では、1936個 の配置が検討されました。その過程では、「不可避集合を作るための探索」と「各配置が可約であることの検証」にコンピュータが使われました。


しかも、コンピュータが調べたのは単に1936個の配置だけではありません。

それぞれの配置が本当に可約であるかを調べるためには、その周囲の色の塗り方を大量に検討する必要があります。配置の周囲を取り囲む領域が14個ある場合、その本質的に異なる彩色パターンは199,291通りにもなります。これらを調べて可約性を判定するのは、人間の手作業では現実的ではありません。

ちなみに、バーコフのダイヤモンドの周囲には本質的に31通りの彩色があります。
実際、私は31通りすべて確認しました。これも後日に。

アッペルとハーケンらは、この可約性の検証のために複数のコンピュータを用い、合計で約1200時間もの計算を行ったとされています。その中には IBM System/370 も含まれていました。

ちなみに、実際に不可避集合を構成する際には「放電法」と呼ばれる非常に面白い手法が使われます。これはオイラーの多面体定理と深く関係する方法なのですが、この話はまた別の機会に。


最終的に得られたリストは、アッペルとハーケンの論文2報のうち、2報目の "Every planar map is four colorable. Part II: Reducibility" に図として掲載されています。

実は、一番左上にある図がバーコフのダイヤモンドです。

つまり、最終的に四色問題の解決に用いられたアッペルとハーケンの不可避集合のリストに、バーコフのダイヤモンドが載っているのです。


まとめると、バーコフのダイヤモンドは四色問題へのアプローチの提唱時に登場したというだけではなく、四色問題の解決にも一役買っているということですね。


最後まで読んでくださってありがとうございます!
それでは今日はこの辺で!!


おまけ:問題の解答例