Le macchine stanno sostituendo l’uomo in diversi lavori. Se da una parte si pronosticano futuri distopici come in Matrix o Blade Runner, dall’altra molti ringraziano l’automatizzazione e la computerizzazione che fa risparmiare un sacco di tempo e fatica, basti pensare alle migliaia di calcoli necessari per le progettazioni. Uno degli ambiti in cui i computer si sono fatti largo è senza dubbio la matematica: vengono, infatti, ampiamente usati per le simulazioni e l’elaborazione di dati. Negli ultimi anni, tuttavia, stanno spuntando anche prove di teoremi o congetture basate sull’uso di computer. Siamo forse vicini a costruire il computer “Pensiero Profondo” del famoso “Guida Galattica Per Autostoppisti”?

Lo scorso maggio è stata pubblicata la prova del problema delle Terne Pitagoriche Booleane, trovata utilizzando i computer.
Per terna pitagorica si intendono tre numeri che soddisfano il teorema di Pitagora a2+b2= c2, come per esempio 3, 4 e 5 (32+42=9+16=25=52) ma anche 11, 60, 61 e 8, 15, 17.
Il problema delle Terne Pitagoriche Booleane chiede se sia possibile o meno dividere i numeri interi in due gruppi in modo tale che in nessuno di essi ci sia una terna pitagorica completa. Un buon modo per immaginarlo è prendere tutti i numeri interi e provare a colorarli di due colori differenti in modo tale che non ci sia una terna pitagorica tutta colorata con lo stesso colore. È questo il metodo usato dai ricercatori dell’Università di Swansea e dell’Università del Kentucky che ha portato alla prova che è possibile per i numeri fino a 7824, ma diventa impossibile da 7825 in su. Per provarlo sono state controllate tutte le 102300 possibili combinazioni di colori, ridotte ad appena un trilione usando varie proprietà e simmetrie dei numeri: un’impresa impossibile per qualunque umano, e proprio qui entrano in gioco i computer. Ma anche per il vostro laptop probabilmente sarebbe un compito troppo impegnativo, per questo è stato usato il supercomputer Stampede dell’Università del Texas, che con 800 processori ha impiegato ben due giorni per generare la risposta. La risposta non è stata una semplice risposta secca (“42”, per esempio), ma un’analisi dal peso record di 200 TB! Per fortuna gli autori hanno prodotto anche una versione “light” di 68 GB per controllare i risultati ottenuti e per permettere verifiche da ulteriori esperti. La prova delle Terne Pitagoriche Booleane ha surclassato il precedente record di dimensioni, detenuto da un caso particolare della congettura di Erdos, dal peso di appena 13 GB.

L’uso di computer per verificare una congettura risale a qualche decennio fa. Uno dei primi a essere stati sottoposti a questa procedura è stato un lontano parente del problema delle terne pitagoriche booleane: il teorema dei quattro colori.
Presentato intorno alla metà dell’ottocento, esso afferma che per colorare una superficie piana divisa in regioni connesse servono quattro colori affinché nessuna regione sia dello stesso colore di una adiacente, insomma se volete colorare un mappamondo politico vi servono almeno quattro colori. Sebbene fosse conosciuto da molto tempo, si ebbe una prova della veridicità del teorema solo nel 1976 per opera di Kenneth Appel e Wolfgang Haken, i quali provarono a far colorare al computer tutte le 1476 mappe a cui è stato ridotto il problema (partendo dall’infinito è una riduzione notevole).
La prova attraverso i computer è una vera dimostrazione matematica? I matematici rischiano di andare in pensione ed essere sostituiti da qualche androide? Per ora, possiamo dire di no. Le dimostrazioni matematiche, infatti, si basano su un ragionamento deduttivo che, partendo dalle ipotesi, arriva a dimostrare la tesi con un ragionamento coerente. I calcolatori, invece, provano solamente tutte le possibili combinazioni per confermare (o confutare) un teorema, ma non forniscono informazioni sul perché sia valido o meno. Per questo, nel 2005, venne prodotta una dimostrazione matematica del problema dei quattro colori (che ha quindi potuto prendere il nome di “teorema”) e si attende ancora quella per il problema delle terne pitagoriche booleane.

I matematici possono stare tranquilli: non rischiano di certo la pensione anticipata per colpa dei computer, e noi non possiamo ancora affidare a una macchina le nostre domande sulla vita, l’universo e tutto quanto.