Twierdzenie o czterech barwach

Każdą mapę na płaszczyźnie (lub sferze) można pokolorować czterema barwami tak, by żadne dwa regiony graniczące ze sobą odcinkiem nie miały tego samego koloru.

W języku grafów: każdy graf planarny da się pokolorować czterema kolorami tak, by końce każdej krawędzi miały różne kolory.

Co mówi twierdzenie

Weź dowolną mapę - polityczną, powiatową, wymyśloną, choćby najbardziej poplątaną - i spróbuj pokolorować regiony tak, żeby sąsiedzi zawsze różnili się kolorem. Twierdzenie mówi, że cztery kredki zawsze wystarczą. Nie „zwykle”, nie „dla rozsądnych map” - zawsze.

Jedno zastrzeżenie w definicji sąsiedztwa: regiony muszą stykać się odcinkiem granicy, a nie pojedynczym punktem. Pola szachownicy stykające się rogami nie są sąsiadami - dlatego szachownicę kolorują dwie barwy.

Cztery regiony, z których każdy graniczy z każdym - taka mapa wymaga czterech barw, więc trzech kolorów nie da się zejść.

Rysunek pokazuje, że mniej niż cztery barwy nie wystarczą: trzy trójkąty stykają się parami wzdłuż odcinków, a otaczające tło graniczy z każdym z nich - cztery regiony parami sąsiednie wymuszają cztery różne kolory. Cała trudność twierdzenia leży w drugiej połowie: pokazać, że cztery barwy zawsze wystarczą. Ta połowa opierała się matematykom przez $124$ lata.

Od mapy do grafu

Każdej mapie odpowiada graf: region to wierzchołek, wspólna granica to krawędź. Taki graf jest planarny - da się go narysować bez przecinających się krawędzi (wierzchołki stawiamy wewnątrz regionów, a krawędzie prowadzimy przez wspólne granice). Kolorowanie mapy to kolorowanie wierzchołków tego grafu.

To ta sama sztuczka, która rozstrzygnęła zagadkę mostów królewieckich: zapomnij o kształtach, zostaw samą strukturę sąsiedztwa. Dzięki niej możemy korzystać z twierdzeń o grafach planarnych - w szczególności z nierówności $K \leq 3W - 6$ , wyprowadzonej ze wzoru Eulera.

Dowód twierdzenia o sześciu barwach

Pokaż dowódUkryj dowód

Pełny dowód czterech barw nie mieści się na tej stronie (ani w żadnej książce - o tym niżej). Ale osłabioną wersję z sześcioma barwami można udowodnić uczciwie i w całości.

Krok 1. W grafie planarnym istnieje wierzchołek o stopniu co najwyżej $5$ . Ze wzoru Eulera wynika, że graf planarny o $W \geq 3$ wierzchołkach ma co najwyżej $K \leq 3W - 6$ krawędzi. Suma stopni wszystkich wierzchołków to $2K \leq 6W - 12$ , więc średni stopień jest mniejszy od $6$ - a skoro średnia jest mniejsza od $6$ , to któryś wierzchołek ma stopień co najwyżej $5$ .

Krok 2. Indukcja po liczbie wierzchołków. Graf o co najwyżej $6$ wierzchołkach kolorujemy trywialnie - każdy wierzchołek innym kolorem. Załóżmy, że każdy graf planarny o mniej niż $W$ wierzchołkach da się pokolorować sześcioma barwami.

Krok 3. Usuwamy oszczędny wierzchołek. W grafie o $W$ wierzchołkach bierzemy wierzchołek $v$ o stopniu co najwyżej $5$ (istnieje z kroku 1) i chwilowo go usuwamy. Reszta jest planarna i mniejsza, więc z założenia indukcyjnego koloruje się sześcioma barwami.

Krok 4. Wstawiamy $v$ z powrotem. Jego sąsiedzi zużywają co najwyżej $5$ z $6$ kolorów - co najmniej jeden kolor jest wolny i dajemy go $v$ . Indukcja zamknięta. $\blacksquare$

Cały dowód mieści się w czterech krokach. Zejście z $6$ do $5$ wymaga już sprytu, a z $5$ do $4$ - komputera.

Dowód twierdzenia o pięciu barwach - metoda Kempego

Pokaż dowódUkryj dowód

Tu pojawia się pomysł, na którym stoi cała historia tego twierdzenia: łańcuchy Kempego.

Krok 1. Ta sama indukcja, trudniejszy przypadek. Jak wyżej bierzemy wierzchołek $v$ stopnia co najwyżej $5$ i kolorujemy resztę pięcioma barwami. Jeśli sąsiedzi $v$ zużywają co najwyżej $4$ kolory - jest kolor wolny i koniec. Problem powstaje tylko, gdy $v$ ma dokładnie $5$ sąsiadów $n_1, \ldots, n_5$ (ponumerowanych zgodnie z ruchem wskazówek zegara) w pięciu różnych kolorach $1, \ldots, 5$ .

