四色定理是一個著名的數學定理：如果在平面上劃出一些鄰接的有限區域，那麼可以用四種顏色來給這些區域染色，使得每兩個鄰接區域染的顏色都不一樣。被稱為鄰接的兩個區域是指它們有一段公共的邊界，而不僅僅是一個公共的交點。四色問題最早是由英國數學家法蘭西斯·古德里在1852年提出的。人們發現，要證明寬鬆一點的「五色定理」很容易，但四色問題卻出人意料地異常困難。1976年，數學家凱尼斯·阿佩爾和沃夫岡·哈肯藉助電腦首次得到一個完全的證明，四色問題也終於成為四色定理。這是首個主要藉助電腦證明的定理。
