四色定理
これは一応は認められたが、人手による実行が(事実上)不可能なほどの複雑なプログラムの実行によるものであることから、ハードウェアやソフトウェア(コンピュータやそのプログラム)のバグの可能性などの懸念から、その確実さについて疑問視する向きもあった。たとえば、東京女子大の小西善二郎講師は、元のSystem/370は現在入手不可能だが、等価回路で元のアセンブラによるプログラムの欠陥がないとは言えない、としている。
しかしその後、1996年にニール・ロバートソン(英語版)らによりアルゴリズムやプログラムの改良が行われ、より簡易な手法(従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えた)による再証明が行われるなど、第三者による複数の改良された証明が行われ、証明は確実視されるようになっていった。2004年にはジョルジュ・ゴンティエ(英語版)が定理証明系Coqを用いて、よりシンプルな証明を行うなど、コンピュータの応用手法の洗練により、より確かな手続きで証明が行われるなどしているため、現在では四色問題は解決していると捉えられている。
{\displaystyle 6v-2e=6\sum _{i=1}^{D}v_{i}-\sum _{i=1}^{D}iv_{i}=\sum _{i=1}^{D}(6-i)v_{i}=12.} .
しかし、12 > 0であり、すべてのi≥ 6に対して6 - i ≤ 0なので、これは次数5以下の頂点が少なくとも1つあることを示している。
もし5色を必要とするグラフがあるとすれば、そのようなグラフは最小であり、どの頂点を取り除いても4色になる。このグラフをGと呼ぶ。もしd(v) ≤ 3 ならば,Gからvを取り除き,小さいグラフを4色化した後,vを再び加え,隣と異なる色を選んで4色化を拡張することができるからである.
先ほどと同様に、頂点vを取り除き、残った頂点を4色に着色する。もしvの4つの隣がすべて異なる色、例えば時計回りの順序で赤、緑、青、黄であれば、赤と青の隣を結ぶ赤と青の頂点の交互のパスを探す。このような経路はケンプ鎖と呼ばれる。赤と青の隣同士を結ぶケンペ鎖があるかもしれないし,緑と黄の隣同士を結ぶケンペ鎖があるかもしれない.連鎖していないのは赤と青の隣同士だとする。赤と青の交互のパスで赤の隣の頂点に接続されているすべての頂点を探索し、これらのすべての頂点で赤と青の色を逆にする。その結果、やはり4色使いになり、vを戻して赤に着色することができる。
これで残るのは次数5の頂点がGにある場合だけであるが、ケンペの議論にはこの場合の欠陥があった。HeawoodはKempeの間違いに気付くと同時に、5色しか必要でないことを証明することで満足するのであれば、(最小反例が6色を必要とすることだけを変えて)上記の議論を実行し、次数5の状況でKempeの鎖を使って五色定理を証明することができることに気付いた。
当時の大型汎用コンピュータであるIBM System/370を1,200時間以上使用したといわれている。
複雑に思える問題に対して簡潔にまとまった比較的短い証明(解答)を、エレガントな証明(解答)と言うことがある。四色定理に対するある種「力業による証明」は、これとは対極にあるものとして揶揄を込めて「エレファント(象)」な証明とも言われた。5色による塗り分けが可能であることの証明が簡潔なものであるのとは対照的である。
その後アルゴリズムは改良されたが、現在でもコンピュータを利用しないで済ませられる証明は得られていない。それどころか完全に自然言語を離れて、プログラムにバグがないことも含めた四色定理の証明全体をコンピュータ上の証明検証系システム(ソフトウェア)Coqによってチェックさせた仕事がある。またコンピュータを使うこと以上に、証明の構成法自体が四色定理の解決のために特化していて、他の問題との関係性に乏しいことも数学者の間で人気のない理由になっている。