Định lý bốn màu

Quy về phản ví dụ nhỏ nhất. Nếu định lý sai, lấy một đồ thị phẳng cần từ 5 màu trở lên với số đỉnh ít nhất có thể. Thêm cạnh vào một đồ thị phẳng mà vẫn giữ tính phẳng chỉ có thể làm tăng số màu cần dùng, nên phản ví dụ nhỏ nhất này có thể coi là một đồ thị phẳng cực đại (một phép tam giác hóa), trong đó mọi miền, kể cả miền ngoài, đều được giới hạn bởi đúng 3 cạnh.

Thiết lập phương pháp xả điện tích. Gán cho mỗi đỉnh $v$ một điện tích ban đầu $6 - \deg(v)$. Dùng $V - E + F = 2$ cùng với $2E = \sum_v \deg(v)$ và $3F \le 2E$ (mỗi miền có ít nhất 3 cạnh), tổng điện tích trên mọi đỉnh tính ra đúng bằng $12$, do đó dương ngặt. Phương pháp xả điện tích sau đó chuyển điện tích cục bộ giữa các đỉnh lân cận theo một tập quy tắc cố định, không làm thay đổi tổng này; phân tích xem điện tích dương còn sót ở đâu sau khi xả cho thấy phải tồn tại một đỉnh bậc thấp cùng một kiểu lân cận cụ thể nào đó xuất hiện đâu đó trong đồ thị. Hữu hạn các kiểu này gọi là các cấu hình không thể tránh, vì ít nhất một trong chúng luôn có mặt trong mọi phép tam giác hóa phẳng.

Tính khử được. Một cấu hình được gọi là khử được nếu, mỗi khi nó xuất hiện trong một phản ví dụ nhỏ nhất giả định, mọi cách tô 4 màu của đồ thị nhỏ hơn thu được bằng cách bỏ hoặc co cấu hình đó luôn có thể mở rộng lại thành một cách tô 4 màu của toàn đồ thị, mâu thuẫn với tính nhỏ nhất. Appel và Haken (1976) đã kiểm tra bằng máy tính rằng mọi cấu hình trong danh sách 1.936 cấu hình không thể tránh của họ (sau này được rút gọn còn 633 bởi Robertson, Sanders, Seymour và Thomas năm 1997) đều khử được, dùng hơn một nghìn giờ máy tính. Điều này khiến định lý bốn màu trở thành định lý lớn đầu tiên có chứng minh dựa cốt yếu vào tính toán máy móc, sau đó được kiểm chứng lại độc lập và, năm 2005, được kiểm tra hình thức từng dòng trong trợ lý chứng minh Coq bởi Gonthier.

Kết luận. Vì mọi cấu hình không thể tránh đều khử được, không thể tồn tại phản ví dụ nhỏ nhất: không đồ thị phẳng nào cần từ 5 màu trở lên, nên $\chi(G) \le 4$ với mọi đồ thị phẳng $G$.