Dimostrazioni umane?

Un paio di settimane fa Paolo Marino mi ha segnalato questo articolo in cui Sir Andrew Wiles (quello della dimostrazione dell’Ultimo teorema di Fermat, per chi non se lo ricordasse) parla di come lui vede le dimostrazioni di teoremi fatte al computer. Senza volere certo paragonarmi a Wiles, provo a raccontare come la penso io. Vi anticipo subito che non dirò nulla di definitivo o troppo specifico.

Per prima cosa, bisogna mettere in chiaro che “dimostrazione al computer” può significare varie cose. Il grande pubblico – “grande” si fa per dire – ha scoperto questo concetto quando Kenneth Appel e Wolfgang Haken annunciarono di avere dimostrato il Teorema dei quattro colori usando un computer per verificare tutte le possibili configurazioni. Detta così però la cosa non è affatto vera: quello che i due matematici in realtà fecero fu dimostrare (a mano, con qualche centinaio di pagine di testo) che esisteva un certo (grande) numero di “configurazioni inevitabili”, nel senso che se ci fosse stato un controesempio al teorema doveva contenere almeno una di tali configurazioni. La parte al computer è servita a dimostrare che a partire da ciascuna configurazione inevitabile se ne poteva ricavare una con un numero minore di regioni che avrebbe fatto da controesempio, il che era assurdo per ipotesi. Una dimostrazione di questo tipo è essenzialmente esaustiva: non nel senso che ci si esaurisce per farla ma che si limita a fare tanti, tanti calcoli che un essere umano non riesce a verificare ma un computer sì. Certo, il programma che fa questi conti potrebbe avere dei bachi: e infatti la dimostrazione è stata fatta usando due computer con architetture hardware diverse, ciascuno dei quali usava un algoritmo essenzialmente diverso scritto da persone diverse. In questo modo la probabilità di avere un errore si riduce essenzialmente a zero, ed è minore di quello di un errore in una dimostrazione “umana”. Ricordo tra l’altro che proprio il teorema dei quattro colori si è creduto essere stato dimostrato tra il 1879 e il 1890, prima che ci si accorgesse che la dimostrazione non era completa.

Nel campo dell’intelligenza artificiale esiste però un altro concetto di dimostrazione al computer, ed è quella nel quale il computer applica una serie di passaggi logici per arrivare dalle ipotesi di un teorema alla tesi. Questo, se ho ben capito, è il vero tema dell’articolo di Spektrum, e qui la cosa diventa in effetti più interessante. I Principia Mathematica funzionano in un certo senso in quel modo: è notorio che per arrivare a dimostrare che 1+1=2 occorre arrivare a pagina 379 (nella prima edizione dell’opera: la seconda ha usato qualche scorciatoia e dà la dimostrazione a pagina 362). Di nuovo, i singoli passi della dimostrazione sono chiaramente comprensibili a un essere umano, ma non credo che costui riesca a concepire la dimostrazione complessiva. Noi siamo abituati a saltare passaggi su passaggi, chi più chi meno: è vero che quello che per alcuni è uno “sketch of proof” per altri è una dimostrazione completa, ma anche la dimostrazione più pedante dà per scontati una serie di passaggi logici che non abbiamo certo voglia di esplicitare. Del resto, a meno che non ci chiamiamo Tristram Shandy, nemmeno nella vita reale specifichiamo mai completamente tutto quello che dobbiamo fare, no?

Il vero problema che potremo avere nel futuro è proprio questo. Un teorema dimostrato per esaustione è un conto: un tipico matematico storcerà il naso dicendo che la dimostrazione non è elegante, magari potrà mettersi a cercarne una migliore, ma il più delle volte se ne farà una ragione. In fin dei conti la sostanza gli è chiara, e la parte al computer sono meri dettagli tecnici. Ma un computer che fa una dimostrazione logica la potrà fare in maniera completamente incomprensibile per noi ad alto livello (ripeto: i singoli passi saranno sempre comprensibili). Questo perché noi umani ci organizziamo tipicamente per imitazione degli altri umani, e quindi abbiamo una linea comune di pensiero. Non è un caso che Ramanujan, che non aveva questa educazione formale e anzi non aveva inizialmente nemmeno chiaro il concetto di dimostrazione, fu inizialmente snobbato da tutti, e Hardy decise di andare più a fondo solo perché ritenne che nessuno si sarebbe potuto inventare quegli enunciati, e che valeva la pena di verificare se fossero dimostrabili oppure no. Un computer non opera per imitazione, lo vediamo con i sistemi di intelligenza artificiale che “imparano a giocare” a scacchi o a go e dei quali non abbiamo alcuna idea riguardo alla loro configurazione interna o al motivo per cui ogni tanto scelgono delle mosse incomprensibili. Se un computer facesse una dimostrazione che richiede decine di migliaia di passi logici dei quali noi non capiamo la logica sottostante, potremmo riconoscere che la dimostrazione è corretta – ci sono tecniche standard per validare una dimostrazione – e quindi il teorema è vero, ma non sapremmo affatto il perché è vero. Finiremmo insomma nella situazione di chi sta vincendo a un gioco di cui non riesce a capire le regole, cosa che per un matematico è una tragedia immane, visto che dal suo punto di vista il vero scopo della matematica è appunto trovare le regole. È bellissimo avere una struttura per un edificio più leggera e allo stesso tempo più robusta di quelle classiche, e un ingegnere giustamente non si preoccupa di come sia stata trovata tale struttura: ma un matematico si sentirà a disagio. È vero che questo scenario non pare ancora prossimo: ma ci pensate? Tra i tanti lavori che l’automazione soppianterà, potrebbe esserci anche quello del matematico!

Mostra commenti ( )