Izrek o štirih barvah — definicija, dokaz in zgodovina

Izrek o štirih barvah je matematični izrek. Pravi, da lahko na kateri koli ravni površini z območji (ljudje si jih predstavljajo kot zemljevide) območja obarvamo z največ štirimi barvami, tako da si sosednji predeli (tisti, ki imajo skupno mejo v obliki neizolirane črte, ne samo točke) ne delijo iste barve. Ta formulacija je enakovredna trditvi, da je vsak planarni graf 4-barven (ima barvanje vozlišč s štirimi barvami, kjer sta sosednji vozlišči različnih barv).

Poenostavljena razlaga in primeri. Čeprav večina praktičnih zemljevidov ne potrebuje več kot treh barv, obstajajo primeri, kjer je četrta barva nujna. Najenostavnejši primer, ki zahteva štiri barve, je graf K4 (tetraedrični graf) v ravnini: štiri regije so takšne, da je vsaka parno sosednja z ostalimi tremi, zato so potrebne štiri različne barve. V razdelkih kartografije so takšni primeri redki, zato je izrek predvsem matematični rezultat, ne pa navodilo za praktično izdelavo zemljevidov.

O vrsti dokaza. Izrek o štirih barvah je znan tudi kot prvi veliki teorem, katerega končni dokaz je bil pridobljen ob pomembni rabi računalnikov. Glavna strategija dokazovanja, ki se je izkazala za uspešno, združuje dve ideji: (1) pojmi neizogibnih množic konfiguracij — nabor konfiguracij, od katerih se ne more izogniti noben morebitni minimalni protiprimer, in (2) pojmi redukcije (vsaka konfiguracija iz tega nabora se izkaže za reducibilno, torej ne more nastopiti v minimalnem protiprimeru). Ta pristop pogosto uporablja t. i. metodo razprševanja (discharging), ki omogoča dokaz, da je neka množica konfiguracij neizogibna. Ker je veliko konfiguracij in je preverjanje reducibilnosti za vsako teh podrobno in deločno, so se pri končnem preverjanju uporabili računalniški programi — to je primer dokaza z izčrpavanjem.

Zgodovina in ključni mejniki. Problem je prvi predstavil Francis Guthrie leta 1852. V zgodovini je bilo več napačnih dokazov in popravkov: Alfred Kempe je leta 1879 objavil dokaz, ki je bil sprejet več let, a ga je leta 1890 razkril kot napak Percy Heawood; Heawood je v istem letu dokazal izrek o petih barvah, ki zagotavlja, da zadostuje pet barv, in njegovo dokazovanje je preprostejše in klasično.

Prvi računalniško podprti končni dokaz so leta 1976 objavila Kenneth Appel in Wolfgang Haken; v njihovem prvem poročilu so uporabili množico okoli 1 936 konfiguracij in računalniško preverjanje reducibilnosti — to je bil dokaz z izčrpavanjem, deloma preverjen s programskimi testi. Zaradi obsežnega računalniškega dela in nemogočnosti ročne preverbe vseh korakov je bila sprejemljivost tega dokaza sprva predmet razprav v matematični skupnosti. Kasnejša dela so dokaz poenostavila in zmanjšala število primerov; najpomembnejši takšen rezultat je delo Roberta Robertsona, Daniela Sandersa, Paul Seymourja in Robin Thomasa (1997), ki je dokaz preuredilo in zmanjšalo število potrebnih konfiguracij na okoli 633.

Glede zanesljivosti sta bila kasneje izvedena tudi projekta formalne verifikacije: Georges Gonthier je v začetku 21. stoletja formaliziral dokaz v dokaznem asistentskem sistemu Coq, kar je še dodatno povečalo zaupanje v računalniško asistiran dokaz izreka.

Zakaj je dokaz težaven. Glavni izziv je, da obstoja veliko možnih lokalnih struktur (konfiguracij) v plani grafih in da je treba pokazati, da nobena potencialna minimalna nepravilnost ne more obstajati. Metoda razprševanja zahteva skrbno izbiro neizogibne množice in zapletene računske preverbe reducibilnosti. Čeprav je splošna ideja dokaza elokventna, njeno dokončno izvedbo brez računalnika danes še vedno ni znano doseči z razumne dolžine.

