Teorem empat warna menyatakan bahawa mana-mana peta yang dilukis pada satah rata boleh diwarnakan menggunakan paling banyak empat warna supaya tiada dua rantau yang berkongsi sempadan mempunyai warna yang sama. Dua rantau yang hanya bersentuhan pada satu titik boleh berkongsi warna. Teorem ini terpakai kepada mana-mana peta, walau serumit mana sekalipun.
Rantau 1, 2, 3, 4 masing-masing berjiran dengan beberapa rantau lain. Rantau kiri (4) dan kanan (4) tidak berkongsi sempadan, jadi kedua-duanya boleh berkongsi satu warna. Tepat 4 warna diperlukan di sini.
Francis Guthrie mencadangkan teorem ini pada tahun 1852 ketika mewarnakan peta daerah-daerah England. Beliau menyedari bahawa empat warna sentiasa kelihatan mencukupi tetapi tidak dapat membuktikannya. Masalah ini membingungkan ahli matematik selama 124 tahun. Banyak bukti palsu diterbitkan lalu disangkal. Lima warna sentiasa mencukupi dan boleh dibuktikan dengan tangan menggunakan formula Euler bagi graf planar.
Teorem empat warna mengambil masa 124 tahun dari konjektur ke bukti. Bukti tahun 1976 ialah teorem besar pertama yang disahkan dengan komputer.
Bukti tahun 1976 oleh Kenneth Appel dan Wolfgang Haken ialah teorem besar pertama yang dibuktikan dengan komputer. Ia mengurangkan semua peta yang mungkin kepada 1,936 konfigurasi dan komputer mengesahkan setiap satunya sepanjang lebih 1,200 jam masa CPU. Ramai ahli matematik tidak selesa dengan bukti yang tidak boleh diperiksa sepenuhnya dengan tangan. Bukti yang benar-benar boleh dibaca manusia, jika ada, masih belum ditemui.
Lima rantau luar (bilangan ganjil) memaksa gelang itu menggunakan 3 warna: kitaran 5 tidak boleh diwarnakan dengan hanya 2 warna. Rantau pusat berjiran dengan kelima-limanya, jadi ia menyentuh ketiga-tiga warna gelang dan mesti menjadi warna keempat. Ini menunjukkan bahawa empat warna kadang-kadang benar-benar diperlukan.
Setiap peta yang dilukis pada satah boleh diwarnakan menggunakan paling banyak empat warna supaya tiada dua rantau yang berkongsi sempadan mempunyai warna yang sama. Francis Guthrie mengemukakannya pada tahun 1852. Appel dan Haken membuktikannya pada tahun 1976 dengan menggunakan komputer untuk mengesahkan 1,936 konfigurasi, menjadikannya teorem besar pertama yang dibuktikan dengan bantuan komputer. Pengesahan yang lebih pendek oleh Robertson, Sanders, Seymour, dan Thomas pada tahun 1997 mengurangkannya kepada 633 konfigurasi. Teorem ini tidak sah pada torus, di mana sehingga tujuh warna mungkin diperlukan.