Teorema dei quattro colori: la mappa che ridisegnò il concetto di dimostrazione

Prendete una qualsiasi cartina geografica — le regioni d'Italia, i dipartimenti della Francia, gli Stati degli USA — e provate a colorarla in modo che due territori confinanti non abbiano mai la stessa tinta. Quanti colori vi servono al minimo? La risposta, sorprendentemente, è sempre la stessa: quattro. È il teorema dei quattro colori, uno dei risultati più celebri e controversi della matematica moderna, perché fu il primo grande teorema a essere dimostrato con l'aiuto decisivo di un computer.

L'enunciato è ingannevolmente semplice: ogni mappa disegnata su un piano (o su una sfera) può essere colorata con non più di quattro colori in modo che regioni adiacenti, cioè che condividono un tratto di confine, abbiano colori diversi. Toccarsi in un solo punto, come gli angoli di un mosaico, non conta come adiacenza.

Un problema nato da un colorista

La congettura nacque nel 1852 da un'osservazione pratica. Francis Guthrie, uno studente che stava colorando la mappa delle contee inglesi, notò che gli bastavano quattro colori e si chiese se fosse sempre così. Girò la domanda al fratello, che la passò al matematico Augustus De Morgan, e da lì il problema entrò nella grande matematica. Come ricorda la voce della Encyclopædia Britannica, per oltre un secolo il teorema resistette a ogni tentativo di dimostrazione, pur sembrando "ovviamente vero" a chiunque si mettesse a colorare.

Nel 1879 Alfred Kempe pubblicò una prova che fu accettata per undici anni, finché Percy Heawood non vi trovò un errore fatale nel 1890. L'idea di Kempe, però, non era sprecata: conteneva il concetto di configurazione riducibile che sarebbe stato la chiave della soluzione finale.

1976: il teorema e il computer

La svolta arrivò all'Università dell'Illinois. Kenneth Appel e Wolfgang Haken ridussero il problema infinito di "tutte le mappe possibili" a un insieme finito di casi critici: dimostrarono che ogni mappa deve contenere almeno una di 1.936 configurazioni inevitabili (poi ridotte a 1.482), e che ciascuna di queste è "riducibile", cioè non può essere il controesempio più piccolo. Verificare a mano migliaia di configurazioni era impensabile, così affidarono il controllo a un calcolatore, che lavorò per circa 1.200 ore. Nel giugno 1976 annunciarono la prova; l'ufficio postale dell'università celebrò l'evento con un timbro che diceva "Four colors suffice", quattro colori bastano. La dimostrazione completa apparve nel 1977 sull'Illinois Journal of Mathematics.

Una dimostrazione che fece arrabbiare i filosofi

Il risultato sollevò un terremoto. Una dimostrazione matematica era sempre stata, per definizione, qualcosa che una mente umana poteva seguire passo dopo passo. Qui invece una parte cruciale era un calcolo opaco, impossibile da verificare a mano da un singolo essere umano. Era ancora "matematica"? Alcuni filosofi della scienza sostennero che Appel e Haken avevano introdotto nella dimostrazione un elemento empirico, simile a un esperimento di laboratorio, e che bisognava "fidarsi" dell'hardware e del software come ci si fida di uno strumento.

Il dibattito spinse la comunità a cercare prove più solide. Nel 1997 Neil Robertson, Daniel Sanders, Paul Seymour e Robin Thomas pubblicarono una nuova dimostrazione semplificata sul Journal of Combinatorial Theory, con sole 633 configurazioni e un algoritmo più trasparente. E nel 2005 il matematico Georges Gonthier produsse una versione completamente formalizzata nell'assistente di prova Coq, in cui ogni singolo passaggio logico è controllato dalla macchina: oggi nessuno serio dubita più del teorema.

Dalle mappe alle reti

Il teorema dei quattro colori sembra un gioco da bambini, ma è un risultato profondo di topologia e di teoria dei grafi: ogni mappa si traduce in un grafo, dove ogni regione è un nodo e ogni confine un collegamento, e colorare la mappa equivale a colorare i nodi del grafo. Problemi identici si presentano nell'assegnazione delle frequenze ai ripetitori telefonici (perché due antenne vicine non interferiscano), nella programmazione degli orari scolastici e nella gestione dei registri di un processore.

La fiducia nella macchina

La formalizzazione completa realizzata da Georges Gonthier merita un approfondimento, perché è la risposta più diretta alle obiezioni filosofiche. In una relazione pubblicata sui Notices dell'American Mathematical Society, Gonthier spiegò di aver tradotto ogni singolo passaggio della dimostrazione — sia la parte logica sia il controllo delle configurazioni — in un linguaggio formale verificabile da un assistente di prova. Il computer, in questo caso, non si limita a "macinare conti": controlla la coerenza logica di ogni inferenza, eliminando la possibilità di errori umani nascosti, come quello che era sfuggito per undici anni nella prova di Kempe.

Il teorema dei quattro colori ha così aperto la strada a un nuovo modo di fare matematica. Altri risultati celebri hanno seguito la stessa via: la dimostrazione della congettura di Keplero sull'impacchettamento ottimale delle sfere, completata da Thomas Hales, è stata anch'essa verificata al computer dopo anni di lavoro. Oggi le dimostrazioni formali assistite sono un campo in piena espansione, e ciò che a metà degli anni Settanta sembrava un'eresia — accettare un teorema il cui controllo sfugge a una singola mente umana — è diventato uno strumento accettato, persino prestigioso.

Soprattutto, il teorema ha cambiato la storia della disciplina: ha inaugurato l'era delle dimostrazioni assistite dal calcolatore, oggi sempre più comuni, costringendo i matematici a ripensare cosa significhi davvero "essere certi" di qualcosa. Da una cartina geografica colorata da uno studente annoiato è nata una delle domande filosofiche più attuali sulla natura della conoscenza.