四色定理
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2024/03/23 13:51 UTC 版)
コンピュータによる証明
四色定理の証明法は次の2段階に分けられる。
- どのような平面グラフをとってきても、その集合に属するグラフのどれか一つが部分グラフとして含まれるグラフの集合を考える。このような性質をもつグラフの集合を不可避集合という。
- 不可避集合をうまく選ぶと、それに属するどのグラフも次の意味で可約にできる。すなわち、その部分グラフを含むグラフがあったとき、その部分グラフを除いたものが4色で塗り分けが可能ならば、グラフ全体も4色で塗り分けができる。
実際、もしも塗り分けに5色以上が必要な四色問題の反例となるグラフがあったとしたならば、その中で頂点の個数が最小のものを考える。すると、1.よりこのグラフは不可避集合に属する部分グラフを含む。2.により、この部分グラフを除いた、より頂点数の少ないグラフが既に四色問題の反例を与えることになる。しかし、それは最小の反例をとってきたという仮定に反する。
アッペルとハーケンはコンピュータによる実験を繰り返し、プログラムを何度も書き換えながら、可約なグラフから成る約2,000個のグラフからなる不可避集合を求めた。当時の大型汎用コンピュータであるIBM System/370[注 2]を1,200時間以上使用したといわれている。
複雑に思える問題に対して簡潔にまとまった比較的短い証明(解答)を、エレガントな証明(解答)と言うことがある。四色定理に対するある種「力業による証明」は、これとは対極にあるものとして揶揄を込めて「エレファント(象)」な証明とも言われた。5色による塗り分けが可能であることの証明が簡潔なものであるのとは対照的である。
その後アルゴリズムは改良されたが、現在でもコンピュータを利用しないで済ませられる証明は得られていない。それどころか完全に自然言語を離れて、プログラムにバグがないことも含めた四色定理の証明全体をコンピュータ上の証明検証系システム(ソフトウェア)Coqによってチェックさせた仕事がある。またコンピュータを使うこと以上に、証明の構成法自体が四色定理の解決のために特化していて、他の問題との関係性に乏しいことも数学者の間で人気のない理由になっている。
注釈
出典
- ^ K. Appel, W. Haken, "Every planar map is four colorable" (Bulletin of the American Mathematical Society Volume 82, Number 5, September 1976)
- ^ "Every planar map is four colorable. Part II: Reducibility" by K. Appel, W. Haken, and J. Koch (Illinois J. Math. Volume 21, Issue 3 (1977), 491–567.)
- ^ Contemporary mathematics 98 "Every Planar Map is Four Colorable" by Kenneth Appel and Wolfgang Haken
- ^ "A new proof of the four-colour theorem" by Neil Robertson, Damiel P. Sanders, Paul Seymour, and Robin Thomas (Electronic Research Announcements of the American Mathematical Society Volume 2, Number 1, August 1996)
- ^ "A computer-checked proof of the Four Colour Theorem" by Georges Gonthier (Microsoft Research Cambridge) http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf
- ^ Weisstein, Eric W. "Map Coloring". mathworld.wolfram.com (英語).
- ^ ガードナー & 一松 (1977)
- ^ 高木 (1976, XIV 最近の話題/パズルの最前線)によると、日本版『サイエンス』誌6月号に掲載、と見える。
- ^ a b 一松 (1978, pp. 197–204)
- ^ Weisstein, Eric W. "McGregor Map". mathworld.wolfram.com (英語). このページでその問題が見られるが、解答(ネタバレ、spoiler)もすぐ隣にあるので、パズルとして楽しみたい場合は他を探すこと。
- 1 四色定理とは
- 2 四色定理の概要
- 3 コンピュータによる証明
- 4 証明のアイディアの概要
- 5 3彩色問題
- 6 外部リンク
- 四色定理のページへのリンク