Lời giải: Chứng minh xả tải của Appel–Haken với tính khử được kiểm tra bằng máy tính (1976)

Mỗi bản đồ cho một đồ thị phẳng qua phép đối ngẫu: đặt một đỉnh vào trong mỗi miền của bản đồ và nối hai đỉnh bằng một cạnh mỗi khi hai miền đó chung một cạnh biên. Bản đồ tô được bằng bốn màu khi và chỉ khi đồ thị đối ngẫu $G$ này thỏa $\chi(G) \le 4$, trong đó $\chi(G)$ là số tô màu — số màu ít nhất trong một phép tô đỉnh đúng. Khuyên không bao giờ xuất hiện (không miền nào tự kề chính nó) và các cạnh song song có thể gộp thành một mà không ảnh hưởng tới khả năng tô màu, nên $G$ có thể lấy là đồ thị phẳng đơn.

Giả sử định lý sai và chọn một phản ví dụ $G$ có ít đỉnh nhất: tính sắp thứ tự tốt của số tự nhiên bảo đảm một $G$ như vậy tồn tại bất cứ khi nào có phản ví dụ nào. Tính tối thiểu là động cơ của toàn bộ lập luận — mọi đồ thị con thực sự hay đồ thị co của $G$ đều nhỏ hơn, do đó tô được bằng bốn màu, và mọi bước sau đều khai thác điều này bằng cách tô một đồ thị nhỏ hơn rồi sửa phép tô trên phần đã bỏ đi. Điều đó cũng giải thích vì sao $G$ không thể quá thưa lẫn quá cứng: $K_5$ không phẳng, nên $G$ không thể chỉ là một trở ngại kiểu đồ thị đầy đủ, và tính phẳng buộc $G$ chứa cấu trúc bậc thấp được nghiên cứu ở bước tiếp theo.

Chiến lược — giả sử một phản ví dụ tối thiểu rồi chỉ ra mọi cấu trúc con bắt buộc phải có của nó đều khử được — bắt nguồn từ nỗ lực năm 1879 của Kempe (có lỗi mà Heawood chỉ ra năm 1890) và được Birkhoff rồi Heesch phát triển; chính Heesch đưa ra các khái niệm tập không thể tránh và tính khử được mà Appel và Haken đã hoàn tất trong bài báo năm 1977 trên Illinois Journal of Mathematics.