Định lý bốn màu

Mọi bản đồ trên mặt phẳng đều có thể tô bằng tối đa $4$ màu sao cho không có hai miền nào chung một đường biên (nhiều hơn các điểm cô lập) có cùng màu. Một cách tương đương, mọi đồ thị phẳng không khuyên $G$ đều tô màu đỉnh được bằng $4$ màu, tức là sắc số của nó thỏa mãn $\chi(G) \le 4$.

Sau khi chứng minh nổi tiếng năm 1879 của Alfred Kempe được chấp nhận suốt mười một năm trước khi Percy Heawood chỉ ra lỗ hổng vào năm 1890 (nhưng cứu vãn được định lý $5$ màu), bài toán này đã trở thành định lý lớn đầu tiên được chứng minh với sự trợ giúp thiết yếu của máy tính. Năm 1976, Kenneth Appel và Wolfgang Haken (với sự hỗ trợ lập trình của John Koch) kết hợp phương pháp phóng điện của Heesch với việc kiểm tra vét cạn bằng máy tính trên $1{,}936$ (sau rút xuống $1{,}476$) cấu hình khả quy, tiêu tốn hơn $1{,}200$ giờ chạy máy IBM 370. Vì người phản biện không thể kiểm tra bằng tay toàn bộ phân tích trường hợp của máy tính, chứng minh này đã khơi mào nhiều tranh luận triết học. Năm 1997, Neil Robertson, Daniel P. Sanders, Paul Seymour và Robin Thomas công bố một chứng minh gọn hơn, chỉ cần $633$ cấu hình cùng quy tắc phóng điện sáng sủa hơn. Cuối cùng, năm 2005, Georges Gonthier (phát triển từ công trình chung với Benjamin Werner) hoàn tất một chứng minh hình thức hóa được máy kiểm tra toàn bộ cho chứng minh Robertson–Sanders–Seymour–Thomas trong trợ lý chứng minh Coq, xóa bỏ mọi nghi ngờ về lỗi phần mềm hay các trường hợp chưa kiểm chứng.