Izrek o štirih barvah — definicija, dokaz in zgodovina

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).

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.

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.

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.

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.