Теоремата за четирите цвята е теорема в математиката. Тя гласи, че във всяка равнинна повърхнина с области в нея (хората мислят за тях като за карти) областите могат да бъдат оцветени с не повече от четири цвята. Две области, които имат обща граница, не трябва да получават един и същ цвят. Те се наричат съседни (един до друг), ако имат общ участък от границата, а не само точка.

Това е първата теорема, доказана от компютър чрез доказателство чрез изчерпване. При доказателството чрез изчерпване заключението се установява, като се разделя на случаи и всеки от тях се доказва поотделно. Възможно е да има много случаи. Например първото доказателство на теоремата за четирите цвята е доказателство чрез изчерпване с 1936 случая. Това доказателство беше спорно, защото повечето от случаите бяха проверени с компютърна програма, а не на ръка. Най-краткото известно днес доказателство на теоремата за четирите цвята все още има над 600 случая.

Въпреки че проблемът е представен за първи път като проблем за оцветяване на политически карти на държави, картографите не се интересуват много от него. Според статия на историка по математика Кенет Мей (Wilson 2002, 2): "Картите, използващи само четири цвята, са рядкост, а тези, които ги използват, обикновено изискват само три. В книгите по картография и история на картографията не се споменава свойството на четирите цвята".

Много по-прости карти могат да бъдат оцветени с три цвята. Четвъртият цвят е необходим за някои карти, като например тази, в която един регион е заобиколен от нечетен брой други, които се допират един до друг в цикъл. Един такъв пример е даден на изображението. Теоремата за петте цвята гласи, че пет цвята са достатъчни за оцветяване на карта. Тя има кратко, елементарно доказателство и е доказана в края на XIX век. (Heawood 1890) Доказването на това, че са необходими само четири цвята, се оказва много по-трудно. След първото изказване на теоремата за четирите цвята през 1852 г. са се появили много фалшиви доказателства и фалшиви контрапримери.




 

Формулировка и еквивалентни варианти

Класическа формулировка: Всяка карта на плоскостта може да се оцвети с не повече от четири цвята така, че съседни области (които споделят част от границата си, а не само точка) да имат различни цветове.

Графова формулировка: Теоремата е еквивалентна на твърдението, че всеки планарен граф може да бъде оцветен с най-много четири цвята (т.е. хроматичното число на всеки планарен граф е ≤ 4). Това се вижда чрез преминаване към дуален граф, в който върховете съответстват на области на картата и две върхове са свързани с ребро точно когато съответните области са съседни.

Кратка история

  • 1852 г. — проблемът е формулиран от франсис Гутри (Francis Guthrie) при оцветяване на картата на графство; въпросът става популярен сред математиците.
  • 1879 г. — Алфред Кемп (Alfred Kempe) публикува доказателство, което дълго време е приемано за вярно.
  • 1890 г. — Пърси Хийууд (Percy Heawood) открива грешка в доказателството на Кемп и същевременно доказва теоремата за петте цвята, която има просто елементарно доказателство.
  • 1976 г. — Крайният етап: Kenneth Appel и Wolfgang Haken предлагат първото публикувано доказателство, което използва компютърна проверка на голям брой случаи (първоначално около 1936 конфигурации). Този подход довежда до дебат за ролята на компютърните доказателства в математиката.
  • 1996–1997 г. — Робъртсън, Сандерс, Сеймър и Томас (Robertson, Sanders, Seymour & Thomas) предлагат опростено и подобрено доказателство, като намаляват и изчистят част от компютърно проверимите случаи.
  • 2005 г. — Georges Gonthier формализира доказателството в системата за доказателства Coq, което дава още по-висока степен на доверие в резултата.

Идея на доказателството (основни понятия)

Основният подход в съвременните доказателства използва две взаимосвързани идеи:

  • Неизбежни множества — чрез комбинаторни аргументи и метода на discharging се показва, че всеки планарен граф съдържа поне една конфигурация от малък вид от ограничен списък (т.е. някаква конфигурация е неизбежна).
  • Редуциращи (невалидни) конфигурации — за всяка конфигурация от този списък се доказва, че ако тя присъства, то картата/графът може да се оцвети (или присъствието ѝ се свежда до по-малък случай). Тези конфигурации се наричат редуциращи, защото тяхното присъствие "редуцира" задачата до по-просто оцветяване.

Комбинирайки, ако наборът от редуциращи конфигурации е неизбежен, неизбежното съдържание гарантира, че винаги има нещо, което може да се редуцира — оттук следва, че винаги съществува 4-оцветяване. Проверката на много отделни конфигурации е именно частта, която вначало се направи (и е) с помощта на компютър.

В доказателството на Кемп се използваше идеята за т.нар. Kempe chains (вериги на Кемп), която макар и подходът да се оказа не напълно коректен за неговото твърдение, остана важен инструмент и се използва в по-късни доказателства и аргументи.

Защо компютърът е бил нужен и какво промени това

Проблемът се оказва труден, защото стандартните ръчни техники довеждат до много отделни конфигурации, които трябва да се проверят. Appel и Haken успяха да покажат, че всеки планарен граф съдържа някоя от голяма, но крайна колекция от конфигурации; проверката дали всяка от тези конфигурации е редуцираща беше извършена с компютър. Това доведе до оживен дебат за приемливостта на компютърните доказателства. Последвалите опростявания и формализации (например Gonthier) значително повишиха доверието в крайния резултат.

Значение и приложения

Въпреки че самата теорема има малко практическо приложение за ежедневната картография (както беше споменато по-горе — много карти могат да се оцветят с три или по-малко цвята), тя има голямо значение в теорията на графите и комбинаториката. Теоремата стимулира развитие на методи като discharging и въпроси за компютърно подпомаганите доказателства, формира поле за изследване на алгоритми за оцветяване на планарни графи и насочи вниманието към формалната проверка на компютърни доказателства.

Допълнителни бележки

  • Важно е да се помни, че понятията "съседни области" в класическата формулировка изключват допир само в един общ връх; изисква се споделяне на сегмент от границата.
  • Теоремата е пример за резултат, който свързва геометрични представяния (карти) и чисто графови свойства (цветове на върховете на дуалния граф).