Kolorowo

https://xpil.eu/zoxsK 📋

Książka, którą ostatnio czytam z zapartym tchem (o której wspominam tutaj) zawiera, oprócz w miarę "tradycyjnych" zagadek matematycznych (typu: Jaś miał pięć jabłek, oddał połowę bratu; ile ma teraz? Oczywiście, cztery i pół...) również zagadnienia z zakresu geometrii, trygonometrii, topologii i różnych innych obszarów matematyki.

Dziś opowiem o zagadce topologicznej, która męczyła matematyków przez ponad 120 lat. Zagadka, której intuicyjne rozwiązanie znano na wiele lat przed opublikowaniem porządnego, formalnego dowodu matematycznego. Który to dowód, nawiasem mówiąc, był jednym z najbardziej kontrowersyjnych dowodów matematycznych zeszłego stulecia, ponieważ po raz pierwszy wykorzystano do tego celu komputery na tak wielką skalę. Nie po to, żeby przeprowadzić symulację, ale po to, żeby sprawdzić około półtora tysiąca przypadków szczególnych (czyli takich, które "nie pasowały" do przedstawionego dowodu ogólnego, ale które jak najbardziej spełniały twierdzenie).

Zagadka brzmi: Jaka jest najmniejsza liczba kolorów wymaganych do pokolorowania dowolnej mapy w taki sposób, żeby żadne dwa sąsiednie państwa nie miały tego samego koloru?
Przez "mapę" rozumiemy tutaj tradycyjną, dwuwymiarową mapę polityczną, z dowolnym układem dowolnie dużej liczby państw.
Przez "sąsiednie" rozumiemy tutaj dwa państwa o wspólnym odcinku granicy.

Zagadnienie to, postawione w połowie dziewiętnastego wieku, jest na pierwszy rzut oka całkiem łatwe (podobnie jak wielkie twierdzenie Fermata). Jednak przez ponad sto dwadzieścia lat okazuje się ono opierać matematycznym narzędziom dowodowym. Kilka pokoleń matematyków z dziewięćdziesięciu sześciu krajów świata próbowało bezskutecznie udowodnić, że liczba ta wynosi cztery. Udało się udowodnić twierdzenie dla sześciu kolorów, udało się potem dla pięciu. Nie udało się jednak znaleźć takiej mapy, której nie można by pokolorować zaledwie czterema kolorami. A więc doświadczenie pokazywało, że liczbą tą jest cztery, jednak udowodnić tę czwórkę było diabelnie trudno.

Dopiero w 1976. roku dwóch matematyków zaprezentowało pełen dowód - niestety, opierał się on w większości na analizie komputerowej, ponieważ trzeba było przeanalizować 1476 konfiguracji, i dla każdej z nich przeprowadzić kilka tysięcy kolorowań. A więc - łącznie - trzeba było przeprowadzić kilka milionów kolorowań. Coś nieosiągalnego człowiekowi.

Oczywiście w "czystym" świecie matematyków zawrzało. W końcu komputerowo przeprowadzony dowód jakiegoś twierdzenia jest tylko tak dobry jak algorytm do tego celu stworzony, i niewiele ma on wspólnego ze stricte heurystycznym procesem dowodzenia twierdzeń, tak bliskim sercom "tradycyjnych" matematyków. Zawrzały dyskusje nad uznawalnością tego typu dowodów - jednak prawdziwy wniosek jest tylko jeden: zamiast martwić się o to, że komputery potrafią przeliczyć więcej kombinacji niż nasz galaretowaty mózg, radujmy się, że wreszcie mamy narzędzia do rozwiązywania problemów, które w innym przypadku pozostałyby nierozwiązane nie dlatego, że rozwiązań nie ma, ale dlatego, że są one kompletnie poza zasięgiem poznawczym człowieka.

Na zakończenie dodam jeszcze, że opisywana przeze mnie wcześniej hipoteza Keplera (postawiona w roku 1611) również została udowodniona dopiero w 1998. roku (a kompletność tego dowodu udało się potwierdzić dopiero w roku 2005.) - i to przy pomocy komputera, który by potrzebny do rozwiązania kilkuset tysięcy problemów optymalizacji, każdy ze stu pięćdziesięcioma zmiennymi. A zagadnienie jest (pozornie) jeszcze bardziej trywialne niż kolorowanie map.

Wot, tiechnika...

https://xpil.eu/zoxsK 📋