Skip to content

Cztery kolory albo nic!

Grudzień 8, 2010

Najwyżej cztery kolory…

Oto mapa Ameryki Południowej. Iloma różnymi kredkami można pokolorować planszę, aby wszystkie graniczące ze sobą państwa były różnego koloru?

AdSblanc_enfin_plutot_vert

I bardziej ogólnie, jeżeli mamy mapę, na której wszystkie kraje są połączone (bez wysp, bez kieszeni), ile kolorów potrzebujemy by ją pokolorować?

Odpowiedź nie zaskoczy nikogo, zwłaszcza że można ją znaleźć w nazwie akapitu. Wystarczą cztery kolory. Jakkolwiek skomplikowana nie byłaby mapa. Tę właściwość nazwano „Twierdzeniem o czterech barwach”.

Metodą prób i błędów, zawsze znajdziemy rozwiązanie które pasuje. Jeśli przyjmiemy, że ocean jest krajem, zaznaczymy go na zielono.

Można nawet powiedzieć więcej: w niektórych przypadkach, takich jak mapa Ameryki Południowej, potrzebujemy aż 4 kolorów. Spójrz tylko na Brazylię, Argentynę, Boliwię i Paragwaj. Ponieważ każdy z krajów posiada granicę z trzema pozostałymi, do pokolorowania mapy użyjemy co najmniej czterech kolorów.

źródło: eljjdx.canalblog.com

Odkrycie tej właściwości datuje się na rok 1850. Botanik i matematyk Francis Guthrie, niedawny absolwent uniwersytetu, zapytał swojego byłego profesora Augustusa De Morgan (wiecie, tego od praw De Morgana), jak można by udowodnić jego odkrycie analizując mapę hrabstw Anglii. Morgan nie wie jak to zrobić i prosi o pomoc Hamiltona, który uprzejmie odpowiada, że podejmie się wyzwania.

Co najwyżej sześć kolorów

Problem czterech kolorów jest właściwie zagadnieniem z teorii grafów. Możemy odwzorować mapę przy pomocy grafu, umieszczając wierzchołek w każdym z państw i łącząc krawędziami graniczące ze sobą państwa. Rezultatem jest graf planarny. A więc pytanie brzmi: czy to każdego grafu planarnego możemy zastosować cztery kolory?

Graf czterokolorowy, to taki, w którym każdy wierzchołek ma jeden z czterech kolorów i dwa sąsiednie wierzchołki nigdy nie są tego samego koloru.

Pokazanie, że każdy graf planarny może być czterokolorowy nie jest proste, ale pokazanie sześciokolorowości grafu planarnego łatwo udowodnić przy pomocy indukcji. Jeżeli graf ma mniej niż 6 wierzchołków, nie ma problemu. Jeżeli ma więcej niż 6 wierzchołków, z formuły Eulera wynika, że w takim grafie planarnym może istnieć wierzchołek co najwyżej stopnia piątego (z maksymalnie 5 sąsiadami). Przy pięciu sąsiadach zawsze znajdzie się kolor, którym możemy pokolorować ten wierzchołek.

Nie więcej niż pięć kolorów

25 lat później, problem Guthriego przemierzył świat, a nadal nie znaleziono dla niego dowodu. Aż do tego dnia, w czerwcu 1879 roku, kiedy Alfred Kempe  ogłasza światu, że udowodnił hipotezę o czterech kolorach, która od tego dnia staje się twierdzeniem. Kempe zbiera laury za swoje odkrycie, zostaje nawet skarbnikiem Angielskiej Akademii Nauk (Royal Society). Ale szczęście nie trwa długo, bo już w roku 1890 Percy Hearwood odkrywa błąd w dowodzie Kempego, błąd przez który problem czterech kolorów zostaje znów sprowadzony do statusu hipotezy.

Hearwood wznawia pracę Kempego, ale nie jest w stanie udowodnić twierdzenia o czterech kolorach a jedynie o pięciu. A to już krok do przodu. Dowód twierdzenia Hearwooda jest dłuższy niż twierdzenie o sześciu kolorach, ale jest utrzymane w tym samym duchu, oparte na formule Eulera.