Krok 2. Łańcuch Kempego. Spójrzmy na podgraf złożony tylko z wierzchołków w kolorach $1$ i $3$ . Jeśli $n_1$ i $n_3$ leżą w różnych spójnych kawałkach tego podgrafu, to w kawałku zawierającym $n_1$ zamieniamy kolory $1 \leftrightarrow 3$ . To legalne (wymieniamy kolory w całym kawałku naraz, więc żadna krawędź nie łączy dwóch jednakowych), a po zamianie $n_1$ ma kolor $3$ - kolor $1$ zwalnia się dla $v$ .

Krok 3. A jeśli łańcuch jest spójny? Wtedy od $n_1$ do $n_3$ biegnie ścieżka naprzemiennie kolorowana $1$ - $3$ , która razem z $v$ zamyka pętlę. Ta pętla oddziela $n_2$ (w środku) od $n_4$ (na zewnątrz) - i tu wkracza planarność: łańcuch kolorów $2$ - $4$ wychodzący z $n_2$ nie może dotrzeć do $n_4$ , bo musiałby przeciąć pętlę, a przecięć w grafie planarnym nie ma.

Krok 4. Druga zamiana. Skoro $n_2$ i $n_4$ są w różnych kawałkach podgrafu $2$ - $4$ , zamieniamy kolory w kawałku z $n_2$ - kolor $2$ zwalnia się dla $v$ . $\blacksquare$

Słynny błąd - dowód, który był prawdziwy przez 11 lat

W 1879 roku londyński prawnik i matematyk Alfred Kempe opublikował dowód twierdzenia o czterech barwach oparty na powyższej metodzie. Dowód przyjęto z uznaniem, Kempe został członkiem Royal Society, a sprawę uważano za zamkniętą.

W 1890 roku Percy Heawood znalazł lukę: przy czterech barwach w kroku analogicznym do naszego kroku 4 trzeba wykonać dwie zamiany łańcuchów jednocześnie - a Heawood skonstruował mapę, w której te zamiany wchodzą sobie w drogę (pierwsza przestawia kolory tak, że druga przestaje być legalna). Dowód upadł.

Heawood uratował z niego, co się dało - właśnie twierdzenie o pięciu barwach - i uczciwie przyznał, że czterech udowodnić nie potrafi. Problem wrócił do stanu otwartego na kolejne $86$ lat. Morał zostaje aktualny: recenzja może przeoczyć subtelny błąd nawet w sławnym wyniku, a zepsuty dowód bywa cenny - metoda łańcuchów Kempego przetrwała i ostatecznie zapracowała w prawdziwym dowodzie.

Pierwsze twierdzenie udowodnione komputerowo

W 1976 roku Kenneth Appel i Wolfgang Haken z Uniwersytetu Illinois ogłosili dowód. Jego plan jest klasyczny - dowód nie wprost przez minimalny kontrprzykład - ale skala nie:

zbiór nieunikniony: lista $1936$ konfiguracji (małych fragmentów mapy), z których co najmniej jedna musi wystąpić w każdej mapie planarnej;
redukowalność: dla każdej z tych konfiguracji pokazuje się, że nie może wystąpić w najmniejszej mapie wymagającej pięciu barw - kolorowanie reszty dałoby się rozszerzyć, m.in. łańcuchami Kempego.

Skoro każda mapa zawiera którąś konfigurację, a żadna konfiguracja nie mieści się w minimalnym kontrprzykładzie - kontrprzykład nie istnieje. Sprawdzenie redukowalności wymagało jednak ponad tysiąca godzin pracy komputera i nie dało się prześledzić ręcznie.

Wybuchła dyskusja filozoficzna: czy to w ogóle jest dowód, skoro żaden człowiek nie jest w stanie go przeczytać? Wątpliwości gasły etapami. W 1997 roku Robertson, Sanders, Seymour i Thomas uprościli dowód (633 konfiguracje) i zautomatyzowali także część „nieuniknioności”. W 2005 roku Georges Gonthier sformalizował całość w asystencie dowodów Coq - odtąd poprawności nie pilnuje program napisany ad hoc, lecz maleńkie, wielokrotnie zweryfikowane jądro logiczne. Dziś dowody wspomagane komputerowo są w matematyce codziennością, a twierdzenie o czterech barwach było ich pierwszym wielkim precedensem.

Co NIE wynika z twierdzenia

