四色問題如何證明？

12-02

1977 年的證明通告中相關的一段我貼在下面。簡短的證明思路即這些定義，他們所做的就是羅列出一個 "unavoidable set of reducible configurations".

通告地址：Appel
,
Haken
:
Every planar map is four colorable
完整的證明描述分兩部分
Appel
,
Haken
:
Every planar map is four colorable. Part I: Discharging（61頁）
Appel
,
Haken
,
Koch
:
Every planar map is four colorable. Part II: Reducibility（76頁，列出了集合）
所以大部分書籍和文章有理由省略具體證明，留給感興趣的讀者自己查資料（存在許多專著）。
第二部分中有關於程序本身的技術描述，相關段落貼在下面，用的是 IBM assembler language

我在維基百科裡面寫了一個比較詳細的介紹：
四色定理
水平有限，歡迎指正。

四色定理的一種表述是：二維球面的任何三角剖分都能被結點四色染，相鄰的結點不同色。簡單講，證明的方法是找出所有的可能出現的三角剖分，證明每一種情形都可以被四種顏色染。乍一看可能的圖形有無窮多種，但是做一定的限制（出現在某點的半徑為2，周長小於16的圓盤內）後，可能的情形就能一一列舉出來。然後使用反證法，假設某種情形不能被四色染，那麼可以推出某種更加簡單的情形也無法被四色染，由於這種窮舉是由簡單到複雜，而所有簡單的情形在前面都已經被證明一定可以被四色染，推出矛盾。
總之，證明的實質就是從簡單到複雜，把地圖每一種可能出現的局部情形都找出來，將每一種都用四色染

記得好像是使用計算機輔助證明的。

答主00後，四色問題還是小學時聽說的，當時只覺得很奇妙……
晚自習的時候突發奇想證了出來，very激動，然而明白並不是第一個證明出來的人類
僅供參考吧
第一行是接觸寫錯了
日期也寫錯了尷尬
估計會有疏漏，歡迎討論