Pomen in nadaljnji razvoj. Izrek o štirih barvah je postal simboličen primer sodelovanja matematične teorije in računalniške verifikacije. Poudarja meje, kjer človeška presoja potrebuje podporo obširnih algoritmičnih preverjanj, hkrati pa je spodbudil razvoj metod za formalno preverjanje dokazov in orodij za dokazne asistente. Poleg tega so raziskave, povezane z izrekom, izboljšale razumevanje planarnih grafov, metod razprševanja in konstrukcij reducibilnih konfiguracij, kar ima odmev v teoriji grafov in kombinatoriki.

Zaključek. Izrek o štirih barvah pravi preprosto in očitno trditev o barvanju zemljevidov, a je zgodovina njegovega dokazovanja zapletena in zanimiva: od začetnih vprašanj iz 19. stoletja, preko napačnih dokazov in izboljšav, do prvega velikega računalniško podprtega dokaza v 20. stoletju in poznejših formalnih verifikacij. Čeprav danes obstaja sprejet dokaz, ostaja izrek dragocen primer, kako se matematična intuicija in računalniška potrditev dopolnjujeta.

Tri barve niso dovolj za barvanje tega zemljevida.

Primer zemljevida s štirimi barvami

Natančna formulacija problema

Intuitivno lahko trditev o štirih barvah izrazimo takole: "Če je dana kakršnakoli razdelitev ravnine na sosednja območja, imenovana zemljevid, lahko območja obarvamo z največ štirimi barvami, tako da nobeno od dveh sosednjih območij nima enake barve. Da bi lahko pravilno rešili problem, je treba pojasniti nekatere vidike: Prvič, vse točke, ki pripadajo trem ali več državam, je treba prezreti. Drugič, za bizarne zemljevide z regijami končne površine in neskončnega oboda so lahko potrebne več kot štiri barve.

Za namen teoremov mora biti vsaka "država" preprosto povezana regija ali sosednja regija. V resničnem svetu to ni res: Aljaska kot del Združenih držav, Nahčivan kot del Azerbajdžana in Kaliningrad kot del Rusije niso sosednje države. Ker mora biti ozemlje določene države enake barve, štiri barve morda ne bodo dovolj. Na primer, upoštevajte poenostavljen zemljevid, kot je prikazan na levi strani: Na tem zemljevidu obe regiji, označeni z A, pripadata isti državi in morata biti enake barve. Na tem zemljevidu je torej potrebnih pet barv, saj regiji A skupaj mejita na štiri druge regije, od katerih je vsaka mejna na vse druge. Če bi imela A le tri regije, bi bilo potrebnih šest ali več barv. Na ta način je mogoče izdelati zemljevide, ki potrebujejo poljubno veliko število barv. Podobna konstrukcija velja tudi, če se za vsa vodna telesa uporabi ena barva, kot je običajno na resničnih zemljevidih.

Lažja različica izreka uporablja teorijo grafov. Množico regij zemljevida lahko abstraktneje predstavimo kot neusmerjeni graf, ki ima vrh za vsako regijo in rob za vsak par regij, ki si delijo mejni odsek. Ta graf je ravninski: lahko ga narišemo v ravnini brez križišč tako, da vsak vrh postavimo na poljubno izbrano mesto znotraj regije, ki ji ustreza, robove pa narišemo kot krivulje, ki vodijo brez križišč znotraj vsake regije od mesta vrha do vsake skupne mejne točke regije. Obratno pa je mogoče na ta način iz zemljevida oblikovati kateri koli ravninski graf. V grafoteoretični terminologiji teorem o štirih barvah pravi, da je mogoče vrhove vsakega ravninskega grafa obarvati z največ štirimi barvami, tako da nobena dva sosednja vrhova nimata enake barve, ali na kratko, "vsak ravninski graf je štiribarvni" (Thomas 1998, str. 849; Wilson 2002).

Primer zemljevida Azerbajdžana z nesorodnimi regijami

Tega zemljevida ni mogoče obarvati s štirimi barvami

Zgodovina

