# 四色定理：地図が4色で塗れる理由と、コンピュータが書いた最初の証明
> 「隣り合う国を違う色にするには4色で足りる」という四色定理を、オイラーの公式から導く六色定理・五色定理の証明とともに追い、1976年のコンピュータ支援証明が数学に残した問いまで扱います。
> https://rikai.mugen-giken.com/mathematics/math-columns/four-color-theorem
## 0. この記事の要点
- 平面に描かれたどんな地図も、隣り合う国が異なる色になるように **4 色**で塗り分けられます。これが四色定理です。
- 「地図」を「平面グラフ」に翻訳すると、問題は「平面グラフの頂点を 4 色で塗れるか」という、絵ではなく点と線の問題になります。
- オイラーの公式から「平面グラフには次数 5 以下の頂点が必ずある」が導かれ、そこから**六色定理**はほとんど自動的に、**五色定理**は「ケンペ鎖」という道具で証明できます。ここまでは紙と鉛筆で 1 時間の仕事です。
- ところが 5 から 4 への最後の一歩だけが異様に硬い。1976 年、Appel と Haken が約 1900 個の「配置」をコンピュータで検査してようやく決着しました。人間が全証明を読み切れない最初の主要定理です。
- 1997 年に証明は大幅に簡略化され、2005 年には証明支援系 Coq で完全に形式化されました。「コンピュータの証明を信じてよいか」という問いは、いまや「どのソフトウェアをどこまで信じるか」という、より具体的な問いに姿を変えています。
## 1. 動機：地図帳の塗り絵から始まった問題
1852 年、ロンドンの学生フランシス・ガスリー（Francis Guthrie）はイングランドの州の地図に色を塗っていて、あることに気づきました。隣り合う州を違う色にしたいのですが、どう工夫しても 4 色あれば足りてしまう。5 色目を使わざるをえない地図を作ろうとしても、なぜか作れない。
彼は弟のフレデリック（当時、数学者ド・モルガンの学生でした）にこの疑問を伝え、フレデリックは指導教員のド・モルガンに尋ねました。ド・モルガンは同年 10 月 23 日、ハミルトンに宛てた手紙でこの問題を紹介しています。四色問題の記録された誕生日です。
問いは子どもでも理解できます。
> 平面上の地図が与えられたとき、国境を共有する 2 国が必ず異なる色になるように塗り分けるには、何色あれば十分か。
「十分」の側は 4 色というのが答えです。「必要」の側、つまり 4 色ないと足りない地図があることは、すぐ後の
どれか 1 つを必ず含む"]
B --> D["可約性: リストのどの配置も
『それを含む最小反例』は作れない"]
C --> E["矛盾"]
D --> E
E --> F["最小反例は存在しない
= 四色定理は真"]`} />
平面グラフの一部分（頂点のいくつかと、それらの次数の情報を伴った小さな部分図）を**配置**と呼びます。
配置の有限集合 $\mathcal{U}$ が**不可避集合**であるとは、$\mathcal{U}$ のどの配置も含まないような平面三角形分割が存在しないことをいいます。言い換えれば、どんな地図も $\mathcal{U}$ の中の少なくとも 1 つの形を必ずどこかに持っている、ということです。
配置 $K$ が**可約**であるとは、$K$ を含む平面グラフ $G$ について、「$G$ より小さいすべての平面グラフが 4 彩色をもつ」という仮定のもとで $G$ 自身も 4 彩色をもつことが示せることをいいます。要するに $K$ は最小反例の中には現れられない、ということです。
不可避集合の全要素が可約なら、最小反例は「必ず含む形」を「含めない」ことになって矛盾します。これで証明は終わりです。