Chodź fałszywy, dowód Kempego jest wciąż interesujący i rozwija ideę twierdzenia o sześciu kolorach.Wybieramy wierzchołek stopnia piątego. W dobrych przypadkach, można Kempe udowodnił rekurencję, w złych…  po prostu ją spreparował.

W roku 1896, Charles-Etienne Jean  Gustave Nicolas le Vieux Baron de la la Vallée Poussin (matematyk znany z twierdzenia w teorii liczb) również odkrył błąd w rozważaniach Kempego. Niestety spóźnił się o sześć lat. Hearwood, natomiast, spędził resztę życia na próżno próbując udowodnić hipotezę o czterech kolorach.

Na pracy, która była kontynuowana w 24 krajach, później 27, 31 i 96 krajach do roku 1976.

Więcej niż cztery kolory

Nowe stulecie, nowe narzędzia. W roku 1976, dwóch amerykanów Appel i Haken ogłosiło, że rozwiązali problem. Po raz drugi, tym razem ostatecznie hipoteza staje się twierdzeniem. Ale jest i haczyk: po raz pierwszy w dowodzie matematycznym, to nie człowiek zawodzi, a komputer. Demonstracja oczekiwana od wieku jest zupełnie rozczarowujące.

Z tego powodu Appel i Haken jeszcze raz podjęli pomysł Kempego, ale z jednym wyjątkiem. Zamiast redukować jednego wierzchołka, redukowali ich kilka, zwanych „konfiguracjami”. Konfiguracje to mniejsze grafy, które znajdziemy  wystarczająco dużych grafach planarnych i istnieje skończona liczba konfiguracji: 1476. Zidentyfikowanie wszystkich takich układów, jeżeli potraficie sobie to wyobrazić, jest niesamowicie żmudne. A mimo to znaleźli je wszystkie ręcznie!

Przy pomocy indukcji, możemy pokolorować graf bez żadnej konfiguracji. Wystarczy jedynie pokazać, że kolorowanie można rozszerzyć na konfigurację. Aby to zrobić, musimy wziąć wszystkie kombinacje kolorów dla małego grafu i pokazać, że rozszerzenie ich jest możliwe. Dla każdej konfiguracji istnieje kilka tysięcy kolorowanek do rozważenia, jedna po drugiej. Aby poradzić sobie z ogromem pracy, Appel i Haken zaprogramowali informatyczne narzędzie, które wykonywało pracę za nich.

Później, innej grupie matematyków udało się zmniejszyć liczbę konfiguracji do 633, ale i przy tej liczbie należało przeprowadzić ogromną liczbę obliczeń.

W skrócie, komputer miał do rozwiązania problem, który z początku wydawał się bardzo subtelny. Jeżeli mielibyśmy zmniejszyć liczbę z pięciu do czterech kolorów, grafy planarne musiałyby mieć właściwość dotąd nam nieznaną. A kiedy problem jest subtelny, zazwyczaj wymaga powstania  nowych koncepcji, podobnie jak na przykład małe twierdzenie Fermata. Ale dowód twierdzenia Fermata okazał się banalny, w porównaniu ze problemem czterech kolorów.

W końcu dylemat czterech kolorów okazał się bardzo trudny, przynajmniej dopóki do jego rozwiązania próbowano użyć metod użytych w dowodzie twierdzenia o pięciu kolorach.

Istniał jeszcze jeden problem: Czy użycie komputera do demonstracji jest wystarczającym dowodem? Problem poprawności dowodu sprowadza się tutaj do poprawności programu, który go stworzył. Na rok 1976, inne twierdzenia zostały udowodnione przy pomocy narzędzi komputerowych, włączając w to hipotezę Keplera o układaniu pomarańczy.

W roku 2004, Georges Gonthier trafia na czołówki czasopism naukowych ogłaszając, że raz na zawsze twierdzenie o czterech kolorach staje się twierdzeniem. Aby tego dokonać, użył narzędzia Coq (Kogut), którego poprawność została potwierdzona. To jedyne narzędzie, które pozwala sprawdzić poprawność kroku indukcyjnego napisanego w jego własnym języku. Kogut nawet sam sprawdził, czy w jego kodzie nie ma błędów!

