Keturių spalvų teorema yra matematikos teorema. Ji teigia, kad bet kuriame plokščiame paviršiuje, kuriame yra regionų (žmonės juos laiko žemėlapiais), regionus galima nuspalvinti ne daugiau kaip keturiomis spalvomis. Du regionai, turintys bendrą ribą, negali būti nuspalvinti ta pačia spalva. Jie vadinami gretimais (esančiais vienas šalia kito), jei turi bendrą sienos atkarpą, o ne tik tašką.

Tai buvo pirmoji teorema, kurią įrodė kompiuteris, atlikdamas įrodymą išsekimo būdu. Įrodinėjant išbaigtumo būdu išvada nustatoma suskirsčius ją į atvejus ir kiekvieną iš jų įrodinėjant atskirai. Atvejų gali būti daug. Pavyzdžiui, pirmasis keturių spalvų teoremos įrodymas buvo įrodymas išsekimo būdu su 1 936 atvejais. Šis įrodymas buvo prieštaringai vertinamas, nes dauguma atvejų buvo tikrinami kompiuterine programa, o ne ranka. Trumpiausias šiandien žinomas keturių spalvų teoremos įrodymas vis dar turi daugiau kaip 600 atvejų.

Nors ši problema pirmą kartą buvo pateikta kaip šalių politinių žemėlapių spalvinimo problema, žemėlapių kūrėjai ja nelabai domisi. Kaip rašoma matematikos istoriko Kennetho May'aus straipsnyje (Wilson 2002, 2), "žemėlapiai, kuriuose naudojamos tik keturios spalvos, pasitaiko retai, o tuose, kuriuose jos naudojamos, paprastai reikia tik trijų. Knygose apie kartografiją ir žemėlapių kūrimo istoriją keturių spalvų savybė neminima".

Daugelį paprastesnių žemėlapių galima nuspalvinti trimis spalvomis. Ketvirtosios spalvos reikia kai kuriems žemėlapiams, pavyzdžiui, tokiems, kuriuose vieną regioną supa nelyginis skaičius kitų, kurie liečiasi vienas su kitu cikliškai. Vienas iš tokių pavyzdžių pateiktas paveikslėlyje. Penkių spalvų teorema teigia, kad žemėlapiui nuspalvinti pakanka penkių spalvų. Ji turi trumpą, elementarų įrodymą ir buvo įrodyta XIX a. pabaigoje. (Heawood 1890) Įrodyti, kad užtenka keturių spalvų, pasirodė daug sunkiau. Nuo 1852 m., kai pirmą kartą buvo iškelta keturių spalvų teorema, atsirado daug klaidingų įrodymų ir klaidingų priešpriešų.

Matematinis suvokimas ir ekvivalenti formulė

Matematiškai užduotis dažnai rekonstruojama naudojant plokštuminį grafą: kiekvienam žemėlapio regionui priskiriamas viršūnė, o dviem regionams turint bendrą sieną atitinka kraštas tarp atitinkamų viršūnių. Tokiu atveju žemėlapio spalvinimo problema tampa viršūnėms skirtos spalvinimo problema plokštiniame grafe. Todėl keturių spalvų teorema teigia, kad kiekvieną plokštinį grafą galima suvereikinti keturiomis spalvomis, t. y. plokštiniai grafai turi chromatinį skaičių ≤ 4.