Prvi je problem poimenoval Francis Guthrie leta 1852. Takrat je bil študent prava v Angliji. Ugotovil je, da potrebuje vsaj štiri barve za obarvanje zemljevida angleških grofij. Augustus de Morgan je o tem problemu prvič razpravljal v pismu, ki ga je avgusta 1852 napisal Rowanu Hamlitonu. V pismu de Morgan sprašuje, ali so štiri barve res dovolj za obarvanje zemljevida, tako da države, ki so druga ob drugi, dobijo različne barve.

Angleški matematik Arthur Cayley je leta 1878 problem predstavil matematičnemu društvu v Londonu. V enem letu je Alfred Kempe našel nekaj, kar je bilo videti kot dokaz problema. Enajst let pozneje, leta 1890, je Percy Heawood pokazal, da je Alfredov dokaz napačen. Peter Guthrie Tait je leta 1880 predstavil še en poskus dokaza. Trajalo je enajst let, da se je pokazalo, da tudi Taitov dokaz ni deloval. Leta 1891 je Julius Petersen to lahko dokazal. Ko je ponaredil Cayleyjev dokaz, je Kempe pokazal tudi dokaz za problem, ki ga je poimenoval Teorem petih barv. Izrek pravi, da lahko vsak tak zemljevid obarvamo z največ petimi barvami. Obstajata dve omejitvi: Prvič, vsaka država je sosednja, ni eksklav. Druga omejitev je, da morajo imeti države skupno mejo; če se dotikajo le v eni točki, jih lahko pobarvamo z isto barvo. Čeprav je bil Kempejev dokaz napačen, je uporabil nekatere zamisli, ki so pozneje omogočile pravilen dokaz.

V šestdesetih in sedemdesetih letih prejšnjega stoletja je Heinrich Heesch razvil prvo skico računalniškega dokaza. Kenneth Appel in Wolfgang Haken sta leta 1976 to skico izboljšala (Robertson et al. 1996). Uspelo jima je zmanjšati število primerov, ki bi jih bilo treba preizkusiti, na 1936; pozneje je bila izdelana različica, ki se je zanašala na preizkus le 1476 primerov. Vsak primer je bilo treba testirati z računalnikom (Appel in Haken 1977).

Leta 1996 so Neil Robertson, Daniel Sanders, Paul Seymour in Robin Thomas izboljšali metodo in zmanjšali število testiranih primerov na 663. Tudi v tem primeru je bilo treba vsak primer testirati z računalnikom.

Leta 2005 sta Georges Gonthier in Benjamin Werner razvila formalni dokaz. To je bil napredek, saj je prvič omogočil uporabo programske opreme za dokazovanje izrekov. Uporabljena programska oprema se imenuje Coq.

Teorem štirih barv je prvi veliki matematični problem, ki je bil dokazan s pomočjo računalnika. Ker dokaza ne more izvesti človek, ga nekateri matematiki niso priznali za pravilnega. Za preverjanje dokaza se je treba zanesti na pravilno delujočo programsko in strojno opremo, ki dokaz potrdi. Ker je bil dokaz narejen s pomočjo računalnika, tudi ni zelo eleganten.

Poskusi, ki so se izkazali za napačne

Izrek o štirih barvah je bil v svoji dolgi zgodovini znan po številnih lažnih dokazih in izpodbijanjih. New York Times najprej ni želel poročati o Appel-Hakenovem dokazu. Časopis je to storil iz političnih razlogov; bal se je, da se bo dokaz izkazal za lažnega, kot so se izkazali prejšnji (Wilson 2002, str. 209). Nekateri dokazi so trajali dolgo, dokler jih ni bilo mogoče ponarediti: Kempejev in Taitov dokaz je bil ponarejen v več kot desetletju.

Najpreprostejši primeri običajno poskušajo ustvariti eno regijo, ki se dotika vseh drugih. To prisili preostale regije, da se obarvajo z le tremi barvami. Ker je teorem štirih barv resničen, je to vedno mogoče; ker pa je oseba, ki riše zemljevid, osredotočena na eno veliko regijo, ne opazi, da je preostale regije dejansko mogoče pobarvati s tremi barvami.

Ta trik je mogoče posplošiti: Če so barve nekaterih regij na zemljevidu izbrane vnaprej, je nemogoče preostale regije obarvati tako, da so skupaj uporabljene le štiri barve. Nekdo, ki preverja protiprimer, morda ne bo pomislil, da je morda treba spremeniti barvo teh regij. Zaradi tega bo protiprimer videti veljaven, čeprav ni.

