Il teorema dei Quattro Colori

Immaginiamo di avere una mappa piana costituita da un numero finito di regioni. Quanti colori sono al massimo necessari per colorarla in modo che due regioni adiacenti (cioè, con un confine in comune) non abbiano lo stesso colore?

Non è difficile costruire una mappa che necessita di quattro colori: si pensi ad una mappa costituita da un cerchio centrale e una corona circolare divisa in tre parti uguali intorno ad esso, come nella figura sotto: 

Una mappa che necessita di quattro colori (a sinistra) e il corrispondente grafo duale (a destra)

Sorge dunque naturale il seguente

Problema dei quattro colori. E' sempre possibile colorare una mappa piana con quattro colori, in modo che due regioni adiacenti abbiano colore differente? Oppure esiste una mappa che necessita di almeno $5$ colori? Equivalentemente, è vero che il numero cromatico del grafo duale di una mappa piana è sempre minore o uguale a $4$?

Si potrebbe pensare che l'origine del problema risalga allo studio della cartografia, ma in realtà le carte geografiche che necessitano di quattro colori sono piuttosto rare (tre colori bastano quasi sempre), e non si è trovata traccia di esso in nessun libro antico sull'argomento. L'origine del Problema dei Quattro Colori sembra in realtà risalire a F. Guthrie, uno studente ad Edimburgo che lo enunciò nel 1852. Guthrie ne parlò al suo insegnante A. De Morgan, il quale ne scrisse a sua volta come segue:

"A student of mine [Guthrie] asked me to day to give him a reason for a fact which I did not know was a fact—and do not yet. He says that if a figure be any how divided and the compartments differently colored so that figures with any portion of common boundary line are differently colored—four colors may be wanted but not more—the following is his case in which four colors are wanted. Query cannot a necessity for five or more be invented…"

Nel 1879, A. Kempe pubblicò una dimostrazione del Teorema dei Quattro Colori [K1879]. L'argomento di Kempe venne ritenuto corretto fino al 1890, quando P. J. Heawood scoprì al suo interno un errore fatale. I tentativi di Heawood di riparare la dimostrazione di Kempe non ebbero successo, tuttavia egli riuscì ad adattarne le tecniche per far vedere che cinque colori sono sempre sufficienti [H1890].

Dopodiché, molti matematici famosi si cimentarono nella dimostrazione del Teorema dei Quattro Colori, ma tutti i loro tentativi furono votati al fallimento. Nella sua biografia di D. Hilbert, C. Reid narra di H. Minkowski che (in un raro moto di arroganza) sostenne durante il suo corso di topologia a Goettingen che per un matematico di prim'ordine come lui ci sarebbe voluto ben poco per produrre una dimostrazione, salvo ritrattare poche settimane dopo spiegando che il suo argomento era fallace e che "il Cielo aveva punito la sua boria". Analogamente, nella sua autobiografia "Ex-prodigy", il pioniere della cibernetica N. Wiener descrive il suo sgomento nel vedere la dimostrazione da lui fornita "sbriciolarsi davanti ai suoi occhi" [Gard3].

La cosa era resa ancora più frustrante dal fatto che, paradossalmente, si conosceva la risposta per mappe disegnate per superfici in apparenza più complicate del piano, come il toro (dove sette colori sono necessari e sufficienti per colorare ogni mappa), la bottiglia di Klein, il nastro di Moebius o il piano proiettivo (dove sei colori sono necessari e sufficienti).

La dimostrazione del Teorema dei Quattro Colori arrivò nel 1976, ad opera di K. Appell e W. Haken [AH77]. Oltre che per il risultato in sé, la dimostrazione di Appell e Haken è storicamente importante in quanto si tratta del primo enunciato di rilievo dimostrato con l'ausilio del computer. La strategia della prova, infatti, consiste dapprima in un lungo e difficile procedimento di riduzione del problema originario ad un problema finito, che coinvolge $1936$ mappe. Tali mappe vengono poi analizzate una per una con l'aiuto del calcolatore, facendo vedere che ognuna di esse può essere colorata con quattro colori e deducendo da ciò che ogni mappa piana ha la stessa proprietà.

Siccome era impossibile verificare a mano i calcoli di Appell e Haken, molti matematici avanzarono dubbi sulla validità del metodo usato, o per lo meno lo trovarono insoddisfacente dal punto di vista epistemologico. Addirittura, il New York Times rifiutò di pubblicare un articolo sulla dimostrazione, temendo che potesse essere sbagliata come molte altre annunciate in precedenza.

Nel 1996, N. Robertson, P. Sanders, P. Seymour e R. Thomas diedero una nuova dimostrazione, basata sulle stesse idee di quella di Appell e Haken ma più efficiente, in quanto richiedeva l'analisi di "sole" 633 configurazioni. Ancora una volta, però, risultò impossibile verificare con carta e penna tutti i passaggi, e si dovette ricorrere al computer [RSST97].

Infine, nel 2005, B. Werner and G. Gonthier hanno implementato la dimostrazione del Teorema dei Quattro Colori nel linguaggio di programmazione (o, meglio, "theorem proving software") Coq, verificando la validità di ciascuno dei passi che la compongono [Gon08].

Riferimenti:

https://en.wikipedia.org/wiki/Four_color_theorem
http://mathworld.wolfram.com/Four-ColorTheorem.html

[AH77] K. Appel; W. Haken: Solution of the Four Color Map Problem, Scientific American, 237 (4), pp. 108–121 (1977)
[Gard3] M. Gardner: Enigmi e giochi matematici, vol 3.
[Gon08] G. Gonthier: Formal Proof—The Four-Color Theorem, Notices of the American Mathematical Society 55 (11), pp. 1382-1393 (2008).
[H1890] P. J. Heawood: Map-Colour Theorem, Quarterly Journal of Mathematics 24, 332–338 (1890).
[K1879] A. B. Kempe (1879): On the Geographical Problem of the Four Colours, American Journal of Mathematics  2 (3): 193–220.
[RSST97] N. Robertson; D. Sanders; P. Seymour; R. Thomas: The Four-Colour Theorem, J. Combin. Theory Ser. B 70 (1), pp. 2–44 (1977)doi:10.1006/jctb.1997.1750,