Teorema empat warna

Masalah Guthrie atau Teorema Empat Warna menyatakan bahwa setiap peta dapat diwarnai dengan menggunakan empat warna, sehingga daerah yang berbatasan tidak memiliki warna yang sama. Pada tahun 1976, Masalah Guthrie menjadi teorema matematika pertama yang dibuktikan menggunakan komputer, akan tetapi ditolak akibat pembuktiannya yang terlalu sulit bagi manusia. Sejak saat itu, bukti ini telah diterima secara luas, meskipun beberapa orang masih meragukannya. Teorema empat warna dibuktikan pada tahun 1976 oleh Kenneth Appel dan Wolfgang Haken setelah banyak pembuktian dan counterexample yang keliru. Untuk menghilangkan keraguan yang tersisa tentang pembuktian Appel-Haken, pembuktian yang lebih sederhana menggunakan ide yang sama dan masih mengandalkan komputer diterbitkan pada tahun 1997 oleh Robertson, Sanders, Seymour, dan Thomas. Selain itu, pada tahun 2005, teorema tersebut dibuktikan oleh Georges Gonthier dengan perangkat lunak pembuktian teorema tujuan umum.