Qualche giorno fa Maxxfi mi ha chiesto cosa ne pensassi delle dimostrazioni matematiche fatte per mezzo del calcolatore. La mia laconica risposta è stata “brutte, ma valide”; provo ad aggiungere qualche considerazione in più.
Innanzitutto, bisogna mettersi d’accordo sui termini: cos’è una dimostrazione matematica al calcolatore? Lascio immediatamente da parte i programmi di intelligenza artificiale che dimostrano semplici teoremi, magari dandone nuove dimostrazioni, oppure se ne escono con nuovi teoremini non pubblicati in precedenza: quelle sono dimostrazioni del computer, e hanno la stessa validità degli esercizi che ci facevano fare nel biennio di matematica (forse un po’ meglio, se il programma è fatto bene e gli sono stati implementati correttamente gli algoritmi.
Esistono poi “dimostrazioni” che non lo sono affatto: prendiamo ad esempio il test di primalità di Miller-Rabin, che permette di verificare molto velocemente se un numero è presumibilmente primo. Un non matematico può pensare che se la probabilità che il numero testato non sia primo sia di 1 su 10¹⁰ ci si potrebbe anche accontentare, e in effetti molti programmi di crittografia usano questi probabili primi accettando il rischio che primi non siano e quindi si possa fare un attacco al testo crittografato; ma un matematico non potrà mai dire “quel numero è primo”.
Resta infine il gruppo di dimostrazioni al computer vere e proprie: quella archetipale è per il teorema dei quattro colori, che afferma che bastano quattro colori per colorare una qualunque mappa in modo che nessuna coppia di regioni confinanti (per un tratto, i singoli punti non contano) abbia lo stesso colore; ma ad esempio c’è stata anche quella della congettura di Keplero, che afferma che il miglior impacchettamento di sfere nello spazio tridimensionale è quello che faremmo tutti, facendo tanti strati a esagono uno sopra l’altro. Queste dimostrazioni, che gli anglofoni definiscono “computer assisted”, hanno una struttura comune. Il teorema è stato inizialmente analizzato e azzannato, e si è arrivati a dire che il caso generale si può ricondurre a un numero finito di sottocasi particolari; nel caso del teorema dei quattro colori si parla di 1476 mappe (grossine) distinte, mentre per la congettura di Keplero sono state ritenute necessarie più di 5000 configurazioni di sfere. In questi casi, il calcolatore serve a verificare che nessuna di queste mappe/configurazioni invalidi il teorema: un lavoro che in linea puramente teorica si potrebbe fare a mano, ma richiederebbe non so quante centinaia d’anni, e si rischierebbe di fare degli errori (tenetevi a mente questa frasetta).
L’atteggiamento dei matematici rispetto a queste dimostrazioni al calcolatore è prettamente filosofico. Alcuni non le considerano valide perché affermano che la dimostrazione deve essere comprensibile a un essere umano, e se non ci si può mettere a verificare tutti i casi allora la dimostrazione in verità non esiste. Altri hanno una preclusione più di principio: come ci si può assicurare che l’algoritmo usato sia corretto, e il programma per computer lo implementi correttamente? Altri ancora, credo la maggioranza, non si fanno di questi problemi e prendono il teorema per dimostrato.
La mia visione personale? Come credo abbiate capito, non ho nessun problema ideologico su una dimostrazione assistita dal computer. Per quanto riguarda la correttezza degli algoritmi, si può ovviare alla cosa implementando indipendentemente più programmi su più architetture diverse – in effetti per il teorema dei quattro colori hanno fatto così – e verificando che l’output sia lo stesso. D’altronde, non è che le dimostrazioni umane siano scevre da errori: proprio il teorema dei quattro colori era stato “dimostrato” nel 1879 salvo poi accorgersi nel 1890 che la dimostrazione era errata. Insomma, la correttezza degli algoritmi e la correttezza delle dimostrazioni sono in fin dei conti la stessa cosa. Nel caso poi degli algoritmi probabilistici di cui sopra, c’è persino chi afferma che se la probabilità che l’algoritmo non ci prenda sia inferiore a quella di un errore hardware della macchina allora si ha la certezza, ma è una linea di pensiero che non mi ispira molto, a meno di pensare anche che tutti gli esseri umani possano venire ipnotizzati contemporaneamente ;-)
Detto tutto questo, resta il mio giudizio lapidario iniziale: il teorema è sì dimostrato, ma la dimostrazione è così brutta che un Vero Matematico se ne fa ben poco, come diceva anche Erdős. Non è detto che esista una dimostrazione “bella” di questi teoremi; visto però che questi teoremi non sono fondamentali nel senso di essere alla base di tanta matematica si può anche decidere di non contarla come dimostrazione dal punto di vista estetico. A voi la scelta!