Dawny spór „za i przeciw komputerowym dowodów” nadal wzbudza wiele emocji. Ale mimo to, na dzisiejszym etapie rozwoju, komputerowy asystent, daje nam co najmniej taką dokładność, jak uważne czytanie stu stronicowego dowodu.

W skrócie, twierdzenie o czterech kolorach nadal ma swoje tajemnice. Kilku stronicowy dowód na pewno kryje się gdzieś w cyfrach liczby pi…

Advertisements
5 komentarzy leave one →
  1. pawiu permalink
    Luty 24, 2011 12:13 pm

    Witaj! Nie jestem kompetenty w matematyce praktycznej ani w jej problemach teoretycznych. Czy moglabys mi prosze wyjasnic, dlaczego przeprowadzanie dowodu przez komupter moze byc niedokladne? Wychodze z zalozenia ze przeprowazdajacy dowod ludzie rowniez moga byc w takim razie zawodni. A czy to nie oni programujac komputer okreslaja warunki prawdziwosci dowodu? Zatem jedno z dwojga: albo zaden dowod nigdy nie bedzie do konca uznany za prawdziwy albo tez taki komputerowy jest z miejsca za prawdziwy uznany. Ale pewnie strasznie pokrecilem.

  2. Luty 24, 2011 5:31 pm

    Nie wiem, czy przeprowadzałeś kiedyś dowód indukcyjny. Powiedzmy, że chcemy udowodnić, że pewna równość jest prawdziwa dla wszystkich liczb naturalnych.

    Dowód indukcyjny składa się z dwóch kroków:
    1. Udowodnienie, że istnieje taki przypadek, dla którego twierdzenie jest prawdziwe.
    Np. Równość jest prawdziwa dla n=1.
    2. Udowodnienie, że twierdzenie dla wszystkich kolejnych przypadków jest prawdziwe.
    Np. Zakładamy że równość jest prawdziwa dla pewnego n i udowadniamy, że jest prawdziwa dla n+1.

    W ten sposób udowodniliśmy, że równość jest zawsze prawdziwa. Bo skoro jest prawdziwa dla 1, to i dla 2, a także dla 3 i tak dalej.

    Wydaje mi się, że Tego typu programy zamiast znaleźć sposób, by udowodnić krok indukcyjny sprawdzają tylko, czy twierdzenie jest prawdziwe dla n=2,3,4, itd. Podobno takie programy mogą proponować sposób wyprowadzenie kroku indukcyjnego, ale w tym przypadku go nie znaleziono.

    Niby jest to jakiś sposób, ale nie jest tak ‚elegancki’ jak prawdziwa indukcja.

    • suchar permalink
      Czerwiec 26, 2011 5:23 pm

      – Jak chińscy matematycy dowodzą przez indukcję?
      – Każdy liczy dla innego n.

    • Czerwiec 26, 2011 8:30 pm

      Istnieje wiele bardzo subtelnych technik automatycznego dowodzenia twierdzeń (przez maszynę), ale z pewnością indukcja nie jest dowodzona w taki sposób jak piszesz. To nie byłby po prostu dowód matematyczny, a twierdzenie o czterech barwach zostało w pełni udowodnione. 🙂
      Sporo problemów, zwłaszcza w teorii grafów, da się przekształcić do problemu spełnialności wyrażenia boolowskiego (SAT) i wtedy przy skończonej liczbie zmiennych zerojedynkowych komputer jest w stanie rozwiązać ten problem (równanie) z pełną precyzją.
      Pozdrawiam

  3. supersekret permalink
    Czerwiec 26, 2011 8:20 pm

    Ciekawa sprawa, w zasadzie nie przepadam za matematyką, jednak uwielbiam takie ciekawostki.

Skomentuj

Wprowadź swoje dane lub kliknij jedną z tych ikon, aby się zalogować:

Logo WordPress.com

Komentujesz korzystając z konta WordPress.com. Log Out / Zmień )

Zdjęcie z Twittera

Komentujesz korzystając z konta Twitter. Log Out / Zmień )

Facebook photo

Komentujesz korzystając z konta Facebook. Log Out / Zmień )

Google+ photo

Komentujesz korzystając z konta Google+. Log Out / Zmień )

Connecting to %s

%d blogerów lubi to: