Il teorema dei quattro colori è il primo risultato matematico dimostrato non da un essere umano ma da un computer. Questo teorema venne enunciato per la prima volta nel 1852 da Francis Guthriem, studente del matematico inglese Augustus De Morgan, che, accortosi che bastavano quattro colori per colorare una mappa delle contee britanniche, chiese al suo professore se ciò era sempre vero. Il primo tentativo di dimostrazione fu fatto nel 1879 da Alfred Kempe, seguito l’anno successivo da Peter Tait. Nel 1890 Percy Heawood si accorse che le due dimostrazioni erano sbagliate e propose un’altra dimostrazione che però dimostrava il teorema con cinque colori e non quattro. Nel 1977 due matematici dell’Università dell’Illinois, Kenneth Appel e Wolfgang Haken, scrissero un algoritmo informatico che dimostrava (costruttivamente) che tutte le infinite configurazioni delle mappe potevano essere ridotte ad un insieme di configurazioni di base (poco meno di duemila) tali che ciascuna di esse poteva essere colorata con solo quattro colori. I due matematici rivendicarono la dimostrazione del teorema che però sembrava fosse stato dimostrato non da un essere umano ma da un computer. In realtà non è proprio così. Il computer era stato usato come strumento per fare tutta una serie di conti impossibili per un essere umano (come quando usiamo una calcolatrice per fare delle operazioni aritmetiche). E’ vero però che a tutt’oggi non esiste una dimostrazione del teorema che possa essere seguita passo passo da un persona in carne e ossa. Secondo te questo fatto…