I recenti sviluppi dell’informatica, e in particolare del machine learning, aprono le porte a molte riflessioni sulla natura dell’intelligenza, dell’apprendimento, della conoscenza. Il titolo di un articolo pubblicato recentemente su Quanta Magazine, “Quanto manca ai computer per automatizzare il ragionamento matematico?”, mi sembra però quasi una domanda fallace, per dirla con i logici medievali, se prima non ci si interroga su che cosa sia un ragionamento matematico.

A questo fine, care lettrici e cari lettori, procederò socraticamente ponendovi tre domande.

*  *  *

1° Domanda. Quanti modi ci sono di risolvere il Sudoku?

Certamente vi sarete cimentati con il Sudoku, gioco geniale di cui si può godere sia su un quotidiano giapponese che su uno norvegese, pur essendo ignoranti delle rispettive lingue. Consiste in una griglia 9×9 nelle cui caselle appaiono sparse alcune cifre, da 1 a 9. L’obiettivo è completare la griglia in modo che in ogni riga, in ogni colonna e in ognuno dei 9 quadratini 3×3, nei quali si può decomporre il quadrato più grande, ogni cifra da 1 a 9 compaia esattamente una volta. Ci sono due modi di risolvere il Sudoku: con la matita e la gomma, oppure con la penna. Nel primo caso, si procede per tentativi, cancellando le cifre che avevamo scritto in modo provvisorio quando ci portano a un vicolo cieco, e sostituendole con altre diverse. Nel secondo caso, si scrive un numero solamente quando si è assolutamente certi che sia corretto (in verità, anche in questo secondo caso si possono annotare nel quadratino più numeri che via via si andranno a escludere, ma comunque si scrivono solo informazioni certe e mai provvisorie).

Dove cominciare?

La domanda che vi pongo è dunque la seguente. “Poiché si giunge in ogni caso alla soluzione, che differenza c’è tra i due modi di affrontare il gioco?”. Non si accettano risposte psicologiche del tipo “Ma nell’altro modo non c’è gusto”, “È una questione di ragionamento”… Appunto voglio che si spieghi quali siano le implicazioni di un ragionamento matematico. Pensateci un attimo prima di continuare a leggere.

Ed ecco la risposta. La differenza è che nel secondo caso avete dimostrato qualcosa, e cioè che c’è un’unica soluzione! Per convincervi, pensate a cosa avreste fatto (sempre nel secondo caso) se vi avessero dato da completare una griglia assolutamente bianca. Niente. Non avreste saputo da dove cominciare. Un automa che dovesse risolvere il Sudoku con un algoritmo di backtracking per tentativi ed errori, l’equivalente di matita e gomma, ne avrebbe invece trovata almeno una.

*  *  *

2°Domanda. Quanti modi ci sono di impacchettare le sfere?

Quando andate al mercato, fateci caso; ci sono due modi ottimali di sistemare le mele – intese come sfere – in modo compatto ad ogni strato: l’impacchettamento esagonale e quello cubico a facce centrate. Keplero (quello delle leggi di Keplero) si chiese se quelli fossero gli unici modi ottimali possibili. Ebbene, per quasi 4 secoli nessuno riuscì a trovare un modo migliore per sistemare le mele, o a dimostrare che non ce ne fossero altri. Finalmente, nel 1998, Thomas Hales dimostrò che i fruttivendoli avevano trovato le soluzioni ottimali da alcune migliaia di anni senza saperlo. La prova di Hales era lunga alcuni gigabyte, e dopo quattro anni di analisi una dozzina di matematici se ne dichiarò convinta al 99%! Non era sufficiente, però. Da allora la dimostrazione è stata certificata usando un sistema interattivo e semi-automatico per la certificazione delle dimostrazioni, chiamato Isabelle.

Noiose (ma utili) certificazioni