Įrodymo idėjos (sutrumpinta apžvalga)

  • Minimalus prieštaravimas: tradicinis būdas – manyti, kad egzistuoja mažiausias prieštaraujantis žemėlapis (arba grafas) ir rodyti, jog toks negali egzistuoti.
  • Kempe grandinės: Alfredas Kempe 1879 m. siūlė metodą, vėliau pavadintą Kempe grandinėmis, bandant permesti spalvas grandinėse, kad atsirastų laisva spalva. Jo argumentas ilgą laiką buvo laikomas įrodymu, tačiau 1890 m. P. J. Heawood parodė, kad jame slypi klaida.
  • Atvejų skirstymas, nulemta kompiuterio: Appel ir Haken (1976 m.) parodė, kad galima suformuluoti galimų konfigūracijų rinkinį (vadinamą „neišvengiamų“ konfigūracijų rinkiniu) ir parodyti, jog kiekviena tokia konfigūracija yra „sumažinama“ (redukcinė), t. y. negali būti minimaliame prieštaravime. Išskyrus daugybę atvejų, dalis tikrinimo atlikta kompiuteriu. Pirmasis jų įrodymas naudojo apie 1 936 atvejus; vėlesni pataisymai pakeitė skaičių, tačiau esmė išliko – daug kompiuterinės patikros.
  • Sutrumpintas kompiuterinis įrodymas: vėliau (1997 m.) Robertson, Sanders, Seymour ir Thomas pateikė trumpesnį įrodymą, sumažinantį reikalingų konfigūracijų skaičių (daugiau nei 600, dažniausiai nurodomas 633 konfigūracijų rinkinys). Šis darbas padarė argumentą struktūriškesnį ir labiau kontroliuojamą.
  • Formalus patvirtinimas: 2005 m. Georges Gonthier ir bendraautoriai pateikė formalizuotą keturių spalvų teoremos įrodymą Coq pagalbinėje sistemoje, kas dar labiau padidino pasitikėjimą kompiuterinių verifikacijų patikimumu.

Istorija – trumpas laiko juostos aprašymas

  • 1852 m. Francis Guthrie pirmasis uždavė klausimą apie žemėlapių spalvinimą.
  • 1879 m. Alfredas Kempe paskelbė tariamą įrodymą; jis dešimtmečius buvo laikomas teisingu.
  • 1890 m. P. J. Heawood atrado klaidą Kempe įrodyme ir, tuo pačiu, įrodė penkių spalvų teoremą, kuri turi elementarų įrodymą.
  • XX a. – daug bandymų, įvairūs pasiūlyti įrodymai, klaidų taisymai ir gilios struktūrinės analizės plokštiniais grafais.
  • 1976–1977 m. Kennethas Appel ir Wolfgangas Hakenas paskelbė pirmą pagrįstą kompiuterinį įrodymą (daugiau nei 1 900 atvejų), sukeldami didelę matematikų bendruomenės diskusiją dėl kompiuterinių įrodymų pobūdžio.
  • 1997 m. Robertson, Sanders, Seymour ir Thomas pagerino ir sutrumpino įrodymą (apie 633 atvejai).
  • 2005 m. Gonthier formalizavo įrodymą sistemoje Coq, kas dar labiau sustiprino teoremos patikimumą.

Reikšmė, taikymas ir algoritmo aspektai

Keturių spalvų teorema turi didelę teorinę reikšmę grafų teorijoje ir kombinatorikoje. Jos įrodymas paskatino naujus metodus, pabrėžiančius kompiuterio vaidmenį įrodant sudėtingus kombinatorinius faktus. Praktiniu požiūriu kartografijoje ši teorema retai naudojama tiesiogiai, nes realūs žemėlapiai paprastai reikalauja mažiau spalvų. Tačiau problema turi įtakos tokioms sritims kaip planarinio grafo spalvinimas, kompiuterinis vaizdų segmentavimas ir kai kurios optimizavimo užduotys.

Kalbant apie algoritmus, keturių spalvų nuspalvinimas plokštiniam grafui yra įgyvendinamas efektyviomis programomis; yra ir teorinių rezultatai, leidžiantys paruošti polinominio laiko algoritmus bei praktiškai greitus heuristinius sprendimus. Robertson ir kt. įrodymas netgi leidžia išvesti algoritmines procedūras, kurios naudoja tuos pačius struktūrinius dalykus, kurie atsirado įrodant teoremą.

Santrauka

Keturių spalvų teorema teigia, kad kiekvieną žemėlapį (plokštinį grafą) galima nudažyti ne daugiau kaip keturiomis spalvomis taip, kad gretimi regionai turėtų skirtingas spalvas. Nors jos paminėjimas kilo iš praktinių žemėlapių spalvinimo užduoties, matematinis įrodymas reikalavo gilesnės grafų teorijos analizės ir kompiuterinių metodų. Dabar teorema yra priimta kaip įrodyta — jos istorija taip pat tapo svarbiu pavyzdžiu, kaip kompiuterinė kontrolė ir formali verifikacija gali papildyti tradicinius matematikos metodus.