1976年にケネス・アッペルとヴォルフガング・ハーケンは、ハインリヒ・ヘーシュにより考案された「放電法」と呼ばれる手続きを改良し、コンピュータを利用して約2000個の（後に1400個あまりに整理された）可約な配置からなる不可避集合を見出し、四色定理を「証明」するに至った。

これは一応は認められたが、人手による実行が（事実上）不可能なほどの複雑なプログラムの実行によるものであることから、ハードウェアやソフトウェア（コンピュータやそのプログラム）のバグの可能性などの懸念から、その確実さについて疑問視する向きもあった。

しかしその後、1996年にニール・ロバートソンらによりアルゴリズムやプログラムの改良が行われ、より簡易な手法（従来の放電手続きよりシンプルな放電手続きを考案し、不可避集合の数を1405個から633個に抑えた）による再証明が行われるなど、第三者による複数の改良された証明が行われ、証明は確実視されるようになっていった。

2004年にはジョルジュ・ゴンティエが定理証明系Coqを用いて、よりシンプルな証明を行うなど、コンピュータの応用手法の洗練により、より確かな手続きで証明が行われるなどしているため、現在では四色問題は解決していると捉えられている。