I sistemi di certificazione – uno dei più famosi è Coq­ – si comportano come pedanti, tonti e noiosi matematici, come degli avvocati del diavolo, che obbligano a esplicitare tutte le ipotesi e assunzioni nascoste. Per esempio, in uno dei suoi passaggi, Hales aveva usato l’espressione favorita dai matematici: “Senza perdita di generalità, ci si può restringere al caso di …”. Isabelle si accorse che l’assunzione non era giustificata, perché nel farlo si potevano perdere dei casi. Una volta individuata, quella falla nel ragionamento fu poi risolta insieme a tanti altri errori minori.

Questo vuol dire che i matematici saranno sostituiti dalle macchine? No, perché in realtà Isabelle e Coq automatizzano molto poco del processo logico, al di là di utilizzare efficientissimi sistemi di analisi per casi.

Bachi costosi

Tornando al problema di Keplero, quello che Hales ha fatto è stato dimostrare che non ci sono soluzioni aggiuntive rispetto a quelle trovate dai fruttivendoli. Ma allora ci si può chiedere: “Che cosa ci si guadagna a dimostrare una cosa negativa, quando bastava andare al mercato per trovare la soluzione?” La risposta a questa domanda è semplice: dimostrare che qualcosa non c’è non solo è concettualmente importante, ma è anche utilissimo se quel qualcosa è un errore, o un bug (in italiano “baco”, ndj), come si dice in informatica. Ci sono molti settori dell’automazione, come l’avionica, in cui un errore può mettere a repentaglio la vita. E dove non è a rischio la vita, può esserlo la reputazione o il bilancio di un’azienda. Il caso più noto è il Pentium bug, che costò oltre mezzo miliardo di dollari alla Intel nel 1994. La legge di Murphy è sempre in agguato in informatica: “Se qualcosa può andare storto, ci andrà sicuramente”: dal Mariner 1 nel 1962 (e il suo trattino che impressionò lo scrittore Arthur C. Clarke) al razzo Ariane 5 nel 1996, ci sono stati via via negli anni tanti casi nei quali si sarebbe fatto meglio a essere un po’ più pedanti nel certificare il software.

Evanescenti certezze

Spero di avervi convinto del perché sia utile dimostrare che certe cose non esistono. In verità, non possiamo mai avere la certezza al 100% dell’esattezza di una certificazione. Il motivo è profondo. Non possiamo dimostrare che il modo nel quale abbiamo formalizzato il comportamento di un dispositivo sia veramente fedele alla realtà. Non si può infatti dimostrare formalmente la correttezza di una formalizzazione: questo è sempre un passaggio soggetto a una certa soggettività. La certificazione riduce però il rischio.

*  *  *

3° Domanda. Che cos’è una dimostrazione?

Una delle prime dimostrazioni della storia fu quella di Euclide sul fatto che i numeri primi sono infiniti. In poche parole: “Se i numeri primi fossero finiti, potremmo farne il prodotto e sommargli 1. Questo numero non sarebbe quindi divisibile per nessuno dei numeri primi noti, perché la divisione darebbe sempre come resto 1. Ma allora ci sarebbe un numero primo che non sta nella lista iniziale, ovvero il numero stesso o un suo divisore, contraddicendo l’ipotesi. Dunque, i numeri primi devono essere infiniti”.

Algoritmi nascosti

Che cosa ci insegna questo esempio? La risposta è il nodo matematico forse più importante e innovativo rispetto alla nostra intuizione di che cosa sia una dimostrazione. Qui ci vorrebbe un altro post o forse un network di post ancora più complesso dei precedenti. Si può dare l’idea rapidamente, però: ogni dimostrazione nasconde in grembo un algoritmo. Nell’esempio di Euclide, la procedura dissimulata nella dimostrazione è quella che permette di trovare un numero i cui fattori primi sono tutti diversi da quelli di qualsiasi lista data a priori.

*  *  *

Tornando alla domanda iniziale…

Tornando alla domanda dalla quale siamo partiti, se la poniamo in termini di algoritmi (“Quanto si sta riducendo la distanza tra gli algoritmi implementati e le dimostrazioni matematiche?”), una risposta provocatoria e paradossale sarebbe dunque: la distanza tra gli algoritmi implementati e le dimostrazioni matematiche non si sta riducendo affatto, in quanto sono due facce della stessa medaglia!