Morda je ena od posledic tega splošnega napačnega razumevanja dejstvo, da barvna omejitev ni prehodna: regija mora biti obarvana drugače le od regij, ki se jih neposredno dotika, ne pa tudi od regij, ki se dotikajo regij, ki se jih dotika. Če bi veljala ta omejitev, bi planarni grafi potrebovali poljubno veliko število barv.

Drugi lažni dokazi kršijo predpostavke izreka na nepričakovan način, na primer z uporabo regije, ki ima več nepovezanih delov, ali pa ne dovolijo, da bi se regije iste barve dotikale v točki.


Zemljevid (levo) je bil obarvan s petimi barvami, za obarvanje s samo štirimi barvami (desno) pa je treba spremeniti vsaj štiri od desetih regij.

Barvanje političnih zemljevidov

V resničnem življenju ima veliko držav eksklave ali kolonije. Ker pripadajo državi, jih je treba obarvati z enako barvo kot matično državo. To pomeni, da je za barvanje takega zemljevida običajno potrebnih več kot štiri barve. Ko matematiki govorijo o grafu, povezanem s problemom, pravijo, da ni ravninski. Čeprav je enostavno preveriti, ali je graf planaren, je iskanje najmanjšega števila barv, potrebnih za njegovo obarvanje, zelo težavno. Gre za NP-poln problem, ki je eden najtežjih obstoječih problemov. Najmanjše število barv, potrebnih za obarvanje grafa, je znano kot njegovo kromatično število. Številne težave, ki se pojavijo, ko poskušamo rešiti teorem štirih barv, so povezane z diskretno matematiko. Zato se pogosto uporabljajo metode iz algebrske topologije.

Razširitev na zemljevide, ki niso ploščati

Teorem štirih barv zahteva, da je "zemljevid" na ravni površini, ki ji matematiki pravijo ravnina. Leta 1890 je Percy John Heawood ustvaril domnevo, ki jo danes imenujemo Heawoodova domneva: V njej se zastavlja enako vprašanje kot v teoremih štirih barv, vendar za kateri koli topološki objekt. Na primer, torus lahko obarvamo z največ sedmimi barvami. Heawoodova domneva podaja formulo, ki deluje za vse take objekte, razen za Kleinovo steklenico.

Vprašanja in odgovori

V: Kaj je teorem štirih barv?

O: Teorem štirih barv je matematični teorem, ki pravi, da lahko na poljubni ravni površini z območji območja obarvamo z največ štirimi barvami. Sosednje regije ne smejo imeti iste barve.

V: Kako je bil izveden prvi dokaz teze o štirih barvah?

O: Prvi dokaz trditve o štirih barvah je bil dokaz z izčrpavanjem s 1 936 primeri. To pomeni, da je bil dokazan tako, da smo ga razdelili na primere in dokazali vsakega posebej.

V: Ali ta problem zanima kartografe?

O: Ne, izdelovalcev zemljevidov ta problem ne zanima preveč, saj so zemljevidi, ki uporabljajo samo štiri barve, redki in običajno zahtevajo samo tri barve. V knjigah o kartografiji in zgodovini izdelave zemljevidov lastnost štirih barv ni omenjena.

V: Kaj je teorem petih barv?

O: Izrek o petih barvah pravi, da za barvanje zemljevida zadostuje pet barv, in ima kratek, osnovni dokaz, ki je bil dokazan konec 19. stoletja.

V: Kako težko je bilo dokazati, da so za barvanje zemljevidov potrebne le štiri barve?

O: Dokazati, da so za barvanje zemljevidov potrebne le štiri barve, se je izkazalo za veliko težje, kot smo pričakovali, saj se je od prve trditve leta 1852 pojavilo veliko lažnih dokazov in lažnih protiprimerov.

V: Ali obstaja primer zemljevida, na katerem bi bilo za pravilno obarvanje vseh regij potrebnih 5 ali več barv?

O: Da, tak primer je, ko je ena regija obdana z lihim številom drugih regij, ki se dotikajo druga druge v krogu - v tem primeru je za pravilno obarvanje vseh regij morda potrebnih 5 ali več barv.