Prawdziwe mapy polityczne mogą wymagać więcej barw - twierdzenie zakłada, że każdy region jest spójny. Państwo z eksklawą (jak Rosja z obwodem królewieckim) to formalnie dwa regiony, które muszą dostać ten sam kolor - i taka dodatkowa więź potrafi wymusić piątą barwę.
Na innych powierzchniach liczba barw jest inna. Na torusie potrzeba i wystarcza siedem barw - istnieje tam mapa siedmiu regionów parami sąsiednich. Ogólny wzór Heawooda wiąże liczbę barw z liczbą „dziur” powierzchni, czyli z jej charakterystyką Eulera. Paradoksalnie przypadki „trudniejszych” powierzchni udowodniono na długo przed płaszczyzną.
Cztery barwy to gwarancja, nie przepis. Twierdzenie mówi, że kolorowanie istnieje, ale szybkie znajdowanie oszczędnych kolorowań to osobny problem: rozstrzygnięcie, czy mapie wystarczą trzy barwy, jest NP-zupełne.

Po co to komu

Kolorowanie grafów, którego to twierdzenie jest najsłynniejszym przykładem, to codzienne narzędzie informatyki:

przydział częstotliwości - nadajniki, które się zagłuszają, łączymy krawędzią; kolory to częstotliwości;
rejestry procesora - kompilator koloruje graf konfliktów zmiennych; zmienne „żyjące” jednocześnie muszą trafić do różnych rejestrów;
układanie planów - egzaminy współdzielące studentów dostają różne terminy (kolory);
sudoku to dokładnie kolorowanie grafu $81$ wierzchołków dziewięcioma kolorami.

Sama liczba „cztery” bywa w tych zastosowaniach mniej ważna niż metody rozwijane przez półtora wieku prób - łańcuchy Kempego, redukowalność, algorytmy kolorowania.

Kto i kiedy

Problem postawił w 1852 roku student Francis Guthrie, kolorując mapę hrabstw Anglii. Jego brat przekazał pytanie Augustusowi De Morganowi, a ten rozpisał je w listach - tak zagadka weszła do obiegu. W 1878 roku Arthur Cayley oficjalnie przyznał, że nie umie jej rozstrzygnąć.

Dalej: Kempe (1879) - dowód z ukrytą luką; Heawood (1890) - obalenie i pięć barw; dziesiątki częściowych wyników przez cały XX wiek; Appel i Haken (1976) - dowód komputerowy; Robertson, Sanders, Seymour, Thomas (1997) - uproszczenie; Gonthier (2005) - pełna formalizacja w Coq. Uniwersytet Illinois świętował wynik z 1976 roku stemplem pocztowym „Four colors suffice”.

Najczęstsze pytania

Czy regiony stykające się jednym punktem muszą mieć różne kolory? Nie - sąsiedztwo wymaga wspólnego odcinka granicy. Gdyby liczyć styk punktowy, twierdzenie byłoby fałszywe: wystarczy tort pokrojony na $n$ kawałków spotykających się w środku.

Czy ktoś kiedyś znalazł mapę wymagającą pięciu barw? Nie - i twierdzenie gwarantuje, że nikt nie znajdzie. Przez dekady amatorzy nadsyłali „kontrprzykłady”; wszystkie dawały się pokolorować czterema barwami, zwykle po dłuższej chwili kombinowania.

Dlaczego dowód komputerowy budził opór? Bo łamał dotychczasową umowę: dowód był zawsze tekstem, który kompetentny czytelnik może zweryfikować od początku do końca. Tu zaufanie przeniosło się częściowo na sprzęt i program. Formalizacja w Coq (2005) odpowiedziała na ten zarzut mocniej, niż potrafi klasyczna recenzja - każdy krok sprawdziło minimalne, audytowalne jądro logiczne.

Czy istnieje krótki, „ludzki” dowód czterech barw? Nie znamy żadnego i nie wiadomo, czy istnieje. Wszystkie znane dowody sprowadzają się do sprawdzenia setek konfiguracji. To osobliwe: twierdzenie brzmi jak zagadka dla dzieci, a opiera się każdej próbie eleganckiego argumentu.

Ile barw potrzeba na torusie? Siedem - i to jest osiągalne: na torusie da się narysować siedem regionów, z których każdy graniczy z każdym. Wersję dla powierzchni z dziurami (wzór Heawooda) udowodniono w pełni w 1968 roku, osiem lat przed płaszczyzną.

Podsumowanie

Cztery barwy wystarczą do pokolorowania każdej mapy planarnej; cztery bywają konieczne, co pokazuje mapa czterech regionów parami sąsiednich.
Sześć barw dowodzi się w cztery kroki (wierzchołek stopnia $\leq 5$ ze wzoru Eulera + indukcja), pięć - łańcuchami Kempego, cztery - tylko komputerowo.
Dowód Kempego z 1879 roku uchodził za poprawny przez $11$ lat; z jego wraku Heawood uratował twierdzenie o pięciu barwach.
Appel i Haken (1976) dali pierwszy wielki dowód komputerowy w historii matematyki; formalizacja Gonthiera w Coq (2005) zamknęła spory o jego wiarygodność.
Zastrzeżenia: regiony muszą być spójne, styk punktowy się nie liczy, a na torusie potrzeba siedmiu barw.