Twierdzenie o czterech barwach mówi, że każdą mapę narysowaną na płaszczyźnie można pokolorować najwyżej czterema kolorami tak, aby żadne dwa regiony mające wspólną granicę nie miały tego samego koloru. Dwa regiony stykające się tylko w jednym punkcie mogą mieć tę samą barwę. Twierdzenie dotyczy każdej mapy, bez względu na to, jak jest złożona.
Regiony 1, 2, 3 i 4 graniczą z wieloma innymi. Lewy region (4) i prawy region (4) nie mają wspólnej granicy, więc mogą mieć ten sam kolor. W tym przykładzie naprawdę potrzeba dokładnie 4 kolorów.
Francis Guthrie sformułował to przypuszczenie w 1852 roku podczas kolorowania mapy hrabstw Anglii. Zauważył, że cztery kolory zawsze wydają się wystarczać, ale nie potrafił tego udowodnić. Problem opierał się matematykom przez 124 lata. Opublikowano wiele fałszywych dowodów, które później obalono. Pięć kolorów zawsze wystarcza i można to udowodnić ręcznie za pomocą wzoru Eulera dla grafów planarnych.
Od hipotezy do dowodu twierdzenie o czterech barwach potrzebowało 124 lat. Dowód z 1976 roku był pierwszym wielkim twierdzeniem zweryfikowanym przez komputer.
Dowód z 1976 roku autorstwa Kennetha Appela i Wolfganga Hakena był pierwszym wielkim twierdzeniem udowodnionym z pomocą komputera. Zredukowali oni wszystkie możliwe mapy do 1936 konfiguracji i kazali komputerowi sprawdzić każdą z nich przez ponad 1200 godzin czasu procesora. Wielu matematyków nie ufało dowodowi, którego nie dało się prześledzić ręcznie. Czy istnieje w pełni „ludzki” dowód, nadal nie wiadomo.
Pięć zewnętrznych regionów (liczba nieparzysta) wymusza użycie 3 kolorów w pierścieniu: cyklu długości 5 nie da się pokolorować dwoma kolorami. Region środkowy sąsiaduje ze wszystkimi pięcioma, więc styka się z wszystkimi trzema kolorami pierścienia i musi dostać czwarty kolor. To pokazuje, że cztery kolory są czasem naprawdę konieczne.
Każdą mapę narysowaną na płaskiej powierzchni można pokolorować co najwyżej czterema kolorami tak, aby żadne dwa regiony mające wspólną granicę nie miały tej samej barwy. Hipotezę sformułował Francis Guthrie w 1852 roku. Appel i Haken udowodnili ją w 1976 roku, wykorzystując komputer do sprawdzenia 1936 konfiguracji, co uczyniło ją pierwszym wielkim twierdzeniem dowiedzionym z pomocą komputera. Krótsza weryfikacja Robertsona, Sandersa, Seymoura i Thomasa z 1997 roku zmniejszyła tę liczbę do 633 konfiguracji. Twierdzenie nie obowiązuje na torusie, gdzie może być potrzebnych nawet siedem kolorów.